:: On the memory of SCM+FSA
:: by Library Committee
::
:: Received October 1, 2011
:: Copyright (c) 2011-2012 Association of Mizar Users


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
proofend;
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))
proofend;
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) ) ) )
proofend;

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 )
proofend;

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 )
proofend;

theorem Th43: :: SCMFSA_M:3
for p being PartState of SCM+FSA holds dom (Initialized p) = ((dom p) \/ {(intloc 0)}) \/ {(IC )}
proofend;

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)
proofend;

theorem :: SCMFSA_M:5
for p being PartState of SCM+FSA holds
( (Initialized p) . (intloc 0) = 1 & (Initialized p) . (IC ) = 0 )
proofend;

theorem :: SCMFSA_M:6
for p being PartState of SCM+FSA
for a being Int-Location st a <> intloc 0 &amp; not a in dom p holds
not a in dom (Initialized p)
proofend;

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)
proofend;

theorem :: SCMFSA_M:8
for s being State of SCM+FSA st s . (intloc 0) = 1 &amp; IC s = 0 holds
Initialized s = s
proofend;

theorem :: SCMFSA_M:9
for p being PartState of SCM+FSA holds (Initialized p) . (intloc 0) = 1
proofend;

theorem Th10: :: SCMFSA_M:10
intloc 0 in dom (Initialize ((intloc 0) .--> 1))
proofend;

theorem Th11: :: SCMFSA_M:11
dom (Initialize ((intloc 0) .--> 1)) = {(intloc 0),(IC )}
proofend;

theorem Th12: :: SCMFSA_M:12
(Initialize ((intloc 0) .--> 1)) . (intloc 0) = 1
proofend;

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
proofend;
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) &amp; 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) &amp; sn =  {  k where k is Element of NAT : not intloc k in L  }  )
proofend;
uniqueness
 for b1, b2 being Int-Location st ex sn being non empty Subset of NAT st
( b1 = intloc (min sn) &amp; sn =  {  k where k is Element of NAT : not intloc k in L  }  ) &amp; ex sn being non empty Subset of NAT st
( b2 = intloc (min sn) &amp; 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) &amp; 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
proofend;

theorem :: SCMFSA_M:15
for m, n being Element of NAT
for L being finite Subset of Int-Locations st FirstNotIn L = intloc m &amp; not intloc n in L holds
m <= n
proofend;

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) &amp; 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) &amp; sn =  {  k where k is Element of NAT : not fsloc k in L  }  )
proofend;
uniqueness
 for b1, b2 being FinSeq-Location st ex sn being non empty Subset of NAT st
( b1 = fsloc (min sn) &amp; sn =  {  k where k is Element of NAT : not fsloc k in L  }  ) &amp; ex sn being non empty Subset of NAT st
( b2 = fsloc (min sn) &amp; 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) &amp; 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
proofend;

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 &amp; not fsloc n in L holds
m <= n
proofend;

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
proofend;
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
proofend;

theorem :: SCMFSA_M:19
for s being State of SCM+FSA st s . (intloc 0) = 1 holds
DataPart (Initialized s) = DataPart s
proofend;

theorem :: SCMFSA_M:20
for s1, s2 being State of SCM+FSA st s1 . (intloc 0) = s2 . (intloc 0) &amp; ( for a being read-write Int-Location holds s1 . a = s2 . a ) &amp; ( for f being FinSeq-Location holds s1 . f = s2 . f ) holds
DataPart s1 = DataPart s2
proofend;

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
proofend;

begin

definition
let d be Int-Location;
:: original:{
redefine func{d} ->  Subset of Int-Locations;
coherence
 {d} is Subset of Int-Locations
proofend;
let e be Int-Location;
:: original:{
redefine func{d,e} ->  Subset of Int-Locations;
coherence
 {d,e} is Subset of Int-Locations
proofend;
let f be Int-Location;
:: original:{
redefine func{d,e,f} ->  Subset of Int-Locations;
coherence
 {d,e,f} is Subset of Int-Locations
proofend;
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
proofend;
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 &amp; k <> 0 )  }  &amp; ( 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)} ) &amp; ( 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 &amp; k <> 0 )  }  &amp; ( 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)} ) &amp; ( for i being Element of NAT holds b1 . i is infinite ) )
proofend;
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 &amp; k <> 0 )  }  &amp; ( 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)} ) &amp; ( for i being Element of NAT holds b1 . i is infinite ) &amp; b2 . 0 =  {  k where k is Element of NAT : ( not intloc k in L &amp; k <> 0 )  }  &amp; ( 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)} ) &amp; ( for i being Element of NAT holds b2 . i is infinite ) holds
b1 = b2
proofend;
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 &amp; k <> 0 )  }  &amp; ( 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)} ) &amp; ( 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 &amp; ( for m being Element of NAT st m in (RWNotIn-seq L) . n holds
not intloc m in L ) )
proofend;

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))
proofend;

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)
proofend;

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
proofend;
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
proofend;

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
proofend;

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 ) &amp; ( for x being FinSeq-Location st x in Floc holds
s1 . x = s2 . x ) ) )
proofend;

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 ) &amp; ( for x being FinSeq-Location holds s1 . x = s2 . x ) ) )
proofend;

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 )
proofend;

theorem :: SCMFSA_M:30
for s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s holds
s . (intloc 0) = 1
proofend;

registration
let n be Element of NAT ;
cluster intloc (n + 1) ->  read-write ;
coherence
 not intloc (n + 1) is read-only
proofend;
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
proofend;
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}
proofend;

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)
proofend;

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 &amp; s . (intloc 0) = 1 )
proofend;

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
proofend;

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 &amp; u is FinSequence of INT &amp; u is non-increasing &amp; p = (fsloc 0) .--> t &amp; 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 &amp; u is FinSequence of INT &amp; u is non-increasing &amp; p = (fsloc 0) .--> t &amp; q = (fsloc 0) .--> u ) )
proofend;
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 &amp; u is FinSequence of INT &amp; u is non-increasing &amp; p = (fsloc 0) .--> t &amp; q = (fsloc 0) .--> u ) ) ) &amp; ( 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 &amp; u is FinSequence of INT &amp; u is non-increasing &amp; p = (fsloc 0) .--> t &amp; q = (fsloc 0) .--> u ) ) ) holds
b1 = b2
proofend;
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 &amp; u is FinSequence of INT &amp; u is non-increasing &amp; p = (fsloc 0) .--> t &amp; 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 )
proofend;

theorem :: SCMFSA_M:36
for t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent &amp; u is non-increasing &amp; u is FinSequence of INT &amp; Sorting-Function . ((fsloc 0) .--> t) = (fsloc 0) .--> u )
proofend;

:: SCMFSA6C:3
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 ) &amp; ( for f being FinSeq-Location holds (Initialized s) . f = s . f ) )
proofend;