let S be Language; :: thesis: for l1, l2 being literal Element of S

for psi1 being wff string of S ex psi2 being wff string of S st

( Depth psi1 = Depth psi2 & (l1 SubstWith l2) . psi1 = psi2 )

let l1, l2 be literal Element of S; :: thesis: for psi1 being wff string of S ex psi2 being wff string of S st

( Depth psi1 = Depth psi2 & (l1 SubstWith l2) . psi1 = psi2 )

let psi1 be wff string of S; :: thesis: ex psi2 being wff string of S st

( Depth psi1 = Depth psi2 & (l1 SubstWith l2) . psi1 = psi2 )

set e = l1 SubstWith l2;

set N = TheNorSymbOf S;

set L = LettersOf S;

defpred S_{1}[ wff string of S] means ex psi being wff string of S st

( Depth psi = Depth $1 & (l1 SubstWith l2) . $1 = psi );

defpred S_{2}[ Nat] means for phi being wff string of S st Depth phi <= $1 holds

S_{1}[phi];

A1: S_{2}[ 0 ]
_{2}[n] holds

S_{2}[n + 1]
_{2}[n]
from NAT_1:sch 2(A1, A2);

hence ex psi2 being wff string of S st

( Depth psi1 = Depth psi2 & (l1 SubstWith l2) . psi1 = psi2 ) ; :: thesis: verum

for psi1 being wff string of S ex psi2 being wff string of S st

( Depth psi1 = Depth psi2 & (l1 SubstWith l2) . psi1 = psi2 )

let l1, l2 be literal Element of S; :: thesis: for psi1 being wff string of S ex psi2 being wff string of S st

( Depth psi1 = Depth psi2 & (l1 SubstWith l2) . psi1 = psi2 )

let psi1 be wff string of S; :: thesis: ex psi2 being wff string of S st

( Depth psi1 = Depth psi2 & (l1 SubstWith l2) . psi1 = psi2 )

set e = l1 SubstWith l2;

set N = TheNorSymbOf S;

set L = LettersOf S;

defpred S

( Depth psi = Depth $1 & (l1 SubstWith l2) . $1 = psi );

defpred S

S

A1: S

proof

A2:
for n being Nat st S
thus
for phi being wff string of S st Depth phi <= 0 holds

S_{1}[phi]
:: thesis: verum

end;S

proof

let phi be wff string of S; :: thesis: ( Depth phi <= 0 implies S_{1}[phi] )

set D = Depth phi;

assume Depth phi <= 0 ; :: thesis: S_{1}[phi]

then Depth phi = 0 ;

then reconsider p0 = phi as 0 -wff string of S by FOMODEL2:def 31;

reconsider psi = (l1,l2) -SymbolSubstIn p0 as 0wff string of S ;

take psi ; :: thesis: ( Depth psi = Depth phi & (l1 SubstWith l2) . phi = psi )

thus Depth psi = Depth phi ; :: thesis: (l1 SubstWith l2) . phi = psi

thus (l1 SubstWith l2) . phi = psi by FOMODEL0:def 22; :: thesis: verum

end;set D = Depth phi;

assume Depth phi <= 0 ; :: thesis: S

then Depth phi = 0 ;

then reconsider p0 = phi as 0 -wff string of S by FOMODEL2:def 31;

reconsider psi = (l1,l2) -SymbolSubstIn p0 as 0wff string of S ;

take psi ; :: thesis: ( Depth psi = Depth phi & (l1 SubstWith l2) . phi = psi )

thus Depth psi = Depth phi ; :: thesis: (l1 SubstWith l2) . phi = psi

thus (l1 SubstWith l2) . phi = psi by FOMODEL0:def 22; :: thesis: verum

S

proof

for n being Nat holds S
let n be Nat; :: thesis: ( S_{2}[n] implies S_{2}[n + 1] )

set Fn = S -formulasOfMaxDepth n;

assume A3: S_{2}[n]
; :: thesis: S_{2}[n + 1]

thus for phi being wff string of S st Depth phi <= n + 1 holds

S_{1}[phi]
:: thesis: verum

end;set Fn = S -formulasOfMaxDepth n;

assume A3: S

thus for phi being wff string of S st Depth phi <= n + 1 holds

S

proof

let phi be wff string of S; :: thesis: ( Depth phi <= n + 1 implies S_{1}[phi] )

set D = Depth phi;

assume A4: Depth phi <= n + 1 ; :: thesis: S_{1}[phi]

end;set D = Depth phi;

assume A4: Depth phi <= n + 1 ; :: thesis: S

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

end;

suppose
phi is 0wff
; :: thesis: S_{1}[phi]

then reconsider p0 = phi as 0wff string of S ;

reconsider psi = (l1,l2) -SymbolSubstIn p0 as 0wff string of S ;

take psi ; :: thesis: ( Depth psi = Depth phi & (l1 SubstWith l2) . phi = psi )

thus Depth psi = Depth phi ; :: thesis: (l1 SubstWith l2) . phi = psi

thus (l1 SubstWith l2) . phi = psi by FOMODEL0:def 22; :: thesis: verum

end;reconsider psi = (l1,l2) -SymbolSubstIn p0 as 0wff string of S ;

take psi ; :: thesis: ( Depth psi = Depth phi & (l1 SubstWith l2) . phi = psi )

thus Depth psi = Depth phi ; :: thesis: (l1 SubstWith l2) . phi = psi

thus (l1 SubstWith l2) . phi = psi by FOMODEL0:def 22; :: thesis: verum

suppose A5:
phi is exal
; :: thesis: S_{1}[phi]

then consider m being Nat such that

A6: Depth phi = m + 1 by NAT_1:6;

phi in m -ExFormulasOf S by A6, A5, FOMODEL2:18;

then consider v being Element of LettersOf S, phi1 being Element of S -formulasOfMaxDepth m such that

A7: phi = <*v*> ^ phi1 ;

reconsider l = v as literal Element of S ;

reconsider phi11 = phi1 as m -wff string of S by FOMODEL2:def 24;

set m1 = Depth phi11;

(Depth phi11) + 1 <= n + 1 by A4, A7, FOMODEL2:17;

then consider psi1 being wff string of S such that

A8: ( Depth psi1 = Depth phi11 & (l1 SubstWith l2) . phi11 = psi1 ) by A3, XREAL_1:8;

( l = l1 or l <> l1 ) ;

then ( (l1 SubstWith l2) . <*l*> = <*l2*> or (l1 SubstWith l2) . <*l*> = <*l*> ) by FOMODEL0:35;

then consider s being literal Element of S such that

A9: (l1 SubstWith l2) . <*l*> = <*s*> ;

take psi = <*s*> ^ psi1; :: thesis: ( Depth psi = Depth phi & (l1 SubstWith l2) . phi = psi )

thus Depth psi = (Depth psi1) + 1 by FOMODEL2:17

.= Depth phi by A8, A7, FOMODEL2:17 ; :: thesis: (l1 SubstWith l2) . phi = psi

thus (l1 SubstWith l2) . phi = psi by A9, A8, A7, FOMODEL0:36; :: thesis: verum

end;A6: Depth phi = m + 1 by NAT_1:6;

phi in m -ExFormulasOf S by A6, A5, FOMODEL2:18;

then consider v being Element of LettersOf S, phi1 being Element of S -formulasOfMaxDepth m such that

A7: phi = <*v*> ^ phi1 ;

reconsider l = v as literal Element of S ;

reconsider phi11 = phi1 as m -wff string of S by FOMODEL2:def 24;

set m1 = Depth phi11;

(Depth phi11) + 1 <= n + 1 by A4, A7, FOMODEL2:17;

then consider psi1 being wff string of S such that

A8: ( Depth psi1 = Depth phi11 & (l1 SubstWith l2) . phi11 = psi1 ) by A3, XREAL_1:8;

( l = l1 or l <> l1 ) ;

then ( (l1 SubstWith l2) . <*l*> = <*l2*> or (l1 SubstWith l2) . <*l*> = <*l*> ) by FOMODEL0:35;

then consider s being literal Element of S such that

A9: (l1 SubstWith l2) . <*l*> = <*s*> ;

take psi = <*s*> ^ psi1; :: thesis: ( Depth psi = Depth phi & (l1 SubstWith l2) . phi = psi )

thus Depth psi = (Depth psi1) + 1 by FOMODEL2:17

.= Depth phi by A8, A7, FOMODEL2:17 ; :: thesis: (l1 SubstWith l2) . phi = psi

thus (l1 SubstWith l2) . phi = psi by A9, A8, A7, FOMODEL0:36; :: thesis: verum

suppose A10:
( not phi is exal & not phi is 0wff )
; :: thesis: S_{1}[phi]

then consider m being Nat such that

A11: Depth phi = m + 1 by NAT_1:6;

phi in m -NorFormulasOf S by FOMODEL2:18, A10, A11;

then consider phi1, phi2 being Element of S -formulasOfMaxDepth m such that

A12: phi = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 ;

reconsider phi11 = phi1, phi22 = phi2 as m -wff string of S by FOMODEL2:def 24;

set m1 = Depth phi11;

set m2 = Depth phi22;

set M = max ((Depth phi11),(Depth phi22));

A13: ( ((max ((Depth phi11),(Depth phi22))) - (Depth phi11)) + (Depth phi11) >= 0 + (Depth phi11) & ((max ((Depth phi11),(Depth phi22))) - (Depth phi22)) + (Depth phi22) >= 0 + (Depth phi22) ) by XREAL_1:6;

n + 1 >= (max ((Depth phi11),(Depth phi22))) + 1 by FOMODEL2:17, A4, A12;

then n >= max ((Depth phi11),(Depth phi22)) by XREAL_1:8;

then ( S_{1}[phi11] & S_{1}[phi22] )
by A3, A13, XXREAL_0:2;

then consider psi1, psi2 being wff string of S such that

A14: ( Depth psi1 = Depth phi11 & (l1 SubstWith l2) . phi11 = psi1 & Depth psi2 = Depth phi22 & (l1 SubstWith l2) . phi22 = psi2 ) ;

take psi = (<*(TheNorSymbOf S)*> ^ psi1) ^ psi2; :: thesis: ( Depth psi = Depth phi & (l1 SubstWith l2) . phi = psi )

thus Depth phi = (max ((Depth phi11),(Depth phi22))) + 1 by A12, FOMODEL2:17

.= Depth psi by A14, FOMODEL2:17 ; :: thesis: (l1 SubstWith l2) . phi = psi

thus (l1 SubstWith l2) . phi = ((l1 SubstWith l2) . (<*(TheNorSymbOf S)*> ^ phi11)) ^ ((l1 SubstWith l2) . phi22) by A12, FOMODEL0:36

.= (((l1 SubstWith l2) . <*(TheNorSymbOf S)*>) ^ ((l1 SubstWith l2) . phi11)) ^ psi2 by A14, FOMODEL0:36

.= psi by FOMODEL0:35, A14 ; :: thesis: verum

end;A11: Depth phi = m + 1 by NAT_1:6;

phi in m -NorFormulasOf S by FOMODEL2:18, A10, A11;

then consider phi1, phi2 being Element of S -formulasOfMaxDepth m such that

A12: phi = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 ;

reconsider phi11 = phi1, phi22 = phi2 as m -wff string of S by FOMODEL2:def 24;

set m1 = Depth phi11;

set m2 = Depth phi22;

set M = max ((Depth phi11),(Depth phi22));

A13: ( ((max ((Depth phi11),(Depth phi22))) - (Depth phi11)) + (Depth phi11) >= 0 + (Depth phi11) & ((max ((Depth phi11),(Depth phi22))) - (Depth phi22)) + (Depth phi22) >= 0 + (Depth phi22) ) by XREAL_1:6;

n + 1 >= (max ((Depth phi11),(Depth phi22))) + 1 by FOMODEL2:17, A4, A12;

then n >= max ((Depth phi11),(Depth phi22)) by XREAL_1:8;

then ( S

then consider psi1, psi2 being wff string of S such that

A14: ( Depth psi1 = Depth phi11 & (l1 SubstWith l2) . phi11 = psi1 & Depth psi2 = Depth phi22 & (l1 SubstWith l2) . phi22 = psi2 ) ;

take psi = (<*(TheNorSymbOf S)*> ^ psi1) ^ psi2; :: thesis: ( Depth psi = Depth phi & (l1 SubstWith l2) . phi = psi )

thus Depth phi = (max ((Depth phi11),(Depth phi22))) + 1 by A12, FOMODEL2:17

.= Depth psi by A14, FOMODEL2:17 ; :: thesis: (l1 SubstWith l2) . phi = psi

thus (l1 SubstWith l2) . phi = ((l1 SubstWith l2) . (<*(TheNorSymbOf S)*> ^ phi11)) ^ ((l1 SubstWith l2) . phi22) by A12, FOMODEL0:36

.= (((l1 SubstWith l2) . <*(TheNorSymbOf S)*>) ^ ((l1 SubstWith l2) . phi11)) ^ psi2 by A14, FOMODEL0:36

.= psi by FOMODEL0:35, A14 ; :: thesis: verum

hence ex psi2 being wff string of S st

( Depth psi1 = Depth psi2 & (l1 SubstWith l2) . psi1 = psi2 ) ; :: thesis: verum