let mm be Element of NAT ; :: thesis: for S being Language
for w being mm + 1 -termal string of S st not w is mm -termal holds
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 st not w is mm -termal holds
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 fam = { (Compound (s,((S -termsOfMaxDepth) . mm))) where s is ofAtomicFormula Element of S : s is operational } ;
let w be mm + 1 -termal string of S; :: thesis: ( not w is mm -termal implies 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) ) )
assume not w is mm -termal ; :: thesis: 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) )
then ( w in (S -termsOfMaxDepth) . (mm + 1) & not w in (S -termsOfMaxDepth) . mm ) by Def33;
then ( w in (union { (Compound (s,((S -termsOfMaxDepth) . mm))) where s is ofAtomicFormula Element of S : s is operational } ) \/ ((S -termsOfMaxDepth) . mm) & not w in (S -termsOfMaxDepth) . mm ) by Def30;
then w in union { (Compound (s,((S -termsOfMaxDepth) . mm))) where s is ofAtomicFormula Element of S : s is operational } by XBOOLE_0:def 3;
then consider C being set such that
A1: ( w in C & C in { (Compound (s,((S -termsOfMaxDepth) . mm))) where s is ofAtomicFormula Element of S : s is operational } ) by TARSKI:def 4;
consider sss being ofAtomicFormula Element of S such that
A2: ( C = Compound (sss,((S -termsOfMaxDepth) . mm)) & sss is operational ) by A1;
reconsider ss = sss as termal Element of S by A2;
take s = ss; :: thesis: ex T being Element of ((S -termsOfMaxDepth) . mm) * st
( T is |.(ar s).| -element & w = <*s*> ^ ((S -multiCat) . T) )
consider StringTuple being Element of ((AllSymbolsOf S) *) * such that
A3: ( w = <*s*> ^ ((S -multiCat) . StringTuple) & rng StringTuple c= (S -termsOfMaxDepth) . mm & StringTuple is |.(ar ss).| -element ) by A1, A2;
reconsider TT = StringTuple as FinSequence of (S -termsOfMaxDepth) . mm by A3, FINSEQ_1:def 4;
reconsider TTT = TT as Element of ((S -termsOfMaxDepth) . mm) * ;
take T = TTT; :: thesis: ( T is |.(ar s).| -element & w = <*s*> ^ ((S -multiCat) . T) )
thus T is |.(ar s).| -element by A3; :: thesis: w = <*s*> ^ ((S -multiCat) . T)
thus w = <*s*> ^ ((S -multiCat) . T) by A3; :: thesis: verum