# Library ac_matching.matching_complete

``` Add LoadPath "basis". Add LoadPath "list_extensions". Add LoadPath "term_algebra". Add LoadPath "term_orderings". Require Import Arith. Require Import List. Require Import more_list. Require Import list_sort. Require Import term. Require Import ac. Require Import cf_eq_ac. Require Import matching_sound. Module Type S. Declare Module Import SMatching : matching_sound.S. Import WFMMatching. Import WFMatching. Import Matching. Import Cf_eq_ac. Import Ac. Import EqTh. Import T. Axiom solve_is_complete :   forall pb, well_formed_pb pb -> forall sigma, is_well_formed_sol pb sigma ->   match pb.(unsolved_part) with   | nil => True     | _ :: _ => exists pb', In pb' (solve pb) /\ is_well_formed_sol pb' sigma   end. End S. Module Make (SMatching1 : matching_sound.S) :  S with Module SMatching := SMatching1. Module Import SMatching := SMatching1. Import WFMMatching. Import WFMatching. Import Matching. Import Cf_eq_ac. Import Ac. Import EqTh. Import T. Import F. Import X. Import Sort. Import LPermut. Lemma remove_a_subterm :   forall sigma f v l1 t l2, arity f = AC -> well_formed_cf_subst sigma ->   well_formed_cf (Term f (Var v :: l1)) ->   well_formed_cf (Term f l2) ->   apply_cf_subst sigma (Var v) = t ->   apply_cf_subst sigma (Term f (Var v :: l1)) = Term f l2 ->   match remove _ eq_term_dec t l2 with   | None =>         match t with         | Var _ => False         | Term g _ => f=g         end   | Some rmv => apply_cf_subst sigma (build f l1) = build f rmv   end. Proof. intros sigma f v l1 t l2 Ar W_sigma Wt1 Wt2 v_sigma t1_sigma; generalize (in_remove _ eq_term_dec t l2); destruct (remove _ eq_term_dec t l2) as [l2''' | ]. intros [cp1 [l2' [l2'' [ H'' [l2_eq l2'''_eq]]]]]; subst cp1. injection l2'''_eq; clear l2'''_eq; intro; subst l2 l2'''; apply flatten_cf with f; trivial. apply well_formed_cf_apply_subst; trivial; apply well_formed_cf_build_cons with (Var v); trivial. apply well_formed_cf_build_inside with t; trivial. setoid_rewrite <- (flatten_apply_cf_subst sigma l1 Ar); setoid_rewrite (flatten_build (l2' ++ l2'') Ar). intros s s_in_l2'_l2''; destruct (in_app_or _ _ _ s_in_l2'_l2'') as [s_in_l2' | s_in_l2'']; apply (well_formed_cf_alien Ar Wt2); apply in_or_app; [left | right; right]; trivial. setoid_rewrite (permut_app1 (t :: nil)). transitivity (l2' ++ t :: l2''). simpl in t1_sigma; rewrite Ar in t1_sigma; simpl in v_sigma; rewrite v_sigma in t1_sigma; inversion_clear t1_sigma; apply permut_sym; apply quick_permut_bis. destruct t as [ x | g ll]. apply permut_refl. destruct (eq_symbol_dec f g) as [f_eq_g | _]. absurd (f=g); trivial. apply (well_formed_cf_alien Ar Wt2 (Term g ll)). apply in_or_app; right; left; trivial. apply permut_refl. simpl; apply permut_sym; setoid_rewrite <- permut_cons_inside; auto. reflexivity. intros t_not_in_l2; simpl in t1_sigma; rewrite Ar in t1_sigma; simpl in v_sigma; rewrite v_sigma in t1_sigma; inversion t1_sigma. destruct t as [x | g ll]. apply (t_not_in_l2 (Var x)); subst l2; trivial. setoid_rewrite <- (list_permut.in_permut_in (quick_permut (Var x :: flatten f (map (apply_cf_subst sigma) l1)))); left; trivial. destruct (eq_symbol_dec f g); trivial. absurd (In (Term g ll) l2); trivial. intro H; apply (t_not_in_l2 (Term g ll)); trivial. subst l2; setoid_rewrite <- (list_permut.in_permut_in (quick_permut (Term g ll :: flatten f (map (apply_cf_subst sigma) l1)))). left; trivial. Qed. Lemma remove_several_subterms :   forall sigma f v l1 t l2, arity f = AC -> well_formed_cf_subst sigma ->   well_formed_cf (Term f (Var v :: l1)) ->   well_formed_cf (Term f l2) ->   apply_cf_subst sigma (Var v) = t ->   apply_cf_subst sigma (Term f (Var v :: l1)) = Term f l2 ->   match t with   | Var _ => True   | Term g l0 =>      if eq_symbol_dec f g      then        match remove_list l0 l2 with        | None => False        | Some l3 =>          if le_gt_dec (length l1) (length l3)          then apply_cf_subst sigma (build f l1) = build f l3          else False        end      else True   end. Proof. intros sigma f v l1 t l2 Ar W_sigma Wt1 Wt2 v_sigma t1_sigma; destruct t as [ x | g ll]; trivial. destruct (eq_symbol_dec f g) as [f_eq_g | f_diff_g]; [subst g | trivial]. assert (W_v : well_formed_cf (Var v)). simpl; trivial. assert (W_v_sigma := well_formed_cf_apply_subst W_sigma _ W_v); rewrite v_sigma in W_v_sigma. generalize (in_remove_list (well_formed_cf_sorted Ar W_v_sigma)                     (well_formed_cf_sorted Ar Wt2)). unfold EDS.A, DOS.A in *; destruct (remove_list ll l2) as [l2' | ]. unfold EDS.A, DOS.A in *; intro P; elim (le_gt_dec (length l1) (length l2')); intro L. assert (Al_l2' : forall t, In t l2' -> match t with Var _ => True | Term g _ => f <> g end). intros t In_t; apply (well_formed_cf_alien Ar Wt2). setoid_rewrite <- (list_permut.in_permut_in P). apply in_or_app; right; trivial. apply flatten_cf with f; trivial. apply well_formed_cf_apply_subst; trivial; apply well_formed_cf_build_cons with (Var v); trivial. apply well_formed_cf_build; trivial. apply le_trans with (length l1); trivial. apply le_S_n; generalize (well_formed_cf_length Ar Wt1); trivial. intros t In_t; apply (well_formed_cf_subterms Wt2). setoid_rewrite <- (list_permut.in_permut_in P); apply in_or_app; right; trivial. setoid_rewrite <- (flatten_apply_cf_subst sigma l1 Ar); setoid_rewrite (flatten_build l2' Ar Al_l2'). setoid_rewrite (permut_app1 ll). transitivity l2. simpl in t1_sigma; rewrite Ar in t1_sigma. inversion_clear t1_sigma. simpl in v_sigma; rewrite v_sigma. destruct (eq_symbol_dec f f) as [_ | f_diff_f]; [idtac | absurd (f=f); trivial]. apply quick_permut. symmetry; trivial. generalize (plus_lt_compat_l _ _ (length ll) L). rewrite <- length_app; assert (L' := list_permut.permut_length P); unfold EDS.A, DOS.A in *; rewrite L'; clear L'. simpl in t1_sigma; rewrite Ar in t1_sigma. inversion_clear t1_sigma; rewrite length_quicksort; simpl in v_sigma; rewrite v_sigma; destruct (eq_symbol_dec f f) as [_ | f_diff_f]; [idtac | absurd (f=f); trivial]. rewrite length_app; intro L'; assert (L'' := plus_lt_reg_l _ _ (length ll) L'); clear L L'. absurd (length l1 < length l1); auto with arith. refine (le_lt_trans _ _ _ _ L''). rewrite <- (length_map (apply_cf_subst sigma)). apply length_flatten_bis; trivial. intros t' t'_in_map_l1; setoid_rewrite in_map_iff in t'_in_map_l1; destruct t'_in_map_l1 as [t [Wt t_sigma]]. subst; apply well_formed_cf_apply_subst; trivial. apply (well_formed_cf_subterms Wt1); right; trivial. intro P; apply (P (flatten f (map (apply_cf_subst sigma) l1))); simpl in v_sigma; simpl in t1_sigma; rewrite Ar in t1_sigma; rewrite v_sigma in t1_sigma; inversion_clear t1_sigma. simpl; trivial; destruct (eq_symbol_dec f f) as [ _ | f_diff_f]; [idtac | absurd (f=f); trivial]. apply quick_permut; auto. Qed. Lemma remove_several_subterms_bis :   forall sigma f v v' l1 t l2, arity f = AC -> well_formed_cf_subst sigma ->   well_formed_cf (Term f (Var v :: l1)) ->   well_formed_cf (Term f l2) ->   apply_cf_subst sigma (Var v) =      Term f (quicksort (flatten f (apply_cf_subst sigma (Var v') :: t :: nil))) ->   apply_cf_subst sigma (Term f (Var v :: l1)) = Term f l2 ->   match t with | Var _ => True | Term g _ => f<>g end ->   match remove _ eq_term_dec t l2 with   | None => False   | Some l3 => apply_cf_subst sigma (build f (Var v' :: l1)) = build f l3   end. Proof. intros sigma f v v' l1 t l2 Ar W_sigma Wt1 Wt2 v_sigma t1_sigma. generalize (in_remove _ eq_term_dec t l2); destruct (remove _ eq_term_dec t l2) as [l2''' | ]. intros [cp1' [l2' [l2'' [ H'' [l2_eq l2'''_eq]]]]] Al_t. injection l2'''_eq; clear l2'''_eq; intro l2'''_eq; apply flatten_cf with f; trivial. apply well_formed_cf_apply_subst; trivial; apply well_formed_cf_build; trivial. simpl; auto with arith. intros s [s_eq_v' | s_in_l1]; [subst; simpl | apply (well_formed_cf_subterms Wt1); right]; trivial. intros s [s_eq_v' | s_in_l1]; [subst; simpl | apply (well_formed_cf_alien Ar Wt1); right]; trivial. subst l2 l2'''; apply well_formed_cf_build_inside with t; subst; trivial. setoid_rewrite <- (flatten_apply_cf_subst sigma (Var v' :: l1) Ar); setoid_rewrite (flatten_build l2''' Ar). subst l2 l2'''; intros s s_in_l2'_l2''; destruct (in_app_or _ _ _ s_in_l2'_l2'') as [s_in_l2' | s_in_l2'']; apply (well_formed_cf_alien Ar Wt2); apply in_or_app; [left | right; right]; trivial. setoid_rewrite (@permut_cons t t). reflexivity. transitivity (l2' ++ t :: l2''). pattern (Var v :: l1) in t1_sigma; simpl in t1_sigma; rewrite Ar in t1_sigma. pattern (Var v') in v_sigma; simpl apply_cf_subst in v_sigma.  rewrite v_sigma in t1_sigma; clear v_sigma. destruct (eq_symbol_dec f f) as [_ | f_diff_f]; [idtac | absurd (f=f); trivial]. assert (Inj : forall l' l'', Term f l' = Term f l'' -> l' = l''). intros l' l'' H'; injection H'; intros; subst; trivial. subst l2 cp1'; rewrite <- (Inj _ _ t1_sigma); clear Inj. apply permut_sym; apply quick_permut_bis. transitivity   (flatten f (apply_cf_subst sigma (Var v') :: t :: nil) ++    flatten f (map (apply_cf_subst sigma) l1)). setoid_rewrite <- permut_app2; apply quick_permut_bis; auto. replace (flatten f (map (apply_cf_subst sigma) (Var v' :: l1))) with ((flatten f (apply_cf_subst sigma (Var v') :: nil)) ++         flatten f (map (apply_cf_subst sigma) l1)); [ rewrite app_comm_cons | rewrite <- flatten_app; trivial]. setoid_rewrite <- permut_app2. replace (flatten f (apply_cf_subst sigma (Var v') :: t :: nil)) with ((flatten f (apply_cf_subst sigma (Var v') :: nil) ++ flatten f (t :: nil))); [idtac | rewrite <- flatten_app; simpl app; trivial]. replace (flatten f (t :: nil)) with (t :: nil). apply permut_sym; setoid_rewrite <- permut_cons_inside. reflexivity. rewrite <- app_nil_end; auto. simpl; destruct t as [x | g ll]; trivial. destruct (eq_symbol_dec f g) as [f_eq_g | _]; [absurd (f=g) | idtac]; trivial. apply permut_sym; setoid_rewrite <- permut_cons_inside; subst; auto. reflexivity. intros Not_in Al_t; pattern (Var v :: l1) in t1_sigma; simpl in t1_sigma; rewrite Ar in t1_sigma. pattern (Var v') in v_sigma; simpl apply_cf_subst in v_sigma. rewrite v_sigma in t1_sigma; clear v_sigma. destruct (eq_symbol_dec f f) as [_ | f_diff_f]; [idtac | absurd (f=f); trivial]. assert (Inj : forall l' l'', Term f l' = Term f l'' -> l' = l''). intros l' l'' H'; injection H'; intros; subst; trivial. rewrite <- (Inj _ _ t1_sigma) in Not_in; clear Inj. apply (Not_in _ (refl_equal _)). setoid_rewrite <- in_quick_in. apply in_or_app; left. setoid_rewrite <- in_quick_in. replace (flatten f (apply_cf_subst sigma (Var v') :: t :: nil)) with (flatten f (apply_cf_subst sigma (Var v') :: nil) ++ flatten f (t :: nil)). apply in_or_app; right; destruct t as [x | g ll]; simpl. left; trivial. destruct (eq_symbol_dec f g) as [f_eq_g | _]; [absurd (f=g) | left ]; trivial. rewrite <- flatten_app; simpl app; trivial. Qed. Lemma remove_several_subterms_bis_nil :   forall sigma f v v' t l2, arity f = AC -> well_formed_cf_subst sigma ->   well_formed_cf (Term f l2) ->   apply_cf_subst sigma (Var v) =      Term f (quicksort (flatten f (apply_cf_subst sigma (Var v') :: t :: nil))) ->   apply_cf_subst sigma (Var v) = Term f l2 ->   match t with | Var _ => True | Term g _ => f<>g end ->   match remove _ eq_term_dec t l2 with   | None => False   | Some l3 => apply_cf_subst sigma (Var v') = build f l3   end. Proof. intros sigma f v v' t l2 Ar W_sigma Wt2 v_sigma t1_sigma Al_t; generalize (in_remove _ eq_term_dec t l2); destruct (remove _ eq_term_dec t l2) as [l2''' | ]. intros [cp1 [l2' [l2'' [ H' [l2_eq l2'''_eq]]]]]. injection l2'''_eq; clear l2'''_eq; intro l2'''_eq; subst l2 l2'''; apply flatten_cf with f; trivial. apply well_formed_cf_apply_subst; trivial; simpl; trivial. apply well_formed_cf_build_inside with t; subst; trivial. apply permut_trans with (l2' ++ l2''). setoid_rewrite (@permut_cons t t). reflexivity. apply permut_trans with (l2' ++ t :: l2''). assert (H:= trans_eq (sym_eq v_sigma) t1_sigma). assert (Inj : forall l' l'', Term f l' = Term f l'' -> l' = l''). intros l' l'' H''; injection H''; intros; subst; trivial. subst cp1; rewrite <- (Inj _ _ H); clear Inj. apply permut_sym; apply quick_permut_bis. apply permut_trans with (flatten f (apply_cf_subst sigma (Var v') :: nil) ++ flatten f (t :: nil)). rewrite <- flatten_app; simpl app; apply permut_refl. refine (permut_trans (list_permut_app_app _ _) _). simpl; destruct t as [ x | g ll ]; [apply permut_refl | idtac]. destruct (eq_symbol_dec f g) as [f_eq_g | _]; [absurd (f=g); trivial | apply permut_refl ]. apply permut_sym; setoid_rewrite <- permut_cons_inside; reflexivity. apply permut_sym; apply flatten_build_inside with t; subst cp1; trivial. intros Not_in; apply (Not_in _ (refl_equal _)). assert (H := trans_eq (sym_eq v_sigma) t1_sigma). assert (Inj : forall l' l'', Term f l' = Term f l'' -> l' = l''). intros l' l'' H'; injection H'; intros; subst; trivial. rewrite <- (Inj _ _ H); clear Inj. setoid_rewrite <- in_quick_in. assert (H':= flatten_app f (apply_cf_subst sigma (Var v') :: nil) (t :: nil)). simpl in H'; simpl; rewrite H'; apply in_or_app; right. destruct t as [ x | g ll ]; simpl; [left; trivial | idtac]. destruct (eq_symbol_dec f g) as [f_eq_g | _]; [absurd (f=g) | left ]; trivial. Qed. Lemma solve_is_complete :   forall pb, well_formed_pb pb -> forall sigma, is_well_formed_sol pb sigma ->   match pb.(unsolved_part) with   | nil => True     | _ :: _ => exists pb', In pb' (solve pb) /\ is_well_formed_sol pb' sigma   end. Proof. cut (forall f g, f=g -> arity f = arity g). intros Ar pb W; unfold well_formed_pb in W; elim W; clear W; intros W1_pb W; elim W; clear W; intros W2_pb W; elim W; clear W; intros W3_pb W4_pb sigma' S'; unfold is_well_formed_sol, solve; elim S'; clear S'; intros sigma S'; elim S'; clear S'; intros R S'; cut (forall t:term, is_rough_sol pb (((fresh_var pb), t) :: sigma)). unfold is_rough_sol; intro R'; elim S'; clear S'; intros S' W_sigma; elim R; clear R; intros S1 S2; elim S2; clear S2; intros S2 S3; generalize (fresh_var_spec pb); unfold occurs_in_pb; intro Fresh_var; destruct pb.(unsolved_part); trivial. destruct p; rename t into t1; rename t0 into t2; elim (W1_pb t1 t2). intros Wt1 Wt2; generalize (S1 t1 t2 (or_introl _ (refl_equal _))); intro t1_sigma; destruct t1 as [v | f1 l1]. cut (forall v', v'=v -> find eq_variable_dec v' (solved_part pb) =                                  find eq_variable_dec v (solved_part pb)). case (find eq_variable_dec v pb.(solved_part)). intros x_val F; generalize (F v (refl_equal _)); clear F; intro F; elim (eq_term_dec x_val t2). intro; subst x_val; exists (mk_pb (existential_vars pb) l (solved_part pb)                        (partly_solved_part pb)); split. left; trivial. exists sigma; intuition. intro; absurd (x_val = t2); trivial. generalize (S3 v); rewrite F; rewrite t1_sigma; intro; apply sym_eq; trivial. intros F; generalize (F v (refl_equal _)); clear F; intro F; cut (forall v', v'=v -> find eq_variable_dec v' (partly_solved_part pb) = find eq_variable_dec v (partly_solved_part pb)). case (find eq_variable_dec v pb.(partly_solved_part)). intros pst F'; generalize (F' v (refl_equal _)); clear F'; intro F'; destruct t2 as [v2 | f2 l2]. generalize (S2 v); rewrite F'; intro E; rewrite t1_sigma in E; inversion E. generalize (S2 v); rewrite F'; intro t1_sigma'; rewrite t1_sigma in t1_sigma'; generalize (W3_pb v); rewrite F'; intro Act; elim (eq_symbol_dec (head_symb pst) f2). intro H; generalize (Ar _ _ (sym_eq H)); destruct (arity (head_symb pst)). elim Act; clear Act; intros Wct Act Af2; rewrite H in t1_sigma'; rewrite H in Act; generalize (remove_several_subterms_bis_nil sigma f2 v (new_var pst) (closed_term pst) l2 Af2 W_sigma Wt2 (trans_eq t1_sigma t1_sigma') t1_sigma Act); destruct (remove _ eq_term_dec (closed_term pst) l2) as [ l2' | ]. intro t_sigma; exists (mk_pb (existential_vars pb) ((Var (new_var pst), build f2 l2') :: l)        (solved_part pb) (partly_solved_part pb)); split. left; trivial. exists sigma. split. split. intros t1 t2 In_t1t2; elim In_t1t2; clear In_t1t2; intro In_t1t2. inversion In_t1t2; trivial. apply S1; right; trivial. split; trivial. split; trivial. contradiction. contradiction. contradiction. intro; inversion t1_sigma'; absurd (head_symb pst = f2); trivial; apply sym_eq; trivial. intro F'; generalize (F' v (refl_equal _)); clear F'; intro F'; exists (mk_pb (existential_vars pb) l ((v, t2) :: (solved_part pb))        (partly_solved_part pb)); split. left; trivial. exists sigma; intuition. simpl solved_part; simpl find; elim (eq_variable_dec v0 v); intro v0_eq_v. subst v0; trivial. apply (S3 v0). intros; subst v; trivial. intros; subst v; trivial. destruct t2 as [v' | f2 l2]. inversion t1_sigma. destruct (eq_symbol_dec f1 f2) as [f1_eq_f2 | f1_diff_f2]. subst f2; generalize (Ar f1); case (arity f1). intro Af; generalize (Af f1 (refl_equal _)); clear Af; intro Af; generalize (sym_eq Af); clear Af; intro Af; elim (le_gt_dec (length l1) (length l2)). intros Ll2; unfold ac_elementary_solve; destruct l1. absurd (2<=0); auto with arith; apply (well_formed_cf_length Af Wt1). destruct t as [v | f k]. cut (forall v', v=v' -> find eq_variable_dec v' (solved_part pb) =                 find eq_variable_dec v (solved_part pb)). case (find eq_variable_dec v (solved_part pb)). intros pst F; generalize (F v (refl_equal _)); clear F; intro F. unfold ac_elementary_solve_term_var_with_val_term; generalize (S3 v); rewrite F; intro v_sigma; generalize (remove_a_subterm sigma f1 v l1 pst l2 Af W_sigma Wt1 Wt2 v_sigma t1_sigma) (remove_several_subterms sigma f1 v l1 pst l2 Af W_sigma Wt1 Wt2 v_sigma t1_sigma); destruct (remove _ eq_term_dec pst l2). intros t_sigma _; exists (mk_pb (existential_vars pb) ((build f1 l1, build f1 l0) :: l)        (solved_part pb) (partly_solved_part pb)); split. left; trivial. exists sigma; split. split. intros t1 t2 In_t1t2; elim In_t1t2; clear In_t1t2; intro In_t1t2. inversion_clear In_t1t2; apply t_sigma; trivial. apply S1; right; trivial. split; trivial. split; trivial. destruct pst as [v' | f k]. contradiction. intro; destruct (eq_symbol_dec f1 f) as [f1_eq_f | f1_diff_f]. subst f; destruct (remove_list k l2) as [k2' | ]. unfold EDS.A, DOS.A in *; elim (le_gt_dec (length l1) (length k2')). intros _ t_sigma; exists (mk_pb (existential_vars pb) ((build f1 l1, build f1 k2') :: l)        (solved_part pb) (partly_solved_part pb)); split. left; trivial. exists sigma; split. split. intros t1 t2 In_t1t2; elim In_t1t2; clear In_t1t2; intro In_t1t2. inversion_clear In_t1t2; trivial. apply S1; right; trivial. split; trivial. split; trivial. contradiction. contradiction. intro; absurd (f1=f); trivial. intro F; generalize (F v (refl_equal _)); clear F; intro F; cut (forall v', v=v' -> find eq_variable_dec v' (partly_solved_part pb) = find eq_variable_dec v (partly_solved_part pb)). destruct (find eq_variable_dec v (partly_solved_part pb)). intro F'; generalize (F' v (refl_equal _)); clear F'; intro F'; unfold ac_elementary_solve_term_var_with_part_val_term; generalize (S2 v); rewrite F'; intro v_sigma; generalize (W3_pb v); rewrite F'; elim (eq_symbol_dec f1 (head_symb p)). intro f_eq_head_p; rewrite <- f_eq_head_p; rewrite Af; rewrite <- f_eq_head_p in v_sigma; intro Act; elim Act; clear Act; intros Wct Act; generalize (remove_several_subterms_bis sigma f1 v (new_var p) l1 (closed_term p) l2 Af W_sigma Wt1 Wt2 v_sigma t1_sigma Act). destruct (remove _ eq_term_dec (closed_term p) l2). intro t_sigma; exists (mk_pb (existential_vars pb)             ((build f1 (Var (new_var p) :: l1), build f1 l0) :: l)             (solved_part pb) (partly_solved_part pb)); split. left; trivial. exists sigma; split. split. intros t1 t2 In_t1t2; elim In_t1t2; clear In_t1t2; intro In_t1t2. inversion_clear In_t1t2; trivial. apply S1; right; trivial. split; trivial. split; trivial. contradiction. intros f_diff_head_p Act; apply (exists_map_without_repetition eq_term_dec (fun pb' =>   ( exists sigma'0 : substitution,     ((forall t1 t2:term,          In (t1, t2) (unsolved_part pb') -> apply_cf_subst sigma'0 t1 = t2) /\       (forall v0:variable,          match find eq_variable_dec v0 (partly_solved_part pb') with          | Some pst =>              apply_cf_subst sigma'0 (Var v0) =              Term (head_symb pst)                (quicksort                   (flatten (head_symb pst)                      (apply_cf_subst sigma'0 (Var (new_var pst))                       :: closed_term pst :: nil)))          | None => True          end) /\       (forall v0:variable,          match find eq_variable_dec v0 (solved_part pb') with          | Some t => apply_cf_subst sigma'0 (Var v0) = t          | None => True          end)) /\      (forall v0:variable,         In v0 (existential_vars pb') \/         apply_cf_subst sigma' (Var v0) = apply_cf_subst sigma'0 (Var v0)) /\      (well_formed_cf_subst sigma'0)))); exists (apply_cf_subst sigma (Var v)); split. simpl in t1_sigma; rewrite Af in t1_sigma; inversion_clear t1_sigma; replace (match find eq_variable_dec v sigma with           | Some v_sigma => v_sigma           | None => Var v           end) with (apply_cf_subst sigma (Var v)); trivial; rewrite v_sigma; elim (eq_symbol_dec f1 (head_symb p)). intro; absurd (f1 = head_symb p); trivial. intros _; setoid_rewrite <- in_quick_in; left; trivial. rewrite v_sigma; elim (eq_symbol_dec (head_symb p) (head_symb p)). intros _; generalize (Ar (head_symb p)); destruct (arity (head_symb p)). elim Act; clear Act; intros Wct Act Ahsp; generalize (Ahsp (head_symb p) (refl_equal _)); clear Ahsp; intro Ahsp; generalize (sym_eq Ahsp); clear Ahsp; intro Ahsp; cut (well_formed_cf    (Term (head_symb p)       (quicksort          (flatten (head_symb p)             (apply_cf_subst sigma (Var (new_var p)) :: closed_term p :: nil))))). intro W; generalize (remove_several_subterms_bis_nil sigma (head_symb p) v (new_var p) (closed_term p) (quicksort (flatten (head_symb p)             (apply_cf_subst sigma (Var (new_var p)) :: closed_term p :: nil))) Ahsp W_sigma W v_sigma v_sigma Act). destruct (remove _ eq_term_dec (closed_term p)     (quicksort        (flatten (head_symb p)           (apply_cf_subst sigma (Var (new_var p)) :: closed_term p :: nil)))). intro v'_sigma; generalize (remove_a_subterm sigma f1 v l1 (apply_cf_subst sigma (Var v)) l2 Af W_sigma Wt1 Wt2 (refl_equal _) t1_sigma). rewrite <- v_sigma; destruct (remove _ eq_term_dec (apply_cf_subst sigma (Var v)) l2). intro t_sigma; exists sigma; split. split. intros t1 t2 In_t1t2; elim In_t1t2; clear In_t1t2; intro In_t1t2. inversion_clear In_t1t2; trivial. elim In_t1t2; clear In_t1t2; intro In_t1t2. inversion_clear In_t1t2; trivial. apply S1; right; trivial. split; trivial. split; trivial. rewrite v_sigma; intro; apply f_diff_head_p; trivial. trivial. rewrite <- v_sigma; apply well_formed_cf_apply_subst; trivial; simpl; trivial. contradiction. contradiction. intro H; apply H; trivial. intro F'; generalize (F' v (refl_equal _)); clear F'; intro F'; unfold ac_elementary_solve_term_var_without_val_term. apply (exists_map12_without_repetition eq_term_dec (fun pb' =>  ( exists sigma'0 : substitution,     ((forall t1 t2:term,          In (t1, t2) (unsolved_part pb') -> apply_cf_subst sigma'0 t1 = t2) /\       (forall v0:variable,          match find eq_variable_dec v0 (partly_solved_part pb') with          | Some pst =>              apply_cf_subst sigma'0 (Var v0) =              Term (head_symb pst)                (quicksort                   (flatten (head_symb pst)                      (apply_cf_subst sigma'0 (Var (new_var pst))                       :: closed_term pst :: nil)))          | None => True          end) /\       (forall v0:variable,          match find eq_variable_dec v0 (solved_part pb') with          | Some t => apply_cf_subst sigma'0 (Var v0) = t          | None => True          end)) /\      (forall v0:variable,         In v0 (existential_vars pb') \/         apply_cf_subst sigma' (Var v0)= apply_cf_subst sigma'0 (Var v0)) /\      well_formed_cf_subst sigma'0)) (fun t => match remove _ eq_term_dec t l2 with           | Some rmv =>               if le_gt_dec (length l2) (length l1 + 1)               then                  (Some                     (mk_pb (existential_vars pb)                        ((build f1 l1, build f1 rmv) :: l)                        ((v, t) :: (solved_part pb))                        (partly_solved_part pb)), None)               else                  (Some                     (mk_pb (existential_vars pb)                        ((build f1 l1, build f1 rmv) :: l)                        ((v, t) :: (solved_part pb))                        (partly_solved_part pb)),                   Some                     (mk_pb (fresh_var pb :: existential_vars pb)                        ((build f1 (Var (fresh_var pb) :: l1), build f1 rmv)                         :: l) (solved_part pb)                        ((v, (mk_pst f1 (fresh_var pb) t)) ::                           (partly_solved_part pb))))           | None => (None, None)           end) l2). elim (le_gt_dec (length l2) (length l1 + 1)); intro L. exists (apply_cf_subst sigma (Var v)); cut (match apply_cf_subst sigma (Var v) with       | Var _ => True       | Term g _ => f1<>g end). intro Axsigma; generalize (remove_a_subterm sigma f1 v l1 (apply_cf_subst sigma (Var v)) l2 Af W_sigma Wt1 Wt2 (refl_equal _) t1_sigma). generalize (in_remove _ eq_term_dec (apply_cf_subst sigma (Var v)) l2); destruct (remove _ eq_term_dec (apply_cf_subst sigma (Var v)) l2). intros [t [l' [l'' [v_sigma_eq_t [l2_eq H]]]]] H'; split. subst; apply in_or_app; right; left; trivial. exists sigma; split. split. intros t1 t2 In_t1t2; elim In_t1t2; clear In_t1t2; intro In_t1t2. inversion_clear In_t1t2; trivial. apply S1; right; trivial. split; trivial. intro v0; simpl; elim (eq_variable_dec v0 v). intro; subst v0; trivial. intros _; generalize (S3 v0); simpl; trivial. destruct (apply_cf_subst sigma (Var v)). split; trivial. split; trivial. intros; destruct (apply_cf_subst sigma (Var v)). contradiction. absurd (f1=a); trivial. assert (L' : 1 + length l1 = length l2). apply le_antisym; [simpl in Ll2; trivial | rewrite plus_comm; trivial]. pattern (Var v :: l1) in t1_sigma; simpl in t1_sigma; rewrite Af in t1_sigma. assert (Inj : forall l' l'', Term f1 l' = Term f1 l'' -> l' = l''). intros l' l'' H'; injection H'; intros; subst; trivial. rewrite <- (Inj _ _ t1_sigma) in L'; clear Inj. rewrite length_quicksort in L'; simpl. assert (Wv_sigma : well_formed_cf (apply_cf_subst sigma (Var v))). apply well_formed_cf_apply_subst; simpl; trivial. simpl in Wv_sigma; destruct (find eq_variable_dec v sigma) as [ [ | g ll ] | ]; trivial. destruct (eq_symbol_dec f1 g) as [f1_eq_g | ]; trivial. subst g; assert (L'' := well_formed_cf_length Af Wv_sigma). rewrite length_app in L'. assert (L''' := plus_le_compat_r _ _ (length (flatten f1 (map (apply_cf_subst sigma) l1))) L''). rewrite <- L' in L'''. assert (Wl1 : forall t, In t (map (apply_cf_subst sigma) l1) -> well_formed_cf t). intros t' t'_in_map_l1; setoid_rewrite in_map_iff in t'_in_map_l1; destruct t'_in_map_l1 as [t [Wt t_sigma]]. subst; apply well_formed_cf_apply_subst; trivial. apply (well_formed_cf_subterms Wt1); right; trivial. assert (L4 := length_flatten_bis Af _ Wl1); rewrite length_map in L4. generalize (le_trans _ _ _ (plus_le_compat_l _ _ 2 L4) L'''). intro; absurd (2 + length l1 <= 1 + length l1); auto with arith. cut (forall v', v'=v -> apply_cf_subst sigma (Var v') = apply_cf_subst sigma (Var v)). destruct (apply_cf_subst sigma (Var v)). intro v_sigma; generalize (v_sigma v (refl_equal _)); clear v_sigma; intro v_sigma; exists (Var a); generalize (in_remove _ eq_term_dec (Var a) l2) (remove_a_subterm sigma f1 v l1 (Var a) l2 Af W_sigma Wt1 Wt2 v_sigma t1_sigma); destruct (remove _ eq_term_dec (Var a) l2). intros [t [l' [l'' [v_sigma_eq_t [l2_eq H]]]]] H'; split. subst; apply in_or_app; right; left; trivial. left; exists sigma; repeat split; trivial. intros t1 t2 In_t1t2; elim In_t1t2; clear In_t1t2; intro In_t1t2. inversion_clear In_t1t2; trivial. apply S1; right; trivial. simpl; intros v1; elim (eq_variable_dec v1 v). intro; subst v1; simpl in v_sigma; trivial. intros _; generalize (S3 v1); simpl; trivial. contradiction. intro v_sigma; generalize (v_sigma v (refl_equal _)); clear v_sigma; intro v_sigma; elim (eq_symbol_dec f1 a). intro; subst a; cut (well_formed_cf (Term f1 l0)). intro W; destruct l0. absurd (2<=0); auto with arith; apply (well_formed_cf_length Af W). generalize ((well_formed_cf_alien Af W) t (or_introl _ (refl_equal _))); intro At; cut (well_formed_cf_subst (((fresh_var pb), (build f1 l0)) :: sigma)). intro W_sigma0; cut (apply_cf_subst (((fresh_var pb), (build f1 l0)) :: sigma) (Var v) =  Term f1    (quicksort       (flatten f1          (apply_cf_subst (((fresh_var pb), (build f1 l0)) :: sigma)             (Var (fresh_var pb)) :: t :: nil)))). intro v_sigma0; cut (apply_cf_subst (((fresh_var pb), (build f1 l0)) :: sigma)    (Term f1 (Var v :: l1)) = Term f1 l2). intro t1_sigma0; generalize (in_remove _ eq_term_dec t l2) (remove_several_subterms_bis (((fresh_var pb), (build f1 l0)) :: sigma) f1 v (fresh_var pb) l1 t l2 Af W_sigma0 Wt1 Wt2 v_sigma0 t1_sigma0 At). intros H1 H'; exists t. destruct (remove _ eq_term_dec t l2). destruct H1 as [t' [l' [l'' [v_sigma_eq_t' [l2_eq H]]]]]; subst t'; split. subst; apply in_or_app; right; left; trivial. right; exists (((fresh_var pb), (build f1 l0)) :: sigma); elim (R' (build f1 l0)); clear R'; intros R1 R2; elim R2; clear R2; intros R2 R3; split. split. intros t1 t2 In_t1t2; elim In_t1t2; clear In_t1t2; intro In_t1t2. inversion_clear In_t1t2; trivial. apply R1; right; trivial. split; trivial. simpl; intro v0; elim (eq_variable_dec v0 v). intro; subst v0; apply v_sigma0. generalize (R2 v0); simpl; trivial. split; trivial. simpl; intro v0; elim (eq_variable_dec v0 (fresh_var pb)). intro; subst v0; left; left; trivial. intros _; elim (S' v0); intro; [ left; right | right ]; trivial. contradiction. elim (R' (build f1 l0)); intros R1 _; apply R1; left; trivial. apply trans_eq with (apply_cf_subst sigma (Var v)). simpl; cut (v <> (fresh_var pb)). intro v_diff_fresh; elim (eq_variable_dec v (fresh_var pb)). intro; absurd (v=fresh_var pb); trivial. intro; trivial. unfold not; intro; apply Fresh_var; left; unfold occurs_in_term_list; simpl; left; left; apply sym_eq; trivial. rewrite v_sigma. apply (f_equal (fun l => Term f1 l)); apply sort_is_unique. apply (well_formed_cf_sorted Af W). apply quick_sorted. apply permut_sym; apply quick_permut_bis. replace (apply_cf_subst (((fresh_var pb), (build f1 l0)) :: sigma)         (Var (fresh_var pb))) with (build f1 l0). replace (flatten f1 (build f1 l0 :: t :: nil)) with (flatten f1 (build f1 l0 :: nil) ++ flatten f1 (t :: nil)); [idtac | rewrite <- flatten_app; simpl app; trivial]. refine (permut_trans (list_permut_app_app _ _) _). apply permut_trans with (t :: flatten f1 (build f1 l0 :: nil)). simpl; destruct t as [ | g ll]; [apply permut_refl | idtac]. destruct (eq_symbol_dec f1 g) as [f1_eq_g | _]; [absurd (f1=g); trivial | apply permut_refl]. setoid_rewrite <- permut_cons. reflexivity. apply flatten_build_cons with t; trivial. simpl; elim (eq_variable_dec (fresh_var pb) (fresh_var pb)). intros _; trivial. intro; absurd (fresh_var pb = fresh_var pb); trivial. unfold well_formed_cf_subst; simpl; intro v0; elim (eq_variable_dec v0 (fresh_var pb)); intro v0_eq_fresh_var_pb. apply (well_formed_cf_build_cons Af W). apply W_sigma. unfold well_formed_cf_subst in W_sigma; generalize (W_sigma v); simpl in v_sigma; destruct (find eq_variable_dec v sigma). subst t; trivial. absurd (Var v = Term f1 l0); trivial; discriminate. intro f_diff_s; exists (Term a l0); generalize (in_remove _ eq_term_dec (Term a l0) l2) (remove_a_subterm sigma f1 v l1 (Term a l0) l2 Af W_sigma Wt1 Wt2 v_sigma t1_sigma). intros H1 H'; destruct (remove _ eq_term_dec (Term a l0) l2). destruct H1 as [t' [l' [l'' [v_sigma_eq_t' [l2_eq H]]]]]; subst t'; split. subst; apply in_or_app; right; left; trivial. left; exists sigma; repeat split; trivial. intros t1 t2 In_t1t2; elim In_t1t2; clear In_t1t2; intro In_t1t2. inversion_clear In_t1t2; trivial. apply S1; right; trivial. simpl; intros v1; elim (eq_variable_dec v1 v). intro; subst v1; simpl in v_sigma; trivial. intros _; generalize (S3 v1); simpl; trivial. absurd (f1=a); trivial. intros; subst v; trivial. intros; subst v; trivial. intros; subst v; trivial. unfold ac_elementary_solve_term_term_term. apply (exists_map_without_repetition eq_term_dec (fun pb' => (exists sigma'0 : substitution,     ((forall t1 t2:term,          In (t1, t2) (unsolved_part pb') -> apply_cf_subst sigma'0 t1 = t2) /\       (forall v:variable,          match find eq_variable_dec v (partly_solved_part pb') with          | Some pst =>              apply_cf_subst sigma'0 (Var v) =              Term (head_symb pst)                (quicksort                   (flatten (head_symb pst)                      (apply_cf_subst sigma'0 (Var (new_var pst))                       :: closed_term pst :: nil)))          | None => True          end) /\       (forall v:variable,          match find eq_variable_dec v (solved_part pb') with          | Some t => apply_cf_subst sigma'0 (Var v) = t          | None => True          end)) /\      (forall v:variable,         In v (existential_vars pb') \/         apply_cf_subst sigma' (Var v) = apply_cf_subst sigma'0 (Var v)) /\      (well_formed_cf_subst sigma'0)))). exists (apply_cf_subst sigma (Term f k)). assert (f_diff_s := well_formed_cf_alien Af Wt1 _ (or_introl _ (refl_equal _))). simpl in f_diff_s. assert (s_l0_in_l2 : In (apply_cf_subst sigma (Term f k)) l2). generalize (S1 _ _ (or_introl _ (refl_equal _))); simpl; rewrite Af; destruct (eq_symbol_dec f1 f) as [f1_eq_f | _]; [absurd (f1=f); trivial | idtac]. intro H; injection H; intros; subst l2. setoid_rewrite <- in_quick_in; left; trivial. split; [trivial | idtac]. generalize (in_remove _ eq_term_dec (apply_cf_subst sigma (Term f k)) l2); destruct (remove _ eq_term_dec (apply_cf_subst sigma (Term f k)) l2) as    [l2''' | ]; [idtac | intro; absurd (In (apply_cf_subst sigma (Term f k)) l2); trivial]. intros [a' [l2' [l2'' [H [l2_eq l2'''_eq]]]]]; subst a'; injection l2'''_eq; clear l2'''_eq; intro; subst l2 l2'''; simpl; destruct (eq_symbol_dec f f) as [ _ | f_diff_f]; [idtac | absurd (f = f); trivial]. exists sigma; repeat split; trivial. simpl unsolved_part; intros t1 t2 [In_t1t2 | [In_t1t2 | In_t1t2]]. injection In_t1t2; intros; subst. apply flatten_cf with f1; trivial. apply well_formed_cf_apply_subst; trivial; apply (well_formed_cf_subterms Wt1); left; trivial. apply (well_formed_cf_apply_subst W_sigma (Term f k)). apply (well_formed_cf_subterms Wt1); left; trivial. apply permut_refl. injection In_t1t2; intros; subst. apply flatten_cf with f1; trivial. apply well_formed_cf_apply_subst; trivial; apply well_formed_cf_build_cons with (Term f k); trivial. apply well_formed_cf_build_inside with (apply_cf_subst sigma (Term f k)); trivial. setoid_rewrite <- (flatten_apply_cf_subst sigma l1 Af); setoid_rewrite (flatten_build (l2' ++ l2'') Af). intros t t_in_l2'_l2''; destruct (in_app_or _ _ _ t_in_l2'_l2'') as [t_in_l2' | t_in_l2'']; apply (well_formed_cf_alien Af Wt2); apply in_or_app; [left | right; right]; trivial. setoid_rewrite (@permut_cons (apply_cf_subst sigma (Term f k))                                               (apply_cf_subst sigma (Term f k))). reflexivity. transitivity (l2' ++ apply_cf_subst sigma (Term f k) :: l2''). simpl in t1_sigma; rewrite Af in t1_sigma; simpl; inversion_clear t1_sigma; apply permut_sym; apply quick_permut_bis; elim (eq_symbol_dec f1 f). intro; absurd (f1=f); trivial. intros _; auto. apply permut_sym; setoid_rewrite <- permut_cons_inside; auto. reflexivity. apply S1; right; trivial. apply H; trivial. intro L; absurd (length l1 > length l2); trivial; unfold gt; apply le_not_lt; simpl in t1_sigma; rewrite Af in t1_sigma; inversion_clear t1_sigma; rewrite length_quicksort; apply length_flatten_ter; trivial. intros; apply (well_formed_cf_subterms Wt1); trivial. intro Af; generalize (Af f1 (refl_equal _)); clear Af; intro Af; generalize (sym_eq Af); clear Af; intro Af. elim Wt1; intros _ H; rewrite Af in H; elim H; clear H; intros Ll1 _; elim Wt2; intros _ H; rewrite Af in H; elim H; clear H; intros Ll2 _; destruct l1. simpl in Ll1; absurd (0=2); trivial. destruct l1. simpl in Ll1; absurd (1=2); trivial. destruct l1. destruct l2. simpl in Ll2; absurd (0=2); trivial. destruct l2. simpl in Ll2; absurd (1=2); trivial. destruct l2. simpl in t1_sigma; rewrite Af in t1_sigma; inversion t1_sigma; generalize (quick_permut (apply_cf_subst sigma t :: apply_cf_subst sigma t0 :: nil));  rewrite H0; intro P; elim (list_permut.permut_length_2 P); clear P; intro P; elim P; clear P; intros t_sigma t0_sigma. exists (mk_pb (existential_vars pb) ((t, t1) :: (t0, t2) :: l) (solved_part pb)        (partly_solved_part pb)); split. left; trivial. exists sigma; repeat split; trivial. intros t3 t4 In_t1t2; elim In_t1t2; clear In_t1t2; intro In_t1t2. injection In_t1t2; intros; subst t3 t4; trivial. elim In_t1t2; clear In_t1t2; intro In_t1t2. injection In_t1t2; intros; subst t3 t4; trivial. apply S1; right; trivial. exists (mk_pb (existential_vars pb) ((t, t2) :: (t0, t1) :: l)           (solved_part pb) (partly_solved_part pb)); split. right; left; trivial. exists sigma; repeat split; trivial. intros t3 t4 In_t1t2; elim In_t1t2; clear In_t1t2; intro In_t1t2. injection In_t1t2; intros; subst t3 t4; trivial. elim In_t1t2; clear In_t1t2; intro In_t1t2. injection In_t1t2; intros; subst t3 t4; trivial. apply S1; right; trivial. simpl in Ll2; discriminate. simpl in Ll1; discriminate. intros n Af; generalize (Af f1 (refl_equal _)); clear Af; intro Af; generalize (sym_eq Af); clear Af; intro Af; simpl in t1_sigma; rewrite Af in t1_sigma; inversion t1_sigma. generalize (length_map (apply_cf_subst sigma) l1); rewrite H0; intro L; cut (forall t1 t2, In (t1,t2) l -> apply_cf_subst sigma t1 = t2). subst l2; clear L Fresh_var R' W1_pb S1 Wt1 Wt2 t1_sigma; intros S1. cut (match         fold_left2           (fun (current_list_of_eqs : list _) t1 t2 => (t1,t2) :: current_list_of_eqs)           l l1 (map (apply_cf_subst sigma) l1) with        | None => False        | Some new_list_of_equations =>          (forall t1 t2, In (t1,t2) new_list_of_equations ->           apply_cf_subst sigma t1 = t2)         end). destruct (fold_left2 (fun (current_list_of_eqs : list _) t1 t2 =>                                (t1,t2) :: current_list_of_eqs)                                l l1 (map (apply_cf_subst sigma) l1)). clear S1; intro S1; exists (mk_pb (existential_vars pb) l0 (solved_part pb)              (partly_solved_part pb)); split. left; trivial. exists sigma; intuition. contradiction. generalize S1; clear S1; generalize l; induction l1; simpl; trivial. intros l0 S1. apply (IHl1 ((a, apply_cf_subst sigma a) :: l0)); intros t1 t2 I; elim I; clear I; intro I. inversion I; trivial. apply S1; trivial. intros; apply S1; right; trivial. absurd (f1=f2); trivial. simpl in t1_sigma; injection t1_sigma; trivial. left; trivial. intro t; apply add_new_var_to_rough_sol; trivial. do 3 (split; trivial). intro f; intros; subst f; trivial. Qed. End Make. ```