proposition: Theorem lt_inc_rpo_0 : forall n, forall o' o, (T1_size o + T1_size o' <= n)%nat-> o < o' -> nf o -> nf o' -> rpo (T1_2_term o) (T1_2_term o').
proof: Proof. induction n. destruct o'. inversion 2. destruct o. simpl. inversion 1. simpl;inversion 1. inversion 2. simpl. intros; apply Top_gt. simpl;trivial. inversion 1. simpl; intros; apply Top_eq_lex. simpl;trivial. left. apply IHn. subst o;subst o'. apply lt_n_Sm_le . apply Lt.lt_le_trans with (T1_size (cons a n0 b) + T1_size (cons a' n' b'))%nat. simpl; auto with arith. omega. auto. auto. nf_inv. nf_inv. simpl;auto. inversion_clear 1. subst s'. change (rpo (T1_2_term a) (T1_2_term (cons a' n' b'))). apply IHn;auto. subst o;subst o'. apply lt_n_Sm_le . apply Lt.lt_le_trans with (T1_size (cons a n0 b) + T1_size (cons a' n' b'))%nat. auto with arith. auto. nf_inv. destruct H7 as [|[|H8]]. subst s'. apply nat_lt_cons. subst s'. change (rpo (T1_2_term b) (T1_2_term (cons a' n' b'))). apply IHn;auto. subst o;subst o'. apply lt_n_Sm_le . apply Lt.lt_le_trans with (T1_size (cons a n0 b) + T1_size (cons a' n' b'))%nat. auto with arith. auto. eauto. nf_inv. case H8. intros. simpl;apply Top_eq_lex. auto. constructor 2. constructor 1. apply nat_2_term_mono. auto. auto. inversion_clear 1. subst s'. change (rpo (T1_2_term a) (T1_2_term (cons a n' b'))). apply IHn;auto. subst o;subst o'. apply lt_n_Sm_le . apply Lt.lt_le_trans with (T1_size (cons a n0 b) + T1_size (cons a n' b'))%nat. auto with arith. auto. apply head_lt_cons. nf_inv. destruct H7 as [|[|H8]]. subst s'. apply nat_lt_cons. subst s'. change (rpo (T1_2_term b) (T1_2_term (cons a n' b'))). apply IHn;auto. subst o;subst o'. apply lt_n_Sm_le . apply Lt.lt_le_trans with (T1_size (cons a n0 b) + T1_size (cons a n' b'))%nat. auto with arith. auto. apply lt_le_trans with (cons a 0 zero). inversion H4. auto with T1. auto with T1. case n'. apply le_tail;auto with T1. auto with T1 arith. nf_inv. case H8. simpl. intros;apply Top_eq_lex. auto. right. right. left. apply IHn. apply lt_n_Sm_le . apply Lt.lt_le_trans with (T1_size (cons a n0 b) + T1_size (cons a n0 b'))%nat. apply plus_lt_compat. auto. auto. subst o;subst o';auto. auto. nf_inv. nf_inv. auto. inversion_clear 1. subst s'. eapply Subterm. 2:eleft. left;auto. destruct H7 as [|[|H8]]. subst s'. apply nat_lt_cons. subst s'. change (rpo (T1_2_term b) (T1_2_term (cons a n0 b'))). apply IHn. apply lt_n_Sm_le . apply Lt.lt_le_trans with (T1_size (cons a n0 b) + T1_size (cons a n0 b'))%nat. auto with arith. subst o;subst o'. auto. apply lt_le_trans with (cons a 0 zero). inversion H4. auto with T1. auto with T1. case n0. apply le_tail;auto with T1. auto with T1 arith. nf_inv. auto. case H8. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List