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

coherence

(intloc n) .--> i is the_Values_of SCM+FSA -compatible

end;
let i be Integer;

coherence

(intloc n) .--> i is the_Values_of SCM+FSA -compatible

proof end;

definition

let I be PartState of SCM+FSA;

I +* (Initialize ((intloc 0) .--> 1)) is PartState of SCM+FSA ;

projectivity

for b_{1}, b_{2} being PartState of SCM+FSA st b_{1} = b_{2} +* (Initialize ((intloc 0) .--> 1)) holds

b_{1} = b_{1} +* (Initialize ((intloc 0) .--> 1))

end;
func Initialized I -> PartState of SCM+FSA equals :: SCMFSA_M:def 1

I +* (Initialize ((intloc 0) .--> 1));

coherence I +* (Initialize ((intloc 0) .--> 1));

I +* (Initialize ((intloc 0) .--> 1)) is PartState of SCM+FSA ;

projectivity

for b

b

proof end;

:: deftheorem defines Initialized SCMFSA_M:def 1 :

for I being PartState of SCM+FSA holds Initialized I = I +* (Initialize ((intloc 0) .--> 1));

for I being PartState of SCM+FSA holds Initialized I = I +* (Initialize ((intloc 0) .--> 1));

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 )

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 )

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

registration
end;

theorem :: SCMFSA_M:5

for p being PartState of SCM+FSA holds

( (Initialized p) . (intloc 0) = 1 & (Initialized p) . (IC ) = 0 )

( (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)

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)

for f being FinSeq-Location st not f in dom p holds

not f in dom (Initialized p)

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

definition
end;

:: deftheorem Def2 defines read-only SCMFSA_M:def 2 :

for IT being Int-Location holds

( IT is read-only iff IT = intloc 0 );

for IT being Int-Location holds

( IT is read-only iff IT = intloc 0 );

definition

let L be finite Subset of Int-Locations;

ex b_{1} being Int-Location ex sn being non empty Subset of NAT st

( b_{1} = intloc (min sn) & sn = { k where k is Element of NAT : not intloc k in L } )

for b_{1}, b_{2} being Int-Location st ex sn being non empty Subset of NAT st

( b_{1} = 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_{2} = intloc (min sn) & sn = { k where k is Element of NAT : not intloc k in L } ) holds

b_{1} = b_{2}
;

end;
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 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 } );

ex b

( b

proof end;

uniqueness for b

( b

( b

b

:: deftheorem Def6 defines FirstNotIn SCMFSA_M:def 3 :

for L being finite Subset of Int-Locations

for b_{2} being Int-Location holds

( b_{2} = FirstNotIn L iff ex sn being non empty Subset of NAT st

( b_{2} = intloc (min sn) & sn = { k where k is Element of NAT : not intloc k in L } ) );

for L being finite Subset of Int-Locations

for b

( b

( b

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

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;

ex b_{1} being FinSeq-Location ex sn being non empty Subset of NAT st

( b_{1} = fsloc (min sn) & sn = { k where k is Element of NAT : not fsloc k in L } )

for b_{1}, b_{2} being FinSeq-Location st ex sn being non empty Subset of NAT st

( b_{1} = 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_{2} = fsloc (min sn) & sn = { k where k is Element of NAT : not fsloc k in L } ) holds

b_{1} = b_{2}
;

end;
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 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 } );

ex b

( b

proof end;

uniqueness for b

( b

( b

b

:: deftheorem Def8 defines First*NotIn SCMFSA_M:def 4 :

for L being finite Subset of FinSeq-Locations

for b_{2} being FinSeq-Location holds

( b_{2} = First*NotIn L iff ex sn being non empty Subset of NAT st

( b_{2} = fsloc (min sn) & sn = { k where k is Element of NAT : not fsloc k in L } ) );

for L being finite Subset of FinSeq-Locations

for b

( b

( b

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

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;

coherence

s +* (li,k) is the_Values_of SCM+FSA -compatible

end;
let li be Int-Location;

let k be Integer;

coherence

s +* (li,k) is the_Values_of SCM+FSA -compatible

proof end;

begin

registration

let a be Int-Location;

let n be Nat;

coherence

for b_{1} being PartState of SCM+FSA st b_{1} = a .--> n holds

b_{1} is data-only
;

end;
let n be Nat;

coherence

for b

b

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

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

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

:: original: {

redefine func {d,e} -> Subset of Int-Locations;

coherence

{d,e} is Subset of Int-Locations

:: original: {

redefine func {d,e,f} -> Subset of Int-Locations;

coherence

{d,e,f} is Subset of Int-Locations

:: original: {

redefine func {d,e,f,g} -> Subset of Int-Locations;

coherence

{d,e,f,g} is Subset of Int-Locations

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

definition

let L be finite Subset of Int-Locations;

ex b_{1} being Function of NAT,(bool NAT) st

( b_{1} . 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 b_{1} . i = sn holds

b_{1} . (i + 1) = sn \ {(min sn)} ) & ( for i being Element of NAT holds b_{1} . i is infinite ) )

for b_{1}, b_{2} being Function of NAT,(bool NAT) st b_{1} . 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 b_{1} . i = sn holds

b_{1} . (i + 1) = sn \ {(min sn)} ) & ( for i being Element of NAT holds b_{1} . i is infinite ) & b_{2} . 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 b_{2} . i = sn holds

b_{2} . (i + 1) = sn \ {(min sn)} ) & ( for i being Element of NAT holds b_{2} . i is infinite ) holds

b_{1} = b_{2}

end;
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 ( 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 ) );

ex b

( b

for sn being non empty Subset of NAT st b

b

proof end;

uniqueness for b

for sn being non empty Subset of NAT st b

b

for sn being non empty Subset of NAT st b

b

b

proof end;

:: deftheorem Def2 defines RWNotIn-seq SCMFSA_M:def 5 :

for L being finite Subset of Int-Locations

for b_{2} being Function of NAT,(bool NAT) holds

( b_{2} = RWNotIn-seq L iff ( b_{2} . 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 b_{2} . i = sn holds

b_{2} . (i + 1) = sn \ {(min sn)} ) & ( for i being Element of NAT holds b_{2} . i is infinite ) ) );

for L being finite Subset of Int-Locations

for b

( b

for sn being non empty Subset of NAT st b

b

registration

let L be finite Subset of Int-Locations;

let n be Element of NAT ;

coherence

not (RWNotIn-seq L) . n is empty by Def2;

end;
let n be Element of NAT ;

coherence

not (RWNotIn-seq L) . n is empty by Def2;

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

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

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)

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;

correctness

coherence

intloc (min ((RWNotIn-seq L) . n)) is Int-Location;

;

end;
let L be finite Subset of Int-Locations;

correctness

coherence

intloc (min ((RWNotIn-seq L) . n)) is Int-Location;

;

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

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

registration

let n be Element of NAT ;

let L be finite Subset of Int-Locations;

coherence

not n -thRWNotIn L is read-only

end;
let L be finite Subset of Int-Locations;

coherence

not n -thRWNotIn L is read-only

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

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

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

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 )

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;

begin

registration

let f be FinSeq-Location ;

let t be FinSequence of INT ;

coherence

f .--> t is the_Values_of SCM+FSA -compatible

end;
let t be FinSequence of INT ;

coherence

f .--> t is the_Values_of SCM+FSA -compatible

proof 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}

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)

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 )

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

for a being Int-Location

for s being State of SCM+FSA holds {a,(IC ),f} c= dom s

proof end;

definition

ex b_{1} being PartFunc of (FinPartSt SCM+FSA),(FinPartSt SCM+FSA) st

for p, q being FinPartState of SCM+FSA holds

( [p,q] in b_{1} 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 b_{1}, b_{2} being PartFunc of (FinPartSt SCM+FSA),(FinPartSt SCM+FSA) st ( for p, q being FinPartState of SCM+FSA holds

( [p,q] in b_{1} 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_{2} 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_{1} = b_{2}
end;

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

ex b

for p, q being FinPartState of SCM+FSA holds

( [p,q] in b

( 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

( [p,q] in b

( 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

( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0) .--> t & q = (fsloc 0) .--> u ) ) ) holds

b

proof end;

:: deftheorem Def3 defines Sorting-Function SCMFSA_M:def 7 :

for b_{1} being PartFunc of (FinPartSt SCM+FSA),(FinPartSt SCM+FSA) holds

( b_{1} = Sorting-Function iff for p, q being FinPartState of SCM+FSA holds

( [p,q] in b_{1} 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 b

( b

( [p,q] in b

( 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 )

( 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 )

( 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 ) )

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