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 abs (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 abs (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 abs (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 abs (ar s) -element & w = <*s*> ^ ((S -multiCat) . T) )
then ( w in (S -termsOfMaxDepth) . (mm + 1) & not w in (S -termsOfMaxDepth) . mm ) by DefTermal;
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 DefTerm;
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
C1: ( 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
C2: ( C = Compound (sss,((S -termsOfMaxDepth) . mm)) & sss is operational ) by C1;
reconsider ss = sss as termal Element of S by C2;
take s = ss; :: thesis: ex T being Element of ((S -termsOfMaxDepth) . mm) * st
( T is abs (ar s) -element & w = <*s*> ^ ((S -multiCat) . T) )
consider StringTuple being Element of ((AllSymbolsOf S) *) * such that
C3: ( w = <*s*> ^ ((S -multiCat) . StringTuple) & rng StringTuple c= (S -termsOfMaxDepth) . mm & StringTuple is abs (ar ss) -element ) by C1, C2;
reconsider TT = StringTuple as FinSequence of (S -termsOfMaxDepth) . mm by C3, FINSEQ_1:def 4;
reconsider TTT = TT as Element of ((S -termsOfMaxDepth) . mm) * by FINSEQ_1:def 11;
take T = TTT; :: thesis: ( T is abs (ar s) -element & w = <*s*> ^ ((S -multiCat) . T) )
thus T is abs (ar s) -element by C3; :: thesis: w = <*s*> ^ ((S -multiCat) . T)
thus w = <*s*> ^ ((S -multiCat) . T) by C3; :: thesis: verum