:: On the memory of SCM+FSA
:: by Library Committee
::
:: Copyright (c) 2011-2021 Association of Mizar Users

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

set q = () .--> 1;

set f = the_Values_of SCM+FSA;

registration
let n be Nat;
let i be Integer;
coherence
proof end;
end;

definition
let I be PartState of SCM+FSA;
func Initialized I -> PartState of SCM+FSA equals :: SCMFSA_M:def 1
I +* (Initialize (() .--> 1));
coherence
I +* (Initialize (() .--> 1)) is PartState of SCM+FSA
;
projectivity
for b1, b2 being PartState of SCM+FSA st b1 = b2 +* (Initialize (() .--> 1)) holds
b1 = b1 +* (Initialize (() .--> 1))
;
end;

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

registration
let I be PartState of SCM+FSA;
coherence ;
end;

registration
let I be FinPartState of SCM+FSA;
coherence ;
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 Nat holds
( S . () = F1(i) & S . () = F2(i) ) ) )
proof 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 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 end;

theorem Th3: :: SCMFSA_M:3
for p being PartState of SCM+FSA holds dom () = ((dom p) \/ {()}) \/ {()}
proof end;

registration
let s be State of SCM+FSA;
coherence ;
end;

theorem Th4: :: SCMFSA_M:4
for p being PartState of SCM+FSA holds intloc 0 in dom ()
proof end;

theorem :: SCMFSA_M:5
for p being PartState of SCM+FSA holds
( () . () = 1 & () . () = 0 )
proof 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 ()
proof 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 ()
proof end;

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

theorem :: SCMFSA_M:9
for p being PartState of SCM+FSA holds () . () = 1
proof end;

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

theorem Th11: :: SCMFSA_M:11
dom (Initialize (() .--> 1)) = {(),()}
proof end;

theorem Th12: :: SCMFSA_M:12
(Initialize (() .--> 1)) . () = 1
proof end;

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

registration
coherence
not Int-Locations is empty
;
end;

definition
let IT be Int-Location;
attr IT 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;
end;

registration
coherence ;
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 end;
end;

definition
let L be finite Subset of Int-Locations;
func FirstNotIn L -> Int-Location means :Def3: :: 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 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 Def3 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 end;

theorem :: SCMFSA_M:15
for m, n being Nat
for L being finite Subset of Int-Locations st FirstNotIn L = intloc m & not intloc n in L holds
m <= n
proof end;

definition
let L be finite Subset of FinSeq-Locations;
func First*NotIn L -> FinSeq-Location means :Def4: :: 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 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 Def4 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 end;

theorem :: SCMFSA_M:17
for m, n being Nat
for L being finite Subset of FinSeq-Locations st First*NotIn L = fsloc m & not fsloc n in L holds
m <= n
proof end;

registration
let s be State of SCM+FSA;
let li be Int-Location;
let k be Integer;
cluster s +* (li,k) -> the_Values_of SCM+FSA -compatible ;
coherence
s +* (li,k) is the_Values_of SCM+FSA -compatible
proof end;
end;

registration
let a be Int-Location;
let n be Nat;
cluster a .--> 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 . () = 1 holds
Initialize s = Initialized s
proof end;

theorem :: SCMFSA_M:19
for s being State of SCM+FSA st s . () = 1 holds
DataPart () = DataPart s
proof end;

theorem :: SCMFSA_M:20
for s1, s2 being State of SCM+FSA st s1 . () = s2 . () & ( 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 end;

theorem :: SCMFSA_M:21
for s being State of SCM+FSA
for a being Int-Location
for l being Nat holds (s +* (Start-At (l,SCM+FSA))) . a = s . a
proof end;

definition
let d be Int-Location;
:: original: {
redefine func {d} -> Subset of Int-Locations;
coherence
proof end;
let e be Int-Location;
:: original: {
redefine func {d,e} -> Subset of Int-Locations;
coherence
{d,e} is Subset of Int-Locations
proof 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 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 end;
end;

definition
let L be finite Subset of Int-Locations;
func RWNotIn-seq L -> sequence of () means :Def5: :: SCMFSA_M:def 5
( it . 0 = { k where k is Element of NAT : ( not intloc k in L & k <> 0 ) } & ( for i being Nat
for sn being non empty Subset of NAT st it . i = sn holds
it . (i + 1) = sn \ {(min sn)} ) & ( for i being Nat holds it . i is infinite ) );
existence
ex b1 being sequence of () st
( b1 . 0 = { k where k is Element of NAT : ( not intloc k in L & k <> 0 ) } & ( for i being Nat
for sn being non empty Subset of NAT st b1 . i = sn holds
b1 . (i + 1) = sn \ {(min sn)} ) & ( for i being Nat holds b1 . i is infinite ) )
proof end;
uniqueness
for b1, b2 being sequence of () st b1 . 0 = { k where k is Element of NAT : ( not intloc k in L & k <> 0 ) } & ( for i being Nat
for sn being non empty Subset of NAT st b1 . i = sn holds
b1 . (i + 1) = sn \ {(min sn)} ) & ( for i being 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 Nat
for sn being non empty Subset of NAT st b2 . i = sn holds
b2 . (i + 1) = sn \ {(min sn)} ) & ( for i being Nat holds b2 . i is infinite ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines RWNotIn-seq SCMFSA_M:def 5 :
for L being finite Subset of Int-Locations
for b2 being sequence of () 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 Nat
for sn being non empty Subset of NAT st b2 . i = sn holds
b2 . (i + 1) = sn \ {(min sn)} ) & ( for i being Nat holds b2 . i is infinite ) ) );

registration
let L be finite Subset of Int-Locations;
let n be Nat;
cluster () . n -> non empty ;
coherence
not () . n is empty
by Def5;
end;

theorem Th22: :: SCMFSA_M:22
for n being Nat
for L being finite Subset of Int-Locations holds
( not 0 in () . n & ( for m being Nat st m in () . n holds
not intloc m in L ) )
proof end;

theorem Th23: :: SCMFSA_M:23
for L being finite Subset of Int-Locations
for n being Nat holds min (() . n) < min (() . (n + 1))
proof end;

theorem Th24: :: SCMFSA_M:24
for L being finite Subset of Int-Locations
for n, m being Element of NAT st n < m holds
min (() . n) < min (() . m)
proof end;

definition
let n be Element of NAT ;
let L be finite Subset of Int-Locations;
func n -thRWNotIn L -> Int-Location equals :: SCMFSA_M:def 6
intloc (min (() . n));
correctness
coherence
intloc (min (() . 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 (() . 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;
coherence
not n -thRWNotIn L is read-only
proof end;
end;

theorem :: SCMFSA_M:25
for L being finite Subset of Int-Locations
for n being Element of NAT holds not n -thRWNotIn L in L
proof end;

theorem :: SCMFSA_M:26
for L being finite Subset of Int-Locations
for n, m being Element of NAT st n <> m holds
n -thRWNotIn L <> m -thRWNotIn L
proof end;

theorem Th27: :: 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 end;

theorem :: SCMFSA_M:28
for s1, s2 being State of SCM+FSA
for Iloc being Subset of Int-Locations holds
( s1 | () = s2 | () 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 end;

theorem :: SCMFSA_M:29
for x being set
for i, m, n being Nat holds
( not x in dom ((() .--> m) +* (Start-At (n,SCM+FSA))) or x = intloc i or x = IC )
proof end;

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

registration
let n be Nat;
cluster intloc (n + 1) -> read-write ;
coherence
not intloc (n + 1) is read-only
by AMI_3:10;
end;

registration
let f be FinSeq-Location ;
let t be FinSequence of INT ;
coherence
proof end;
end;

theorem :: SCMFSA_M:31
for w being FinSequence of INT
for f being FinSeq-Location holds dom (Initialized (f .--> w)) = {(),(),f}
proof end;

theorem :: SCMFSA_M:32
for t being FinSequence of INT
for f being FinSeq-Location holds dom (Initialize (() .--> 1)) misses dom (f .--> t)
proof 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 . () = 1 )
proof end;

theorem :: SCMFSA_M:34
for f being FinSeq-Location
for a being Int-Location
for s being State of SCM+FSA holds {a,(),f} c= dom s
proof end;

definition
func Sorting-Function -> PartFunc of , means :Def7: :: 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 = () .--> t & q = () .--> u ) );
existence
ex b1 being PartFunc of , 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 = () .--> t & q = () .--> u ) )
proof end;
uniqueness
for b1, b2 being PartFunc of , 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 = () .--> t & q = () .--> 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 = () .--> t & q = () .--> u ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines Sorting-Function SCMFSA_M:def 7 :
for b1 being PartFunc of , 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 = () .--> t & q = () .--> u ) ) );

theorem :: SCMFSA_M:35
for p being set holds
( p in dom Sorting-Function iff ex t being FinSequence of INT st p = () .--> t )
proof 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 . (() .--> t) = () .--> u )
proof end;

:: SCMFSA6C:3
theorem :: SCMFSA_M:37
for s being State of SCM+FSA holds
( ( for a being read-write Int-Location holds () . a = s . a ) & ( for f being FinSeq-Location holds () . f = s . f ) )
proof end;

theorem :: SCMFSA_M:38
for a being Int-Location
for s being State of SCM+FSA holds () . a = s . a
proof end;