proposition: Lemma decomposition_step_decreases : forall pb, Inv_solved_part pb -> match decomposition_step pb with | Normal _ pb' => lt_pb pb' pb | _ => True end.
proof: Proof. intros [sigma [ | [s t] l]] Inv_pb; simpl; trivial. unfold decomposition_step; simpl unsolved_part; cbv iota beta. generalize (T1.eq_bool_ok s t); case (T1.eq_bool s t); [intro s_eq_t | intro s_diff_t]. subst s; apply remove_trivial_eq_decreases. destruct s as [ x | f l1 ]; destruct t as [ y | g l2]. assert (Hx := find_map_subst x x (Var y) sigma). case_eq (find X.eq_bool x sigma); [intros x_val x_sigma | intro x_sigma ]; rewrite x_sigma in Hx; simpl solved_part; rewrite Hx. apply coalesce1_decreases; trivial; intro; apply s_diff_t; subst; trivial. apply coalesce2_decreases; trivial; intro; apply s_diff_t; subst; trivial. simpl solved_part. case_eq (find X.eq_bool x sigma); [intros x_val x_sigma | intro x_sigma ]. destruct (lt_ge_dec (T.size (Term g l2)) (T.size x_val)) as [t2_lt_x_val | t2_ge_x_val]. apply merge1_decreases; trivial. apply merge2_decreases; trivial. apply move_eq_decreases; trivial. simpl solved_part. case_eq (find X.eq_bool y sigma); [intros y_val y_sigma | intro y_sigma ]. destruct (lt_ge_dec (T.size (Term f l1)) (T.size y_val)) as [t1_lt_y_val | t1_ge_y_val]. unfold lt_pb; rewrite (measure_for_unif_pb_swapp_eq (Term f l1)); apply merge1_decreases; trivial. unfold lt_pb; rewrite (measure_for_unif_pb_swapp_eq (Term f l1)); apply merge2_decreases; trivial. unfold Inv_solved_part in *; simpl solved_part in *; intros x; generalize (Inv_pb x). destruct (find X.eq_bool x sigma) as [[v | f' l'] | ]; trivial. intro H; rewrite solved_var_swapp_eq; trivial. unfold lt_pb; rewrite (measure_for_unif_pb_swapp_eq (Term f l1)); apply move_eq_decreases; trivial. generalize (F.Symb.eq_bool_ok f g); case (F.Symb.eq_bool f g); [intro f_eq_g; subst g | intros _; trivial]. generalize (beq_nat_ok (length l1) (length l2)); case (Nat.eqb (length l1) (length l2)); intro L; trivial. simpl solved_part; apply decomposition_decreases. 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)