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
set prd = PrimRec-Approximation ;
defpred S₂[ Element of NAT ] means for f being Element of HFuncs NAT st f in PrimRec-Approximation . $1 holds
f is quasi_total ;
A1: S₂[ 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 Def23;
then A2: ( 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 A2, TARSKI:def 2;

suppose f = 0 const 0 ; :: thesis: f is quasi_total

hence f is quasi_total by Th32; :: thesis: verum

end;

suppose f = 1 succ 1 ; :: thesis: f is quasi_total

hence f is quasi_total by Th32; :: thesis: verum

end;

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

then consider n, i being Element of NAT such that
A3: ( f = n proj i & 1 <= i & i <= n ) ;
thus f is quasi_total by A3, Th32; :: thesis: verum

end;

end;

end;

A4: for m being Element of NAT st S₂[m] holds
S₂[m + 1]

proof

let m be Element of NAT ; :: thesis: ( S₂[m] implies S₂[m + 1] )
assume A5: S₂[m] ; :: thesis: S₂[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 A6: f in (PR-closure (PrimRec-Approximation . m)) \/ (composition-closure (PrimRec-Approximation . m)) by Def23;

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

suppose A7: 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 A7, XBOOLE_0:def 3;

suppose f in PrimRec-Approximation . m ; :: thesis: f is quasi_total

hence f is quasi_total by A5; :: thesis: verum

end;

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
A8: f = g and
A9: 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
A10: ( f1 in PrimRec-Approximation . m & f2 in PrimRec-Approximation . m ) and
A11: g is_primitive-recursively_expressed_by f1,f2,i by A9;
( f1 is quasi_total & f2 is quasi_total ) by A5, A10;
hence f is quasi_total by A8, A11, Th72; :: thesis: verum

end;

end;

end;

end;

suppose A12: 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 A12, XBOOLE_0:def 3;

suppose f in PrimRec-Approximation . m ; :: thesis: f is quasi_total

hence f is quasi_total by A5; :: thesis: verum

end;

suppose 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 ) } ; :: thesis: f is quasi_total

then consider h being Element of HFuncs NAT , F being with_the_same_arity Element of (HFuncs NAT ) * such that
A13: ( f = h * <:F:> & h in PrimRec-Approximation . m & arity h = len F & rng F c= PrimRec-Approximation . m ) ;
A14: h is quasi_total by A5, A13;
for h being Element of HFuncs NAT st h in rng F holds
h is quasi_total by A5, A13;
hence f is quasi_total by A13, A14, Th50; :: thesis: verum

end;

end;

end;

end;

end;

end;

for m being Element of NAT holds S₂[m] from NAT_1:sch 1(A1, A4);
hence for f being Element of HFuncs NAT st f in PrimRec-Approximation . m holds
f is quasi_total ; :: thesis: verum