proposition: Lemma plus_nf : forall alpha, nf alpha -> forall beta, nf beta -> nf (alpha + beta).
proof: Proof. intros alpha Halpha. pattern alpha. apply transfinite_induction. destruct x. simpl;auto with T2. destruct beta. simpl;auto with T2. intros;simpl. caseEq ( compare (cons x1 x2 0 zero) (cons beta1 beta2 0 zero)). intro;apply nf_intro. nf_inv. nf_inv. generalize ( compare_eq_rw H2). injection 1. intros; subst beta1; subst beta2. inversion_clear H1. auto with T2. apply psi_relevance;auto with T2. nf_inv. auto. intro;apply nf_intro. nf_inv. nf_inv. apply psi_principal. nf_inv. inversion H;auto. apply psi_relevance;auto with T2. apply psi_relevance;unfold psi; apply compare_gt_rw;auto with T2. eapply H0;auto with T2. nf_inv. apply lt_tail;auto with T2. assumption. 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