proposition: Lemma limit_plus_F_ok : forall alpha, is_limit alpha -> forall n, limit_plus_F alpha n (alpha + F n).
proof: Proof. induction alpha. simpl;constructor 1. simpl. inversion 1. intro n1;case n1. simpl. constructor 2;auto. change (limit_plus_F zero 0 (F 0)). constructor 1. simpl. caseEq (compare [alpha1, alpha2] [zero, zero]). intro H7; generalize (compare_eq_rw H7). injection 1;intros;subst alpha1;subst alpha2. subst alpha;subst beta. case H3;intro;lt_clean. intro H7; generalize (compare_lt_rw H7). inversion 1;intros;try lt_clean. simpl. intros. change (limit_plus_F (cons alpha1 alpha2 n zero) (S n2) (cons alpha1 alpha2 n (F (S n2)))). constructor. auto. constructor. destruct n1. simpl. constructor 2. eapply is_limit_ab. eexact H. generalize H2. generalize (nf_c H5). elim alpha3. intros; change ( limit_plus_F zero 0 (F 0));constructor. constructor. eapply is_limit_ab. eexact H10. case (is_limit_cons_inv H9 H10). intros. apply H8. nf_inv. auto. intro;subst t1;change (limit_plus_F zero 0 (F 0));constructor. simpl. caseEq (compare [alpha1, alpha2] [zero, zero]). intro H7;generalize (compare_eq_rw H7);injection 1;intros. subst alpha1;subst alpha2;subst beta;subst alpha. generalize (is_limit_ab H). destruct 1;lt_clean. intro H7;generalize (compare_lt_rw H7);intros. inversion H6;lt_clean. intro. replace (cons zero zero n1 zero) with (F (S n1)). constructor 2. generalize (compare_gt_rw H6);intros. inversion_clear H7;auto with T2. lt_clean. lt_clean. apply IHalpha3. auto. auto. 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