environ
vocabularies HIDDEN, NUMBERS, STRUCT_0, RELAT_1, XBOOLE_0, SUBSET_1, FINSEQ_1, TDGROUP, TARSKI, ORDINAL4, ARYTM_3, CARD_1, FUNCT_1, XXREAL_0, NAT_1, ZFMISC_1, ORDINAL1, FINSET_1, LANG1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, DOMAIN_1, RELAT_1, STRUCT_0, FUNCT_1, FINSEQ_1, FINSET_1, RELSET_1, PARTFUN1, FUNCT_2, FINSEQ_2, XXREAL_0, PRE_POLY;
definitions XBOOLE_0, TARSKI, RELAT_1, STRUCT_0;
theorems TARSKI, ZFMISC_1, RELAT_1, FINSEQ_1, NAT_1, RELSET_1, TREES_2, FUNCT_2, FINSEQ_3, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, ORDINAL1, XTUPLE_0;
schemes NAT_1, FUNCT_2;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FINSET_1, XXREAL_0, XREAL_0, FINSEQ_1, STRUCT_0, ORDINAL1, CARD_1, RELSET_1;
constructors HIDDEN, PARTFUN1, DOMAIN_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_2, STRUCT_0, RELSET_1, PRE_POLY;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities ORDINAL1;
expansions TARSKI;
definition
let a be
set ;
existence
ex b1 being strict GrammarStr st
( the carrier of b1 = {a} & the Rules of b1 = {[a,{}]} )
uniqueness
for b1, b2 being strict GrammarStr st the carrier of b1 = {a} & the Rules of b1 = {[a,{}]} & the carrier of b2 = {a} & the Rules of b2 = {[a,{}]} holds
b1 = b2
let b be
set ;
existence
ex b1 being strict GrammarStr st
( the carrier of b1 = {a,b} & the InitialSym of b1 = a & the Rules of b1 = {[a,<*b*>]} )
uniqueness
for b1, b2 being strict GrammarStr st the carrier of b1 = {a,b} & the InitialSym of b1 = a & the Rules of b1 = {[a,<*b*>]} & the carrier of b2 = {a,b} & the InitialSym of b2 = a & the Rules of b2 = {[a,<*b*>]} holds
b1 = b2
;
existence
ex b1 being strict GrammarStr st
( the carrier of b1 = {a,b} & the InitialSym of b1 = a & the Rules of b1 = {[a,<*b,a*>],[a,{}]} )
uniqueness
for b1, b2 being strict GrammarStr st the carrier of b1 = {a,b} & the InitialSym of b1 = a & the Rules of b1 = {[a,<*b,a*>],[a,{}]} & the carrier of b2 = {a,b} & the InitialSym of b2 = a & the Rules of b2 = {[a,<*b,a*>],[a,{}]} holds
b1 = b2
;
end;
definition
let D be non
empty set ;
existence
ex b1 being strict GrammarStr st
( the carrier of b1 = succ D & the InitialSym of b1 = D & the Rules of b1 = { [D,<*d,D*>] where d is Element of D : d = d } \/ {[D,{}]} )
uniqueness
for b1, b2 being strict GrammarStr st the carrier of b1 = succ D & the InitialSym of b1 = D & the Rules of b1 = { [D,<*d,D*>] where d is Element of D : d = d } \/ {[D,{}]} & the carrier of b2 = succ D & the InitialSym of b2 = D & the Rules of b2 = { [D,<*d,D*>] where d is Element of D : d = d } \/ {[D,{}]} holds
b1 = b2
;
end;
:: a set of non-terminal and terminal symbols, I is an initial symbol,
:: and R is a set of rules (ordered pairs).