let m be Nat; :: thesis: for S being Language
for w being string of S st w is m + 1 -wff & not w is m -wff & ( for v being literal Element of S
for phi being m -wff string of S holds not w = <*v*> ^ phi ) holds
ex phi1, phi2 being m -wff string of S st w = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2
let S be Language; :: thesis: for w being string of S st w is m + 1 -wff & not w is m -wff & ( for v being literal Element of S
for phi being m -wff string of S holds not w = <*v*> ^ phi ) holds
ex phi1, phi2 being m -wff string of S st w = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2
let w be string of S; :: thesis: ( w is m + 1 -wff & not w is m -wff & ( for v being literal Element of S
for phi being m -wff string of S holds not w = <*v*> ^ phi ) implies ex phi1, phi2 being m -wff string of S st w = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 )
set Phim = S -formulasOfMaxDepth m;
set PhiM = S -formulasOfMaxDepth (m + 1);
set L = LettersOf S;
set N = TheNorSymbOf S;
set EF = m -ExFormulasOf S;
set NF = m -NorFormulasOf S;
assume w is m + 1 -wff ; :: thesis: ( w is m -wff or ex v being literal Element of S ex phi being m -wff string of S st w = <*v*> ^ phi or ex phi1, phi2 being m -wff string of S st w = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 )
then w in S -formulasOfMaxDepth (m + 1) ;
then w in ((m -ExFormulasOf S) \/ (m -NorFormulasOf S)) \/ (S -formulasOfMaxDepth m) by Th9;
then A1: ( w in m -ExFormulasOf S or w in m -NorFormulasOf S or w in S -formulasOfMaxDepth m ) by Lm8;
assume A2: not w is m -wff ; :: thesis: ( ex v being literal Element of S ex phi being m -wff string of S st w = <*v*> ^ phi or ex phi1, phi2 being m -wff string of S st w = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 )
assume A3: for v being literal Element of S
for phi being m -wff string of S holds not w = <*v*> ^ phi ; :: thesis: ex phi1, phi2 being m -wff string of S st w = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2
( w in m -ExFormulasOf S implies ex v being literal Element of S ex phi being m -wff string of S st w = <*v*> ^ phi )
proof
assume w in m -ExFormulasOf S ; :: thesis: ex v being literal Element of S ex phi being m -wff string of S st w = <*v*> ^ phi
then consider vv being Element of LettersOf S, phi being Element of S -formulasOfMaxDepth m such that
A4: w = <*vv*> ^ phi ;
reconsider phii = phi as m -wff string of S by Def23;
reconsider v = vv as literal Element of S ;
take v ; :: thesis: ex phi being m -wff string of S st w = <*v*> ^ phi
take phii ; :: thesis: w = <*v*> ^ phii
thus w = <*v*> ^ phii by A4; :: thesis: verum
end;
then consider phi1, phi2 being Element of S -formulasOfMaxDepth m such that
A5: w = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 by A3, A2, A1;
reconsider phi11 = phi1, phi22 = phi2 as m -wff string of S by Def23;
take phi11 ; :: thesis: ex phi2 being m -wff string of S st w = (<*(TheNorSymbOf S)*> ^ phi11) ^ phi2
take phi22 ; :: thesis: w = (<*(TheNorSymbOf S)*> ^ phi11) ^ phi22
thus w = (<*(TheNorSymbOf S)*> ^ phi11) ^ phi22 by A5; :: thesis: verum