:: 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
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 ((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 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 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 Th43: :: SCMFSA_M:3
for p being PartState of SCM+FSA holds dom (Initialized p) = ((dom p) \/ {(intloc 0)}) \/ {(IC )}
proof 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 end;

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

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

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

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

theorem Th12: :: SCMFSA_M:12
(Initialize ((intloc 0) .--> 1)) . (intloc 0) = 1
proof 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;
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;
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 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 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 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 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 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 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 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;

begin

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 . (intloc 0) = 1 holds
Initialize s = Initialized s
proof end;

theorem :: SCMFSA_M:19
for s being State of SCM+FSA st s . (intloc 0) = 1 holds
DataPart (Initialized s) = DataPart s
proof 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 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 end;

begin

definition
let d be Int-Location;
:: original: {
redefine func {d} -> Subset of Int-Locations;
coherence
{d} is Subset of Int-Locations
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 -> 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 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 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 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 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 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 ((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;
cluster n -thRWNotIn L -> read-write ;
coherence
not n -thRWNotIn L is read-only
proof 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 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 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 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 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 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 end;

registration
let n be Element of NAT ;
cluster intloc (n + 1) -> read-write ;
coherence
not intloc (n + 1) is read-only
proof end;
end;

begin

registration
let f be FinSeq-Location ;
let t be FinSequence of INT ;
cluster f .--> t -> the_Values_of SCM+FSA -compatible ;
coherence
f .--> t is the_Values_of SCM+FSA -compatible
proof 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 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 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 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 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 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 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 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 end;

:: 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 ) & ( for f being FinSeq-Location holds (Initialized s) . f = s . f ) )
proof end;