proposition: Lemma lt_inc_rpo_0 : forall n, forall o' o, (T2_size o + T2_size o' <= n)%nat-> o < o' -> nf o -> nf o' -> rpo (T2_2_term o) (T2_2_term o').
proof: Proof. induction n. destruct o;destruct o'. inversion 2. simpl. inversion 1. inversion 2. simpl. inversion 1. destruct o'. inversion 2. destruct o. intros. case (cons_rw o'1 o'2 n0 o'3). intros (H'1,(H'2,H'3)). rewrite H'3. simpl;apply Top_gt. simpl;auto with T2. destruct 1. intro H3;rewrite H3. simpl;apply Top_gt. simpl;auto with T2. destruct 1. intros. case (le_lt_or_eq _ _ H). intros;apply IHn;auto with arith T2. intros; eapply lt_rpo_cons_cons;eauto with T2. Qed.
imports: EPSILON0 Arith List Omega Compare_dec Relations Wellfounded Max Tools More_nat AccP not_decreasing EPSILON0 More_nat Gamma0_prelude Gamma0_length term rpo