:: by Andrzej Trybulec , Yatsuka Nakamura and Piotr Rudnicki

::

:: Received February 3, 1996

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

:: deftheorem defines SCM+FSA-Memory SCMFSA_1:def 2 :

SCM+FSA-Memory = SCM-Memory \/ SCM+FSA-Data*-Loc;

SCM+FSA-Memory = SCM-Memory \/ SCM+FSA-Data*-Loc;

definition

:: original: SCM+FSA-Data-Loc

redefine func SCM+FSA-Data-Loc -> Subset of SCM+FSA-Memory;

coherence

SCM+FSA-Data-Loc is Subset of SCM+FSA-Memory

end;
redefine func SCM+FSA-Data-Loc -> Subset of SCM+FSA-Memory;

coherence

SCM+FSA-Data-Loc is Subset of SCM+FSA-Memory

proof end;

definition

:: original: SCM+FSA-Data*-Loc

redefine func SCM+FSA-Data*-Loc -> Subset of SCM+FSA-Memory;

coherence

SCM+FSA-Data*-Loc is Subset of SCM+FSA-Memory by XBOOLE_1:7;

end;
redefine func SCM+FSA-Data*-Loc -> Subset of SCM+FSA-Memory;

coherence

SCM+FSA-Data*-Loc is Subset of SCM+FSA-Memory by XBOOLE_1:7;

registration
end;

definition

(SCM+FSA-Memory --> 2) +* SCM-OK is Function of SCM+FSA-Memory,(Segm 3)
end;

::$CD

func SCM+FSA-OK -> Function of SCM+FSA-Memory,(Segm 3) equals :: SCMFSA_1:def 4

(SCM+FSA-Memory --> 2) +* SCM-OK;

coherence (SCM+FSA-Memory --> 2) +* SCM-OK;

(SCM+FSA-Memory --> 2) +* SCM-OK is Function of SCM+FSA-Memory,(Segm 3)

proof end;

::$CT 3

::$CT 2

Lm1: SCM+FSA-Data*-Loc misses SCM-Memory

proof end;

Lm2: dom SCM-OK c= dom SCM+FSA-OK

proof end;

Lm3: NAT in dom SCM+FSA-OK

proof end;

Lm4: SCM+FSA-OK . NAT = 0

proof end;

Lm5: for b being Element of SCM+FSA-Data-Loc holds SCM+FSA-OK . b = 1

proof end;

Lm6: for f being Element of SCM+FSA-Data*-Loc holds SCM+FSA-OK . f = 2

proof end;

Lm7: dom SCM+FSA-OK = SCM+FSA-Memory

by PARTFUN1:def 2;

len <%NAT,INT,(INT *)%> = 3

by AFINSQ_1:39;

then rng SCM+FSA-OK c= dom SCM*-VAL

by RELAT_1:def 19;

then Lm8: dom (SCM*-VAL * SCM+FSA-OK) = SCM+FSA-Memory

by Lm7, RELAT_1:27;

::$CT 5

definition
end;

:: deftheorem defines SCM+FSA-Chg SCMFSA_1:def 6 :

for s being SCM+FSA-State

for u being Nat holds SCM+FSA-Chg (s,u) = s +* (NAT .--> u);

for s being SCM+FSA-State

for u being Nat holds SCM+FSA-Chg (s,u) = s +* (NAT .--> u);

definition

let s be SCM+FSA-State;

let t be Element of SCM+FSA-Data-Loc ;

let u be Integer;

coherence

s +* (t .--> u) is SCM+FSA-State

end;
let t be Element of SCM+FSA-Data-Loc ;

let u be Integer;

coherence

s +* (t .--> u) is SCM+FSA-State

proof end;

:: deftheorem defines SCM+FSA-Chg SCMFSA_1:def 7 :

for s being SCM+FSA-State

for t being Element of SCM+FSA-Data-Loc

for u being Integer holds SCM+FSA-Chg (s,t,u) = s +* (t .--> u);

for s being SCM+FSA-State

for t being Element of SCM+FSA-Data-Loc

for u being Integer holds SCM+FSA-Chg (s,t,u) = s +* (t .--> u);

definition

let s be SCM+FSA-State;

let t be Element of SCM+FSA-Data*-Loc ;

let u be FinSequence of INT ;

coherence

s +* (t .--> u) is SCM+FSA-State

end;
let t be Element of SCM+FSA-Data*-Loc ;

let u be FinSequence of INT ;

coherence

s +* (t .--> u) is SCM+FSA-State

proof end;

:: deftheorem defines SCM+FSA-Chg SCMFSA_1:def 8 :

for s being SCM+FSA-State

for t being Element of SCM+FSA-Data*-Loc

for u being FinSequence of INT holds SCM+FSA-Chg (s,t,u) = s +* (t .--> u);

for s being SCM+FSA-State

for t being Element of SCM+FSA-Data*-Loc

for u being FinSequence of INT holds SCM+FSA-Chg (s,t,u) = s +* (t .--> u);

registration
end;

definition

let s be SCM+FSA-State;

let a be Element of SCM+FSA-Data*-Loc ;

:: original: .

redefine func s . a -> FinSequence of INT ;

coherence

s . a is FinSequence of INT

end;
let a be Element of SCM+FSA-Data*-Loc ;

:: original: .

redefine func s . a -> FinSequence of INT ;

coherence

s . a is FinSequence of INT

proof end;

definition

let x be Element of SCM+FSA-Instr ;

let s be SCM+FSA-State;

( ( x `1_3 <= 8 implies ex b_{1} being SCM+FSA-State ex x9 being Element of SCM-Instr ex s9 being SCM-State st

( x = x9 & s9 = s | SCM-Memory & b_{1} = s +* (SCM-Exec-Res (x9,s9)) ) ) & ( x `1_3 = 9 implies ex b_{1} being SCM+FSA-State ex i being Integer ex k being Nat st

( k = |.(s . (x int_addr2)).| & i = (s . (x coll_addr1)) /. k & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr1),i)),((IC s) + 1)) ) ) & ( x `1_3 = 10 implies ex b_{1} being SCM+FSA-State ex f being FinSequence of INT ex k being Nat st

( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),((IC s) + 1)) ) ) & ( x `1_3 = 11 implies ex b_{1} being SCM+FSA-State st b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr3),(len (s . (x coll_addr2))))),((IC s) + 1)) ) & ( x `1_3 = 12 implies ex b_{1} being SCM+FSA-State ex f being FinSequence of INT ex k being Nat st

( k = |.(s . (x int_addr3)).| & f = k |-> 0 & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr2),f)),((IC s) + 1)) ) ) & ( x `1_3 = 13 implies ex b_{1} being SCM+FSA-State ex i being Integer st

( i = 1 & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),((IC s) + 1)) ) ) & ( not x `1_3 <= 8 & not x `1_3 = 9 & not x `1_3 = 10 & not x `1_3 = 11 & not x `1_3 = 12 & not x `1_3 = 13 implies ex b_{1} being SCM+FSA-State st b_{1} = s ) )

for b_{1}, b_{2} being SCM+FSA-State holds

( ( x `1_3 <= 8 & ex x9 being Element of SCM-Instr ex s9 being SCM-State st

( x = x9 & s9 = s | SCM-Memory & b_{1} = s +* (SCM-Exec-Res (x9,s9)) ) & ex x9 being Element of SCM-Instr ex s9 being SCM-State st

( x = x9 & s9 = s | SCM-Memory & b_{2} = s +* (SCM-Exec-Res (x9,s9)) ) implies b_{1} = b_{2} ) & ( x `1_3 = 9 & ex i being Integer ex k being Nat st

( k = |.(s . (x int_addr2)).| & i = (s . (x coll_addr1)) /. k & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr1),i)),((IC s) + 1)) ) & ex i being Integer ex k being Nat st

( k = |.(s . (x int_addr2)).| & i = (s . (x coll_addr1)) /. k & b_{2} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr1),i)),((IC s) + 1)) ) implies b_{1} = b_{2} ) & ( x `1_3 = 10 & ex f being FinSequence of INT ex k being Nat st

( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),((IC s) + 1)) ) & ex f being FinSequence of INT ex k being Nat st

( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & b_{2} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),((IC s) + 1)) ) implies b_{1} = b_{2} ) & ( x `1_3 = 11 & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr3),(len (s . (x coll_addr2))))),((IC s) + 1)) & b_{2} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr3),(len (s . (x coll_addr2))))),((IC s) + 1)) implies b_{1} = b_{2} ) & ( x `1_3 = 12 & ex f being FinSequence of INT ex k being Nat st

( k = |.(s . (x int_addr3)).| & f = k |-> 0 & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr2),f)),((IC s) + 1)) ) & ex f being FinSequence of INT ex k being Nat st

( k = |.(s . (x int_addr3)).| & f = k |-> 0 & b_{2} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr2),f)),((IC s) + 1)) ) implies b_{1} = b_{2} ) & ( x `1_3 = 13 & ex i being Integer st

( i = 1 & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),((IC s) + 1)) ) & ex i being Integer st

( i = 1 & b_{2} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),((IC s) + 1)) ) implies b_{1} = b_{2} ) & ( not x `1_3 <= 8 & not x `1_3 = 9 & not x `1_3 = 10 & not x `1_3 = 11 & not x `1_3 = 12 & not x `1_3 = 13 & b_{1} = s & b_{2} = s implies b_{1} = b_{2} ) )
;

consistency

for b_{1} being SCM+FSA-State holds

( ( x `1_3 <= 8 & x `1_3 = 9 implies ( ex x9 being Element of SCM-Instr ex s9 being SCM-State st

( x = x9 & s9 = s | SCM-Memory & b_{1} = s +* (SCM-Exec-Res (x9,s9)) ) iff ex i being Integer ex k being Nat st

( k = |.(s . (x int_addr2)).| & i = (s . (x coll_addr1)) /. k & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr1),i)),((IC s) + 1)) ) ) ) & ( x `1_3 <= 8 & x `1_3 = 10 implies ( ex x9 being Element of SCM-Instr ex s9 being SCM-State st

( x = x9 & s9 = s | SCM-Memory & b_{1} = s +* (SCM-Exec-Res (x9,s9)) ) iff ex f being FinSequence of INT ex k being Nat st

( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),((IC s) + 1)) ) ) ) & ( x `1_3 <= 8 & x `1_3 = 11 implies ( ex x9 being Element of SCM-Instr ex s9 being SCM-State st

( x = x9 & s9 = s | SCM-Memory & b_{1} = s +* (SCM-Exec-Res (x9,s9)) ) iff b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr3),(len (s . (x coll_addr2))))),((IC s) + 1)) ) ) & ( x `1_3 <= 8 & x `1_3 = 12 implies ( ex x9 being Element of SCM-Instr ex s9 being SCM-State st

( x = x9 & s9 = s | SCM-Memory & b_{1} = s +* (SCM-Exec-Res (x9,s9)) ) iff ex f being FinSequence of INT ex k being Nat st

( k = |.(s . (x int_addr3)).| & f = k |-> 0 & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr2),f)),((IC s) + 1)) ) ) ) & ( x `1_3 <= 8 & x `1_3 = 13 implies ( ex x9 being Element of SCM-Instr ex s9 being SCM-State st

( x = x9 & s9 = s | SCM-Memory & b_{1} = s +* (SCM-Exec-Res (x9,s9)) ) iff ex i being Integer st

( i = 1 & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),((IC s) + 1)) ) ) ) & ( x `1_3 = 9 & x `1_3 = 10 implies ( ex i being Integer ex k being Nat st

( k = |.(s . (x int_addr2)).| & i = (s . (x coll_addr1)) /. k & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr1),i)),((IC s) + 1)) ) iff ex f being FinSequence of INT ex k being Nat st

( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),((IC s) + 1)) ) ) ) & ( x `1_3 = 9 & x `1_3 = 11 implies ( ex i being Integer ex k being Nat st

( k = |.(s . (x int_addr2)).| & i = (s . (x coll_addr1)) /. k & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr1),i)),((IC s) + 1)) ) iff b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr3),(len (s . (x coll_addr2))))),((IC s) + 1)) ) ) & ( x `1_3 = 9 & x `1_3 = 12 implies ( ex i being Integer ex k being Nat st

( k = |.(s . (x int_addr2)).| & i = (s . (x coll_addr1)) /. k & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr1),i)),((IC s) + 1)) ) iff ex f being FinSequence of INT ex k being Nat st

( k = |.(s . (x int_addr3)).| & f = k |-> 0 & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr2),f)),((IC s) + 1)) ) ) ) & ( x `1_3 = 9 & x `1_3 = 13 implies ( ex i being Integer ex k being Nat st

( k = |.(s . (x int_addr2)).| & i = (s . (x coll_addr1)) /. k & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr1),i)),((IC s) + 1)) ) iff ex i being Integer st

( i = 1 & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),((IC s) + 1)) ) ) ) & ( x `1_3 = 10 & x `1_3 = 11 implies ( ex f being FinSequence of INT ex k being Nat st

( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),((IC s) + 1)) ) iff b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr3),(len (s . (x coll_addr2))))),((IC s) + 1)) ) ) & ( x `1_3 = 10 & x `1_3 = 12 implies ( ex f being FinSequence of INT ex k being Nat st

( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),((IC s) + 1)) ) iff ex f being FinSequence of INT ex k being Nat st

( k = |.(s . (x int_addr3)).| & f = k |-> 0 & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr2),f)),((IC s) + 1)) ) ) ) & ( x `1_3 = 10 & x `1_3 = 13 implies ( ex f being FinSequence of INT ex k being Nat st

( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),((IC s) + 1)) ) iff ex i being Integer st

( i = 1 & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),((IC s) + 1)) ) ) ) & ( x `1_3 = 11 & x `1_3 = 12 implies ( b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr3),(len (s . (x coll_addr2))))),((IC s) + 1)) iff ex f being FinSequence of INT ex k being Nat st

( k = |.(s . (x int_addr3)).| & f = k |-> 0 & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr2),f)),((IC s) + 1)) ) ) ) & ( x `1_3 = 11 & x `1_3 = 13 implies ( b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr3),(len (s . (x coll_addr2))))),((IC s) + 1)) iff ex i being Integer st

( i = 1 & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),((IC s) + 1)) ) ) ) & ( x `1_3 = 12 & x `1_3 = 13 implies ( ex f being FinSequence of INT ex k being Nat st

( k = |.(s . (x int_addr3)).| & f = k |-> 0 & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr2),f)),((IC s) + 1)) ) iff ex i being Integer st

( i = 1 & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),((IC s) + 1)) ) ) ) )
;

end;
let s be SCM+FSA-State;

func SCM+FSA-Exec-Res (x,s) -> SCM+FSA-State means :: SCMFSA_1:def 16

ex x9 being Element of SCM-Instr ex s9 being SCM-State st

( x = x9 & s9 = s | SCM-Memory & it = s +* (SCM-Exec-Res (x9,s9)) ) if x `1_3 <= 8

ex i being Integer ex k being Nat st

( k = |.(s . (x int_addr2)).| & i = (s . (x coll_addr1)) /. k & it = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr1),i)),((IC s) + 1)) ) if x `1_3 = 9

ex f being FinSequence of INT ex k being Nat st

( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & it = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),((IC s) + 1)) ) if x `1_3 = 10

it = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr3),(len (s . (x coll_addr2))))),((IC s) + 1)) if x `1_3 = 11

ex f being FinSequence of INT ex k being Nat st

( k = |.(s . (x int_addr3)).| & f = k |-> 0 & it = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr2),f)),((IC s) + 1)) ) if x `1_3 = 12

ex i being Integer st

( i = 1 & it = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),((IC s) + 1)) ) if x `1_3 = 13

otherwise it = s;

existence ex x9 being Element of SCM-Instr ex s9 being SCM-State st

( x = x9 & s9 = s | SCM-Memory & it = s +* (SCM-Exec-Res (x9,s9)) ) if x `1_3 <= 8

ex i being Integer ex k being Nat st

( k = |.(s . (x int_addr2)).| & i = (s . (x coll_addr1)) /. k & it = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr1),i)),((IC s) + 1)) ) if x `1_3 = 9

ex f being FinSequence of INT ex k being Nat st

( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & it = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),((IC s) + 1)) ) if x `1_3 = 10

it = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr3),(len (s . (x coll_addr2))))),((IC s) + 1)) if x `1_3 = 11

ex f being FinSequence of INT ex k being Nat st

( k = |.(s . (x int_addr3)).| & f = k |-> 0 & it = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr2),f)),((IC s) + 1)) ) if x `1_3 = 12

ex i being Integer st

( i = 1 & it = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),((IC s) + 1)) ) if x `1_3 = 13

otherwise it = s;

( ( x `1_3 <= 8 implies ex b

( x = x9 & s9 = s | SCM-Memory & b

( k = |.(s . (x int_addr2)).| & i = (s . (x coll_addr1)) /. k & b

( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & b

( k = |.(s . (x int_addr3)).| & f = k |-> 0 & b

( i = 1 & b

proof end;

uniqueness for b

( ( x `1_3 <= 8 & ex x9 being Element of SCM-Instr ex s9 being SCM-State st

( x = x9 & s9 = s | SCM-Memory & b

( x = x9 & s9 = s | SCM-Memory & b

( k = |.(s . (x int_addr2)).| & i = (s . (x coll_addr1)) /. k & b

( k = |.(s . (x int_addr2)).| & i = (s . (x coll_addr1)) /. k & b

( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & b

( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & b

( k = |.(s . (x int_addr3)).| & f = k |-> 0 & b

( k = |.(s . (x int_addr3)).| & f = k |-> 0 & b

( i = 1 & b

( i = 1 & b

consistency

for b

( ( x `1_3 <= 8 & x `1_3 = 9 implies ( ex x9 being Element of SCM-Instr ex s9 being SCM-State st

( x = x9 & s9 = s | SCM-Memory & b

( k = |.(s . (x int_addr2)).| & i = (s . (x coll_addr1)) /. k & b

( x = x9 & s9 = s | SCM-Memory & b

( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & b

( x = x9 & s9 = s | SCM-Memory & b

( x = x9 & s9 = s | SCM-Memory & b

( k = |.(s . (x int_addr3)).| & f = k |-> 0 & b

( x = x9 & s9 = s | SCM-Memory & b

( i = 1 & b

( k = |.(s . (x int_addr2)).| & i = (s . (x coll_addr1)) /. k & b

( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & b

( k = |.(s . (x int_addr2)).| & i = (s . (x coll_addr1)) /. k & b

( k = |.(s . (x int_addr2)).| & i = (s . (x coll_addr1)) /. k & b

( k = |.(s . (x int_addr3)).| & f = k |-> 0 & b

( k = |.(s . (x int_addr2)).| & i = (s . (x coll_addr1)) /. k & b

( i = 1 & b

( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & b

( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & b

( k = |.(s . (x int_addr3)).| & f = k |-> 0 & b

( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & b

( i = 1 & b

( k = |.(s . (x int_addr3)).| & f = k |-> 0 & b

( i = 1 & b

( k = |.(s . (x int_addr3)).| & f = k |-> 0 & b

( i = 1 & b

:: deftheorem defines SCM+FSA-Exec-Res SCMFSA_1:def 16 :

for x being Element of SCM+FSA-Instr

for s, b_{3} being SCM+FSA-State holds

( ( x `1_3 <= 8 implies ( b_{3} = SCM+FSA-Exec-Res (x,s) iff ex x9 being Element of SCM-Instr ex s9 being SCM-State st

( x = x9 & s9 = s | SCM-Memory & b_{3} = s +* (SCM-Exec-Res (x9,s9)) ) ) ) & ( x `1_3 = 9 implies ( b_{3} = SCM+FSA-Exec-Res (x,s) iff ex i being Integer ex k being Nat st

( k = |.(s . (x int_addr2)).| & i = (s . (x coll_addr1)) /. k & b_{3} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr1),i)),((IC s) + 1)) ) ) ) & ( x `1_3 = 10 implies ( b_{3} = SCM+FSA-Exec-Res (x,s) iff ex f being FinSequence of INT ex k being Nat st

( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & b_{3} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),((IC s) + 1)) ) ) ) & ( x `1_3 = 11 implies ( b_{3} = SCM+FSA-Exec-Res (x,s) iff b_{3} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr3),(len (s . (x coll_addr2))))),((IC s) + 1)) ) ) & ( x `1_3 = 12 implies ( b_{3} = SCM+FSA-Exec-Res (x,s) iff ex f being FinSequence of INT ex k being Nat st

( k = |.(s . (x int_addr3)).| & f = k |-> 0 & b_{3} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr2),f)),((IC s) + 1)) ) ) ) & ( x `1_3 = 13 implies ( b_{3} = SCM+FSA-Exec-Res (x,s) iff ex i being Integer st

( i = 1 & b_{3} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),((IC s) + 1)) ) ) ) & ( not x `1_3 <= 8 & not x `1_3 = 9 & not x `1_3 = 10 & not x `1_3 = 11 & not x `1_3 = 12 & not x `1_3 = 13 implies ( b_{3} = SCM+FSA-Exec-Res (x,s) iff b_{3} = s ) ) );

for x being Element of SCM+FSA-Instr

for s, b

( ( x `1_3 <= 8 implies ( b

( x = x9 & s9 = s | SCM-Memory & b

( k = |.(s . (x int_addr2)).| & i = (s . (x coll_addr1)) /. k & b

( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & b

( k = |.(s . (x int_addr3)).| & f = k |-> 0 & b

( i = 1 & b

definition

ex b_{1} being Action of SCM+FSA-Instr,(product (SCM*-VAL * SCM+FSA-OK)) st

for x being Element of SCM+FSA-Instr

for y being SCM+FSA-State holds (b_{1} . x) . y = SCM+FSA-Exec-Res (x,y)

for b_{1}, b_{2} being Action of SCM+FSA-Instr,(product (SCM*-VAL * SCM+FSA-OK)) st ( for x being Element of SCM+FSA-Instr

for y being SCM+FSA-State holds (b_{1} . x) . y = SCM+FSA-Exec-Res (x,y) ) & ( for x being Element of SCM+FSA-Instr

for y being SCM+FSA-State holds (b_{2} . x) . y = SCM+FSA-Exec-Res (x,y) ) holds

b_{1} = b_{2}
end;

func SCM+FSA-Exec -> Action of SCM+FSA-Instr,(product (SCM*-VAL * SCM+FSA-OK)) means :: SCMFSA_1:def 17

for x being Element of SCM+FSA-Instr

for y being SCM+FSA-State holds (it . x) . y = SCM+FSA-Exec-Res (x,y);

existence for x being Element of SCM+FSA-Instr

for y being SCM+FSA-State holds (it . x) . y = SCM+FSA-Exec-Res (x,y);

ex b

for x being Element of SCM+FSA-Instr

for y being SCM+FSA-State holds (b

proof end;

uniqueness for b

for y being SCM+FSA-State holds (b

for y being SCM+FSA-State holds (b

b

proof end;

:: deftheorem defines SCM+FSA-Exec SCMFSA_1:def 17 :

for b_{1} being Action of SCM+FSA-Instr,(product (SCM*-VAL * SCM+FSA-OK)) holds

( b_{1} = SCM+FSA-Exec iff for x being Element of SCM+FSA-Instr

for y being SCM+FSA-State holds (b_{1} . x) . y = SCM+FSA-Exec-Res (x,y) );

for b

( b

for y being SCM+FSA-State holds (b

theorem :: SCMFSA_1:20

for s being SCM+FSA-State

for u being Nat

for mk being Element of SCM+FSA-Data-Loc holds (SCM+FSA-Chg (s,u)) . mk = s . mk

for u being Nat

for mk being Element of SCM+FSA-Data-Loc holds (SCM+FSA-Chg (s,u)) . mk = s . mk

proof end;

theorem :: SCMFSA_1:21

for s being SCM+FSA-State

for u being Nat

for p being Element of SCM+FSA-Data*-Loc holds (SCM+FSA-Chg (s,u)) . p = s . p

for u being Nat

for p being Element of SCM+FSA-Data*-Loc holds (SCM+FSA-Chg (s,u)) . p = s . p

proof end;

theorem :: SCMFSA_1:23

for s being SCM+FSA-State

for t being Element of SCM+FSA-Data-Loc

for u being Integer holds (SCM+FSA-Chg (s,t,u)) . NAT = s . NAT

for t being Element of SCM+FSA-Data-Loc

for u being Integer holds (SCM+FSA-Chg (s,t,u)) . NAT = s . NAT

proof end;

theorem :: SCMFSA_1:24

for s being SCM+FSA-State

for t being Element of SCM+FSA-Data-Loc

for u being Integer holds (SCM+FSA-Chg (s,t,u)) . t = u

for t being Element of SCM+FSA-Data-Loc

for u being Integer holds (SCM+FSA-Chg (s,t,u)) . t = u

proof end;

theorem :: SCMFSA_1:25

for s being SCM+FSA-State

for t being Element of SCM+FSA-Data-Loc

for u being Integer

for mk being Element of SCM+FSA-Data-Loc st mk <> t holds

(SCM+FSA-Chg (s,t,u)) . mk = s . mk

for t being Element of SCM+FSA-Data-Loc

for u being Integer

for mk being Element of SCM+FSA-Data-Loc st mk <> t holds

(SCM+FSA-Chg (s,t,u)) . mk = s . mk

proof end;

theorem :: SCMFSA_1:26

for s being SCM+FSA-State

for t being Element of SCM+FSA-Data-Loc

for u being Integer

for f being Element of SCM+FSA-Data*-Loc holds (SCM+FSA-Chg (s,t,u)) . f = s . f

for t being Element of SCM+FSA-Data-Loc

for u being Integer

for f being Element of SCM+FSA-Data*-Loc holds (SCM+FSA-Chg (s,t,u)) . f = s . f

proof end;

theorem :: SCMFSA_1:27

for s being SCM+FSA-State

for t being Element of SCM+FSA-Data*-Loc

for u being FinSequence of INT holds (SCM+FSA-Chg (s,t,u)) . t = u

for t being Element of SCM+FSA-Data*-Loc

for u being FinSequence of INT holds (SCM+FSA-Chg (s,t,u)) . t = u

proof end;

theorem :: SCMFSA_1:28

for s being SCM+FSA-State

for t being Element of SCM+FSA-Data*-Loc

for u being FinSequence of INT

for mk being Element of SCM+FSA-Data*-Loc st mk <> t holds

(SCM+FSA-Chg (s,t,u)) . mk = s . mk

for t being Element of SCM+FSA-Data*-Loc

for u being FinSequence of INT

for mk being Element of SCM+FSA-Data*-Loc st mk <> t holds

(SCM+FSA-Chg (s,t,u)) . mk = s . mk

proof end;

theorem :: SCMFSA_1:29

for s being SCM+FSA-State

for t being Element of SCM+FSA-Data*-Loc

for u being FinSequence of INT

for a being Element of SCM+FSA-Data-Loc holds (SCM+FSA-Chg (s,t,u)) . a = s . a

for t being Element of SCM+FSA-Data*-Loc

for u being FinSequence of INT

for a being Element of SCM+FSA-Data-Loc holds (SCM+FSA-Chg (s,t,u)) . a = s . a

proof end;

::$CT