begin
Lm1:
for S being non degenerated ZeroOneStr holds (S TrivialArity) . the ZeroF of S = - 2
Lm2:
ex S being Language-like st
( not S is degenerated & S is eligible )
Lm3:
for S being non degenerated Language-like holds TheEqSymbOf S in (AllSymbolsOf S) \ {(TheNorSymbOf S)}
Lm4:
for m being Nat
for S being Language holds (S -termsOfMaxDepth) . m c= ((AllSymbolsOf S) *) \ {{}}
Lm5:
for m, n being Nat
for S being Language holds (S -termsOfMaxDepth) . m c= (S -termsOfMaxDepth) . (m + n)
Lm6:
for x being set
for S being Language st x in AllTermsOf S holds
ex nn being Element of NAT st x in (S -termsOfMaxDepth) . nn
Lm7:
for mm being Element of NAT
for S being Language
for w being b1 + 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) )
Lm8:
for mm being Element of NAT
for S being Language
for w being b1 + 1 -termal string of S 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) )
Lm9:
for m being Nat
for S being Language holds (S -termsOfMaxDepth) . m is S -prefix
Lm10:
for S being Language holds AllTermsOf S is S -prefix
Lm11:
for m being Nat
for S being Language holds (S -termsOfMaxDepth) . m c= (TermSymbolsOf S) *
Lm12:
for S1 being non empty Language-like
for f being INT -valued Function holds
( LettersOf (S1 extendWith f) = ((f | ((dom f) \ (AllSymbolsOf S1))) " {0}) \/ (LettersOf S1) & the adicity of (S1 extendWith f) | (OwnSymbolsOf S1) = the adicity of S1 | (OwnSymbolsOf S1) )
::###################### basic definitions ##########################
::#####################################################################
::#####################################################################