Commit c704bf4c authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

Goodstein file now speak about Goodstein

parent 6123457f
......@@ -8,13 +8,18 @@ def Nat := eps nat.
0 : Nat.
S : Nat -> Nat.
def 1 := S 0.
def 2 := S 1.
def 3 := S 2.
def 4 := S 3.
bool : type.
def Bool := eps bool.
T : Bool.
F : Bool.
list : type.
def List := esp list.
def List := eps list.
Nil : List.
Cons : Nat -> List -> List.
......@@ -36,18 +41,21 @@ def mult : Nat -> Nat -> Nat.
[m,n] mult (S m) n --> plus n (mult m n).
def expo : Nat -> Nat -> Nat.
[] expo 0 _ --> S 0.
[m,n] expo (S m) n --> mult n (expo m n).
[] expo _ 0 --> S 0.
[m,n] expo m (S n) --> mult m (expo m n).
def pred : Nat -> Nat.
[n] pred (S n) --> n.
def less : Nat -> Nat -> Bool.
[] less 0 0 --> F.
[] less _ 0 --> F.
[] less 0 (S _) --> T.
[m,n] less (S m) (S n) --> less m n.
def eq : Nat -> Nat -> Bool.
[] eq 0 0 --> T.
[] eq 0 (S _) --> F.
[m,n] eq (S m) (S n) --> eq m n.
def leq : Nat -> Nat -> Bool.
[] leq 0 _ --> T.
[] leq (S _) 0 --> F.
[m,n] leq (S m) (S n) --> leq m n.
def quo : Nat -> Nat -> Nat.
def quo_bis : Nat -> Bool -> Nat -> Nat -> Nat.
......@@ -70,8 +78,38 @@ def while_aux : A : type -> Bool -> (eps A -> Bool) -> (eps A -> eps A) -> eps A
[A,test,fct,ctx] while_aux A T test fct ctx --> while A test fct (fct ctx).
[ctx] while_aux _ F _ _ ctx --> ctx.
def hd : List -> Nat.
[x] hd (Cons x _) --> x.
def fst : Couple -> Nat.
[n] fst (Pair n _) --> n.
def snd : Couple -> List.
[l] snd (Pair _ l) --> l.
def findExpo : Nat -> Nat -> Nat.
[k,n] findExpo k (S n) --> while nat (i : Nat =>leq (expo k (S i)) (S n)) S 0.
def raise : Nat -> Nat -> Nat.
def raise_bis : Nat -> Nat -> Bool -> Nat.
[k] raise k 0 --> 0.
[k,n] raise k (S n) --> raise_bis k (S n) (less (S n) k).
[k,n] raise_bis k n T --> n.
[k,n] raise_bis k n F --> plus (mult (expo (S k) (raise k (findExpo k n))) (quo n (expo k (findExpo k n)))) (raise k (remainder n (expo k (findExpo k n)))).
def GoodsteinAll : Nat -> Couple.
[n] GoodsteinAll (S n) --> while couple (ctx : Couple => less 0 (hd (snd ctx)))
(ctx : Couple => Pair (S (fst ctx)) (Cons (pred (raise (fst ctx) (hd (snd ctx)))) (snd ctx)))
(Pair 2 (Cons (S n) Nil)).
def Goodstein : Nat -> Nat -> Nat.
def Goodstein_bis : Nat -> Nat -> Nat -> Nat.
[seed,index] Goodstein seed index --> Goodstein_bis seed index 2.
[seed] Goodstein_bis seed 0 _ --> seed
[seed,remaining,base] Goodstein_bis seed (S remaining) base -->
Goodstein_bis (pred (raise base seed)) remaining (S base).
#SNF GoodsteinAll 3.
#SNF Goodstein 4 2.
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment