let U be non empty set ; :: thesis:
let S be Language; :: thesis:
let l be literal Element of S; :: thesis:
let psi be wff string of S; :: thesis:
let tt be Element of AllTermsOf S; :: thesis:
set II = U -InterpretersOf S;
set TT = AllTermsOf S;
set AF = AtomicFormulasOf S;
set F = S -firstChar ;
set L = LettersOf S;
set f0 = l AtomicSubst tt;
set f1 = l Subst1 tt;
set f4 = (l,tt) Subst4 (l Subst1 tt);
set FF = AllFormulasOf S;
set N = TheNorSymbOf S;
defpred S₁[ Nat] means for phi being wff string of S st Depth phi <= $1 holds
( Depth ((l,tt) SubstIn phi) = Depth phi & ( for I being Element of U -InterpretersOf S holds I -TruthEval ((l,tt) SubstIn phi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phi ) );
tt null {} is {} \/ (rng tt) -valued FinSequence ;
then tt is FinSequence of rng tt by FOMODEL0:26;
then reconsider ttt = tt as Element of (rng tt) * ;
A1: S₁[ 0 ]

proof

let phi be wff string of S; :: thesis:
set d = Depth phi;
set IT = (l,tt) SubstIn phi;
assume A2: Depth phi <= 0 ; :: thesis:
reconsider phii = phi as 0wff string of S by A2;
Depth ((l,tt) SubstIn phii) = 0 ;
hence Depth ((l,tt) SubstIn phi) = Depth phi ; :: thesis:
let I be Element of U -InterpretersOf S; :: thesis:
set u = (I -TermEval) . tt;
set J = (l,((I -TermEval) . tt)) ReassignIn I;
I -TruthEval ((l,tt) AtomicSubst phii) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phii by Th8;
hence I -TruthEval ((l,tt) SubstIn phi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phi ; :: thesis:

end;

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

proof

let n be Nat; :: thesis:
assume A4: S₁[n] ; :: thesis:
let phi be wff string of S; :: thesis:
reconsider X = (LettersOf S) \ (((rng tt) \/ (rng (head phi))) \/ {l}) as infinite Subset of (LettersOf S) ;
reconsider XX = X as non empty Subset of (LettersOf S) ;
set ll2 = the Element of X;
reconsider l2 = the Element of X as literal Element of S by TARSKI:def 3;
assume C0: Depth phi <= n + 1 ; :: thesis:
not l2 in ((rng tt) \/ (rng (head phi))) \/ {l} by XBOOLE_0:def 5;
then ( not l2 in (rng tt) \/ (rng (head phi)) & not l2 in {l} ) by XBOOLE_0:def 3;
then A5: ( l2 <> l & not l2 in rng tt & not l2 in rng (head phi) ) by XBOOLE_0:def 3, TARSKI:def 1;

per cases ;

suppose phi is exal ; :: thesis:

then reconsider phii = phi as non 0wff wff exal string of S ;
consider m being Nat such that
A6: Depth phii = m + 1 by NAT_1:6;
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
D1: m <= n by XREAL_1:8, C0, A6;
reconsider phii = phii as non 0wff m + 1 -wff exal string of S by A6, FOMODEL2:def 31;
set IT = (l,tt) SubstIn phii;
set d = Depth phii;
reconsider l1 = (S -firstChar) . phii as literal Element of S ;
reconsider phi1 = head phii as Element of AllFormulasOf S by FOMODEL2:16;
set d1 = Depth phi1;
reconsider phi2 = tail phii as empty set ;
reconsider psi = (l1,l2) -SymbolSubstIn phi as m + 1 -wff string of S ;
reconsider psi1 = (l1,l2) -SymbolSubstIn (head phii) as m -wff string of S ;
(Depth psi1) \+\ (Depth phi1) = {} ;
then A7: Depth psi1 = Depth phi1 by FOMODEL0:29;
reconsider Phi1 = (l,tt) SubstIn psi1 as wff string of S ;
A8: phii = (<*l1*> ^ phi1) ^ phi2 by FOMODEL2:23
.= <*l1*> ^ phi1 ;
Depth phi1 <= m by FOMODEL2:def 31;
then A9: Depth phi1 <= n by XXREAL_0:2, D1;
then A10: Depth Phi1 = Depth (head phii) by A4, A7;
reconsider m1 = m - (Depth phi1) as Nat ;
reconsider new1 = (l,tt) SubstIn phi1 as wff string of S ;
set d11 = Depth new1;
A11: (l,tt) SubstIn phii = (l,tt,m,(((l,tt) Subst4 (l Subst1 tt)) . mm)) Subst2 phii by A6, Lm44;

per cases ;

suppose l1 <> l ; :: thesis:

then A12: (l,tt) SubstIn phii = <*l2*> ^ ((((l,tt) Subst4 (l Subst1 tt)) . mm) . ((l1,l2) -SymbolSubstIn phi1)) by A6, Def20, A11
.= <*l2*> ^ ((l,tt) SubstIn psi1) by Lm46 ;
then Depth ((l,tt) SubstIn phii) = (Depth phi1) + 1 by A10, FOMODEL2:17
.= Depth phi by A8, FOMODEL2:17 ;
hence Depth ((l,tt) SubstIn phi) = Depth phi ; :: thesis:
let I be Element of U -InterpretersOf S; :: thesis:
set tu = (I -TermEval) . tt;
set It = (l,((I -TermEval) . tt)) ReassignIn I;
( I -TruthEval ((l,tt) SubstIn phii) = 1 iff ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phii = 1 )

proof

hereby :: thesis:

assume I -TruthEval ((l,tt) SubstIn phii) = 1 ; :: thesis:
then consider u being Element of U such that
A13: ((l2,u) ReassignIn I) -TruthEval Phi1 = 1 by A12, FOMODEL2:19;
set I2 = (l2,u) ReassignIn I;
1 = ((l,((((l2,u) ReassignIn I) -TermEval) . tt)) ReassignIn ((l2,u) ReassignIn I)) -TruthEval psi1 by A13, A7, A9, A4
.= ((l,((I -TermEval) . tt)) ReassignIn ((l2,u) ReassignIn I)) -TruthEval psi1 by A5, FOMODEL2:25
.= ((l2,u) ReassignIn ((l,((I -TermEval) . tt)) ReassignIn I)) -TruthEval psi1 by A5, FOMODEL0:43
.= ((l1,u) ReassignIn ((l,((I -TermEval) . tt)) ReassignIn I)) -TruthEval (head phii) by A5, Th9 ;
hence 1 = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phii by A8, FOMODEL2:19; :: thesis:

end;

assume ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phii = 1 ; :: thesis:
then consider u1 being Element of U such that
A14: ((l1,u1) ReassignIn ((l,((I -TermEval) . tt)) ReassignIn I)) -TruthEval (head phii) = 1 by A8, FOMODEL2:19;
1 = ((l2,u1) ReassignIn ((l,((I -TermEval) . tt)) ReassignIn I)) -TruthEval psi1 by A14, Th9, A5
.= ((l,((I -TermEval) . tt)) ReassignIn ((l2,u1) ReassignIn I)) -TruthEval psi1 by FOMODEL0:43, A5
.= ((l,((((l2,u1) ReassignIn I) -TermEval) . tt)) ReassignIn ((l2,u1) ReassignIn I)) -TruthEval psi1 by FOMODEL2:25, A5
.= ((l2,u1) ReassignIn I) -TruthEval Phi1 by A7, A9, A4 ;
hence I -TruthEval ((l,tt) SubstIn phii) = 1 by A12, FOMODEL2:19; :: thesis:

end;

then ( I -TruthEval ((l,tt) SubstIn phii) = 1 iff not ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phii = 0 ) by FOMODEL0:39;
hence I -TruthEval ((l,tt) SubstIn phi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phi by FOMODEL0:39; :: thesis:

end;

suppose A15: l1 = l ; :: thesis:

then A16: phi = (l,tt) SubstIn phii by Lm45;
thus Depth ((l,tt) SubstIn phi) = Depth phi by A15, Lm45; :: thesis:
let I be Element of U -InterpretersOf S; :: thesis:
set tu = (I -TermEval) . tt;
set It = (l,((I -TermEval) . tt)) ReassignIn I;
( ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phii = 1 iff I -TruthEval phii = 1 )

proof

hereby :: thesis:

assume ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phii = 1 ; :: thesis:
then consider u being Element of U such that
A17: ((l1,u) ReassignIn ((l,((I -TermEval) . tt)) ReassignIn I)) -TruthEval phi1 = 1 by A8, FOMODEL2:19;
1 = ((l1,u) ReassignIn I) -TruthEval phi1 by A17, A15, FOMODEL0:43;
hence I -TruthEval phii = 1 by A8, FOMODEL2:19; :: thesis:

end;

assume I -TruthEval phii = 1 ; :: thesis:
then consider u1 being Element of U such that
A18: ((l1,u1) ReassignIn I) -TruthEval phi1 = 1 by A8, FOMODEL2:19;
((l1,u1) ReassignIn ((l,((I -TermEval) . tt)) ReassignIn I)) -TruthEval phi1 = 1 by A15, A18, FOMODEL0:43;
hence ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phii = 1 by A8, FOMODEL2:19; :: thesis:

end;

then ( ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phi = 1 iff not I -TruthEval phi = 0 ) by FOMODEL0:39;
hence I -TruthEval ((l,tt) SubstIn phi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phi by A16, FOMODEL0:39; :: thesis:

end;

suppose ( not phi is exal & not phi is 0wff ) ; :: thesis:

then reconsider phii = phi as non 0wff wff non exal string of S ;
set IT = (l,tt) SubstIn phii;
set d = Depth phii;
consider m being Nat such that
A19: Depth phii = m + 1 by NAT_1:6;
W1: (m + 1) + (- 1) <= (n + 1) - 1 by XREAL_1:8, C0, A19;
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
reconsider phii = phii as non 0wff m + 1 -wff non exal string of S by A19, FOMODEL2:def 31;
reconsider phi1 = head phii, phi2 = tail phii as Element of AllFormulasOf S by FOMODEL2:16;
set d1 = Depth phi1;
set d2 = Depth phi2;
( ((S -firstChar) . phii) \+\ (TheNorSymbOf S) = {} & phii = (<*((S -firstChar) . phii)*> ^ phi1) ^ phi2 ) by FOMODEL2:23;
then A20: phii = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 by FOMODEL0:29;
D2: ( Depth phi1 <= m & Depth phi2 <= m ) by FOMODEL2:def 31;
reconsider m1 = m - (Depth phi1), m2 = m - (Depth phi2) as Nat ;
reconsider new1 = (l,tt) SubstIn phi1, new2 = (l,tt) SubstIn phi2 as wff string of S ;
set d11 = Depth new1;
set d22 = Depth new2;
A21: ( Depth phi1 <= n & Depth phi2 <= n ) by W1, D2, XXREAL_0:2;
A22: (l,tt) SubstIn phii = (l,tt,m,(((l,tt) Subst4 (l Subst1 tt)) . mm)) Subst2 phii by A19, Lm44
.= (<*(TheNorSymbOf S)*> ^ ((((l,tt) Subst4 (l Subst1 tt)) . ((Depth phi1) + m1)) . phi1)) ^ ((((l,tt) Subst4 (l Subst1 tt)) . ((Depth phi2) + m2)) . phi2) by Def20, A19
.= (<*(TheNorSymbOf S)*> ^ new1) ^ ((((l,tt) Subst4 (l Subst1 tt)) . ((Depth phi2) + m2)) . phi2) by Lm45
.= (<*(TheNorSymbOf S)*> ^ new1) ^ new2 by Lm45 ;
then Depth ((l,tt) SubstIn phii) = 1 + (max ((Depth new1),(Depth new2))) by FOMODEL2:17
.= 1 + (max ((Depth phi1),(Depth new2))) by A21, A4
.= 1 + (max ((Depth phi1),(Depth phi2))) by A21, A4
.= Depth phii by FOMODEL2:17, A20 ;
hence Depth ((l,tt) SubstIn phi) = Depth phi ; :: thesis:
let I be Element of U -InterpretersOf S; :: thesis:
set TE = I -TermEval ;
set u = (I -TermEval) . tt;
set J = (l,((I -TermEval) . tt)) ReassignIn I;
set LH = I -TruthEval ((l,tt) SubstIn phii);
set RH = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phii;
( I -TruthEval new1 = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phi1 & I -TruthEval new2 = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phi2 ) by A21, A4;
then ( ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phii = 1 iff ( I -TruthEval new1 = 0 & I -TruthEval new2 = 0 ) ) by A20, FOMODEL2:19;
then ( I -TruthEval ((l,tt) SubstIn phii) = 1 iff not ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phii = 0 ) by FOMODEL2:19, A22, FOMODEL0:39;
hence I -TruthEval ((l,tt) SubstIn phi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phi by FOMODEL0:39; :: thesis:

end;

suppose phi is 0wff ; :: thesis:

hence ( Depth ((l,tt) SubstIn phi) = Depth phi & ( for I being Element of U -InterpretersOf S holds I -TruthEval ((l,tt) SubstIn phi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phi ) ) by A1; :: thesis:

end;

A23: for m being Nat holds S₁[m] from NAT_1:sch 2(A1, A3);
set m = Depth psi;
thus Depth ((l,tt) SubstIn psi) = Depth psi by A23; :: thesis:
let I be Element of U -InterpretersOf S; :: thesis:
thus I -TruthEval ((l,tt) SubstIn psi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval psi by A23; :: thesis: