:: by Andrzej Trybulec

::

:: Received April 28, 2011

:: Copyright (c) 2011-2019 Association of Mizar Users

definition

let N be set ;

attr c_{2} is strict ;

struct Mem-Struct over N -> ZeroStr ;

aggr Mem-Struct(# carrier, ZeroF, Object-Kind, ValuesF #) -> Mem-Struct over N;

sel Object-Kind c_{2} -> Function of the carrier of c_{2},N;

sel ValuesF c_{2} -> ManySortedSet of N;

end;
attr c

struct Mem-Struct over N -> ZeroStr ;

aggr Mem-Struct(# carrier, ZeroF, Object-Kind, ValuesF #) -> Mem-Struct over N;

sel Object-Kind c

sel ValuesF c

definition

let N be with_zero set ;

ex b_{1} being strict Mem-Struct over N st

( the carrier of b_{1} = {0} & the ZeroF of b_{1} = 0 & the Object-Kind of b_{1} = 0 .--> 0 & the ValuesF of b_{1} = N --> NAT )

for b_{1}, b_{2} being strict Mem-Struct over N st the carrier of b_{1} = {0} & the ZeroF of b_{1} = 0 & the Object-Kind of b_{1} = 0 .--> 0 & the ValuesF of b_{1} = N --> NAT & the carrier of b_{2} = {0} & the ZeroF of b_{2} = 0 & the Object-Kind of b_{2} = 0 .--> 0 & the ValuesF of b_{2} = N --> NAT holds

b_{1} = b_{2}
;

end;
func Trivial-Mem N -> strict Mem-Struct over N means :Def1: :: MEMSTR_0:def 1

( the carrier of it = {0} & the ZeroF of it = 0 & the Object-Kind of it = 0 .--> 0 & the ValuesF of it = N --> NAT );

existence ( the carrier of it = {0} & the ZeroF of it = 0 & the Object-Kind of it = 0 .--> 0 & the ValuesF of it = N --> NAT );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def1 defines Trivial-Mem MEMSTR_0:def 1 :

for N being with_zero set

for b_{2} being strict Mem-Struct over N holds

( b_{2} = Trivial-Mem N iff ( the carrier of b_{2} = {0} & the ZeroF of b_{2} = 0 & the Object-Kind of b_{2} = 0 .--> 0 & the ValuesF of b_{2} = N --> NAT ) );

for N being with_zero set

for b

( b

registration

let N be with_zero set ;

existence

ex b_{1} being Mem-Struct over N st b_{1} is 1 -element

end;
existence

ex b

proof end;

notation

let N be with_zero set ;

let S be Mem-Struct over N;

synonym IC S for 0. N;

synonym Data-Locations S for NonZero N;

end;
let S be Mem-Struct over N;

synonym IC S for 0. N;

synonym Data-Locations S for NonZero N;

definition

let N be with_zero set ;

let S be Mem-Struct over N;

the ValuesF of S * the Object-Kind of S is ManySortedSet of the carrier of S ;

end;
let S be Mem-Struct over N;

func the_Values_of S -> ManySortedSet of the carrier of S equals :: MEMSTR_0:def 2

the ValuesF of S * the Object-Kind of S;

coherence the ValuesF of S * the Object-Kind of S;

the ValuesF of S * the Object-Kind of S is ManySortedSet of the carrier of S ;

:: deftheorem defines the_Values_of MEMSTR_0:def 2 :

for N being with_zero set

for S being Mem-Struct over N holds the_Values_of S = the ValuesF of S * the Object-Kind of S;

for N being with_zero set

for S being Mem-Struct over N holds the_Values_of S = the ValuesF of S * the Object-Kind of S;

definition

let N be with_zero set ;

let S be Mem-Struct over N;

mode PartState of S is the carrier of S -defined the_Values_of S -compatible Function;

end;
let S be Mem-Struct over N;

mode PartState of S is the carrier of S -defined the_Values_of S -compatible Function;

:: Jest potrzeba zagwarantowania, ze

:: the_Values_of S is non-empty

:: to bylo wczsniej obsluzone, ze stary N byl

:: with_non-empty_elements

:: teraz jest to wlasnosc Mem-Str

:: sa tutaj rozne warianty, najprosciej jednak napisac co wymgamy:

:: the_Values_of S is non-empty

:: to bylo wczsniej obsluzone, ze stary N byl

:: with_non-empty_elements

:: teraz jest to wlasnosc Mem-Str

:: sa tutaj rozne warianty, najprosciej jednak napisac co wymgamy:

:: deftheorem Def3 defines with_non-empty_values MEMSTR_0:def 3 :

for N being with_zero set

for S being Mem-Struct over N holds

( S is with_non-empty_values iff the_Values_of S is non-empty );

for N being with_zero set

for S being Mem-Struct over N holds

( S is with_non-empty_values iff the_Values_of S is non-empty );

registration
end;

registration

let N be with_zero set ;

existence

ex b_{1} being Mem-Struct over N st b_{1} is with_non-empty_values

end;
existence

ex b

proof end;

registration

let N be with_zero set ;

let S be with_non-empty_values Mem-Struct over N;

coherence

the_Values_of S is non-empty by Def3;

end;
let S be with_non-empty_values Mem-Struct over N;

coherence

the_Values_of S is non-empty by Def3;

definition

let N be with_zero set ;

let S be with_non-empty_values Mem-Struct over N;

mode State of S is total PartState of S;

end;
let S be with_non-empty_values Mem-Struct over N;

mode State of S is total PartState of S;

definition
end;

definition

let N be with_zero set ;

let S be non empty Mem-Struct over N;

let o be Object of S;

correctness

coherence

the Object-Kind of S . o is Element of N;

;

end;
let S be non empty Mem-Struct over N;

let o be Object of S;

correctness

coherence

the Object-Kind of S . o is Element of N;

;

:: deftheorem defines ObjectKind MEMSTR_0:def 4 :

for N being with_zero set

for S being non empty Mem-Struct over N

for o being Object of S holds ObjectKind o = the Object-Kind of S . o;

for N being with_zero set

for S being non empty Mem-Struct over N

for o being Object of S holds ObjectKind o = the Object-Kind of S . o;

definition

let N be with_zero set ;

let S be non empty Mem-Struct over N;

let o be Object of S;

correctness

coherence

(the_Values_of S) . o is set ;

;

end;
let S be non empty Mem-Struct over N;

let o be Object of S;

correctness

coherence

(the_Values_of S) . o is set ;

;

:: deftheorem defines Values MEMSTR_0:def 5 :

for N being with_zero set

for S being non empty Mem-Struct over N

for o being Object of S holds Values o = (the_Values_of S) . o;

for N being with_zero set

for S being non empty Mem-Struct over N

for o being Object of S holds Values o = (the_Values_of S) . o;

:: Jezeli dodamy wartosci, to pewnie nie unikniemy zdefiniowania

:: funktora, ktory odpowiada staremu Object-Kind

:: np. the_Object-Kind_of, lub the_Values_of

:: i wtedy podmiana nie powinna byc zbyt skomplikowana.

:: Poza tym trzeba bedzie zmienic komputery, dodajac pole ValuesF

:: wykorzystac mozna atrybut with_zero, ale trzeba wprowadzic nowy:

:: (the ValuesF of S).0 = NAT

:: funktora, ktory odpowiada staremu Object-Kind

:: np. the_Object-Kind_of, lub the_Values_of

:: i wtedy podmiana nie powinna byc zbyt skomplikowana.

:: Poza tym trzeba bedzie zmienic komputery, dodajac pole ValuesF

:: wykorzystac mozna atrybut with_zero, ale trzeba wprowadzic nowy:

:: (the ValuesF of S).0 = NAT

:: deftheorem Def6 defines IC-Ins-separated MEMSTR_0:def 6 :

for N being with_zero set

for IT being non empty Mem-Struct over N holds

( IT is IC-Ins-separated iff Values (IC ) = NAT );

for N being with_zero set

for IT being non empty Mem-Struct over N holds

( IT is IC-Ins-separated iff Values (IC ) = NAT );

Lm1: for N being with_zero set holds the_Values_of (Trivial-Mem N) = 0 .--> NAT

proof end;

registration

let N be with_zero set ;

ex b_{1} being 1 -element Mem-Struct over N st

( b_{1} is IC-Ins-separated & b_{1} is with_non-empty_values & b_{1} is strict )

end;
cluster non empty V116() finite 1 -element strict with_non-empty_values IC-Ins-separated for Mem-Struct over N;

existence ex b

( b

proof end;

definition

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let p be PartState of S;

coherence

p . (IC ) is Element of NAT

end;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let p be PartState of S;

coherence

p . (IC ) is Element of NAT

proof end;

:: deftheorem defines IC MEMSTR_0:def 7 :

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S holds IC p = p . (IC );

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S holds IC p = p . (IC );

theorem :: MEMSTR_0:1

for N being with_zero set

for S being 1 -element with_non-empty_values IC-Ins-separated Mem-Struct over N

for s1, s2 being State of S st IC s1 = IC s2 holds

s1 = s2

for S being 1 -element with_non-empty_values IC-Ins-separated Mem-Struct over N

for s1, s2 being State of S st IC s1 = IC s2 holds

s1 = s2

proof end;

registration

let N be with_zero set ;

let S be non empty with_non-empty_values Mem-Struct over N;

let o be Object of S;

coherence

not Values o is empty ;

end;
let S be non empty with_non-empty_values Mem-Struct over N;

let o be Object of S;

coherence

not Values o is empty ;

registration

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let la be Object of S;

let a be Element of Values la;

coherence

la .--> a is the_Values_of S -compatible

let b be Element of Values lb;

coherence

(la,lb) --> (a,b) is the_Values_of S -compatible ;

end;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let la be Object of S;

let a be Element of Values la;

coherence

la .--> a is the_Values_of S -compatible

proof end;

let lb be Object of S;let b be Element of Values lb;

coherence

(la,lb) --> (a,b) is the_Values_of S -compatible ;

theorem Th2: :: MEMSTR_0:2

for N being with_zero set

for S being non empty with_non-empty_values Mem-Struct over N

for s being State of S holds IC in dom s

for S being non empty with_non-empty_values Mem-Struct over N

for s being State of S holds IC in dom s

proof end;

definition

let N be with_zero set ;

let S be Mem-Struct over N;

let p be PartState of S;

coherence

p | (Data-Locations ) is PartState of S ;

projectivity

for b_{1}, b_{2} being PartState of S st b_{1} = b_{2} | (Data-Locations ) holds

b_{1} = b_{1} | (Data-Locations )
;

end;
let S be Mem-Struct over N;

let p be PartState of S;

coherence

p | (Data-Locations ) is PartState of S ;

projectivity

for b

b

:: deftheorem defines DataPart MEMSTR_0:def 8 :

for N being with_zero set

for S being Mem-Struct over N

for p being PartState of S holds DataPart p = p | (Data-Locations );

for N being with_zero set

for S being Mem-Struct over N

for p being PartState of S holds DataPart p = p | (Data-Locations );

:: deftheorem Def9 defines data-only MEMSTR_0:def 9 :

for N being with_zero set

for S being Mem-Struct over N

for p being PartState of S holds

( p is data-only iff dom p misses {(IC )} );

for N being with_zero set

for S being Mem-Struct over N

for p being PartState of S holds

( p is data-only iff dom p misses {(IC )} );

registration

let N be with_zero set ;

let S be Mem-Struct over N;

for b_{1} being PartState of S st b_{1} is empty holds

b_{1} is data-only
by RELAT_1:38, XBOOLE_1:65;

end;
let S be Mem-Struct over N;

cluster empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible -> data-only for set ;

coherence for b

b

registration

let N be with_zero set ;

let S be Mem-Struct over N;

ex b_{1} being PartState of S st b_{1} is empty

end;
let S be Mem-Struct over N;

cluster empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible for set ;

existence ex b

proof end;

theorem Th3: :: MEMSTR_0:3

for N being with_zero set

for S being Mem-Struct over N

for p being PartState of S holds not IC in dom (DataPart p)

for S being Mem-Struct over N

for p being PartState of S holds not IC in dom (DataPart p)

proof end;

theorem :: MEMSTR_0:4

theorem :: MEMSTR_0:5

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being data-only PartState of S

for q being PartState of S holds

( p c= q iff p c= DataPart q )

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being data-only PartState of S

for q being PartState of S holds

( p c= q iff p c= DataPart q )

proof end;

registration

let N be with_zero set ;

let S be Mem-Struct over N;

let p be PartState of S;

coherence

DataPart p is data-only by Th3, ZFMISC_1:50;

end;
let S be Mem-Struct over N;

let p be PartState of S;

coherence

DataPart p is data-only by Th3, ZFMISC_1:50;

theorem Th6: :: MEMSTR_0:6

for N being with_zero set

for S being Mem-Struct over N

for p being PartState of S holds

( p is data-only iff dom p c= Data-Locations ) by RELAT_1:def 18, XBOOLE_1:86, XBOOLE_1:106;

for S being Mem-Struct over N

for p being PartState of S holds

( p is data-only iff dom p c= Data-Locations ) by RELAT_1:def 18, XBOOLE_1:86, XBOOLE_1:106;

theorem :: MEMSTR_0:7

for N being with_zero set

for S being Mem-Struct over N

for p being data-only PartState of S holds DataPart p = p

for S being Mem-Struct over N

for p being data-only PartState of S holds DataPart p = p

proof end;

theorem Th8: :: MEMSTR_0:8

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s being State of S holds Data-Locations c= dom s

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s being State of S holds Data-Locations c= dom s

proof end;

theorem Th9: :: MEMSTR_0:9

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s being State of S holds dom (DataPart s) = Data-Locations

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s being State of S holds dom (DataPart s) = Data-Locations

proof end;

theorem Th10: :: MEMSTR_0:10

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for d being data-only PartState of S holds not IC in dom d

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for d being data-only PartState of S holds not IC in dom d

proof end;

theorem Th11: :: MEMSTR_0:11

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for d being data-only PartState of S holds IC (p +* d) = IC p

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for d being data-only PartState of S holds IC (p +* d) = IC p

proof end;

theorem :: MEMSTR_0:12

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S holds DataPart p c= p by RELAT_1:59;

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S holds DataPart p c= p by RELAT_1:59;

theorem Th13: :: MEMSTR_0:13

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s being State of S holds dom s = {(IC )} \/ (Data-Locations )

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s being State of S holds dom s = {(IC )} \/ (Data-Locations )

proof end;

theorem :: MEMSTR_0:14

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S holds (dom p) /\ (Data-Locations ) = dom (DataPart p) by RELAT_1:61;

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S holds (dom p) /\ (Data-Locations ) = dom (DataPart p) by RELAT_1:61;

registration

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let l be Nat;

let s be State of S;

coherence

s +* ((IC ),l) is the_Values_of S -compatible

end;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let l be Nat;

let s be State of S;

coherence

s +* ((IC ),l) is the_Values_of S -compatible

proof end;

definition

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let l be Nat;

correctness

coherence

(IC ) .--> l is PartState of S;

end;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let l be Nat;

correctness

coherence

(IC ) .--> l is PartState of S;

proof end;

:: deftheorem defines Start-At MEMSTR_0:def 10 :

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for l being Nat holds Start-At (l,S) = (IC ) .--> l;

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for l being Nat holds Start-At (l,S) = (IC ) .--> l;

definition

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let l be Nat;

let p be PartState of S;

end;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let l be Nat;

let p be PartState of S;

:: deftheorem Def11 defines -started MEMSTR_0:def 11 :

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for l being Nat

for p being PartState of S holds

( p is l -started iff ( IC in dom p & IC p = l ) );

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for l being Nat

for p being PartState of S holds

( p is l -started iff ( IC in dom p & IC p = l ) );

registration

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let l be Nat;

coherence

( Start-At (l,S) is l -started & not Start-At (l,S) is empty )

end;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let l be Nat;

coherence

( Start-At (l,S) is l -started & not Start-At (l,S) is empty )

proof end;

theorem Th15: :: MEMSTR_0:15

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for l being Nat holds IC in dom (Start-At (l,S))

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for l being Nat holds IC in dom (Start-At (l,S))

proof end;

theorem Th16: :: MEMSTR_0:16

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for n being Nat holds IC (p +* (Start-At (n,S))) = n

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for n being Nat holds IC (p +* (Start-At (n,S))) = n

proof end;

registration

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let l be Nat;

ex b_{1} being State of S st b_{1} is l -started

end;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let l be Nat;

cluster non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible total l -started for set ;

existence ex b

proof end;

registration

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let l be Nat;

let p be PartState of S;

let q be l -started PartState of S;

coherence

p +* q is l -started

end;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let l be Nat;

let p be PartState of S;

let q be l -started PartState of S;

coherence

p +* q is l -started

proof end;

definition

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let l be Nat;

let s be State of S;

compatibility

( s is l -started iff IC s = l ) by Th2;

end;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let l be Nat;

let s be State of S;

compatibility

( s is l -started iff IC s = l ) by Th2;

:: deftheorem defines -started MEMSTR_0:def 12 :

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for l being Nat

for s being State of S holds

( s is l -started iff IC s = l );

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for l being Nat

for s being State of S holds

( s is l -started iff IC s = l );

theorem :: MEMSTR_0:17

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for l being Nat

for p being b_{3} -started PartState of S

for s being PartState of S st p c= s holds

s is l -started

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for l being Nat

for p being b

for s being PartState of S st p c= s holds

s is l -started

proof end;

theorem Th18: :: MEMSTR_0:18

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s being State of S holds Start-At ((IC s),S) = s | {(IC )}

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s being State of S holds Start-At ((IC s),S) = s | {(IC )}

proof end;

theorem Th19: :: MEMSTR_0:19

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S st IC in dom p holds

p = (Start-At ((IC p),S)) +* (DataPart p)

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S st IC in dom p holds

p = (Start-At ((IC p),S)) +* (DataPart p)

proof end;

theorem Th20: :: MEMSTR_0:20

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for l being Nat holds DataPart (Start-At (l,S)) = {}

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for l being Nat holds DataPart (Start-At (l,S)) = {}

proof end;

theorem :: MEMSTR_0:21

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for l1, l2, k being Nat holds

( Start-At ((l1 + k),S) = Start-At ((l2 + k),S) iff Start-At (l1,S) = Start-At (l2,S) )

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for l1, l2, k being Nat holds

( Start-At ((l1 + k),S) = Start-At ((l2 + k),S) iff Start-At (l1,S) = Start-At (l2,S) )

proof end;

theorem :: MEMSTR_0:22

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for l1, l2, k being Nat st Start-At (l1,S) = Start-At (l2,S) holds

Start-At ((l1 -' k),S) = Start-At ((l2 -' k),S)

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for l1, l2, k being Nat st Start-At (l1,S) = Start-At (l2,S) holds

Start-At ((l1 -' k),S) = Start-At ((l2 -' k),S)

proof end;

theorem Th23: :: MEMSTR_0:23

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for d being data-only PartState of S

for k being Nat holds d tolerates Start-At (k,S)

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for d being data-only PartState of S

for k being Nat holds d tolerates Start-At (k,S)

proof end;

theorem Th24: :: MEMSTR_0:24

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S st IC in dom p holds

dom p = {(IC )} \/ (dom (DataPart p))

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S st IC in dom p holds

dom p = {(IC )} \/ (dom (DataPart p))

proof end;

theorem :: MEMSTR_0:25

theorem Th26: :: MEMSTR_0:26

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S st IC in dom p holds

p = (DataPart p) +* (Start-At ((IC p),S))

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S st IC in dom p holds

p = (DataPart p) +* (Start-At ((IC p),S))

proof end;

theorem Th27: :: MEMSTR_0:27

for k being Nat

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S holds IC in dom (p +* (Start-At (k,S)))

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S holds IC in dom (p +* (Start-At (k,S)))

proof end;

theorem :: MEMSTR_0:28

for k being Nat

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s being State of S

for p being PartState of S st p +* (Start-At (k,S)) c= s holds

IC s = k

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s being State of S

for p being PartState of S st p +* (Start-At (k,S)) c= s holds

IC s = k

proof end;

theorem Th29: :: MEMSTR_0:29

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for l being Nat

for p being PartState of S holds

( p is l -started iff Start-At (l,S) c= p )

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for l being Nat

for p being PartState of S holds

( p is l -started iff Start-At (l,S) c= p )

proof end;

registration

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let k be Nat;

let p be k -started PartState of S;

let d be data-only PartState of S;

coherence

p +* d is k -started

end;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let k be Nat;

let p be k -started PartState of S;

let d be data-only PartState of S;

coherence

p +* d is k -started

proof end;

theorem Th30: :: MEMSTR_0:30

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s being State of S holds Start-At ((IC s),S) c= s

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s being State of S holds Start-At ((IC s),S) c= s

proof end;

theorem :: MEMSTR_0:31

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s being State of S holds s +* (Start-At ((IC s),S)) = s by Th30, FUNCT_4:98;

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s being State of S holds s +* (Start-At ((IC s),S)) = s by Th30, FUNCT_4:98;

theorem :: MEMSTR_0:32

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S holds dom p c= {(IC )} \/ (dom (DataPart p))

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S holds dom p c= {(IC )} \/ (dom (DataPart p))

proof end;

theorem Th33: :: MEMSTR_0:33

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s being State of S holds s = s | ((Data-Locations ) \/ {(IC )})

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s being State of S holds s = s | ((Data-Locations ) \/ {(IC )})

proof end;

theorem :: MEMSTR_0:34

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s1, s2 being State of S st s1 | ((Data-Locations ) \/ {(IC )}) = s2 | ((Data-Locations ) \/ {(IC )}) holds

s1 = s2

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s1, s2 being State of S st s1 | ((Data-Locations ) \/ {(IC )}) = s2 | ((Data-Locations ) \/ {(IC )}) holds

s1 = s2

proof end;

theorem :: MEMSTR_0:35

theorem Th36: :: MEMSTR_0:36

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for k, l being Nat holds (p +* (Start-At (k,S))) +* (Start-At (l,S)) = p +* (Start-At (l,S))

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for k, l being Nat holds (p +* (Start-At (k,S))) +* (Start-At (l,S)) = p +* (Start-At (l,S))

proof end;

theorem :: MEMSTR_0:37

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S st IC in dom p holds

p +* (Start-At ((IC p),S)) = p by FUNCT_4:7, FUNCT_4:98;

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S st IC in dom p holds

p +* (Start-At ((IC p),S)) = p by FUNCT_4:7, FUNCT_4:98;

theorem :: MEMSTR_0:38

for k being Nat

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s being State of S

for p being PartState of S st p +* (Start-At (k,S)) c= s holds

IC s = k

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s being State of S

for p being PartState of S st p +* (Start-At (k,S)) c= s holds

IC s = k

proof end;

theorem :: MEMSTR_0:39

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S st Start-At (0,S) c= p holds

IC p = 0

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S st Start-At (0,S) c= p holds

IC p = 0

proof end;

theorem :: MEMSTR_0:40

for k being Nat

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S st Start-At (k,S) c= p holds

IC p = k

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S st Start-At (k,S) c= p holds

IC p = k

proof end;

registration

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

not for b_{1} being PartState of S holds b_{1} is empty

end;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

cluster non empty Relation-like the carrier of S -defined Function-like the_Values_of S -compatible for set ;

existence not for b

proof end;

theorem :: MEMSTR_0:41

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being non empty PartState of S holds dom p meets {(IC )} \/ (Data-Locations )

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being non empty PartState of S holds dom p meets {(IC )} \/ (Data-Locations )

proof end;

definition

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let p be PartState of S;

coherence

p +* (Start-At (0,S)) is PartState of S ;

projectivity

for b_{1}, b_{2} being PartState of S st b_{1} = b_{2} +* (Start-At (0,S)) holds

b_{1} = b_{1} +* (Start-At (0,S))
;

end;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let p be PartState of S;

coherence

p +* (Start-At (0,S)) is PartState of S ;

projectivity

for b

b

:: deftheorem defines Initialize MEMSTR_0:def 13 :

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S holds Initialize p = p +* (Start-At (0,S));

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S holds Initialize p = p +* (Start-At (0,S));

registration

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let p be PartState of S;

coherence

Initialize p is 0 -started ;

end;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let p be PartState of S;

coherence

Initialize p is 0 -started ;

theorem Th42: :: MEMSTR_0:42

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S holds dom (Initialize p) = (dom p) \/ {(IC )}

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S holds dom (Initialize p) = (dom p) \/ {(IC )}

proof end;

theorem :: MEMSTR_0:43

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for x being set holds

( not x in dom (Initialize p) or x in dom p or x = IC )

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for x being set holds

( not x in dom (Initialize p) or x in dom p or x = IC )

proof end;

theorem :: MEMSTR_0:44

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being 0 -started PartState of S holds Initialize p = p

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being 0 -started PartState of S holds Initialize p = p

proof end;

theorem Th45: :: MEMSTR_0:45

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S holds DataPart (Initialize p) = DataPart p

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S holds DataPart (Initialize p) = DataPart p

proof end;

theorem :: MEMSTR_0:46

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s being State of S st IC s = 0 holds

Initialize s = s

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s being State of S st IC s = 0 holds

Initialize s = s

proof end;

registration

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let s be State of S;

coherence

Initialize s is total ;

end;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let s be State of S;

coherence

Initialize s is total ;

theorem Th47: :: MEMSTR_0:47

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s being State of S

for p being PartState of S st Initialize p c= s holds

IC s = 0

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s being State of S

for p being PartState of S st Initialize p c= s holds

IC s = 0

proof end;

theorem Th48: :: MEMSTR_0:48

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S holds IC in dom (Initialize p)

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S holds IC in dom (Initialize p)

proof end;

theorem :: MEMSTR_0:49

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p, q being PartState of S holds IC in dom (p +* (Initialize q))

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p, q being PartState of S holds IC in dom (p +* (Initialize q))

proof end;

theorem :: MEMSTR_0:50

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p, q being PartState of S st Initialize p c= q holds

Start-At (0,S) c= q

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p, q being PartState of S st Initialize p c= q holds

Start-At (0,S) c= q

proof end;

definition

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let p be PartState of S;

let k be Nat;

correctness

coherence

p +* (Start-At (((IC p) + k),S)) is PartState of S;

;

end;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let p be PartState of S;

let k be Nat;

correctness

coherence

p +* (Start-At (((IC p) + k),S)) is PartState of S;

;

:: deftheorem defines IncIC MEMSTR_0:def 14 :

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for k being Nat holds IncIC (p,k) = p +* (Start-At (((IC p) + k),S));

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for k being Nat holds IncIC (p,k) = p +* (Start-At (((IC p) + k),S));

theorem Th51: :: MEMSTR_0:51

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for k being Nat holds DataPart (IncIC (p,k)) = DataPart p

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for k being Nat holds DataPart (IncIC (p,k)) = DataPart p

proof end;

theorem Th52: :: MEMSTR_0:52

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for k being Nat holds IC in dom (IncIC (p,k))

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for k being Nat holds IC in dom (IncIC (p,k))

proof end;

theorem Th53: :: MEMSTR_0:53

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for k being Nat holds IC (IncIC (p,k)) = (IC p) + k

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for k being Nat holds IC (IncIC (p,k)) = (IC p) + k

proof end;

theorem :: MEMSTR_0:54

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for d being data-only PartState of S

for k being Nat holds IncIC ((p +* d),k) = (IncIC (p,k)) +* d

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for d being data-only PartState of S

for k being Nat holds IncIC ((p +* d),k) = (IncIC (p,k)) +* d

proof end;

theorem :: MEMSTR_0:55

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for k being Nat holds Start-At (((IC p) + k),S) c= IncIC (p,k)

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for k being Nat holds Start-At (((IC p) + k),S) c= IncIC (p,k)

proof end;

theorem :: MEMSTR_0:56

for k being Nat

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S st IC in dom p holds

IncIC (p,k) = (DataPart p) +* (Start-At (((IC p) + k),S))

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S st IC in dom p holds

IncIC (p,k) = (DataPart p) +* (Start-At (((IC p) + k),S))

proof end;

registration

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let s be State of S;

let k be Nat;

coherence

IncIC (s,k) is total ;

end;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let s be State of S;

let k be Nat;

coherence

IncIC (s,k) is total ;

theorem :: MEMSTR_0:57

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for i, j being Nat holds IncIC ((IncIC (p,i)),j) = IncIC (p,(i + j))

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for i, j being Nat holds IncIC ((IncIC (p,i)),j) = IncIC (p,(i + j))

proof end;

theorem :: MEMSTR_0:58

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for j, k being Nat holds IncIC ((p +* (Start-At (j,S))),k) = p +* (Start-At ((j + k),S))

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for j, k being Nat holds IncIC ((p +* (Start-At (j,S))),k) = p +* (Start-At ((j + k),S))

proof end;

theorem :: MEMSTR_0:59

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s being State of S

for k being Nat holds (IC (IncIC (s,k))) -' k = IC s

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s being State of S

for k being Nat holds (IC (IncIC (s,k))) -' k = IC s

proof end;

theorem :: MEMSTR_0:60

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p, q being PartState of S

for k being Nat st IC in dom q holds

IncIC ((p +* q),k) = p +* (IncIC (q,k))

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p, q being PartState of S

for k being Nat st IC in dom q holds

IncIC ((p +* q),k) = p +* (IncIC (q,k))

proof end;

theorem :: MEMSTR_0:61

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for k being Nat

for p being PartState of S

for s1, s2 being State of S st p c= s1 & IncIC (p,k) c= s2 holds

p c= s1 +* (DataPart s2)

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for k being Nat

for p being PartState of S

for s1, s2 being State of S st p c= s1 & IncIC (p,k) c= s2 holds

p c= s1 +* (DataPart s2)

proof end;

theorem :: MEMSTR_0:62

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for k being Nat holds DataPart p c= IncIC (p,k)

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for k being Nat holds DataPart p c= IncIC (p,k)

proof end;

definition

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let p be PartState of S;

let k be Nat;

correctness

coherence

p +* (Start-At (((IC p) -' k),S)) is PartState of S;

;

end;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let p be PartState of S;

let k be Nat;

correctness

coherence

p +* (Start-At (((IC p) -' k),S)) is PartState of S;

;

:: deftheorem defines DecIC MEMSTR_0:def 15 :

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for k being Nat holds DecIC (p,k) = p +* (Start-At (((IC p) -' k),S));

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for k being Nat holds DecIC (p,k) = p +* (Start-At (((IC p) -' k),S));

theorem :: MEMSTR_0:63

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for k being Nat holds DataPart (DecIC (p,k)) = DataPart p

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for k being Nat holds DataPart (DecIC (p,k)) = DataPart p

proof end;

theorem Th64: :: MEMSTR_0:64

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for k being Nat holds IC in dom (DecIC (p,k))

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for k being Nat holds IC in dom (DecIC (p,k))

proof end;

theorem Th65: :: MEMSTR_0:65

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for k being Nat holds IC (DecIC (p,k)) = (IC p) -' k

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for k being Nat holds IC (DecIC (p,k)) = (IC p) -' k

proof end;

theorem :: MEMSTR_0:66

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for d being data-only PartState of S

for k being Nat holds DecIC ((p +* d),k) = (DecIC (p,k)) +* d

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for d being data-only PartState of S

for k being Nat holds DecIC ((p +* d),k) = (DecIC (p,k)) +* d

proof end;

theorem :: MEMSTR_0:67

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for k being Nat holds Start-At (((IC p) -' k),S) c= DecIC (p,k)

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for k being Nat holds Start-At (((IC p) -' k),S) c= DecIC (p,k)

proof end;

theorem :: MEMSTR_0:68

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for k being Nat st IC in dom p holds

DecIC (p,k) = (DataPart p) +* (Start-At (((IC p) -' k),S))

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for k being Nat st IC in dom p holds

DecIC (p,k) = (DataPart p) +* (Start-At (((IC p) -' k),S))

proof end;

registration

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let s be State of S;

let k be Nat;

coherence

DecIC (s,k) is total ;

end;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let s be State of S;

let k be Nat;

coherence

DecIC (s,k) is total ;

theorem :: MEMSTR_0:69

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for i, j being Nat holds DecIC ((DecIC (p,i)),j) = DecIC (p,(i + j))

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for i, j being Nat holds DecIC ((DecIC (p,i)),j) = DecIC (p,(i + j))

proof end;

theorem :: MEMSTR_0:70

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for j, k being Nat holds DecIC ((p +* (Start-At (j,S))),k) = p +* (Start-At ((j -' k),S))

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for j, k being Nat holds DecIC ((p +* (Start-At (j,S))),k) = p +* (Start-At ((j -' k),S))

proof end;

theorem :: MEMSTR_0:71

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s being State of S

for k being Nat st k <= IC s holds

(IC (DecIC (s,k))) + k = IC s

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s being State of S

for k being Nat st k <= IC s holds

(IC (DecIC (s,k))) + k = IC s

proof end;

theorem Th72: :: MEMSTR_0:72

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p, q being PartState of S

for k being Nat st IC in dom q holds

DecIC ((p +* q),k) = p +* (DecIC (q,k))

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p, q being PartState of S

for k being Nat st IC in dom q holds

DecIC ((p +* q),k) = p +* (DecIC (q,k))

proof end;

theorem Th73: :: MEMSTR_0:73

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for k being Nat st IC in dom p holds

DecIC ((IncIC (p,k)),k) = p

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p being PartState of S

for k being Nat st IC in dom p holds

DecIC ((IncIC (p,k)),k) = p

proof end;

theorem :: MEMSTR_0:74

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p, q being PartState of S

for k being Nat st IC in dom q holds

DecIC ((p +* (IncIC (q,k))),k) = p +* q

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for p, q being PartState of S

for k being Nat st IC in dom q holds

DecIC ((p +* (IncIC (q,k))),k) = p +* q

proof end;

registration

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let k be Nat;

let p be k -started PartState of S;

coherence

DecIC (p,k) is 0 -started

end;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let k be Nat;

let p be k -started PartState of S;

coherence

DecIC (p,k) is 0 -started

proof end;

registration

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let l be Nat;

correctness

coherence

Start-At (l,S) is finite ;

;

end;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let l be Nat;

correctness

coherence

Start-At (l,S) is finite ;

;

definition
end;

registration

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let l be Nat;

ex b_{1} being FinPartState of S st b_{1} is l -started

end;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let l be Nat;

cluster Relation-like the carrier of S -defined Function-like the_Values_of S -compatible finite countable l -started for set ;

existence ex b

proof end;

registration

let N be with_zero set ;

let S be Mem-Struct over N;

let p be FinPartState of S;

coherence

DataPart p is finite ;

end;
let S be Mem-Struct over N;

let p be FinPartState of S;

coherence

DataPart p is finite ;

registration

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let p be FinPartState of S;

coherence

Initialize p is finite ;

end;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let p be FinPartState of S;

coherence

Initialize p is finite ;

registration

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let p be FinPartState of S;

let k be Nat;

coherence

IncIC (p,k) is finite ;

end;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let p be FinPartState of S;

let k be Nat;

coherence

IncIC (p,k) is finite ;

registration

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let p be FinPartState of S;

let k be Nat;

coherence

DecIC (p,k) is finite ;

end;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let p be FinPartState of S;

let k be Nat;

coherence

DecIC (p,k) is finite ;

definition

let N be with_zero set ;

let S be with_non-empty_values Mem-Struct over N;

{ p where p is Element of sproduct (the_Values_of S) : p is finite } is Subset of (sproduct (the_Values_of S))

end;
let S be with_non-empty_values Mem-Struct over N;

func FinPartSt S -> Subset of (sproduct (the_Values_of S)) equals :: MEMSTR_0:def 16

{ p where p is Element of sproduct (the_Values_of S) : p is finite } ;

coherence { p where p is Element of sproduct (the_Values_of S) : p is finite } ;

{ p where p is Element of sproduct (the_Values_of S) : p is finite } is Subset of (sproduct (the_Values_of S))

proof end;

:: deftheorem defines FinPartSt MEMSTR_0:def 16 :

for N being with_zero set

for S being with_non-empty_values Mem-Struct over N holds FinPartSt S = { p where p is Element of sproduct (the_Values_of S) : p is finite } ;

for N being with_zero set

for S being with_non-empty_values Mem-Struct over N holds FinPartSt S = { p where p is Element of sproduct (the_Values_of S) : p is finite } ;

theorem Th75: :: MEMSTR_0:75

for N being with_zero set

for S being with_non-empty_values Mem-Struct over N

for p being FinPartState of S holds p in FinPartSt S

for S being with_non-empty_values Mem-Struct over N

for p being FinPartState of S holds p in FinPartSt S

proof end;

registration

let N be with_zero set ;

let S be with_non-empty_values Mem-Struct over N;

coherence

not FinPartSt S is empty by Th75;

end;
let S be with_non-empty_values Mem-Struct over N;

coherence

not FinPartSt S is empty by Th75;

theorem :: MEMSTR_0:76

for N being with_zero set

for S being with_non-empty_values Mem-Struct over N

for p being Element of FinPartSt S holds p is FinPartState of S

for S being with_non-empty_values Mem-Struct over N

for p being Element of FinPartSt S holds p is FinPartState of S

proof end;

definition

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let IT be PartFunc of (FinPartSt S),(FinPartSt S);

end;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let IT be PartFunc of (FinPartSt S),(FinPartSt S);

:: deftheorem defines data-only MEMSTR_0:def 17 :

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for IT being PartFunc of (FinPartSt S),(FinPartSt S) holds

( IT is data-only iff for p being PartState of S st p in dom IT holds

( p is data-only & ( for q being PartState of S st q = IT . p holds

q is data-only ) ) );

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for IT being PartFunc of (FinPartSt S),(FinPartSt S) holds

( IT is data-only iff for p being PartState of S st p in dom IT holds

( p is data-only & ( for q being PartState of S st q = IT . p holds

q is data-only ) ) );

registration

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

ex b_{1} being PartFunc of (FinPartSt S),(FinPartSt S) st b_{1} is data-only

end;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

cluster Relation-like FinPartSt S -defined FinPartSt S -valued Function-like Function-yielding V38() data-only for Element of K10(K11((FinPartSt S),(FinPartSt S)));

existence ex b

proof end;

theorem :: MEMSTR_0:77

for N being with_zero set

for A being non empty with_non-empty_values Mem-Struct over N

for s being State of A

for o being Object of A holds s . o in Values o

for A being non empty with_non-empty_values Mem-Struct over N

for s being State of A

for o being Object of A holds s . o in Values o

proof end;

theorem Th78: :: MEMSTR_0:78

for N being with_zero set

for A being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s1, s2 being State of A st IC s1 = IC s2 & DataPart s1 = DataPart s2 holds

s1 = s2

for A being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s1, s2 being State of A st IC s1 = IC s2 & DataPart s1 = DataPart s2 holds

s1 = s2

proof end;

theorem :: MEMSTR_0:79

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s being State of S

for l being Nat holds DataPart s = DataPart (s +* (Start-At (l,S)))

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s being State of S

for l being Nat holds DataPart s = DataPart (s +* (Start-At (l,S)))

proof end;

theorem :: MEMSTR_0:80

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s1, s2 being State of S st DataPart s1 = DataPart s2 holds

Initialize s1 = Initialize s2

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for s1, s2 being State of S st DataPart s1 = DataPart s2 holds

Initialize s1 = Initialize s2

proof end;

theorem :: MEMSTR_0:81

::from SCMFSA9A

definition

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let f be Function of (product (the_Values_of S)),NAT;

end;
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N;

let f be Function of (product (the_Values_of S)),NAT;

attr f is on_data_only means :: MEMSTR_0:def 18

for s1, s2 being State of S st DataPart s1 = DataPart s2 holds

f . s1 = f . s2;

for s1, s2 being State of S st DataPart s1 = DataPart s2 holds

f . s1 = f . s2;

:: deftheorem defines on_data_only MEMSTR_0:def 18 :

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for f being Function of (product (the_Values_of S)),NAT holds

( f is on_data_only iff for s1, s2 being State of S st DataPart s1 = DataPart s2 holds

f . s1 = f . s2 );

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N

for f being Function of (product (the_Values_of S)),NAT holds

( f is on_data_only iff for s1, s2 being State of S st DataPart s1 = DataPart s2 holds

f . s1 = f . s2 );

:: na razie wykorzystujemy tylko rejestracje, ze 'with_zero'

:: musi byc 'non empty' i w definicji Trivial-Mem N

:: ale tutaj mozna sie tego pozbyc, biorac zamiast 0

:: the Element of N i potrzebujemy tylko to, ze N jest niepusty