let m be Nat; :: thesis: for S being Language

for phi being wff string of S st not phi is 0wff & not phi is exal & phi is m + 1 -wff holds

( head phi is m -wff string of S & tail phi is m -wff string of S )

let S be Language; :: thesis: for phi being wff string of S st not phi is 0wff & not phi is exal & phi is m + 1 -wff holds

( head phi is m -wff string of S & tail phi is m -wff string of S )

let phi be wff string of S; :: thesis: ( not phi is 0wff & not phi is exal & phi is m + 1 -wff implies ( head phi is m -wff string of S & tail phi is m -wff string of S ) )

assume ( not phi is 0wff & not phi is exal & phi is m + 1 -wff ) ; :: thesis: ( head phi is m -wff string of S & tail phi is m -wff string of S )

then reconsider phii = phi as non 0wff m + 1 -wff non exal string of S ;

set N = TheNorSymbOf S;

set F = S -firstChar ;

set s = (S -firstChar) . phii;

set dh = Depth (head phii);

set dt = Depth (tail phii);

set M = max ((Depth (head phii)),(Depth (tail phii)));

set d = Depth phii;

reconsider h = head phii as Depth (head phii) -wff string of S by Def30;

reconsider t = tail phii as Depth (tail phii) -wff string of S by Def30;

A1: Depth phii <= m + 1 by Def30;

((S -firstChar) . phii) \+\ (TheNorSymbOf S) = {} ;

then (S -firstChar) . phii = TheNorSymbOf S by FOMODEL0:29;

then phii = (<*(TheNorSymbOf S)*> ^ h) ^ t by Th23;

then (max ((Depth (head phii)),(Depth (tail phii)))) + 1 <= m + 1 by A1, Th17;

then ((max ((Depth (head phii)),(Depth (tail phii)))) + 1) - 1 <= (m + 1) - 1 by XREAL_1:8;

then ( (max ((Depth (head phii)),(Depth (tail phii)))) + (- (Depth (head phii))) <= m + (- (Depth (head phii))) & (max ((Depth (head phii)),(Depth (tail phii)))) + (- (Depth (tail phii))) <= m + (- (Depth (tail phii))) ) by XREAL_1:6;

then ( (max ((Depth (head phii)),(Depth (tail phii)))) - (Depth (head phii)) <= m - (Depth (head phii)) & (max ((Depth (head phii)),(Depth (tail phii)))) - (Depth (tail phii)) <= m - (Depth (tail phii)) ) ;

then ( 0 <= m - (Depth (head phii)) & 0 <= m - (Depth (tail phii)) ) ;

then reconsider nh = m - (Depth (head phii)), nt = m - (Depth (tail phii)) as Nat ;

( h is (Depth (head phii)) + (0 * nh) -wff & t is (Depth (tail phii)) + (0 * nt) -wff ) ;

then ( h is (Depth (head phii)) + nh -wff & t is (Depth (tail phii)) + nt -wff ) ;

hence ( head phi is m -wff string of S & tail phi is m -wff string of S ) ; :: thesis: verum

for phi being wff string of S st not phi is 0wff & not phi is exal & phi is m + 1 -wff holds

( head phi is m -wff string of S & tail phi is m -wff string of S )

let S be Language; :: thesis: for phi being wff string of S st not phi is 0wff & not phi is exal & phi is m + 1 -wff holds

( head phi is m -wff string of S & tail phi is m -wff string of S )

let phi be wff string of S; :: thesis: ( not phi is 0wff & not phi is exal & phi is m + 1 -wff implies ( head phi is m -wff string of S & tail phi is m -wff string of S ) )

assume ( not phi is 0wff & not phi is exal & phi is m + 1 -wff ) ; :: thesis: ( head phi is m -wff string of S & tail phi is m -wff string of S )

then reconsider phii = phi as non 0wff m + 1 -wff non exal string of S ;

set N = TheNorSymbOf S;

set F = S -firstChar ;

set s = (S -firstChar) . phii;

set dh = Depth (head phii);

set dt = Depth (tail phii);

set M = max ((Depth (head phii)),(Depth (tail phii)));

set d = Depth phii;

reconsider h = head phii as Depth (head phii) -wff string of S by Def30;

reconsider t = tail phii as Depth (tail phii) -wff string of S by Def30;

A1: Depth phii <= m + 1 by Def30;

((S -firstChar) . phii) \+\ (TheNorSymbOf S) = {} ;

then (S -firstChar) . phii = TheNorSymbOf S by FOMODEL0:29;

then phii = (<*(TheNorSymbOf S)*> ^ h) ^ t by Th23;

then (max ((Depth (head phii)),(Depth (tail phii)))) + 1 <= m + 1 by A1, Th17;

then ((max ((Depth (head phii)),(Depth (tail phii)))) + 1) - 1 <= (m + 1) - 1 by XREAL_1:8;

then ( (max ((Depth (head phii)),(Depth (tail phii)))) + (- (Depth (head phii))) <= m + (- (Depth (head phii))) & (max ((Depth (head phii)),(Depth (tail phii)))) + (- (Depth (tail phii))) <= m + (- (Depth (tail phii))) ) by XREAL_1:6;

then ( (max ((Depth (head phii)),(Depth (tail phii)))) - (Depth (head phii)) <= m - (Depth (head phii)) & (max ((Depth (head phii)),(Depth (tail phii)))) - (Depth (tail phii)) <= m - (Depth (tail phii)) ) ;

then ( 0 <= m - (Depth (head phii)) & 0 <= m - (Depth (tail phii)) ) ;

then reconsider nh = m - (Depth (head phii)), nt = m - (Depth (tail phii)) as Nat ;

( h is (Depth (head phii)) + (0 * nh) -wff & t is (Depth (tail phii)) + (0 * nt) -wff ) ;

then ( h is (Depth (head phii)) + nh -wff & t is (Depth (tail phii)) + nt -wff ) ;

hence ( head phi is m -wff string of S & tail phi is m -wff string of S ) ; :: thesis: verum