let m be Nat; :: thesis: for S being Language holds S -formulasOfMaxDepth m is S -prefix
let S be Language; :: thesis:
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)) \ () is AllSymbolsOf S -prefix
proof
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 A5: p1 in (S -formulasOfMaxDepth (n + 1)) \ () ; :: thesis: ( p2 in (S -formulasOfMaxDepth (n + 1)) \ () & 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 ;
assume A7: p2 in (S -formulasOfMaxDepth (n + 1)) \ () ; :: 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 ;
consider k1 being Nat such that
A9: n = m1 + k1 by ;
consider k2 being Nat such that
A10: n = m2 + k2 by ;
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 = (<*()*> ^ r1) ^ s1 ) by ;
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 = (<*()*> ^ r2) ^ s2 ) by ;
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 ;
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 ;
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 ;
hence ( p1 = p2 & q1 = q2 ) by ; :: thesis: verum
end;
suppose ex r2, s2 being m2 -wff string of S st phi2 = (<*()*> ^ r2) ^ s2 ; :: thesis: ( b1 = b3 & b2 = b4 )
then consider r2, s2 being m2 -wff string of S such that
A18: phi2 = (<*()*> ^ r2) ^ s2 ;
phi1 . 1 = (phi2 ^ q2) . 1 by
.= phi2 . 1 by FOMODEL0:28
.= (<*()*> ^ (r2 ^ s2)) . 1 by
.= TheNorSymbOf S by FINSEQ_1:41 ;
hence ( p1 = p2 & q1 = q2 ) by ; :: thesis: verum
end;
end;
end;
suppose ex r1, s1 being m1 -wff string of S st phi1 = (<*()*> ^ r1) ^ s1 ; :: thesis: ( b1 = b3 & b2 = b4 )
then consider r1, s1 being m1 -wff string of S such that
A19: phi1 = (<*()*> ^ r1) ^ s1 ;
A20: phi1 . 1 = (<*()*> ^ (r1 ^ s1)) . 1 by
.= 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 = (<*()*> ^ r2) ^ s2 ) by ;
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
.= (<*v2*> ^ phi22) . 1 by
.= 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 = (<*()*> ^ r2) ^ s2 ; :: thesis: ( b1 = b3 & b2 = b4 )
then consider r2, s2 being m2 -wff string of S such that
A22: phi2 = (<*()*> ^ 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 ;
<*()*> ^ ((r1 ^ s1) ^ q1) = (<*()*> ^ (r1 ^ s1)) ^ q1 by FINSEQ_1:32
.= ((<*()*> ^ r2) ^ s2) ^ q2 by
.= (<*()*> ^ (r2 ^ s2)) ^ q2 by FINSEQ_1:32
.= <*()*> ^ ((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 ;
hence ( p1 = p2 & q1 = q2 ) by ; :: thesis: verum
end;
end;
end;
end;
end;
hence (S -formulasOfMaxDepth (n + 1)) \ () 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 ;
() . phi2 = phi2 . 1 by FOMODEL0:6
.= (phi1 ^ q1) . 1 by
.= phi1 . 1 by FOMODEL0:28
.= () . phi11 by FOMODEL0:6 ;
then not phi2 is 0 -wff ;
then not phi2 in S -formulasOfMaxDepth 0 ;
then ( phi1 in (S -formulasOfMaxDepth (n + 1)) \ () & phi2 in (S -formulasOfMaxDepth (n + 1)) \ () ) by ;
hence ( p1 = p2 & q1 = q2 ) by ; :: 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