fact: Definition ac_elementary_solve pb t1 t2 list_of_equations := match t1, t2 with | (Term f (s :: list_of_terms as l)), (Term _ l') => match s with | Term g lg => ac_elementary_solve_term_term_term pb f g lg list_of_terms l' list_of_equations | Var x => match find X.eq_bool x (solved_part pb) with | Some x_val => ac_elementary_solve_term_var_with_val_term pb f x_val list_of_terms l' list_of_equations | None => match find X.eq_bool x (partly_solved_part pb) with | Some x_part_val => ac_elementary_solve_term_var_with_part_val_term pb f x_part_val list_of_terms l' list_of_equations | None => ac_elementary_solve_term_var_without_val_term pb f x list_of_terms l' list_of_equations end end end | (Term _ nil), (Term _ _) => let new_pb := mk_pb (existential_vars pb) list_of_equations (solved_part pb) (partly_solved_part pb) in new_pb :: nil | _, _ => nil end.
imports: Coq(Arith List) CoLoR(more_list list_sort term_spec ac cf_eq_ac)