proposition: Lemma decomposition_decreases : forall f l1 l2 l sigma, lt_pb (mk_pb sigma (combine term l l1 l2)) (mk_pb sigma ((Term f l1, Term f l2) :: l)).
proof: Proof. intros f l1 l2 l sigma; unfold lt_pb, measure_for_unif_pb; apply lex_le_lt. assert (H : forall z, VSet.mem z (set_of_variables_in_unsolved_part (combine term l l1 l2)) -> VSet.mem z (set_of_variables_in_unsolved_part ((Term f l1, Term f l2) :: l))). unfold set_of_variables_in_unsolved_part at 2. unfold set_of_variables. revert l2 l; induction l1 as [ | t1 l1]; intros [ | t2 l2] l z. simpl; intros; apply VSet.union_2; trivial. simpl; intros; apply VSet.union_2; trivial. simpl; intros; apply VSet.union_2; trivial. intro H; assert (z_in_l1l2_t1t2l := IHl1 l2 ((t1,t2) :: l) z H). destruct_set z_in_l1l2_t1t2l z_in_l1l2 z_in_t1t2l. destruct_set z_in_l1l2 z_in_l1 z_in_l2. apply VSet.union_1; apply VSet.union_1; apply VSet.union_2; trivial. apply VSet.union_1; apply VSet.union_2; apply VSet.union_2; trivial. destruct_set z_in_t1t2l z_in_t1t2 z_in_l. destruct_set z_in_t1t2 z_in_t1 z_in_t2. do 3 apply VSet.union_1; trivial. apply VSet.union_1; apply VSet.union_2; apply VSet.union_1; trivial. apply VSet.union_2; trivial. unfold phi1; apply VSet.cardinal_subset; apply VSet.subset_filter. apply VSet.subset_subset_union. intros z z_in_l1_l2_l; generalize (H _ z_in_l1_l2_l); clear z_in_l1_l2_l; intro z_in_l1_l2_l. destruct_set z_in_l1_l2_l z_in_l1_l2 z_in_l. destruct_set z_in_l1_l2 z_in_l1 z_in_l2. simpl; do 3 apply VSet.union_1; trivial. simpl; do 2 apply VSet.union_1; apply VSet.union_2; trivial. simpl; apply VSet.union_1; apply VSet.union_2; trivial. apply VSet.subset_subset_union. intros z z_in_dom_sig; apply VSet.union_2; apply VSet.union_1; trivial. intros z z_in_sigma; do 2 apply VSet.union_2; trivial. intro z; do 2 (rewrite Dummy_bool; rewrite not_solved_var); simpl; destruct (find X.eq_bool z sigma) as [z_val | ]; trivial. intros [H1 | H1]. left; apply H; trivial. right; trivial. apply NatMul.mult_is_complete_less_than with lt. exact lt_bool_ok. intros n1 n2 n3; apply Nat.lt_trans. apply Nat.lt_irrefl. unfold phi2, size_of_solved_part, size_of_unsolved_part; simpl. unfold lt_mul; apply NatMul.context_trans_clos_multiset_extension_step_app1. do 2 rewrite (list_size_fold size). revert l2 l; induction l1 as [ | t1 l1]; intros [ | t2 l2] l. left; simpl; refine (@NatMul.rmv_case lt _ _ (list_size_mul (term * term) (fun s_t : term * term => let (s, t) := s_t in max (size s) (size t)) l) nil 1 _ _ _); try apply NatMul.LP.permut_refl. intros; contradiction. left; simpl; refine (@NatMul.rmv_case lt _ _ (list_size_mul (term * term) (fun s_t : term * term => let (s, t) := s_t in max (size s) (size t)) l) nil _ _ _ _); try apply NatMul.LP.permut_refl. intros; contradiction. left; simpl; refine (@NatMul.rmv_case lt _ _ (list_size_mul (term * term) (fun s_t : term * term => let (s, t) := s_t in max (size s) (size t)) l) nil _ _ _ _); try apply NatMul.LP.permut_refl. intros; contradiction. generalize (IHl1 l2 ((t1,t2) :: l)). simpl list_size; simpl combine; simpl list_size_mul. generalize (size_ge_one t1) (size_ge_one t2). generalize (list_size_mul (term * term) (fun s_t : term * term => let (s, t) := s_t in max (size s) (size t)) (combine term ((t1, t2) :: l) l1 l2)) (list_size size l1) (list_size size l2) (size t1) (size t2) (list_size_mul (term * term) (fun s_t : term * term => let (s, t) := s_t in max (size s) (size t)) l). clear t1 l1 sigma IHl1 t2 l2 l. intros nl nl1 nl2 nt1 nt2 n H1 H2. intro H; refine (@trans_clos_is_trans _ (NatMul.multiset_extension_step lt) _ _ _ H _). left; apply (NatMul.rmv_case lt (l1 := S (max nl1 nl2) :: max nt1 nt2 :: n) (l2 := S (max (nt1 + nl1) (nt2 + nl2)) :: n) (l := n) (S (max nl1 nl2) :: max nt1 nt2 :: nil) (a := S (max (nt1 + nl1) (nt2 + nl2)))). unfold NatMul.DS.eq_A. intros b [b_eq | [b_eq | b_in_nil]]. subst b. apply le_n_S; apply (Nat.max_case nl1 nl2). refine (Nat.le_trans _ _ _ _ (Nat.le_max_l _ _)); destruct nt1 as [ | nt1]. inversion H1. simpl; apply le_n_S; apply NatCompat.le_add_l. refine (Nat.le_trans _ _ _ _ (Nat.le_max_r _ _)); destruct nt2 as [ | nt2]. inversion H2. simpl; apply le_n_S; apply NatCompat.le_add_l. subst b; apply (Nat.max_case nt1 nt2). simpl; apply le_n_S; refine (Nat.le_trans _ _ _ _ (Nat.le_max_l _ _)); apply Nat.le_add_r. simpl; apply le_n_S; refine (Nat.le_trans _ _ _ _ (Nat.le_max_r _ _)); apply Nat.le_add_r. contradiction. reflexivity. reflexivity. 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)