On Goodstein Sequences

This exercise is linked with the Goodstein sequence starting at 4 in base 2 (G(4,2)). See for instance Kirby and Paris "Independence results for Peano Arithmetic" Journal of Symbolic Logic, 1978, vol 43, pp 725-731.
Consider the following definitions :

Require Import Arith.
Require Import Omega.
Require Import Relations.

Record item :Set := quad {
                    b: nat ; 
                    c2 : nat ; (* coefficient of b^2 *)
                    c1 :nat ; (* coefficient of b *)
                    c0 :nat    (* coefficient of b^0 *) }.


(* relation between two consecutive items of the sequence *)

Inductive R: item -> item ->Prop :=
 exp0 : forall n i j k, R (quad n i j (S k)) (quad  (S n) i j k)
|exp1 : forall n i j , R (quad n i (S j) 0) (quad (S n) i j n)
|exp2 : forall n i  , R (quad n (S i) 0 0)  (quad (S n) i n n).

Definition Rplus := clos_trans _ R.
Definition Rstar := clos_refl_trans _ R.

Definition reachable (q:item) := Rstar (quad 3 2 2 2) q.

Prove a theorem of the form reachable (quad N 0 0 0)

Remark

This exercise can be adapted in C: Which value is printed when the following program terminates (if it terminates) ?
The source

Solution

Look at this file .

Going home