proposition: Lemma L2_6_2 (p: nat) : forall alpha, nf alpha -> forall beta, const_pathS p alpha beta -> T1.succ beta t1< alpha -> const_pathS (S p) alpha (T1.succ beta).
proof: Proof. intros alpha ; transfinite_induction alpha. clear alpha ; intros alpha HRecAlpha Halpha . intros;assert (beta t1<= canon alpha (S p))%t1. - apply small_lemma; auto. - destruct (LE_LT_eq_dec H1). + assert (T1.succ beta t1<= canon alpha (S p))%t1. { apply LT_succ_LE;auto. } destruct (LE_LT_eq_dec H2). * specialize (HRecAlpha (canon alpha (S p)) ). assert (canon alpha (S p) t1< alpha)%t1. { apply canonS_LT; auto. intro; subst alpha; destruct (not_LT_zero H0). } apply const_pathS_trans with (canon alpha (S p)). { apply Cor12 with p; auto. left; split. intro H4;subst; destruct (not_LT_zero H0). reflexivity. } { apply HRecAlpha. apply canonS_LT; auto with T1. intro; subst. destruct (not_LT_zero H0). destruct H3;tauto. apply Proposition_2_3a with alpha; trivial. intro H4; subst. destruct (not_LT_zero H0). left. split. intro; subst. destruct (not_LT_zero H0). reflexivity. auto. } * rewrite e; apply Cor12 with p; auto. apply canonS_LT; auto with T1. intro; subst alpha. destruct (not_LT_zero H0). left. split. intro;subst; destruct (not_LT_zero H0). trivial. + clear H1; destruct alpha. { destruct (not_LT_zero H0). } { destruct n. destruct alpha2. nf_decomp Halpha. destruct (@zero_limit_succ_dec alpha1); trivial. destruct s. subst; cbn in H0. destruct (LT_irrefl H0). rename alpha1 into lambda. rewrite canonS_lim1 in e. assert (const_pathS p lambda (canon lambda (S p))). left. split. intro;subst. destruct (@T1limit_not_zero zero); trivial. trivial. assert (const_pathS (S p) lambda (T1.succ (canon lambda (S p)))). { apply HRecAlpha;auto. apply head_LT_cons; eauto with T1. apply succ_lt_limit; auto. apply canonS_LT;auto with T1. } apply const_pathS_trans with (T1.cons (T1.succ (canon lambda (S p))) 0 zero); eauto with T1. apply KS_thm_2_4_lemma5; trivial. auto with T1. apply HRecAlpha; trivial. apply LT2. apply single_nf. apply succ_nf. apply nf_canon. assumption. apply single_nf; eauto with T1. apply succ_lt_limit; auto. apply canonS_LT;auto with T1. apply succ_nf; apply nf_canon; eauto with T1. subst; apply KS_thm_2_4_lemma5; trivial. left; rewrite canon_succ; auto. split. apply succ_not_zero; auto. trivial. apply nf_canon; eauto with T1. apply succ_nf; apply nf_canon; eauto with T1. apply succ_not_zero. rewrite e; apply succ_lt_limit; auto. apply single_nf; trivial. apply succ_nf; apply nf_canon; eauto with T1. simpl; case_eq (T1.succ (canon lambda (S p))). intro; destruct (succ_not_zero (canon lambda (S p))); auto. auto. apply LT2; trivial. apply single_nf; trivial. apply nf_canon; eauto with T1. apply single_nf; trivial. apply succ_nf; apply nf_canon; eauto with T1. apply LT_succ. apply nf_canon; eauto with T1. eauto with T1. auto. { destruct s as [gamma [H1 H2]];destruct (T1_eq_dec gamma zero). { subst gamma alpha1; simpl in e; subst beta; left. split. discriminate. rewrite canonS_phi0_succ_eqn; trivial. } assert ( beta = T1.cons gamma p zero). { rewrite e, H2; now rewrite canonS_phi0_succ_eqn. } apply const_pathS_trans with (T1.cons gamma (S p) zero). { left; rewrite H2; now rewrite canonS_phi0_succ_eqn. } apply HRecAlpha. - subst alpha1; apply LT2. apply single_nf; auto with T1. apply single_nf; trivial. apply LT_succ; auto. - apply single_nf;auto. - rewrite H3. apply KS_thm_2_4_lemma3_0; auto. - apply succ_lt_limit; eauto with T1. cbn; destruct gamma. + now destruct n. + auto. + rewrite H3; apply LT3; auto with arith. } { rewrite canon_tail in e. - subst beta; destruct (T1_eq_dec alpha2_1 zero). { subst alpha2_1; assert (alpha2_2 = zero). { apply nf_inv2 in Halpha; now apply nf_of_finite in Halpha. } subst alpha2_2; simpl canon; destruct n. simpl in H0. destruct alpha1. destruct H0. destruct H1. discriminate H1. destruct (LT_irrefl H0). simpl in H0. destruct alpha1. destruct n. generalize (nf_of_finite Halpha); discriminate. generalize (nf_of_finite Halpha); discriminate. destruct (LT_irrefl H0). } rewrite succ_cons. + apply KS_thm_2_4_lemma1; eauto with T1. discriminate. apply HRecAlpha; trivial. apply LT2; eauto with T1. split; eauto with T1. eapply nf_inv2, Halpha. now left. rewrite succ_cons in H0. apply remove_first_sumand in H0. auto. destruct alpha2_1. destruct n0; auto. { cbn. destruct n, alpha2_2, alpha2_1_1, n1; try discriminate. all: destruct (T1.pred alpha2_1_2); try discriminate. } apply nf_LT_right with (T1.cons alpha2_1 n alpha2_2). eapply Halpha. apply canonS_LT; trivial. eauto with T1. discriminate. + eapply canonS_cons_not_zero; eauto. + eapply nf_LT_right; eauto. apply canonS_LT; trivial. eauto with T1. discriminate. - eauto with T1. - discriminate. } destruct (T1_eq_dec alpha2 zero). { subst alpha2; rewrite canon_SSn_zero in e. destruct (T1_eq_dec alpha1 zero). { subst alpha1; simpl canon in e; subst beta; simpl in H0. destruct (LT_irrefl H0). } rewrite e, succ_cons. apply KS_thm_2_4_lemma1'. eauto with T1. auto. apply HRecAlpha. apply LT3; auto with arith. eauto with T1. now left. apply succ_lt_limit; eauto with T1. cbn; destruct alpha1; auto. apply canonS_LT; trivial. discriminate. apply canonS_cons_not_zero; auto. apply nf_intro. eauto with T1. apply nf_canon; eauto with T1. apply lt_a_phi0_b_phi0R. destruct (@canonS_LT p (T1.cons alpha1 0 zero)). eauto with T1. discriminate. destruct H2;auto. eauto with T1. } rewrite canon_tail in e; auto. rewrite e; simpl succ; destruct alpha1. apply nf_of_finite in Halpha. now destruct n0. apply KS_thm_2_4_lemma1; auto. rewrite e in H0. cbn in H0; apply remove_first_sumand in H0. apply HRecAlpha; auto. apply tail_LT_cons; auto. eauto with T1. now left. } Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)