let mm be Element of NAT ; :: thesis: for S being Language
for w being mm + 1 -termal string of S ex s being termal Element of S ex T being Element of ((S -termsOfMaxDepth) . mm) * st
( T is |.(ar s).| -element & w = <*s*> ^ ((S -multiCat) . T) )
let S be Language; :: thesis: for w being mm + 1 -termal string of S ex s being termal Element of S ex T being Element of ((S -termsOfMaxDepth) . mm) * st
( T is |.(ar s).| -element & w = <*s*> ^ ((S -multiCat) . T) )
set TS = TermSymbolsOf S;
set T = S -termsOfMaxDepth ;
set C = S -multiCat ;
set L = LettersOf S;
defpred S₁[ Element of omega ] means for w being $1 + 1 -termal string of S ex s being termal Element of S ex T being Element of ((S -termsOfMaxDepth) . $1) * st
( T is |.(ar s).| -element & w = <*s*> ^ ((S -multiCat) . T) );
defpred S₂[ Nat] means ex mm being Element of NAT st
( mm = $1 & S₁[mm] );
A1: S₂[ 0 ]

proof

take 0 ; :: thesis: ( 0 = 0 & S₁[ 0 ] )
thus 0 = 0 ; :: thesis: S₁[ 0 ]
thus S₁[ 0 ] :: thesis: verum

proof

let w be 0 + 1 -termal string of S; :: thesis: ex s being termal Element of S ex T being Element of ((S -termsOfMaxDepth) . 0) * st
( T is |.(ar s).| -element & w = <*s*> ^ ((S -multiCat) . T) )

per cases ( w is 0 -termal or not w is 0 -termal ) ;

suppose w is 0 -termal ; :: thesis: ex s being termal Element of S ex T being Element of ((S -termsOfMaxDepth) . 0) * st
( T is |.(ar s).| -element & w = <*s*> ^ ((S -multiCat) . T) )

then w in (S -termsOfMaxDepth) . 0 ;
then w in AtomicTermsOf S by Def30;
then w in { <*ss*> where ss is Element of LettersOf S : verum } by FINSEQ_2:96;
then consider ss being Element of LettersOf S such that
A2: w = <*ss*> ;
reconsider sss = ss as literal Element of S by Def14;
reconsider TT = {} as FinSequence ;
rng TT = {} ;
then reconsider TTT = TT as FinSequence of (S -termsOfMaxDepth) . 0 by XBOOLE_1:2, FINSEQ_1:def 4;
reconsider TTTT = TTT as Element of ((S -termsOfMaxDepth) . 0) * ;
take s = sss; :: thesis: ex T being Element of ((S -termsOfMaxDepth) . 0) * st
( T is |.(ar s).| -element & w = <*s*> ^ ((S -multiCat) . T) )
take T = TTTT; :: thesis: ( T is |.(ar s).| -element & w = <*s*> ^ ((S -multiCat) . T) )
thus T is |.(ar s).| -element ; :: thesis: w = <*s*> ^ ((S -multiCat) . T)
reconsider s = sss as Element of TermSymbolsOf S by Def18;
( (S -multiCat) . {} = {} & <*sss*> ^ {} = <*sss*> ) ;
hence w = <*s*> ^ ((S -multiCat) . T) by A2; :: thesis: verum

end;

suppose not w is 0 -termal ; :: thesis: ex s being termal Element of S ex T being Element of ((S -termsOfMaxDepth) . 0) * st
( T is |.(ar s).| -element & w = <*s*> ^ ((S -multiCat) . T) )

hence ex s being termal Element of S ex T being Element of ((S -termsOfMaxDepth) . 0) * st
( T is |.(ar s).| -element & w = <*s*> ^ ((S -multiCat) . T) ) by Lm7; :: thesis: verum

end;

end;

end;

end;

A3: for m being Nat st S₂[m] holds
S₂[m + 1]

proof

let m be Nat; :: thesis: ( S₂[m] implies S₂[m + 1] )
reconsider mm = m, mmm = m + 1 as Element of NAT by ORDINAL1:def 12;
assume A4: S₂[m] ; :: thesis: S₂[m + 1]
take mmm ; :: thesis: ( mmm = m + 1 & S₁[mmm] )
thus mmm = m + 1 ; :: thesis: S₁[mmm]
let w be mmm + 1 -termal string of S; :: thesis: ex s being termal Element of S ex T being Element of ((S -termsOfMaxDepth) . mmm) * st
( T is |.(ar s).| -element & w = <*s*> ^ ((S -multiCat) . T) )

per cases ( not w is mmm -termal or w is mmm -termal ) ;

suppose not w is mmm -termal ; :: thesis: ex s being termal Element of S ex T being Element of ((S -termsOfMaxDepth) . mmm) * st
( T is |.(ar s).| -element & w = <*s*> ^ ((S -multiCat) . T) )

hence ex s being termal Element of S ex T being Element of ((S -termsOfMaxDepth) . mmm) * st
( T is |.(ar s).| -element & w = <*s*> ^ ((S -multiCat) . T) ) by Lm7; :: thesis: verum

end;

suppose w is mmm -termal ; :: thesis: ex s being termal Element of S ex T being Element of ((S -termsOfMaxDepth) . mmm) * st
( T is |.(ar s).| -element & w = <*s*> ^ ((S -multiCat) . T) )

then consider s being termal Element of S, T being Element of ((S -termsOfMaxDepth) . mm) * such that
A5: ( T is |.(ar s).| -element & w = <*s*> ^ ((S -multiCat) . T) ) by A4;
set high = (S -termsOfMaxDepth) . mmm;
reconsider low = (S -termsOfMaxDepth) . mm as Subset of ((S -termsOfMaxDepth) . mmm) by Lm5;
( T in low * & low * is Subset of (((S -termsOfMaxDepth) . mmm) *) ) ;
then reconsider TT = T as Element of ((S -termsOfMaxDepth) . mmm) * ;
take s ; :: thesis: ex T being Element of ((S -termsOfMaxDepth) . mmm) * st
( T is |.(ar s).| -element & w = <*s*> ^ ((S -multiCat) . T) )
take TT ; :: thesis: ( TT is |.(ar s).| -element & w = <*s*> ^ ((S -multiCat) . TT) )
thus ( TT is |.(ar s).| -element & w = <*s*> ^ ((S -multiCat) . TT) ) by A5; :: thesis: verum

end;

end;

end;

A6: for m being Nat holds S₂[m] from NAT_1:sch 2(A1, A3);

now :: thesis: for mm being Element of NAT holds S₁[mm]

let mm be Element of NAT ; :: thesis: S₁[mm]
reconsider m = mm as Nat ;
consider nn being Element of NAT such that
A7: ( nn = m & S₁[nn] ) by A6;
thus S₁[mm] by A7; :: thesis: verum

end;

hence for w being mm + 1 -termal string of S ex s being termal Element of S ex T being Element of ((S -termsOfMaxDepth) . mm) * st
( T is |.(ar s).| -element & w = <*s*> ^ ((S -multiCat) . T) ) ; :: thesis: verum