proposition: Lemma phi_psi : forall beta0 beta n, nf beta -> limit_plus_F beta0 n beta -> phi alpha beta0 = beta0 -> [alpha, beta] = phi alpha (succ beta).
proof: Proof. intros. case (phi_fix _ H1). intros beta1 (beta2,(H2,H3)). assert (beta = (cons beta1 beta2 0 (F n))). Focus 2. subst beta. simpl. subst beta0. generalize H3 H1. case beta1;case beta2. inversion 1. inversion 2. inversion H2. replace (succ (F n)) with (F (S n)). intros;rewrite phi_to_psi_1. auto with T2. auto with T2. induction n;simpl;auto with T2. replace (succ (F n)) with (F (S n)). intros;rewrite phi_to_psi_1. auto with T2. auto with T2. induction n;simpl;auto with T2. subst beta0. inversion H0. inversion H9. auto with T2. inversion H10. auto with T2. inversion H10;auto with T2. 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