fact: Definition ac_elementary_solve_term_var_with_val_term pb f x_val list_of_terms l' list_of_equations : list matching_problem := match remove T.eq_bool x_val l' with | None => match x_val with | Var _ => nil | Term g ll => if F.Symb.eq_bool f g then match remove_list ll l' with | Some rmv => if le_gt_dec (length list_of_terms) (length rmv) then let t1' := build f list_of_terms in let t2' := build f rmv in let new_pb := mk_pb (existential_vars pb) (cons (t1',t2') list_of_equations) (solved_part pb) (partly_solved_part pb) in cons new_pb nil else nil | None => nil end else nil end | Some rmv => let t1' := build f 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.
imports: Coq(Arith List) CoLoR(more_list list_sort term_spec ac cf_eq_ac)