let m be Element of NAT ; :: thesis: for f being Element of HFuncs NAT st f in PrimRec-Approximation . m holds
f is quasi_total
defpred S2[ Nat] means for f being Element of HFuncs NAT st f in PrimRec-Approximation . $1 holds
f is quasi_total ;
set prd = PrimRec-Approximation ;
A1: for m being Nat st S2[m] holds
S2[m + 1]
proof
let m be Nat; :: thesis: ( S2[m] implies S2[m + 1] )
assume A2: S2[m] ; :: thesis: S2[m + 1]
let f be Element of HFuncs NAT; :: thesis: ( f in PrimRec-Approximation . (m + 1) implies f is quasi_total )
assume f in PrimRec-Approximation . (m + 1) ; :: thesis: f is quasi_total
then A3: f in (PR-closure (PrimRec-Approximation . m)) \/ (composition-closure (PrimRec-Approximation . m)) by Def20;
per cases ( f in PR-closure (PrimRec-Approximation . m) or f in composition-closure (PrimRec-Approximation . m) ) by A3, XBOOLE_0:def 3;
suppose A4: f in PR-closure (PrimRec-Approximation . m) ; :: thesis: f is quasi_total
thus f is quasi_total :: thesis: verum
proof
per cases ( f in PrimRec-Approximation . m or f 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 A4, XBOOLE_0:def 3;
suppose f 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: f is quasi_total
then consider g being Element of HFuncs NAT such that
A5: f = g and
A6: 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 ) ;
consider f1, f2 being Element of HFuncs NAT, i being Element of NAT such that
A7: f1 in PrimRec-Approximation . m and
A8: f2 in PrimRec-Approximation . m and
A9: g is_primitive-recursively_expressed_by f1,f2,i by A6;
A10: f2 is quasi_total by A2, A8;
f1 is quasi_total by A2, A7;
hence f is quasi_total by A5, A9, A10, Th67; :: thesis: verum
end;
end;
end;
end;
suppose A11: f in composition-closure (PrimRec-Approximation . m) ; :: thesis: f is quasi_total
thus f is quasi_total :: thesis: verum
proof
per cases ( f in PrimRec-Approximation . m or f in { (h * <:F:>) where h is Element of HFuncs NAT, F is with_the_same_arity Element of (HFuncs NAT) * : ( h in PrimRec-Approximation . m & arity h = len F & rng F c= PrimRec-Approximation . m ) } ) by A11, XBOOLE_0:def 3;
end;
end;
end;
end;
end;
A17: S2[ 0 ]
proof
let f be Element of HFuncs NAT; :: thesis: ( f in PrimRec-Approximation . 0 implies f is quasi_total )
assume f in PrimRec-Approximation . 0 ; :: thesis: f is quasi_total
then f in initial-funcs by Def20;
then A18: ( f in {(0 const 0),(1 succ 1)} or f in { (n proj i) where n, i is Element of NAT : ( 1 <= i & i <= n ) } ) by XBOOLE_0:def 3;
per cases ( f = 0 const 0 or f = 1 succ 1 or f in { (n proj i) where n, i is Element of NAT : ( 1 <= i & i <= n ) } ) by A18, TARSKI:def 2;
suppose f in { (n proj i) where n, i is Element of NAT : ( 1 <= i & i <= n ) } ; :: thesis: f is quasi_total
then ex n, i being Element of NAT st
( f = n proj i & 1 <= i & i <= n ) ;
hence f is quasi_total by Th28; :: thesis: verum
end;
end;
end;
for m being Nat holds S2[m] from NAT_1:sch 2(A17, A1);
 hence for f being Element of HFuncs NAT st f in PrimRec-Approximation . m holds
f is quasi_total ; :: thesis: verum