:: SCMFSA_M semantic presentation

begin

   set SA0 = Start-At (0,SCM+FSA);

      set q = (intloc 0) .--> 1;

set f = the_Values_of SCM+FSA;

registration
let n be Nat;
let i be Integer;
cluster(intloc n) .--> i ->  the_Values_of SCM+FSA -compatible ;
coherence
 (intloc n) .--> i is the_Values_of SCM+FSA -compatible
proof
set q = (intloc n) .--> i;
A1: dom ((intloc n) .--> i) = {(intloc n)} by FUNCOP_1:13;
 i in INT by INT_1:def_2;
then A2: ( rng ((intloc n) .--> i) = {i} & {i} c= INT ) by FUNCOP_1:8, ZFMISC_1:31;
let x be set ; :: according to FUNCT_1:def_14 ::_thesis: ( not x in dom ((intloc n) .--> i) or ((intloc n) .--> i) . x in (the_Values_of SCM+FSA) . x )
assume A3: x in dom ((intloc n) .--> i) ; ::_thesis: ((intloc n) .--> i) . x in (the_Values_of SCM+FSA) . x
reconsider l = x as Int-Location by A1, A3, TARSKI:def_1;
A4: (the_Values_of SCM+FSA) . l = Values l
.= INT by SCMFSA_2:11 ;
 ((intloc n) .--> i) . x in rng ((intloc n) .--> i) by A3, FUNCT_1:def_3;
hence  ((intloc n) .--> i) . x in (the_Values_of SCM+FSA) . x by A4, A2; ::_thesis: verum
end;
end;

definition
let I be PartState of SCM+FSA;
func Initialized I ->  PartState of SCM+FSA equals :: SCMFSA_M:def 1
I +* (Initialize ((intloc 0) .--> 1));
coherence
 I +* (Initialize ((intloc 0) .--> 1)) is PartState of SCM+FSA ;
projectivity
 for b1, b2 being PartState of SCM+FSA st b1 = b2 +* (Initialize ((intloc 0) .--> 1)) holds
b1 = b1 +* (Initialize ((intloc 0) .--> 1))
proof
let IT, s be PartState of SCM+FSA; ::_thesis: ( IT = s +* (Initialize ((intloc 0) .--> 1)) implies IT = IT +* (Initialize ((intloc 0) .--> 1)) )
assume Z: IT = s +* (Initialize ((intloc 0) .--> 1)) ; ::_thesis: IT = IT +* (Initialize ((intloc 0) .--> 1))
 dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then A2: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def_1;
A3: s +* (Initialize ((intloc 0) .--> 1)) = Initialize (s +* ((intloc 0) .--> 1)) by FUNCT_4:14;
 dom ((intloc 0) .--> 1) = {(intloc 0)} by FUNCOP_1:13;
then A5: intloc 0 in dom ((intloc 0) .--> 1) by TARSKI:def_1;
A6: not intloc 0 in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:102;
B1: (s +* (Initialize ((intloc 0) .--> 1))) . (intloc 0) = (Initialize (s +* ((intloc 0) .--> 1))) . (intloc 0) by FUNCT_4:14
.= (s +* ((intloc 0) .--> 1)) . (intloc 0) by A6, FUNCT_4:11
.= ((intloc 0) .--> 1) . (intloc 0) by A5, FUNCT_4:13
.= 1 by FUNCOP_1:72 ;
 (Start-At (0,SCM+FSA)) . (IC ) = 0 by FUNCOP_1:72;
then B2: IC IT = 0 by Z, A2, A3, FUNCT_4:13;
A3: IC in dom IT by Z, MEMSTR_0:49;
X1: dom IT = (dom s) \/ (dom (Initialize ((intloc 0) .--> 1))) by Z, FUNCT_4:def_1;
X2: dom (Initialize ((intloc 0) .--> 1)) = (dom ((intloc 0) .--> 1)) \/ (dom (Start-At (0,SCM+FSA))) by FUNCT_4:def_1;
 dom ((intloc 0) .--> 1) = {(intloc 0)} by FUNCOP_1:13;
then  intloc 0 in dom ((intloc 0) .--> 1) by TARSKI:def_1;
then  intloc 0 in dom (Initialize ((intloc 0) .--> 1)) by X2, XBOOLE_0:def_3;
then A4: intloc 0 in dom IT by X1, XBOOLE_0:def_3;
thus IT +* (Initialize ((intloc 0) .--> 1)) = Initialize (IT +* ((intloc 0) .--> 1)) by FUNCT_4:14
.= IT +* ((IC ) .--> 0) by B1, A4, Z, FUNCT_7:109
.= IT by B2, A3, FUNCT_7:109 ; ::_thesis: verum
end;
end;

:: deftheorem  defines Initialized SCMFSA_M:def_1_:_
 for I being PartState of SCM+FSA holds Initialized I = I +* (Initialize ((intloc 0) .--> 1));

registration
let I be PartState of SCM+FSA;
cluster Initialized I ->  0 -started ;
coherence
 Initialized I is 0 -started ;
end;

registration
let I be FinPartState of SCM+FSA;
cluster Initialized I ->  finite ;
coherence
 Initialized I is finite ;
end;

scheme :: SCMFSA_M:sch 1
SCMFSAEx{ F1( set ) ->  Integer, F2( set ) ->  FinSequence of INT , F3() ->  Element of NAT } :
 ex S being State of SCM+FSA st
( IC S = F3() & ( for i being Element of NAT holds
( S . (intloc i) = F1(i) & S . (fsloc i) = F2(i) ) ) )
proof
defpred S1[ set , set ] means  ex m being Element of NAT st
( ( $1 = IC & $2 = F3() ) or ( $1 = intloc m & $2 = F1(m) ) or ( $1 = fsloc m & $2 = F2(m) ) );
A1: for e being set st e in the carrier of SCM+FSA holds
ex u being set st S1[e,u]
proof
let e be set ; ::_thesis: ( e in the carrier of SCM+FSA implies ex u being set st S1[e,u] )
assume  e in the carrier of SCM+FSA ; ::_thesis: ex u being set st S1[e,u]
then  e in (Data-Locations ) \/ {(IC )} by STRUCT_0:4;
then A2: ( e in Data-Locations or e in {(IC )} ) by XBOOLE_0:def_3;
now__::_thesis:_(_(_e_in_{(IC_)}_&_e_=_IC_)_or_(_e_in_Int-Locations_&_ex_m_being_Element_of_NAT_st_e_=_intloc_m_)_or_(_e_in_FinSeq-Locations_&_ex_m_being_Element_of_NAT_st_e_=_fsloc_m_)_)
percases ( e in {(IC )} or e in Int-Locations or e in FinSeq-Locations ) by A2, SCMFSA_2:100, XBOOLE_0:def_3;
case e in {(IC )} ; ::_thesis: e = IC
hence  e = IC by TARSKI:def_1; ::_thesis: verum
end;
case e in Int-Locations ; ::_thesis: ex m being Element of NAT st e = intloc m
then  e is Int-Location by AMI_2:def_16;
hence  ex m being Element of NAT st e = intloc m by SCMFSA_2:8; ::_thesis: verum
end;
case e in FinSeq-Locations ; ::_thesis: ex m being Element of NAT st e = fsloc m
then  e is FinSeq-Location by SCMFSA_2:def_5;
hence  ex m being Element of NAT st e = fsloc m by SCMFSA_2:9; ::_thesis: verum
end;
end;
end;
then consider m being Element of NAT  such that
A3: ( e = IC or e = intloc m or e = fsloc m ) ;
percases ( e = IC or e = intloc m or e = fsloc m ) by A3;
supposeA4: e = IC ; ::_thesis: ex u being set st S1[e,u]
take u = F3(); ::_thesis: S1[e,u]
thus  S1[e,u] by A4; ::_thesis: verum
end;
supposeA6: e = intloc m ; ::_thesis: ex u being set st S1[e,u]
take u = F1(m); ::_thesis: S1[e,u]
thus  S1[e,u] by A6; ::_thesis: verum
end;
supposeA7: e = fsloc m ; ::_thesis: ex u being set st S1[e,u]
take u = F2(m); ::_thesis: S1[e,u]
thus  S1[e,u] by A7; ::_thesis: verum
end;
end;
end;
consider f being Function such that
A8: dom f = the carrier of SCM+FSA and
A9: for e being set st e in the carrier of SCM+FSA holds
S1[e,f . e] from CLASSES1:sch_1(A1);
A10: dom the Object-Kind of SCM+FSA = the carrier of SCM+FSA by FUNCT_2:def_1;
now__::_thesis:_for_x_being_set_st_x_in_dom_the_Object-Kind_of_SCM+FSA_holds_
f_._x_in_(the_Values_of_SCM+FSA)_._x
let x be set ; ::_thesis: ( x in dom the Object-Kind of SCM+FSA implies f . b1 in (the_Values_of SCM+FSA) . b1 )
assume A11: x in dom the Object-Kind of SCM+FSA ; ::_thesis: f . b1 in (the_Values_of SCM+FSA) . b1
then consider m being Element of NAT  such that
A12: ( ( x = IC & f . x = F3() ) or ( x = intloc m & f . x = F1(m) ) or ( x = fsloc m & f . x = F2(m) ) ) by A9, A10;
 x in (Data-Locations ) \/ {(IC )} by A11, A10, STRUCT_0:4;
then A13: ( x in Data-Locations or x in {(IC )} ) by XBOOLE_0:def_3;
percases ( x in Int-Locations or x in FinSeq-Locations or x in {(IC )} ) by A13, SCMFSA_2:100, XBOOLE_0:def_3;
suppose x in Int-Locations ; ::_thesis: f . b1 in (the_Values_of SCM+FSA) . b1
then A14: x is Int-Location by AMI_2:def_16;
then (the_Values_of SCM+FSA) . x = Values (intloc m) by A12, SCMFSA_2:56, SCMFSA_2:58
.= INT by SCMFSA_2:11 ;
hence  f . x in (the_Values_of SCM+FSA) . x by A12, A14, INT_1:def_2, SCMFSA_2:58; ::_thesis: verum
end;
suppose x in FinSeq-Locations ; ::_thesis: f . b1 in (the_Values_of SCM+FSA) . b1
then A15: x is FinSeq-Location by SCMFSA_2:def_5;
then (the_Values_of SCM+FSA) . x = Values (fsloc m) by A12, SCMFSA_2:57, SCMFSA_2:58
.= INT * by SCMFSA_2:12 ;
hence  f . x in (the_Values_of SCM+FSA) . x by A12, A15, FINSEQ_1:def_11, SCMFSA_2:57, SCMFSA_2:58; ::_thesis: verum
end;
supposeA16: x in {(IC )} ; ::_thesis: f . b1 in (the_Values_of SCM+FSA) . b1
then A17: (the_Values_of SCM+FSA) . x = Values (IC ) by TARSKI:def_1
.= NAT by MEMSTR_0:def_6 ;
 x = IC by A16, TARSKI:def_1;
hence  f . x in (the_Values_of SCM+FSA) . x by A12, A17, SCMFSA_2:56, SCMFSA_2:57; ::_thesis: verum
end;
end;
end;
then reconsider f = f as State of SCM+FSA by A8, A10, FUNCT_1:def_14, PARTFUN1:def_2, RELAT_1:def_18;
take  f ; ::_thesis: ( IC f = F3() & ( for i being Element of NAT holds
( f . (intloc i) = F1(i) & f . (fsloc i) = F2(i) ) ) )
 ex m being Element of NAT st
( ( IC = IC & f . (IC ) = F3() ) or ( IC = intloc m & f . (IC ) = F1(m) ) or ( IC = fsloc m & f . (IC ) = F2(m) ) ) by A9;
hence  IC f = F3() by SCMFSA_2:56, SCMFSA_2:57; ::_thesis: for i being Element of NAT holds
( f . (intloc i) = F1(i) & f . (fsloc i) = F2(i) )
let i be Element of NAT ; ::_thesis: ( f . (intloc i) = F1(i) & f . (fsloc i) = F2(i) )
 ex m being Element of NAT st
( ( intloc i = IC & f . (intloc i) = F3() ) or ( intloc i = intloc m & f . (intloc i) = F1(m) ) or ( intloc i = fsloc m & f . (intloc i) = F2(m) ) ) by A9;
hence  f . (intloc i) = F1(i) by AMI_3:10, SCMFSA_2:56, SCMFSA_2:58; ::_thesis: f . (fsloc i) = F2(i)
 ex m being Element of NAT st
( ( fsloc i = IC & f . (fsloc i) = F3() ) or ( fsloc i = intloc m & f . (fsloc i) = F1(m) ) or ( fsloc i = fsloc m & f . (fsloc i) = F2(m) ) ) by A9;
hence  f . (fsloc i) = F2(i) by SCMFSA_2:57, SCMFSA_2:58; ::_thesis: verum
end;

theorem Th1: :: SCMFSA_M:1
for s being State of SCM+FSA
for x being set holds
( not x in dom s or x is Int-Location or x is FinSeq-Location or x = IC )
proof
let s be State of SCM+FSA; ::_thesis: for x being set holds
( not x in dom s or x is Int-Location or x is FinSeq-Location or x = IC )
let x be set ; ::_thesis: ( not x in dom s or x is Int-Location or x is FinSeq-Location or x = IC )
assume A1: x in dom s ; ::_thesis: ( x is Int-Location or x is FinSeq-Location or x = IC )
 x in (Data-Locations ) \/ {(IC )} by A1, MEMSTR_0:13;
then  ( x in Data-Locations or x in {(IC )} ) by XBOOLE_0:def_3;
then  ( x in Int-Locations or x in FinSeq-Locations or x = IC ) by SCMFSA_2:100, TARSKI:def_1, XBOOLE_0:def_3;
hence  ( x is Int-Location or x is FinSeq-Location or x = IC ) by AMI_2:def_16, SCMFSA_2:def_5; ::_thesis: verum
end;

theorem :: SCMFSA_M:2
for s1, s2 being State of SCM+FSA holds
( ( ( for a being Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) ) iff DataPart s1 = DataPart s2 )
proof
let s1, s2 be State of SCM+FSA; ::_thesis: ( ( ( for a being Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) ) iff DataPart s1 = DataPart s2 )
A2: now__::_thesis:_(_(_for_a_being_Int-Location_holds_s1_._a_=_s2_._a_)_&_(_for_f_being_FinSeq-Location_holds_s1_._f_=_s2_._f_)_implies_for_x_being_set_st_x_in_Data-Locations_holds_
s1_._x_=_s2_._x_)
assume that
A3: for a being Int-Location holds s1 . a = s2 . a and
A4: for f being FinSeq-Location holds s1 . f = s2 . f ; ::_thesis: for x being set st x in Data-Locations holds
s1 . x = s2 . x
hereby  ::_thesis: verum
let x be set ; ::_thesis: ( x in Data-Locations implies s1 . b1 = s2 . b1 )
assume A5: x in Data-Locations ; ::_thesis: s1 . b1 = s2 . b1
percases ( x in Int-Locations or not x in Int-Locations ) ;
suppose x in Int-Locations ; ::_thesis: s1 . b1 = s2 . b1
then  x is Int-Location by AMI_2:def_16;
hence  s1 . x = s2 . x by A3; ::_thesis: verum
end;
suppose not x in Int-Locations ; ::_thesis: s1 . b1 = s2 . b1
then  x in FinSeq-Locations by A5, SCMFSA_2:100, XBOOLE_0:def_3;
then  x is FinSeq-Location by SCMFSA_2:def_5;
hence  s1 . x = s2 . x by A4; ::_thesis: verum
end;
end;
end;
end;
A6: now__::_thesis:_(_(_for_x_being_set_st_x_in_Data-Locations_holds_
s1_._x_=_s2_._x_)_implies_(_(_for_a_being_Int-Location_holds_s1_._a_=_s2_._a_)_&_(_for_f_being_FinSeq-Location_holds_s1_._f_=_s2_._f_)_)_)
assume A7: for x being set st x in Data-Locations holds
s1 . x = s2 . x ; ::_thesis: ( ( for a being Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) )
hereby  ::_thesis: for f being FinSeq-Location holds s1 . f = s2 . f
let a be Int-Location; ::_thesis: s1 . a = s2 . a
 a in Int-Locations by AMI_2:def_16;
then  a in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
hence  s1 . a = s2 . a by A7; ::_thesis: verum
end;
hereby  ::_thesis: verum
let f be FinSeq-Location ; ::_thesis: s1 . f = s2 . f
 f in FinSeq-Locations by SCMFSA_2:def_5;
then  f in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3;
hence  s1 . f = s2 . f by A7; ::_thesis: verum
end;
end;
 dom s2 = (Data-Locations ) \/ {(IC )} by MEMSTR_0:13;
then A8: Data-Locations c= dom s2 by XBOOLE_1:7;
 dom s1 = (Data-Locations ) \/ {(IC )} by MEMSTR_0:13;
then  Data-Locations c= dom s1 by XBOOLE_1:7;
hence  ( ( ( for a being Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) ) iff DataPart s1 = DataPart s2 ) by A8, A2, A6, FUNCT_1:95; ::_thesis: verum
end;

theorem Th43: :: SCMFSA_M:3
for p being PartState of SCM+FSA holds dom (Initialized p) = ((dom p) \/ {(intloc 0)}) \/ {(IC )}
proof
let p be PartState of SCM+FSA; ::_thesis: dom (Initialized p) = ((dom p) \/ {(intloc 0)}) \/ {(IC )}
A1: ( dom ((intloc 0) .--> 1) = {(intloc 0)} & dom (Start-At (0,SCM+FSA)) = {(IC )} ) by FUNCOP_1:13;
 Initialized p = Initialize (p +* ((intloc 0) .--> 1)) by FUNCT_4:14;
hence  dom (Initialized p) = (dom (p +* ((intloc 0) .--> 1))) \/ (dom (Start-At (0,SCM+FSA))) by FUNCT_4:def_1
.= ((dom p) \/ {(intloc 0)}) \/ {(IC )} by A1, FUNCT_4:def_1 ;
::_thesis: verum
end;

registration
let s be State of SCM+FSA;
cluster Initialized s ->  total ;
coherence
 Initialized s is total ;
end;

theorem Th4: :: SCMFSA_M:4
for p being PartState of SCM+FSA holds intloc 0 in dom (Initialized p)
proof
let p be PartState of SCM+FSA; ::_thesis: intloc 0 in dom (Initialized p)
A1: ( dom ((intloc 0) .--> 1) = {(intloc 0)} & dom (Start-At (0,SCM+FSA)) = {(IC )} ) by FUNCOP_1:13;
 intloc 0 in {(intloc 0)} by TARSKI:def_1;
then A2: intloc 0 in (dom p) \/ {(intloc 0)} by XBOOLE_0:def_3;
 Initialized p = Initialize (p +* ((intloc 0) .--> 1)) by FUNCT_4:14;
then  dom (Initialized p) = (dom (p +* ((intloc 0) .--> 1))) \/ (dom (Start-At (0,SCM+FSA))) by FUNCT_4:def_1
.= ((dom p) \/ {(intloc 0)}) \/ {(IC )} by A1, FUNCT_4:def_1 ;
hence  intloc 0 in dom (Initialized p) by A2, XBOOLE_0:def_3; ::_thesis: verum
end;

theorem :: SCMFSA_M:5
for p being PartState of SCM+FSA holds
( (Initialized p) . (intloc 0) = 1 & (Initialized p) . (IC ) = 0 )
proof
let p be PartState of SCM+FSA; ::_thesis: ( (Initialized p) . (intloc 0) = 1 & (Initialized p) . (IC ) = 0 )
 intloc 0 in {(intloc 0)} by TARSKI:def_1;
then A1: intloc 0 in dom ((intloc 0) .--> 1) by FUNCOP_1:13;
A2: Initialized p = Initialize (p +* ((intloc 0) .--> 1)) by FUNCT_4:14;
 intloc 0 <> IC by SCMFSA_2:56;
then  not intloc 0 in {(IC )} by TARSKI:def_1;
then  not intloc 0 in dom (Start-At (0,SCM+FSA)) by FUNCOP_1:13;
hence (Initialized p) . (intloc 0) = (p +* ((intloc 0) .--> 1)) . (intloc 0) by A2, FUNCT_4:11
.= ((intloc 0) .--> 1) . (intloc 0) by A1, FUNCT_4:13
.= 1 by FUNCOP_1:72 ;
::_thesis: (Initialized p) . (IC ) = 0
 IC in {(IC )} by TARSKI:def_1;
then  IC in dom (Start-At (0,SCM+FSA)) by FUNCOP_1:13;
hence (Initialized p) . (IC ) = (Start-At (0,SCM+FSA)) . (IC ) by A2, FUNCT_4:13
.= 0 by FUNCOP_1:72 ;
::_thesis: verum
end;

theorem :: SCMFSA_M:6
for p being PartState of SCM+FSA
for a being Int-Location st a <> intloc 0 & not a in dom p holds
not a in dom (Initialized p)
proof
let p be PartState of SCM+FSA; ::_thesis: for a being Int-Location st a <> intloc 0 & not a in dom p holds
not a in dom (Initialized p)
let a be Int-Location; ::_thesis: ( a <> intloc 0 & not a in dom p implies not a in dom (Initialized p) )
assume that
A1: a <> intloc 0 and
Z: not a in dom p ; ::_thesis: not a in dom (Initialized p)
assume  a in dom (Initialized p) ; ::_thesis: contradiction
then  a in ((dom p) \/ {(intloc 0)}) \/ {(IC )} by Th43;
then A2: ( a in (dom p) \/ {(intloc 0)} or a in {(IC )} ) by XBOOLE_0:def_3;
percases ( a in {(intloc 0)} or a in {(IC )} ) by A2, Z, XBOOLE_0:def_3;
suppose a in {(intloc 0)} ; ::_thesis: contradiction
hence  contradiction by A1, TARSKI:def_1; ::_thesis: verum
end;
suppose a in {(IC )} ; ::_thesis: contradiction
then  a = IC by TARSKI:def_1;
hence  contradiction by SCMFSA_2:56; ::_thesis: verum
end;
end;
end;

theorem :: SCMFSA_M:7
for p being PartState of SCM+FSA
for f being FinSeq-Location st not f in dom p holds
not f in dom (Initialized p)
proof
let p be PartState of SCM+FSA; ::_thesis: for f being FinSeq-Location st not f in dom p holds
not f in dom (Initialized p)
let f be FinSeq-Location ; ::_thesis: ( not f in dom p implies not f in dom (Initialized p) )
assume Z: not f in dom p ; ::_thesis: not f in dom (Initialized p)
assume  f in dom (Initialized p) ; ::_thesis: contradiction
then  f in ((dom p) \/ {(intloc 0)}) \/ {(IC )} by Th43;
then A1: ( f in (dom p) \/ {(intloc 0)} or f in {(IC )} ) by XBOOLE_0:def_3;
percases ( f in {(intloc 0)} or f in {(IC )} ) by A1, Z, XBOOLE_0:def_3;
suppose f in {(intloc 0)} ; ::_thesis: contradiction
then  f = intloc 0 by TARSKI:def_1;
hence  contradiction by SCMFSA_2:58; ::_thesis: verum
end;
suppose f in {(IC )} ; ::_thesis: contradiction
then  f = IC by TARSKI:def_1;
hence  contradiction by SCMFSA_2:57; ::_thesis: verum
end;
end;
end;

theorem :: SCMFSA_M:8
for s being State of SCM+FSA st s . (intloc 0) = 1 & IC s = 0 holds
Initialized s = s
proof
let s be State of SCM+FSA; ::_thesis: ( s . (intloc 0) = 1 & IC s = 0 implies Initialized s = s )
assume A1: s . (intloc 0) = 1 ; ::_thesis: ( not IC s = 0 or Initialized s = s )
assume A2: IC s = 0 ; ::_thesis: Initialized s = s
A3: IC in dom s by MEMSTR_0:2;
A4: intloc 0 in dom s by SCMFSA_2:42;
thus  Initialized s = Initialize (s +* ((intloc 0) .--> 1)) by FUNCT_4:14
.= s +* ((IC ) .--> 0) by A1, A4, FUNCT_7:109
.= s by A2, A3, FUNCT_7:109 ; ::_thesis: verum
end;

theorem :: SCMFSA_M:9
for p being PartState of SCM+FSA holds (Initialized p) . (intloc 0) = 1
proof
let p be PartState of SCM+FSA; ::_thesis: (Initialized p) . (intloc 0) = 1
A1: ((intloc 0) .--> 1) . (intloc 0) = 1 by FUNCOP_1:72;
A3: Initialized p = Initialize (p +* ((intloc 0) .--> 1)) by FUNCT_4:14;
 dom ((intloc 0) .--> 1) = {(intloc 0)} by FUNCOP_1:13;
then A5: intloc 0 in dom ((intloc 0) .--> 1) by TARSKI:def_1;
 not intloc 0 in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:102;
hence (Initialized p) . (intloc 0) = (p +* ((intloc 0) .--> 1)) . (intloc 0) by A3, FUNCT_4:11
.= 1 by A5, A1, FUNCT_4:13 ;
::_thesis: verum
end;

theorem Th10: :: SCMFSA_M:10
intloc 0 in dom (Initialize ((intloc 0) .--> 1))
proof
A: dom (Initialize ((intloc 0) .--> 1)) = (dom (Start-At (0,SCM+FSA))) \/ (dom ((intloc 0) .--> 1)) by FUNCT_4:def_1;
 dom ((intloc 0) .--> 1) = {(intloc 0)} by FUNCOP_1:13;
then  intloc 0 in dom ((intloc 0) .--> 1) by TARSKI:def_1;
hence  intloc 0 in dom (Initialize ((intloc 0) .--> 1)) by A, XBOOLE_0:def_3; ::_thesis: verum
end;

theorem Th11: :: SCMFSA_M:11
dom (Initialize ((intloc 0) .--> 1)) = {(intloc 0),(IC )}
proof
thus  dom (Initialize ((intloc 0) .--> 1)) = (dom ((intloc 0) .--> 1)) \/ (dom (Start-At (0,SCM+FSA))) by FUNCT_4:def_1
.= (dom ((intloc 0) .--> 1)) \/ {(IC )} by FUNCOP_1:13
.= {(intloc 0)} \/ {(IC )} by FUNCOP_1:13
.= {(intloc 0),(IC )} by ENUMSET1:1 ; ::_thesis: verum
end;

theorem Th12: :: SCMFSA_M:12
(Initialize ((intloc 0) .--> 1)) . (intloc 0) = 1
proof
 not intloc 0 in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:102;
hence (Initialize ((intloc 0) .--> 1)) . (intloc 0) = ((intloc 0) .--> 1) . (intloc 0) by FUNCT_4:11
.= 1 by FUNCOP_1:72 ;
::_thesis: verum
end;

theorem :: SCMFSA_M:13
for p being PartState of SCM+FSA holds Initialize ((intloc 0) .--> 1) c= Initialized p by FUNCT_4:25;

begin

registration
cluster Int-Locations  ->  non empty ;
coherence
 not Int-Locations is empty ;
end;

definition
let IT be Int-Location;
attrIT is read-only  means :Def2: :: SCMFSA_M:def 2
IT = intloc 0;
end;

:: deftheorem Def2 defines read-only SCMFSA_M:def_2_:_
 for IT being Int-Location holds
( IT is read-only iff IT = intloc 0 );

notation
let IT be Int-Location;
antonym  read-write IT for  read-only ;
end;

registration
cluster intloc 0 ->  read-only ;
coherence
 intloc 0 is read-only by Def2;
end;

registration
cluster Int-like read-write for Element of the carrier of SCM+FSA;
existence
 ex b1 being Int-Location st b1 is read-write
proof
take  intloc 1 ; ::_thesis: intloc 1 is read-write
 intloc 1 <> intloc 0 by AMI_3:10;
hence  intloc 1 is read-write by Def2; ::_thesis: verum
end;
end;

definition
let L be finite Subset of Int-Locations;
func FirstNotIn L ->  Int-Location means :Def6: :: SCMFSA_M:def 3
 ex sn being non empty Subset of NAT st
( it = intloc (min sn) & sn =  {  k where k is Element of NAT : not intloc k in L  }  );
existence
 ex b1 being Int-Location ex sn being non empty Subset of NAT st
( b1 = intloc (min sn) & sn =  {  k where k is Element of NAT : not intloc k in L  }  )
proof
defpred S1[ Element of NAT ] means  not intloc $1 in L;
set sn =  {  k where k is Element of NAT : S1[k]  }  ;
A1:  {  k where k is Element of NAT : S1[k]  }  is Subset of NAT from DOMAIN_1:sch_7();
 Int-Locations = [:{1},NAT:] by SCM_INST:def_1;
then  not Int-Locations c= L ;
then consider x being set  such that
A2: x in Int-Locations and
A3: not x in L by TARSKI:def_3;
reconsider x = x as Int-Location by A2, AMI_2:def_16;
consider k being Element of NAT  such that
A4: x = intloc k by SCMFSA_2:8;
 k in  {  k where k is Element of NAT : S1[k]  }  by A3, A4;
then reconsider sn =  {  k where k is Element of NAT : S1[k]  }  as non empty Subset of NAT by A1;
take  intloc (min sn) ; ::_thesis: ex sn being non empty Subset of NAT st
( intloc (min sn) = intloc (min sn) & sn =  {  k where k is Element of NAT : not intloc k in L  }  )
take  sn ; ::_thesis: ( intloc (min sn) = intloc (min sn) & sn =  {  k where k is Element of NAT : not intloc k in L  }  )
thus  ( intloc (min sn) = intloc (min sn) & sn =  {  k where k is Element of NAT : not intloc k in L  }  ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Int-Location st ex sn being non empty Subset of NAT st
( b1 = intloc (min sn) & sn =  {  k where k is Element of NAT : not intloc k in L  }  ) & ex sn being non empty Subset of NAT st
( b2 = intloc (min sn) & sn =  {  k where k is Element of NAT : not intloc k in L  }  ) holds
b1 = b2 ;
end;

:: deftheorem Def6 defines FirstNotIn SCMFSA_M:def_3_:_
 for L being finite Subset of Int-Locations
for b2 being Int-Location holds
( b2 = FirstNotIn L iff ex sn being non empty Subset of NAT st
( b2 = intloc (min sn) & sn =  {  k where k is Element of NAT : not intloc k in L  }  ) );

theorem :: SCMFSA_M:14
for L being finite Subset of Int-Locations holds not FirstNotIn L in L
proof
let L be finite Subset of Int-Locations; ::_thesis: not FirstNotIn L in L
set FNI = FirstNotIn L;
consider sn being non empty Subset of NAT such that
A1: FirstNotIn L = intloc (min sn) and
A2: sn =  {  k where k is Element of NAT : not intloc k in L  }  by Def6;
 min sn in sn by XXREAL_2:def_7;
then  ex k being Element of NAT st
( k = min sn & not intloc k in L ) by A2;
hence  not FirstNotIn L in L by A1; ::_thesis: verum
end;

theorem :: SCMFSA_M:15
for m, n being Element of NAT
for L being finite Subset of Int-Locations st FirstNotIn L = intloc m & not intloc n in L holds
m <= n
proof
let m, n be Element of NAT ; ::_thesis: for L being finite Subset of Int-Locations st FirstNotIn L = intloc m & not intloc n in L holds
m <= n
let L be finite Subset of Int-Locations; ::_thesis: ( FirstNotIn L = intloc m & not intloc n in L implies m <= n )
consider sn being non empty Subset of NAT such that
A1: ( FirstNotIn L = intloc (min sn) & sn =  {  k where k is Element of NAT : not intloc k in L  }  ) by Def6;
assume  ( FirstNotIn L = intloc m & not intloc n in L ) ; ::_thesis: m <= n
then  ( m = min sn & n in sn ) by A1, AMI_3:10;
hence  m <= n by XXREAL_2:def_7; ::_thesis: verum
end;

definition
let L be finite Subset of FinSeq-Locations;
func First*NotIn L ->  FinSeq-Location  means :Def8: :: SCMFSA_M:def 4
 ex sn being non empty Subset of NAT st
( it = fsloc (min sn) & sn =  {  k where k is Element of NAT : not fsloc k in L  }  );
existence
 ex b1 being FinSeq-Location ex sn being non empty Subset of NAT st
( b1 = fsloc (min sn) & sn =  {  k where k is Element of NAT : not fsloc k in L  }  )
proof
defpred S1[ Element of NAT ] means  not fsloc $1 in L;
set sn =  {  k where k is Element of NAT : S1[k]  }  ;
A1:  {  k where k is Element of NAT : S1[k]  }  is Subset of NAT from DOMAIN_1:sch_7();
 not FinSeq-Locations c= L ;
then consider x being set  such that
A2: x in FinSeq-Locations and
A3: not x in L by TARSKI:def_3;
reconsider x = x as FinSeq-Location by A2, SCMFSA_2:def_5;
consider k being Element of NAT  such that
A4: x = fsloc k by SCMFSA_2:9;
 k in  {  k where k is Element of NAT : S1[k]  }  by A3, A4;
then reconsider sn =  {  k where k is Element of NAT : S1[k]  }  as non empty Subset of NAT by A1;
take  fsloc (min sn) ; ::_thesis: ex sn being non empty Subset of NAT st
( fsloc (min sn) = fsloc (min sn) & sn =  {  k where k is Element of NAT : not fsloc k in L  }  )
take  sn ; ::_thesis: ( fsloc (min sn) = fsloc (min sn) & sn =  {  k where k is Element of NAT : not fsloc k in L  }  )
thus  ( fsloc (min sn) = fsloc (min sn) & sn =  {  k where k is Element of NAT : not fsloc k in L  }  ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being FinSeq-Location st ex sn being non empty Subset of NAT st
( b1 = fsloc (min sn) & sn =  {  k where k is Element of NAT : not fsloc k in L  }  ) & ex sn being non empty Subset of NAT st
( b2 = fsloc (min sn) & sn =  {  k where k is Element of NAT : not fsloc k in L  }  ) holds
b1 = b2 ;
end;

:: deftheorem Def8 defines First*NotIn SCMFSA_M:def_4_:_
 for L being finite Subset of FinSeq-Locations
for b2 being FinSeq-Location holds
( b2 = First*NotIn L iff ex sn being non empty Subset of NAT st
( b2 = fsloc (min sn) & sn =  {  k where k is Element of NAT : not fsloc k in L  }  ) );

theorem :: SCMFSA_M:16
for L being finite Subset of FinSeq-Locations holds not First*NotIn L in L
proof
let L be finite Subset of FinSeq-Locations; ::_thesis: not First*NotIn L in L
set FNI = First*NotIn L;
consider sn being non empty Subset of NAT such that
A1: First*NotIn L = fsloc (min sn) and
A2: sn =  {  k where k is Element of NAT : not fsloc k in L  }  by Def8;
 min sn in sn by XXREAL_2:def_7;
then  ex k being Element of NAT st
( k = min sn & not fsloc k in L ) by A2;
hence  not First*NotIn L in L by A1; ::_thesis: verum
end;

theorem :: SCMFSA_M:17
for m, n being Element of NAT
for L being finite Subset of FinSeq-Locations st First*NotIn L = fsloc m & not fsloc n in L holds
m <= n
proof
let m, n be Element of NAT ; ::_thesis: for L being finite Subset of FinSeq-Locations st First*NotIn L = fsloc m & not fsloc n in L holds
m <= n
let L be finite Subset of FinSeq-Locations; ::_thesis: ( First*NotIn L = fsloc m & not fsloc n in L implies m <= n )
assume that
A1: First*NotIn L = fsloc m and
A2: not fsloc n in L ; ::_thesis: m <= n
consider sn being non empty Subset of NAT such that
A3: First*NotIn L = fsloc (min sn) and
A4: sn =  {  k where k is Element of NAT : not fsloc k in L  }  by Def8;
 n in sn by A2, A4;
hence  m <= n by A1, A3, XXREAL_2:def_7; ::_thesis: verum
end;

registration
let s be State of SCM+FSA;
let li be Int-Location;
let k be Integer;
clusters +* (li,k) ->  the_Values_of SCM+FSA -compatible ;
coherence
 s +* (li,k) is the_Values_of SCM+FSA -compatible
proof
let x be set ; :: according to FUNCT_1:def_14 ::_thesis: ( not x in dom (s +* (li,k)) or (s +* (li,k)) . x in (the_Values_of SCM+FSA) . x )
assume  x in dom (s +* (li,k)) ; ::_thesis: (s +* (li,k)) . x in (the_Values_of SCM+FSA) . x
then A2: x in dom s by FUNCT_7:30;
percases ( x = li or x <> li ) ;
supposeA3: x = li ; ::_thesis: (s +* (li,k)) . x in (the_Values_of SCM+FSA) . x
then A4: (the_Values_of SCM+FSA) . x = Values li
.= INT by SCMFSA_2:11 ;
 (s +* (li,k)) . x = k by A3, A2, FUNCT_7:31;
hence  (s +* (li,k)) . x in (the_Values_of SCM+FSA) . x by A4, INT_1:def_2; ::_thesis: verum
end;
suppose x <> li ; ::_thesis: (s +* (li,k)) . x in (the_Values_of SCM+FSA) . x
then  (s +* (li,k)) . x = s . x by FUNCT_7:32;
hence  (s +* (li,k)) . x in (the_Values_of SCM+FSA) . x by A2, FUNCT_1:def_14; ::_thesis: verum
end;
end;
end;
end;

begin

registration
let a be Int-Location;
let n be Nat;
clustera .--> n ->  data-only for PartState of SCM+FSA;
coherence
 for b1 being PartState of SCM+FSA st b1 = a .--> n holds
b1 is data-only ;
end;

theorem :: SCMFSA_M:18
for s being State of SCM+FSA st s . (intloc 0) = 1 holds
Initialize s = Initialized s
proof
let s be State of SCM+FSA; ::_thesis: ( s . (intloc 0) = 1 implies Initialize s = Initialized s )
A1: intloc 0 in dom s by SCMFSA_2:42;
assume  s . (intloc 0) = 1 ; ::_thesis: Initialize s = Initialized s
then A2: s = s +* ((intloc 0) .--> 1) by A1, FUNCT_7:109;
thus  Initialized s = Initialize s by A2, FUNCT_4:14; ::_thesis: verum
end;

theorem :: SCMFSA_M:19
for s being State of SCM+FSA st s . (intloc 0) = 1 holds
DataPart (Initialized s) = DataPart s
proof
let s be State of SCM+FSA; ::_thesis: ( s . (intloc 0) = 1 implies DataPart (Initialized s) = DataPart s )
assume A1: s . (intloc 0) = 1 ; ::_thesis: DataPart (Initialized s) = DataPart s
A2: intloc 0 in dom s by SCMFSA_2:42;
 Initialized s = Initialize (s +* ((intloc 0) .--> 1)) by FUNCT_4:14;
then  Initialized s = Initialize s by A1, A2, FUNCT_7:109;
hence  DataPart (Initialized s) = DataPart s by MEMSTR_0:79; ::_thesis: verum
end;

theorem :: SCMFSA_M:20
for s1, s2 being State of SCM+FSA st s1 . (intloc 0) = s2 . (intloc 0) & ( for a being read-write Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) holds
DataPart s1 = DataPart s2
proof
let s1, s2 be State of SCM+FSA; ::_thesis: ( s1 . (intloc 0) = s2 . (intloc 0) & ( for a being read-write Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) implies DataPart s1 = DataPart s2 )
set D = Data-Locations ;
assume A1: s1 . (intloc 0) = s2 . (intloc 0) ; ::_thesis: ( ex a being read-write Int-Location st not s1 . a = s2 . a or ex f being FinSeq-Location st not s1 . f = s2 . f or DataPart s1 = DataPart s2 )
assume A2: for a being read-write Int-Location holds s1 . a = s2 . a ; ::_thesis: ( ex f being FinSeq-Location st not s1 . f = s2 . f or DataPart s1 = DataPart s2 )
A3: dom (DataPart s1) = (dom s1) /\ (Data-Locations ) by RELAT_1:61
.= ((Data-Locations ) \/ {(IC )}) /\ (Data-Locations ) by MEMSTR_0:13
.= (dom s2) /\ (Data-Locations ) by MEMSTR_0:13
.= dom (DataPart s2) by RELAT_1:61 ;
assume A4: for f being FinSeq-Location holds s1 . f = s2 . f ; ::_thesis: DataPart s1 = DataPart s2
now__::_thesis:_for_x_being_set_st_x_in_dom_(DataPart_s1)_holds_
(DataPart_s1)_._x_=_(DataPart_s2)_._x
let x be set ; ::_thesis: ( x in dom (DataPart s1) implies (DataPart s1) . b1 = (DataPart s2) . b1 )
assume A5: x in dom (DataPart s1) ; ::_thesis: (DataPart s1) . b1 = (DataPart s2) . b1
then A6: x in (dom s1) /\ (Data-Locations ) by RELAT_1:61;
then A7: x in dom s1 by XBOOLE_0:def_4;
percases ( x is Int-Location or x is FinSeq-Location or x = IC ) by A7, Th1;
supposeA9: x is Int-Location ; ::_thesis: (DataPart s1) . b1 = (DataPart s2) . b1
hereby  ::_thesis: verum
percases ( x is read-write Int-Location or not x is read-write Int-Location ) ;
supposeA10: x is read-write Int-Location ; ::_thesis: (DataPart s1) . x = (DataPart s2) . x
thus (DataPart s1) . x = s1 . x by A5, FUNCT_1:47
.= s2 . x by A2, A10
.= (DataPart s2) . x by A3, A5, FUNCT_1:47 ; ::_thesis: verum
end;
supposeA11: x is not read-write Int-Location ; ::_thesis: (DataPart s1) . x = (DataPart s2) . x
reconsider a = x as Int-Location by A9;
 a = intloc 0 by A11, Def2;
hence (DataPart s1) . x = s2 . a by A1, A5, FUNCT_1:47
.= (DataPart s2) . x by A3, A5, FUNCT_1:47 ;
::_thesis: verum
end;
end;
end;
end;
supposeA12: x is FinSeq-Location ; ::_thesis: (DataPart s1) . b1 = (DataPart s2) . b1
thus (DataPart s1) . x = s1 . x by A5, FUNCT_1:47
.= s2 . x by A4, A12
.= (DataPart s2) . x by A3, A5, FUNCT_1:47 ; ::_thesis: verum
end;
suppose x = IC ; ::_thesis: (DataPart s1) . b1 = (DataPart s2) . b1
then  not x in Data-Locations by STRUCT_0:3;
hence  (DataPart s1) . x = (DataPart s2) . x by A6, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
end;
then  DataPart s1 c= DataPart s2 by A3, GRFUNC_1:2;
hence  DataPart s1 = DataPart s2 by A3, GRFUNC_1:3; ::_thesis: verum
end;

theorem :: SCMFSA_M:21
for s being State of SCM+FSA
for a being Int-Location
for l being Element of NAT holds (s +* (Start-At (l,SCM+FSA))) . a = s . a
proof
let s be State of SCM+FSA; ::_thesis: for a being Int-Location
for l being Element of NAT holds (s +* (Start-At (l,SCM+FSA))) . a = s . a
let a be Int-Location; ::_thesis: for l being Element of NAT holds (s +* (Start-At (l,SCM+FSA))) . a = s . a
let l be Element of NAT ; ::_thesis: (s +* (Start-At (l,SCM+FSA))) . a = s . a
 not a in dom (Start-At (l,SCM+FSA)) by SCMFSA_2:102;
hence  (s +* (Start-At (l,SCM+FSA))) . a = s . a by FUNCT_4:11; ::_thesis: verum
end;

begin

definition
let d be Int-Location;
:: original: {
redefine func{d} ->  Subset of Int-Locations;
coherence
 {d} is Subset of Int-Locations
proof
 d in SCM-Data-Loc by AMI_2:def_16;
hence  {d} is Subset of Int-Locations by SUBSET_1:33; ::_thesis: verum
end;
let e be Int-Location;
:: original: {
redefine func{d,e} ->  Subset of Int-Locations;
coherence
 {d,e} is Subset of Int-Locations
proof
A1: e in SCM-Data-Loc by AMI_2:def_16;
 d in SCM-Data-Loc by AMI_2:def_16;
hence  {d,e} is Subset of Int-Locations by A1, SUBSET_1:34; ::_thesis: verum
end;
let f be Int-Location;
:: original: {
redefine func{d,e,f} ->  Subset of Int-Locations;
coherence
 {d,e,f} is Subset of Int-Locations
proof
A2: f in SCM-Data-Loc by AMI_2:def_16;
A3: e in SCM-Data-Loc by AMI_2:def_16;
 d in SCM-Data-Loc by AMI_2:def_16;
hence  {d,e,f} is Subset of Int-Locations by A3, A2, SUBSET_1:35; ::_thesis: verum
end;
let g be Int-Location;
:: original: {
redefine func{d,e,f,g} ->  Subset of Int-Locations;
coherence
 {d,e,f,g} is Subset of Int-Locations
proof
A4: g in SCM-Data-Loc by AMI_2:def_16;
A5: f in SCM-Data-Loc by AMI_2:def_16;
A6: e in SCM-Data-Loc by AMI_2:def_16;
 d in SCM-Data-Loc by AMI_2:def_16;
hence  {d,e,f,g} is Subset of Int-Locations by A6, A5, A4, SUBSET_1:36; ::_thesis: verum
end;
end;

definition
let L be finite Subset of Int-Locations;
func RWNotIn-seq L ->  Function of NAT,(bool NAT) means :Def2: :: SCMFSA_M:def 5
( it . 0 =  {  k where k is Element of NAT : ( not intloc k in L & k <> 0 )  }  & ( for i being Element of NAT
for sn being non empty Subset of NAT st it . i = sn holds
it . (i + 1) = sn \ {(min sn)} ) & ( for i being Element of NAT holds it . i is infinite ) );
existence
 ex b1 being Function of NAT,(bool NAT) st
( b1 . 0 =  {  k where k is Element of NAT : ( not intloc k in L & k <> 0 )  }  & ( for i being Element of NAT
for sn being non empty Subset of NAT st b1 . i = sn holds
b1 . (i + 1) = sn \ {(min sn)} ) & ( for i being Element of NAT holds b1 . i is infinite ) )
proof
set M = L \/ {(intloc 0)};
defpred S1[ Element of NAT ] means ( not intloc $1 in L & $1 <> 0 );
set sn =  {  k where k is Element of NAT : S1[k]  }  ;
A1:  {  k where k is Element of NAT : S1[k]  }  is Subset of NAT from DOMAIN_1:sch_7();
 not Int-Locations c= L \/ {(intloc 0)} by AMI_3:27;
then consider x being set  such that
A2: x in Int-Locations and
A3: not x in L \/ {(intloc 0)} by TARSKI:def_3;
reconsider x = x as Int-Location by A2, AMI_2:def_16;
consider k being Element of NAT  such that
A4: x = intloc k by SCMFSA_2:8;
 not intloc k in {(intloc 0)} by A3, A4, XBOOLE_0:def_3;
then A5: k <> 0 by TARSKI:def_1;
 not intloc k in L by A3, A4, XBOOLE_0:def_3;
then  k in  {  k where k is Element of NAT : S1[k]  }  by A5;
then reconsider sn =  {  k where k is Element of NAT : S1[k]  }  as non empty Subset of NAT by A1;
defpred S2[ Element of NAT , Subset of NAT, Subset of NAT] means  for N being non empty Subset of NAT st N = $2 holds
$3 = $2 \ {(min N)};
A6: now__::_thesis:_for_n_being_Element_of_NAT_
for_x_being_Subset_of_NAT_ex_y_being_Subset_of_NAT_st_S2[n,x,y]
let n be Element of NAT ; ::_thesis: for x being Subset of NAT ex y being Subset of NAT st S2[y,b3,b4]
let x be Subset of NAT; ::_thesis: ex y being Subset of NAT st S2[y,b2,b3]
percases ( x is empty or not x is empty ) ;
suppose x is empty ; ::_thesis: ex y being Subset of NAT st S2[y,b2,b3]
then  S2[n,x, {} NAT] ;
hence  ex y being Subset of NAT st S2[n,x,y] ; ::_thesis: verum
end;
suppose not x is empty ; ::_thesis: ex y being Subset of NAT st S2[y,b2,b3]
then reconsider x9 = x as non empty Subset of NAT ;
now__::_thesis:_ex_t_being_Subset_of_NAT_st_
for_N_being_non_empty_Subset_of_NAT_st_N_=_x_holds_
t_=_x_\_{(min_N)}
reconsider mx9 = {(min x9)} as Subset of NAT ;
reconsider t = x9 \ mx9 as Subset of NAT ;
take t = t; ::_thesis: for N being non empty Subset of NAT st N = x holds
t = x \ {(min N)}
let N be non empty Subset of NAT; ::_thesis: ( N = x implies t = x \ {(min N)} )
assume  N = x ; ::_thesis: t = x \ {(min N)}
hence  t = x \ {(min N)} ; ::_thesis: verum
end;
hence  ex y being Subset of NAT st S2[n,x,y] ; ::_thesis: verum
end;
end;
end;
consider f being Function of NAT,(bool NAT) such that
A7: f . 0 = sn and
A8: for n being Element of NAT holds S2[n,f . n,f . (n + 1)] from RECDEF_1:sch_2(A6);
take  f ; ::_thesis: ( f . 0 =  {  k where k is Element of NAT : ( not intloc k in L & k <> 0 )  }  & ( for i being Element of NAT
for sn being non empty Subset of NAT st f . i = sn holds
f . (i + 1) = sn \ {(min sn)} ) & ( for i being Element of NAT holds f . i is infinite ) )
thus  f . 0 =  {  v where v is Element of NAT : ( not intloc v in L & v <> 0 )  }  by A7; ::_thesis: ( ( for i being Element of NAT
for sn being non empty Subset of NAT st f . i = sn holds
f . (i + 1) = sn \ {(min sn)} ) & ( for i being Element of NAT holds f . i is infinite ) )
thus  for i being Element of NAT
for sn being non empty Subset of NAT st f . i = sn holds
f . (i + 1) = sn \ {(min sn)} by A8; ::_thesis: for i being Element of NAT holds f . i is infinite
defpred S3[ Element of NAT ] means f . $1 is infinite ;
A9: S3[ 0 ]
proof
deffunc H1( Element of NAT ) ->  Element of the carrier of SCM+FSA = intloc $1;
set Isn =  {  H1(v) where v is Element of NAT : v in sn  }  ;
assume  f . 0 is finite ; ::_thesis: contradiction
then A10: sn is finite by A7;
  {  H1(v) where v is Element of NAT : v in sn  }  is finite from FRAENKEL:sch_21(A10);
then reconsider Isn =  {  H1(v) where v is Element of NAT : v in sn  }  as finite set ;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(L_\/_{(intloc_0)})_\/_Isn_implies_x_in_Int-Locations_)_&_(_x_in_Int-Locations_implies_x_in_(L_\/_{(intloc_0)})_\/_Isn_)_)
let x be set ; ::_thesis: ( ( x in (L \/ {(intloc 0)}) \/ Isn implies x in Int-Locations ) & ( x in Int-Locations implies x in (L \/ {(intloc 0)}) \/ Isn ) )
hereby  ::_thesis: ( x in Int-Locations implies x in (L \/ {(intloc 0)}) \/ Isn )
assume A11: x in (L \/ {(intloc 0)}) \/ Isn ; ::_thesis: x in Int-Locations
percases ( x in L \/ {(intloc 0)} or x in Isn ) by A11, XBOOLE_0:def_3;
suppose x in L \/ {(intloc 0)} ; ::_thesis: x in Int-Locations
hence  x in Int-Locations ; ::_thesis: verum
end;
suppose x in Isn ; ::_thesis: x in Int-Locations
then  ex k being Element of NAT st
( intloc k = x & k in sn ) ;
hence  x in Int-Locations by AMI_2:def_16; ::_thesis: verum
end;
end;
end;
assume  x in Int-Locations ; ::_thesis: x in (L \/ {(intloc 0)}) \/ Isn
then reconsider x9 = x as Int-Location by AMI_2:def_16;
consider i being Element of NAT  such that
A12: x9 = intloc i by SCMFSA_2:8;
now__::_thesis:_(_not_x_in_L_\/_{(intloc_0)}_implies_x_in_Isn_)
assume A13: not x in L \/ {(intloc 0)} ; ::_thesis: x in Isn
then  not x9 in {(intloc 0)} by XBOOLE_0:def_3;
then A14: i <> 0 by A12, TARSKI:def_1;
 not intloc i in L by A12, A13, XBOOLE_0:def_3;
then  i in sn by A14;
hence  x in Isn by A12; ::_thesis: verum
end;
hence  x in (L \/ {(intloc 0)}) \/ Isn by XBOOLE_0:def_3; ::_thesis: verum
end;
hence  contradiction by AMI_3:27, TARSKI:1; ::_thesis: verum
end;
A15: for n being Element of NAT st S3[n] holds
S3[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S3[n] implies S3[n + 1] )
assume A16: f . n is infinite ; ::_thesis: S3[n + 1]
then reconsider sn = f . n as non empty Subset of NAT ;
 min sn in sn by XXREAL_2:def_7;
then A17: {(min sn)} c= sn by ZFMISC_1:31;
assume  f . (n + 1) is finite ; ::_thesis: contradiction
then reconsider sn1 = f . (n + 1) as finite set ;
A18: sn1 \/ {(min sn)} is finite ;
 f . (n + 1) = sn \ {(min sn)} by A8;
hence  contradiction by A16, A17, A18, XBOOLE_1:45; ::_thesis: verum
end;
thus  for n being Element of NAT holds S3[n] from NAT_1:sch_1(A9, A15); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of NAT,(bool NAT) st b1 . 0 =  {  k where k is Element of NAT : ( not intloc k in L & k <> 0 )  }  & ( for i being Element of NAT
for sn being non empty Subset of NAT st b1 . i = sn holds
b1 . (i + 1) = sn \ {(min sn)} ) & ( for i being Element of NAT holds b1 . i is infinite ) & b2 . 0 =  {  k where k is Element of NAT : ( not intloc k in L & k <> 0 )  }  & ( for i being Element of NAT
for sn being non empty Subset of NAT st b2 . i = sn holds
b2 . (i + 1) = sn \ {(min sn)} ) & ( for i being Element of NAT holds b2 . i is infinite ) holds
b1 = b2
proof
let IT1, IT2 be Function of NAT,(bool NAT); ::_thesis: ( IT1 . 0 =  {  k where k is Element of NAT : ( not intloc k in L & k <> 0 )  }  & ( for i being Element of NAT
for sn being non empty Subset of NAT st IT1 . i = sn holds
IT1 . (i + 1) = sn \ {(min sn)} ) & ( for i being Element of NAT holds IT1 . i is infinite ) & IT2 . 0 =  {  k where k is Element of NAT : ( not intloc k in L & k <> 0 )  }  & ( for i being Element of NAT
for sn being non empty Subset of NAT st IT2 . i = sn holds
IT2 . (i + 1) = sn \ {(min sn)} ) & ( for i being Element of NAT holds IT2 . i is infinite ) implies IT1 = IT2 )
assume that
A19: IT1 . 0 =  {  k where k is Element of NAT : ( not intloc k in L & k <> 0 )  }  and
A20: for i being Element of NAT
for sn being non empty Subset of NAT st IT1 . i = sn holds
IT1 . (i + 1) = sn \ {(min sn)} and
 for i being Element of NAT holds IT1 . i is infinite and
A21: IT2 . 0 =  {  k where k is Element of NAT : ( not intloc k in L & k <> 0 )  }  and
A22: for i being Element of NAT
for sn being non empty Subset of NAT st IT2 . i = sn holds
IT2 . (i + 1) = sn \ {(min sn)} and
A23: for i being Element of NAT holds IT2 . i is infinite ; ::_thesis: IT1 = IT2
now__::_thesis:_(_NAT_=_dom_IT1_&_NAT_=_dom_IT2_&_(_for_x_being_set_st_x_in_NAT_holds_
IT1_._x_=_IT2_._x_)_)
defpred S1[ Element of NAT ] means IT1 . $1 = IT2 . $1;
thus  NAT = dom IT1 by FUNCT_2:def_1; ::_thesis: ( NAT = dom IT2 & ( for x being set st x in NAT holds
IT1 . x = IT2 . x ) )
thus  NAT = dom IT2 by FUNCT_2:def_1; ::_thesis: for x being set st x in NAT holds
IT1 . x = IT2 . x
A24: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A25: IT1 . n = IT2 . n ; ::_thesis: S1[n + 1]
then reconsider IT1n = IT1 . n as non empty Subset of NAT by A23;
thus IT1 . (n + 1) = IT1n \ {(min IT1n)} by A20
.= IT2 . (n + 1) by A22, A25 ; ::_thesis: verum
end;
A26: S1[ 0 ] by A19, A21;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A26, A24);
hence  for x being set st x in NAT holds
IT1 . x = IT2 . x ; ::_thesis: verum
end;
hence  IT1 = IT2 by FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines RWNotIn-seq SCMFSA_M:def_5_:_
 for L being finite Subset of Int-Locations
for b2 being Function of NAT,(bool NAT) holds
( b2 = RWNotIn-seq L iff ( b2 . 0 =  {  k where k is Element of NAT : ( not intloc k in L & k <> 0 )  }  & ( for i being Element of NAT
for sn being non empty Subset of NAT st b2 . i = sn holds
b2 . (i + 1) = sn \ {(min sn)} ) & ( for i being Element of NAT holds b2 . i is infinite ) ) );

registration
let L be finite Subset of Int-Locations;
let n be Element of NAT ;
cluster(RWNotIn-seq L) . n ->  non empty ;
coherence
 not (RWNotIn-seq L) . n is empty by Def2;
end;

theorem Th18: :: SCMFSA_M:22
for n being Element of NAT
for L being finite Subset of Int-Locations holds
( not 0 in (RWNotIn-seq L) . n & ( for m being Element of NAT st m in (RWNotIn-seq L) . n holds
not intloc m in L ) )
proof
let n be Element of NAT ; ::_thesis: for L being finite Subset of Int-Locations holds
( not 0 in (RWNotIn-seq L) . n & ( for m being Element of NAT st m in (RWNotIn-seq L) . n holds
not intloc m in L ) )
let L be finite Subset of Int-Locations; ::_thesis: ( not 0 in (RWNotIn-seq L) . n & ( for m being Element of NAT st m in (RWNotIn-seq L) . n holds
not intloc m in L ) )
set RL = RWNotIn-seq L;
defpred S1[ Element of NAT ] means ( not 0 in (RWNotIn-seq L) . $1 & ( for m being Element of NAT st m in (RWNotIn-seq L) . $1 holds
not intloc m in L ) );
A1: S1[ 0 ]
proof
A2: (RWNotIn-seq L) . 0 =  {  k where k is Element of NAT : ( not intloc k in L & k <> 0 )  }  by Def2;
hereby  ::_thesis: for m being Element of NAT st m in (RWNotIn-seq L) . 0 holds
not intloc m in L
assume  0 in (RWNotIn-seq L) . 0 ; ::_thesis: contradiction
then  ex k being Element of NAT st
( k = 0 & not intloc k in L & k <> 0 ) by A2;
hence  contradiction ; ::_thesis: verum
end;
let m be Element of NAT ; ::_thesis: ( m in (RWNotIn-seq L) . 0 implies not intloc m in L )
assume  m in (RWNotIn-seq L) . 0 ; ::_thesis: not intloc m in L
then  ex k being Element of NAT st
( k = m & not intloc k in L & k <> 0 ) by A2;
hence  not intloc m in L ; ::_thesis: verum
end;
A3: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume that
A4: not 0 in (RWNotIn-seq L) . n and
A5: for m being Element of NAT st m in (RWNotIn-seq L) . n holds
not intloc m in L ; ::_thesis: S1[n + 1]
reconsider sn = (RWNotIn-seq L) . n as non empty Subset of NAT ;
A6: (RWNotIn-seq L) . (n + 1) = sn \ {(min sn)} by Def2;
hence  not 0 in (RWNotIn-seq L) . (n + 1) by A4, XBOOLE_0:def_5; ::_thesis: for m being Element of NAT st m in (RWNotIn-seq L) . (n + 1) holds
not intloc m in L
let m be Element of NAT ; ::_thesis: ( m in (RWNotIn-seq L) . (n + 1) implies not intloc m in L )
assume  m in (RWNotIn-seq L) . (n + 1) ; ::_thesis: not intloc m in L
then  m in (RWNotIn-seq L) . n by A6, XBOOLE_0:def_5;
hence  not intloc m in L by A5; ::_thesis: verum
end;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A1, A3);
hence  ( not 0 in (RWNotIn-seq L) . n & ( for m being Element of NAT st m in (RWNotIn-seq L) . n holds
not intloc m in L ) ) ; ::_thesis: verum
end;

theorem Th19: :: SCMFSA_M:23
for n being Element of NAT
for L being finite Subset of Int-Locations holds min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . (n + 1))
proof
let n be Element of NAT ; ::_thesis: for L being finite Subset of Int-Locations holds min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . (n + 1))
let L be finite Subset of Int-Locations; ::_thesis: min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . (n + 1))
set RL = RWNotIn-seq L;
set sn = (RWNotIn-seq L) . n;
set sn1 = (RWNotIn-seq L) . (n + 1);
assume A1: min ((RWNotIn-seq L) . n) >= min ((RWNotIn-seq L) . (n + 1)) ; ::_thesis: contradiction
A2: (RWNotIn-seq L) . (n + 1) = ((RWNotIn-seq L) . n) \ {(min ((RWNotIn-seq L) . n))} by Def2;
then  min ((RWNotIn-seq L) . n) <= min ((RWNotIn-seq L) . (n + 1)) by XBOOLE_1:36, XXREAL_2:60;
then  min ((RWNotIn-seq L) . n) = min ((RWNotIn-seq L) . (n + 1)) by A1, XXREAL_0:1;
then A3: min ((RWNotIn-seq L) . (n + 1)) in {(min ((RWNotIn-seq L) . n))} by TARSKI:def_1;
 min ((RWNotIn-seq L) . (n + 1)) in (RWNotIn-seq L) . (n + 1) by XXREAL_2:def_7;
hence  contradiction by A2, A3, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem Th20: :: SCMFSA_M:24
for n, m being Element of NAT
for L being finite Subset of Int-Locations st n < m holds
min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . m)
proof
let n, m be Element of NAT ; ::_thesis: for L being finite Subset of Int-Locations st n < m holds
min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . m)
let L be finite Subset of Int-Locations; ::_thesis: ( n < m implies min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . m) )
set RL = RWNotIn-seq L;
now__::_thesis:_for_n,_n_being_Element_of_NAT_holds_S1[n]
let n be Element of NAT ; ::_thesis: for n being Element of NAT holds S1[n]
defpred S1[ Element of NAT ] means ( n < $1 implies min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . $1) );
A1: for m being Element of NAT st S1[m] holds
S1[m + 1]
proof
let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A2: ( n < m implies min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . m) ) ; ::_thesis: S1[m + 1]
assume  n < m + 1 ; ::_thesis: min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . (m + 1))
then A3: n <= m by NAT_1:13;
percases ( n = m or n < m ) by A3, XXREAL_0:1;
suppose n = m ; ::_thesis: min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . (m + 1))
hence  min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . (m + 1)) by Th19; ::_thesis: verum
end;
suppose n < m ; ::_thesis: min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . (m + 1))
hence  min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . (m + 1)) by A2, Th19, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
A4: S1[ 0 ] by NAT_1:2;
thus  for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A1); ::_thesis: verum
end;
hence  ( n < m implies min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . m) ) ; ::_thesis: verum
end;

definition
let n be Element of NAT ;
let L be finite Subset of Int-Locations;
funcn -thRWNotIn L ->  Int-Location equals :: SCMFSA_M:def 6
 intloc (min ((RWNotIn-seq L) . n));
correctness
coherence
intloc (min ((RWNotIn-seq L) . n)) is Int-Location;
;
end;

:: deftheorem  defines -thRWNotIn SCMFSA_M:def_6_:_
 for n being Element of NAT
for L being finite Subset of Int-Locations holds n -thRWNotIn L = intloc (min ((RWNotIn-seq L) . n));

notation
let n be Element of NAT ;
let L be finite Subset of Int-Locations;
synonym n -stRWNotIn L for n -thRWNotIn L;
synonym n -ndRWNotIn L for n -thRWNotIn L;
synonym n -rdRWNotIn L for n -thRWNotIn L;
end;

registration
let n be Element of NAT ;
let L be finite Subset of Int-Locations;
clustern -thRWNotIn L ->  read-write ;
coherence
 not n -thRWNotIn L is read-only
proof
set sn = (RWNotIn-seq L) . n;
A1: min ((RWNotIn-seq L) . n) in (RWNotIn-seq L) . n by XXREAL_2:def_7;
assume  n -thRWNotIn L = intloc 0 ; :: according to SCMFSA_M:def_2 ::_thesis: contradiction
then  min ((RWNotIn-seq L) . n) = 0 by AMI_3:10;
hence  contradiction by A1, Th18; ::_thesis: verum
end;
end;

theorem :: SCMFSA_M:25
for n being Element of NAT
for L being finite Subset of Int-Locations holds not n -thRWNotIn L in L
proof
let n be Element of NAT ; ::_thesis: for L being finite Subset of Int-Locations holds not n -thRWNotIn L in L
let L be finite Subset of Int-Locations; ::_thesis: not n -thRWNotIn L in L
set FNI = n -thRWNotIn L;
set sn = (RWNotIn-seq L) . n;
 min ((RWNotIn-seq L) . n) in (RWNotIn-seq L) . n by XXREAL_2:def_7;
hence  not n -thRWNotIn L in L by Th18; ::_thesis: verum
end;

theorem :: SCMFSA_M:26
for n, m being Element of NAT
for L being finite Subset of Int-Locations st n <> m holds
n -thRWNotIn L <> m -thRWNotIn L
proof
let n, m be Element of NAT ; ::_thesis: for L being finite Subset of Int-Locations st n <> m holds
n -thRWNotIn L <> m -thRWNotIn L
let L be finite Subset of Int-Locations; ::_thesis: ( n <> m implies n -thRWNotIn L <> m -thRWNotIn L )
assume  n <> m ; ::_thesis: n -thRWNotIn L <> m -thRWNotIn L
then  ( n < m or m < n ) by XXREAL_0:1;
then A1: min ((RWNotIn-seq L) . n) <> min ((RWNotIn-seq L) . m) by Th20;
assume  n -thRWNotIn L = m -thRWNotIn L ; ::_thesis: contradiction
hence  contradiction by A1, AMI_3:10; ::_thesis: verum
end;

begin

theorem Th6: :: SCMFSA_M:27
for s1, s2 being State of SCM+FSA
for Iloc being Subset of Int-Locations
for Floc being Subset of FinSeq-Locations holds
( s1 | (Iloc \/ Floc) = s2 | (Iloc \/ Floc) iff ( ( for x being Int-Location st x in Iloc holds
s1 . x = s2 . x ) & ( for x being FinSeq-Location st x in Floc holds
s1 . x = s2 . x ) ) )
proof
let s1, s2 be State of SCM+FSA; ::_thesis: for Iloc being Subset of Int-Locations
for Floc being Subset of FinSeq-Locations holds
( s1 | (Iloc \/ Floc) = s2 | (Iloc \/ Floc) iff ( ( for x being Int-Location st x in Iloc holds
s1 . x = s2 . x ) & ( for x being FinSeq-Location st x in Floc holds
s1 . x = s2 . x ) ) )
let Iloc be Subset of Int-Locations; ::_thesis: for Floc being Subset of FinSeq-Locations holds
( s1 | (Iloc \/ Floc) = s2 | (Iloc \/ Floc) iff ( ( for x being Int-Location st x in Iloc holds
s1 . x = s2 . x ) & ( for x being FinSeq-Location st x in Floc holds
s1 . x = s2 . x ) ) )
let Floc be Subset of FinSeq-Locations; ::_thesis: ( s1 | (Iloc \/ Floc) = s2 | (Iloc \/ Floc) iff ( ( for x being Int-Location st x in Iloc holds
s1 . x = s2 . x ) & ( for x being FinSeq-Location st x in Floc holds
s1 . x = s2 . x ) ) )
 FinSeq-Locations c= dom s1 by SCMFSA_2:46;
then A1: Floc c= dom s1 by XBOOLE_1:1;
 FinSeq-Locations c= dom s2 by SCMFSA_2:46;
then A2: Floc c= dom s2 by XBOOLE_1:1;
 Int-Locations c= dom s2 by SCMFSA_2:45;
then A3: Iloc c= dom s2 by XBOOLE_1:1;
then A4: Iloc \/ Floc c= dom s2 by A2, XBOOLE_1:8;
 Int-Locations c= dom s1 by SCMFSA_2:45;
then A5: Iloc c= dom s1 by XBOOLE_1:1;
then A6: Iloc \/ Floc c= dom s1 by A1, XBOOLE_1:8;
hereby  ::_thesis: ( ( for x being Int-Location st x in Iloc holds
s1 . x = s2 . x ) & ( for x being FinSeq-Location st x in Floc holds
s1 . x = s2 . x ) implies s1 | (Iloc \/ Floc) = s2 | (Iloc \/ Floc) )
assume A7: s1 | (Iloc \/ Floc) = s2 | (Iloc \/ Floc) ; ::_thesis: ( ( for x being Int-Location st x in Iloc holds
s1 . x = s2 . x ) & ( for x being FinSeq-Location st x in Floc holds
s1 . x = s2 . x ) )
hereby  ::_thesis: for x being FinSeq-Location st x in Floc holds
s1 . x = s2 . x
let x be Int-Location; ::_thesis: ( x in Iloc implies s1 . x = s2 . x )
assume  x in Iloc ; ::_thesis: s1 . x = s2 . x
then  x in Iloc \/ Floc by XBOOLE_0:def_3;
hence  s1 . x = s2 . x by A6, A4, A7, FUNCT_1:95; ::_thesis: verum
end;
let x be FinSeq-Location ; ::_thesis: ( x in Floc implies s1 . x = s2 . x )
assume  x in Floc ; ::_thesis: s1 . x = s2 . x
then  x in Iloc \/ Floc by XBOOLE_0:def_3;
hence  s1 . x = s2 . x by A6, A4, A7, FUNCT_1:95; ::_thesis: verum
end;
assume that
A8: for x being Int-Location st x in Iloc holds
s1 . x = s2 . x and
A9: for x being FinSeq-Location st x in Floc holds
s1 . x = s2 . x ; ::_thesis: s1 | (Iloc \/ Floc) = s2 | (Iloc \/ Floc)
A10: now__::_thesis:_(_(_for_x_being_set_st_x_in_Iloc_holds_
s1_._x_=_s2_._x_)_&_(_for_x_being_set_st_x_in_Floc_holds_
s1_._x_=_s2_._x_)_)
hereby  ::_thesis: for x being set st x in Floc holds
s1 . x = s2 . x
let x be set ; ::_thesis: ( x in Iloc implies s1 . x = s2 . x )
assume A11: x in Iloc ; ::_thesis: s1 . x = s2 . x
then  x in Int-Locations ;
then reconsider x9 = x as Int-Location by AMI_2:def_16;
thus s1 . x = s2 . x9 by A8, A11
.= s2 . x ; ::_thesis: verum
end;
let x be set ; ::_thesis: ( x in Floc implies s1 . x = s2 . x )
assume A12: x in Floc ; ::_thesis: s1 . x = s2 . x
then  x in FinSeq-Locations ;
then reconsider x9 = x as FinSeq-Location by SCMFSA_2:def_5;
thus s1 . x = s2 . x9 by A9, A12
.= s2 . x ; ::_thesis: verum
end;
then A13: s1 | Floc = s2 | Floc by A1, A2, FUNCT_1:95;
 s1 | Iloc = s2 | Iloc by A5, A3, A10, FUNCT_1:95;
hence  s1 | (Iloc \/ Floc) = s2 | (Iloc \/ Floc) by A13, RELAT_1:150; ::_thesis: verum
end;

theorem :: SCMFSA_M:28
for s1, s2 being State of SCM+FSA
for Iloc being Subset of Int-Locations holds
( s1 | (Iloc \/ FinSeq-Locations) = s2 | (Iloc \/ FinSeq-Locations) iff ( ( for x being Int-Location st x in Iloc holds
s1 . x = s2 . x ) & ( for x being FinSeq-Location holds s1 . x = s2 . x ) ) )
proof
let s1, s2 be State of SCM+FSA; ::_thesis: for Iloc being Subset of Int-Locations holds
( s1 | (Iloc \/ FinSeq-Locations) = s2 | (Iloc \/ FinSeq-Locations) iff ( ( for x being Int-Location st x in Iloc holds
s1 . x = s2 . x ) & ( for x being FinSeq-Location holds s1 . x = s2 . x ) ) )
set FSL = FinSeq-Locations ;
let Iloc be Subset of Int-Locations; ::_thesis: ( s1 | (Iloc \/ FinSeq-Locations) = s2 | (Iloc \/ FinSeq-Locations) iff ( ( for x being Int-Location st x in Iloc holds
s1 . x = s2 . x ) & ( for x being FinSeq-Location holds s1 . x = s2 . x ) ) )
A1: ( ( for x being FinSeq-Location holds s1 . x = s2 . x ) implies for x being FinSeq-Location st x in FinSeq-Locations holds
s1 . x = s2 . x ) ;
A2: ( ( for x being FinSeq-Location st x in FinSeq-Locations holds
s1 . x = s2 . x ) implies for x being FinSeq-Location holds s1 . x = s2 . x )
proof
assume A3: for x being FinSeq-Location st x in FinSeq-Locations holds
s1 . x = s2 . x ; ::_thesis: for x being FinSeq-Location holds s1 . x = s2 . x
let x be FinSeq-Location ; ::_thesis: s1 . x = s2 . x
 x in FinSeq-Locations by SCMFSA_2:def_5;
hence  s1 . x = s2 . x by A3; ::_thesis: verum
end;
 [#] FinSeq-Locations = FinSeq-Locations ;
hence  ( s1 | (Iloc \/ FinSeq-Locations) = s2 | (Iloc \/ FinSeq-Locations) iff ( ( for x being Int-Location st x in Iloc holds
s1 . x = s2 . x ) & ( for x being FinSeq-Location holds s1 . x = s2 . x ) ) ) by A1, A2, Th6; ::_thesis: verum
end;

begin

theorem :: SCMFSA_M:29
for x being set
for i, m, n being Element of NAT holds
( not x in dom (((intloc i) .--> m) +* (Start-At (n,SCM+FSA))) or x = intloc i or x = IC )
proof
let x be set ; ::_thesis: for i, m, n being Element of NAT holds
( not x in dom (((intloc i) .--> m) +* (Start-At (n,SCM+FSA))) or x = intloc i or x = IC )
let i, m, n be Element of NAT ; ::_thesis: ( not x in dom (((intloc i) .--> m) +* (Start-At (n,SCM+FSA))) or x = intloc i or x = IC )
set iS = ((intloc i) .--> m) +* (Start-At (n,SCM+FSA));
 ( dom ((intloc i) .--> m) = {(intloc i)} & dom (Start-At (n,SCM+FSA)) = {(IC )} ) by FUNCOP_1:13;
then A1: dom (((intloc i) .--> m) +* (Start-At (n,SCM+FSA))) = {(intloc i)} \/ {(IC )} by FUNCT_4:def_1;
assume  x in dom (((intloc i) .--> m) +* (Start-At (n,SCM+FSA))) ; ::_thesis: ( x = intloc i or x = IC )
then  ( x in {(intloc i)} or x in {(IC )} ) by A1, XBOOLE_0:def_3;
hence  ( x = intloc i or x = IC ) by TARSKI:def_1; ::_thesis: verum
end;

theorem :: SCMFSA_M:30
for s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s holds
s . (intloc 0) = 1
proof
let s be State of SCM+FSA; ::_thesis: ( Initialize ((intloc 0) .--> 1) c= s implies s . (intloc 0) = 1 )
set iS = Initialize ((intloc 0) .--> 1);
Y: dom (Initialize ((intloc 0) .--> 1)) = (dom ((intloc 0) .--> 1)) \/ (dom (Start-At (0,SCM+FSA))) by FUNCT_4:def_1;
 intloc 0 in dom ((intloc 0) .--> 1) by FUNCOP_1:74;
then A1: intloc 0 in dom (Initialize ((intloc 0) .--> 1)) by Y, XBOOLE_0:def_3;
C: dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
 IC <> intloc 0 by SCMFSA_2:56;
then  not intloc 0 in dom (Start-At (0,SCM+FSA)) by C, TARSKI:def_1;
then (Initialize ((intloc 0) .--> 1)) . (intloc 0) = ((intloc 0) .--> 1) . (intloc 0) by FUNCT_4:11
.= 1 by FUNCOP_1:72 ;
hence  ( Initialize ((intloc 0) .--> 1) c= s implies s . (intloc 0) = 1 ) by A1, GRFUNC_1:2; ::_thesis: verum
end;

registration
let n be Element of NAT ;
cluster intloc (n + 1) ->  read-write ;
coherence
 not intloc (n + 1) is read-only
proof
thus  intloc (n + 1) <> intloc 0 by AMI_3:10; :: according to SCMFSA_M:def_2 ::_thesis: verum
end;
end;

begin

registration
let f be FinSeq-Location ;
let t be FinSequence of INT ;
clusterf .--> t ->  the_Values_of SCM+FSA -compatible ;
coherence
 f .--> t is the_Values_of SCM+FSA -compatible
proof
A1: t is Element of INT * by FINSEQ_1:def_11;
 Values f = INT * by SCMFSA_2:12;
hence  f .--> t is the_Values_of SCM+FSA -compatible by A1; ::_thesis: verum
end;
end;

theorem :: SCMFSA_M:31
for w being FinSequence of INT
for f being FinSeq-Location holds dom (Initialized (f .--> w)) = {(intloc 0),(IC ),f}
proof
let w be FinSequence of INT ; ::_thesis: for f being FinSeq-Location holds dom (Initialized (f .--> w)) = {(intloc 0),(IC ),f}
let f be FinSeq-Location ; ::_thesis: dom (Initialized (f .--> w)) = {(intloc 0),(IC ),f}
dom (Initialized (f .--> w)) = (dom (Initialize ((intloc 0) .--> 1))) \/ (dom (f .--> w)) by FUNCT_4:def_1
.= {(intloc 0),(IC )} \/ {f} by Th11, FUNCOP_1:13 ;
hence  dom (Initialized (f .--> w)) = {(intloc 0),(IC ),f} by ENUMSET1:3; ::_thesis: verum
end;

theorem :: SCMFSA_M:32
for t being FinSequence of INT
for f being FinSeq-Location holds dom (Initialize ((intloc 0) .--> 1)) misses dom (f .--> t)
proof
let t be FinSequence of INT ; ::_thesis: for f being FinSeq-Location holds dom (Initialize ((intloc 0) .--> 1)) misses dom (f .--> t)
let f be FinSeq-Location ; ::_thesis: dom (Initialize ((intloc 0) .--> 1)) misses dom (f .--> t)
set x = f .--> t;
A1: dom (f .--> t) = {f} by FUNCOP_1:13;
set DI = dom (Initialize ((intloc 0) .--> 1));
assume  (dom (Initialize ((intloc 0) .--> 1))) /\ (dom (f .--> t)) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then consider y being set  such that
A2: y in (dom (Initialize ((intloc 0) .--> 1))) /\ (dom (f .--> t)) by XBOOLE_0:def_1;
A3: y in dom (Initialize ((intloc 0) .--> 1)) by A2, XBOOLE_0:def_4;
 y in dom (f .--> t) by A2, XBOOLE_0:def_4;
then A4: y = f by A1, TARSKI:def_1;
 ( y = intloc 0 or y = IC ) by A3, Th11, TARSKI:def_2;
hence  contradiction by A4, SCMFSA_2:57, SCMFSA_2:58; ::_thesis: verum
end;

theorem :: SCMFSA_M:33
for w being FinSequence of INT
for f being FinSeq-Location
for s being State of SCM+FSA st Initialized (f .--> w) c= s holds
( s . f = w & s . (intloc 0) = 1 )
proof
let w be FinSequence of INT ; ::_thesis: for f being FinSeq-Location
for s being State of SCM+FSA st Initialized (f .--> w) c= s holds
( s . f = w & s . (intloc 0) = 1 )
let f be FinSeq-Location ; ::_thesis: for s being State of SCM+FSA st Initialized (f .--> w) c= s holds
( s . f = w & s . (intloc 0) = 1 )
let s be State of SCM+FSA; ::_thesis: ( Initialized (f .--> w) c= s implies ( s . f = w & s . (intloc 0) = 1 ) )
set t = f .--> w;
set p = Initialized (f .--> w);
assume A2: Initialized (f .--> w) c= s ; ::_thesis: ( s . f = w & s . (intloc 0) = 1 )
reconsider pt = Initialized (f .--> w) as PartState of SCM+FSA ;
 dom (f .--> w) = {f} by FUNCOP_1:13;
then B3: f in dom (f .--> w) by TARSKI:def_1;
A4: f in dom pt by B3, FUNCT_4:12;
A5: intloc 0 in dom pt by Th4;
 ex i being Element of NAT st f = fsloc i by SCMFSA_2:9;
then  f <> intloc 0 by SCMFSA_2:99;
then  not f in {(intloc 0)} by TARSKI:def_1;
then A6: not f in dom ((intloc 0) .--> 1) by FUNCOP_1:13;
A7: dom (Initialize ((intloc 0) .--> 1)) = (dom ((intloc 0) .--> 1)) \/ (dom (Start-At (0,SCM+FSA))) by FUNCT_4:def_1;
 not f in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:103;
then A8: not f in dom (Initialize ((intloc 0) .--> 1)) by A6, A7, XBOOLE_0:def_3;
thus s . f = pt . f by A2, A4, GRFUNC_1:2
.= (f .--> w) . f by A8, FUNCT_4:11
.= w by FUNCOP_1:72 ; ::_thesis: s . (intloc 0) = 1
thus s . (intloc 0) = (Initialized (f .--> w)) . (intloc 0) by A2, A5, GRFUNC_1:2
.= 1 by Th12, Th10, FUNCT_4:13 ; ::_thesis: verum
end;

theorem :: SCMFSA_M:34
for f being FinSeq-Location
for a being Int-Location
for s being State of SCM+FSA holds {a,(IC ),f} c= dom s
proof
let f be FinSeq-Location ; ::_thesis: for a being Int-Location
for s being State of SCM+FSA holds {a,(IC ),f} c= dom s
let a be Int-Location; ::_thesis: for s being State of SCM+FSA holds {a,(IC ),f} c= dom s
let s be State of SCM+FSA; ::_thesis: {a,(IC ),f} c= dom s
A1: a in dom s by SCMFSA_2:42;
 IC in dom s by MEMSTR_0:2;
then A2: {a,(IC )} c= dom s by A1, ZFMISC_1:32;
 f in dom s by SCMFSA_2:43;
then  {f} c= dom s by ZFMISC_1:31;
then  {a,(IC )} \/ {f} c= dom s by A2, XBOOLE_1:8;
hence  {a,(IC ),f} c= dom s by ENUMSET1:3; ::_thesis: verum
end;

definition
func Sorting-Function  ->  PartFunc of (FinPartSt SCM+FSA),(FinPartSt SCM+FSA) means :Def3: :: SCMFSA_M:def 7
 for p, q being FinPartState of SCM+FSA holds
( [p,q] in it 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 ) );
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 ) )
proof
defpred S1[ set , set ] means  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 & $1 = (fsloc 0) .--> t & $2 = (fsloc 0) .--> u );
A1: for x, y1, y2 being set st S1[x,y1] & S1[x,y2] holds
y1 = y2
proof
let p, q1, q2 be set ; ::_thesis: ( S1[p,q1] & S1[p,q2] implies q1 = q2 )
given t1 being FinSequence of INT , u1 being FinSequence of REAL  such that A2: t1,u1 are_fiberwise_equipotent and
 u1 is FinSequence of INT and
A3: u1 is non-increasing and
A4: p = (fsloc 0) .--> t1 and
A5: q1 = (fsloc 0) .--> u1 ; ::_thesis: ( not S1[p,q2] or q1 = q2 )
given t2 being FinSequence of INT , u2 being FinSequence of REAL  such that A6: t2,u2 are_fiberwise_equipotent and
 u2 is FinSequence of INT and
A7: u2 is non-increasing and
A8: p = (fsloc 0) .--> t2 and
A9: q2 = (fsloc 0) .--> u2 ; ::_thesis: q1 = q2
t1 = ((fsloc 0) .--> t1) . (fsloc 0) by FUNCOP_1:72
.= t2 by A4, A8, FUNCOP_1:72 ;
hence  q1 = q2 by A2, A3, A5, A6, A7, A9, CLASSES1:76, RFINSEQ:23; ::_thesis: verum
end;
consider f being Function such that
A10: for p, q being set holds
( [p,q] in f iff ( p in FinPartSt SCM+FSA & S1[p,q] ) ) from FUNCT_1:sch_1(A1);
A11: dom f c= FinPartSt SCM+FSA
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in dom f or e in FinPartSt SCM+FSA )
assume  e in dom f ; ::_thesis: e in FinPartSt SCM+FSA
then  [e,(f . e)] in f by FUNCT_1:1;
hence  e in FinPartSt SCM+FSA by A10; ::_thesis: verum
end;
 rng f c= FinPartSt SCM+FSA
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in rng f or q in FinPartSt SCM+FSA )
assume  q in rng f ; ::_thesis: q in FinPartSt SCM+FSA
then consider p being set  such that
A12: [p,q] in f by XTUPLE_0:def_13;
consider t being FinSequence of INT , u being FinSequence of REAL  such that
 t,u are_fiberwise_equipotent and
A13: u is FinSequence of INT and
 u is non-increasing and
 p = (fsloc 0) .--> t and
A14: q = (fsloc 0) .--> u by A10, A12;
reconsider u = u as FinSequence of INT by A13;
 (fsloc 0) .--> u is FinPartState of SCM+FSA ;
hence  q in FinPartSt SCM+FSA by A14, MEMSTR_0:75; ::_thesis: verum
end;
then reconsider f = f as PartFunc of (FinPartSt SCM+FSA),(FinPartSt SCM+FSA) by A11, RELSET_1:4;
take  f ; ::_thesis: for p, q being FinPartState of SCM+FSA holds
( [p,q] in f 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 ) )
let p, q be FinPartState of SCM+FSA; ::_thesis: ( [p,q] in f 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 ) )
thus  ( [p,q] in f implies 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 ) ) by A10; ::_thesis: ( 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 ) implies [p,q] in f )
given t being FinSequence of INT , u being FinSequence of REAL  such that A15: t,u are_fiberwise_equipotent and
A16: u is FinSequence of INT and
A17: u is non-increasing and
A18: p = (fsloc 0) .--> t and
A19: q = (fsloc 0) .--> u ; ::_thesis: [p,q] in f
 p in FinPartSt SCM+FSA by MEMSTR_0:75;
hence  [p,q] in f by A10, A15, A16, A17, A18, A19; ::_thesis: verum
end;
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
proof
let IT1, IT2 be PartFunc of (FinPartSt SCM+FSA),(FinPartSt SCM+FSA); ::_thesis: ( ( for p, q being FinPartState of SCM+FSA holds
( [p,q] in IT1 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 IT2 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 ) ) ) implies IT1 = IT2 )
assume that
A20: for p, q being FinPartState of SCM+FSA holds
( [p,q] in IT1 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 ) ) and
A21: for p, q being FinPartState of SCM+FSA holds
( [p,q] in IT2 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 ) ) ; ::_thesis: IT1 = IT2
defpred S1[ set , set ] means  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 & $1 = (fsloc 0) .--> t & $2 = (fsloc 0) .--> u );
A22: for p, q being Element of FinPartSt SCM+FSA holds
( [p,q] in IT1 iff S1[p,q] )
proof
let p, q be Element of FinPartSt SCM+FSA; ::_thesis: ( [p,q] in IT1 iff S1[p,q] )
reconsider p = p, q = q as FinPartState of SCM+FSA by MEMSTR_0:76;
 ( [p,q] in IT1 iff S1[p,q] ) by A20;
hence  ( [p,q] in IT1 iff S1[p,q] ) ; ::_thesis: verum
end;
A23: for p, q being Element of FinPartSt SCM+FSA holds
( [p,q] in IT2 iff S1[p,q] )
proof
let p, q be Element of FinPartSt SCM+FSA; ::_thesis: ( [p,q] in IT2 iff S1[p,q] )
reconsider p = p, q = q as FinPartState of SCM+FSA by MEMSTR_0:76;
 ( [p,q] in IT2 iff S1[p,q] ) by A21;
hence  ( [p,q] in IT2 iff S1[p,q] ) ; ::_thesis: verum
end;
thus  IT1 = IT2 from RELSET_1:sch_4(A22, A23); ::_thesis: verum
end;
end;

:: deftheorem Def3 defines Sorting-Function SCMFSA_M:def_7_:_
 for b1 being PartFunc of (FinPartSt SCM+FSA),(FinPartSt SCM+FSA) holds
( b1 = Sorting-Function iff 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 ) ) );

theorem :: SCMFSA_M:35
for p being set holds
( p in dom Sorting-Function iff ex t being FinSequence of INT st p = (fsloc 0) .--> t )
proof
set f = Sorting-Function ;
let p be set ; ::_thesis: ( p in dom Sorting-Function iff ex t being FinSequence of INT st p = (fsloc 0) .--> t )
hereby  ::_thesis: ( ex t being FinSequence of INT st p = (fsloc 0) .--> t implies p in dom Sorting-Function )
set q = Sorting-Function . p;
assume A1: p in dom Sorting-Function ; ::_thesis: ex t being FinSequence of INT st p = (fsloc 0) .--> t
then A2: [p,(Sorting-Function . p)] in Sorting-Function by FUNCT_1:1;
 dom Sorting-Function c= FinPartSt SCM+FSA by RELAT_1:def_18;
then A3: p is FinPartState of SCM+FSA by A1, MEMSTR_0:76;
 Sorting-Function . p in FinPartSt SCM+FSA by A1, PARTFUN1:4;
then  Sorting-Function . p is FinPartState of SCM+FSA by MEMSTR_0:76;
then consider t being FinSequence of INT , u being FinSequence of REAL  such that
 t,u are_fiberwise_equipotent and
 u is FinSequence of INT and
 u is non-increasing and
A4: p = (fsloc 0) .--> t and
 Sorting-Function . p = (fsloc 0) .--> u by A2, A3, Def3;
take t = t; ::_thesis: p = (fsloc 0) .--> t
thus  p = (fsloc 0) .--> t by A4; ::_thesis: verum
end;
given t being FinSequence of INT  such that A5: p = (fsloc 0) .--> t ; ::_thesis: p in dom Sorting-Function
consider u being FinSequence of REAL  such that
A6: t,u are_fiberwise_equipotent and
A7: u is FinSequence of INT and
A8: u is non-increasing by RFINSEQ:33;
reconsider u1 = u as FinSequence of INT by A7;
set q = (fsloc 0) .--> u1;
 [p,((fsloc 0) .--> u1)] in Sorting-Function by A5, A6, A8, Def3;
hence  p in dom Sorting-Function by FUNCT_1:1; ::_thesis: verum
end;

theorem :: SCMFSA_M:36
for t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & Sorting-Function . ((fsloc 0) .--> t) = (fsloc 0) .--> u )
proof
let t be FinSequence of INT ; ::_thesis: ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & Sorting-Function . ((fsloc 0) .--> t) = (fsloc 0) .--> u )
consider u being FinSequence of REAL  such that
A1: t,u are_fiberwise_equipotent and
A2: u is FinSequence of INT and
A3: u is non-increasing by RFINSEQ:33;
reconsider u = u as FinSequence of INT by A2;
set p = (fsloc 0) .--> t;
set q = (fsloc 0) .--> u;
 [((fsloc 0) .--> t),((fsloc 0) .--> u)] in Sorting-Function by A1, A3, Def3;
then  Sorting-Function . ((fsloc 0) .--> t) = (fsloc 0) .--> u by FUNCT_1:1;
hence  ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & Sorting-Function . ((fsloc 0) .--> t) = (fsloc 0) .--> u ) by A1, A3; ::_thesis: verum
end;

theorem :: SCMFSA_M:37
for s being State of SCM+FSA holds
( ( for a being read-write Int-Location holds (Initialized s) . a = s . a ) & ( for f being FinSeq-Location holds (Initialized s) . f = s . f ) )
proof
let s be State of SCM+FSA; ::_thesis: ( ( for a being read-write Int-Location holds (Initialized s) . a = s . a ) & ( for f being FinSeq-Location holds (Initialized s) . f = s . f ) )
A1: Initialized s = Initialize (s +* ((intloc 0) .--> 1)) by FUNCT_4:14;
A2: dom ((intloc 0) .--> 1) = {(intloc 0)} by FUNCOP_1:13;
hereby  ::_thesis: for f being FinSeq-Location holds (Initialized s) . f = s . f
let a be read-write Int-Location; ::_thesis: (Initialized s) . a = s . a
A3: not a in dom ((intloc 0) .--> 1) by A2, TARSKI:def_1;
 not a in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:102;
hence (Initialized s) . a = (s +* ((intloc 0) .--> 1)) . a by A1, FUNCT_4:11
.= s . a by A3, FUNCT_4:11 ;
::_thesis: verum
end;
hereby  ::_thesis: verum
let f be FinSeq-Location ; ::_thesis: (Initialized s) . f = s . f
 intloc 0 <> f by SCMFSA_2:58;
then A4: not f in dom ((intloc 0) .--> 1) by A2, TARSKI:def_1;
 not f in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:103;
hence (Initialized s) . f = (s +* ((intloc 0) .--> 1)) . f by A1, FUNCT_4:11
.= s . f by A4, FUNCT_4:11 ;
::_thesis: verum
end;
end;