set PROJ = { (n proj i) where n, i is Element of NAT : ( 1 <= i & i <= n ) } ;
set prd = PrimRec-Approximation ;
set UP = Union PrimRec-Approximation;
A1:
dom PrimRec-Approximation = NAT
by FUNCT_2:def 1;
A2:
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;
0 const 0 in {(0 const 0),(1 succ 1)}
by TARSKI:def 2;
then
0 const 0 in PrimRec-Approximation . 0
by A2, XBOOLE_0:def 3;
hence
0 const 0 in Union PrimRec-Approximation
by A1, CARD_5:2; COMPUT_1:def 14 ( 1 succ 1 in Union PrimRec-Approximation & ( for n, i being Nat st 1 <= i & i <= n holds
n proj i in Union PrimRec-Approximation ) & Union PrimRec-Approximation is composition_closed & Union PrimRec-Approximation is primitive-recursion_closed )
1 succ 1 in {(0 const 0),(1 succ 1)}
by TARSKI:def 2;
then
1 succ 1 in PrimRec-Approximation . 0
by A2, XBOOLE_0:def 3;
hence
1 succ 1 in Union PrimRec-Approximation
by A1, CARD_5:2; ( ( for n, i being Nat st 1 <= i & i <= n holds
n proj i in Union PrimRec-Approximation ) & Union PrimRec-Approximation is composition_closed & Union PrimRec-Approximation is primitive-recursion_closed )
hereby COMPUT_1:def 12 Union PrimRec-Approximation is primitive-recursion_closed
deffunc H1(
Element of
NAT )
-> set =
{ (f * <:F:>) where f is Element of HFuncs NAT, F is with_the_same_arity Element of (HFuncs NAT) * : ( f in PrimRec-Approximation . $1 & arity f = len F & rng F c= PrimRec-Approximation . $1 ) } ;
let f be
Element of
HFuncs NAT;
for F being with_the_same_arity FinSequence of HFuncs NAT st f in Union PrimRec-Approximation & arity f = len F & rng F c= Union PrimRec-Approximation holds
b2 * <:b3:> in Union PrimRec-Approximationlet F be
with_the_same_arity FinSequence of
HFuncs NAT;
( f in Union PrimRec-Approximation & arity f = len F & rng F c= Union PrimRec-Approximation implies b1 * <:b2:> in Union PrimRec-Approximation )assume that A5:
f in Union PrimRec-Approximation
and A6:
arity f = len F
and A7:
rng F c= Union PrimRec-Approximation
;
b1 * <:b2:> in Union PrimRec-Approximationconsider kf being
object such that A8:
kf in dom PrimRec-Approximation
and A9:
f in PrimRec-Approximation . kf
by A5, CARD_5:2;
reconsider kf =
kf as
Element of
NAT by A8;
per cases
( arity f = 0 or arity f <> 0 )
;
suppose A11:
arity f <> 0
;
b1 * <:b2:> in Union PrimRec-Approximationdefpred S2[
object ,
object ]
means ex
k being
Element of
NAT st
(
F . $1
in PrimRec-Approximation . k & $2
= k );
A12:
for
x being
object st
x in Seg (len F) holds
ex
y being
Element of
NAT st
S2[
x,
y]
consider fKF being
Function of
(Seg (len F)),
NAT such that A15:
for
x being
object st
x in Seg (len F) holds
S2[
x,
fKF . x]
from MONOID_1:sch 1(A12);
set KF =
rng fKF;
reconsider KF =
rng fKF as non
empty finite Subset of
NAT by A6, A11, RELAT_1:def 19;
set K =
max KF;
set k =
max (
kf,
(max KF));
reconsider k =
max (
kf,
(max KF)) as
Element of
NAT by ORDINAL1:def 12;
A16:
dom fKF = Seg (len F)
by FUNCT_2:def 1;
A17:
rng F c= PrimRec-Approximation . k
A24:
F is
with_the_same_arity Element of
(HFuncs NAT) *
by FINSEQ_1:def 11;
PrimRec-Approximation . kf c= PrimRec-Approximation . k
by Th74, XXREAL_0:25;
then
f * <:F:> in H1(
k)
by A6, A9, A17, A24;
then
f * <:F:> in (PrimRec-Approximation . k) \/ H1(
k)
by XBOOLE_0:def 3;
then
f * <:F:> in (PR-closure (PrimRec-Approximation . k)) \/ (composition-closure (PrimRec-Approximation . k))
by XBOOLE_0:def 3;
then
f * <:F:> in PrimRec-Approximation . (k + 1)
by Def20;
hence
f * <:F:> in Union PrimRec-Approximation
by A1, CARD_5:2;
verum end;
end;
deffunc H1( Element of NAT ) -> set = { 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 . $1 & f2 in PrimRec-Approximation . $1 & g is_primitive-recursively_expressed_by f1,f2,i ) } ;
let g, f1, f2 be Element of HFuncs NAT; COMPUT_1:def 13 for i being Nat st g is_primitive-recursively_expressed_by f1,f2,i & f1 in Union PrimRec-Approximation & f2 in Union PrimRec-Approximation holds
g in Union PrimRec-Approximation
let i be Nat; ( g is_primitive-recursively_expressed_by f1,f2,i & f1 in Union PrimRec-Approximation & f2 in Union PrimRec-Approximation implies g in Union PrimRec-Approximation )
assume that
A25:
g is_primitive-recursively_expressed_by f1,f2,i
and
A26:
f1 in Union PrimRec-Approximation
and
A27:
f2 in Union PrimRec-Approximation
; g in Union PrimRec-Approximation
B1:
i in NAT
by ORDINAL1:def 12;
consider k2 being object such that
A28:
k2 in dom PrimRec-Approximation
and
A29:
f2 in PrimRec-Approximation . k2
by A27, CARD_5:2;
reconsider k2 = k2 as Element of NAT by A28;
consider k1 being object such that
A30:
k1 in dom PrimRec-Approximation
and
A31:
f1 in PrimRec-Approximation . k1
by A26, CARD_5:2;
reconsider k1 = k1 as Element of NAT by A30;