proposition: Lemma Acc_implies_Acc_strong : forall alpha, Acc LT alpha -> Acc_strong alpha.
proof: Proof. unfold Acc_strong; intros alpha Aalpha. pattern alpha; eapply Acc_ind with (R:= LT);[| assumption]; clear alpha Aalpha; intros alpha Aalpha IHalpha. assert(beta_Acc: forall beta, lt beta (phi0 alpha) -> nf alpha -> nf beta -> Acc LT beta). { intros beta H H' H''; assert (H0 : LT beta (phi0 alpha)). { repeat split;auto; apply lt_a_phi0_b_phi0; auto. } generalize H0; pattern beta; case beta. - intro;apply Acc_zero. - intros t n t0 H1; case H1; destruct 2; case (lt_inv H3). + intro H5;generalize H2;case n. { inversion 1. - intros; apply IHalpha. + split. * apply nf_inv1 in H2. auto. * split;auto. + auto. } intros;apply IHalpha. split;auto. eapply nf_inv1;eauto. auto. + destruct 1. case H5;intros H6 H7; abstract lia. case H5;intros _ (_,H6);destruct (not_lt_zero H6). } induction n. - intros b Hb; assert (H : Acc LT b). { apply beta_Acc. - rewrite <- lt_a_phi0_b_def; eapply lt_a_phi0_b_intro; eauto. - eapply nf_inv1;eauto. - eapply nf_inv2;eauto. } { pattern b;eapply Acc_ind;[|eexact H]. intros; split; intro y; case y. - intro; apply Acc_zero. - intros c n c0 H3; case (LT_cons_0 H3). intro; unfold LT; case H3;auto. intros (e,(e',r)); subst n c; auto. } - { intros b H; generalize H; pattern b; eapply Acc_ind with (R:= LT). - split; intro y;pattern y; case y. intro;apply Acc_zero. intros c n0 c0 H3. case (LT_inv H3). + intro; apply IHalpha;auto. case H3; auto. + intros (e,[i|(e',r')]). assert (disj:n0 = n \/ (n0 < n)%nat). { inversion i;auto with arith. } case disj;intro H4. * subst n c; apply IHn. case H3;auto. * apply Acc_inv with (cons alpha n zero). apply IHn. apply single_nf; auto. subst c; eapply nf_inv1;eauto. subst c; split. case H3; auto. split. auto with T1. apply single_nf;auto. case H3;intros;eapply nf_inv1;eauto. * subst n0 c;apply H1; auto. case H3;auto. - apply beta_Acc. + rewrite <- lt_a_phi0_b_def. eapply lt_a_phi0_b_intro;eauto. + eapply nf_inv1;eauto. + eapply nf_inv2;eauto. } 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)