let m be Nat; for S being Language
for U being non empty set holds dom (NorIterator ((S,U) -TruthEval m)) = [:(U -InterpretersOf S),(m -NorFormulasOf S):]
let S be Language; for U being non empty set holds dom (NorIterator ((S,U) -TruthEval m)) = [:(U -InterpretersOf S),(m -NorFormulasOf S):]
let U be non empty set ; dom (NorIterator ((S,U) -TruthEval m)) = [:(U -InterpretersOf S),(m -NorFormulasOf S):]
set mm = m;
set II = U -InterpretersOf S;
set SS = AllSymbolsOf S;
set N = TheNorSymbOf S;
set Fm = (S,U) -TruthEval m;
set Phim = S -formulasOfMaxDepth m;
set IT = NorIterator ((S,U) -TruthEval m);
deffunc H1( FinSequence, FinSequence) -> set = (<*(TheNorSymbOf S)*> ^ $1) ^ $2;
defpred S1[] means verum;
set A = { H1(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S1[] } ;
set LH = dom (NorIterator ((S,U) -TruthEval m));
set RH = [:(U -InterpretersOf S), { H1(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S1[] } :];
(S,U) -TruthEval m is Element of Funcs ([:(U -InterpretersOf S),(S -formulasOfMaxDepth m):],BOOLEAN)
by Th8;
then reconsider Fmm = (S,U) -TruthEval m as Function of [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):],BOOLEAN ;
A1:
dom Fmm = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):]
by FUNCT_2:def 1;
reconsider ITT = NorIterator ((S,U) -TruthEval m) as PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN ;
A2:
[:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):] = { [x,y] where x is Element of U -InterpretersOf S, y is Element of ((AllSymbolsOf S) *) \ {{}} : verum }
by DOMAIN_1:19;
now for z being object st z in dom (NorIterator ((S,U) -TruthEval m)) holds
z in [:(U -InterpretersOf S), { H1(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S1[] } :]let z be
object ;
( z in dom (NorIterator ((S,U) -TruthEval m)) implies z in [:(U -InterpretersOf S), { H1(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S1[] } :] )assume A3:
z in dom (NorIterator ((S,U) -TruthEval m))
;
z in [:(U -InterpretersOf S), { H1(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S1[] } :]then
z in [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):]
;
then consider x being
Element of
U -InterpretersOf S,
y being
Element of
((AllSymbolsOf S) *) \ {{}} such that A4:
z = [x,y]
by A2;
consider phi1,
phi2 being
Element of
((AllSymbolsOf S) *) \ {{}} such that A5:
(
y = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 &
[x,phi1] in dom ((S,U) -TruthEval m) &
[x,phi2] in dom ((S,U) -TruthEval m) )
by Def18, A3, A4;
reconsider phi11 =
phi1,
phi22 =
phi2 as
Element of
S -formulasOfMaxDepth m by ZFMISC_1:87, A5, A1;
set yy =
H1(
phi11,
phi22);
(
x in U -InterpretersOf S &
H1(
phi11,
phi22)
in { H1(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S1[] } &
z = [x,H1(phi11,phi22)] )
by A4, A5;
hence
z in [:(U -InterpretersOf S), { H1(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S1[] } :]
by ZFMISC_1:def 2;
verum end;
then A6:
dom (NorIterator ((S,U) -TruthEval m)) c= [:(U -InterpretersOf S), { H1(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S1[] } :]
;
now for z being object st z in [:(U -InterpretersOf S), { H1(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S1[] } :] holds
z in dom (NorIterator ((S,U) -TruthEval m))let z be
object ;
( z in [:(U -InterpretersOf S), { H1(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S1[] } :] implies z in dom (NorIterator ((S,U) -TruthEval m)) )assume
z in [:(U -InterpretersOf S), { H1(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S1[] } :]
;
z in dom (NorIterator ((S,U) -TruthEval m))then consider xx,
yy being
object such that A7:
(
xx in U -InterpretersOf S &
yy in { H1(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S1[] } &
z = [xx,yy] )
by ZFMISC_1:def 2;
reconsider x =
xx as
Element of
U -InterpretersOf S by A7;
consider phi1,
phi2 being
Element of
S -formulasOfMaxDepth m such that A8:
yy = H1(
phi1,
phi2)
by A7;
reconsider phi11 =
phi1,
phi22 =
phi2 as
string of
S ;
(<*(TheNorSymbOf S)*> ^ phi11) ^ phi22 is
string of
S
;
then reconsider y =
yy as
string of
S by A8;
(
[x,phi1] in dom Fmm &
[x,phi2] in dom Fmm )
by A1;
then
[x,y] in dom (NorIterator ((S,U) -TruthEval m))
by A8, Def18;
hence
z in dom (NorIterator ((S,U) -TruthEval m))
by A7;
verum end;
then
[:(U -InterpretersOf S), { H1(phi1,phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : S1[] } :] c= dom (NorIterator ((S,U) -TruthEval m))
;
hence
dom (NorIterator ((S,U) -TruthEval m)) = [:(U -InterpretersOf S),(m -NorFormulasOf S):]
by A6; verum