proposition: Lemma inv_solved_part_e : forall pb, Inv_solved_part pb \/ pb.(unsolved_part) = nil -> Inv_solved_part_e (decomposition_step pb).
proof: Proof. intros [sigma [ | [s t] l]] [Inv_pb | l_eq_nil]. simpl; trivial. simpl; trivial. generalize (inv_solved_part _ Inv_pb); unfold decomposition_step; simpl. case (T1.eq_bool s t). trivial. destruct s as [x | f1 l1]; destruct t as [y | f2 l2]. case (find X.eq_bool x (map_subst (fun (_ : variable) (v_sigma : term) => apply_subst ((x, Var y) :: nil) v_sigma) sigma)); trivial. case (find X.eq_bool x sigma); trivial. intro x_val; case (lt_ge_dec (T.size (Term f2 l2)) (T.size x_val)); trivial. case (find X.eq_bool y sigma); trivial. intro y_val; case (lt_ge_dec (T.size (Term f1 l1)) (T.size y_val)); trivial. case (F.Symb.eq_bool f1 f2); trivial. case (Nat.eqb (length l1) (length l2)); trivial. discriminate. 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)