proposition: Lemma merge1_decreases : forall x g l2 l sigma x_val, find X.eq_bool x sigma = Some x_val -> size (Term g l2) < size x_val -> lt_pb (mk_pb ((x, Term g l2) :: sigma) ((x_val, Term g l2) :: l)) (mk_pb sigma ((Var x, Term g l2) :: l)).
proof: Proof. intros x g l2 l sigma x_val x_sigma L; unfold lt_pb, measure_for_unif_pb; apply lex_le_meq_lt. generalize (Term g l2) L; clear g l2 L; intros t2 L. unfold phi1; apply VSet.cardinal_subset; apply VSet.subset_filter. apply VSet.subset_subset_union. simpl; intros z z_in_x_val_t2_l; destruct_set z_in_x_val_t2_l z_in_x_val_t2 x_in_l. destruct_set z_in_x_val_t2 z_in_x_val z_in_t2. do 2 apply VSet.union_2; apply (solved_var_inc_occ_in_subst _ _ _ _ x_sigma z_in_x_val). do 2 apply VSet.union_1; apply VSet.union_2; trivial. apply VSet.union_1; apply VSet.union_2; trivial. simpl; intros z z_in_x_dom_sig_t2_sigma; destruct_set z_in_x_dom_sig_t2_sigma z_in_x_dom_sig z_in_t2_sigma. destruct (VSet.add_12 _ _ _ z_in_x_dom_sig) as [z_in_x | z_in_dom_sig]. do 3 apply VSet.union_1; left; subst; trivial. apply VSet.union_2; apply VSet.union_1; trivial. destruct_set z_in_t2_sigma z_in_t2 z_in_sigma. do 2 apply VSet.union_1; apply VSet.union_2; trivial. do 2 apply VSet.union_2; trivial. intros z; do 2 (rewrite Dummy_bool; rewrite not_solved_var); simpl. generalize (X.eq_bool_ok z x); case (X.eq_bool z x); [intro z_eq_x; subst z | intro z_diff_x]. intros _; rewrite x_sigma; left; do 2 apply VSet.union_1; left; subst; reflexivity. case_eq (find X.eq_bool z sigma); [ intros z_val z_sigma | intro z_sigma ]. intros [ z_in_x_val_t2_l | z_in_t2_sigma]. destruct_set z_in_x_val_t2_l z_in_x_val_t2 z_in_l. destruct_set z_in_x_val_t2 z_in_x_val z_in_t2. right; apply (solved_var_inc_occ_in_subst x z x_val); trivial. left; apply VSet.union_1; apply VSet.union_2; trivial. left; apply VSet.union_2; trivial. destruct_set z_in_t2_sigma z_in_t2 z_in_sigma. left; apply VSet.union_1; apply VSet.union_2; trivial. right; trivial. trivial. generalize (Term g l2) L; clear g l2 L; intros t2 L. assert (x_in_dom_sig : VSet.mem x (domain_of_subst sigma)). unfold VSet.mem; induction sigma as [ | [y t] sigma]. discriminate. simpl in x_sigma; revert x_sigma; generalize (X.eq_bool_ok x y); case (X.eq_bool x y); [intro x_eq_y; subst y | intro x_diff_y]. intros _; apply VSet.add_1. intro x_sigma; apply VSet.add_2;apply IHsigma; trivial. destruct (mem_split_set _ _ X.eq_bool_ok _ _ x_in_dom_sig) as [x' [s1 [s2 [x_eq_x' [dom_sig_eq_s1_x_s2 _]]]]]; simpl in x_eq_x'; simpl in dom_sig_eq_s1_x_s2. unfold VSet.LP.EDS.eq_A, VSet.EDS.eq_A, DecVar.eq_A in *; subst x'. unfold phi2, size_of_solved_part, size_of_unsolved_part; simpl. replace (VSet.add x (domain_of_subst sigma)) with (domain_of_subst sigma). rewrite max_l; [idtac | auto with arith]. rewrite dom_sig_eq_s1_x_s2; do 2 rewrite list_size_mul_app. simpl; generalize (X.eq_bool_ok x x); case (X.eq_bool x x); [intros _ | intro x_diff_x; apply False_rect; apply x_diff_x; reflexivity]. rewrite x_sigma. generalize (size_ge_one t2); destruct (size t2) as [ | n2]; [intro; absurd (1 <= 0); auto with arith | intros _ ]. apply NatMul.mult_is_complete_equiv. rewrite <- ass_app; rewrite <- app_comm_cons; rewrite <- NatMul.LP.permut_add_inside. rewrite <- ass_app; rewrite <- app_comm_cons; rewrite ass_app; rewrite <- NatMul.LP.permut_add_inside. rewrite ass_app; rewrite <- NatMul.LP.permut_app2. do 2 rewrite <- list_size_mul_app. assert (x_not_in_s1_s2 : ~mem (@eq _) x (s1 ++ s2)). assert (W := VSet.is_a_set (domain_of_subst sigma)). rewrite dom_sig_eq_s1_x_s2 in W. assert (P : VSet.LP.permut (x :: s1 ++ s2) (s1 ++ x :: s2)). rewrite <- VSet.LP.permut_cons_inside; reflexivity. assert (W'' := VSet.without_red_permut W (VSet.LP.permut_sym P)). generalize (VSet.without_red_permut W (VSet.LP.permut_sym P)). unfold VSet.without_red; simpl; unfold DecVar.A, DecVar.eq_bool. generalize (mem_bool_ok _ _ X.eq_bool_ok x (s1 ++ s2)); case (mem_bool X.eq_bool x (s1 ++ s2)). intros; discriminate. intros; assumption. generalize (s1 ++ s2) x_not_in_s1_s2; intros s x_not_in_s; induction s as [ | v s]. apply NatMul.LP.permut_refl. simpl; generalize (X.eq_bool_ok v x); case (X.eq_bool v x); [intro v_eq_x | intro v_diff_x]. absurd (mem (@eq _) x (v :: s)); trivial; subst; left; reflexivity. rewrite <- NatMul.LP.permut_cons. apply IHs; intro; apply x_not_in_s; right; trivial. reflexivity. reflexivity. reflexivity. rewrite VSet.already_mem_add. reflexivity. unfold VSet.mem; rewrite dom_sig_eq_s1_x_s2. rewrite <- mem_or_app; right; left; reflexivity. unfold phi3, nb_var_eq_of_unsolved_part; simpl. destruct x_val as [v | f l1]. simpl in L; assert (L' := Nat.nle_succ_0 _ (proj2 (Nat.succ_lt_mono _ _) L)); contradiction. auto with arith. Defined.
imports: Coq(Arith Wf_nat Wellfounded List Multiset Relations) CoLoR(closure decidable_set ordered_set more_list list_permut list_set list_sort dickson term_spec term)