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
for J being Subset of (Polish-WFF-set (L,E))
for H being Function of J,D
for J1 being Subset of (Polish-WFF-set (L,E))
for H1 being Function of J1,D
for a being object st J = Polish-expression-hierarchy (L,E,n) & H is g -recursive & J c= J1 & H1 is g -recursive & a in J holds
H . a = H1 . a
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
for J being Subset of (Polish-WFF-set (L,E))
for H being Function of J,D
for J1 being Subset of (Polish-WFF-set (L,E))
for H1 being Function of J1,D
for a being object st J = Polish-expression-hierarchy (L,E,n) & H is g -recursive & J c= J1 & H1 is g -recursive & a in J holds
H . a = H1 . a
let D be non empty set ; for g being Polish-recursion-function of E,D
for n being Nat
for J being Subset of (Polish-WFF-set (L,E))
for H being Function of J,D
for J1 being Subset of (Polish-WFF-set (L,E))
for H1 being Function of J1,D
for a being object st J = Polish-expression-hierarchy (L,E,n) & H is g -recursive & J c= J1 & H1 is g -recursive & a in J holds
H . a = H1 . a
let g be Polish-recursion-function of E,D; for n being Nat
for J being Subset of (Polish-WFF-set (L,E))
for H being Function of J,D
for J1 being Subset of (Polish-WFF-set (L,E))
for H1 being Function of J1,D
for a being object st J = Polish-expression-hierarchy (L,E,n) & H is g -recursive & J c= J1 & H1 is g -recursive & a in J holds
H . a = H1 . a
let n be Nat; for J being Subset of (Polish-WFF-set (L,E))
for H being Function of J,D
for J1 being Subset of (Polish-WFF-set (L,E))
for H1 being Function of J1,D
for a being object st J = Polish-expression-hierarchy (L,E,n) & H is g -recursive & J c= J1 & H1 is g -recursive & a in J holds
H . a = H1 . a
let J be Subset of (Polish-WFF-set (L,E)); for H being Function of J,D
for J1 being Subset of (Polish-WFF-set (L,E))
for H1 being Function of J1,D
for a being object st J = Polish-expression-hierarchy (L,E,n) & H is g -recursive & J c= J1 & H1 is g -recursive & a in J holds
H . a = H1 . a
let H be Function of J,D; for J1 being Subset of (Polish-WFF-set (L,E))
for H1 being Function of J1,D
for a being object st J = Polish-expression-hierarchy (L,E,n) & H is g -recursive & J c= J1 & H1 is g -recursive & a in J holds
H . a = H1 . a
let J1 be Subset of (Polish-WFF-set (L,E)); for H1 being Function of J1,D
for a being object st J = Polish-expression-hierarchy (L,E,n) & H is g -recursive & J c= J1 & H1 is g -recursive & a in J holds
H . a = H1 . a
let H1 be Function of J1,D; for a being object st J = Polish-expression-hierarchy (L,E,n) & H is g -recursive & J c= J1 & H1 is g -recursive & a in J holds
H . a = H1 . a
let a be object ; ( J = Polish-expression-hierarchy (L,E,n) & H is g -recursive & J c= J1 & H1 is g -recursive & a in J implies H . a = H1 . a )
assume that
A1:
J = Polish-expression-hierarchy (L,E,n)
and
A2:
H is g -recursive
and
A3:
J c= J1
and
A4:
H1 is g -recursive
and
A5:
a in J
; H . a = H1 . a
defpred S1[ Nat] means for a being object st a in J & a in Polish-expression-hierarchy (L,E,$1) holds
H . a = H1 . a;
A10:
S1[ 0 ]
proof
let a be
object ;
( a in J & a in Polish-expression-hierarchy (L,E,0) implies H . a = H1 . a )
assume A11:
a in J
;
( not a in Polish-expression-hierarchy (L,E,0) or H . a = H1 . a )
then reconsider G =
a as
Polish-WFF of
L,
E ;
assume
a in Polish-expression-hierarchy (
L,
E,
0)
;
H . a = H1 . a
then A13:
a in Polish-atoms (
L,
E)
by TH22;
then
a in L
by Def9;
then
Polish-WFF-head G = G
by Th18;
then
Polish-arity G = 0
by A13, Def9;
then A15:
Polish-WFF-args G = {}
by Th51;
then A16:
rng (Polish-WFF-args G) c= J
;
A17:
rng (Polish-WFF-args G) c= J1
by A15;
thus H . a =
g . [(L -head G),(H * {})]
by A2, A11, A15, A16
.=
g . [(L -head G),(H1 * {})]
.=
H1 . a
by A3, A4, A11, A15, A17
;
verum
end;
A20:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A21:
S1[
k]
;
S1[k + 1]
set J2 =
Polish-expression-hierarchy (
L,
E,
k);
set J3 =
Polish-expression-hierarchy (
L,
E,
(k + 1));
let a be
object ;
( a in J & a in Polish-expression-hierarchy (L,E,(k + 1)) implies H . a = H1 . a )
assume A22:
a in J
;
( not a in Polish-expression-hierarchy (L,E,(k + 1)) or H . a = H1 . a )
assume A23:
a in Polish-expression-hierarchy (
L,
E,
(k + 1))
;
H . a = H1 . a
per cases
( n <= k or k < n )
;
suppose
k < n
;
H . a = H1 . athen
k + 1
<= n
by NAT_1:13;
then consider m being
Nat such that A30:
n = (k + 1) + m
by NAT_1:10;
A31:
Polish-expression-hierarchy (
L,
E,
(k + 1))
c= J
by A1, A30, Th34;
reconsider F1 =
a as
Polish-WFF of
L,
E by A22;
A32:
rng (Polish-WFF-args F1) c= Polish-expression-hierarchy (
L,
E,
k)
by A23, Th67;
Polish-expression-hierarchy (
L,
E,
k)
c= Polish-expression-hierarchy (
L,
E,
(k + 1))
by Th34;
then A33:
rng (Polish-WFF-args F1) c= J
by A31, A32;
then A34:
rng (Polish-WFF-args F1) c= J1
by A3;
for
b being
object st
b in rng (Polish-WFF-args F1) holds
H . b = H1 . b
by A21, A32, A33;
then A37:
H * (Polish-WFF-args F1) = H1 * (Polish-WFF-args F1)
by A33, A34, Th68;
thus H . a =
g . [(L -head F1),(H * (Polish-WFF-args F1))]
by A2, A22, A33
.=
H1 . a
by A3, A4, A22, A34, A37
;
verum end; end;
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(A10, A20);
hence
H . a = H1 . a
by A1, A5; verum