:: The Ackermann Function and Primitive Recursive Functions
:: by Artur Korni{\l}owicz and Karol P\kak
::
:: Received September 6, 2026
:: Copyright (c) 2026 Association of Mizar Users

Lm1: 2 |^ 2 = 2 * 2
by POLYEQ_5:1;

Lm2: 2 |^ 3 = (2 * 2) * 2
by POLYEQ_5:2;

Lm3: 2 |^ 4 = ((2 * 2) * 2) * 2
by POLYEQ_5:3;

Lm4: 2 |^ 16 = ((((((((((((((2 * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2
by NUMBER09:6;

set T1 = 1 -tuples_on NAT;

set T2 = 2 -tuples_on NAT;

theorem Th1: :: ACKERMAN:1

for m, n being Nat holds m |^|^ (n + 1) = m |^ (m |^|^ n)

proof end;

Lm5: now :: thesis: for m being Nat holds
( m |^|^ 1 = m & m |^|^ 2 = m |^ m & m |^|^ 3 = m |^ (m |^ m) & m |^|^ 4 = m |^ (m |^ (m |^ m)) & m |^|^ 5 = m |^ (m |^ (m |^ (m |^ m))) )

let m be Nat; :: thesis: ( m |^|^ 1 = m & m |^|^ 2 = m |^ m & m |^|^ 3 = m |^ (m |^ m) & m |^|^ 4 = m |^ (m |^ (m |^ m)) & m |^|^ 5 = m |^ (m |^ (m |^ (m |^ m))) )
A1: m |^|^ 0 = 1 by ORDINAL5:13;
A2: m |^|^ (0 + 1) = m |^ (m |^|^ 0) by Th1;
A3: m |^|^ (1 + 1) = m |^ (m |^|^ 1) by Th1;
A4: m |^|^ (2 + 1) = m |^ (m |^|^ 2) by Th1;
A5: m |^|^ (3 + 1) = m |^ (m |^|^ 3) by Th1;
A6: m |^|^ (4 + 1) = m |^ (m |^|^ 4) by Th1;
thus m |^|^ 1 = m by A1, A2; :: thesis: ( m |^|^ 2 = m |^ m & m |^|^ 3 = m |^ (m |^ m) & m |^|^ 4 = m |^ (m |^ (m |^ m)) & m |^|^ 5 = m |^ (m |^ (m |^ (m |^ m))) )
thus m |^|^ 2 = m |^ m by A1, A2, A3; :: thesis: ( m |^|^ 3 = m |^ (m |^ m) & m |^|^ 4 = m |^ (m |^ (m |^ m)) & m |^|^ 5 = m |^ (m |^ (m |^ (m |^ m))) )
thus m |^|^ 3 = m |^ (m |^ m) by A1, A2, A3, A4; :: thesis: ( m |^|^ 4 = m |^ (m |^ (m |^ m)) & m |^|^ 5 = m |^ (m |^ (m |^ (m |^ m))) )
thus m |^|^ 4 = m |^ (m |^ (m |^ m)) by A1, A2, A3, A4, A5; :: thesis: m |^|^ 5 = m |^ (m |^ (m |^ (m |^ m)))
thus m |^|^ 5 = m |^ (m |^ (m |^ (m |^ m))) by A1, A2, A3, A4, A5, A6; :: thesis: verum

end;

registration

let m be Nat;

reduce m |^|^ 1 to m;

reducibility
m |^|^ 1 = m by Lm5;

end;

theorem :: ACKERMAN:2

for m being Nat holds m |^|^ 2 = m |^ m by Lm5;

theorem Th3: :: ACKERMAN:3

for m being Nat holds m |^|^ 3 = m |^ (m |^ m) by Lm5;

theorem Th4: :: ACKERMAN:4

for m being Nat holds m |^|^ 4 = m |^ (m |^ (m |^ m)) by Lm5;

theorem Th5: :: ACKERMAN:5

for m being Nat holds m |^|^ 5 = m |^ (m |^ (m |^ (m |^ m))) by Lm5;

definition

func AckermannFunction -> BinOp of NAT means :Def1: :: ACKERMAN:def 1
for m, n being Nat holds
( it . (0,n) = n + 1 & ( m > 0 implies it . (m,0) = it . ((m - 1),1) ) & ( m > 0 & n > 0 implies it . (m,n) = it . ((m - 1),(it . (m,(n - 1)))) ) );

existence
ex b₁ being BinOp of NAT st
for m, n being Nat holds
( b₁ . (0,n) = n + 1 & ( m > 0 implies b₁ . (m,0) = b₁ . ((m - 1),1) ) & ( m > 0 & n > 0 implies b₁ . (m,n) = b₁ . ((m - 1),(b₁ . (m,(n - 1)))) ) )

proof end;

uniqueness
for b₁, b₂ being BinOp of NAT st ( for m, n being Nat holds
( b₁ . (0,n) = n + 1 & ( m > 0 implies b₁ . (m,0) = b₁ . ((m - 1),1) ) & ( m > 0 & n > 0 implies b₁ . (m,n) = b₁ . ((m - 1),(b₁ . (m,(n - 1)))) ) ) ) & ( for m, n being Nat holds
( b₂ . (0,n) = n + 1 & ( m > 0 implies b₂ . (m,0) = b₂ . ((m - 1),1) ) & ( m > 0 & n > 0 implies b₂ . (m,n) = b₂ . ((m - 1),(b₂ . (m,(n - 1)))) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines AckermannFunction ACKERMAN:def 1 :
for b₁ being BinOp of NAT holds
( b₁ = AckermannFunction iff for m, n being Nat holds
( b₁ . (0,n) = n + 1 & ( m > 0 implies b₁ . (m,0) = b₁ . ((m - 1),1) ) & ( m > 0 & n > 0 implies b₁ . (m,n) = b₁ . ((m - 1),(b₁ . (m,(n - 1)))) ) ) );

set AF = AckermannFunction ;

definition

let m, n be Nat;

func Ackermann (m,n) -> Element of NAT equals :: ACKERMAN:def 2
AckermannFunction . (m,n);

coherence
AckermannFunction . (m,n) is Element of NAT

proof end;

end;

:: deftheorem defines Ackermann ACKERMAN:def 2 :
for m, n being Nat holds Ackermann (m,n) = AckermannFunction . (m,n);

deffunc H₁( Nat, Nat) -> Element of NAT = Ackermann ($1,$2);

theorem Th6: :: ACKERMAN:6

for m being Nat holds Ackermann ((m + 1),0) = Ackermann (m,1)

proof end;

theorem Th7: :: ACKERMAN:7

for m, n being Nat holds Ackermann ((m + 1),(n + 1)) = Ackermann (m,(Ackermann ((m + 1),n)))

proof end;

theorem :: ACKERMAN:8

for n being Nat holds Ackermann (0,n) = n + 1 by Def1;

theorem Th9: :: ACKERMAN:9

for n being Nat holds Ackermann (1,n) = n + 2

proof end;

theorem Th10: :: ACKERMAN:10

for n being Nat holds Ackermann (2,n) = (2 * n) + 3

proof end;

theorem Th11: :: ACKERMAN:11

for n being Nat holds Ackermann (3,n) = (2 |^ (n + 3)) - 3

proof end;

theorem Th12: :: ACKERMAN:12

for n being Nat holds Ackermann (4,n) = (2 |^|^ (n + 3)) - 3

proof end;

theorem :: ACKERMAN:13

Ackermann (4,0) = 13

proof end;

theorem :: ACKERMAN:14

Ackermann (4,1) = 65533

proof end;

theorem :: ACKERMAN:15

Ackermann (4,2) = (2 |^ 65536) - 3

proof end;

theorem Th16: :: ACKERMAN:16

for m, n being Nat holds n < Ackermann (m,n)

proof end;

theorem Th17: :: ACKERMAN:17

for m, n being Nat holds Ackermann (m,n) < Ackermann (m,(n + 1))

proof end;

theorem Th18: :: ACKERMAN:18

for a, b, m being Nat st a < b holds
Ackermann (m,a) < Ackermann (m,b)

proof end;

theorem Th19: :: ACKERMAN:19

for a, b, m being Nat st a <= b holds
Ackermann (m,a) <= Ackermann (m,b)

proof end;

theorem Th20: :: ACKERMAN:20

for m, n being Nat holds m < Ackermann (m,n)

proof end;

theorem Th21: :: ACKERMAN:21

for m, n being Nat holds Ackermann (m,(n + 1)) <= Ackermann ((m + 1),n)

proof end;

theorem Th22: :: ACKERMAN:22

for m, n being Nat holds Ackermann (m,n) < Ackermann ((m + 1),n)

proof end;

theorem Th23: :: ACKERMAN:23

for a, b, n being Nat st a < b holds
Ackermann (a,n) < Ackermann (b,n)

proof end;

theorem Th24: :: ACKERMAN:24

for a, b, n being Nat st a <= b holds
Ackermann (a,n) <= Ackermann (b,n)

proof end;

theorem Th25: :: ACKERMAN:25

for k, m, n being Nat holds Ackermann (k,(Ackermann (m,n))) < Ackermann (((k + m) + 2),n)

proof end;

theorem :: ACKERMAN:26

for r, s, y being Nat holds (Ackermann (r,y)) + (Ackermann (s,y)) < Ackermann ((4 + (max (r,s))),y)

proof end;

theorem Th27: :: ACKERMAN:27

for r, n being Nat holds Ackermann (r,(n + n)) < Ackermann ((r + 4),n)

proof end;

registration

let m, n be Nat;

cluster Ackermann (m,n) -> non zero ;

coherence
not Ackermann (m,n) is zero by Th16;

end;

definition

let m be Nat;

func AckermannFunction m -> UnOp of NAT means :Def3: :: ACKERMAN:def 3
for n being Nat holds it . n = Ackermann (m,n);

existence
ex b₁ being UnOp of NAT st
for n being Nat holds b₁ . n = Ackermann (m,n)

proof end;

uniqueness
for b₁, b₂ being UnOp of NAT st ( for n being Nat holds b₁ . n = Ackermann (m,n) ) & ( for n being Nat holds b₂ . n = Ackermann (m,n) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines AckermannFunction ACKERMAN:def 3 :
for m being Nat
for b₂ being UnOp of NAT holds
( b₂ = AckermannFunction m iff for n being Nat holds b₂ . n = Ackermann (m,n) );

deffunc H₂( Nat) -> UnOp of NAT = AckermannFunction $1;

registration

let m be Nat;

cluster AckermannFunction m -> positive-yielding ;

coherence
AckermannFunction m is positive-yielding

proof end;

end;

registration

let m be Nat;

cluster AckermannFunction m -> increasing ;

coherence
AckermannFunction m is increasing

proof end;

end;

theorem :: ACKERMAN:28

for m being Nat holds (AckermannFunction (m + 1)) . 0 = (AckermannFunction m) . 1

proof end;

theorem :: ACKERMAN:29

for m, n being Nat holds (AckermannFunction (m + 1)) . (n + 1) = (AckermannFunction m) . ((AckermannFunction (m + 1)) . n)

proof end;

definition

let f be Function;

func dom2tuple f -> Function means :Def4: :: ACKERMAN:def 4
( dom it = 1 -tuples_on (dom f) & ( for x being object st x in dom f holds
it . <*x*> = f . x ) ) if not f is empty
otherwise it = {} ;

existence
( ( not f is empty implies ex b₁ being Function st
( dom b₁ = 1 -tuples_on (dom f) & ( for x being object st x in dom f holds
b₁ . <*x*> = f . x ) ) ) & ( f is empty implies ex b₁ being Function st b₁ = {} ) )

proof end;

uniqueness
for b₁, b₂ being Function holds
( ( not f is empty & dom b₁ = 1 -tuples_on (dom f) & ( for x being object st x in dom f holds
b₁ . <*x*> = f . x ) & dom b₂ = 1 -tuples_on (dom f) & ( for x being object st x in dom f holds
b₂ . <*x*> = f . x ) implies b₁ = b₂ ) & ( f is empty & b₁ = {} & b₂ = {} implies b₁ = b₂ ) )

proof end;

consistency
for b₁ being Function holds verum ;

end;

:: deftheorem Def4 defines dom2tuple ACKERMAN:def 4 :
for f, b₂ being Function holds
( ( not f is empty implies ( b₂ = dom2tuple f iff ( dom b₂ = 1 -tuples_on (dom f) & ( for x being object st x in dom f holds
b₂ . <*x*> = f . x ) ) ) ) & ( f is empty implies ( b₂ = dom2tuple f iff b₂ = {} ) ) );

deffunc H₃( Function) -> Function = dom2tuple $1;

registration

let f be empty Function;

cluster dom2tuple f -> empty ;

coherence
dom2tuple f is empty by Def4;

end;

registration

let f be non empty Function;

cluster dom2tuple f -> non empty ;

coherence
not dom2tuple f is empty

proof end;

end;

registration

let D be set ;
let f be D -defined Function;

cluster dom2tuple f -> D * -defined ;

coherence
dom2tuple f is D * -defined

proof end;

end;

registration

let D be set ;
let f be D -valued Function;

cluster dom2tuple f -> D -valued ;

coherence
dom2tuple f is D -valued

proof end;

end;

registration

let D be non empty set ;
let f be D -defined Function;

cluster dom2tuple f -> homogeneous ;

coherence
dom2tuple f is homogeneous

proof end;

end;

theorem Th30: :: ACKERMAN:30

for D being set
for f being UnOp of D holds dom2tuple f is PartFunc of (D *),D

proof end;

registration

let D be non empty set ;
let f be UnOp of D;

cluster dom2tuple f -> 1 -ary ;

coherence
dom2tuple f is 1 -ary

proof end;

end;

definition

let D be set ;
let f be BinOp of D;

func dom2tuple f -> Function means :Def5: :: ACKERMAN:def 5
( dom it = 2 -tuples_on D & ( for x, y being object st [x,y] in dom f holds
it . <*x,y*> = f . (x,y) ) ) if not D is empty
otherwise it = {} ;

existence
( ( not D is empty implies ex b₁ being Function st
( dom b₁ = 2 -tuples_on D & ( for x, y being object st [x,y] in dom f holds
b₁ . <*x,y*> = f . (x,y) ) ) ) & ( D is empty implies ex b₁ being Function st b₁ = {} ) )

proof end;

uniqueness
for b₁, b₂ being Function holds
( ( not D is empty & dom b₁ = 2 -tuples_on D & ( for x, y being object st [x,y] in dom f holds
b₁ . <*x,y*> = f . (x,y) ) & dom b₂ = 2 -tuples_on D & ( for x, y being object st [x,y] in dom f holds
b₂ . <*x,y*> = f . (x,y) ) implies b₁ = b₂ ) & ( D is empty & b₁ = {} & b₂ = {} implies b₁ = b₂ ) )

proof end;

consistency
for b₁ being Function holds verum ;

end;

:: deftheorem Def5 defines dom2tuple ACKERMAN:def 5 :
for D being set
for f being BinOp of D
for b₃ being Function holds
( ( not D is empty implies ( b₃ = dom2tuple f iff ( dom b₃ = 2 -tuples_on D & ( for x, y being object st [x,y] in dom f holds
b₃ . <*x,y*> = f . (x,y) ) ) ) ) & ( D is empty implies ( b₃ = dom2tuple f iff b₃ = {} ) ) );

registration

let f be BinOp of NAT;

cluster dom2tuple f -> NAT * -defined ;

coherence
dom2tuple f is NAT * -defined

proof end;

end;

registration

let D be set ;
let f be BinOp of D;

cluster dom2tuple f -> D -valued ;

coherence
dom2tuple f is D -valued

proof end;

end;

theorem Th31: :: ACKERMAN:31

for D being set
for f being BinOp of D holds dom2tuple f is PartFunc of (D *),D

proof end;

registration

let D be non empty set ;
let f be BinOp of D;

cluster dom2tuple f -> homogeneous ;

coherence
dom2tuple f is homogeneous

proof end;

end;

registration

let D be non empty set ;
let f be BinOp of D;

cluster dom2tuple f -> 2 -ary ;

coherence
dom2tuple f is 2 -ary

proof end;

end;

theorem :: ACKERMAN:32

dom2tuple AckermannFunction in HFuncs NAT

proof end;

Lm6: <*0*> in 1 -tuples_on NAT
by FINSEQ_2:98;

0 -tuples_on NAT = {{}}
by COMPUT_1:5;

then Lm7: {} in 0 -tuples_on NAT
by TARSKI:def 1;

definition

let f be Function-yielding ManySortedSet of NAT ;

attr f is homogeneous means :Def6: :: ACKERMAN:def 6
for n being Nat holds f . n is homogeneous ;

attr f is to-naturals means :Def7: :: ACKERMAN:def 7
for n being Nat holds f . n is to-naturals ;

attr f is primitive-recursive means :Def8: :: ACKERMAN:def 8
for n being Nat holds f . n is primitive-recursive ;

end;

:: deftheorem Def6 defines homogeneous ACKERMAN:def 6 :
for f being Function-yielding ManySortedSet of NAT holds
( f is homogeneous iff for n being Nat holds f . n is homogeneous );

:: deftheorem Def7 defines to-naturals ACKERMAN:def 7 :
for f being Function-yielding ManySortedSet of NAT holds
( f is to-naturals iff for n being Nat holds f . n is to-naturals );

:: deftheorem Def8 defines primitive-recursive ACKERMAN:def 8 :
for f being Function-yielding ManySortedSet of NAT holds
( f is primitive-recursive iff for n being Nat holds f . n is primitive-recursive );

definition

let D be set ;
let f be Function-yielding ManySortedSet of NAT ;

attr f is D -defined means :Def9: :: ACKERMAN:def 9
for n being Nat holds f . n is D -defined ;

end;

:: deftheorem Def9 defines -defined ACKERMAN:def 9 :
for D being set
for f being Function-yielding ManySortedSet of NAT holds
( f is D -defined iff for n being Nat holds f . n is D -defined );

definition

let f be Function-yielding ManySortedSet of NAT ;

attr f is satisfying_primrec_conditions means :: ACKERMAN:def 10
( f is homogeneous & f is to-naturals & f is NAT * -defined );

end;

:: deftheorem defines satisfying_primrec_conditions ACKERMAN:def 10 :
for f being Function-yielding ManySortedSet of NAT holds
( f is satisfying_primrec_conditions iff ( f is homogeneous & f is to-naturals & f is NAT * -defined ) );

registration

let f be homogeneous Function;

cluster NAT --> f -> homogeneous ;

coherence
NAT --> f is homogeneous by FUNCOP_1:7, ORDINAL1:def 12;

end;

registration

let f be to-naturals Function;

cluster NAT --> f -> to-naturals ;

coherence
NAT --> f is to-naturals by FUNCOP_1:7, ORDINAL1:def 12;

end;

registration

let f be primitive-recursive Function;

cluster NAT --> f -> primitive-recursive ;

coherence
NAT --> f is primitive-recursive by FUNCOP_1:7, ORDINAL1:def 12;

end;

registration

let D be set ;
let f be D -defined Function;

cluster NAT --> f -> D -defined ;

coherence
NAT --> f is D -defined by FUNCOP_1:7, ORDINAL1:def 12;

end;

registration

cluster non empty Relation-like NAT -defined Function-like total Function-yielding Relation-yielding satisfying_primrec_conditions for set ;

existence
ex b₁ being Function-yielding ManySortedSet of NAT st b₁ is satisfying_primrec_conditions

proof end;

end;

registration

cluster Relation-like NAT -defined Function-like total Function-yielding satisfying_primrec_conditions -> Function-yielding homogeneous to-naturals NAT * -defined for set ;

coherence
for b₁ being Function-yielding ManySortedSet of NAT st b₁ is satisfying_primrec_conditions holds
( b₁ is homogeneous & b₁ is to-naturals & b₁ is NAT * -defined ) ;

cluster Relation-like NAT -defined Function-like total Function-yielding homogeneous to-naturals NAT * -defined -> Function-yielding satisfying_primrec_conditions for set ;

coherence
for b₁ being Function-yielding ManySortedSet of NAT st b₁ is homogeneous & b₁ is to-naturals & b₁ is NAT * -defined holds
b₁ is satisfying_primrec_conditions ;

end;

registration

let f be Function-yielding homogeneous ManySortedSet of NAT ;
let n be Nat;

cluster f . n -> homogeneous ;

coherence
f . n is homogeneous by Def6;

end;

registration

let f be Function-yielding to-naturals ManySortedSet of NAT ;
let n be Nat;

cluster f . n -> to-naturals ;

coherence
f . n is to-naturals by Def7;

end;

registration

cluster non empty Relation-like NAT -defined Function-like total Function-yielding Relation-yielding primitive-recursive for set ;

existence
ex b₁ being Function-yielding ManySortedSet of NAT st b₁ is primitive-recursive

proof end;

end;

registration

let f be Function-yielding primitive-recursive ManySortedSet of NAT ;
let n be Nat;

cluster f . n -> primitive-recursive ;

coherence
f . n is primitive-recursive by Def8;

end;

registration

let D be set ;

cluster non empty Relation-like NAT -defined Function-like total Function-yielding Relation-yielding D -defined for set ;

existence
ex b₁ being Function-yielding ManySortedSet of NAT st b₁ is D -defined

proof end;

end;

registration

let D be set ;
let f be Function-yielding D -defined ManySortedSet of NAT ;
let n be Nat;

cluster f . n -> D -defined ;

coherence
f . n is D -defined by Def9;

end;

definition

let k be Nat;
let f be Function-yielding homogeneous ManySortedSet of NAT ;

attr f is k -ary means :Def11: :: ACKERMAN:def 11
for n being Nat holds f . n is k -ary ;

end;

:: deftheorem Def11 defines -ary ACKERMAN:def 11 :
for k being Nat
for f being Function-yielding homogeneous ManySortedSet of NAT holds
( f is k -ary iff for n being Nat holds f . n is k -ary );

registration

let k be non zero Nat;

cluster non empty Relation-like NAT -defined Function-like total Function-yielding Relation-yielding homogeneous to-naturals primitive-recursive NAT * -defined k -ary for set ;

existence
ex b₁ being Function-yielding homogeneous ManySortedSet of NAT st
( b₁ is k -ary & b₁ is primitive-recursive & b₁ is to-naturals & b₁ is NAT * -defined )

proof end;

end;

registration

let k be non zero Nat;
let f be Function-yielding homogeneous k -ary ManySortedSet of NAT ;
let n be Nat;

cluster f . n -> k -ary ;

coherence
f . n is k -ary by Def11;

end;

definition

let k be Nat;

func k -aryPrimRecFuncs -> Subset of (HFuncs NAT) equals :: ACKERMAN:def 12
{ f where f is Element of HFuncs NAT : ( f is k -ary & f is primitive-recursive ) } ;

coherence
{ f where f is Element of HFuncs NAT : ( f is k -ary & f is primitive-recursive ) } is Subset of (HFuncs NAT)

proof end;

end;

:: deftheorem defines -aryPrimRecFuncs ACKERMAN:def 12 :
for k being Nat holds k -aryPrimRecFuncs = { f where f is Element of HFuncs NAT : ( f is k -ary & f is primitive-recursive ) } ;

theorem Th33: :: ACKERMAN:33

for k, n being Nat holds k const n in k -aryPrimRecFuncs

proof end;

registration

let k be Nat;

cluster k -aryPrimRecFuncs -> non empty ;

coherence
not k -aryPrimRecFuncs is empty by Th33;

end;

theorem Th34: :: ACKERMAN:34

for k, n being Nat st 1 <= n & n <= k holds
k succ n in k -aryPrimRecFuncs

proof end;

definition

func AckermannSequence -> Function-yielding primitive-recursive satisfying_primrec_conditions 1 -ary ManySortedSet of NAT means :Def13: :: ACKERMAN:def 13
( it . 0 = 1 succ 1 & ( for m being Nat holds it . (m + 1) = primrec ((0 const (Ackermann (m,1))),((it . m) * <:<*(2 proj 2)*>:>),1) ) );

existence
ex b₁ being Function-yielding primitive-recursive satisfying_primrec_conditions 1 -ary ManySortedSet of NAT st
( b₁ . 0 = 1 succ 1 & ( for m being Nat holds b₁ . (m + 1) = primrec ((0 const (Ackermann (m,1))),((b₁ . m) * <:<*(2 proj 2)*>:>),1) ) )

proof end;

uniqueness
for b₁, b₂ being Function-yielding primitive-recursive satisfying_primrec_conditions 1 -ary ManySortedSet of NAT st b₁ . 0 = 1 succ 1 & ( for m being Nat holds b₁ . (m + 1) = primrec ((0 const (Ackermann (m,1))),((b₁ . m) * <:<*(2 proj 2)*>:>),1) ) & b₂ . 0 = 1 succ 1 & ( for m being Nat holds b₂ . (m + 1) = primrec ((0 const (Ackermann (m,1))),((b₂ . m) * <:<*(2 proj 2)*>:>),1) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def13 defines AckermannSequence ACKERMAN:def 13 :
for b₁ being Function-yielding primitive-recursive satisfying_primrec_conditions 1 -ary ManySortedSet of NAT holds
( b₁ = AckermannSequence iff ( b₁ . 0 = 1 succ 1 & ( for m being Nat holds b₁ . (m + 1) = primrec ((0 const (Ackermann (m,1))),((b₁ . m) * <:<*(2 proj 2)*>:>),1) ) ) );

set AS = AckermannSequence ;

registration

cluster AckermannSequence -> HFuncs NAT -valued Function-yielding primitive-recursive satisfying_primrec_conditions 1 -ary ;

coherence
AckermannSequence is HFuncs NAT -valued

proof end;

end;

theorem Th35: :: ACKERMAN:35

for m being Nat holds arity ((AckermannSequence . m) * <:<*(2 proj 2)*>:>) = 2

proof end;

theorem Th36: :: ACKERMAN:36

for m, n being Nat holds (AckermannSequence . m) . <*n*> = Ackermann (m,n)

proof end;

theorem Th37: :: ACKERMAN:37

dom2tuple (AckermannFunction 0) = 1 succ 1

proof end;

theorem Th38: :: ACKERMAN:38

for m being Nat holds dom2tuple (AckermannFunction (m + 1)) = primrec ((0 const (Ackermann (m,1))),((AckermannSequence . m) * <:<*(2 proj 2)*>:>),1)

proof end;

theorem Th39: :: ACKERMAN:39

for m being Nat holds dom2tuple (AckermannFunction m) = AckermannSequence . m

proof end;

registration

let m be Nat;

cluster dom2tuple (AckermannFunction m) -> primitive-recursive ;

coherence
dom2tuple (AckermannFunction m) is primitive-recursive

proof end;

end;

registration

let k be Nat;

cluster Relation-like NAT * -defined omega -valued Function-like complex-valued ext-real-valued real-valued rational-valued integer-valued to-naturals homogeneous k -ary for set ;

existence
ex b₁ being NAT * -defined to-naturals homogeneous Function st b₁ is k -ary

proof end;

end;

definition

let f be BinOp of NAT;
let g be to-naturals Function;

pred f majorizes g means :: ACKERMAN:def 14
ex N being Element of NAT st
for F being non empty FinSequence of NAT st F in dom g holds
for a being Element of NAT st a = max (rng F) holds
g . F < f . (N,a);

end;

:: deftheorem defines majorizes ACKERMAN:def 14 :
for f being BinOp of NAT
for g being to-naturals Function holds
( f majorizes g iff ex N being Element of NAT st
for F being non empty FinSequence of NAT st F in dom g holds
for a being Element of NAT st a = max (rng F) holds
g . F < f . (N,a) );

theorem Th40: :: ACKERMAN:40

for f being BinOp of NAT holds not f majorizes dom2tuple f

proof end;

definition

let f be BinOp of NAT;

func majorizedBy f -> Subset of (HFuncs NAT) equals :: ACKERMAN:def 15
{ g where g is NAT * -defined to-naturals homogeneous Function : f majorizes g } ;

coherence
{ g where g is NAT * -defined to-naturals homogeneous Function : f majorizes g } is Subset of (HFuncs NAT)

proof end;

end;

:: deftheorem defines majorizedBy ACKERMAN:def 15 :
for f being BinOp of NAT holds majorizedBy f = { g where g is NAT * -defined to-naturals homogeneous Function : f majorizes g } ;

theorem Th41: :: ACKERMAN:41

for g being NAT * -defined to-naturals homogeneous Function st arity g = 0 holds
AckermannFunction majorizes g

proof end;

theorem Th42: :: ACKERMAN:42

for G being FinSequence of HFuncs NAT st rng G c= majorizedBy AckermannFunction holds
ex N being Element of NAT st
for g being NAT * -defined to-naturals homogeneous Function st g in rng G holds
for F being non empty FinSequence of NAT st F in dom g holds
for a being Element of NAT st a = max (rng F) holds
g . F < Ackermann (N,a)

proof end;

theorem Th43: :: ACKERMAN:43

for m, n being Nat holds AckermannFunction majorizes m const n

proof end;

theorem Th44: :: ACKERMAN:44

for m, n being Nat holds m const n in majorizedBy AckermannFunction

proof end;

theorem Th45: :: ACKERMAN:45

for m, n1, n2 being Nat st m const n1 = m const n2 holds
n1 = n2

proof end;

theorem :: ACKERMAN:46

for m, n1, n2 being Nat st 1 <= n1 & n1 <= m & 1 <= n2 & n2 <= m & m succ n1 = m succ n2 holds
n1 = n2

proof end;

theorem :: ACKERMAN:47

for m, n1, n2 being Nat st 1 <= n1 & n1 <= m & 1 <= n2 & n2 <= m & m proj n1 = m proj n2 holds
n1 = n2

proof end;

definition

let m be Nat;

func constF m -> Function of NAT,(HFuncs NAT) means :Def16: :: ACKERMAN:def 16
for n being Nat holds it . n = m const n;

existence
ex b₁ being Function of NAT,(HFuncs NAT) st
for n being Nat holds b₁ . n = m const n

proof end;

uniqueness
for b₁, b₂ being Function of NAT,(HFuncs NAT) st ( for n being Nat holds b₁ . n = m const n ) & ( for n being Nat holds b₂ . n = m const n ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def16 defines constF ACKERMAN:def 16 :
for m being Nat
for b₂ being Function of NAT,(HFuncs NAT) holds
( b₂ = constF m iff for n being Nat holds b₂ . n = m const n );

registration

let m be Nat;

cluster constF m -> one-to-one ;

coherence
constF m is one-to-one

proof end;

end;

theorem Th48: :: ACKERMAN:48

for m being Nat holds rng (constF m) c= PrimRec

proof end;

registration

cluster PrimRec -> infinite ;

coherence
not PrimRec is finite

proof end;

end;

theorem Th49: :: ACKERMAN:49

for m, n being Nat st 1 <= n & n <= m holds
AckermannFunction majorizes m succ n

proof end;

theorem Th50: :: ACKERMAN:50

for m, n being Nat st 1 <= n & n <= m holds
m succ n in majorizedBy AckermannFunction

proof end;

theorem Th51: :: ACKERMAN:51

for m, n being Nat st 1 <= n & n <= m holds
AckermannFunction majorizes m proj n

proof end;

theorem Th52: :: ACKERMAN:52

for m, n being Nat st 1 <= n & n <= m holds
m proj n in majorizedBy AckermannFunction

proof end;

registration

cluster majorizedBy AckermannFunction -> composition_closed ;

coherence
majorizedBy AckermannFunction is composition_closed

proof end;

end;

registration

cluster majorizedBy AckermannFunction -> primitive-recursion_closed ;

coherence
majorizedBy AckermannFunction is primitive-recursion_closed

proof end;

end;

registration

cluster majorizedBy AckermannFunction -> primitive-recursively_closed ;

coherence
majorizedBy AckermannFunction is primitive-recursively_closed

proof end;

end;

theorem Th53: :: ACKERMAN:53

PrimRec c= majorizedBy AckermannFunction by COMPUT_1:74;

registration

cluster majorizedBy AckermannFunction -> infinite ;

coherence
not majorizedBy AckermannFunction is finite by Th53;

end;

theorem Th54: :: ACKERMAN:54

not dom2tuple AckermannFunction is primitive-recursive

proof end;

theorem :: ACKERMAN:55

not dom2tuple AckermannFunction in PrimRec by Th54;

theorem :: ACKERMAN:56

for d being UnOp of NAT st ( for n being Nat holds d . n = Ackermann (n,n) ) holds
not dom2tuple d is primitive-recursive

proof end;