let L be non trivial Polish-language; for E being Polish-arity-function of L
for D being non empty set
for g being Polish-recursion-function of E,D
for n being Nat ex J being Subset of (Polish-WFF-set (L,E)) ex H being Function of J,D st
( J = Polish-expression-hierarchy (L,E,n) & H is g -recursive )
let E be Polish-arity-function of L; for D being non empty set
for g being Polish-recursion-function of E,D
for n being Nat ex J being Subset of (Polish-WFF-set (L,E)) ex H being Function of J,D st
( J = Polish-expression-hierarchy (L,E,n) & H is g -recursive )
let D be non empty set ; for g being Polish-recursion-function of E,D
for n being Nat ex J being Subset of (Polish-WFF-set (L,E)) ex H being Function of J,D st
( J = Polish-expression-hierarchy (L,E,n) & H is g -recursive )
let g be Polish-recursion-function of E,D; for n being Nat ex J being Subset of (Polish-WFF-set (L,E)) ex H being Function of J,D st
( J = Polish-expression-hierarchy (L,E,n) & H is g -recursive )
defpred S1[ Nat] means ex J being Subset of (Polish-WFF-set (L,E)) ex H being Function of J,D st
( J = Polish-expression-hierarchy (L,E,$1) & H is g -recursive );
A1:
S1[ 0 ]
by Lm72;
A2:
for n being Nat st S1[n] holds
S1[n + 1]
by Lm75;
thus
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A2); verum