let m be Nat; for S being Language
for w2 being string of S
for U being non empty set
for phi1 being wff string of S
for I being Element of U -InterpretersOf S
for f being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN st dom f = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):] & phi1 is m -wff holds
( f -NorFunctor (I,((<*(TheNorSymbOf S)*> ^ phi1) ^ w2)) = 1 iff ( f . (I,phi1) = 0 & f . (I,w2) = 0 ) )
let S be Language; for w2 being string of S
for U being non empty set
for phi1 being wff string of S
for I being Element of U -InterpretersOf S
for f being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN st dom f = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):] & phi1 is m -wff holds
( f -NorFunctor (I,((<*(TheNorSymbOf S)*> ^ phi1) ^ w2)) = 1 iff ( f . (I,phi1) = 0 & f . (I,w2) = 0 ) )
let w2 be string of S; for U being non empty set
for phi1 being wff string of S
for I being Element of U -InterpretersOf S
for f being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN st dom f = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):] & phi1 is m -wff holds
( f -NorFunctor (I,((<*(TheNorSymbOf S)*> ^ phi1) ^ w2)) = 1 iff ( f . (I,phi1) = 0 & f . (I,w2) = 0 ) )
let U be non empty set ; for phi1 being wff string of S
for I being Element of U -InterpretersOf S
for f being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN st dom f = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):] & phi1 is m -wff holds
( f -NorFunctor (I,((<*(TheNorSymbOf S)*> ^ phi1) ^ w2)) = 1 iff ( f . (I,phi1) = 0 & f . (I,w2) = 0 ) )
let phi1 be wff string of S; for I being Element of U -InterpretersOf S
for f being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN st dom f = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):] & phi1 is m -wff holds
( f -NorFunctor (I,((<*(TheNorSymbOf S)*> ^ phi1) ^ w2)) = 1 iff ( f . (I,phi1) = 0 & f . (I,w2) = 0 ) )
let I be Element of U -InterpretersOf S; for f being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN st dom f = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):] & phi1 is m -wff holds
( f -NorFunctor (I,((<*(TheNorSymbOf S)*> ^ phi1) ^ w2)) = 1 iff ( f . (I,phi1) = 0 & f . (I,w2) = 0 ) )
set II = U -InterpretersOf S;
set SS = AllSymbolsOf S;
set N = TheNorSymbOf S;
set phi2 = w2;
set psi = (<*(TheNorSymbOf S)*> ^ phi1) ^ w2;
set FF = AllFormulasOf S;
set Phim = S -formulasOfMaxDepth m;
let f be PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN; ( dom f = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):] & phi1 is m -wff implies ( f -NorFunctor (I,((<*(TheNorSymbOf S)*> ^ phi1) ^ w2)) = 1 iff ( f . (I,phi1) = 0 & f . (I,w2) = 0 ) ) )
assume A1:
( dom f = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):] & phi1 is m -wff )
; ( f -NorFunctor (I,((<*(TheNorSymbOf S)*> ^ phi1) ^ w2)) = 1 iff ( f . (I,phi1) = 0 & f . (I,w2) = 0 ) )
set LH = f -NorFunctor (I,((<*(TheNorSymbOf S)*> ^ phi1) ^ w2));
set RH1 = f . (I,phi1);
set RH2 = f . (I,w2);
hereby ( f . (I,phi1) = 0 & f . (I,w2) = 0 implies f -NorFunctor (I,((<*(TheNorSymbOf S)*> ^ phi1) ^ w2)) = 1 )
assume
f -NorFunctor (
I,
((<*(TheNorSymbOf S)*> ^ phi1) ^ w2))
= 1
;
( f . (I,phi1) = 0 & f . (I,w2) = 0 )then consider w,
w1 being
string of
S such that A2:
(
[I,w] in dom f &
f . (
I,
w)
= FALSE &
f . (
I,
w1)
= FALSE &
(<*(TheNorSymbOf S)*> ^ phi1) ^ w2 = (<*(TheNorSymbOf S)*> ^ w) ^ w1 )
by Def17;
A3:
(
w in S -formulasOfMaxDepth m &
phi1 in S -formulasOfMaxDepth m )
by A1, A2, ZFMISC_1:87;
<*(TheNorSymbOf S)*> ^ (w ^ w1) =
(<*(TheNorSymbOf S)*> ^ phi1) ^ w2
by A2, FINSEQ_1:32
.=
<*(TheNorSymbOf S)*> ^ (phi1 ^ w2)
by FINSEQ_1:32
;
then
w ^ w1 = phi1 ^ w2
by FINSEQ_1:33;
hence
(
f . (
I,
phi1)
= 0 &
f . (
I,
w2)
= 0 )
by A2, FOMODEL0:def 19, A3;
verum
end;
assume
( f . (I,phi1) = 0 & f . (I,w2) = 0 )
; f -NorFunctor (I,((<*(TheNorSymbOf S)*> ^ phi1) ^ w2)) = 1
hence
f -NorFunctor (I,((<*(TheNorSymbOf S)*> ^ phi1) ^ w2)) = 1
by A1, ZFMISC_1:87, Def17; verum