:: 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
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 4.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/4.0/.
environ
vocabularies NUMBERS, NAT_1, BINOP_1, FUNCT_1, SUBSET_1, ARYTM_3, CARD_1,
XXREAL_0, ACKERMAN, ARYTM_1, ORDINAL1, RELAT_1, NEWTON, ORDINAL5,
ORDINAL2, ORDINAL4, COMPUT_1, ASYMPT_0, UNIALG_1, TARSKI, XBOOLE_0,
FUNCT_2, ZFMISC_1, FUNCOP_1, PARTFUN3, XCMPLX_0, REAL_1, FINSEQ_1,
FINSEQ_2, FINSEQ_3, PARTFUN1, FUNCT_4, PRALG_3, CARD_3, PBOOLE, FINSET_1,
FUNCT_7, FUNCT_6;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0,
RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, XXREAL_0, XXREAL_2,
FINSET_1, CARD_3, XCMPLX_0, NAT_1, CARD_1, BINOP_1, NEWTON, ORDINAL2,
ORDINAL5, FUNCT_6, FUNCT_7, FUNCOP_1, VALUED_0, FINSEQ_1, FINSEQ_2,
FINSEQ_3, PBOOLE, FINSEQ_4, MARGREL1, COMPUT_1, PARTFUN3;
constructors RELSET_1, NEWTON, ORDINAL5, COMPUT_1, PARTFUN3, RECDEF_1,
FINSEQ_3, FINSEQ_4, FUNCT_6, XXREAL_2;
registrations ORDINAL1, RELSET_1, FINSET_1, XREAL_0, NAT_6, NAT_1, NEWTON,
ORDINAL5, COMPUT_1, RELAT_1, VALUED_0, XBOOLE_0, FUNCT_1, FUNCOP_1,
CARD_1, FUNCT_2, FINSEQ_1, FINSEQ_2, PBOOLE, XXREAL_2, FUNCT_7;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, RELAT_1, FUNCT_1, FUNCT_2, SEQM_3, PARTFUN3, COMPUT_1;
equalities ORDINAL1, COMPUT_1;
expansions BINOP_1;
theorems ORDINAL1, XXREAL_0, NEWTON, POLYEQ_5, NUMBER09, ORDINAL5, NAT_1,
ZFMISC_1, COMPUT_1, FUNCT_2, FUNCT_1, RELAT_1, FUNCOP_1, XREAL_1, TARSKI,
FINSEQ_1, XBOOLE_1, FINSEQ_2, RELSET_1, CARD_1, FINSEQ_3, PARTFUN1,
XXREAL_2, SUBSET_1, MARGREL1, FUNCT_6, CARD_3, XBOOLE_0, FUNCT_7;
schemes NAT_1, CLASSES1, BINOP_1, FUNCT_1, FUNCT_2, RECDEF_1;
begin :: Preliminaries
reserve D for set;
reserve a,b,i,k,m,n,n1,n2 for Nat;
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:
m|^|^(n+1) = m|^(m|^|^n)
proof
succ Segm(n) = Segm(n+1) by NAT_1:38;
hence m|^|^(n+1) = exp(m,m|^|^n) by ORDINAL5:14
.= m|^(m|^|^n);
end;
Lm5: now
let 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;
thus m|^|^2 = m|^m by A1,A2,A3;
thus m|^|^3 = m|^(m|^m) by A1,A2,A3,A4;
thus m|^|^4 = m|^(m|^(m|^m)) by A1,A2,A3,A4,A5;
thus m|^|^5 = m|^(m|^(m|^(m|^m))) by A1,A2,A3,A4,A5,A6;
end;
registration
let m;
reduce m|^|^1 to m;
reducibility by Lm5;
end;
theorem
m|^|^2 = m|^m by Lm5;
theorem Th3:
m|^|^3 = m|^(m|^m) by Lm5;
theorem Th4:
m|^|^4 = m|^(m|^(m|^m)) by Lm5;
theorem Th5:
m|^|^5 = m|^(m|^(m|^(m|^m))) by Lm5;
begin :: Ackermann Function
definition
func AckermannFunction -> BinOp of NAT means :Def1:
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
proof
set NN = Funcs(NAT,NAT);
defpred g[Nat,object,object] means
for h being Function of Segm ($1+1),NN st h = $2 holds
$3 is Function of Segm ($1+1+1),NN &
for t being Function of Segm ($1+1+1),NN st t = $3 holds
t | Segm ($1+1) = h &
for ti being Function of NAT,NAT st ti = t.($1+1) holds
ti.0 = h.$1.1 &
for n being Nat holds ti.(n+1) = h.$1.(ti.n);
defpred G[object,object] means
for i being Nat st i = $1 holds
$2 is Function of Funcs(Segm (i+1),NN),Funcs(Segm (i+1+1),NN) &
for g being Function of Funcs(Segm (i+1),NN),Funcs(Segm (i+1+1),NN)
st g = $2 for h being Function of Segm (i+1),NN holds g[i,h,g.h];
A1: for i being object st i in NAT ex H being object st G[i,H]
proof
let x be object;
assume x in NAT;
then reconsider i = x as Element of NAT;
defpred gi[object,object] means g[i,$1,$2];
A2: for x being object st x in Funcs(Segm (i+1),NN)
ex y being object st y in Funcs(Segm (i+1+1),NN) & gi[x,y]
proof
let x be object such that
A3: x in Funcs(Segm (i+1),NN);
reconsider h = x as Function of Segm (i+1),NN by A3,FUNCT_2:66;
defpred P[object,object] means
for n being Nat st n = $1 holds
(n <= i implies $2 = h.$1) &
(n = i+1 implies ($2 is Function of NAT,NAT &
for ti being Function of NAT,NAT st ti = $2 holds
ti.0 = h.i.1 &
for n being Nat holds ti.(n+1) = h.i.(ti.n)));
A4: for z being object st z in Segm (i+1+1)
ex t being object st t in NN & P[z,t]
proof
let c be object such that
A5: c in Segm (i+1+1);
reconsider z = c as Nat by A5;
z < i+1+1 by A5,NAT_1:44;
then z <= i+1 by NAT_1:13;
then per cases by XXREAL_0:1;
suppose
A6: z < i+1;
take hz = h.z;
z in Segm (i+1) = dom h by A6,FUNCT_2:def 1,NAT_1:44;
then h.z in rng h c= NN by FUNCT_1:def 3;
hence thesis by A6;
end;
suppose
A7: z = i+1;
deffunc T(object,object) = h.i.$2;
consider t being Function such that
A8: dom t = NAT & t.0 = h.i.1 and
A9: for n being Nat holds t.(n+1) = T(n,t.n) from NAT_1:sch 11;
take t;
rng t c= NAT
proof
let y be object such that
A10: y in rng t;
consider x being object such that
A11: x in dom t & t.x = y by A10,FUNCT_1:def 3;
reconsider x as Nat by A11,A8;
i < i+1 by NAT_1:13;
then i in Segm (i+1) = dom h by NAT_1:44,FUNCT_2:def 1;
then h.i in rng h c= NN by FUNCT_1:def 3;
then reconsider hi = h.i as Function of NAT,NAT by FUNCT_2:66;
defpred H[Nat] means t.$1 in NAT;
A12: dom hi = NAT & rng hi c= NAT by FUNCT_2:def 1;
hi.1 in rng hi by A12,FUNCT_1:def 3;
then
A13: H[0] by A8;
A14: for j being Nat st H[j] holds H[j+1]
proof
let j be Nat;
assume H[j];
then t.(j+1) = hi.(t.j) in rng hi by A12,A9,FUNCT_1:def 3;
hence thesis;
end;
for j being Nat holds H[j] from NAT_1:sch 2(A13,A14);
then t.x in NAT;
hence thesis by A11;
end;
then t is Function of NAT,NAT by A8,FUNCT_2:2;
hence thesis by A7,NAT_1:13,A8,A9,FUNCT_2:9;
end;
end;
consider P being Function such that
A15: dom P = Segm (i+1+1) & rng P c= NN
& for z being object st z in Segm (i+1+1) holds P[z,P.z]
from FUNCT_1:sch 6(A4);
take P;
thus
A16: P in Funcs(Segm (i+1+1),NN) by A15,FUNCT_2:def 2;
thus g[i,x,P]
proof
let h1 be Function of Segm (i+1),NN such that
A17: h1 = x;
thus P is Function of Segm (i+1+1),NN by A16,FUNCT_2:66;
let t be Function of Segm (i+1+1),NN such that
A18: t = P;
A19: dom h1 = Segm (i+1) by FUNCT_2:def 1;
A20: i+1 < i+1+1 by NAT_1:13;
then
A21: Segm (i+1) c= Segm (i+1+1) = dom t by NAT_1:39, FUNCT_2:def 1;
then
A22: dom (t | Segm (i+1)) = Segm (i+1) by RELAT_1:62;
for z being object st z in Segm (i+1) holds (t | Segm (i+1)).z = h1.z
proof
let z be object such that
A23: z in Segm(i+1);
reconsider z as Nat by A23;
z < i+1 by A23,NAT_1:44;
then z <= i by NAT_1:13;
then P.z = h.z by A15,A23,A21;
hence thesis by A17,A18,A23,FUNCT_1:49;
end;
hence t | Segm (i+1) = h1 by A19,A22,FUNCT_1:2;
let ti be Function of NAT,NAT such that
A24: ti = t.(i+1);
i+1 in Segm (i+1+1) by A20,NAT_1:44;
hence thesis by A24,A17,A18,A15;
end;
end;
consider H being Function such that
A25: dom H = Funcs(Segm (i+1),NN) & rng H c= Funcs(Segm (i+1+1),NN)
& for x being object st x in Funcs(Segm (i+1),NN) holds gi[x,H.x]
from FUNCT_1:sch 6(A2);
take H;
let j be Nat such that
A26: j = x;
thus H is Function of Funcs(Segm (j+1),NN),Funcs(Segm (j+1+1),NN)
by A26,A25,FUNCT_2:2;
let g be Function of Funcs(Segm (j+1),NN),Funcs(Segm (j+1+1),NN)
such that
A27: g = H;
let h be Function of Segm (j+1),NN;
h in Funcs(Segm (i+1),NN) by A26,FUNCT_2:8;
hence g[j,h,g.h] by A25,A27,A26;
end;
consider GG being Function such that
A28: dom GG = NAT & for i being object st i in NAT holds G[i,GG.i]
from CLASSES1:sch 1(A1);
for x being object st x in dom GG holds GG.x is Function by A28;
then reconsider GG as Function-yielding Function by FUNCOP_1:def 6;
deffunc Q(object,object) = GG.$1.$2;
deffunc A0(Element of NAT) = $1+1;
consider a0 being Function of NAT,NAT such that
A29: for x being Element of NAT holds a0.x = A0(x) from FUNCT_2:sch 4;
set f0 = (Segm 1) --> a0;
a0 in NN by FUNCT_2:8;
then
A30: {a0} c= NN by ZFMISC_1:31;
A31: rng f0 = {a0} & dom f0 = Segm 1 by FUNCOP_1:8;
consider Ack being Function such that
A32: dom Ack = NAT & Ack.0 = f0 and
A33: for n being Nat holds Ack.(n+1) = Q(n,Ack.n) from NAT_1:sch 11;
defpred A[Nat] means Ack.$1 in Funcs(Segm ($1+1),NN);
A34:A[0] by A32,A31,A30,FUNCT_2:def 2;
A35:for j being Nat st A[j] holds A[j+1]
proof
let j be Nat such that
A36: A[j];
j in NAT by ORDINAL1:def 12;
then reconsider GGj = GG.j as Function of
Funcs(Segm (j+1),NN),Funcs(Segm (j+1+1),NN) by A28;
A37: Ack.(j+1) = GGj.(Ack.j) by A33;
Funcs(Segm (j+1),NN) = dom GGj by FUNCT_2:def 1;
then GGj.(Ack.j) in rng GGj c= Funcs(Segm (j+1+1),NN)
by A36,FUNCT_1:def 3;
hence thesis by A37;
end;
A38:for j being Nat holds A[j] from NAT_1:sch 2(A34,A35);
for x being object st x in dom Ack holds Ack.x is Function
proof
let x be object;
assume x in dom Ack;
then reconsider x as Nat by A32;
Ack.x in Funcs(Segm (x+1),NN) by A38;
hence thesis;
end;
then reconsider Ack as Function-yielding Function by FUNCOP_1:def 6;
defpred ack[object,object,object] means
for A being Function of NAT,NAT st A = Ack.$1.$1 holds $3 = A.$2;
A39:for x,y being object st x in NAT & y in NAT
ex z being object st z in NAT & ack[x,y,z]
proof
let x,y be object such that
A40: x in NAT & y in NAT;
reconsider x as Nat by A40;
Ack.x in Funcs(Segm (x+1),NN) by A38;
then reconsider Ackx = Ack.x as Function of Segm (x+1),NN by FUNCT_2:66;
x < x+1 by NAT_1:13;
then x in Segm (x+1) = dom Ackx by NAT_1:44,FUNCT_2:def 1;
then Ackx.x in rng Ackx c= NN by FUNCT_1:def 3;
then reconsider Ackxx = Ackx.x as Function of NAT,NAT by FUNCT_2:66;
take z = Ackxx.y;
dom Ackxx = NAT by FUNCT_2:def 1;
then z in rng Ackxx c= NAT by A40,FUNCT_1:def 3;
hence thesis;
end;
consider IT being BinOp of NAT such that
A41:for x,y being object st x in NAT & y in NAT holds ack[x,y,IT.(x,y)]
from BINOP_1:sch 1(A39);
take IT;
let m,n be Nat;
A42:n in NAT by ORDINAL1:def 12;
reconsider m as Element of NAT by ORDINAL1:def 12;
f0.0 = a0 by NAT_1:44,FUNCOP_1:7;
then IT.(0,n) = a0.n by A32,A41,A42;
hence IT.(0,n) = n+1 by A42,A29;
m > 0 implies IT.(m,0) = IT.(m-1,1) &
(n > 0 implies IT.(m,n) = IT.(m-1,IT.(m,n-1)))
proof
assume m > 0;
then reconsider m1 = m-1 as Element of NAT by NAT_1:20;
Ack.m in Funcs(Segm (m+1),NN) by A38;
then reconsider Ackm = Ack.m as Function of Segm (m+1),NN by FUNCT_2:66;
m < m+1 by NAT_1:13;
then m in Segm (m+1) = dom Ackm by NAT_1:44,FUNCT_2:def 1;
then Ackm.m in rng Ackm c= NN by FUNCT_1:def 3;
then reconsider Ackmm = Ackm.m as Function of NAT,NAT by FUNCT_2:66;
Ack.m1 in Funcs(Segm (m1+1),NN) by A38;
then reconsider Ackm1 = Ack.m1 as Function of Segm (m1+1),NN
by FUNCT_2:66;
m1 < m1+1 by NAT_1:13;
then m1 in Segm (m1+1) = dom Ackm1 by NAT_1:44,FUNCT_2:def 1;
then Ackm1.m1 in rng Ackm1 c= NN by FUNCT_1:def 3;
then reconsider Ackm1m1 = Ackm1.m1 as Function of NAT,NAT by FUNCT_2:66;
reconsider GGm = GG.m as
Function of Funcs(Segm (m+1),NN),Funcs(Segm (m+1+1),NN) by A28;
reconsider GGmA = GGm.Ackm as Function of Segm (m+1+1),NN by A28;
m+1 < m+1+1 by NAT_1:13;
then m+1 in Segm (m+1+1) = dom GGmA by NAT_1:44,FUNCT_2:def 1;
then GGmA.(m+1) in rng GGmA c= NN by FUNCT_1:def 3;
then reconsider GGmAm = GGmA.(m+1) as Function of NAT,NAT by FUNCT_2:66;
reconsider GGm1 = GG.m1 as
Function of Funcs(Segm (m1+1),NN),Funcs(Segm (m1+1+1),NN) by A28;
reconsider GGm1A = GGm1.Ackm1 as Function of Segm (m1+1+1),NN by A28;
m1+1 < m1+1+1 by NAT_1:13;
then m1+1 in Segm (m1+1+1) = dom GGm1A by NAT_1:44,FUNCT_2:def 1;
then GGm1A.(m1+1) in rng GGm1A c= NN by FUNCT_1:def 3;
then reconsider GGm1Am = GGm1A.(m1+1) as Function of NAT,NAT
by FUNCT_2:66;
A43: Ackmm = GGm1A.m by A33;
then
A44: Ackmm.0 = Ackm1.m1.1 by A28;
IT.(m1,1) = Ackm1m1.1 by A41;
hence IT.(m,0) = IT.(m-1,1) by A44,A41;
assume n > 0;
then reconsider n1 = n-1 as Element of NAT by NAT_1:20;
IT.(m,n) = Ackmm.(n1+1) by A41;
then
A45: IT.(m,n) = Ackm1.m1.(GGm1Am.n1) by A28,A43;
IT.(m1,IT.(m,n1)) = Ackm1m1.(IT.(m,n1)) by A41;
hence thesis by A45,A43,A41;
end;
hence thesis;
end;
uniqueness
proof
let A1,A2 be BinOp of NAT such that
A46: for m,n being Nat holds
A1.(0,n) = n+1 &
(m > 0 implies A1.(m,0) = A1.(m-1,1)) &
(m > 0 & n > 0 implies A1.(m,n) = A1.(m-1,A1.(m,n-1))) and
A47: for m,n being Nat holds
A2.(0,n) = n+1 &
(m > 0 implies A2.(m,0) = A2.(m-1,1)) &
(m > 0 & n > 0 implies A2.(m,n) = A2.(m-1,A2.(m,n-1)));
defpred P[Nat] means
for i being Nat holds A1.($1,i) = A2.($1,i);
A48:P[0]
proof
let i be Nat;
thus A1.(0,i) = i+1 by A46
.= A2.(0,i) by A47;
end;
A49:for m being Nat st P[m] holds P[m+1]
proof
let m be Nat such that
A50: P[m];
defpred Q[Nat] means A1.(m+1,$1) = A2.(m+1,$1);
A51: m = m+1-1;
then A1.(m+1,0) = A1.(m,1) by A46
.= A2.(m,1) by A50;
then
A52: Q[0] by A47,A51;
A53: for n being Nat st Q[n] holds Q[n+1]
proof
let n be Nat such that
A54: Q[n];
reconsider m,n as Element of NAT by ORDINAL1:def 12;
A55: n = n+1-1;
then A1.(m+1,n+1) = A1.(m,A2.(m+1,n)) by A54,A51,A46
.= A2.(m,A2.(m+1,n)) by A50;
hence thesis by A55,A51,A47;
end;
for n being Nat holds Q[n] from NAT_1:sch 2(A52,A53);
hence thesis;
end;
for m being Nat holds P[m] from NAT_1:sch 2(A48,A49);
hence thesis;
end;
end;
set AF = AckermannFunction;
definition
let m,n be Nat;
func Ackermann(m,n) -> Element of NAT equals
AckermannFunction.(m,n);
coherence
proof
reconsider m,n as Element of NAT by ORDINAL1:def 12;
AF.(m,n) is Element of NAT;
hence thesis;
end;
end;
deffunc A(Nat,Nat) = Ackermann($1,$2);
theorem Th6:
Ackermann(m+1,0) = Ackermann(m,1)
proof
m+1-1 = m;
hence thesis by Def1;
end;
theorem Th7:
Ackermann(m+1,n+1) = Ackermann(m,Ackermann(m+1,n))
proof
m+1-1 = m & n+1-1 = n;
hence thesis by Def1;
end;
theorem
Ackermann(0,n) = n+1 by Def1;
theorem Th9:
Ackermann(1,n) = n+2
proof
defpred P[Nat] means A(1,$1) = $1+2;
A1: P[0]
proof
thus A(1,0) = A(1-1,1) by Def1
.= 1+1 by Def1
.= 0+2;
end;
A2: for k st P[k] holds P[k+1]
proof
let k such that
A3: P[k];
thus A(1,k+1) = A(1-1,A(1,k+1-1)) by Def1
.= A(1,k)+1 by Def1
.= k+1+2 by A3;
end;
for k holds P[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th10:
Ackermann(2,n) = 2*n+3
proof
defpred P[Nat] means A(2,$1) = 2*$1+3;
A1: P[0]
proof
thus A(2,0) = A(2-1,1) by Def1
.= 2+1 by Th9
.= 2*0+3;
end;
A2: for k st P[k] holds P[k+1]
proof
let k such that
A3: P[k];
thus A(2,k+1) = A(2-1,A(2,k+1-1)) by Def1
.= A(2,k)+2 by Th9
.= 2*(k+1)+3 by A3;
end;
for k holds P[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th11:
Ackermann(3,n) = 2|^(n+3)-3
proof
defpred P[Nat] means A(3,$1) = 2|^($1+3)-3;
A1: P[0]
proof
thus A(3,0) = A(3-1,1) by Def1
.= 2*1+3 by Th10
.= 2|^(0+3)-3 by Lm2;
end;
A2: for k st P[k] holds P[k+1]
proof
let k such that
A3: P[k];
thus A(3,k+1) = A(3-1,A(3,k+1-1)) by Def1
.= 2*A(3,k)+3 by Th10
.= 2*2|^(k+3)-3 by A3
.= 2|^(k+3+1)-3 by NEWTON:6
.= 2|^(k+1+3)-3;
end;
for k holds P[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th12:
Ackermann(4,n) = 2|^|^(n+3)-3
proof
defpred P[Nat] means A(4,$1) = 2|^|^($1+3)-3;
A1: P[0]
proof
A2: 2 |^|^ 3 = exp(2,exp(2,2)) by ORDINAL5:19;
thus A(4,0) = A(4-1,1) by Def1
.= 2|^(1+3)-3 by Th11
.= 2|^|^(0+3)-3 by A2,Lm1;
end;
A3: for k st P[k] holds P[k+1]
proof
let k such that
A4: P[k];
A5: A(4,k)+3 = 2|^|^(k+3) by A4;
succ Segm(k+3) = Segm(k+3+1) by NAT_1:38;
then
A6: 2|^|^(k+4) = exp(2,2|^|^(k+3)) by ORDINAL5:14
.= 2|^(2|^|^(k+3));
thus A(4,k+1) = A(4-1,A(4,k+1-1)) by Def1
.= 2|^|^(k+1+3)-3 by A5,A6,Th11;
end;
for k holds P[k] from NAT_1:sch 2(A1,A3);
hence thesis;
end;
theorem
Ackermann(4,0) = 13
proof
2|^|^3 = 2|^(2|^2) by Th3;
hence 13 = 2|^|^(0+3)-3 by Lm1,Lm3
.= A(4,0) by Th12;
end;
theorem
Ackermann(4,1) = 65533
proof
2|^|^4 = 2|^(2|^(2|^2)) by Th4;
hence 65533 = 2|^|^(1+3)-3 by Lm1,Lm3,Lm4
.= A(4,1) by Th12;
end;
theorem
Ackermann(4,2) = 2|^65536-3
proof
thus 2|^65536-3 = 2|^|^(2+3)-3 by Lm1,Lm3,Lm4,Th5
.= A(4,2) by Th12;
end;
theorem Th16:
n < Ackermann(m,n)
proof
defpred M[Nat] means for n holds n < A($1,n);
A1: M[0]
proof
let n;
A(0,n) = n+1 by Def1;
hence thesis by NAT_1:16;
end;
A2: for m st M[m] holds M[m+1]
proof
let m such that
A3: M[m];
defpred N[Nat] means $1 < A(m+1,$1);
A4: N[0]
proof
A(m+1,0) = A(m,1) by Th6;
hence 0 < A(m+1,0) by A3;
end;
A5: for n st N[n] holds N[n+1]
proof
let n;
assume N[n];
then
A6: n+1 <= A(m+1,n) by NAT_1:13;
A(m,A(m+1,n)) = A(m+1,n+1) by Th7;
hence thesis by A3,A6,XXREAL_0:2;
end;
for n holds N[n] from NAT_1:sch 2(A4,A5);
hence thesis;
end;
for k holds M[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th17:
Ackermann(m,n) < Ackermann(m,n+1)
proof
defpred P[Nat] means A($1,n) < A($1,n+1);
A1: P[0]
proof
A(0,n) = n+1 & A(0,n+1) = n+1+1 by Def1;
hence A(0,n) < A(0,n+1) by NAT_1:16;
end;
A2: for k st P[k] holds P[k+1]
proof
let k such that P[k];
A(k+1,n+1) = A(k,A(k+1,n)) by Th7;
hence A(k+1,n) < A(k+1,n+1) by Th16;
end;
for k holds P[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th18:
a < b implies Ackermann(m,a) < Ackermann(m,b)
proof
defpred P[Nat] means for a st a < $1 holds A(m,a) < A(m,$1);
A1: P[0];
A2: for k st P[k] holds P[k+1]
proof
let k such that
A3: P[k];
let a;
assume a < k+1;
then a <= k by NAT_1:13;
then per cases by XXREAL_0:1;
suppose a < k;
then A(m,a) < A(m,k) by A3;
hence A(m,a) < A(m,k+1) by Th17,XXREAL_0:2;
end;
suppose a = k;
hence A(m,a) < A(m,k+1) by Th17;
end;
end;
for k holds P[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th19:
a <= b implies Ackermann(m,a) <= Ackermann(m,b)
proof
assume a <= b;
then a < b or a = b by XXREAL_0:1;
hence thesis by Th18;
end;
theorem Th20:
m < Ackermann(m,n)
proof
defpred M[Nat] means for m holds m < A(m,$1);
A1: M[0]
proof
let m;
defpred N[Nat] means $1 < A($1,0);
A2: N[0]
proof
A(0,0) = 0+1 by Def1;
hence thesis;
end;
A3: for k st N[k] holds N[k+1]
proof
let k;
assume N[k];
then
A4: k+1 <= A(k,0) by NAT_1:13;
A5: A(k,0) < A(k,0+1) by Th17;
A(k+1,0) = A(k,1) by Th6;
hence k+1 < A(k+1,0) by A4,A5,XXREAL_0:2;
end;
for k holds N[k] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
A6: for n st M[n] holds M[n+1]
proof
let n such that
A7: M[n];
defpred N[Nat] means $1 < A($1,n+1);
A8: N[0]
proof
A(0,n+1) = n+1+1 by Def1;
hence 0 < A(0,n+1);
end;
A9: for a st N[a] holds N[a+1]
proof
let a;
assume N[a];
A10: A(a,A(a+1,n)) = A(a+1,n+1) by Th7;
A(a+1,n) < A(a,A(a+1,n)) by Th16;
hence thesis by A7,A10,XXREAL_0:2;
end;
for n holds N[n] from NAT_1:sch 2(A8,A9);
hence thesis;
end;
for k holds M[k] from NAT_1:sch 2(A1,A6);
hence thesis;
end;
theorem Th21:
Ackermann(m,n+1) <= Ackermann(m+1,n)
proof
defpred P[Nat] means for m holds A(m,$1+1) <= A(m+1,$1);
A1: P[0] by Th6;
A2: for k st P[k] holds P[k+1]
proof
let k such that
A3: P[k];
let m;
k+1+1 <= A(m,k+1) by Th16,NAT_1:13;
then
A4: A(m,k+1+1) <= A(m,A(m,k+1)) by Th19;
A(m,A(m,k+1)) <= A(m,A(m+1,k)) by A3,Th19;
then A(m,k+1+1) <= A(m,A(m+1,k)) by A4,XXREAL_0:2;
hence A(m,k+1+1) <= A(m+1,k+1) by Th7;
end;
for k holds P[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th22:
Ackermann(m,n) < Ackermann(m+1,n)
proof
defpred P[Nat] means for n holds A($1,n) < A($1+1,n);
A1: P[0]
proof
let n;
A2: A(0,n) = n+1 by Def1;
A(1,n) = n+2 by Th9;
hence A(0,n) < A(0+1,n) by A2,XREAL_1:6;
end;
A3: for k st P[k] holds P[k+1]
proof
let k such that
A4: P[k];
defpred A[Nat] means A(k+1,$1) < A(k+2,$1);
A5: A[0]
proof
A(k+1,0) = A(k,1) & A(k+1+1,0) = A(k+1,1) by Th6;
hence A(k+1,0) < A(k+2,0) by A4;
end;
A6: for b st A[b] holds A[b+1]
proof
let b such that
A7: A[b];
A8: A(k+1,b+1) = A(k,A(k+1,b)) by Th7;
A(k,A(k+1,b)) < A(k,A(k+2,b)) by A7,Th18;
then A(k,A(k+1,b)) < A(k+1,A(k+1+1,b)) by A4,XXREAL_0:2;
hence A(k+1,b+1) < A(k+2,b+1) by A8,Th7;
end;
for b holds A[b] from NAT_1:sch 2(A5,A6);
hence thesis;
end;
for k holds P[k] from NAT_1:sch 2(A1,A3);
hence thesis;
end;
theorem Th23:
a < b implies Ackermann(a,n) < Ackermann(b,n)
proof
defpred P[Nat] means for a st a < $1 holds A(a,n) < A($1,n);
A1: P[0];
A2: for k st P[k] holds P[k+1]
proof
let k such that
A3: P[k];
let a;
assume a < k+1;
then a <= k by NAT_1:13;
then per cases by XXREAL_0:1;
suppose a < k;
then A(a,n) < A(k,n) by A3;
hence A(a,n) < A(k+1,n) by Th22,XXREAL_0:2;
end;
suppose a = k;
hence A(a,n) < A(k+1,n) by Th22;
end;
end;
for k holds P[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th24:
a <= b implies Ackermann(a,n) <= Ackermann(b,n)
proof
assume a <= b;
then a < b or a = b by XXREAL_0:1;
hence thesis by Th23;
end;
theorem Th25:
Ackermann(k,Ackermann(m,n)) < Ackermann(k+m+2,n)
proof
A1: A(k,A(m,n)) <= A(k+m,A(m,n)) by Th24,NAT_1:11;
m < m+(k+1) by NAT_1:16;
then A(m,n) < A(k+m+1,n) by Th23;
then A(k+m,A(m,n)) < A(k+m,A(k+m+1,n)) by Th18;
then
A2: A(k,A(m,n)) < A(k+m,A(k+m+1,n)) by A1,XXREAL_0:2;
A3: A(k+m,A(k+m+1,n)) = A(k+m+1,n+1) by Th7;
A(k+m+1,n+1) <= A(k+m+1+1,n) by Th21;
hence A(k,A(m,n)) < A(k+m+2,n) by A2,A3,XXREAL_0:2;
end;
theorem
for r,s,y being Nat holds
Ackermann(r,y) + Ackermann(s,y) < Ackermann(4+max(r,s),y)
proof
let r,s,y be Nat;
reconsider z = max(r,s) as Nat by TARSKI:1;
set t = 4+max(r,s);
A(r,y) <= A(z,y) & A(s,y) <= A(z,y) by Th24,XXREAL_0:25;
then
A1: A(r,y)+A(s,y) <= A(z,y)+A(z,y) by XREAL_1:7;
2*A(z,y)+3 = A(2,A(z,y)) by Th10;
then
A2: A(r,y)+A(s,y) < A(2,A(z,y)) by A1,XXREAL_0:2,NAT_1:16;
A(2,A(z,y)) < A(2+z+2,y) by Th25;
hence thesis by A2,XXREAL_0:2;
end;
theorem Th27:
for r,n being Nat holds Ackermann(r,n+n) < Ackermann(r+4,n)
proof
let r,n be Nat;
A1: n+n < A(2,n)
proof
2*n = n+n;
then A(2,n) = n+n+3 by Th10;
hence thesis by NAT_1:16;
end;
A(r,n+n) < A(r,A(2,n)) by A1,Th18;
then A(r,n+n) < A(r+2+2,n) by Th25,XXREAL_0:2;
hence thesis;
end;
registration
let m,n;
cluster Ackermann(m,n) -> non zero;
coherence by Th16;
end;
definition
let m;
func AckermannFunction(m) -> UnOp of NAT means :Def3:
for n being Nat holds it.n = Ackermann(m,n);
existence
proof
deffunc F(Nat) = A(m,$1);
consider f being Function of NAT,NAT such that
A1: for x being Element of NAT holds f.x = F(x) from FUNCT_2:sch 4;
take f;
let n;
n in NAT by ORDINAL1:def 12;
hence thesis by A1;
end;
uniqueness
proof
let f,g be UnOp of NAT such that
A2: for n being Nat holds f.n = A(m,n) and
A3: for n being Nat holds g.n = A(m,n);
let n be Element of NAT;
thus f.n = A(m,n) by A2
.= g.n by A3;
end;
end;
deffunc AF(Nat) = AckermannFunction($1);
registration
let m;
cluster AckermannFunction(m) -> positive-yielding;
coherence
proof
set f = AF(m);
let r be Real;
assume r in rng f;
then consider x being object such that
A1: x in dom f and
A2: f.x = r by FUNCT_1:def 3;
reconsider x as Nat by A1;
f.x = A(m,x) by Def3;
hence thesis by A2;
end;
end;
registration
let m;
cluster AckermannFunction(m) -> increasing;
coherence
proof
set f = AF(m);
let a,b;
f.a = A(m,a) & f.b = A(m,b) by Def3;
hence thesis by Th18;
end;
end;
theorem
AckermannFunction(m+1).0 = AckermannFunction(m).1
proof
thus AF(m+1).0 = A(m+1,0) by Def3
.= A(m,1) by Th6
.= AF(m).1 by Def3;
end;
theorem
AckermannFunction(m+1).(n+1) = AckermannFunction(m).(AckermannFunction(m+1).n)
proof
A1: A(m+1,n) = AF(m+1).n by Def3;
thus AF(m+1).(n+1) = A(m+1,n+1) by Def3
.= A(m,A(m+1,n)) by Th7
.= AF(m).(AF(m+1).n) by A1,Def3;
end;
begin :: Auxiliary operations
definition
let f be Function;
func dom2tuple(f) -> Function means :Def4:
dom it = 1-tuples_on dom f &
for x being object st x in dom f holds it.<*x*> = f.x if f is non empty
otherwise it = {};
existence
proof
thus f is non empty implies
ex F being Function st dom F = 1-tuples_on dom f &
for x being object st x in dom f holds F.<*x*> = f.x
proof
assume f is non empty;
defpred P[object,object] means
ex x being object st $1 = <*x*> & $2 = f.x;
set X = 1-tuples_on dom f;
A1: for e being object st e in X ex u being object st P[e,u]
proof
let e be object;
assume e in X;
then consider x being set such that
x in dom f and
A2: e = <*x*> by FINSEQ_2:135;
take f.x;
thus thesis by A2;
end;
consider F being Function such that
A3: dom F = X and
A4: for e being object st e in X holds P[e,F.e] from CLASSES1:sch 1(A1);
take F;
thus dom F = X by A3;
let e be object;
assume e in dom f;
then P[<*e*>,F.<*e*>] by A4,FINSEQ_2:98;
hence F.<*e*> = f.e by FINSEQ_1:76;
end;
thus thesis;
end;
uniqueness
proof
let g,h be Function;
thus f is non empty &
(dom g = 1-tuples_on dom f) &
(for x being object st x in dom f holds g.<*x*> = f.x) &
(dom h = 1-tuples_on dom f) &
(for x being object st x in dom f holds h.<*x*> = f.x) implies g = h
proof
assume that
f is non empty and
A5: dom g = 1-tuples_on dom f and
A6: for x being object st x in dom f holds g.<*x*> = f.x and
A7: dom h = 1-tuples_on dom f and
A8: for x being object st x in dom f holds h.<*x*> = f.x;
thus dom g = dom h by A5,A7;
let a be object;
assume a in dom g;
then consider x being set such that
A9: x in dom f & a = <*x*> by A5,FINSEQ_2:135;
thus g.a = f.x by A6,A9
.= h.a by A8,A9;
end;
thus thesis;
end;
consistency;
end;
deffunc D(Function) = dom2tuple($1);
registration
let f be empty Function;
cluster dom2tuple(f) -> empty;
coherence by Def4;
end;
registration
let f be non empty Function;
cluster dom2tuple(f) -> non empty;
coherence
proof
dom D(f) = 1-tuples_on dom f by Def4;
hence thesis;
end;
end;
registration
let D be set;
let f be D-defined Function;
cluster dom2tuple(f) -> D*-defined;
coherence
proof
set F = D(f);
per cases;
suppose f is empty;
then dom F = {};
hence dom F c= D* by XBOOLE_1:2;
end;
suppose f is non empty;
then
A1: dom F = 1-tuples_on dom f by Def4;
thus dom F c= D*
proof
let a be object;
assume a in dom F;
then consider x being set such that
A2: x in dom f and
A3: a = <*x*> by A1,FINSEQ_2:135;
reconsider D as non empty set by A2;
reconsider x as Element of D by A2;
<*x*> is FinSequence of D;
hence thesis by A3,FINSEQ_1:def 11;
end;
end;
end;
end;
registration
let D be set;
let f be D-valued Function;
cluster dom2tuple(f) -> D-valued;
coherence
proof
set F = D(f);
per cases;
suppose f is empty;
then rng F = {};
hence rng F c= D by XBOOLE_1:2;
end;
suppose
A1: f is non empty;
then
A2: dom F = 1-tuples_on dom f by Def4;
thus rng F c= D
proof
let y be object;
assume y in rng F;
then consider a being object such that
A3: a in dom F and
A4: F.a = y by FUNCT_1:def 3;
consider x being set such that
A5: x in dom f and
A6: a = <*x*> by A2,A3,FINSEQ_2:135;
A7: F.<*x*> = f.x by A1,A5,Def4;
f.x in rng f by A5,FUNCT_1:def 3;
hence thesis by A4,A6,A7;
end;
end;
end;
end;
registration
let D be non empty set;
let f be D-defined Function;
cluster dom2tuple(f) -> homogeneous;
coherence
proof
set F = D(f);
now
per cases;
suppose f is empty;
then dom F = {};
hence dom F c= 1-tuples_on D by XBOOLE_1:2;
end;
suppose f is non empty;
then
A1: dom F = 1-tuples_on dom f by Def4;
thus dom F c= 1-tuples_on D
proof
let a be object;
assume a in dom F;
then consider x being set such that
A2: x in dom f and
A3: a = <*x*> by A1,FINSEQ_2:135;
reconsider x as Element of D by A2;
<*x*> is FinSequence of D;
hence thesis by A3,FINSEQ_2:98;
end;
end;
end;
hence thesis by COMPUT_1:16;
end;
end;
theorem Th30:
for f being UnOp of D holds dom2tuple(f) is PartFunc of D*,D
proof
let f be UnOp of D;
set F = dom2tuple(f);
per cases;
suppose f is empty;
then F = {};
hence thesis by XBOOLE_1:2;
end;
suppose f is non empty;
then
A1: dom F = 1-tuples_on dom f by Def4;
rng F c= D;
hence thesis by A1,RELSET_1:4;
end;
end;
registration
let D be non empty set;
let f be UnOp of D;
cluster dom2tuple(f) -> 1-ary;
coherence
proof
set F = dom2tuple(f);
A1: F is Relation of D*,D by Th30;
A2: dom F = 1-tuples_on dom f by Def4;
dom f = D by FUNCT_2:def 1;
hence arity F = 1 by A1,A2,COMPUT_1:25;
end;
end;
definition
let D be set;
let f be BinOp of D;
func dom2tuple(f) -> Function means :Def5:
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 D is non empty
otherwise it = {};
existence
proof
thus D is non empty implies
ex F being Function st dom F = 2-tuples_on D &
for x,y being object st [x,y] in dom f holds F.<*x,y*> = f.(x,y)
proof
assume D is non empty;
defpred P[object,object] means
ex x,y being object st $1 = <*x,y*> & $2 = f.(x,y);
set X = 2-tuples_on D;
A1: for e being object st e in X ex u being object st P[e,u]
proof
let e be object;
assume e in X;
then consider x,y being object such that
x in D & y in D and
A2: e = <*x,y*> by FINSEQ_2:137;
take f.(x,y);
thus thesis by A2;
end;
consider F being Function such that
A3: dom F = X and
A4: for e being object st e in X holds P[e,F.e] from CLASSES1:sch 1(A1);
take F;
thus dom F = X by A3;
let e1,e2 be object;
assume [e1,e2] in dom f;
then e1 in D & e2 in D by ZFMISC_1:87;
then consider x,y being object such that
A5: <*e1,e2*> = <*x,y*> and
A6: F.<*e1,e2*> = f.(x,y) by A4,FINSEQ_2:101;
e1 = x & e2 = y by A5,FINSEQ_1:77;
hence F.<*e1,e2*> = f.(e1,e2) by A6;
end;
thus thesis;
end;
uniqueness
proof
let g,h be Function;
thus D is non empty &
(dom g = 2-tuples_on D) &
(for x,y being object st [x,y] in dom f holds g.<*x,y*> = f.(x,y)) &
(dom h = 2-tuples_on D) &
(for x,y being object st [x,y] in dom f holds h.<*x,y*> = f.(x,y))
implies g = h
proof
assume that
A7: D is non empty and
A8: dom g = 2-tuples_on D and
A9: for x,y being object st [x,y] in dom f holds g.<*x,y*> = f.(x,y) and
A10: dom h = 2-tuples_on D and
A11: for x,y being object st [x,y] in dom f holds h.<*x,y*> = f.(x,y);
thus dom g = dom h by A8,A10;
let a be object;
assume a in dom g;
then consider x,y being object such that
A12: x in D & y in D and
A13: a = <*x,y*> by A8,FINSEQ_2:137;
dom f = [:D,D:] by A7,FUNCT_2:def 1;
then
A14: [x,y] in dom f by A12,ZFMISC_1:87;
hence g.a = f.(x,y) by A9,A13
.= h.a by A11,A13,A14;
end;
thus thesis;
end;
consistency;
end;
registration
let f be BinOp of NAT;
cluster dom2tuple(f) -> NAT*-defined;
coherence
proof
set F = dom2tuple(f);
dom F = 2-tuples_on NAT by Def5;
hence dom F c= NAT* by FINSEQ_2:142;
end;
end;
registration
let D be set;
let f be BinOp of D;
cluster dom2tuple(f) -> D-valued;
coherence
proof
set F = dom2tuple(f);
thus rng F c= D
proof
per cases;
suppose D is empty;
then F = {} by Def5;
then rng F = {};
hence thesis by XBOOLE_1:2;
end;
suppose
A1: D is non empty;
let y be object;
assume y in rng F;
then consider x being object such that
A2: x in dom F and
A3: F.x = y by FUNCT_1:def 3;
dom F = 2-tuples_on D by A1,Def5;
then consider a,b being object such that
A4: a in D & b in D and
A5: x = <*a,b*> by A2,FINSEQ_2:137;
reconsider a,b as Element of D by A4;
dom f = [:D,D:] by A1,FUNCT_2:def 1;
then [a,b] in dom f by A1,ZFMISC_1:87;
then F.<*a,b*> = f.(a,b) by A1,Def5;
hence thesis by A1,A3,A5;
end;
end;
end;
end;
theorem Th31:
for f being BinOp of D holds dom2tuple(f) is PartFunc of D*,D
proof
let f be BinOp of D;
set F = dom2tuple(f);
per cases;
suppose D is empty;
then F = {};
hence thesis by XBOOLE_1:2;
end;
suppose D is non empty;
then
A1: dom F = 2-tuples_on D by Def5;
rng F c= D;
hence thesis by A1,RELSET_1:4,FINSEQ_2:134;
end;
end;
registration
let D be non empty set;
let f be BinOp of D;
cluster dom2tuple(f) -> homogeneous;
coherence
proof
dom dom2tuple(f) = 2-tuples_on D by Def5;
hence thesis by COMPUT_1:16;
end;
end;
registration
let D be non empty set;
let f be BinOp of D;
cluster dom2tuple(f) -> 2-ary;
coherence
proof
set F = dom2tuple(f);
A1: F is Relation of D*,D by Th31;
dom F = 2-tuples_on D by Def5;
hence arity F = 2 by A1,COMPUT_1:25;
end;
end;
theorem
dom2tuple(AckermannFunction) in HFuncs NAT
proof
dom2tuple(AckermannFunction) is Element of HFuncs NAT by COMPUT_1:28;
hence thesis;
end;
begin :: Primitive recursiveness
Lm6: <*0*> in T1 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:
for n being Nat holds f.n is homogeneous;
attr f is to-naturals means :Def7:
for n being Nat holds f.n is to-naturals;
attr f is primitive-recursive means :Def8:
for n being Nat holds f.n is primitive-recursive;
end;
definition
let D be set;
let f be Function-yielding ManySortedSet of NAT;
attr f is D-defined means :Def9:
for n being Nat holds f.n is D-defined;
end;
definition
let f be Function-yielding ManySortedSet of NAT;
attr f is satisfying_primrec_conditions means
f is homogeneous to-naturals NAT*-defined;
end;
registration
let f be homogeneous Function;
cluster NAT --> f -> homogeneous;
coherence by FUNCOP_1:7,ORDINAL1:def 12;
end;
registration
let f be to-naturals Function;
cluster NAT --> f -> to-naturals;
coherence by FUNCOP_1:7,ORDINAL1:def 12;
end;
registration
let f be primitive-recursive Function;
cluster NAT --> f -> primitive-recursive;
coherence 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 by FUNCOP_1:7,ORDINAL1:def 12;
end;
registration
cluster satisfying_primrec_conditions
for Function-yielding ManySortedSet of NAT;
existence
proof
take NAT --> the homogeneous to-naturals NAT*-defined Function;
thus thesis;
end;
end;
registration
cluster satisfying_primrec_conditions
-> homogeneous to-naturals NAT*-defined
for Function-yielding ManySortedSet of NAT;
coherence;
cluster homogeneous to-naturals NAT*-defined
-> satisfying_primrec_conditions
for Function-yielding ManySortedSet of NAT;
coherence;
end;
registration
let f be homogeneous Function-yielding ManySortedSet of NAT;
let n be Nat;
cluster f.n -> homogeneous;
coherence by Def6;
end;
registration
let f be to-naturals Function-yielding ManySortedSet of NAT;
let n be Nat;
cluster f.n -> to-naturals;
coherence by Def7;
end;
registration
cluster primitive-recursive for Function-yielding ManySortedSet of NAT;
existence
proof
take NAT --> 1 succ 1;
thus thesis;
end;
end;
registration
let f be primitive-recursive Function-yielding ManySortedSet of NAT;
let n be Nat;
cluster f.n -> primitive-recursive;
coherence by Def8;
end;
registration
let D be set;
cluster D-defined for Function-yielding ManySortedSet of NAT;
existence
proof
take NAT --> {};
thus thesis by RELAT_1:171;
end;
end;
registration
let D be set;
let f be D-defined Function-yielding ManySortedSet of NAT;
let n be Nat;
cluster f.n -> D-defined;
coherence by Def9;
end;
definition
let k be Nat;
let f be homogeneous Function-yielding ManySortedSet of NAT;
attr f is k-ary means :Def11:
for n being Nat holds f.n is k-ary;
end;
registration
let k be non zero Nat;
cluster k-ary primitive-recursive to-naturals NAT*-defined
for homogeneous Function-yielding ManySortedSet of NAT;
existence
proof
reconsider f = NAT --> k succ k
as homogeneous Function-yielding ManySortedSet of NAT;
take f;
thus f is k-ary by FUNCOP_1:7,ORDINAL1:def 12;
thus f is primitive-recursive;
thus f is to-naturals;
thus f is NAT*-defined;
end;
end;
registration
let k be non zero Nat;
let f be k-ary homogeneous Function-yielding ManySortedSet of NAT;
let n be Nat;
cluster f.n -> k-ary;
coherence by Def11;
end;
definition
let k be Nat;
func k-aryPrimRecFuncs -> Subset of HFuncs NAT equals
{f where f is Element of HFuncs NAT: f is k-ary primitive-recursive};
coherence
proof
set A =
{f where f is Element of HFuncs NAT: f is k-ary primitive-recursive};
A c= HFuncs NAT
proof
let a be object;
assume a in A;
then ex f being Element of HFuncs NAT st
a = f & f is k-ary primitive-recursive;
hence thesis;
end;
hence thesis;
end;
end;
theorem Th33:
k const n in k-aryPrimRecFuncs
proof
k const n in HFuncs NAT by COMPUT_1:31;
hence thesis;
end;
registration
let k be Nat;
cluster k-aryPrimRecFuncs -> non empty;
coherence by Th33;
end;
theorem Th34:
1 <= n <= k implies k succ n in k-aryPrimRecFuncs
proof
assume that
A1: 1 <= n & n <= k;
set f = k succ n;
A2: f in HFuncs NAT by COMPUT_1:33;
A3: f is k-ary
proof
thus arity f = k;
end;
f is primitive-recursive
proof
thus f in PrimRec by A1,COMPUT_1:70;
end;
hence thesis by A2,A3;
end;
definition
func AckermannSequence -> 1-ary satisfying_primrec_conditions
primitive-recursive Function-yielding ManySortedSet of NAT means :Def13:
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
proof
set D = 1-aryPrimRecFuncs;
reconsider d = 1 succ 1 as Element of D by Th34;
defpred P[Nat,set,set] means
($1 = 0 implies
$3 = primrec(0 const A(0,1),(1 succ 1)*<:<*2 proj 2*>:>, 1))
&
($1 <> 0 implies
ex g being 1-ary primitive-recursive Function st $2 = g &
$3 = primrec(0 const A($1,1),g*<:<*2 proj 2*>:>, 1));
A1: for n being Nat for x being Element of D
ex y being Element of D st P[n,x,y]
proof
let n be Nat;
let x be Element of D;
per cases by NAT_1:6;
suppose
A2: n = 0;
set y = primrec(0 const A(0,1),(1 succ 1)*<:<*2 proj 2*>:>, 1);
y in D;
then reconsider y as Element of D;
take y;
thus P[n,x,y] by A2;
end;
suppose ex a being Nat st n = a+1;
then consider a being Nat such that
A3: n = a+1;
x in D;
then consider g being Element of HFuncs NAT such that
A4: x = g and
A5: g is 1-ary primitive-recursive;
reconsider g as 1-ary primitive-recursive Function by A5;
set y = primrec(0 const A(n,1),g*<:<*2 proj 2*>:>, 1);
y in D;
then reconsider y as Element of D;
take y;
thus thesis by A3,A4;
end;
end;
consider f being sequence of D such that
A6: f.0 = d and
A7: for n being Nat holds P[n,f.n,f.(n+1)] from RECDEF_1:sch 2(A1);
reconsider f as Function-yielding ManySortedSet of NAT;
f is homogeneous
proof
let n;
per cases;
suppose n = 0;
hence thesis by A6;
end;
suppose
A8: n <> 0;
P[n,f.n,f.(n+1)] by A7;
hence thesis by A8;
end;
end;
then reconsider f as homogeneous Function-yielding ManySortedSet of NAT;
A9: f is 1-ary
proof
let n;
per cases;
suppose n = 0;
hence thesis by A6;
end;
suppose
A10: n <> 0;
P[n,f.n,f.(n+1)] by A7;
hence thesis by A10;
end;
end;
A11: f is primitive-recursive
proof
let n;
per cases;
suppose n = 0;
hence thesis by A6;
end;
suppose
A12: n <> 0;
P[n,f.n,f.(n+1)] by A7;
hence thesis by A12;
end;
end;
A13: f is to-naturals
proof
let n;
per cases;
suppose n = 0;
hence thesis by A6;
end;
suppose
A14: n <> 0;
P[n,f.n,f.(n+1)] by A7;
hence thesis by A14;
end;
end;
f is NAT*-defined by A11;
then reconsider f as 1-ary satisfying_primrec_conditions
primitive-recursive Function-yielding ManySortedSet of NAT by A9,A11,A13;
take f;
thus f.0 = 1 succ 1 by A6;
let n;
per cases;
suppose n = 0;
hence thesis by A6,A7;
end;
suppose
A15: n <> 0;
P[n,f.n,f.(n+1)] by A7;
hence thesis by A15;
end;
end;
uniqueness
proof
let f1,f2 be 1-ary satisfying_primrec_conditions
primitive-recursive Function-yielding ManySortedSet of NAT such that
A16: f1.0 = 1 succ 1 and
A17: for n being Nat holds
f1.(n+1) = primrec(0 const A(n,1), (f1.n)*<:<*2 proj 2*>:>, 1) and
A18: f2.0 = 1 succ 1 and
A19: for n being Nat holds
f2.(n+1) = primrec(0 const A(n,1), (f2.n)*<:<*2 proj 2*>:>, 1);
dom f1 = NAT by PARTFUN1:def 2;
hence dom f1 = dom f2 by PARTFUN1:def 2;
let n be object;
assume n in dom f1;
then reconsider m = n as Nat;
defpred P[Nat] means f1.$1 = f2.$1;
A20: P[0] by A16,A18;
A21: for n st P[n] holds P[n+1]
proof
let n;
assume P[n];
hence f2.(n+1) = primrec(0 const A(n,1), (f1.n)*<:<*2 proj 2*>:>, 1)
by A19
.= f1.(n+1) by A17;
end;
for k holds P[k] from NAT_1:sch 2(A20,A21);
then P[m];
hence thesis;
end;
end;
set AS = AckermannSequence;
registration
cluster AckermannSequence -> (HFuncs NAT)-valued;
coherence
proof
thus rng AS c= HFuncs NAT
proof
let y be object;
assume y in rng AS;
then consider x being object such that
A1: x in dom AS and
A2: AS.x = y by FUNCT_1:def 3;
reconsider x as Nat by A1;
per cases by NAT_1:6;
suppose x = 0;
then AS.x = 1 succ 1 by Def13;
hence thesis by A2,COMPUT_1:33;
end;
suppose ex n being Nat st x = n+1;
then consider n being Nat such that
A3: x = n+1;
AS.(n+1) = primrec(0 const A(n,1), (AS.n)*<:<*2 proj 2*>:>, 1)
by Def13;
hence thesis by A2,A3;
end;
end;
end;
end;
theorem Th35:
arity ((AckermannSequence.m)*<:<*2 proj 2*>:>) = 2
proof
set p1 = 2 proj 2;
set g1 = <:<*p1*>:>;
set f2 = (AS.m)*g1;
A1: f2 is Element of HFuncs NAT by COMPUT_1:28;
A2: m in NAT by ORDINAL1:def 12;
dom AS = NAT by PARTFUN1:def 2;
then
A3: AS.m in rng AS by A2,FUNCT_1:def 3;
p1 is Element of HFuncs NAT by COMPUT_1:28;
then <*p1*> is FinSequence of HFuncs NAT by FINSEQ_1:74;
hence arity f2 = arity <*p1*> by A1,A3,COMPUT_1:44
.= arity p1 by COMPUT_1:43
.= 2;
end;
theorem Th36:
AckermannSequence.m.<*n*> = Ackermann(m,n)
proof
defpred P[Nat] means for n holds AS.$1.<*n*> = A($1,n);
set p1 = 2 proj 2;
set g1 = <:<*p1*>:>;
A1: P[0]
proof
let m;
A2: AS.0 = 1 succ 1 by Def13;
defpred Q[Nat] means AS.0.<*$1*> = A(0,$1);
A3: Q[0]
proof
thus AS.0.<*0*> = <*0*>.1+1 by A2,Lm6,COMPUT_1:def 7
.= A(0,0) by Def1;
end;
A4: for k st Q[k] holds Q[k+1]
proof
let k such that Q[k];
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
<*k1+1*> in T1 by FINSEQ_2:98;
hence AS.0.<*k+1*> = <*k+1*>.1+1 by A2,COMPUT_1:def 7
.= A(0,k+1) by Def1;
end;
for k holds Q[k] from NAT_1:sch 2(A3,A4);
hence thesis;
end;
A5: for k st P[k] holds P[k+1]
proof
let k such that
A6: P[k];
A7: arity (0 const A(k,1)) = 0;
A8: AS.(k+1) = primrec(0 const A(k,1), (AS.k)*g1, 1) by Def13;
defpred Q[Nat] means AS.(k+1).<*$1*> = A(k+1,$1);
A9: Q[0]
proof
thus AS.(k+1).<*0*> = (0 const A(k,1)).{} by A7,A8,COMPUT_1:80
.= A(k,1) by Lm7,FUNCOP_1:7
.= A(k+1,0) by Th6;
end;
A10: for w being Nat st Q[w] holds Q[w+1]
proof
let w be Nat such that
A11: Q[w];
reconsider w1 = w as Element of NAT by ORDINAL1:def 12;
set f2 = (AS.k)*g1;
set x2 = primrec(0 const A(k,1),f2,1).<*w1*>;
set x = <*w1,x2*>;
A12: dom p1 = T2 by COMPUT_1:36;
A13: x2 in NAT by ORDINAL1:def 12;
then
x in T2 by FINSEQ_2:101;
then
A14: p1.x = x.2 by COMPUT_1:38;
A15: x2 = A(k+1,w) by A11,Def13;
A16: dom g1 = T2 by A12,FINSEQ_3:141;
arity f2 = 2 by Th35;
hence AS.(k+1).<*w+1*> = f2.x by A7,A8,COMPUT_1:82
.= (AS.k).(g1.x) by A13,A16,FINSEQ_2:101,FUNCT_1:13
.= (AS.k).<*x2*> by A12,A13,A14,FINSEQ_2:101,FINSEQ_3:141
.= A(k,x2) by A6
.= A(k+1,w+1) by A15,Th7;
end;
for k holds Q[k] from NAT_1:sch 2(A9,A10);
hence thesis;
end;
for k holds P[k] from NAT_1:sch 2(A1,A5);
hence thesis;
end;
theorem Th37:
dom2tuple(AckermannFunction(0)) = 1 succ 1
proof
set f = D(AF(0));
set s = 1 succ 1;
set D = 1-tuples_on dom(AF(0));
dom f = D by Def4;
then
A1: dom f = 1-tuples_on NAT by FUNCT_2:def 1;
hence dom f = dom s by COMPUT_1:def 7;
let x be object;
assume
A2: x in dom f;
then consider a being set such that
A3: a in NAT and
A4: x = <*a*> by A1,FINSEQ_2:135;
reconsider a as Element of NAT by A3;
a in dom AF(0) by A3,FUNCT_2:def 1;
hence f.x = AF(0).a by A4,Def4
.= A(0,a) by Def3
.= <*a*>.1+1 by Def1
.= s.x by A1,A2,A4,COMPUT_1:def 7;
end;
theorem Th38:
dom2tuple(AckermannFunction(m+1)) =
primrec(0 const Ackermann(m,1), (AckermannSequence.m)*<:<*2 proj 2*>:>, 1)
proof
set f = D(AF(m+1));
set c = primrec(0 const A(m,1), (AS.m)*<:<*2 proj 2*>:>, 1);
set D = 1-tuples_on dom(AF(m+1));
A1: dom f = D by Def4;
then
A2: dom f = 1-tuples_on NAT by FUNCT_2:def 1;
set f1 = 0 const A(m,1);
set f2 = (AS.m)*<:<*2 proj 2*>:>;
arity f2 = 0+2 by Th35;
then
dom primrec(f1,f2,1) = (arity f1+1)-tuples_on NAT by COMPUT_1:57;
hence dom f = dom c by A1,FUNCT_2:def 1;
let x be object;
assume x in dom f;
then consider n being set such that
A3: n in NAT and
A4: x = <*n*> by A2,FINSEQ_2:135;
reconsider n as Element of NAT by A3;
dom AF(m+1) = NAT by FUNCT_2:def 1;
hence f.x = AF(m+1).n by A4,Def4
.= A(m+1,n) by Def3
.= AS.(m+1).<*n*> by Th36
.= c.x by A4,Def13;
end;
theorem Th39:
dom2tuple(AckermannFunction(m)) = AckermannSequence.m
proof
per cases by NAT_1:6;
suppose m = 0;
hence thesis by Def13,Th37;
end;
suppose ex a being Nat st m = a+1;
then consider a being Nat such that
A1: m = a+1;
dom2tuple(AF(a+1)) =
primrec(0 const A(a,1), (AS.a)*<:<*2 proj 2*>:>, 1) by Th38;
hence thesis by A1,Def13;
end;
end;
registration
let m;
cluster dom2tuple(AckermannFunction(m)) -> primitive-recursive;
coherence
proof
dom2tuple(AckermannFunction(m)) = AckermannSequence.m by Th39;
hence thesis;
end;
end;
registration
let k be Nat;
cluster k-ary for homogeneous to-naturals NAT*-defined Function;
existence
proof
take k const 0;
thus thesis;
end;
end;
definition
let f be BinOp of NAT;
let g be to-naturals Function;
pred f majorizes g means
ex N being Element of NAT st
for F being non empty FinSequence of NAT st F in dom g
for a being Element of NAT st a = max rng F
holds g.F < f.(N,a);
end;
theorem Th40:
for f being BinOp of NAT holds not f majorizes dom2tuple(f)
proof
let f be BinOp of NAT;
set g = dom2tuple(f);
given N being Element of NAT such that
A1: for F being non empty FinSequence of NAT st F in dom g
for a being Element of NAT st a = max rng F
holds g.F < f.(N,a);
reconsider H = <*N,N*> as non empty FinSequence of NAT;
rng H = {N,N} by FINSEQ_2:127;
then
A2: max rng H = max(N,N) by XXREAL_2:12
.= N;
dom g = 2-tuples_on NAT by Def5;
then
A3: g.H < f.(N,N) by A1,A2,FINSEQ_2:101;
dom f = [:NAT,NAT:] by FUNCT_2:def 1;
then [N,N] in dom f by ZFMISC_1:87;
hence contradiction by A3,Def5;
end;
definition
let f be BinOp of NAT;
func majorizedBy(f) -> Subset of HFuncs(NAT) equals
{ g where g is homogeneous to-naturals NAT*-defined Function:
f majorizes g };
coherence
proof
set X = {g where g is homogeneous to-naturals NAT*-defined Function:
f majorizes g};
X c= HFuncs(NAT)
proof
let x be object;
assume x in X;
then consider g being homogeneous to-naturals NAT*-defined Function
such that
A1: x = g and f majorizes g;
g is Element of HFuncs(NAT) by COMPUT_1:28;
hence thesis by A1;
end;
hence thesis;
end;
end;
theorem Th41:
for g being homogeneous to-naturals NAT*-defined Function
st arity g = 0 holds AckermannFunction majorizes g
proof
let g be homogeneous to-naturals NAT*-defined Function such that
A1: arity g = 0;
take N = 0;
let F be non empty FinSequence of NAT such that
A2: F in dom g;
let a be Element of NAT such that a = max rng F;
len F = 0 by A1,A2,MARGREL1:def 25;
hence thesis;
end;
theorem Th42:
for G being FinSequence of HFuncs NAT
st rng G c= majorizedBy(AckermannFunction)
ex N being Element of NAT st
for g being homogeneous to-naturals NAT*-defined Function st g in rng G
for F being non empty FinSequence of NAT st F in dom g
for a being Element of NAT st a = max rng F holds g.F < Ackermann(N,a)
proof
defpred P[Nat] means
for G being FinSequence of HFuncs NAT
st len G = $1 & rng G c= majorizedBy(AckermannFunction)
holds
ex N being Element of NAT st
for g being homogeneous to-naturals NAT*-defined Function st g in rng G
for F being non empty FinSequence of NAT st F in dom g
for a being Element of NAT st a = max rng F holds g.F < Ackermann(N,a);
A1: P[0]
proof
let G be FinSequence of HFuncs NAT such that
A2: len G = 0 and
rng G c= majorizedBy(AckermannFunction);
take N = 0;
let g be homogeneous to-naturals NAT*-defined Function such that
A3: g in rng G;
G = {} by A2;
hence thesis by A3;
end;
A4: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A5: P[k];
let G be FinSequence of HFuncs NAT such that
A6: len G = k+1 and
A7: rng G c= majorizedBy(AckermannFunction);
reconsider Pfx = G | Seg k as FinSequence of HFuncs NAT by FINSEQ_1:18;
A8: len Pfx = k by A6,FINSEQ_3:53;
rng Pfx c= rng G by RELAT_1:70;
then consider N1 being Element of NAT such that
A9: for g being homogeneous to-naturals NAT*-defined Function st g in rng Pfx
for F being non empty FinSequence of NAT st F in dom g
for a being Element of NAT st a = max rng F holds g.F < Ackermann(N1,a)
by A5,A8,A7,XBOOLE_1:1;
1 <= k+1 by NAT_1:11;
then k+1 in dom G by A6,FINSEQ_3:25;
then G.(k+1) in rng G by FUNCT_1:def 3;
then G.(k+1) in majorizedBy(AckermannFunction) by A7;
then consider gx being homogeneous to-naturals NAT*-defined Function
such that
A10: G.(k+1) = gx and
A11: AF majorizes gx;
consider N2 being Element of NAT such that
A12: for F being non empty FinSequence of NAT st F in dom gx
for a being Element of NAT st a = max rng F holds gx.F < AF.(N2,a)
by A11;
take N = max(N1,N2);
let g be homogeneous to-naturals NAT*-defined Function such that
A13: g in rng G;
let F be non empty FinSequence of NAT such that
A14: F in dom g;
let a be Element of NAT such that
A15: a = max rng F;
consider j being object such that
A16: j in dom G and
A17: G.j = g by A13,FUNCT_1:def 3;
reconsider j as Nat by A16;
dom G = Seg(k+1) by A6,FINSEQ_1:def 3;
then
A18: 1 <= j & j <= k+1 by A16,FINSEQ_1:1;
per cases;
suppose j <= k;
then
A19: j in Seg k by A18,FINSEQ_1:1;
then
A20: j in dom Pfx by A6,FINSEQ_3:54;
(G | Seg k).j = G.j by A19,FUNCT_1:49;
then
A21: g in rng Pfx by A17,A20,FUNCT_1:def 3;
A(N1,a) <= A(N,a) by XXREAL_0:25,Th24;
hence thesis by A9,A14,A15,A21,XXREAL_0:2;
end;
suppose
not j <= k;
then k+1 <= j by NAT_1:13;
then
A22: j = k+1 by A18,XXREAL_0:1;
A(N2,a) <= A(N,a) by XXREAL_0:25,Th24;
hence thesis by A10,A12,A14,A15,A17,A22,XXREAL_0:2;
end;
end;
let G be FinSequence of HFuncs NAT such that
A23: rng G c= majorizedBy(AckermannFunction);
for k being Nat holds P[k] from NAT_1:sch 2(A1,A4);
then P[len G];
hence thesis by A23;
end;
theorem Th43:
AckermannFunction majorizes m const n
proof
set g = m const n;
take N = n+1;
let F be non empty FinSequence of NAT such that
A1: F in dom g;
let a be Element of NAT such that a = max rng F;
n < n+1 by NAT_1:13;
then n < A(n+1,a) by Th20,XXREAL_0:2;
hence g.F < AF.(N,a) by A1,FUNCOP_1:7;
end;
theorem Th44:
m const n in majorizedBy(AckermannFunction)
proof
AF majorizes m const n by Th43;
hence thesis;
end;
theorem Th45:
m const n1 = m const n2 implies n1 = n2
proof
set x = the Element of m-tuples_on NAT;
(m const n1).x = n1 & (m const n2).x = n2;
hence thesis;
end;
theorem
1 <= n1 <= m & 1 <= n2 <= m & m succ n1 = m succ n2 implies n1 = n2
proof
assume that
A1: 1 <= n1 <= m and
A2: 1 <= n2 <= m and
A3: m succ n1 = m succ n2;
set x = idseq m;
x is Element of m-tuples_on NAT by FINSEQ_2:111;
then
A4: (m succ n1).x = x.n1+1 & (m succ n2).x = x.n2+1 by COMPUT_1:def 7;
n1 in Seg m by A1,FINSEQ_1:1;
then
A5: x.n1 = n1 by FINSEQ_2:49;
n2 in Seg m by A2,FINSEQ_1:1;
hence thesis by A3,A4,A5,FINSEQ_2:49;
end;
theorem
1 <= n1 <= m & 1 <= n2 <= m & m proj n1 = m proj n2 implies n1 = n2
proof
assume that
A1: 1 <= n1 <= m and
A2: 1 <= n2 <= m and
A3: m proj n1 = m proj n2;
set x = idseq m;
x is Element of m-tuples_on NAT by FINSEQ_2:111;
then
A4: (m proj n1).x = x.n1 & (m proj n2).x = x.n2 by COMPUT_1:38;
n1 in Seg m by A1,FINSEQ_1:1;
then
A5: x.n1 = n1 by FINSEQ_2:49;
n2 in Seg m by A2,FINSEQ_1:1;
hence thesis by A3,A4,A5,FINSEQ_2:49;
end;
definition
let m be Nat;
func constF(m) -> Function of NAT,HFuncs NAT means :Def16:
for n being Nat holds it.n = m const n;
existence
proof
deffunc F(Nat) = In(m const $1,HFuncs NAT);
consider f being Function of NAT,HFuncs NAT such that
A1: for n being Element of NAT holds f.n = F(n) from FUNCT_2:sch 4;
take f;
let n be Nat;
n in NAT by ORDINAL1:def 12;
hence f.n = F(n) by A1
.= m const n by COMPUT_1:31,SUBSET_1:def 8;
end;
uniqueness
proof
let f,g be Function of NAT,HFuncs NAT such that
A2: for n being Nat holds f.n = m const n and
A3: for n being Nat holds g.n = m const n;
let n be Element of NAT;
thus f.n = m const n by A2
.= g.n by A3;
end;
end;
registration
let m;
cluster constF(m) -> one-to-one;
coherence
proof
set f = constF(m);
for x1,x2 being object st x1 in NAT & x2 in NAT & f.x1 = f.x2 holds x1 = x2
proof
let x1,x2 be object;
assume that
A1: x1 in NAT & x2 in NAT and
A2: f.x1 = f.x2;
reconsider x1,x2 as Element of NAT by A1;
A3: f.x1 = m const x1 by Def16;
f.x2 = m const x2 by Def16;
hence thesis by A2,A3,Th45;
end;
hence thesis by FUNCT_2:19;
end;
end;
theorem Th48:
rng constF(m) c= PrimRec
proof
set f = constF(m);
let y be object;
assume y in rng f;
then consider x being Element of NAT such that
A1: f.x = y by FUNCT_2:113;
f.x = m const x by Def16;
hence thesis by A1,COMPUT_1:69;
end;
registration
cluster PrimRec -> infinite;
coherence
proof
A1: dom constF(0) = NAT by FUNCT_2:def 1;
rng constF(0) c= PrimRec by Th48;
hence thesis by A1,CARD_1:59;
end;
end;
theorem Th49:
1 <= n <= m implies AckermannFunction majorizes m succ n
proof
assume
A1: 1 <= n & n <= m;
set g = m succ n;
take N = n+1;
let F be non empty FinSequence of NAT such that
A2: F in dom g;
let a be Element of NAT such that
A3: a = max rng F;
A4: dom g = m-tuples_on NAT by COMPUT_1:def 7;
then
A5: g.F = (F.n)+1 by A2,COMPUT_1:def 7;
len F = m by A2,A4,FINSEQ_2:132;
then n in dom F by A1,FINSEQ_3:25;
then F.n in rng F by FUNCT_1:def 3;
then F.n <= a by A3,XXREAL_2:def 8;
then
A6: (F.n)+1 <= a+1 by XREAL_1:6;
a+1 < a+2 by XREAL_1:6;
then (F.n)+1 < a+2 by A6,XXREAL_0:2;
then
A7: g.F < A(1,a) by A5,Th9;
A(1,a) <= A(N,a) by Th24,NAT_1:11;
hence g.F < AF.(N,a) by A7,XXREAL_0:2;
end;
theorem Th50:
1 <= n <= m implies m succ n in majorizedBy(AckermannFunction)
proof
assume 1 <= n & n <= m;
then AF majorizes m succ n by Th49;
hence thesis;
end;
theorem Th51:
1 <= n <= m implies AckermannFunction majorizes m proj n
proof
assume
A1: 1 <= n & n <= m;
set g = m proj n;
take N = n+1;
let F be non empty FinSequence of NAT such that
A2: F in dom g;
let a be Element of NAT such that
A3: a = max rng F;
A4: dom g = m-tuples_on NAT by COMPUT_1:36;
then
A5: g.F = F.n by A2,COMPUT_1:38;
len F = m by A2,A4,FINSEQ_2:132;
then n in dom F by A1,FINSEQ_3:25;
then F.n in rng F by FUNCT_1:def 3;
then
A6: F.n <= a by A3,XXREAL_2:def 8;
A(0,a) <= A(N,a) by Th24;
hence g.F < AF.(N,a) by A6,A5,Th16,XXREAL_0:2;
end;
theorem Th52:
1 <= n <= m implies m proj n in majorizedBy(AckermannFunction)
proof
assume 1 <= n & n <= m;
then AF majorizes m proj n by Th51;
hence thesis;
end;
registration
cluster majorizedBy(AckermannFunction) -> composition_closed;
coherence
proof
let h be Element of HFuncs(NAT);
let G be with_the_same_arity FinSequence of HFuncs(NAT) such that
A1: h in majorizedBy(AckermannFunction) and
A2: arity h = len G and
A3: rng G c= majorizedBy(AckermannFunction);
reconsider hG0 = h*<:G:> as Element of HFuncs NAT by COMPUT_1:42;
reconsider hG = hG0 as homogeneous to-naturals NAT*-defined Function;
per cases;
suppose arity h = 0;
then arity G = 0 by A2,COMPUT_1:26;
then
A4: dom hG c= 0-tuples_on NAT by COMPUT_1:42;
per cases;
suppose hG is empty;
then AF majorizes hG by Th41,COMPUT_1:18;
hence thesis;
end;
suppose
A5: hG is non empty;
consider x being object such that
A6: x in dom hG by A5,XBOOLE_0:def 1;
dom hG c= (arity hG)-tuples_on NAT by COMPUT_1:21;
then reconsider x1 = x as Element of (arity hG)-tuples_on NAT
by A6;
reconsider x0 = x as Element of 0-tuples_on NAT by A4,A6;
arity hG = len x1 by CARD_1:def 7
.= len x0
.= 0;
then AF majorizes hG by Th41;
hence thesis;
end;
end;
suppose
A7: arity h <> 0;
consider h1 being homogeneous to-naturals NAT*-defined Function such that
A8: h = h1 and
A9: AF majorizes h1 by A1;
consider Nh being Element of NAT such that
A10: for F being non empty FinSequence of NAT st F in dom h1
for a being Element of NAT st a = max rng F holds h1.F < AF.(Nh,a)
by A9;
consider Ng being Element of NAT such that
A11: for g being homogeneous to-naturals NAT*-defined Function st g in rng G
for F being non empty FinSequence of NAT st F in dom g
for a being Element of NAT st a = max rng F
holds g.F < Ackermann(Ng,a)
by A3,Th42;
AF majorizes hG
proof
take N = Nh+Ng+2;
let F be non empty FinSequence of NAT such that
A12: F in dom hG;
let a be Element of NAT such that
A13: a = max rng F;
reconsider GF = G as Function-yielding Function;
set Y = <:GF:>.F;
A14: F in dom <:GF:> & Y in dom h by A12,FUNCT_1:11;
then reconsider Y as FinSequence of NAT by FINSEQ_1:def 11;
arity h = len Y by A14,MARGREL1:def 25;
then reconsider Y as non empty FinSequence of NAT by A7;
A15: max rng Y in rng Y by XXREAL_2:def 8;
reconsider b = max rng Y as Element of NAT by A15;
consider i being object such that
A16: i in dom Y and
A17: Y.i = b by A15,FUNCT_1:def 3;
A18: Y in rng <:GF:> by A14,FUNCT_1:def 3;
rng <:GF:> c= product rngs GF by FUNCT_6:29;
then dom Y = dom rngs GF by A18,CARD_3:9;
then
A19: dom Y = dom G by FUNCT_6:60;
reconsider i as Nat by A16;
reconsider Gi0 = G.i as Element of HFuncs NAT by A16,A19,FINSEQ_2:11;
reconsider Gi = Gi0 as homogeneous to-naturals NAT*-defined Function;
A20: Gi in rng G by A16,A19,FUNCT_1:def 3;
A21: F in dom Gi by A14,A20,FUNCT_6:32;
Y.i = Gi.F by A14,A16,A19,FUNCT_6:34;
then A(Nh,b) < A(Nh,A(Ng,a)) by A17,A11,A13,A20,A21,Th18;
then h1.Y < A(Nh,A(Ng,a)) by A8,A10,A14,XXREAL_0:2;
then h1.Y < A(N,a) by Th25,XXREAL_0:2;
hence hG.F < AF.(N,a) by A8,A12,FUNCT_1:12;
end;
hence thesis;
end;
end;
end;
registration
cluster majorizedBy(AckermannFunction) -> primitive-recursion_closed;
coherence
proof
let g,f1,f2 be Element of HFuncs NAT;
let i be Nat such that
A1: g is_primitive-recursively_expressed_by f1,f2,i and
A2: f1 in majorizedBy(AckermannFunction) and
A3: f2 in majorizedBy(AckermannFunction);
reconsider g0 = g, f10 = f1, f20 = f2 as
homogeneous to-naturals NAT*-defined Function;
per cases;
suppose f1 = {};
then g = {} by A1,COMPUT_1:67;
then AF majorizes g by Th41,COMPUT_1:18;
hence thesis;
end;
suppose
A4: f1 <> {};
consider n being Element of NAT such that
A5: dom g0 c= n-tuples_on NAT and
A6: 1 <= i and
A7: i <= n and
arity f10+1 = n and
n+1 = arity f20 and
A8: for p being FinSequence of NAT st len p = n holds
(p+*(i,0) in dom g iff Del(p,i) in dom f1) &
(p+*(i,0) in dom g implies g.(p+*(i,0)) = f1.Del(p,i)) &
for m being Nat holds
(p+*(i,m+1) in dom g iff
p+*(i,m) in dom g & (p+*(i,m)) ^ <*g.(p+*(i,m))*> in dom f2) &
(p+*(i,m+1) in dom g implies
g.(p+*(i,m+1)) = f2.((p+*(i,m)) ^ <*g.(p+*(i,m))*>))
by A1,COMPUT_1:def 9;
consider f1m being
homogeneous to-naturals NAT*-defined Function such that
A9: f1 = f1m and
A10: AF majorizes f1m by A2;
consider f2m being homogeneous to-naturals NAT*-defined Function
such that
A11: f2 = f2m and
A12: AF majorizes f2m by A3;
consider N1 being Element of NAT such that
A13: for F being non empty FinSequence of NAT st F in dom f1m
for a being Element of NAT st a = max rng F holds f1m.F < AF.(N1,a)
by A10;
consider N2 being Element of NAT such that
A14: for F being non empty FinSequence of NAT st F in dom f2m
for a being Element of NAT st a = max rng F holds f2m.F < AF.(N2,a)
by A12;
ex C being Element of NAT st
(arity f10 = 0 implies {} in dom f10 & C = f10.{}) &
(arity f10 <> 0 implies C = 0)
proof
per cases;
suppose
A15: arity f10 = 0;
consider x being object such that
A16: x in dom f10 by A4,XBOOLE_0:def 1;
reconsider x as FinSequence of NAT by A16,FINSEQ_1:def 11;
len x = 0 by A15,A16,MARGREL1:def 25;
then
A17: x = {};
then
f10.{} in rng f10 by A16,FUNCT_1:def 3;
then reconsider c = f10.{} as Element of NAT;
take c;
thus thesis by A15,A16,A17;
end;
suppose
A18: arity f10 <> 0;
take 0;
thus thesis by A18;
end;
end;
then consider C being Element of NAT such that
A19: arity f10 = 0 implies {} in dom f10 & C = f10.{} and
arity f10 <> 0 implies C = 0;
set M = max(max(N1,N2),C);
set R = M+5;
set S = R+1;
A20: N1 <= max(N1,N2) by XXREAL_0:25;
A21: max(N1,N2) <= M by XXREAL_0:25;
A22: N1 <= M by A20,A21,XXREAL_0:2;
A23: N2 <= max(N1,N2) by XXREAL_0:25;
max(N1,N2) <= M by XXREAL_0:25;
then N2 <= M by A23,XXREAL_0:2;
then
A24: N2 < R by NAT_1:16,XXREAL_0:2;
A25: C <= M by XXREAL_0:25;
N1 <= R by A22,NAT_1:16,XXREAL_0:2;
then
A26: N1 <= S by NAT_1:12;
C < R by A25,NAT_1:16,XXREAL_0:2;
then
A27: C < S by NAT_1:13;
AF majorizes g0
proof
take N = S+4;
let F be non empty FinSequence of NAT such that
A28: F in dom g0;
let a be Element of NAT such that
A29: a = max rng F;
defpred P[Nat] means
for p being FinSequence of NAT st len p = n &
(for x being Nat st x in rng p holds x <= a) &
p+*(i,$1) in dom g0
holds g0.(p+*(i,$1)) < A(S,a+$1);
A30: P[0]
proof
let p be FinSequence of NAT such that
A31: len p = n and
A32: for x being Nat st x in rng p holds x <= a and
A33: p+*(i,0) in dom g0;
A34: (p+*(i,0) in dom g0 iff Del(p,i) in dom f10) &
(p+*(i,0) in dom g0 implies g0.(p+*(i,0)) = f10.Del(p,i))
by A8,A31;
reconsider D = Del(p,i) as FinSequence of NAT by FINSEQ_3:105;
per cases;
suppose
A35: D = {};
len D = arity f10 by A33,A34,MARGREL1:def 25;
hence thesis by A27,A19,A34,A35,XXREAL_0:2,Th20;
end;
suppose D <> {};
then reconsider D as non empty FinSequence of NAT;
A36: max rng D in rng D by XXREAL_2:def 8;
then reconsider d = max rng D as Element of NAT;
rng D c= rng p by FINSEQ_3:106;
then A(N1,d) <= A(N1,a) by A32,A36,Th19;
then
A37: f1m.D < A(N1,a) by A9,A13,A33,A34,XXREAL_0:2;
A(N1,a) <= A(S,a) by A26,Th24;
hence thesis by A9,A33,A34,A37,XXREAL_0:2;
end;
end;
A38: for m being Nat st P[m] holds P[m+1]
proof
let m be Nat such that
A39: P[m];
let p be FinSequence of NAT such that
A40: len p = n and
A41: for x being Nat st x in rng p holds x <= a and
A42: p+*(i,m+1) in dom g0;
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
A43: p+*(i,mm) in dom g0 by A8,A40,A42;
reconsider U = p+*(i,mm) as FinSequence of NAT;
reconsider v = g.U as Element of NAT by A43,PARTFUN1:4;
reconsider W = U ^ <* v *> as non empty FinSequence of NAT;
A44: W in dom f20 by A42,A8,A40;
A45: g0.U < A(S,a+m) by A39,A40,A41,A43;
A46: max rng W in rng W by XXREAL_2:def 8;
then reconsider b = max rng W as Element of NAT;
A47: b < A(S,a+m)
proof
A48: rng W = rng U \/ rng <*v*> by FINSEQ_1:31;
per cases by A46,A48,XBOOLE_0:def 3;
suppose
A49: b in rng U;
rng U c= rng p \/ {m} by FUNCT_7:100;
then b in rng p or b in {m} by A49,XBOOLE_0:def 3;
then
A50: b <= a or b = m by A41,TARSKI:def 1;
a <= a+m by NAT_1:11;
then b <= a+m by A50,XXREAL_0:2,NAT_1:11;
hence thesis by Th16,XXREAL_0:2;
end;
suppose
A51: b in rng <*v*>;
rng <*v*> = {v} by FINSEQ_1:38;
hence thesis by A45,A51,TARSKI:def 1;
end;
end;
A(N2,b) < A(N2,A(S,a+m)) by A47,Th18;
then
A52: f2m.W < A(N2,A(S,a+m)) by A14,A11,A44,XXREAL_0:2;
A(N2,A(S,a+m)) < A(R,A(S,a+m)) by A24,Th23;
then
A53: f2m.W < A(R,A(S,a+m)) by A52,XXREAL_0:2;
A(R,A(S,a+m)) = A(S,a+m+1) by Th7
.= A(S,a+(m+1));
hence thesis by A11,A42,A8,A40,A53;
end;
A54: for m being Nat holds P[m] from NAT_1:sch 2(A30,A38);
A55: len F = n by A5,A28,CARD_1:def 7;
i in Seg n by A6,A7,FINSEQ_1:1;
then
A56: i in dom F by A55,FINSEQ_1:def 3;
then F.i in rng F by FUNCT_1:def 3;
then reconsider m = F.i as Element of NAT;
A57: for x being Nat st x in rng F holds x <= a by A29,XXREAL_2:def 8;
A58: F = F+*(i,m) by FUNCT_7:35;
m in rng F by A56,FUNCT_1:def 3;
then a+m <= a+a by A57,XREAL_1:6;
then A(S,a+m) <= A(S,a+a) by Th19;
then
A59: g0.F < A(S,a+a) by A28,A54,A55,A57,A58,XXREAL_0:2;
A(S,a+a) < A(S+4,a) by Th27;
hence g0.F < AF.(N,a) by A59,XXREAL_0:2;
end;
hence thesis;
end;
end;
end;
registration
cluster majorizedBy(AckermannFunction) -> primitive-recursively_closed;
coherence
proof
thus 0 const 0 in majorizedBy(AckermannFunction) by Th44;
thus 1 succ 1 in majorizedBy(AckermannFunction) by Th50;
thus for n,i being Nat st 1 <= i & i <= n holds
n proj i in majorizedBy(AckermannFunction) by Th52;
thus thesis;
end;
end;
theorem Th53:
PrimRec c= majorizedBy(AckermannFunction) by COMPUT_1:74;
registration
cluster majorizedBy(AckermannFunction) -> infinite;
coherence by Th53;
end;
theorem Th54:
dom2tuple(AckermannFunction) is non primitive-recursive
proof
set f = dom2tuple(AF);
assume not thesis;
then f in PrimRec by COMPUT_1:def 16;
then f in majorizedBy(AckermannFunction) by Th53;
then ex g being homogeneous to-naturals NAT*-defined Function st
g = f & AF majorizes g;
hence contradiction by Th40;
end;
theorem
not dom2tuple(AckermannFunction) in PrimRec by Th54;
theorem
for d being UnOp of NAT st for n being Nat holds d.n = Ackermann(n,n) holds
dom2tuple(d) is non primitive-recursive
proof
let d be UnOp of NAT such that
A1: for n being Nat holds d.n = Ackermann(n,n);
set g = dom2tuple(d);
assume not thesis;
then g in PrimRec by COMPUT_1:def 16;
then g in majorizedBy(AckermannFunction) by Th53;
then consider h being homogeneous to-naturals NAT*-defined Function
such that
A2: h = g and
A3: AckermannFunction majorizes h;
consider N being Element of NAT such that
A4: for F being non empty FinSequence of NAT st F in dom h
for a being Element of NAT st a = max rng F
holds h.F < AF.(N,a) by A3;
reconsider F = <*N*> as non empty FinSequence of NAT;
A5: dom d = NAT by FUNCT_2:def 1;
then
A6: dom g = 1-tuples_on NAT by Def4;
rng F = {N} by FINSEQ_1:38;
then
A7: max rng F = N by XXREAL_2:11;
g.F = d.N by A5,Def4
.= Ackermann(N,N) by A1;
hence contradiction by A2,A4,A6,A7,FINSEQ_2:98;
end;