let U be non empty set ; :: thesis: for S being Language
for phi being wff string of S
for I1, I2 being Element of U -InterpretersOf S st I1 | ((rng phi) /\ (OwnSymbolsOf S)) = I2 | ((rng phi) /\ (OwnSymbolsOf S)) holds
I1 -TruthEval phi = I2 -TruthEval phi
let S be Language; :: thesis: for phi being wff string of S
for I1, I2 being Element of U -InterpretersOf S st I1 | ((rng phi) /\ (OwnSymbolsOf S)) = I2 | ((rng phi) /\ (OwnSymbolsOf S)) holds
I1 -TruthEval phi = I2 -TruthEval phi
let phi be wff string of S; :: thesis: for I1, I2 being Element of U -InterpretersOf S st I1 | ((rng phi) /\ (OwnSymbolsOf S)) = I2 | ((rng phi) /\ (OwnSymbolsOf S)) holds
I1 -TruthEval phi = I2 -TruthEval phi
set O = OwnSymbolsOf S;
set II = U -InterpretersOf S;
set a = the adicity of S;
set E = TheEqSymbOf S;
set F = S -firstChar ;
set C = S -multiCat ;
defpred S₁[ Nat] means for I1, I2 being Element of U -InterpretersOf S
for phi being $1 -wff string of S st I1 | ((rng phi) /\ (OwnSymbolsOf S)) = I2 | ((rng phi) /\ (OwnSymbolsOf S)) holds
I1 -TruthEval phi = I2 -TruthEval phi;
A1: S₁[ 0 ]

proof

let I1, I2 be Element of U -InterpretersOf S; :: thesis: for phi being 0 -wff string of S st I1 | ((rng phi) /\ (OwnSymbolsOf S)) = I2 | ((rng phi) /\ (OwnSymbolsOf S)) holds
I1 -TruthEval phi = I2 -TruthEval phi
let phi be 0 -wff string of S; :: thesis: ( I1 | ((rng phi) /\ (OwnSymbolsOf S)) = I2 | ((rng phi) /\ (OwnSymbolsOf S)) implies I1 -TruthEval phi = I2 -TruthEval phi )
reconsider phi1 = phi as 0wff string of S ;
assume I1 | ((rng phi) /\ (OwnSymbolsOf S)) = I2 | ((rng phi) /\ (OwnSymbolsOf S)) ; :: thesis: I1 -TruthEval phi = I2 -TruthEval phi
then ( I1 | ((rng phi1) /\ (OwnSymbolsOf S)) = I2 | ((rng phi1) /\ (OwnSymbolsOf S)) & the adicity of S | ((rng phi1) /\ (OwnSymbolsOf S)) = the adicity of S | ((rng phi1) /\ (OwnSymbolsOf S)) & TheEqSymbOf S = TheEqSymbOf S ) ;
then consider phi2 being 0wff string of S such that
A2: ( phi2 = phi1 & I2 -AtomicEval phi2 = I1 -AtomicEval phi1 ) by Lm48;
thus I1 -TruthEval phi = I2 -TruthEval phi by A2; :: thesis: verum

end;

A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
let I1, I2 be Element of U -InterpretersOf S; :: thesis: for phi being n + 1 -wff string of S st I1 | ((rng phi) /\ (OwnSymbolsOf S)) = I2 | ((rng phi) /\ (OwnSymbolsOf S)) holds
I1 -TruthEval phi = I2 -TruthEval phi
let phi be n + 1 -wff string of S; :: thesis: ( I1 | ((rng phi) /\ (OwnSymbolsOf S)) = I2 | ((rng phi) /\ (OwnSymbolsOf S)) implies I1 -TruthEval phi = I2 -TruthEval phi )
assume A5: I1 | ((rng phi) /\ (OwnSymbolsOf S)) = I2 | ((rng phi) /\ (OwnSymbolsOf S)) ; :: thesis: I1 -TruthEval phi = I2 -TruthEval phi

per cases ( ( not phi is 0wff & not phi is exal ) or ( phi is exal & not phi is 0wff ) or phi is 0wff ) ;

suppose ( not phi is 0wff & not phi is exal ) ; :: thesis: I1 -TruthEval phi = I2 -TruthEval phi

then reconsider phii = phi as non 0wff n + 1 -wff non exal string of S ;
set X = (rng phii) /\ (OwnSymbolsOf S);
set s = (S -firstChar) . phii;
reconsider h = head phii, t = tail phii as n -wff string of S ;
phii = (<*((S -firstChar) . phii)*> ^ h) ^ t by FOMODEL2:23
.= <*((S -firstChar) . phii)*> ^ (h ^ t) by FINSEQ_1:32 ;
then ( rng (h ^ t) c= rng phii & rng t c= rng (h ^ t) & rng h c= rng (h ^ t) ) by FINSEQ_1:29, FINSEQ_1:30;
then ( rng h c= rng phii & rng t c= rng phii ) by XBOOLE_1:1;
then reconsider rh = (rng h) /\ (OwnSymbolsOf S), rt = (rng t) /\ (OwnSymbolsOf S) as Subset of ((rng phii) /\ (OwnSymbolsOf S)) by XBOOLE_1:26;
set v1 = I1 -TruthEval phii;
set v2 = I2 -TruthEval phii;
set h1 = I1 -TruthEval h;
set h2 = I2 -TruthEval h;
set t1 = I1 -TruthEval t;
set t2 = I2 -TruthEval t;
A6: I1 | rh = I1 | (rh null ((rng phii) /\ (OwnSymbolsOf S)))
.= (I1 | ((rng phii) /\ (OwnSymbolsOf S))) | rh by RELAT_1:71
.= I2 | (rh null ((rng phii) /\ (OwnSymbolsOf S))) by A5, RELAT_1:71 ;
I1 | rt = I1 | (rt null ((rng phii) /\ (OwnSymbolsOf S)))
.= (I1 | ((rng phii) /\ (OwnSymbolsOf S))) | rt by RELAT_1:71
.= I2 | (rt null ((rng phii) /\ (OwnSymbolsOf S))) by A5, RELAT_1:71 ;
then A7: I1 -TruthEval t = I2 -TruthEval t by A4;
( (I1 -TruthEval phii) \+\ ((I1 -TruthEval h) 'nor' (I1 -TruthEval t)) = {} & (I2 -TruthEval phii) \+\ ((I2 -TruthEval h) 'nor' (I2 -TruthEval t)) = {} ) ;
then ( I1 -TruthEval phii = (I1 -TruthEval h) 'nor' (I1 -TruthEval t) & I2 -TruthEval phii = (I2 -TruthEval h) 'nor' (I2 -TruthEval t) ) by FOMODEL0:29;
hence I1 -TruthEval phi = I2 -TruthEval phi by A4, A6, A7; :: thesis: verum

end;

suppose ( phi is exal & not phi is 0wff ) ; :: thesis: I1 -TruthEval phi = I2 -TruthEval phi

then reconsider phii = phi as wff exal string of S ;
set l = (S -firstChar) . phii;
reconsider h = head phii as n -wff string of S ;
A8: phii = (<*((S -firstChar) . phii)*> ^ h) ^ (tail phii) by FOMODEL2:23
.= <*((S -firstChar) . phii)*> ^ h ;
then reconsider rh = rng h as Subset of (rng phii) by FINSEQ_1:30;

now :: thesis: ( ( I1 -TruthEval phii = 1 implies I2 -TruthEval phii = 1 ) & ( I2 -TruthEval phii = 1 implies I1 -TruthEval phii = 1 ) )

hereby :: thesis: ( I2 -TruthEval phii = 1 implies I1 -TruthEval phii = 1 )

assume I1 -TruthEval phii = 1 ; :: thesis: I2 -TruthEval phii = 1
then consider u being Element of U such that
A9: ((((S -firstChar) . phii),u) ReassignIn I1) -TruthEval h = 1 by A8, FOMODEL2:19;
set f = ((S -firstChar) . phii) .--> ({} .--> u);
reconsider I1u = (((S -firstChar) . phii),u) ReassignIn I1, I2u = (((S -firstChar) . phii),u) ReassignIn I2 as Element of U -InterpretersOf S ;
I1u | ((rng h) /\ (OwnSymbolsOf S)) = (I1 | ((rh null (rng phii)) /\ (OwnSymbolsOf S))) +* ((((S -firstChar) . phii) .--> ({} .--> u)) | (rh /\ (OwnSymbolsOf S))) by FUNCT_4:71
.= (I1 | (rh /\ ((rng phii) /\ (OwnSymbolsOf S)))) +* ((((S -firstChar) . phii) .--> ({} .--> u)) | (rh /\ (OwnSymbolsOf S))) by XBOOLE_1:16
.= ((I1 | ((rng phii) /\ (OwnSymbolsOf S))) | rh) +* ((((S -firstChar) . phii) .--> ({} .--> u)) | (rh /\ (OwnSymbolsOf S))) by RELAT_1:71
.= (I2 | (((rng phii) /\ (OwnSymbolsOf S)) /\ rh)) +* ((((S -firstChar) . phii) .--> ({} .--> u)) | (rh /\ (OwnSymbolsOf S))) by RELAT_1:71, A5
.= (I2 | (((rng phii) /\ rh) /\ (OwnSymbolsOf S))) +* ((((S -firstChar) . phii) .--> ({} .--> u)) | (rh /\ (OwnSymbolsOf S))) by XBOOLE_1:16
.= I2u | ((rng h) /\ (OwnSymbolsOf S)) by FUNCT_4:71 ;
then I2u -TruthEval h = 1 by A9, A4;
hence I2 -TruthEval phii = 1 by A8, FOMODEL2:19; :: thesis: verum

end;

assume I2 -TruthEval phii = 1 ; :: thesis: I1 -TruthEval phii = 1
then consider u being Element of U such that
A10: ((((S -firstChar) . phii),u) ReassignIn I2) -TruthEval h = 1 by A8, FOMODEL2:19;
set f = ((S -firstChar) . phii) .--> ({} .--> u);
reconsider I1u = (((S -firstChar) . phii),u) ReassignIn I1, I2u = (((S -firstChar) . phii),u) ReassignIn I2 as Element of U -InterpretersOf S ;
I1u | ((rng h) /\ (OwnSymbolsOf S)) = (I1 | ((rh null (rng phii)) /\ (OwnSymbolsOf S))) +* ((((S -firstChar) . phii) .--> ({} .--> u)) | (rh /\ (OwnSymbolsOf S))) by FUNCT_4:71
.= (I1 | (rh /\ ((rng phii) /\ (OwnSymbolsOf S)))) +* ((((S -firstChar) . phii) .--> ({} .--> u)) | (rh /\ (OwnSymbolsOf S))) by XBOOLE_1:16
.= ((I1 | ((rng phii) /\ (OwnSymbolsOf S))) | rh) +* ((((S -firstChar) . phii) .--> ({} .--> u)) | (rh /\ (OwnSymbolsOf S))) by RELAT_1:71
.= (I2 | (((rng phii) /\ (OwnSymbolsOf S)) /\ rh)) +* ((((S -firstChar) . phii) .--> ({} .--> u)) | (rh /\ (OwnSymbolsOf S))) by RELAT_1:71, A5
.= (I2 | (((rng phii) /\ rh) /\ (OwnSymbolsOf S))) +* ((((S -firstChar) . phii) .--> ({} .--> u)) | (rh /\ (OwnSymbolsOf S))) by XBOOLE_1:16
.= I2u | ((rng h) /\ (OwnSymbolsOf S)) by FUNCT_4:71 ;
then I1u -TruthEval h = 1 by A10, A4;
hence I1 -TruthEval phii = 1 by A8, FOMODEL2:19; :: thesis: verum

end;

then ( I1 -TruthEval phii = 1 iff not I2 -TruthEval phii = 0 ) by FOMODEL0:39;
hence I1 -TruthEval phi = I2 -TruthEval phi by FOMODEL0:39; :: thesis: verum

end;

suppose phi is 0wff ; :: thesis: I1 -TruthEval phi = I2 -TruthEval phi

hence I1 -TruthEval phi = I2 -TruthEval phi by A1, A5; :: thesis: verum

end;

end;

end;

A11: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A3);
let I1, I2 be Element of U -InterpretersOf S; :: thesis: ( I1 | ((rng phi) /\ (OwnSymbolsOf S)) = I2 | ((rng phi) /\ (OwnSymbolsOf S)) implies I1 -TruthEval phi = I2 -TruthEval phi )
set d = Depth phi;
phi null 0 is (Depth phi) + 0 -wff ;
then reconsider phii = phi as Depth phi -wff string of S ;
assume I1 | ((rng phi) /\ (OwnSymbolsOf S)) = I2 | ((rng phi) /\ (OwnSymbolsOf S)) ; :: thesis: I1 -TruthEval phi = I2 -TruthEval phi
then I1 | ((rng phii) /\ (OwnSymbolsOf S)) = I2 | ((rng phii) /\ (OwnSymbolsOf S)) ;
hence I1 -TruthEval phi = I2 -TruthEval phi by A11; :: thesis: verum