let L be non trivial Polish-language; :: thesis: for E being Polish-arity-function of L
for D being non empty set
for g being Polish-recursion-function of E,D ex J being Subset of (Polish-WFF-set (L,E)) ex H being Function of J,D st
( J = Polish-expression-hierarchy (L,E,0) & H is g -recursive )
let E be Polish-arity-function of L; :: thesis: for D being non empty set
for g being Polish-recursion-function of E,D ex J being Subset of (Polish-WFF-set (L,E)) ex H being Function of J,D st
( J = Polish-expression-hierarchy (L,E,0) & H is g -recursive )
let D be non empty set ; :: thesis: for g being Polish-recursion-function of E,D ex J being Subset of (Polish-WFF-set (L,E)) ex H being Function of J,D st
( J = Polish-expression-hierarchy (L,E,0) & H is g -recursive )
let g be Polish-recursion-function of E,D; :: thesis: ex J being Subset of (Polish-WFF-set (L,E)) ex H being Function of J,D st
( J = Polish-expression-hierarchy (L,E,0) & H is g -recursive )
deffunc H₁( object ) -> set = g . [$1,{}];
set J = Polish-expression-hierarchy (L,E,0);
reconsider J = Polish-expression-hierarchy (L,E,0) as Subset of (Polish-WFF-set (L,E)) by Th26;
A1: for a being object st a in J holds
H₁(a) in D

proof

let a be object ; :: thesis: ( a in J implies H₁(a) in D )
assume a in J ; :: thesis: H₁(a) in D
then A6: a in Polish-atoms (L,E) by Def9;
then reconsider t = a as Element of L by Def7;
set p = <*> D;
set b = [t,(<*> D)];
len (<*> D) = E . t by A6, Def7;
then [t,(<*> D)] in Polish-recursion-domain (E,D) ;
hence H₁(a) in D by FUNCT_2:5; :: thesis: verum

end;

consider H being Function of J,D such that
A9: for a being object st a in J holds
H . a = H₁(a) from FUNCT_2:sch 2(A1);
take J ; :: thesis: ex H being Function of J,D st
( J = Polish-expression-hierarchy (L,E,0) & H is g -recursive )
take H ; :: thesis: ( J = Polish-expression-hierarchy (L,E,0) & H is g -recursive )
thus J = Polish-expression-hierarchy (L,E,0) ; :: thesis: H is g -recursive
let F be Polish-WFF of L,E; :: according to POLNOT_1:def 43 :: thesis: ( F in J & rng (Polish-WFF-args F) c= J implies H . F = g . [(L -head F),(H * (Polish-WFF-args F))] )
assume that
A10: F in J and
rng (Polish-WFF-args F) c= J ; :: thesis: H . F = g . [(L -head F),(H * (Polish-WFF-args F))]
A12: F in Polish-atoms (L,E) by A10, Def9;
then F in L by Def7;
then A14: Polish-WFF-head F = F by Th53;
then Polish-arity F = 0 by A12, Def7;
then A15: Polish-WFF-args F = {} by Th61;
thus H . F = g . [(L -head F),{}] by A9, A10, A14
.= g . [(L -head F),(H * (Polish-WFF-args F))] by A15 ; :: thesis: verum