environ
vocabularies HIDDEN, NUMBERS, NAT_1, FINSEQ_1, RELAT_1, ARYTM_3, CARD_1, XXREAL_0, ORDINAL4, REWRITE1, TARSKI, SUBSET_1, FUNCT_1, AFINSQ_1, XBOOLE_0, ORDINAL2, RELAT_2, PRELAMB, FINSEQ_5, LANG1, CIRCTRM1, REWRITE2, ORDINAL1, FINSET_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, FINSET_1, RELAT_1, DOMAIN_1, XCMPLX_0, NAT_1, FINSEQ_5, FUNCT_1, RELSET_1, XXREAL_0, AFINSQ_1, RELAT_2, FINSEQ_1, REWRITE1, FLANG_1, LANG1, PARTIT_2;
definitions TARSKI;
theorems AFINSQ_1, NAT_1, RELAT_1, RELAT_2, XREAL_1, ZFMISC_1, FINSEQ_1, FINSEQ_2, FUNCT_1, REWRITE1, FINSEQ_3, FINSEQ_5, TARSKI, XBOOLE_0, XBOOLE_1, ABCMIZ_0, RELSET_1, PARTIT_2, XTUPLE_0;
schemes CLASSES1, NAT_1, RELSET_1;
registrations NAT_1, AFINSQ_1, REWRITE1, FINSEQ_1, XXREAL_0, XBOOLE_0, RELAT_1, FUNCT_1, XREAL_0, ORDINAL1;
constructors HIDDEN, NAT_1, FINSEQ_5, REWRITE1, FLANG_1, LANG1, XREAL_0, RELSET_1, PARTIT_2;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities FINSEQ_1;
expansions TARSKI, FINSEQ_1;
definition
let E be
set ;
let S be
semi-Thue-system of
E;
existence
ex b1 being Relation of (E ^omega) st
for s, t being Element of E ^omega holds
( [s,t] in b1 iff s ==>. t,S )
uniqueness
for b1, b2 being Relation of (E ^omega) st ( for s, t being Element of E ^omega holds
( [s,t] in b1 iff s ==>. t,S ) ) & ( for s, t being Element of E ^omega holds
( [s,t] in b2 iff s ==>. t,S ) ) holds
b1 = b2
end;
:: These definitions will be later used for introduction of
:: reduction sequences between words from E^omega (XFinSequences).