environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, SUBSET_1, AFINSQ_1, NAT_1, REWRITE3, XXREAL_0, ARYTM_3, CARD_1, FINSEQ_1, ORDINAL4, RELAT_1, FUNCT_1, FLANG_1, FSM_1, STRUCT_0, ZFMISC_1, TARSKI, FINSET_1, REWRITE2, PRELAMB, FSM_2, LANG1, REWRITE1, MCART_1, FSM_3;
notations HIDDEN, CARD_1, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, XCMPLX_0, ORDINAL1, DOMAIN_1, FUNCT_1, RELSET_1, XXREAL_0, FINSET_1, AFINSQ_1, SUBSET_1, REWRITE1, FLANG_1, STRUCT_0, NUMBERS, MCART_1, FINSEQ_1, REWRITE3;
definitions STRUCT_0;
theorems AFINSQ_1, CARD_1, FLANG_1, FUNCT_1, NAT_1, ORDINAL1, RELAT_1, RELSET_1, REWRITE1, SUBSET_1, TARSKI, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, ZFMISC_1, FINSEQ_1, FINSEQ_3, FINSEQ_5, REWRITE3, XTUPLE_0;
schemes FINSEQ_1, FRAENKEL, NAT_1, RELSET_1;
registrations CARD_1, NAT_1, XREAL_0, XBOOLE_0, XXREAL_0, STRUCT_0, SUBSET_1, REWRITE1, AFINSQ_1, RELAT_1, FINSET_1, FINSEQ_1, REWRITE3, FUNCT_1, RELSET_1, ORDINAL1, XTUPLE_0;
constructors HIDDEN, NAT_1, MEMBERED, REWRITE1, FLANG_1, XREAL_0, REWRITE3, RELSET_1, XTUPLE_0;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities ;
expansions STRUCT_0;
theorem Th1:
for
i,
k,
l being
Nat st
i >= k + l holds
i >= k
definition
let E be non
empty set ;
let F be
Subset of
(E ^omega);
let TS be non
empty transition-system over
F;
existence
ex b1 being strict transition-system over Lex E st
( the carrier of b1 = bool the carrier of TS & ( for S being Subset of TS
for w being Element of E ^omega
for T being Subset of TS holds
( [[S,w],T] in the Tran of b1 iff ( len w = 1 & T = w -succ_of (S,TS) ) ) ) )
uniqueness
for b1, b2 being strict transition-system over Lex E st the carrier of b1 = bool the carrier of TS & ( for S being Subset of TS
for w being Element of E ^omega
for T being Subset of TS holds
( [[S,w],T] in the Tran of b1 iff ( len w = 1 & T = w -succ_of (S,TS) ) ) ) & the carrier of b2 = bool the carrier of TS & ( for S being Subset of TS
for w being Element of E ^omega
for T being Subset of TS holds
( [[S,w],T] in the Tran of b2 iff ( len w = 1 & T = w -succ_of (S,TS) ) ) ) holds
b1 = b2
end;
definition
let E be non
empty set ;
let F be
Subset of
(E ^omega);
let SA be non
empty semiautomaton over
F;
existence
ex b1 being strict semiautomaton over Lex E st
( transition-system(# the carrier of b1, the Tran of b1 #) = _bool transition-system(# the carrier of SA, the Tran of SA #) & the InitS of b1 = {((<%> E) -succ_of ( the InitS of SA,SA))} )
uniqueness
for b1, b2 being strict semiautomaton over Lex E st transition-system(# the carrier of b1, the Tran of b1 #) = _bool transition-system(# the carrier of SA, the Tran of SA #) & the InitS of b1 = {((<%> E) -succ_of ( the InitS of SA,SA))} & transition-system(# the carrier of b2, the Tran of b2 #) = _bool transition-system(# the carrier of SA, the Tran of SA #) & the InitS of b2 = {((<%> E) -succ_of ( the InitS of SA,SA))} holds
b1 = b2
;
end;
definition
let E be non
empty set ;
let F be
Subset of
(E ^omega);
let A be non
empty automaton over
F;
existence
ex b1 being strict automaton over Lex E st
( semiautomaton(# the carrier of b1, the Tran of b1, the InitS of b1 #) = _bool semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) & the FinalS of b1 = { Q where Q is Element of b1 : Q meets the FinalS of A } )
uniqueness
for b1, b2 being strict automaton over Lex E st semiautomaton(# the carrier of b1, the Tran of b1, the InitS of b1 #) = _bool semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) & the FinalS of b1 = { Q where Q is Element of b1 : Q meets the FinalS of A } & semiautomaton(# the carrier of b2, the Tran of b2, the InitS of b2 #) = _bool semiautomaton(# the carrier of A, the Tran of A, the InitS of A #) & the FinalS of b2 = { Q where Q is Element of b2 : Q meets the FinalS of A } holds
b1 = b2
;
end;