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

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 b₁, b₂ being PartState of SCM+FSA st b₁ = b₂ +* (Initialize ((intloc 0) .--> 1)) holds
b₁ = b₁ +* (Initialize ((intloc 0) .--> 1)) ;

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{ F₁( set ) -> Integer, F₂( set ) -> FinSequence of INT , F₃() -> Element of NAT } :

ex S being State of SCM+FSA st
( IC S = F₃() & ( for i being Nat holds
( S . (intloc i) = F₁(i) & S . (fsloc i) = F₂(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 (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;

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 ;

end;

registration

cluster Int-like read-write for Element of the carrier of SCM+FSA;

existence
ex b₁ being Int-Location st b₁ 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 b₁ being Int-Location ex sn being non empty Subset of NAT st
( b₁ = intloc (min sn) & sn = { k where k is Element of NAT : not intloc k in L } )

proof end;

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

end;

:: deftheorem Def3 defines FirstNotIn SCMFSA_M:def 3 :
for L being finite Subset of Int-Locations
for b₂ being Int-Location holds
( b₂ = FirstNotIn L iff ex sn being non empty Subset of NAT st
( b₂ = 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 b₁ being FinSeq-Location ex sn being non empty Subset of NAT st
( b₁ = fsloc (min sn) & sn = { k where k is Element of NAT : not fsloc k in L } )

proof end;

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

end;

:: deftheorem Def4 defines First*NotIn SCMFSA_M:def 4 :
for L being finite Subset of FinSeq-Locations
for b₂ being FinSeq-Location holds
( b₂ = First*NotIn L iff ex sn being non empty Subset of NAT st
( b₂ = 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 b₁ being PartState of SCM+FSA st b₁ = a .--> n holds
b₁ 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 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
{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 -> sequence of (bool NAT) 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 b₁ being sequence of (bool NAT) st
( b₁ . 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 b₁ . i = sn holds
b₁ . (i + 1) = sn \ {(min sn)} ) & ( for i being Nat holds b₁ . i is infinite ) )

proof end;

uniqueness
for b₁, b₂ being sequence of (bool NAT) st b₁ . 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 b₁ . i = sn holds
b₁ . (i + 1) = sn \ {(min sn)} ) & ( for i being Nat holds b₁ . i is infinite ) & b₂ . 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 b₂ . i = sn holds
b₂ . (i + 1) = sn \ {(min sn)} ) & ( for i being Nat holds b₂ . i is infinite ) holds
b₁ = b₂

proof end;

end;

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

registration

let L be finite Subset of Int-Locations;
let n be Nat;

cluster (RWNotIn-seq L) . n -> non empty ;

coherence
not (RWNotIn-seq L) . 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 (RWNotIn-seq L) . n & ( for m being Nat st m in (RWNotIn-seq L) . 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 ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . (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 ((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 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 | (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;

theorem :: SCMFSA_M:29

for x being set
for i, m, n being 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 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 ;

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 :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 = (fsloc 0) .--> t & q = (fsloc 0) .--> u ) );

existence
ex b₁ being PartFunc of (FinPartSt SCM+FSA),(FinPartSt SCM+FSA) st
for p, q being FinPartState of SCM+FSA holds
( [p,q] in b₁ 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 b₁, b₂ being PartFunc of (FinPartSt SCM+FSA),(FinPartSt SCM+FSA) st ( for p, q being FinPartState of SCM+FSA holds
( [p,q] in b₁ 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 b₂ 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
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines Sorting-Function SCMFSA_M:def 7 :
for b₁ being PartFunc of (FinPartSt SCM+FSA),(FinPartSt SCM+FSA) holds
( b₁ = Sorting-Function iff for p, q being FinPartState of SCM+FSA holds
( [p,q] in b₁ 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;

theorem :: SCMFSA_M:38

for a being Int-Location
for s being State of SCM+FSA holds (Initialize s) . a = s . a

proof end;