let m, n be Nat; :: thesis: (AckermannSequence . m) . <*n*> = Ackermann (m,n)
defpred S₁[ Nat] means for n being Nat holds (AckermannSequence . $1) . <*n*> = H₁($1,n);
set p1 = 2 proj 2;
set g1 = <:<*(2 proj 2)*>:>;
A1: S₁[ 0 ]

proof

let m be Nat; :: thesis: (AckermannSequence . 0) . <*m*> = H₁( 0 ,m)
A2: AckermannSequence . 0 = 1 succ 1 by Def13;
defpred S₂[ Nat] means (AckermannSequence . 0) . <*$1*> = H₁( 0 ,$1);
A3: S₂[ 0 ]

proof

thus (AckermannSequence . 0) . <*0*> = (<*0*> . 1) + 1 by A2, Lm6, COMPUT_1:def 7
.= H₁( 0 , 0 ) by Def1 ; :: thesis: verum

end;

A4: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume S₂[k] ; :: thesis: S₂[k + 1]
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
<*(k1 + 1)*> in 1 -tuples_on NAT by FINSEQ_2:98;
hence (AckermannSequence . 0) . <*(k + 1)*> = (<*(k + 1)*> . 1) + 1 by A2, COMPUT_1:def 7
.= H₁( 0 ,k + 1) by Def1 ;
:: thesis: verum

end;

for k being Nat holds S₂[k] from NAT_1:sch 2(A3, A4);
hence (AckermannSequence . 0) . <*m*> = H₁( 0 ,m) ; :: thesis: verum

end;

A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]
A7: arity (0 const H₁(k,1)) = 0 ;
A8: AckermannSequence . (k + 1) = primrec ((0 const H₁(k,1)),((AckermannSequence . k) * <:<*(2 proj 2)*>:>),1) by Def13;
defpred S₂[ Nat] means (AckermannSequence . (k + 1)) . <*$1*> = H₁(k + 1,$1);
A9: S₂[ 0 ]

proof

thus (AckermannSequence . (k + 1)) . <*0*> = (0 const H₁(k,1)) . {} by A7, A8, COMPUT_1:80
.= H₁(k,1) by Lm7, FUNCOP_1:7
.= H₁(k + 1, 0 ) by Th6 ; :: thesis: verum

end;

A10: for w being Nat st S₂[w] holds
S₂[w + 1]

proof

let w be Nat; :: thesis: ( S₂[w] implies S₂[w + 1] )
assume A11: S₂[w] ; :: thesis: S₂[w + 1]
reconsider w1 = w as Element of NAT by ORDINAL1:def 12;
set f2 = (AckermannSequence . k) * <:<*(2 proj 2)*>:>;
set x2 = (primrec ((0 const H₁(k,1)),((AckermannSequence . k) * <:<*(2 proj 2)*>:>),1)) . <*w1*>;
set x = <*w1,((primrec ((0 const H₁(k,1)),((AckermannSequence . k) * <:<*(2 proj 2)*>:>),1)) . <*w1*>)*>;
A12: dom (2 proj 2) = 2 -tuples_on NAT by COMPUT_1:36;
A13: (primrec ((0 const H₁(k,1)),((AckermannSequence . k) * <:<*(2 proj 2)*>:>),1)) . <*w1*> in NAT by ORDINAL1:def 12;
then <*w1,((primrec ((0 const H₁(k,1)),((AckermannSequence . k) * <:<*(2 proj 2)*>:>),1)) . <*w1*>)*> in 2 -tuples_on NAT by FINSEQ_2:101;
then A14: (2 proj 2) . <*w1,((primrec ((0 const H₁(k,1)),((AckermannSequence . k) * <:<*(2 proj 2)*>:>),1)) . <*w1*>)*> = <*w1,((primrec ((0 const H₁(k,1)),((AckermannSequence . k) * <:<*(2 proj 2)*>:>),1)) . <*w1*>)*> . 2 by COMPUT_1:38;
A15: (primrec ((0 const H₁(k,1)),((AckermannSequence . k) * <:<*(2 proj 2)*>:>),1)) . <*w1*> = H₁(k + 1,w) by A11, Def13;
A16: dom <:<*(2 proj 2)*>:> = 2 -tuples_on NAT by A12, FINSEQ_3:141;
arity ((AckermannSequence . k) * <:<*(2 proj 2)*>:>) = 2 by Th35;
hence (AckermannSequence . (k + 1)) . <*(w + 1)*> = ((AckermannSequence . k) * <:<*(2 proj 2)*>:>) . <*w1,((primrec ((0 const H₁(k,1)),((AckermannSequence . k) * <:<*(2 proj 2)*>:>),1)) . <*w1*>)*> by A7, A8, COMPUT_1:82
.= (AckermannSequence . k) . (<:<*(2 proj 2)*>:> . <*w1,((primrec ((0 const H₁(k,1)),((AckermannSequence . k) * <:<*(2 proj 2)*>:>),1)) . <*w1*>)*>) by A13, A16, FINSEQ_2:101, FUNCT_1:13
.= (AckermannSequence . k) . <*((primrec ((0 const H₁(k,1)),((AckermannSequence . k) * <:<*(2 proj 2)*>:>),1)) . <*w1*>)*> by A12, A13, A14, FINSEQ_2:101, FINSEQ_3:141
.= H₁(k,(primrec ((0 const H₁(k,1)),((AckermannSequence . k) * <:<*(2 proj 2)*>:>),1)) . <*w1*>) by A6
.= H₁(k + 1,w + 1) by A15, Th7 ;
:: thesis: verum

end;

for k being Nat holds S₂[k] from NAT_1:sch 2(A9, A10);
hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A5);
hence (AckermannSequence . m) . <*n*> = Ackermann (m,n) ; :: thesis: verum