begin
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).