let n be Nat; :: thesis: Ackermann (1,n) = n + 2
defpred S₁[ Nat] means H₁(1,$1) = $1 + 2;
A1: S₁[ 0 ]

proof

thus H₁(1, 0 ) = H₁(1 - 1,1) by Def1
.= 1 + 1 by Def1
.= 0 + 2 ; :: thesis: verum

end;

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

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
thus H₁(1,k + 1) = H₁(1 - 1,H₁(1,(k + 1) - 1)) by Def1
.= H₁(1,k) + 1 by Def1
.= (k + 1) + 2 by A3 ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence Ackermann (1,n) = n + 2 ; :: thesis: verum