let U be non empty set ; for u1 being Element of U
for S being Language
for l1, l2 being literal Element of S
for psi being wff string of S st not l2 in rng psi holds
for I being Element of U -InterpretersOf S holds ((l1,u1) ReassignIn I) -TruthEval psi = ((l2,u1) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn psi)
let u1 be Element of U; for S being Language
for l1, l2 being literal Element of S
for psi being wff string of S st not l2 in rng psi holds
for I being Element of U -InterpretersOf S holds ((l1,u1) ReassignIn I) -TruthEval psi = ((l2,u1) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn psi)
let S be Language; for l1, l2 being literal Element of S
for psi being wff string of S st not l2 in rng psi holds
for I being Element of U -InterpretersOf S holds ((l1,u1) ReassignIn I) -TruthEval psi = ((l2,u1) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn psi)
let l1, l2 be literal Element of S; for psi being wff string of S st not l2 in rng psi holds
for I being Element of U -InterpretersOf S holds ((l1,u1) ReassignIn I) -TruthEval psi = ((l2,u1) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn psi)
let psi be wff string of S; ( not l2 in rng psi implies for I being Element of U -InterpretersOf S holds ((l1,u1) ReassignIn I) -TruthEval psi = ((l2,u1) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn psi) )
set II = U -InterpretersOf S;
set s = l1 SubstWith l2;
set SS = AllSymbolsOf S;
set SSS = (AllSymbolsOf S) \ {l2};
set TT = AllTermsOf S;
set T = S -termsOfMaxDepth ;
set F = S -firstChar ;
set N = TheNorSymbOf S;
reconsider SSSS = (AllSymbolsOf S) \ {l2} as non empty Subset of (AllSymbolsOf S) ;
defpred S1[ Nat] means for I being Element of U -InterpretersOf S
for u being Element of U
for phi being wff string of S st phi is $1 -wff & phi is (AllSymbolsOf S) \ {l2} -valued holds
((l1,u) ReassignIn I) -TruthEval phi = ((l2,u) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn phi);
A1:
S1[ 0 ]
proof
let I be
Element of
U -InterpretersOf S;
for u being Element of U
for phi being wff string of S st phi is 0 -wff & phi is (AllSymbolsOf S) \ {l2} -valued holds
((l1,u) ReassignIn I) -TruthEval phi = ((l2,u) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn phi)let u be
Element of
U;
for phi being wff string of S st phi is 0 -wff & phi is (AllSymbolsOf S) \ {l2} -valued holds
((l1,u) ReassignIn I) -TruthEval phi = ((l2,u) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn phi)let phi be
wff string of
S;
( phi is 0 -wff & phi is (AllSymbolsOf S) \ {l2} -valued implies ((l1,u) ReassignIn I) -TruthEval phi = ((l2,u) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn phi) )
set I1 = (
l1,
u)
ReassignIn I;
set I2 = (
l2,
u)
ReassignIn I;
assume
phi is
0 -wff
;
( not phi is (AllSymbolsOf S) \ {l2} -valued or ((l1,u) ReassignIn I) -TruthEval phi = ((l2,u) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn phi) )
then reconsider phi0 =
phi as
0wff string of
S ;
assume
phi is
(AllSymbolsOf S) \ {l2} -valued
;
((l1,u) ReassignIn I) -TruthEval phi = ((l2,u) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn phi)
then
((l1,u) ReassignIn I) -TruthEval phi0 = ((l2,u) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn phi0)
by Lm41;
hence
((l1,u) ReassignIn I) -TruthEval phi = ((l2,u) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn phi)
;
verum
end;
A2:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A3:
S1[
n]
;
S1[n + 1]
let I be
Element of
U -InterpretersOf S;
for u being Element of U
for phi being wff string of S st phi is n + 1 -wff & phi is (AllSymbolsOf S) \ {l2} -valued holds
((l1,u) ReassignIn I) -TruthEval phi = ((l2,u) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn phi)let u be
Element of
U;
for phi being wff string of S st phi is n + 1 -wff & phi is (AllSymbolsOf S) \ {l2} -valued holds
((l1,u) ReassignIn I) -TruthEval phi = ((l2,u) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn phi)let phi be
wff string of
S;
( phi is n + 1 -wff & phi is (AllSymbolsOf S) \ {l2} -valued implies ((l1,u) ReassignIn I) -TruthEval phi = ((l2,u) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn phi) )
set I1 = (
l1,
u)
ReassignIn I;
set I2 = (
l2,
u)
ReassignIn I;
assume A4:
(
phi is
n + 1
-wff &
phi is
(AllSymbolsOf S) \ {l2} -valued )
;
((l1,u) ReassignIn I) -TruthEval phi = ((l2,u) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn phi)
then reconsider phii =
phi as
n + 1
-wff string of
S ;
reconsider x =
phi as non
empty SSSS -valued FinSequence by A4;
{(x . 1)} \ ((AllSymbolsOf S) \ {l2}) = {}
;
then
phii . 1
in (AllSymbolsOf S) \ {l2}
by ZFMISC_1:60;
then
(S -firstChar) . phii in (AllSymbolsOf S) \ {l2}
by FOMODEL0:6;
then
not
(S -firstChar) . phii in {l2}
by XBOOLE_0:def 5;
then A5:
(S -firstChar) . phii <> l2
by TARSKI:def 1;
reconsider psi = (
l1,
l2)
-SymbolSubstIn phii as
n + 1
-wff string of
S ;
reconsider phi1 =
head phii as
n -wff string of
S ;
reconsider psi1 = (
l1,
l2)
-SymbolSubstIn phi1 as
n -wff string of
S ;
per cases
( ( phi is exal & not phi is 0wff ) or ( not phi is exal & not phi is 0wff ) or phi is 0 -wff )
;
suppose
(
phi is
exal & not
phi is
0wff )
;
((l1,u) ReassignIn I) -TruthEval phi = ((l2,u) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn phi)then reconsider phii =
phii as non
0wff n + 1
-wff exal string of
S ;
set l =
(S -firstChar) . phii;
set phi2 =
tail phii;
A6:
phii =
(<*((S -firstChar) . phii)*> ^ phi1) ^ (tail phii)
by FOMODEL2:23
.=
<*((S -firstChar) . phii)*> ^ phi1
;
then (l1 SubstWith l2) . phii =
((l1 SubstWith l2) . <*((S -firstChar) . phii)*>) ^ ((l1 SubstWith l2) . phi1)
by FOMODEL0:36
.=
((l1 SubstWith l2) . <*((S -firstChar) . phii)*>) ^ psi1
by FOMODEL0:def 22
;
then A7:
psi = ((l1 SubstWith l2) . <*((S -firstChar) . phii)*>) ^ psi1
by FOMODEL0:def 22;
x = (<*((S -firstChar) . phii)*> ^ phi1) ^ {}
by A6;
then A8:
phi1 is
SSSS -valued
by FOMODEL0:44;
(
((l1,u) ReassignIn I) -TruthEval phii = 1 iff
((l2,u) ReassignIn I) -TruthEval psi = 1 )
proof
per cases
( (S -firstChar) . phii = l1 or (S -firstChar) . phii <> l1 )
;
suppose A9:
(S -firstChar) . phii = l1
;
( ((l1,u) ReassignIn I) -TruthEval phii = 1 iff ((l2,u) ReassignIn I) -TruthEval psi = 1 )then A10:
psi = <*l2*> ^ psi1
by A7, FOMODEL0:35;
hereby ( ((l2,u) ReassignIn I) -TruthEval psi = 1 implies ((l1,u) ReassignIn I) -TruthEval phii = 1 )
assume
((l1,u) ReassignIn I) -TruthEval phii = 1
;
((l2,u) ReassignIn I) -TruthEval psi = 1then consider u1 being
Element of
U such that A11:
((((S -firstChar) . phii),u1) ReassignIn ((l1,u) ReassignIn I)) -TruthEval phi1 = 1
by A6, FOMODEL2:19;
1 =
((l1,u1) ReassignIn I) -TruthEval phi1
by A11, A9, FOMODEL0:43
.=
((l2,u1) ReassignIn I) -TruthEval psi1
by A8, A3
.=
((l2,u1) ReassignIn ((l2,u) ReassignIn I)) -TruthEval psi1
by FOMODEL0:43
;
hence
((l2,u) ReassignIn I) -TruthEval psi = 1
by A10, FOMODEL2:19;
verum
end; assume
((l2,u) ReassignIn I) -TruthEval psi = 1
;
((l1,u) ReassignIn I) -TruthEval phii = 1then consider u2 being
Element of
U such that A12:
((l2,u2) ReassignIn ((l2,u) ReassignIn I)) -TruthEval psi1 = 1
by A10, FOMODEL2:19;
1 =
((l2,u2) ReassignIn I) -TruthEval psi1
by A12, FOMODEL0:43
.=
((l1,u2) ReassignIn I) -TruthEval phi1
by A8, A3
.=
((((S -firstChar) . phii),u2) ReassignIn ((l1,u) ReassignIn I)) -TruthEval phi1
by A9, FOMODEL0:43
;
hence
((l1,u) ReassignIn I) -TruthEval phii = 1
by A6, FOMODEL2:19;
verum end; suppose A13:
(S -firstChar) . phii <> l1
;
( ((l1,u) ReassignIn I) -TruthEval phii = 1 iff ((l2,u) ReassignIn I) -TruthEval psi = 1 )then A14:
psi = <*((S -firstChar) . phii)*> ^ psi1
by A7, FOMODEL0:35;
hereby ( ((l2,u) ReassignIn I) -TruthEval psi = 1 implies ((l1,u) ReassignIn I) -TruthEval phii = 1 )
assume
((l1,u) ReassignIn I) -TruthEval phii = 1
;
((l2,u) ReassignIn I) -TruthEval psi = 1then consider u1 being
Element of
U such that A15:
((((S -firstChar) . phii),u1) ReassignIn ((l1,u) ReassignIn I)) -TruthEval phi1 = 1
by A6, FOMODEL2:19;
1 =
((l1,u) ReassignIn ((((S -firstChar) . phii),u1) ReassignIn I)) -TruthEval phi1
by A15, A13, FOMODEL0:43
.=
((l2,u) ReassignIn ((((S -firstChar) . phii),u1) ReassignIn I)) -TruthEval psi1
by A3, A8
.=
((((S -firstChar) . phii),u1) ReassignIn ((l2,u) ReassignIn I)) -TruthEval psi1
by A5, FOMODEL0:43
;
hence
((l2,u) ReassignIn I) -TruthEval psi = 1
by A14, FOMODEL2:19;
verum
end; assume
((l2,u) ReassignIn I) -TruthEval psi = 1
;
((l1,u) ReassignIn I) -TruthEval phii = 1then consider u2 being
Element of
U such that A16:
((((S -firstChar) . phii),u2) ReassignIn ((l2,u) ReassignIn I)) -TruthEval psi1 = 1
by A14, FOMODEL2:19;
1 =
((l2,u) ReassignIn ((((S -firstChar) . phii),u2) ReassignIn I)) -TruthEval psi1
by A5, A16, FOMODEL0:43
.=
((l1,u) ReassignIn ((((S -firstChar) . phii),u2) ReassignIn I)) -TruthEval phi1
by A3, A8
.=
((((S -firstChar) . phii),u2) ReassignIn ((l1,u) ReassignIn I)) -TruthEval phi1
by A13, FOMODEL0:43
;
hence
((l1,u) ReassignIn I) -TruthEval phii = 1
by A6, FOMODEL2:19;
verum end;
end; then
(
((l1,u) ReassignIn I) -TruthEval phii = 1 iff not
((l2,u) ReassignIn I) -TruthEval psi = 0 )
by FOMODEL0:39;
hence
((l1,u) ReassignIn I) -TruthEval phi = ((l2,u) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn phi)
by FOMODEL0:39;
verum end; suppose
( not
phi is
exal & not
phi is
0wff )
;
((l1,u) ReassignIn I) -TruthEval phi = ((l2,u) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn phi)then reconsider phii =
phii as non
0wff n + 1
-wff non
exal string of
S ;
reconsider phi2 =
tail phii as
n -wff string of
S ;
reconsider psi2 = (
l1,
l2)
-SymbolSubstIn phi2 as
n -wff string of
S ;
((S -firstChar) . phii) \+\ (TheNorSymbOf S) = {}
;
then
(S -firstChar) . phii = TheNorSymbOf S
by FOMODEL0:29;
then A17:
phii = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2
by FOMODEL2:23;
then
(
phi1 is
(AllSymbolsOf S) \ {l2} -valued &
phi2 is
(AllSymbolsOf S) \ {l2} -valued & (
((l1,u) ReassignIn I) -TruthEval phii = 1 implies (
((l1,u) ReassignIn I) -TruthEval phi1 = 0 &
((l1,u) ReassignIn I) -TruthEval phi2 = 0 ) ) & (
((l1,u) ReassignIn I) -TruthEval phi1 = 0 &
((l1,u) ReassignIn I) -TruthEval phi2 = 0 implies
((l1,u) ReassignIn I) -TruthEval phii = 1 ) )
by A4, FOMODEL0:44, FOMODEL2:19;
then A18:
(
((l1,u) ReassignIn I) -TruthEval phii = 1 iff (
((l2,u) ReassignIn I) -TruthEval psi1 = 0 &
((l2,u) ReassignIn I) -TruthEval psi2 = 0 ) )
by A3;
A19:
(
(l1 SubstWith l2) . phii = psi &
(l1 SubstWith l2) . phi1 = psi1 &
(l1 SubstWith l2) . phi2 = psi2 )
by FOMODEL0:def 22;
then psi =
((l1 SubstWith l2) . (<*(TheNorSymbOf S)*> ^ phi1)) ^ ((l1 SubstWith l2) . phi2)
by A17, FOMODEL0:36
.=
(((l1 SubstWith l2) . <*(TheNorSymbOf S)*>) ^ ((l1 SubstWith l2) . phi1)) ^ ((l1 SubstWith l2) . phi2)
by FOMODEL0:36
.=
(<*(TheNorSymbOf S)*> ^ psi1) ^ psi2
by FOMODEL0:35, A19
;
then
(
((l2,u) ReassignIn I) -TruthEval psi = 1 iff not
((l1,u) ReassignIn I) -TruthEval phi = 0 )
by FOMODEL0:39, FOMODEL2:19, A18;
hence
((l1,u) ReassignIn I) -TruthEval phi = ((l2,u) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn phi)
by FOMODEL0:39;
verum end;
end;
A20:
for m being Nat holds S1[m]
from NAT_1:sch 2(A1, A2);
set m = Depth psi;
assume
not l2 in rng psi
; for I being Element of U -InterpretersOf S holds ((l1,u1) ReassignIn I) -TruthEval psi = ((l2,u1) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn psi)
then
( {l2} misses rng psi & rng psi c= AllSymbolsOf S )
by RELAT_1:def 19, ZFMISC_1:50;
then A21:
( psi is Depth psi -wff & psi is (AllSymbolsOf S) \ {l2} -valued )
by XBOOLE_1:86, FOMODEL2:def 31, RELAT_1:def 19;
let I be Element of U -InterpretersOf S; ((l1,u1) ReassignIn I) -TruthEval psi = ((l2,u1) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn psi)
thus
((l1,u1) ReassignIn I) -TruthEval psi = ((l2,u1) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn psi)
by A20, A21; verum