proposition: Lemma L12 : forall a n b c p d , a <> zero -> c <> zero -> alpha = cons a n b -> beta = cons c p d -> P beta.
proof: Proof. unfold P; intros; subst. assert (nf (cons a n b * cons c p d)). { rewrite L05; auto. destruct (T1_eq_dec d zero). + subst; rewrite mult_a_0; apply single_nf. apply plus_nf; eauto with T1. + apply nf_intro. apply plus_nf; eauto with T1. generalize (@IHbeta d); intro H1; destruct H1; auto with T1. apply tail_LT_cons; eauto with T1. eauto with T1. apply lt_a_phi0_b_phi0R. apply lt_le_trans with (cons a n b * phi0 c). { generalize (@IHbeta (phi0 c)); intro H1; unfold P in H1. destruct H1; auto. - destruct p. + apply LT4; eauto with T1. apply not_zero_lt; eauto with T1. + apply LT3; eauto with T1; auto with arith. - eauto with T1. - assert (cons a n b <> zero) by discriminate. specialize (H2 H4 d). rewrite nf_LT_iff in H3. destruct H2. tauto. destruct H5; auto. } rewrite L5; auto. * apply le_refl. } split; auto. intros _ gamma Hgamma; assert (nf gamma) by eauto with T1. rewrite L05; auto. destruct (cases_for_mult H2). - subst; rewrite mult_a_0; apply LT1. rewrite <- L05; auto. - destruct H4. + destruct H4 as [q Hq]; rewrite Hq. rewrite L03; auto. apply LT2; auto. generalize (@IHbeta (FS q)); intros H5. destruct H5; auto. subst; auto. apply nf_FS; auto. rewrite <- L05; auto. apply LT_add; eauto with T1. + destruct H4. destruct H4 as [x [x0 [H4 H5]]]. rewrite H5, L05, mult_a_0. rewrite H5 in Hgamma. destruct (LT_inv Hgamma). * apply LT2. apply single_nf; eauto with T1. apply plus_nf; eauto with T1. rewrite <- L05; auto. apply plus_smono_LT_r; eauto with T1. * destruct H6. subst x. destruct H7. apply LT3. apply single_nf; eauto with T1. apply plus_nf; eauto with T1. rewrite <- L05; auto. auto. destruct H6; subst x0. apply LT4. apply single_nf; auto with T1. apply plus_nf; eauto with T1. rewrite <- L05; auto. assert (nf (cons a n b * d)). { destruct (@IHbeta d); eauto with T1. apply tail_LT_cons; eauto with T1. } apply not_zero_lt; auto. apply L10; eauto with T1. intro; subst; destruct (LT_irrefl H7). * auto. * auto. * destruct H4 as [e [q [f [H6 [H7 H8]]]]]. rewrite H8, L05; auto. rewrite H8 in Hgamma. destruct (LT_inv Hgamma). -- apply LT2. rewrite <- L05; auto. destruct (@IHbeta ( cons e q f)); auto. subst;auto. rewrite <- L05;auto. apply plus_smono_LT_r; eauto with T1. -- destruct H4; subst. destruct H5. ++ apply LT3; auto. rewrite <- L05; auto. destruct (@IHbeta (cons c q f)); auto. rewrite <- L05; auto. ++ destruct H4; subst. apply LT4; auto. rewrite <- L05; auto. destruct (@IHbeta (cons c p f)); auto. rewrite <- L05; auto. destruct (@IHbeta d); eauto with T1. apply tail_LT_cons; auto. assert (cons a n b <> zero) by discriminate. specialize (H8 H9 f H5); auto. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)