proposition: Lemma trans_aux : gcons a1 b1 n1 c1 t2< gcons a3 b3 n3 c3.
proof: Proof. Proof with eauto with T2. inversion H12. - inversion H23. + constructor 2. * apply induc with a2 ... generalize (length_a a1 b1 n1 c1). generalize (length_a a2 b2 n2 c2). generalize (length_a a3 b3 n3 c3). clear induc;lia. * assert (lt (gcons a2 b2 0 zero) (gcons a3 b3 0 zero)) by auto with T2. apply induc with (gcons a2 b2 0 zero) ... generalize (length_b a1 b1 n1 c1). generalize (length_psi a2 b2 n2 c2). generalize (length_psi a3 b3 n3 c3). clear induc; lia. + subst a3; constructor 2 ... apply induc with (gcons a2 b2 0 zero). 2:auto with T2. 2:constructor 3;auto with T2. generalize (length_b a1 b1 n1 c1); generalize (length_psi a2 b2 n2 c2); generalize (length_psi a2 b3 n3 c3); clear induc;lia. + tricho a1 a3 H20. * constructor 2 ... apply induc with (gcons a2 b2 0 zero). 2:auto with T2. generalize (length_b a1 b1 n1 c1); generalize(length_psi a2 b2 n2 c2); generalize (length_psi a3 b3 n3 c3); clear induc;lia. constructor 4 ... * clear H;subst a1; constructor 3. apply induc with (gcons a2 b2 0 zero) ... generalize (length_b a3 b1 n1 c1); generalize (length_b a3 b3 n3 c3); generalize (length_psi a2 b2 n2 c2); clear induc;lia. * constructor 4 ... apply induc with (gcons a2 b2 0 zero) ... generalize (length_psi a1 b1 n1 c1); generalize (length_psi a2 b2 n2 c2); generalize (length_b a3 b3 n3 c3);clear induc;lia. + tricho a1 a3 H20. * constructor 2 ... apply induc with (gcons a2 b2 0 zero) ... subst b3; generalize (length_b a1 b1 n1 c1); generalize (length_psi a2 b2 n2 c2); generalize (length_psi a3 (gcons a2 b2 0 zero) n3 c3); clear induc;lia. * clear H15 H9 H11 H17 H18 ;subst a3; constructor 3 ... * constructor 4 ... + clear H9 H11 H4 H5; subst a3 b3; constructor 2 ... + clear H9 H11 H4 H5; subst a3 b3; constructor 2 ... - clear H H1 H2 H3 H5 H6 H7 beta1 beta2 gamma1 gamma2. inversion H23. + constructor 2 ... apply induc with b2 ... generalize (length_b a1 b1 n1 c1); generalize (length_b a2 b2 n2 c2); generalize (length_psi a3 b3 n3 c3);clear induc;lia. + constructor 3 ... eapply induc with b2 ... generalize (length_b a1 b1 n1 c1); generalize (length_b a2 b2 n2 c2); generalize (length_b a3 b3 n3 c3);clear induc;lia. + constructor 4 ... apply induc with (gcons a2 b2 0 zero) ... pattern a2 at 1;rewrite <- H4. generalize (length_psi a1 b1 n1 c1); generalize (length_psi a2 b2 n2 c2); generalize (length_b a3 b3 n3 c3);clear induc;lia. + clear H;subst a2; constructor 4 ... + rewrite <- H7; constructor 3 ... + rewrite <- H7; constructor 3 ... - inversion H23 ... + assert (H20 :lt (gcons a1 b1 0 zero) (gcons a3 b3 0 zero)). { apply induc with b2 ... generalize (length_psi a1 b1 n1 c1). generalize (length_b a2 b2 n2 c2). generalize (length_psi a3 b3 n3 c3); clear induc; lia. } inversion_clear H20 ... * inversion H21. * inversion H21. + subst a3; constructor 4 ... apply induc with b2 ... generalize (length_psi a1 b1 n1 c1); generalize (length_b a2 b2 n2 c2); generalize (length_b a2 b3 n3 c3);clear induc;lia. + constructor 4 ... apply induc with a2 ... generalize (length_a a1 b1 n1 c1); generalize (length_a a2 b2 n2 c2); generalize (length_a a3 b3 n3 c3);clear induc; lia. apply induc with (gcons a2 b2 0 zero) ... generalize (length_psi a1 b1 n1 c1); generalize (length_psi a2 b2 n2 c2); generalize (length_b a3 b3 n3 c3);clear induc; lia. + constructor 4 ... apply induc with a2 ... generalize (length_a a1 b1 n1 c1); generalize (length_a a2 b2 n2 c2); generalize (length_a a3 b3 n3 c3);clear induc;lia. + clear H9 H11; subst b3; subst a3; constructor 4 ... + clear H9 H11;subst b3;subst a3; constructor 4 ... - subst b2; inversion H23 ... + inversion_clear H17 ... inversion H18. inversion H18. + subst a3; constructor 4 ... + constructor 4 ... apply induc with a2 ... generalize (length_a a1 b1 n1 c1); generalize (length_a a2 (gcons a1 b1 0 zero) n2 c2); generalize (length_a a3 b3 n3 c3);clear induc;lia. apply induc with (gcons a2 (gcons a1 b1 0 zero) 0 zero) ... generalize (length_psi a1 b1 n1 c1); generalize (length_psi a2 (gcons a1 b1 0 zero) n2 c2); generalize (length_b a3 b3 n3 c3) ;clear induc;lia. + constructor 4 . apply induc with a2 ... generalize (length_a a1 b1 n1 c1); generalize (length_a a2 (gcons a1 b1 0 zero) n2 c2); generalize (length_a a3 b3 n3 c3);clear induc;lia. constructor 5;auto with T2. + subst a3. constructor 5. auto with T2. + subst a3. constructor 5;auto with T2. - subst a2; subst b2. inversion H23 ... + subst a3 b3; constructor 6; eauto with T2 arith. + subst b3;subst a3;subst n3 ; constructor 6 ... - clear H H1;subst a1;subst b1 n2. inversion H23 ... constructor 7; apply induc with c2 ... generalize (length_c a2 b2 n1 c1); generalize (length_c a2 b2 n1 c2); generalize (length_c a3 b3 n3 c3);clear induc;lia. 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)