proposition: Theorem Goodstein_thm : forall c , nf c -> forall N0, correct (S (S N0)) c -> {N':nat | (N0,c) -G->* (N',zero)}.
proof: Proof. intros c Hc. pattern c;apply EPSILON0.transfinite_induction. 2:auto. destruct x. intros ; exists N0. constructor 2. intros. pose (c':= goodstein_next_ord N0 (cons x1 n x2) H H1). assert (c' < (cons x1 n x2)). assert ((N0,(cons x1 n x2)) -G-> (S N0, c')). unfold c'; constructor. subst c'. case (Goodstein_decrease _ _ _ _ H2). destruct 1. discriminate H3. auto. assert (nf c'). unfold c'; apply goodstein_next_ord_nf. assert (correct (S (S (S N0))) c'). unfold c'; apply goodstein_next_ord_correct. case (H0 c' H3 H2 (S N0) H4). intros. exists x. constructor 3 with (S N0, c'). constructor 1. unfold c'; constructor. auto. Qed.
imports: More_nat Arith ArithRing EPSILON0 Relations