proposition: Lemma remove_trivial_eq_decreases : forall s l sigma, lt_pb (mk_pb sigma l) (mk_pb sigma ((s,s) :: l)).
proof: Proof. intros s l sigma; unfold lt_pb, measure_for_unif_pb; apply lex_le_lt. unfold phi1; apply VSet.cardinal_subset; apply VSet.subset_filter. apply VSet.union_compat_subset_1. simpl; intro v; apply VSet.union_2; trivial. intro v; case_eq (is_a_solved_var v (mk_pb sigma l)). intros _ Abs; discriminate. intros H _; assert (H' : is_a_solved_var v (mk_pb sigma ((s, s) :: l)) = false). revert H; do 2 rewrite not_solved_var. case (find X.eq_bool v sigma); [intros _ | trivial]. intros [H | H]. left; apply VSet.union_2; trivial. right; trivial. rewrite H'; reflexivity. unfold lt_mul, phi2, size_of_unsolved_part, size_of_solved_part; simpl. refine (NatMul.mult_is_complete_less_than _ _ _ _ _). apply lt_bool_ok. intros n1 n2 n3; apply Nat.lt_trans. apply Nat.lt_irrefl. left; refine (@NatMul.rmv_case lt _ _ (list_size_mul _ (fun x => match find X.eq_bool x sigma with | Some x_val => size x_val | None => 0 end) (VSet.support (domain_of_subst sigma)) ++ list_size_mul (term * term) (fun s_t : term * term => let (s0, t) := s_t in max (size s0) (size t)) l) nil (max (size s) (size s)) _ _ _). intros; contradiction. reflexivity. symmetry. rewrite <- NatMul.LP.permut_cons_inside; 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)