let m be Nat; :: thesis: for S being Language holds S -formulasOfMaxDepth m is S -prefix
let S be Language; :: thesis: S -formulasOfMaxDepth m is S -prefix
set SS = AllSymbolsOf S;
set AF = AtomicFormulasOf S;
set Nor = TheNorSymbOf S;
set Phi0 = S -formulasOfMaxDepth 0;
set F = S -firstChar ;
defpred S₁[ Nat] means S -formulasOfMaxDepth $1 is AllSymbolsOf S -prefix ;
A0: S₁[ 0 ] ;
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume B0: S₁[n] ; :: thesis: S₁[n + 1]
set N = n + 1;
set PhiN = S -formulasOfMaxDepth (n + 1);
set Phin = S -formulasOfMaxDepth n;
B1: (S -formulasOfMaxDepth (n + 1)) \ (S -formulasOfMaxDepth 0) is AllSymbolsOf S -prefix

proof

now

let p1, q1, p2, q2 be AllSymbolsOf S -valued FinSequence; :: thesis: ( p1 in (S -formulasOfMaxDepth (n + 1)) \ (S -formulasOfMaxDepth 0) & p2 in (S -formulasOfMaxDepth (n + 1)) \ (S -formulasOfMaxDepth 0) & p1 ^ q1 = p2 ^ q2 implies ( b₁ = b₃ & b₂ = b₄ ) )
assume C1: p1 in (S -formulasOfMaxDepth (n + 1)) \ (S -formulasOfMaxDepth 0) ; :: thesis: ( p2 in (S -formulasOfMaxDepth (n + 1)) \ (S -formulasOfMaxDepth 0) & p1 ^ q1 = p2 ^ q2 implies ( b₁ = b₃ & b₂ = b₄ ) )
then reconsider phi1 = p1 as n + 1 -wff string of S by DefWff1;
consider m1 being Nat such that
C3: ( phi1 is m1 + 1 -wff & not phi1 is m1 -wff & m1 + 1 <= n + 1 ) by Lm16, C1;
assume C4: p2 in (S -formulasOfMaxDepth (n + 1)) \ (S -formulasOfMaxDepth 0) ; :: thesis: ( p1 ^ q1 = p2 ^ q2 implies ( b₁ = b₃ & b₂ = b₄ ) )
then reconsider phi2 = p2 as n + 1 -wff string of S by DefWff1;
consider m2 being Nat such that
C5: ( phi2 is m2 + 1 -wff & not phi2 is m2 -wff & m2 + 1 <= n + 1 ) by Lm16, C4;
C8: ( m1 <= n & m2 <= n ) by C3, C5, XREAL_1:6;
then consider k1 being Nat such that
C9: n = m1 + k1 by NAT_1:10;
consider k2 being Nat such that
C10: n = m2 + k2 by C8, NAT_1:10;
assume C7: p1 ^ q1 = p2 ^ q2 ; :: thesis: ( b₁ = b₃ & b₂ = b₄ )

per cases ( ex v1 being literal Element of S ex phi11 being m1 -wff string of S st phi1 = <*v1*> ^ phi11 or ex r1, s1 being m1 -wff string of S st phi1 = (<*(TheNorSymbOf S)*> ^ r1) ^ s1 ) by Lm8, C3;

suppose ex v1 being literal Element of S ex phi11 being m1 -wff string of S st phi1 = <*v1*> ^ phi11 ; :: thesis: ( b₁ = b₃ & b₂ = b₄ )

then consider v1 being literal Element of S, phi11 being m1 -wff string of S such that
D0: phi1 = <*v1*> ^ phi11 ;

per cases ( ex v2 being literal Element of S ex phi22 being m2 -wff string of S st phi2 = <*v2*> ^ phi22 or ex r2, s2 being m2 -wff string of S st phi2 = (<*(TheNorSymbOf S)*> ^ r2) ^ s2 ) by Lm8, C5;

suppose ex v2 being literal Element of S ex phi22 being m2 -wff string of S st phi2 = <*v2*> ^ phi22 ; :: thesis: ( b₁ = b₃ & b₂ = b₄ )

then consider v2 being literal Element of S, phi22 being m2 -wff string of S such that
E0: phi2 = <*v2*> ^ phi22 ;
(<*v2*> ^ phi22) ^ q2 = <*v1*> ^ (phi11 ^ q1) by E0, C7, D0, FINSEQ_1:32;
then E1: <*v2*> ^ (phi22 ^ q2) = <*v1*> ^ (phi11 ^ q1) by FINSEQ_1:32;
then Z0: (<*v2*> ^ (phi22 ^ q2)) . 1 = v1 by FINSEQ_1:41;
then E3: v2 = v1 by FINSEQ_1:41;
<*v1*> ^ (phi22 ^ q2) = <*v1*> ^ (phi11 ^ q1) by E1, Z0, FINSEQ_1:41;
then E2: phi22 ^ q2 = phi11 ^ q1 by FINSEQ_1:33;
( phi11 is m1 + (0 * k1) -wff & phi22 is m2 + (0 * k2) -wff ) ;
then ( phi11 in S -formulasOfMaxDepth n & phi22 in S -formulasOfMaxDepth n ) by C9, C10, DefWff1;
hence ( p1 = p2 & q1 = q2 ) by D0, E3, E0, B0, E2, FOMODEL0:def 20; :: thesis: verum

end;

suppose ex r2, s2 being m2 -wff string of S st phi2 = (<*(TheNorSymbOf S)*> ^ r2) ^ s2 ; :: thesis: ( b₁ = b₃ & b₂ = b₄ )

then consider r2, s2 being m2 -wff string of S such that
E0: phi2 = (<*(TheNorSymbOf S)*> ^ r2) ^ s2 ;
phi1 . 1 = (phi2 ^ q2) . 1 by C7, FOMODEL0:28
.= phi2 . 1 by FOMODEL0:28
.= (<*(TheNorSymbOf S)*> ^ (r2 ^ s2)) . 1 by E0, FINSEQ_1:32
.= TheNorSymbOf S by FINSEQ_1:41 ;
hence ( p1 = p2 & q1 = q2 ) by D0, FINSEQ_1:41; :: thesis: verum

end;

end;

end;

suppose ex r1, s1 being m1 -wff string of S st phi1 = (<*(TheNorSymbOf S)*> ^ r1) ^ s1 ; :: thesis: ( b₁ = b₃ & b₂ = b₄ )

then consider r1, s1 being m1 -wff string of S such that
D0: phi1 = (<*(TheNorSymbOf S)*> ^ r1) ^ s1 ;
Z0: phi1 . 1 = (<*(TheNorSymbOf S)*> ^ (r1 ^ s1)) . 1 by D0, FINSEQ_1:32
.= TheNorSymbOf S by FINSEQ_1:41 ;

per cases ( ex v2 being literal Element of S ex phi22 being m2 -wff string of S st phi2 = <*v2*> ^ phi22 or ex r2, s2 being m2 -wff string of S st phi2 = (<*(TheNorSymbOf S)*> ^ r2) ^ s2 ) by C5, Lm8;

suppose ex v2 being literal Element of S ex phi22 being m2 -wff string of S st phi2 = <*v2*> ^ phi22 ; :: thesis: ( b₁ = b₃ & b₂ = b₄ )

then consider v2 being literal Element of S, phi22 being m2 -wff string of S such that
E0: phi2 = <*v2*> ^ phi22 ;
phi1 . 1 = (phi2 ^ q2) . 1 by C7, FOMODEL0:28
.= (<*v2*> ^ phi22) . 1 by E0, FOMODEL0:28
.= v2 by FINSEQ_1:41 ;
hence ( p1 = p2 & q1 = q2 ) by Z0; :: thesis: verum

end;

suppose ex r2, s2 being m2 -wff string of S st phi2 = (<*(TheNorSymbOf S)*> ^ r2) ^ s2 ; :: thesis: ( b₁ = b₃ & b₂ = b₄ )

then consider r2, s2 being m2 -wff string of S such that
E0: phi2 = (<*(TheNorSymbOf S)*> ^ r2) ^ s2 ;
( r1 is m1 + (0 * k1) -wff & r2 is m2 + (0 * k2) -wff ) ;
then E1: ( r1 in S -formulasOfMaxDepth n & r2 in S -formulasOfMaxDepth n & s1 in S -formulasOfMaxDepth n & s2 in S -formulasOfMaxDepth n ) by C9, C10, DefWff1;
<*(TheNorSymbOf S)*> ^ ((r1 ^ s1) ^ q1) = (<*(TheNorSymbOf S)*> ^ (r1 ^ s1)) ^ q1 by FINSEQ_1:32
.= ((<*(TheNorSymbOf S)*> ^ r2) ^ s2) ^ q2 by D0, E0, C7, FINSEQ_1:32
.= (<*(TheNorSymbOf S)*> ^ (r2 ^ s2)) ^ q2 by FINSEQ_1:32
.= <*(TheNorSymbOf S)*> ^ ((r2 ^ s2) ^ q2) by FINSEQ_1:32 ;
then (r1 ^ s1) ^ q1 = (r2 ^ s2) ^ q2 by FINSEQ_1:33
.= r2 ^ (s2 ^ q2) by FINSEQ_1:32 ;
then r1 ^ (s1 ^ q1) = r2 ^ (s2 ^ q2) by FINSEQ_1:32;
then ( r1 = r2 & s1 ^ q1 = s2 ^ q2 ) by B0, E1, FOMODEL0:def 20;
hence ( p1 = p2 & q1 = q2 ) by D0, E0, B0, E1, FOMODEL0:def 20; :: thesis: verum

end;

end;

end;

end;

end;

hence (S -formulasOfMaxDepth (n + 1)) \ (S -formulasOfMaxDepth 0) is AllSymbolsOf S -prefix by FOMODEL0:def 20; :: thesis: verum

end;

now

let p1, q1, p2, q2 be AllSymbolsOf S -valued FinSequence; :: thesis: ( p1 in S -formulasOfMaxDepth (n + 1) & p2 in S -formulasOfMaxDepth (n + 1) & p1 ^ q1 = p2 ^ q2 implies ( b₁ = b₃ & b₂ = b₄ ) )
assume C0: ( p1 in S -formulasOfMaxDepth (n + 1) & p2 in S -formulasOfMaxDepth (n + 1) & p1 ^ q1 = p2 ^ q2 ) ; :: thesis: ( b₁ = b₃ & b₂ = b₄ )
then reconsider phi1 = p1, phi2 = p2 as n + 1 -wff string of S by DefWff1;

per cases ( phi1 in S -formulasOfMaxDepth 0 or not phi1 in S -formulasOfMaxDepth 0 ) ;

suppose D0: phi1 in S -formulasOfMaxDepth 0 ; :: thesis: ( b₁ = b₃ & b₂ = b₄ )

then phi1 is 0 -wff by DefWff1;
then reconsider phi11 = phi1 as 0wff string of S ;
(S -firstChar) . phi11 is relational Element of S ;
then phi1 . 1 is relational Element of S by FOMODEL0:6;
then (phi2 ^ q2) . 1 is relational Element of S by C0, FOMODEL0:28;
then phi2 . 1 is relational Element of S by FOMODEL0:28;
then (S -firstChar) . phi2 is relational by FOMODEL0:6;
then phi2 is 0wff ;
then phi2 is 0 -wff ;
then ( phi2 in S -formulasOfMaxDepth 0 & phi1 in S -formulasOfMaxDepth 0 ) by D0, DefWff1;
hence ( p1 = p2 & q1 = q2 ) by C0, FOMODEL0:def 20; :: thesis: verum

end;

suppose D0: not phi1 in S -formulasOfMaxDepth 0 ; :: thesis: ( b₁ = b₃ & b₂ = b₄ )

then not phi1 is 0 -wff by DefWff1;
then reconsider phi11 = phi1 as non 0wff wff string of S ;
(S -firstChar) . phi2 = phi2 . 1 by FOMODEL0:6
.= (phi1 ^ q1) . 1 by C0, FOMODEL0:28
.= phi1 . 1 by FOMODEL0:28
.= (S -firstChar) . phi11 by FOMODEL0:6 ;
then not phi2 is 0 -wff ;
then not phi2 in S -formulasOfMaxDepth 0 by DefWff1;
then ( phi1 in (S -formulasOfMaxDepth (n + 1)) \ (S -formulasOfMaxDepth 0) & phi2 in (S -formulasOfMaxDepth (n + 1)) \ (S -formulasOfMaxDepth 0) ) by C0, D0, XBOOLE_0:def 5;
hence ( p1 = p2 & q1 = q2 ) by C0, B1, FOMODEL0:def 20; :: thesis: verum

end;

end;

end;

hence S₁[n + 1] by FOMODEL0:def 20; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A0, A1);
then S -formulasOfMaxDepth m is AllSymbolsOf S -prefix ;
hence S -formulasOfMaxDepth m is S -prefix ; :: thesis: verum