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 )

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

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

then consider phi1, phi2 being Element of S -formulasOfMaxDepth m such that
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 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

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