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 S₂[ Element of 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 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 A2: 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 A3: 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 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 PrimRec-Approximation . m ; :: thesis: f is quasi_total

hence f is quasi_total by A2; :: 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
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, Th72; :: 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;

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

hence f is quasi_total by A2; :: 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
A12: f = h * <:F:> and
A13: h in PrimRec-Approximation . m and
A14: arity h = len F and
A15: rng F c= PrimRec-Approximation . m ;
A16: for h being Element of HFuncs NAT st h in rng F holds
h is quasi_total by A2, A15;
h is quasi_total by A2, A13;
hence f is quasi_total by A12, A14, A16, Th50; :: thesis: verum

end;

end;

end;

end;

end;

end;

A17: 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 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 = 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 ex n, i being Element of NAT st
( f = n proj i & 1 <= i & i <= n ) ;
hence f is quasi_total by Th32; :: thesis: verum

end;

end;

end;

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