proposition: Theorem phi_principalR : forall alpha beta, nf alpha -> nf beta -> {gamma:T2 | [alpha, beta] = phi zero gamma}.
proof: Proof. intros alpha beta Valpha Vbeta; case (phi_cases' alpha Vbeta). destruct 1. case s; intros b1 (b2,(H1,(H2,H3))). case (lt_ge_dec zero alpha). intro. exists [alpha, beta]. simpl. rewrite (compare_rw_lt l);auto with T2. intro; assert(alpha = zero). inversion l;auto with T2. lt_clean. subst alpha. subst beta. exists (cons b1 b2 0 (F 1)). simpl. rewrite (compare_rw_lt H2);auto with T2. case (lt_ge_dec zero alpha). exists (phi alpha beta). rewrite phi_spec1;auto with T2. intro;assert (alpha=zero). case l. auto with T2. intro;lt_clean. subst alpha. exists beta. auto with T2. intros (b1,(b2,(n,(H1,(H2,H3))))). subst beta. case (lt_ge_dec zero alpha). intro l. exists [alpha, (cons b1 b2 0 (F (S n)))]. simpl. rewrite (compare_rw_lt l). auto with T2. intro;assert (alpha=zero). case l. auto with T2. intro;lt_clean. subst alpha. exists (cons b1 b2 0 (F (S (S n)))). simpl. rewrite (compare_rw_lt H2). auto with T2. Defined.
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