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