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 S1[ Nat] means S -formulasOfMaxDepth $1 is AllSymbolsOf S -prefix ;
A1: S1[ 0 ] ;
A2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A3: S1[n] ; :: thesis: S1[n + 1]
set N = n + 1;
set PhiN = S -formulasOfMaxDepth (n + 1);
set Phin = S -formulasOfMaxDepth n;
A4: (S -formulasOfMaxDepth (n + 1)) \ (S -formulasOfMaxDepth 0) is AllSymbolsOf S -prefix
proof
now :: thesis: for p1, q1, p2, q2 being AllSymbolsOf S -valued FinSequence st p1 in (S -formulasOfMaxDepth (n + 1)) \ (S -formulasOfMaxDepth 0) & p2 in (S -formulasOfMaxDepth (n + 1)) \ (S -formulasOfMaxDepth 0) & p1 ^ q1 = p2 ^ q2 holds
( p1 = p2 & q1 = q2 )
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 ( b1 = b3 & b2 = b4 ) )
assume A5: p1 in (S -formulasOfMaxDepth (n + 1)) \ (S -formulasOfMaxDepth 0) ; :: thesis: ( p2 in (S -formulasOfMaxDepth (n + 1)) \ (S -formulasOfMaxDepth 0) & p1 ^ q1 = p2 ^ q2 implies ( b1 = b3 & b2 = b4 ) )
then reconsider phi1 = p1 as n + 1 -wff string of S by Def23;
consider m1 being Nat such that
A6: ( phi1 is m1 + 1 -wff & not phi1 is m1 -wff & m1 + 1 <= n + 1 ) by Lm20, A5;
assume A7: p2 in (S -formulasOfMaxDepth (n + 1)) \ (S -formulasOfMaxDepth 0) ; :: thesis: ( p1 ^ q1 = p2 ^ q2 implies ( b1 = b3 & b2 = b4 ) )
then reconsider phi2 = p2 as n + 1 -wff string of S by Def23;
consider m2 being Nat such that
A8: ( phi2 is m2 + 1 -wff & not phi2 is m2 -wff & m2 + 1 <= n + 1 ) by Lm20, A7;
consider k1 being Nat such that
A9: n = m1 + k1 by A6, XREAL_1:8, NAT_1:10;
consider k2 being Nat such that
A10: n = m2 + k2 by A8, XREAL_1:8, NAT_1:10;
assume A11: p1 ^ q1 = p2 ^ q2 ; :: thesis: ( b1 = b3 & b2 = b4 )
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 Lm21, A6;
suppose ex v1 being literal Element of S ex phi11 being m1 -wff string of S st phi1 = <*v1*> ^ phi11 ; :: thesis: ( b1 = b3 & b2 = b4 )
then consider v1 being literal Element of S, phi11 being m1 -wff string of S such that
A12: 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 Lm21, A8;
suppose ex v2 being literal Element of S ex phi22 being m2 -wff string of S st phi2 = <*v2*> ^ phi22 ; :: thesis: ( b1 = b3 & b2 = b4 )
then consider v2 being literal Element of S, phi22 being m2 -wff string of S such that
A13: phi2 = <*v2*> ^ phi22 ;
(<*v2*> ^ phi22) ^ q2 = <*v1*> ^ (phi11 ^ q1) by A13, A11, A12, FINSEQ_1:32;
then A14: <*v2*> ^ (phi22 ^ q2) = <*v1*> ^ (phi11 ^ q1) by FINSEQ_1:32;
then A15: (<*v2*> ^ (phi22 ^ q2)) . 1 = v1 by FINSEQ_1:41;
then A16: v2 = v1 by FINSEQ_1:41;
<*v1*> ^ (phi22 ^ q2) = <*v1*> ^ (phi11 ^ q1) by A14, A15, FINSEQ_1:41;
then A17: 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 A9, A10, Def23;
hence ( p1 = p2 & q1 = q2 ) by A12, A16, A13, A3, A17, FOMODEL0:def 19; :: thesis: verum
end;
suppose ex r2, s2 being m2 -wff string of S st phi2 = (<*(TheNorSymbOf S)*> ^ r2) ^ s2 ; :: thesis: ( b1 = b3 & b2 = b4 )
then consider r2, s2 being m2 -wff string of S such that
A18: phi2 = (<*(TheNorSymbOf S)*> ^ r2) ^ s2 ;
phi1 . 1 = (phi2 ^ q2) . 1 by FOMODEL0:28, A11
.= phi2 . 1 by FOMODEL0:28
.= (<*(TheNorSymbOf S)*> ^ (r2 ^ s2)) . 1 by A18, FINSEQ_1:32
.= TheNorSymbOf S by FINSEQ_1:41 ;
hence ( p1 = p2 & q1 = q2 ) by A12, 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: ( b1 = b3 & b2 = b4 )
then consider r1, s1 being m1 -wff string of S such that
A19: phi1 = (<*(TheNorSymbOf S)*> ^ r1) ^ s1 ;
A20: phi1 . 1 = (<*(TheNorSymbOf S)*> ^ (r1 ^ s1)) . 1 by A19, 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 A8, Lm21;
suppose ex v2 being literal Element of S ex phi22 being m2 -wff string of S st phi2 = <*v2*> ^ phi22 ; :: thesis: ( b1 = b3 & b2 = b4 )
then consider v2 being literal Element of S, phi22 being m2 -wff string of S such that
A21: phi2 = <*v2*> ^ phi22 ;
phi1 . 1 = (phi2 ^ q2) . 1 by FOMODEL0:28, A11
.= (<*v2*> ^ phi22) . 1 by FOMODEL0:28, A21
.= v2 by FINSEQ_1:41 ;
hence ( p1 = p2 & q1 = q2 ) by A20; :: thesis: verum
end;
suppose ex r2, s2 being m2 -wff string of S st phi2 = (<*(TheNorSymbOf S)*> ^ r2) ^ s2 ; :: thesis: ( b1 = b3 & b2 = b4 )
then consider r2, s2 being m2 -wff string of S such that
A22: phi2 = (<*(TheNorSymbOf S)*> ^ r2) ^ s2 ;
( r1 is m1 + (0 * k1) -wff & r2 is m2 + (0 * k2) -wff ) ;
then A23: ( r1 in S -formulasOfMaxDepth n & r2 in S -formulasOfMaxDepth n & s1 in S -formulasOfMaxDepth n & s2 in S -formulasOfMaxDepth n ) by A9, A10, Def23;
<*(TheNorSymbOf S)*> ^ ((r1 ^ s1) ^ q1) = (<*(TheNorSymbOf S)*> ^ (r1 ^ s1)) ^ q1 by FINSEQ_1:32
.= ((<*(TheNorSymbOf S)*> ^ r2) ^ s2) ^ q2 by A19, A22, A11, 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 A3, FOMODEL0:def 19, A23;
hence ( p1 = p2 & q1 = q2 ) by A19, A22, A3, A23, FOMODEL0:def 19; :: thesis: verum
end;
end;
end;
end;
end;
hence (S -formulasOfMaxDepth (n + 1)) \ (S -formulasOfMaxDepth 0) is AllSymbolsOf S -prefix ; :: thesis: verum
end;
now :: thesis: for p1, q1, p2, q2 being AllSymbolsOf S -valued FinSequence st p1 in S -formulasOfMaxDepth (n + 1) & p2 in S -formulasOfMaxDepth (n + 1) & p1 ^ q1 = p2 ^ q2 holds
( p1 = p2 & q1 = q2 )
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 ( b1 = b3 & b2 = b4 ) )
assume A24: ( p1 in S -formulasOfMaxDepth (n + 1) & p2 in S -formulasOfMaxDepth (n + 1) & p1 ^ q1 = p2 ^ q2 ) ; :: thesis: ( b1 = b3 & b2 = b4 )
then reconsider phi1 = p1, phi2 = p2 as n + 1 -wff string of S by Def23;
per cases ( phi1 in S -formulasOfMaxDepth 0 or not phi1 in S -formulasOfMaxDepth 0 ) ;
suppose A26: not phi1 in S -formulasOfMaxDepth 0 ; :: thesis: ( b1 = b3 & b2 = b4 )
then not phi1 is 0 -wff ;
then reconsider phi11 = phi1 as non 0wff wff string of S ;
(S -firstChar) . phi2 = phi2 . 1 by FOMODEL0:6
.= (phi1 ^ q1) . 1 by A24, 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 ;
then ( phi1 in (S -formulasOfMaxDepth (n + 1)) \ (S -formulasOfMaxDepth 0) & phi2 in (S -formulasOfMaxDepth (n + 1)) \ (S -formulasOfMaxDepth 0) ) by A24, A26, XBOOLE_0:def 5;
hence ( p1 = p2 & q1 = q2 ) by A24, A4; :: thesis: verum
end;
end;
end;
hence S1[n + 1] by FOMODEL0:def 19; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A1, A2);
 then S -formulasOfMaxDepth m is AllSymbolsOf S -prefix ;
hence S -formulasOfMaxDepth m is S -prefix ; :: thesis: verum