environ
vocabularies HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, NAT_1, INT_1, RELAT_1, FINSEQ_1, FUNCT_1, ARYTM_3, XCMPLX_0, CARD_1, MONOID_0, ORDINAL1, ARYTM_1, STRUCT_0, XXREAL_0, ORDINAL4, BINOP_1, FINSEQ_2, COMPLEX1, PARTFUN1, FINSET_1, SUPINF_2, MESFUNC1, PRE_POLY, SETFAM_1, FUNCT_4, FUNCOP_1, FUNCT_2, CARD_3, FOMODEL0, FOMODEL1;
notations HIDDEN, TARSKI, CARD_1, XBOOLE_0, SUBSET_1, NAT_1, ZFMISC_1, ORDINAL1, NUMBERS, INT_1, PRE_POLY, FINSEQ_1, XCMPLX_0, RELAT_1, FUNCT_1, FUNCT_2, MONOID_0, XXREAL_0, XREAL_0, ALGSTR_0, BINOP_1, FINSEQ_2, ENUMSET1, MCART_1, PARTFUN1, INT_2, FINSEQOP, FINSET_1, MATRIX_1, STRUCT_0, RELSET_1, SETFAM_1, FUNCT_4, FUNCOP_1, DOMAIN_1, CARD_3, ORDERS_4, FOMODEL0;
definitions ;
theorems TARSKI, XBOOLE_0, INT_1, FUNCT_1, FINSEQ_1, RELAT_1, XBOOLE_1, STRUCT_0, ZFMISC_1, FUNCT_2, XXREAL_0, NAT_1, ORDINAL1, FINSEQ_5, FUNCT_4, FINSEQ_2, COMPLEX1, FINSEQ_4, RELSET_1, GRFUNC_1, FUNCOP_1, CARD_4, ORDERS_4, PARTFUN1, FOMODEL0, CARD_1, ABSVALUE;
schemes NAT_1, FUNCT_2, DOMAIN_1;
registrations ORDINAL1, XCMPLX_0, NAT_1, RELAT_1, NUMBERS, FUNCT_1, INT_1, FINSEQ_1, STRUCT_0, FUNCT_2, FINSEQ_2, SUBSET_1, CARD_1, CARD_5, FINSET_1, PRALG_1, PRE_POLY, FINSEQ_6, FOMODEL0, XBOOLE_0, XXREAL_0, XREAL_0, FUNCOP_1, FUNCT_4, RELSET_1, RAMSEY_1, CARD_3;
constructors HIDDEN, TARSKI, NAT_1, CARD_1, ZFMISC_1, NUMBERS, INT_1, ARYTM_3, FINSEQ_1, MONOID_0, STRUCT_0, XXREAL_0, BINOP_1, FINSEQ_2, COMPLEX1, RELSET_1, INT_2, FINSEQOP, DOMAIN_1, FINSET_1, MATRIX_1, REAL_1, PRE_POLY, SETFAM_1, FUNCT_4, FUNCOP_1, RELAT_1, FUNCT_1, FUNCT_2, CARD_3, ORDERS_4, WELLORD2, FOMODEL0;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
equalities FINSEQ_1, XBOOLE_0, STRUCT_0, FUNCOP_1, FOMODEL0, ORDINAL1;
expansions XBOOLE_0, STRUCT_0, FOMODEL0;
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 |.(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 |.(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) )
Lm13:
for S being Language
for t1, t2 being termal string of S holds (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is 0wff string of S
::###################### basic definitions ##########################
::#####################################################################
::#####################################################################