environ
vocabularies HIDDEN, XBOOLE_0, AMI_1, FSM_1, CAT_1, FUNCT_1, RELAT_1, STRUCT_0, SUBSET_1, FUNCT_4, FUNCOP_1, GOBOARD5, FRECHET, AMISTD_1, ZFMISC_1, NUMBERS, CARD_1, GLIB_000, AMISTD_2, NET_1, TARSKI, AMISTD_4, QUANTAL1, GOBRD13, MEMSTR_0, COMPOS_1, ARYTM_3;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, ZFMISC_1, XTUPLE_0, MCART_1, ORDINAL1, NUMBERS, FUNCOP_1, FUNCT_4, XCMPLX_0, NAT_1, STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, FUNCT_7, MEASURE6, AMISTD_1, AMISTD_2;
definitions EXTPRO_1, AMISTD_1, XBOOLE_0;
theorems FUNCT_7, TARSKI, AMISTD_1, SUBSET_1, FUNCOP_1, ZFMISC_1, FUNCT_1, XBOOLE_0, XBOOLE_1, PARTFUN1, STRUCT_0, MEMSTR_0, MEASURE6, XTUPLE_0, NAT_1;
schemes SUBSET_1;
registrations FUNCOP_1, STRUCT_0, AMISTD_1, AMISTD_2, ORDINAL1, EXTPRO_1, ORDINAL6, FUNCT_4, MEMSTR_0, MEASURE6, NAT_1, XCMPLX_0;
constructors HIDDEN, ZFMISC_1, AMISTD_2, NAT_1, PRE_POLY, EXTPRO_1, AMISTD_1, DOMAIN_1, FUNCT_7, FUNCT_4, MEMSTR_0, RELSET_1, MEASURE6, PBOOLE, XTUPLE_0;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS;
equalities XBOOLE_0, FUNCOP_1, MEMSTR_0;
expansions XBOOLE_0;
definition
let N be
with_zero set ;
let A be non
empty with_non-empty_values IC-Ins-separated AMI-Struct over
N;
let I be
Instruction of
A;
existence
ex b1 being Subset of A st
for o being Object of A holds
( o in b1 iff for s being State of A
for a being Element of Values o holds Exec (I,s) = Exec (I,(s +* (o,a))) )
uniqueness
for b1, b2 being Subset of A st ( for o being Object of A holds
( o in b1 iff for s being State of A
for a being Element of Values o holds Exec (I,s) = Exec (I,(s +* (o,a))) ) ) & ( for o being Object of A holds
( o in b2 iff for s being State of A
for a being Element of Values o holds Exec (I,s) = Exec (I,(s +* (o,a))) ) ) holds
b1 = b2
existence
ex b1 being Subset of A st
for o being Object of A holds
( o in b1 iff ex s being State of A ex a being Element of Values o st Exec (I,(s +* (o,a))) <> (Exec (I,s)) +* (o,a) )
uniqueness
for b1, b2 being Subset of A st ( for o being Object of A holds
( o in b1 iff ex s being State of A ex a being Element of Values o st Exec (I,(s +* (o,a))) <> (Exec (I,s)) +* (o,a) ) ) & ( for o being Object of A holds
( o in b2 iff ex s being State of A ex a being Element of Values o st Exec (I,(s +* (o,a))) <> (Exec (I,s)) +* (o,a) ) ) holds
b1 = b2
end;