proposition: Lemma move_eq_decreases : forall x g l2 l sigma, find X.eq_bool x sigma = None -> lt_pb (mk_pb ((x, Term g l2) :: sigma) l) (mk_pb sigma ((Var x, Term g l2) :: l)).
proof: Proof. intros x g l2 l sigma x_sigma; unfold lt_pb, measure_for_unif_pb; apply lex_le_meq_lt. generalize (Term g l2); clear g l2; intro t2; unfold phi1; apply VSet.cardinal_subset. apply VSet.subset_filter. simpl. apply VSet.subset_subset_union. intros z z_in_l; apply VSet.union_1; apply VSet.union_2; trivial. apply VSet.subset_subset_union. intros z z_in_x_dom_sig; destruct (VSet.add_12 _ _ _ z_in_x_dom_sig) as [z_eq_x | z_in_dom_sig]. do 3 apply VSet.union_1; left; subst; trivial. apply VSet.union_2; apply VSet.union_1; trivial. apply VSet.subset_subset_union. intros z z_in_t2; do 2 apply VSet.union_1; apply VSet.union_2; trivial. intros z z_in_sigma; 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]. rewrite x_sigma; trivial. destruct (find X.eq_bool z sigma) as [z_val | ]; trivial. intros [z_in_l | z_in_t2_sigma]. 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. apply NatMul.mult_is_complete_equiv. unfold phi2, size_of_solved_part, size_of_unsolved_part. generalize (Term g l2); intro t2; clear g l2; simpl solved_part; simpl unsolved_part. assert (x_not_in_dom_sig : ~ VSet.mem x (domain_of_subst sigma)). induction sigma as [ | [y t] sigma]. intro; contradiction. simpl in x_sigma; intro x_in_y_dom_sig; destruct (VSet.add_12 _ _ _ x_in_y_dom_sig) as [x_eq_y | x_in_dom_sig]; clear x_in_y_dom_sig. unfold VSet.LP.EDS.eq_A, VSet.EDS.eq_A, DecVar.eq_A in *; subst y. revert x_sigma; generalize (X.eq_bool_ok x x); case (X.eq_bool x x); [intros _; discriminate | intro x_diff_x; apply False_rect; apply x_diff_x; reflexivity]. apply IHsigma; trivial. revert x_sigma; case (X.eq_bool x y); trivial; intros; discriminate. replace (VSet.support (domain_of_subst ((x, t2) :: sigma))) with (x :: (VSet.support (domain_of_subst sigma))). 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]. generalize (size_ge_one t2); case (size t2). intro Abs; apply False_rect; apply (Nat.nlt_0_r _ Abs). intros n _; rewrite <- NatMul.LP.permut_cons_inside. rewrite <- NatMul.LP.permut_app2. clear l; revert x_not_in_dom_sig; unfold VSet.mem, DecVar.eq_A. generalize (VSet.support (domain_of_subst sigma)); fix move_eq_decreases 1. intro l; case l; clear l. intros _; reflexivity. simpl; intros a l x_not_in_al. generalize (X.eq_bool_ok a x); case (X.eq_bool a x); [intro a_eq_x | intros _]. apply False_rect; apply x_not_in_al; left; symmetry; assumption. rewrite <- NatMul.LP.permut_cons. apply move_eq_decreases. intro x_in_l; apply x_not_in_al; right; assumption. reflexivity. reflexivity. revert x_not_in_dom_sig; simpl; apply VSet.not_already_mem_add. unfold phi3, nb_var_eq_of_unsolved_part; simpl; 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)