Library ac_matching.matching_well_formed
Add LoadPath "basis".
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.
Require Import matching_well_founded.
Module Type S.
Declare Module Import WFMatching : matching_well_founded.S.
Import Matching.
Import Cf_eq_ac.
Import Ac.
Import EqTh.
Import T.
Axiom well_formed_solve :
forall pb, well_formed_pb pb -> forall pb', In pb' (solve pb) -> well_formed_pb pb'.
End S.
Module Make (WFMatching1 : matching_well_founded.S) :
S with Module WFMatching := WFMatching1.
Module Import WFMatching := WFMatching1.
Import Matching.
Import Cf_eq_ac.
Import Ac.
Import EqTh.
Import T.
Import F.
Import X.
Import Sort.
Import LPermut.
Theorem well_formed_solve :
forall pb, well_formed_pb pb -> forall pb', In pb' (solve pb) -> well_formed_pb pb'.
Proof.
unfold solve, well_formed_pb; intros pb [W1 [W2 [W3 [W4 [W5 W6]]]]] pb' In_pb';
assert (Fresh_var_spec :~ (occurs_in_term_list (fresh_var pb)
(map (fun p : term * term => let (t1, _) := p in t1) (unsolved_part pb)))).
unfold not; intro; apply (fresh_var_spec pb); left; trivial.
unfold occurs_in_pb in W6; destruct (unsolved_part pb) as [ | [[v1 | f1 l1] t2] l].
contradiction.
assert (F : forall v, v=v1 -> find eq_variable_dec v (solved_part pb) =
find eq_variable_dec v1 (solved_part pb)). intros; subst; trivial.
destruct (find eq_variable_dec v1 (solved_part pb)) as [t1 | ];
generalize (F v1 (refl_equal _)); clear F; intro F.
destruct (eq_term_dec t1 t2) as [t1_eq_t2 | _]; [idtac | contradiction];
inversion_clear In_pb' as [pb'_eq_ | ]; [idtac | contradiction]; subst.
split; [intros; apply W1; right; trivial | idtac].
split; [intros; apply W2; right; trivial | idtac].
split; [intros; apply W3; right; trivial | idtac].
split; [intros; apply W4; right; trivial | idtac].
split; [intros; apply W5; right; trivial | idtac].
intros v p H; generalize (W6 v p H); intros [[H1 | H1'] | [H2 | H3]].
right; right; rewrite H1; simpl; rewrite F; trivial.
left; trivial.
right; left; trivial.
right; right; trivial.
generalize (W3 v1);
assert (F' : forall v, v=v1 -> find eq_variable_dec v (partly_solved_part pb) =
find eq_variable_dec v1 (partly_solved_part pb)). intros; subst; trivial.
destruct (find eq_variable_dec v1 (partly_solved_part pb)) as [p1 | ];
generalize (F' v1 (refl_equal _)); clear F'; intro F'.
destruct t2 as [ v2 | f2 l2]; [contradiction | idtac];
destruct (eq_symbol_dec (head_symb p1) f2) as [f1_eq_f2 | ]; [rewrite f1_eq_f2 | contradiction];
destruct_arity f2 n2 Af2; [ idtac | contradiction | contradiction].
intros [W_p1 H_p1]; generalize (in_remove _ eq_term_dec (closed_term p1) l2);
destruct (remove _ eq_term_dec (closed_term p1) l2) as [ l2''' |]; [idtac | contradiction].
intros [cp1 [l2' [l2'' [ H [l2_eq l2'''_eq]]]]].
injection l2'''_eq; clear l2'''_eq; intro; subst l2''';
inversion_clear In_pb' as [pb'_eq_ | ]; [idtac | contradiction]; subst; split.
intros t1 t2 [H | In_l].
inversion H; split; simpl; trivial.
apply well_formed_cf_build_inside with (closed_term p1); trivial;
refine (proj2 (A:= well_formed_cf (Var v1)) _); apply W1; left; trivial.
apply W1; right; trivial.
split; [intros; apply W2; right; trivial | idtac].
split; [intros; apply W3; right; trivial | idtac].
split; [intros; apply W4; right; trivial | idtac].
split; [intros; apply W5; right; trivial | idtac].
intros v p H; generalize (W6 v p H); intros [[H1 | H1'] | [H2 | H3]].
right; left; rewrite H1; simpl; rewrite F'; trivial.
left; right; trivial.
right; left; trivial.
right; right; trivial.
inversion_clear In_pb' as [pb'_eq_ | ]; [idtac | contradiction].
intros _; subst.
split; [intros; apply W1; right; trivial | idtac]; split.
intros v; simpl; destruct (eq_variable_dec v v1) as [_ | _]; [idtac | apply W2];
refine (proj2 (A:= well_formed_cf (Var v1)) _); apply W1; left; trivial.
split; [intros; apply W3; right; trivial | idtac]; split.
intros v; simpl; destruct (eq_variable_dec v v1) as [v_eq_v1 | _]; [idtac | apply W4].
subst v; rewrite (none_nb_occ_O _ _ _ F); rewrite (none_nb_occ_O _ _ _ F');
auto with arith.
split; [intros; apply W5; right; trivial | idtac].
intros v p H; generalize (W6 v p H); intros [[H1 | H1'] | [H2 | H3]].
right; right; rewrite H1; simpl; destruct (eq_variable_dec v1 v1) as [ _ | v1_diff_v1]; trivial;
absurd (v1 = v1); trivial.
left; trivial.
right; left; trivial.
right; right; simpl; destruct (eq_variable_dec (new_var p) v1) as [ _ | _]; trivial.
destruct t2 as [ v2 | f2 l2 ]; [contradiction | idtac];
destruct (eq_symbol_dec f1 f2) as [f1_eq_f2 | _]; [idtac | contradiction].
subst f2; destruct_arity f1 n1 Af1.
destruct (le_gt_dec (length l1) (length l2)) as [_ | _]; [idtac | contradiction].
unfold ac_elementary_solve in *.
assert (W_t1 : well_formed_cf (Term f1 l1)).
refine (proj1 _ (B:= (well_formed_cf (Term f1 l2)))); apply W1; left; trivial.
assert (W_t2 : well_formed_cf (Term f1 l2)).
apply (proj2 (A:= (well_formed_cf (Term f1 l1)))); apply W1; left; trivial.
destruct l1 as [ | t1 l1].
absurd (2 <= @length term nil); auto with arith;
apply well_formed_cf_length with f1; trivial.
destruct t1 as [v1 | g1 ll1].
generalize (W2 v1);
assert (F : forall v, v=v1 -> find eq_variable_dec v (solved_part pb) =
find eq_variable_dec v1 (solved_part pb)). intros; subst; trivial.
destruct (find eq_variable_dec v1 (solved_part pb)) as [s1 | ];
generalize (F v1 (refl_equal _)); clear F; intro F.
intro W_s1; unfold ac_elementary_solve_term_var_with_val_term in *.
generalize (in_remove _ eq_term_dec s1 l2);
destruct (remove _ eq_term_dec s1 l2) as [ l2''' |].
intros [cp1 [l2' [l2'' [ H [l2_eq l2'''_eq]]]]].
injection l2'''_eq; clear l2'''_eq; intro; subst l2''';
inversion_clear In_pb' as [pb'_eq_ | ]; [idtac | contradiction]; subst; split.
intros t1 t2 [H | In_l].
inversion H; split.
replace l1 with (nil ++ l1); trivial; apply well_formed_cf_build_inside with (Var v1); trivial.
apply well_formed_cf_build_inside with cp1; trivial.
apply W1; right; trivial.
split; [intros; apply W2; right; trivial | idtac].
split; [intros; apply W3; right; trivial | idtac].
split; [intros; apply W4; right; trivial | idtac].
split; [intros; apply W5; right; trivial | idtac].
intros v p H; generalize (W6 v p H); intros [[[H1 | H1'] | H1''] | [H2 | H3]].
right; right; rewrite H1; simpl; rewrite F; trivial.
left; left; destruct l1 as [ | u1 [ | u2 l1]]; [contradiction | intuition | idtac];
simpl; apply list_permut_occurs_in_term_list with (u1 :: u2 :: l1); trivial;
apply quick_permut.
left; right; trivial.
right; left; trivial.
right; right; trivial.
intros _; destruct s1 as [| g1 ll1]; [contradiction | idtac ];
destruct (eq_symbol_dec f1 g1) as [f1_eq_g1 | _]; [idtac | contradiction].
assert (S_ll1 : is_sorted ll1).
apply well_formed_cf_sorted with g1; subst; trivial.
assert (S_l2 : is_sorted l2).
apply well_formed_cf_sorted with f1; trivial.
generalize (in_remove_list S_ll1 S_l2); unfold EDS.A, DOS.A in *;
destruct (remove_list ll1 l2) as [l2' | ]; [idtac | contradiction ].
unfold EDS.A, DOS.A in *; destruct (le_gt_dec (length l1) (length l2')) as [L_l1_l2' |]; [idtac | contradiction].
inversion_clear In_pb' as [pb'_eq_ | ]; [idtac | contradiction]; intro P; subst; split.
intros t1 t2 [H | In_l].
inversion H; split.
replace l1 with (nil ++ l1); trivial; apply well_formed_cf_build_inside with (Var v1); trivial.
assert (In_l2'_In_l2 : forall t, In t l2' -> In t l2).
intros t In_l2'; setoid_rewrite <- (list_permut.in_permut_in P); apply in_or_app; right; trivial.
apply well_formed_cf_build; trivial.
apply le_trans with (length l1); trivial; apply le_S_n;
replace (S (length l1)) with (length (Var v1 :: l1)); trivial;
apply well_formed_cf_length with g1; trivial.
intros t In_l2'; apply well_formed_cf_subterms with g1 l2; trivial; apply In_l2'_In_l2; trivial.
intros t In_l2'; apply well_formed_cf_alien with l2; trivial; apply In_l2'_In_l2; trivial.
apply W1; right; trivial.
split; [intros; apply W2; right; trivial | idtac].
split; [intros; apply W3; right; trivial | idtac].
split; [intros; apply W4; right; trivial | idtac].
split; [intros; apply W5; right; trivial | idtac].
intros v p H; generalize (W6 v p H); intros [[[H1 | H1'] | H1''] | [H2 | H3]].
right; right; rewrite H1; simpl; rewrite F; trivial.
left; left; destruct l1 as [ | u1 [ | u2 l1]]; [contradiction | intuition | idtac];
simpl; apply list_permut_occurs_in_term_list with (u1 :: u2 :: l1); trivial;
apply quick_permut.
left; right; trivial.
right; left; trivial.
right; right; trivial.
intros _; generalize (W3 v1);
assert (F' : forall v, v=v1 -> find eq_variable_dec v (partly_solved_part pb) =
find eq_variable_dec v1 (partly_solved_part pb)). intros; subst; trivial.
destruct (find eq_variable_dec v1 (partly_solved_part pb)) as [p1 | ];
generalize (F' v1 (refl_equal _)); clear F'; intro F'.
unfold ac_elementary_solve_term_var_with_part_val_term in *.
destruct (eq_symbol_dec f1 (head_symb p1)) as [f1_eq_hd_p1 | f1_diff_hd_p1].
generalize (in_remove _ eq_term_dec (closed_term p1) l2);
destruct (remove _ eq_term_dec (closed_term p1) l2) as [l2''' | ]; [idtac | contradiction].
inversion_clear In_pb' as [pb'_eq_ | ]; [idtac | contradiction].
intros [cp1 [l2' [l2'' [ H [l2_eq l2'''_eq]]]]].
injection l2'''_eq; clear l2'''_eq; intro; subst;
split.
intros t1 t2 [H'' | In_l].
replace t1 with (fst (t1,t2)); trivial; rewrite <- H'';
replace t2 with (snd (t1,t2)); trivial; rewrite <- H''; unfold fst, snd; split.
apply well_formed_cf_build; trivial.
simpl; auto with arith.
intros t [t_eq | In_t_l1]; [subst; simpl; trivial | idtac];
apply well_formed_cf_subterms with (head_symb p1) (Var v1 :: l1); trivial; right; trivial.
intros t [t_eq | In_t_l1]; [subst; simpl; trivial | idtac].
apply well_formed_cf_alien with (Var v1 :: l1); trivial; right; trivial.
apply well_formed_cf_build_inside with (closed_term p1); trivial.
apply W1; right; trivial.
split; [intros; apply W2; right; trivial | idtac].
split; [intros; apply W3; right; trivial | idtac].
split; [intros; apply W4; right; trivial | idtac].
split; [intros; apply W5; right; trivial | idtac].
intros v p H''; generalize (W6 v p H''); intros [[[H1 | H1'] | H1''] | [H2 | H3]].
right; left; rewrite H1; simpl; rewrite F'; trivial.
left; left; destruct l1 as [ | u1 l1]; [contradiction | idtac].
simpl; apply list_permut_occurs_in_term_list with (Var (new_var p1) :: u1 :: l1);
[ apply quick_permut | idtac]; right; trivial.
left; right; trivial.
right; left; trivial.
right; right; trivial.
intros W3_v1;
pattern pb';
refine
(prop_map_without_repetition (B:=matching_problem) eq_term_dec _ _ _ _ pb' In_pb');
clear pb' In_pb'; intros [ | g2 ll2] In_t2; trivial;
destruct (eq_symbol_dec g2 (head_symb p1)) as [g2_eq_hd_p1 | g2_diff_hd_p1]; trivial.
generalize (in_remove _ eq_term_dec (closed_term p1) ll2);
destruct (remove _ eq_term_dec (closed_term p1) ll2) as [ll2''' | ]; trivial.
intros [cp1 [ll2' [ll2'' [ H [ll2_eq ll2'''_eq]]]]].
injection ll2'''_eq; clear ll2'''_eq; intro; subst ll2''';
generalize (in_remove _ eq_term_dec (Term g2 ll2) l2);
destruct (remove _ eq_term_dec (Term g2 ll2) l2) as [l2''' | ]; trivial.
intros [cp1' [l2' [l2'' [ H' [l2_eq l2'''_eq]]]]].
injection l2'''_eq; clear l2'''_eq; intro; subst;
split.
intros t1 t2 [H'' | [H'' | In_l]].
inversion H''; split; simpl; trivial; subst.
apply well_formed_cf_build_inside with (closed_term p1).
destruct (arity (head_symb p1)) as [ | | n]; [trivial | contradiction | contradiction].
apply (well_formed_cf_subterms W_t2); apply in_or_app; right; left; trivial.
inversion H''; split; subst.
replace l1 with (nil ++ l1); trivial;
replace (Var v1 :: l1) with (nil ++ Var v1 :: l1) in W_t1; trivial;
apply well_formed_cf_build_inside with (Var v1); trivial.
apply well_formed_cf_build_inside with
(Term (head_symb p1) (ll2' ++ closed_term p1 :: ll2'')); trivial.
apply W1; right; trivial.
split; [intros; apply W2; right; trivial | idtac].
split; [intros; apply W3; right; trivial | idtac].
split; [intros; apply W4; right; trivial | idtac].
split; [intros; apply W5; right; trivial | idtac].
intros v p H''; generalize (W6 v p H''); intros [[[H1 | H1'] | H1''] | [H2 | H3]].
right; left; rewrite H1; simpl; rewrite F'; trivial.
left; right; left; destruct l1 as [ | u1 [ | u2 l1]]; [contradiction | intuition | idtac].
simpl; apply list_permut_occurs_in_term_list with (u1 :: u2 :: l1);
[ apply quick_permut | idtac]; trivial.
left; right; right; trivial.
right; left; trivial.
right; right; trivial.
intros _; unfold ac_elementary_solve_term_var_without_val_term in *.
pattern pb';
refine
(prop_map12_without_repetition (B:=matching_problem) eq_term_dec _ _ _ _ pb' In_pb');
clear pb' In_pb';
intros t2 In_t2; generalize (in_remove _ eq_term_dec t2 l2);
destruct (remove _ eq_term_dec t2 l2) as [l2''' | ]; trivial.
intros [cp1' [l2' [l2'' [ H' [l2_eq l2'''_eq]]]]].
injection l2'''_eq; clear l2'''_eq; intro; subst l2''';
unfold DOS.A, EDS.A in *; destruct (le_gt_dec (length l2) (length l1 + 1)) as [_ | _]; trivial.
split.
intros t1 t3 [H'' | In_l].
inversion H''; split; simpl; trivial; subst.
replace l1 with (nil ++ l1); trivial;
replace (Var v1 :: l1) with (nil ++ Var v1 :: l1) in W_t1; trivial;
apply well_formed_cf_build_inside with (Var v1); trivial.
apply well_formed_cf_build_inside with cp1'; trivial.
apply W1; right; trivial.
split.
intro v; simpl; destruct (eq_variable_dec v v1) as [_ | _];
[ apply well_formed_cf_subterms with f1 l2; trivial | apply W2 ].
split; [intros; apply W3; right; trivial | idtac].
split.
intro v; simpl; destruct (eq_variable_dec v v1) as [v_eq_v1 | _].
subst; rewrite (none_nb_occ_O _ _ _ F); rewrite (none_nb_occ_O _ _ _ F');
auto with arith.
apply W4.
split; [intros; apply W5; right; trivial | idtac].
intros v p H''; generalize (W6 v p H''); intros [[[H1 | H1'] | H1''] | [H2 | H3]].
right; right; rewrite H1; simpl;
destruct (eq_variable_dec v1 v1) as [_ | v1_diff_v1]; [idtac | absurd (v1 = v1)]; trivial.
left; left; destruct l1 as [ | u1 [ | u2 l1]]; [contradiction | intuition | idtac];
simpl; apply list_permut_occurs_in_term_list with (u1 :: u2 :: l1); trivial;
apply quick_permut.
left; right; trivial.
right; left; trivial.
right; right; simpl; destruct (eq_variable_dec (new_var p) v1) as [_ | _]; trivial.
split.
split.
intros t1 t3 [H'' | In_l].
inversion H''; split; simpl; trivial; subst.
replace l1 with (nil ++ l1); trivial;
replace (Var v1 :: l1) with (nil ++ Var v1 :: l1) in W_t1; trivial;
apply well_formed_cf_build_inside with (Var v1); trivial.
apply well_formed_cf_build_inside with cp1'; trivial.
apply W1; right; trivial.
split.
intro v; simpl; destruct (eq_variable_dec v v1) as [_ | _];
[ apply well_formed_cf_subterms with f1 l2; trivial | apply W2 ].
split; [intros; apply W3; right; trivial | idtac].
split.
intro v; simpl; destruct (eq_variable_dec v v1) as [v_eq_v1 | _].
subst; rewrite (none_nb_occ_O _ _ _ F); rewrite (none_nb_occ_O _ _ _ F');
auto with arith.
apply W4.
split; [intros; apply W5; right; trivial | idtac].
intros v p H''; generalize (W6 v p H''); intros [[[H1 | H1'] | H1''] | [H2 | H3]].
right; right; rewrite H1; simpl;
destruct (eq_variable_dec v1 v1) as [_ | v1_diff_v1]; [idtac | absurd (v1 = v1)]; trivial.
left; left; destruct l1 as [ | u1 [ | u2 l1]]; [contradiction | intuition | idtac];
simpl; apply list_permut_occurs_in_term_list with (u1 :: u2 :: l1); trivial;
apply quick_permut.
left; right; trivial.
right; left; trivial.
right; right; simpl; destruct (eq_variable_dec (new_var p) v1) as [_ | _]; trivial.
split.
intros t1 t3 [H'' | In_l].
replace t1 with (fst (t1,t3)); trivial; rewrite <- H''; unfold fst;
replace t3 with (snd (t1,t3)); trivial; rewrite <- H''; unfold snd; split.
apply well_formed_cf_build; trivial.
simpl; auto with arith.
intros t [t_eq | In_t_l1]; [subst t; simpl; trivial | idtac];
apply well_formed_cf_subterms with f1 (Var v1 :: l1); trivial; right; trivial.
intros t [t_eq | In_t_l1]; [subst t; simpl; trivial | idtac];
apply well_formed_cf_alien with (Var v1 :: l1); trivial; right; trivial.
subst; apply well_formed_cf_build_inside with cp1'; trivial.
apply W1; right; trivial.
split; [intros; apply W2; right; trivial | idtac].
split.
intro v; simpl; destruct (eq_variable_dec v v1) as [_ | _].
simpl; rewrite Af1; split.
apply well_formed_cf_subterms with f1 l2; trivial.
apply well_formed_cf_alien with l2; trivial.
apply W3.
split.
intro v; simpl; destruct (eq_variable_dec v v1) as [v_eq_v1 | _].
subst; rewrite (none_nb_occ_O _ _ _ F); rewrite (none_nb_occ_O _ _ _ F');
auto with arith.
apply W4.
split.
unfold well_sorted_partly_solved_part;
split; [idtac | split; [idtac | apply W5]].
simpl; intro; apply Fresh_var_spec; left; left; subst v1; simpl; trivial.
unfold new_var; intros v' one_v' v'_eq_fresh_var_pb; apply (fresh_var_spec pb);
right; left; rewrite <- v'_eq_fresh_var_pb.
generalize (none_nb_occ_O eq_variable_dec v' (partly_solved_part pb));
destruct (find eq_variable_dec v' (partly_solved_part pb)); trivial;
intro H; generalize (H (refl_equal _)); clear H; intro H; rewrite H in one_v';
absurd (1 <= 0); trivial; auto with arith.
simpl; intros v p H; destruct (eq_variable_dec v v1) as [_ | v_diff_v1].
injection H; clear H; intro H; subst p; simpl.
left; left; destruct l1 as [ | u1 l1]; simpl; [trivial | idtac];
apply list_permut_occurs_in_term_list with (Var (fresh_var pb) :: u1 :: l1);
[apply quick_permut | left; simpl; trivial].
generalize (W6 _ _ H); intros [[[H1 | H1'] | H1''] | [H2 | H3]].
right; left; simpl;
destruct (eq_variable_dec (new_var p) v1) as [_ | new_var_p_diff_v1]; trivial;
absurd (new_var p = v1); trivial.
left; left; destruct l1 as [ | u1 l1]; simpl; [contradiction | idtac];
apply list_permut_occurs_in_term_list with (Var (fresh_var pb) :: u1 :: l1);
[apply quick_permut | right; trivial].
left; right; trivial.
right; left; simpl; destruct (eq_variable_dec (new_var p) v1) as [_ | _]; trivial.
right; right; trivial.
unfold ac_elementary_solve_term_term_term in *.
pattern pb';
refine
(prop_map_without_repetition (B:=matching_problem) eq_term_dec _ _ _ _ pb' In_pb');
clear pb' In_pb'; intros [ | g2 ll2] In_t2; trivial;
destruct (eq_symbol_dec g1 g2) as [g1_eq_g2 | g1_diff_g2]; trivial.
generalize (in_remove _ eq_term_dec (Term g2 ll2) l2);
destruct (remove _ eq_term_dec (Term g2 ll2) l2) as [l2''' | ]; trivial.
intros [cp1' [l2' [l2'' [ H' [l2_eq l2'''_eq]]]]].
injection l2'''_eq; clear l2'''_eq; intro; subst l2''';
split.
intros t1 t2 [H | [H | In_l]]; [idtac | idtac | apply W1; right; trivial].
injection H; clear H; intros; subst t1 t2; split.
apply (well_formed_cf_subterms W_t1); left; trivial.
apply (well_formed_cf_subterms W_t2); subst l2 cp1';
apply in_or_app; right; left; trivial.
injection H; clear H; intros; subst t1 t2; split.
replace l1 with (nil ++ l1); trivial;
replace (Term g1 ll1 :: l1) with (nil ++ Term g1 ll1 :: l1) in W_t1; trivial;
apply well_formed_cf_build_inside with (Term g1 ll1); trivial.
subst; apply well_formed_cf_build_inside with (Term g2 ll2); trivial.
split; [intros; apply W2; right; trivial | idtac].
split; [intros; apply W3; right; trivial | idtac].
split; [intros; apply W4; right; trivial | idtac].
split; [intros; apply W5; right; trivial | idtac].
intros v p H; generalize (W6 v p H); intros [[[H1 | H1'] | H1''] | [H2 | H3]].
left; left; trivial.
left; right; left; destruct l1 as [ | u1 [ | u2 l1]]; [contradiction | intuition | idtac];
simpl; apply list_permut_occurs_in_term_list with (u1 :: u2 :: l1); trivial;
apply quick_permut.
left; right; right; trivial.
right; left; trivial.
right; right; trivial.
destruct l1 as [ | u1 [ | u2 [ | u3 l1]]]; [contradiction | contradiction | idtac | contradiction].
destruct l2 as [ | v1 [ | v2 [ | v3 l2]]]; [contradiction | contradiction | idtac | contradiction].
inversion_clear In_pb' as [pb'_eq_ | In_pb''];
[idtac | inversion_clear In_pb'' as [pb''_eq_ | ]; [idtac | contradiction]]; subst.
split.
intros t1 t2 [H | [H | In_l]]; [idtac | idtac | apply W1; right; trivial].
injection H; clear H; intros; subst t1 t2; split.
apply well_formed_cf_subterms with f1 (u1 :: u2 :: nil); [idtac | left; trivial];
refine (proj1 _ (B:= (well_formed_cf (Term f1 (v1 :: v2 :: nil))))); apply W1; left; trivial.
apply well_formed_cf_subterms with f1 (v1 :: v2 :: nil); [idtac | left; trivial];
apply (proj2 (A:= (well_formed_cf (Term f1 (u1 :: u2 :: nil))))); apply W1; left; trivial.
injection H; clear H; intros; subst t1 t2; split.
apply well_formed_cf_subterms with f1 (u1 :: u2 :: nil); [idtac | right; left; trivial];
refine (proj1 _ (B:= (well_formed_cf (Term f1 (v1 :: v2 :: nil))))); apply W1; left; trivial.
apply well_formed_cf_subterms with f1 (v1 :: v2 :: nil); [idtac | right; left; trivial];
apply (proj2 (A:= (well_formed_cf (Term f1 (u1 :: u2 :: nil))))); apply W1; left; trivial.
split; [intros; apply W2; right; trivial | idtac].
split; [intros; apply W3; right; trivial | idtac].
split; [intros; apply W4; right; trivial | idtac].
split; [intros; apply W5; right; trivial | idtac].
intros v p H; generalize (W6 v p H); intros [[[H1 | [H1' | H1'']] | H1'''] | [H2 | H3]].
left; left; trivial.
left; right; left; trivial.
contradiction.
left; right; right; trivial.
right; left; trivial.
right; right; trivial.
split.
intros t1 t2 [H | [H | In_l]]; [idtac | idtac | apply W1; right; trivial].
injection H; clear H; intros; subst t1 t2; split.
apply well_formed_cf_subterms with f1 (u1 :: u2 :: nil); [idtac | left; trivial];
refine (proj1 _ (B:= (well_formed_cf (Term f1 (v1 :: v2 :: nil))))); apply W1; left; trivial.
apply well_formed_cf_subterms with f1 (v1 :: v2 :: nil); [idtac | right; left; trivial];
apply (proj2 (A:= (well_formed_cf (Term f1 (u1 :: u2 :: nil))))); apply W1; left; trivial.
injection H; clear H; intros; subst t1 t2; split.
apply well_formed_cf_subterms with f1 (u1 :: u2 :: nil); [idtac | right; left; trivial];
refine (proj1 _ (B:= (well_formed_cf (Term f1 (v1 :: v2 :: nil))))); apply W1; left; trivial.
apply well_formed_cf_subterms with f1 (v1 :: v2 :: nil); [idtac | left; trivial];
apply (proj2 (A:= (well_formed_cf (Term f1 (u1 :: u2 :: nil))))); apply W1; left; trivial.
split; [intros; apply W2; right; trivial | idtac].
split; [intros; apply W3; right; trivial | idtac].
split; [intros; apply W4; right; trivial | idtac].
split; [intros; apply W5; right; trivial | idtac].
intros v p H; generalize (W6 v p H); intros [[[H1 | [H1' | H1'']] | H1'''] | [H2 | H3]].
left; left; trivial.
left; right; left; trivial.
contradiction.
left; right; right; trivial.
right; left; trivial.
right; right; trivial.
assert (L12 : length l1 = length l2).
apply trans_eq with n1; [idtac | apply sym_eq];
generalize (W1 (Term f1 l1) (Term f1 l2) (or_introl _ (refl_equal _)));
intros [[_ W_t1] [_ W_t2]]; [rewrite Af1 in W_t1 | rewrite Af1 in W_t2]; trivial.
split.
assert (W1_l : forall t1 t2, In (t1,t2) l -> well_formed_cf t1 /\ well_formed_cf t2).
intros; apply W1; right; trivial.
assert (W_l1 : forall t, In t l1 -> well_formed_cf t).
intros; apply well_formed_cf_subterms with f1 l1; trivial;
refine (proj1 _ (B:= (well_formed_cf (Term f1 l2)))); apply W1; left; trivial.
assert (W_l2 : forall t, In t l2 -> well_formed_cf t).
intros; apply well_formed_cf_subterms with f1 l2; trivial;
apply (proj2 (A:= (well_formed_cf (Term f1 l1)))); apply W1; left; trivial.
generalize l l2 In_pb' L12 W1_l W_l1 W_l2; simpl;
clear W1 W2 W3 W4 W5 W6 Fresh_var_spec l l2 In_pb' L12 W1_l W_l1 W_l2;
induction l1 as [ | t1 l1]; destruct l2 as [ | t2 l2].
intros [In_pb' | In_pb'] _; [idtac | contradiction]; subst pb'; simpl; trivial.
intros _ L12; simpl L12; discriminate.
intros _ L12; simpl L12; discriminate.
intros In_pb' L12; simpl in L12; generalize (eq_add_S _ _ L12); clear L12; intro L12;
intros W1_l W_l1 W_l2; intros; apply IHl1 with ((t1, t2) :: l) l2; trivial.
intros t4 t5 [H' | In_l].
injection H'; split; subst; [apply W_l1 | apply W_l2]; left; trivial.
apply W1_l; trivial.
intros; apply W_l1; right; trivial.
intros; apply W_l2; right; trivial.
assert (H : forall l', l' = l ->
fold_left2 (fun (current_list_of_eqs : list (term * term)) (t1 t2 : term) =>
(t1, t2) :: current_list_of_eqs) l' l1 l2 =
fold_left2 (fun (current_list_of_eqs : list (term * term)) (t1 t2 : term) =>
(t1, t2) :: current_list_of_eqs) l l1 l2). intros; subst; trivial.
destruct (fold_left2
(fun (current_list_of_eqs : list (term * term)) (t1 t2 : term) =>
(t1, t2) :: current_list_of_eqs) l l1 l2) as [new_list_of_equations | ];
generalize (H l (refl_equal _)); clear H; intro H;
[idtac | contradiction].
destruct In_pb' as [pb'_eq | ]; [idtac | contradiction]; subst.
split; [intros; apply W2; right; trivial | idtac].
split; [intros; apply W3; right; trivial | idtac].
split; [intros; apply W4; right; trivial | idtac].
split; [intros; apply W5; right; trivial | idtac].
assert (H' : forall l1 l new_list_of_equations l2,
fold_left2 (fun cl (t1 t2 : term) => (t1, t2) :: cl) l l1 l2 = Some new_list_of_equations ->
forall u1 u2, In (u1, u2) l -> In (u1, u2) new_list_of_equations).
clear l l1 l2 W1 W6 Fresh_var_spec L12 H new_list_of_equations.
induction l1 as [ | v1 l1].
intros l new_list_of_equations [ | v2 l2]; simpl; [idtac | intros; discriminate];
intros H; injection H; intro; subst; trivial.
intros l new_list_of_equations [| v2 l2]; simpl; [intros; discriminate | idtac].
intros; apply IHl1 with ((v1,v2) :: l) l2; trivial; right; trivial.
intros v p H''; generalize (W6 v p H''); intros [ [H1 | H1'] | [H2 | H3]].
left; simpl occurs_in_term in H1; unfold unsolved_part.
generalize l l2 L12 H H1; clear l l2 W1 W6 Fresh_var_spec L12 H H1;
induction l1 as [ | u1 l1]; [contradiction | idtac].
intros l [| u2 l2] L12 H; [discriminate | idtac]; intros [In_u1 | In_l1].
assert (In_u1_new_list : In (u1,u2) new_list_of_equations).
simpl in H; apply H' with l1 ((u1,u2) :: l) l2; trivial; left; trivial.
generalize new_list_of_equations In_u1_new_list;
clear new_list_of_equations H'' IHl1 H In_u1_new_list;
induction new_list_of_equations as [| [w1 w2] nle]; [contradiction | idtac].
intros [u12_eq | In_u12]; [injection u12_eq; intros; subst; left; trivial | idtac].
right; apply IHnle; trivial.
apply IHl1 with ((u1,u2) :: l) l2; trivial; apply eq_add_S; trivial.
left; assert (H''' : exists u1, exists u2, occurs_in_term (new_var p) u1 /\ In (u1, u2) l).
generalize (new_var p) l H1'; clear l H1' W1 W6 Fresh_var_spec H H'';
induction l as [ | [u1 u2] l]; [contradiction | idtac]; intros [u12_eq | In_u12].
exists u1; exists u2; intuition.
generalize (IHl In_u12);
intros [u3 [u4 [H1 H2]]]; exists u3; exists u4; split; trivial; right; trivial.
generalize H'''; clear H'''; intros [u1 [u2 [H''' In_u12]]];
generalize (H' _ _ _ _ H _ _ In_u12); clear l W1 W6 Fresh_var_spec H H1' In_u12 H'';
induction new_list_of_equations as [ | [v1 v2] nle]; [contradiction | idtac];
intros [u12_eq | In_u12].
injection u12_eq; intros; subst; left; trivial.
right; apply IHnle; trivial.
right; left; trivial.
right; right; trivial.
Qed.
End Make.