set prd = PrimRec-Approximation ;
defpred S₂[ Nat] means PrimRec-Approximation . $1 c= PrimRec ;

A1: now :: thesis: for m being Nat st S₂[m] holds
S₂[m + 1]

let m be Nat; :: thesis: ( S₂[m] implies S₂[m + 1] )
assume A2: S₂[m] ; :: thesis: S₂[m + 1]
thus S₂[m + 1] :: thesis: verum

proof

set mcocl = { (f * <:F:>) where f is Element of HFuncs NAT, F is with_the_same_arity Element of (HFuncs NAT) * : ( f in PrimRec-Approximation . m & arity f = len F & rng F c= PrimRec-Approximation . m ) } ;
set mprcl = { g where g is Element of HFuncs NAT : ex f1, f2 being Element of HFuncs NAT ex i being Element of NAT st
( f1 in PrimRec-Approximation . m & f2 in PrimRec-Approximation . m & g is_primitive-recursively_expressed_by f1,f2,i ) } ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in PrimRec-Approximation . (m + 1) or x in PrimRec )
A3: PrimRec-Approximation . (m + 1) = (PR-closure (PrimRec-Approximation . m)) \/ (composition-closure (PrimRec-Approximation . m)) by Def20;
assume A4: x in PrimRec-Approximation . (m + 1) ; :: thesis: x in PrimRec

per cases ( x in PR-closure (PrimRec-Approximation . m) or x in composition-closure (PrimRec-Approximation . m) ) by A4, A3, XBOOLE_0:def 3;

suppose A5: x in PR-closure (PrimRec-Approximation . m) ; :: thesis: x in PrimRec

thus x in PrimRec :: thesis: verum

proof

per cases ( x in PrimRec-Approximation . m or x in { g where g is Element of HFuncs NAT : ex f1, f2 being Element of HFuncs NAT ex i being Element of NAT st
( f1 in PrimRec-Approximation . m & f2 in PrimRec-Approximation . m & g is_primitive-recursively_expressed_by f1,f2,i ) } ) by A5, XBOOLE_0:def 3;

suppose x in PrimRec-Approximation . m ; :: thesis: x in PrimRec

hence x in PrimRec by A2; :: thesis: verum

end;

suppose A6: x in { g where g is Element of HFuncs NAT : ex f1, f2 being Element of HFuncs NAT ex i being Element of NAT st
( f1 in PrimRec-Approximation . m & f2 in PrimRec-Approximation . m & g is_primitive-recursively_expressed_by f1,f2,i ) } ; :: thesis: x in PrimRec

A7: PrimRec is primitive-recursion_closed by Def14;
ex g being Element of HFuncs NAT st
( x = g & ex f1, f2 being Element of HFuncs NAT ex i being Element of NAT st
( f1 in PrimRec-Approximation . m & f2 in PrimRec-Approximation . m & g is_primitive-recursively_expressed_by f1,f2,i ) ) by A6;
hence x in PrimRec by A2, A7; :: thesis: verum

end;

end;

end;

end;

suppose A8: x in composition-closure (PrimRec-Approximation . m) ; :: thesis: x in PrimRec

thus x in PrimRec :: thesis: verum

proof

per cases ( x in PrimRec-Approximation . m or x in { (f * <:F:>) where f is Element of HFuncs NAT, F is with_the_same_arity Element of (HFuncs NAT) * : ( f in PrimRec-Approximation . m & arity f = len F & rng F c= PrimRec-Approximation . m ) } ) by A8, XBOOLE_0:def 3;

suppose x in PrimRec-Approximation . m ; :: thesis: x in PrimRec

hence x in PrimRec by A2; :: thesis: verum

end;

suppose A9: x in { (f * <:F:>) where f is Element of HFuncs NAT, F is with_the_same_arity Element of (HFuncs NAT) * : ( f in PrimRec-Approximation . m & arity f = len F & rng F c= PrimRec-Approximation . m ) } ; :: thesis: x in PrimRec

A10: PrimRec is composition_closed by Def14;
consider f being Element of HFuncs NAT, F being with_the_same_arity Element of (HFuncs NAT) * such that
A11: x = f * <:F:> and
A12: f in PrimRec-Approximation . m and
A13: arity f = len F and
A14: rng F c= PrimRec-Approximation . m by A9;
rng F c= PrimRec by A2, A14, XBOOLE_1:1;
hence x in PrimRec by A2, A11, A12, A13, A10; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

A15: S₂[ 0 ]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in PrimRec-Approximation . 0 or x in PrimRec )
assume A16: x in PrimRec-Approximation . 0 ; :: thesis: x in PrimRec
PrimRec-Approximation . 0 = {(0 const 0),(1 succ 1)} \/ { (n proj i) where n, i is Element of NAT : ( 1 <= i & i <= n ) } by Def20;
then A17: ( x in {(0 const 0),(1 succ 1)} or x in { (n proj i) where n, i is Element of NAT : ( 1 <= i & i <= n ) } ) by A16, XBOOLE_0:def 3;

per cases ( x = 0 const 0 or x = 1 succ 1 or x in { (n proj i) where n, i is Element of NAT : ( 1 <= i & i <= n ) } ) by A17, TARSKI:def 2;

suppose x = 0 const 0 ; :: thesis: x in PrimRec

hence x in PrimRec by Def14; :: thesis: verum

end;

suppose x = 1 succ 1 ; :: thesis: x in PrimRec

hence x in PrimRec by Def14; :: thesis: verum

end;

suppose x in { (n proj i) where n, i is Element of NAT : ( 1 <= i & i <= n ) } ; :: thesis: x in PrimRec

then ex n, i being Element of NAT st
( x = n proj i & 1 <= i & i <= n ) ;
hence x in PrimRec by Def14; :: thesis: verum

end;

end;

end;

A18: for k being Nat holds S₂[k] from NAT_1:sch 2(A15, A1);
A19: Union PrimRec-Approximation c= PrimRec

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Union PrimRec-Approximation or x in PrimRec )
assume that
A20: x in Union PrimRec-Approximation and
A21: not x in PrimRec ; :: thesis: contradiction
consider X being set such that
A22: x in X and
A23: X in rng PrimRec-Approximation by A20, TARSKI:def 4;
consider m being object such that
A24: m in dom PrimRec-Approximation and
A25: PrimRec-Approximation . m = X by A23, FUNCT_1:def 3;
reconsider m = m as Element of NAT by A24;
PrimRec-Approximation . m c= PrimRec by A18;
hence contradiction by A21, A22, A25; :: thesis: verum

end;

PrimRec c= Union PrimRec-Approximation by Th73, Th75;
hence PrimRec = Union PrimRec-Approximation by A19, XBOOLE_0:def 10; :: thesis: verum