environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, AMI_1, SCMFSA_2, FUNCT_4, FUNCOP_1, RELAT_1, FUNCT_1, TARSKI, XBOOLE_0, CARD_1, NAT_1, ARYTM_3, FINSET_1, STRUCT_0, FSM_1, AMI_2, INT_1, PARTFUN1, FINSEQ_1, XXREAL_0, ZFMISC_1, SCMFSA6A, SCMFSA6C, GOBRD13, MEMSTR_0, SF_MASTR, SFMASTR1, SCMBSORT, CLASSES1, VALUED_0, ORDINAL1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, COMPLEX1, XXREAL_2, ENUMSET1, CARD_3, CLASSES1, INT_1, RELAT_1, FUNCT_1, NAT_1, PARTFUN1, FUNCT_2, FINSEQ_1, INT_2, NAT_D, SEQ_4, VALUED_0, RFINSEQ, FINSEQ_2, FINSET_1, FUNCT_4, DOMAIN_1, VALUED_1, AFINSQ_1, STRUCT_0, MEMSTR_0, AMI_2, AMI_3, EXTPRO_1, FUNCT_7, SCMFSA_2, FUNCOP_1, XXREAL_0;
definitions FUNCT_1, XBOOLE_0, TARSKI;
theorems FUNCT_2, RELAT_1, FUNCT_7, FUNCT_4, FUNCT_1, ZFMISC_1, FUNCOP_1, TARSKI, SCMFSA_2, MEMSTR_0, ENUMSET1, INT_1, FINSEQ_1, XBOOLE_0, XBOOLE_1, PARTFUN1, STRUCT_0, AMI_2, AMI_3, XXREAL_2, SCM_INST, GRFUNC_1, SUBSET_1, XXREAL_0, NAT_1, RFINSEQ, RELSET_1, CLASSES1, XTUPLE_0, ORDINAL1;
schemes CLASSES1, DOMAIN_1, RECDEF_1, FRAENKEL, NAT_1, FUNCT_1, RELSET_1;
registrations FUNCT_1, ORDINAL1, RELSET_1, FUNCOP_1, FINSET_1, XREAL_0, INT_1, STRUCT_0, SCMFSA_2, FUNCT_4, MEMSTR_0, AMI_3, SCM_INST, CARD_1, XXREAL_2, NAT_1, MEMBERED, AMI_5, VALUED_0;
constructors HIDDEN, WELLORD2, DOMAIN_1, XXREAL_0, INT_2, SCMFSA_2, RELSET_1, VALUED_1, AMI_3, PRE_POLY, AMISTD_1, FUNCT_7, MEMSTR_0, SCMFSA_1, XXREAL_2, SEQ_4, XXREAL_1, ENUMSET1, CLASSES1, VALUED_0, RFINSEQ;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities FUNCOP_1, SCMFSA_2, XBOOLE_0, SUBSET_1, MEMSTR_0;
expansions FUNCT_1, TARSKI;
set SA0 = Start-At (0,SCM+FSA);
set q = (intloc 0) .--> 1;
set f = the_Values_of SCM+FSA;
definition
let d be
Int-Location;
{redefine func {d} -> Subset of
Int-Locations;
coherence
{d} is Subset of Int-Locations
let e be
Int-Location;
{redefine func {d,e} -> Subset of
Int-Locations;
coherence
{d,e} is Subset of Int-Locations
let f be
Int-Location;
{redefine func {d,e,f} -> Subset of
Int-Locations;
coherence
{d,e,f} is Subset of Int-Locations
let g be
Int-Location;
{redefine func {d,e,f,g} -> Subset of
Int-Locations;
coherence
{d,e,f,g} is Subset of Int-Locations
end;
definition
existence
ex b1 being PartFunc of (FinPartSt SCM+FSA),(FinPartSt SCM+FSA) st
for p, q being FinPartState of SCM+FSA holds
( [p,q] in b1 iff ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0) .--> t & q = (fsloc 0) .--> u ) )
uniqueness
for b1, b2 being PartFunc of (FinPartSt SCM+FSA),(FinPartSt SCM+FSA) st ( for p, q being FinPartState of SCM+FSA holds
( [p,q] in b1 iff ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0) .--> t & q = (fsloc 0) .--> u ) ) ) & ( for p, q being FinPartState of SCM+FSA holds
( [p,q] in b2 iff ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0) .--> t & q = (fsloc 0) .--> u ) ) ) holds
b1 = b2
end;