begin
set SA0 = Start-At (0,SCM+FSA);
set q = (intloc 0) .--> 1;
set f = the_Values_of SCM+FSA;
begin
begin
begin
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;
begin
begin
begin
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;