fact: Definition ac_elementary_solve_term_var_with_part_val_term pb f x_part_val list_of_terms l' list_of_equations : list matching_problem := if (F.Symb.eq_bool f (head_symb x_part_val)) then match remove T.eq_bool (closed_term x_part_val) l' with | None => nil | Some rmv => let t1' := build f (cons (Var (new_var x_part_val)) list_of_terms) in let t2' := build f rmv in let new_pb := mk_pb (existential_vars pb) ((t1',t2') :: list_of_equations) (solved_part pb) (partly_solved_part pb) in new_pb :: nil end else map_without_repetition T.eq_bool (fun t => match t with | Term h l''' => if F.Symb.eq_bool h (head_symb x_part_val) then match remove T.eq_bool (closed_term x_part_val) l''' with | None => None | Some rmv => match remove T.eq_bool t l' with | None => None | Some rmv2 => let y := new_var x_part_val in let y_val := build h rmv in let t1' := build f list_of_terms in let t2' := build f rmv2 in let new_pb := mk_pb (existential_vars pb) ((Var y, y_val) :: (t1',t2') :: list_of_equations) (solved_part pb) (partly_solved_part pb) in Some new_pb end end else None | Var _ => None end) l'.
imports: Coq(Arith List) CoLoR(more_list list_sort term_spec ac cf_eq_ac)