proposition: Lemma lt_rpo_cons_cons : rpo (T2_2_term (gcons a1 b1 n1 c1)) (T2_2_term (gcons a2 b2 n2 c2)).
proof: Proof. inversion H. - assert (rpo (T2_2_term a1) (T2_2_term a2)). apply Hrec. + simpl in Hsize;lia. + auto with T2. + auto with T2. + auto with T2. + assert (rpo (T2_2_term b1) (Term ord_psi ((T2_2_term a2):: ((T2_2_term b2)::nil)))). { change (rpo (T2_2_term b1) (T2_2_term (gcons a2 b2 0 zero))). apply Hrec. simpl;simpl in Hsize;lia. auto with T2. auto with T2. constructor;auto with T2. } assert (rpo (T2_2_term c1) (Term ord_psi (T2_2_term a1 :: T2_2_term b1 :: nil))). { change (rpo (T2_2_term c1) (T2_2_term (gcons a1 b1 0 zero))). apply Hrec. simpl;simpl in Hsize;lia. inversion_clear nf1. auto with T2. apply psi_lt_head;auto with T2. auto with T2. constructor;auto with T2. } case (cons_rw a1 b1 n1 c1). intros (H'2,(H'3,H'4)). rewrite H'2;rewrite H'3. case (cons_rw a2 b2 n2 c2). intros (H'5,(H'6,H'7)). rewrite H'5;rewrite H'6. simpl. apply rpo_2_2;auto with T2. intro H'6;rewrite H'6. simpl. apply rpo_2_4 ; auto with T2. intro H'6;rewrite H'6. case (cons_rw a2 b2 n2 c2). intros (H''5,(H''6,H''7)). rewrite H''7. apply rpo_2_3;auto with T2. intro H'7;rewrite H'7. apply rpo_2_1;auto with T2. - subst a2. assert (rpo (T2_2_term b1) (T2_2_term b2)). { apply Hrec. simpl in Hsize;lia. auto with T2. auto with T2. eauto using nf_b. } assert (rpo (T2_2_term c1) (Term ord_psi (T2_2_term a1 :: T2_2_term b1 :: nil))). { change (rpo (T2_2_term c1) (T2_2_term (gcons a1 b1 0 zero))). apply Hrec. simpl;simpl in Hsize;lia. inversion_clear nf1. auto with T2. apply psi_lt_head;auto with T2. auto with T2. constructor;auto with T2. } case (cons_rw a1 b1 n1 c1). intros (H'2,(H'3,H'4)). rewrite H'4. case (cons_rw a1 b2 n2 c2). intros (H'5,(H'6,H'7)). rewrite H'7. apply rpo_3_2;auto with T2. intro H'6;rewrite H'6. apply rpo_3_4 ; auto with T2. intro H'6;rewrite H'6. case (cons_rw a1 b2 n2 c2). intros (H''5,(H''6,H''7)). rewrite H''7. apply rpo_3_3;auto with T2. intro H'7;rewrite H'7. apply rpo_3_1;auto with T2. - assert (rpo (Term ord_psi ((T2_2_term a1):: (T2_2_term b1) ::nil)) (T2_2_term b2)). { change (rpo (T2_2_term (gcons a1 b1 0 zero)) (T2_2_term b2)). apply Hrec. simpl in Hsize. simpl;lia. auto with T2. auto with T2. auto with T2. } assert (rpo (T2_2_term c1) (Term ord_psi (T2_2_term a1 :: T2_2_term b1 :: nil))). { change (rpo (T2_2_term c1) (T2_2_term (gcons a1 b1 0 zero))). apply Hrec. simpl;simpl in Hsize;lia. inversion_clear nf1. auto with T2. apply psi_lt_head;auto with T2. auto with T2. constructor;auto with T2. } case (cons_rw a1 b1 n1 c1). intros (H'2,(H'3,H'4)). rewrite H'4. case (cons_rw a2 b2 n2 c2). intros (H'5,(H'6,H'7)). rewrite H'7. apply rpo_4_2;auto with T2. intro H'6;rewrite H'6. apply rpo_4_4 ; auto with T2. intro H'6;rewrite H'6. case (cons_rw a2 b2 n2 c2). intros (H''5,(H''6,H''7)). rewrite H''7. apply rpo_4_3;auto with T2. intro H'7;rewrite H'7. apply rpo_4_1;auto with T2. - assert (rpo (T2_2_term c1) (Term ord_psi ((T2_2_term a1)::(T2_2_term b1)::nil))). { change (rpo (T2_2_term c1) (T2_2_term (gcons a1 b1 0 zero))). apply Hrec. simpl;simpl in Hsize;lia. inversion_clear nf1;auto with T2. apply psi_lt_head;auto with T2. auto with T2. constructor;auto with T2. } case (cons_rw a1 b1 n1 c1). intros (H'2,(H'3,H'4)). rewrite H'4. case (cons_rw a2 (gcons a1 b1 0 zero) n2 c2). intros (H''5,(H''6,H''7)). rewrite H''7. simpl;apply rpo_5_2;auto with T2. intro H'7;rewrite H'7. simpl;apply rpo_5_4. intro H'7;rewrite H'7. case (cons_rw a2 (gcons a1 b1 0 zero) n2 c2). intros (H''5,(H''6,H''7)). rewrite H''7. simpl;apply rpo_5_3. auto with T2. intro H''7;rewrite H''7. simpl;apply rpo_5_1. auto with T2. - subst a2. subst b2. assert (rpo (T2_2_term c1) (Term ord_psi ((T2_2_term a1):: (T2_2_term b1) ::nil))). { change (rpo (T2_2_term c1) (T2_2_term (gcons a1 b1 0 zero))). apply Hrec. simpl; simpl in Hsize;lia. inversion nf1;auto with T2. apply psi_lt_head;auto with T2. auto with T2. constructor;auto with T2. } case (cons_rw a1 b1 n1 c1). intros (H'2,(H'3,H'4)). rewrite H'4. case (cons_rw a1 b1 n2 c2). intros (H''2,(H''3,H''4)). rewrite H''2 in H1. inversion H1. intro H'7;rewrite H'7. apply rpo_6_4. rewrite H'2 in H1;auto with T2. intro H'7;rewrite H'7. case (cons_rw a1 b1 n2 c2). intros (H''2,(H''3,H''4)). rewrite H''2 in H1. inversion H1. intro H''7;rewrite H''7. apply rpo_6_1. auto with T2. auto with T2. - assert (rpo (T2_2_term c1) (Term ord_psi ((T2_2_term a1):: (T2_2_term b1) ::nil))). { change (rpo (T2_2_term c1) (T2_2_term (gcons a1 b1 0 zero))). apply Hrec. simpl; simpl in Hsize;lia. inversion nf1;auto with T2. apply psi_lt_head;auto with T2. auto with T2. constructor;auto with T2. } assert (rpo (T2_2_term c1) (T2_2_term c2)). { apply Hrec. simpl; simpl in Hsize;lia. auto with T2. auto with T2. auto with T2. } case (cons_rw a2 b2 n2 c1). + intros (H'2,(H'3,H'4)). rewrite H'4. case (cons_rw a2 b2 n2 c2). * intros (H''2,(H''3,H''4)). rewrite H''3 in H1. inversion H1. * intro H'7;rewrite H'7. eapply Subterm; [| eleft]. left. auto with T2. + intro H'7;rewrite H'7. case (cons_rw a2 b2 n2 c2). * intros (H''2,(H''3,H''4)). rewrite H''3 in H1;inversion H1. * intro H''7;rewrite H''7. apply rpo_7_1. auto with T2. subst a2;subst b2. auto with T2. auto with T2. Qed.
imports: Coq(Arith List Lia Compare_dec Relations Wellfounded RelationClasses) hydras(Epsilon0) hydras(More_Arith Restriction) hydras(ON_Generic) hydras(rpo.term rpo.rpo) hydras(T2) hydras(Compat815)