proposition: Theorem lt_inc_rpo_0 : forall n, forall o' o, (T1_size o + T1_size o' <= n)%nat-> lt o o' -> nf o -> nf o' -> rpo (T1_2_term o) (T1_2_term o').
proof: Proof. induction n. - destruct o'. + intros; destruct (not_lt_zero H0). + destruct o; simpl; inversion 1. - intros o' o H H0 H1 H2; destruct o, o'. + now apply not_lt_zero in H0. + simpl; apply Top_gt. * simpl; trivial. * inversion 1. + destruct (not_lt_zero H0). + destruct (lt_inv H0) as [H3 | H3]. * simpl; intros; apply Top_eq_lex. -- simpl;trivial. -- left. ++ apply IHn. apply Nat.lt_succ_r. apply Nat.lt_le_trans with (T1_size (cons o1 n0 o2) + T1_size (cons o'1 n1 o'2))%nat. simpl; auto with arith rpo. abstract lia. auto. auto. eauto with T1. eauto with T1. ++ simpl;auto with rpo. -- inversion_clear 1. ** subst s'. change (rpo (T1_2_term o1) (T1_2_term (cons o'1 n1 o'2))). apply IHn;auto with rpo. apply Nat.lt_succ_r. apply Nat.lt_le_trans with (T1_size (cons o1 n0 o2) + T1_size (cons o'1 n1 o'2))%nat. auto with arith rpo. auto with rpo. eauto with T1 rpo. ** destruct H5 as [|[|H8]]. subst s'; apply nat_lt_cons. subst s'; change (rpo (T1_2_term o2) (T1_2_term (cons o'1 n1 o'2))). apply IHn;auto with rpo. apply Nat.lt_succ_r. apply Nat.lt_le_trans with (T1_size (cons o1 n0 o2) + T1_size (cons o'1 n1 o'2))%nat. auto with arith rpo. auto with rpo. eauto with rpo. eauto with T1. case H8. * simpl;apply Top_eq_lex. decompose [or and] H3. -- auto with rpo. -- subst; auto. -- decompose [or and] H3. ++ subst; constructor 2. constructor 1. apply nat_2_term_mono. auto. auto. ++ subst; decompose [or and] H3. destruct (Nat.lt_irrefl _ H6). subst; apply List_eq. apply List_eq. apply List_gt. eapply IHn; eauto. simpl in H; ring_simplify in H. clear IHn; simpl in H; abstract lia. eauto with T1. eauto with T1. reflexivity. -- decompose [or and] H3. ++ clear H3; subst; inversion_clear 1. subst s'. change (rpo (T1_2_term o'1) (T1_2_term (cons o'1 n1 o'2))). apply IHn;auto. apply Nat.lt_succ_r. apply Nat.lt_le_trans with (T1_size (cons o'1 n0 o2) + T1_size (cons o'1 n1 o'2))%nat. auto with arith rpo. auto with rpo. apply head_lt_cons. eauto with T1. destruct H4 as [|[|H8]]. subst s'; apply nat_lt_cons. ** subst s'. change (rpo (T1_2_term o2) (T1_2_term (cons o'1 n1 o'2))). apply IHn;auto with rpo. apply Nat.lt_succ_r. apply Nat.lt_le_trans with (T1_size (cons o'1 n0 o2) + T1_size (cons o'1 n1 o'2))%nat. auto with arith rpo. auto with rpo. apply lt_le_trans with (cons o'1 0 zero). apply lt_a_phi0_b_phi0. eapply lt_a_phi0_b_intro. eauto. auto with T1 rpo. auto with T1 rpo. apply lt_incl_le. apply LT3. eauto with T1. eauto with T1. eauto with arith. eauto with T1. ** inversion H8. ++ subst o'1 n1; clear H3. inversion_clear 1. subst. change (rpo (T1_2_term o1) (T1_2_term (cons o1 n0 o'2))). apply IHn; auto. apply Nat.lt_succ_r. apply Nat.lt_le_trans with (T1_size (cons o1 n0 o2) + T1_size (cons o1 n0 o'2))%nat. auto with arith rpo. auto with rpo. apply head_lt_cons. eauto with T1 rpo. inversion_clear H4. subst s'. apply nat_lt_cons. inversion_clear H3. subst s'; apply Eps0_rpo.rpo_trans with (T1_2_term o'2). apply Subterm with (T1_2_term o'2). simpl. right; right; now left. apply Eq. apply IHn; eauto with T1 rpo. simpl in H; clear IHn; abstract lia. inversion H4. Qed.
imports: Coq(Arith Lia Compare_dec Relations Wellfounded Wf_nat List Bool Eqdep_dec Ensembles ArithRing Logic) hydras(More_Arith Restriction DecPreOrder rpo.term rpo.rpo Epsilon0.T1)