set prd = PrimRec-Approximation ;
defpred S2[ Nat] means PrimRec-Approximation . $1 c= PrimRec ;
A1: now :: thesis: for m being Nat st S2[m] holds
S2[m + 1]
let m be Nat; :: thesis: ( S2[m] implies S2[m + 1] )
assume A2: S2[m] ; :: thesis: S2[m + 1]
thus S2[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;
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;
end;
end;
end;
end;
end;
end;
A15: S2[ 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 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 S2[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