proposition: Lemma merge2_decreases : forall x g l2 l sigma x_val, Inv_solved_part (mk_pb sigma ((Var x, Term g l2) :: l)) -> find X.eq_bool x sigma = Some x_val -> size (Term g l2) >= size x_val -> lt_pb (mk_pb 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 Inv_pb x_sigma L; assert (x_in_dom_sig : VSet.mem x (domain_of_subst sigma)). clear Inv_pb; 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 x | intro x_diff_y]. intros _; apply VSet.add_1. intro; apply VSet.add_2; apply IHsigma; trivial. unfold lt_pb, measure_for_unif_pb; apply lex_le_meq_lt. generalize (Term g l2) L; clear g l2 L Inv_pb; 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 z_in_l. destruct_set z_in_x_val_t2 z_in_x_val z_in_t2. do 2 apply VSet.union_2; refine (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. apply VSet.subset_subset_union. simpl; intros z z_in_dom_sig; apply VSet.union_2; apply VSet.union_1; trivial. simpl; intros z z_in_sigma; do 2 apply VSet.union_2; trivial. intros z; do 2 (rewrite Dummy_bool; rewrite not_solved_var); simpl. destruct (find X.eq_bool z sigma) as [ z_val | ]; trivial. intros [z_in_x_val_t2_l | z_in_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. right; trivial. unfold phi2, size_of_unsolved_part, size_of_solved_part. generalize (Term g l2) L; clear g l2 L Inv_pb; intros t2 L. simpl; rewrite max_r; [idtac | unfold ge; trivial]. generalize (size_ge_one t2); destruct (size t2) as [ | n2]; [intro; absurd (1<=0); auto with arith | intros _]. apply NatMul.mult_is_complete_equiv. apply NatMul.LP.permut_refl. destruct x_val as [ v | f l']. apply False_rect. generalize (Inv_pb x); simpl; rewrite x_sigma. rewrite solved_var; rewrite x_sigma. intros [ H _ ]; apply H; do 2 apply VSet.union_1; left; reflexivity. 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)