:: An Extension of { \bf SCM }
:: by Andrzej Trybulec , Yatsuka Nakamura and Piotr Rudnicki
::
:: Received February 3, 1996
:: Copyright (c) 1996 Association of Mizar Users


notation
synonym SCM+FSA-Data-Loc for SCM-Data-Loc ;
end;

definition
func SCM+FSA-Data*-Loc -> set equals :: SCMFSA_1:def 1
INT \ NAT ;
coherence
INT \ NAT is set ;
end;

:: deftheorem defines SCM+FSA-Data*-Loc SCMFSA_1:def 1 :
SCM+FSA-Data*-Loc = INT \ NAT ;

definition
func SCM+FSA-Memory -> set equals :: SCMFSA_1:def 2
SCM-Memory \/ SCM+FSA-Data*-Loc ;
coherence
SCM-Memory \/ SCM+FSA-Data*-Loc is set ;
end;

:: deftheorem defines SCM+FSA-Memory SCMFSA_1:def 2 :
SCM+FSA-Memory = SCM-Memory \/ SCM+FSA-Data*-Loc ;

registration
cluster SCM+FSA-Memory -> non empty ;
coherence
not SCM+FSA-Memory is empty ;
end;

theorem Th1: :: SCMFSA_1:1
SCM-Memory c= SCM+FSA-Memory by XBOOLE_1:7;

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
proof end;
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;
canceled;
end;

:: deftheorem SCMFSA_1:def 3 :
canceled;

definition
:: original: omega
redefine func NAT -> Subset of SCM+FSA-Memory ;
coherence
omega is Subset of SCM+FSA-Memory by Th1, XBOOLE_1:1;
end;

registration
cluster SCM+FSA-Data*-Loc -> non empty ;
coherence
not SCM+FSA-Data*-Loc is empty
proof end;
end;

definition
func SCM+FSA-Instr -> Subset of [:NAT ,(((union {INT ,(INT * )}) \/ SCM+FSA-Memory ) * ):] equals :: SCMFSA_1:def 4
(SCM-Instr \/ { [J,<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM+FSA-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } ) \/ { [K,<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM+FSA-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } ;
coherence
(SCM-Instr \/ { [J,<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM+FSA-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } ) \/ { [K,<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM+FSA-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } is Subset of [:NAT ,(((union {INT ,(INT * )}) \/ SCM+FSA-Memory ) * ):]
proof end;
end;

:: deftheorem defines SCM+FSA-Instr SCMFSA_1:def 4 :
SCM+FSA-Instr = (SCM-Instr \/ { [J,<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM+FSA-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } ) \/ { [K,<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM+FSA-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } ;

theorem Th2: :: SCMFSA_1:2
SCM-Instr c= SCM+FSA-Instr
proof end;

registration
cluster SCM+FSA-Instr -> non empty ;
coherence
not SCM+FSA-Instr is empty ;
end;

registration
let I be Element of SCM+FSA-Instr ;
cluster I `1 -> natural ;
coherence
InsCode I is natural
proof end;
end;

theorem Th3: :: SCMFSA_1:3
for I being Element of SCM+FSA-Instr st InsCode I <= 8 holds
I in SCM-Instr
proof end;

theorem :: SCMFSA_1:4
[0 ,{} ] in SCM+FSA-Instr by Th2, AMI_2:2;

definition
canceled;
func SCM+FSA-OK -> Function of SCM+FSA-Memory ,{INT ,(INT * )} \/ {SCM+FSA-Instr ,NAT } equals :: SCMFSA_1:def 6
((SCM+FSA-Memory --> (INT * )) +* SCM-OK ) +* ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT ));
coherence
((SCM+FSA-Memory --> (INT * )) +* SCM-OK ) +* ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT )) is Function of SCM+FSA-Memory ,{INT ,(INT * )} \/ {SCM+FSA-Instr ,NAT }
proof end;
end;

:: deftheorem SCMFSA_1:def 5 :
canceled;

:: deftheorem defines SCM+FSA-OK SCMFSA_1:def 6 :
SCM+FSA-OK = ((SCM+FSA-Memory --> (INT * )) +* SCM-OK ) +* ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT ));

Lm1: dom ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT )) c= NAT
proof end;

Lm2: rng (SCM-OK | NAT ) c= {SCM-Instr }
proof end;

Lm3: NAT c= dom ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT ))
proof end;

theorem Th5: :: SCMFSA_1:5
NAT in SCM+FSA-Memory
proof end;

theorem :: SCMFSA_1:6
for x being set
for c, b being Element of SCM+FSA-Data-Loc
for f being Element of SCM+FSA-Data*-Loc st x in {9,10} holds
[x,<*c,f,b*>] in SCM+FSA-Instr
proof end;

theorem :: SCMFSA_1:7
for x being set
for c being Element of SCM+FSA-Data-Loc
for f being Element of SCM+FSA-Data*-Loc st x in {11,12} holds
[x,<*c,f*>] in SCM+FSA-Instr
proof end;

theorem Th8: :: SCMFSA_1:8
SCM+FSA-Memory = (({NAT } \/ SCM+FSA-Data-Loc ) \/ SCM+FSA-Data*-Loc ) \/ NAT by XBOOLE_1:4;

theorem Th9: :: SCMFSA_1:9
SCM+FSA-OK . NAT = NAT
proof end;

theorem Th10: :: SCMFSA_1:10
for b being Element of SCM+FSA-Data-Loc holds SCM+FSA-OK . b = INT
proof end;

theorem Th11: :: SCMFSA_1:11
for a being Element of NAT holds SCM+FSA-OK . a = SCM+FSA-Instr
proof end;

Lm4: SCM+FSA-Data*-Loc misses SCM-Memory
proof end;

theorem Th12: :: SCMFSA_1:12
for f being Element of SCM+FSA-Data*-Loc holds SCM+FSA-OK . f = INT *
proof end;

theorem Th13: :: SCMFSA_1:13
( NAT <> INT & SCM+FSA-Instr <> INT & NAT <> SCM+FSA-Instr & NAT <> INT * & SCM+FSA-Instr <> INT * )
proof end;

theorem :: SCMFSA_1:14
for i being Element of SCM+FSA-Memory st SCM+FSA-OK . i = NAT holds
i = NAT
proof end;

theorem :: SCMFSA_1:15
for i being Element of SCM+FSA-Memory st SCM+FSA-OK . i = INT holds
i in SCM+FSA-Data-Loc
proof end;

theorem :: SCMFSA_1:16
for i being Element of SCM+FSA-Memory st SCM+FSA-OK . i = SCM+FSA-Instr holds
i in NAT
proof end;

theorem :: SCMFSA_1:17
for i being Element of SCM+FSA-Memory st SCM+FSA-OK . i = INT * holds
i in SCM+FSA-Data*-Loc
proof end;

definition
mode SCM+FSA-State is Element of product SCM+FSA-OK ;
end;

theorem Th18: :: SCMFSA_1:18
for s being SCM+FSA-State
for I being Element of SCM-Instr holds (s | SCM-Memory ) +* (NAT --> I) is SCM-State
proof end;

theorem Th19: :: SCMFSA_1:19
for s being SCM+FSA-State
for s' being SCM-State holds (s +* s') +* (s | NAT ) is SCM+FSA-State
proof end;

definition
let s be SCM+FSA-State;
let u be Nat;
func SCM+FSA-Chg s,u -> SCM+FSA-State equals :: SCMFSA_1:def 7
s +* (NAT .--> u);
coherence
s +* (NAT .--> u) is SCM+FSA-State
proof end;
end;

:: deftheorem defines SCM+FSA-Chg SCMFSA_1:def 7 :
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;
func SCM+FSA-Chg s,t,u -> SCM+FSA-State equals :: SCMFSA_1:def 8
s +* (t .--> u);
coherence
s +* (t .--> u) is SCM+FSA-State
proof end;
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 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 ;
func SCM+FSA-Chg s,t,u -> SCM+FSA-State equals :: SCMFSA_1:def 9
s +* (t .--> u);
coherence
s +* (t .--> u) is SCM+FSA-State
proof end;
end;

:: deftheorem defines SCM+FSA-Chg SCMFSA_1:def 9 :
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);

definition
let s be SCM+FSA-State;
let a be Element of SCM+FSA-Data-Loc ;
:: original: .
redefine func s . a -> Integer;
coherence
s . a is Integer
proof end;
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
proof end;
end;

definition
let x be Element of SCM+FSA-Instr ;
given c being Element of SCM+FSA-Data-Loc , f being Element of SCM+FSA-Data*-Loc , b being Element of SCM+FSA-Data-Loc , J being Element of Segm 13 such that A1: x = [J,<*c,f,b*>] ;
func x int_addr1 -> Element of SCM+FSA-Data-Loc means :: SCMFSA_1:def 10
 ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc st
( <*c,f,b*> = x `2 & it = c );
existence
ex b1, c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc st
( <*c,f,b*> = x `2 & b1 = c )
proof end;
uniqueness
for b1, b2 being Element of SCM+FSA-Data-Loc st ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc st
( <*c,f,b*> = x `2 & b1 = c ) & ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc st
( <*c,f,b*> = x `2 & b2 = c ) holds
b1 = b2
proof end;
func x int_addr2 -> Element of SCM+FSA-Data-Loc means :: SCMFSA_1:def 11
 ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc st
( <*c,f,b*> = x `2 & it = b );
existence
ex b1, c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc st
( <*c,f,b*> = x `2 & b1 = b )
proof end;
correctness
uniqueness
for b1, b2 being Element of SCM+FSA-Data-Loc st ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc st
( <*c,f,b*> = x `2 & b1 = b ) & ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc st
( <*c,f,b*> = x `2 & b2 = b ) holds
b1 = b2;
proof end;
func x coll_addr1 -> Element of SCM+FSA-Data*-Loc means :: SCMFSA_1:def 12
 ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc st
( <*c,f,b*> = x `2 & it = f );
existence
ex b1 being Element of SCM+FSA-Data*-Loc ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc st
( <*c,f,b*> = x `2 & b1 = f )
proof end;
correctness
uniqueness
for b1, b2 being Element of SCM+FSA-Data*-Loc st ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc st
( <*c,f,b*> = x `2 & b1 = f ) & ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc st
( <*c,f,b*> = x `2 & b2 = f ) holds
b1 = b2;
proof end;
end;

:: deftheorem defines int_addr1 SCMFSA_1:def 10 :
for x being Element of SCM+FSA-Instr st ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc ex J being Element of Segm 13 st x = [J,<*c,f,b*>] holds
for b2 being Element of SCM+FSA-Data-Loc holds
( b2 = x int_addr1 iff ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc st
( <*c,f,b*> = x `2 & b2 = c ) );

:: deftheorem defines int_addr2 SCMFSA_1:def 11 :
for x being Element of SCM+FSA-Instr st ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc ex J being Element of Segm 13 st x = [J,<*c,f,b*>] holds
for b2 being Element of SCM+FSA-Data-Loc holds
( b2 = x int_addr2 iff ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc st
( <*c,f,b*> = x `2 & b2 = b ) );

:: deftheorem defines coll_addr1 SCMFSA_1:def 12 :
for x being Element of SCM+FSA-Instr st ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc ex J being Element of Segm 13 st x = [J,<*c,f,b*>] holds
for b2 being Element of SCM+FSA-Data*-Loc holds
( b2 = x coll_addr1 iff ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex b being Element of SCM+FSA-Data-Loc st
( <*c,f,b*> = x `2 & b2 = f ) );

definition
let x be Element of SCM+FSA-Instr ;
given c being Element of SCM+FSA-Data-Loc , f being Element of SCM+FSA-Data*-Loc , J being Element of Segm 13 such that A1: x = [J,<*c,f*>] ;
func x int_addr3 -> Element of SCM+FSA-Data-Loc means :: SCMFSA_1:def 13
 ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `2 & it = c );
existence
ex b1, c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `2 & b1 = c )
proof end;
uniqueness
for b1, b2 being Element of SCM+FSA-Data-Loc st ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `2 & b1 = c ) & ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `2 & b2 = c ) holds
b1 = b2
proof end;
func x coll_addr2 -> Element of SCM+FSA-Data*-Loc means :: SCMFSA_1:def 14
 ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `2 & it = f );
existence
ex b1 being Element of SCM+FSA-Data*-Loc ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `2 & b1 = f )
proof end;
correctness
uniqueness
for b1, b2 being Element of SCM+FSA-Data*-Loc st ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `2 & b1 = f ) & ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `2 & b2 = f ) holds
b1 = b2;
proof end;
canceled;
end;

:: deftheorem defines int_addr3 SCMFSA_1:def 13 :
for x being Element of SCM+FSA-Instr st ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex J being Element of Segm 13 st x = [J,<*c,f*>] holds
for b2 being Element of SCM+FSA-Data-Loc holds
( b2 = x int_addr3 iff ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `2 & b2 = c ) );

:: deftheorem defines coll_addr2 SCMFSA_1:def 14 :
for x being Element of SCM+FSA-Instr st ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc ex J being Element of Segm 13 st x = [J,<*c,f*>] holds
for b2 being Element of SCM+FSA-Data*-Loc holds
( b2 = x coll_addr2 iff ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `2 & b2 = f ) );

:: deftheorem SCMFSA_1:def 15 :
canceled;

definition
let s be SCM+FSA-State;
func IC s -> Element of NAT equals :: SCMFSA_1:def 16
s . NAT ;
coherence
s . NAT is Element of NAT
proof end;
end;

:: deftheorem defines IC SCMFSA_1:def 16 :
for s being SCM+FSA-State holds IC s = s . NAT ;

definition
let x be Element of SCM+FSA-Instr ;
let s be SCM+FSA-State;
func SCM+FSA-Exec-Res x,s -> SCM+FSA-State means :: SCMFSA_1:def 17
 ex x' being Element of SCM-Instr ex s' being SCM-State st
( x = x' & s' = (s | SCM-Memory ) +* (NAT --> x') & it = (s +* (SCM-Exec-Res x',s')) +* (s | NAT ) ) if InsCode x <= 8
ex i being Integer ex k being Element of NAT st
( k = abs (s . (x int_addr2 )) & i = (s . (x coll_addr1 )) /. k & it = SCM+FSA-Chg (SCM+FSA-Chg s,(x int_addr1 ),i),(succ (IC s)) ) if InsCode x = 9
ex f being FinSequence of INT ex k being Element of NAT st
( k = abs (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),(succ (IC s)) ) if InsCode x = 10
it = SCM+FSA-Chg (SCM+FSA-Chg s,(x int_addr3 ),(len (s . (x coll_addr2 )))),(succ (IC s)) if InsCode x = 11
ex f being FinSequence of INT ex k being Element of NAT st
( k = abs (s . (x int_addr3 )) & f = k |-> 0 & it = SCM+FSA-Chg (SCM+FSA-Chg s,(x coll_addr2 ),f),(succ (IC s)) ) if InsCode x = 12
otherwise it = s;
existence
( ( InsCode x <= 8 implies ex b1 being SCM+FSA-State ex x' being Element of SCM-Instr ex s' being SCM-State st
( x = x' & s' = (s | SCM-Memory ) +* (NAT --> x') & b1 = (s +* (SCM-Exec-Res x',s')) +* (s | NAT ) ) ) & ( InsCode x = 9 implies ex b1 being SCM+FSA-State ex i being Integer ex k being Element of NAT st
( k = abs (s . (x int_addr2 )) & i = (s . (x coll_addr1 )) /. k & b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x int_addr1 ),i),(succ (IC s)) ) ) & ( InsCode x = 10 implies ex b1 being SCM+FSA-State ex f being FinSequence of INT ex k being Element of NAT st
( k = abs (s . (x int_addr2 )) & f = (s . (x coll_addr1 )) +* k,(s . (x int_addr1 )) & b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x coll_addr1 ),f),(succ (IC s)) ) ) & ( InsCode x = 11 implies ex b1 being SCM+FSA-State st b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x int_addr3 ),(len (s . (x coll_addr2 )))),(succ (IC s)) ) & ( InsCode x = 12 implies ex b1 being SCM+FSA-State ex f being FinSequence of INT ex k being Element of NAT st
( k = abs (s . (x int_addr3 )) & f = k |-> 0 & b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x coll_addr2 ),f),(succ (IC s)) ) ) & ( not InsCode x <= 8 & not InsCode x = 9 & not InsCode x = 10 & not InsCode x = 11 & not InsCode x = 12 implies ex b1 being SCM+FSA-State st b1 = s ) )
proof end;
uniqueness
for b1, b2 being SCM+FSA-State holds
( ( InsCode x <= 8 & ex x' being Element of SCM-Instr ex s' being SCM-State st
( x = x' & s' = (s | SCM-Memory ) +* (NAT --> x') & b1 = (s +* (SCM-Exec-Res x',s')) +* (s | NAT ) ) & ex x' being Element of SCM-Instr ex s' being SCM-State st
( x = x' & s' = (s | SCM-Memory ) +* (NAT --> x') & b2 = (s +* (SCM-Exec-Res x',s')) +* (s | NAT ) ) implies b1 = b2 ) & ( InsCode x = 9 & ex i being Integer ex k being Element of NAT st
( k = abs (s . (x int_addr2 )) & i = (s . (x coll_addr1 )) /. k & b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x int_addr1 ),i),(succ (IC s)) ) & ex i being Integer ex k being Element of NAT st
( k = abs (s . (x int_addr2 )) & i = (s . (x coll_addr1 )) /. k & b2 = SCM+FSA-Chg (SCM+FSA-Chg s,(x int_addr1 ),i),(succ (IC s)) ) implies b1 = b2 ) & ( InsCode x = 10 & ex f being FinSequence of INT ex k being Element of NAT st
( k = abs (s . (x int_addr2 )) & f = (s . (x coll_addr1 )) +* k,(s . (x int_addr1 )) & b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x coll_addr1 ),f),(succ (IC s)) ) & ex f being FinSequence of INT ex k being Element of NAT st
( k = abs (s . (x int_addr2 )) & f = (s . (x coll_addr1 )) +* k,(s . (x int_addr1 )) & b2 = SCM+FSA-Chg (SCM+FSA-Chg s,(x coll_addr1 ),f),(succ (IC s)) ) implies b1 = b2 ) & ( InsCode x = 11 & b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x int_addr3 ),(len (s . (x coll_addr2 )))),(succ (IC s)) & b2 = SCM+FSA-Chg (SCM+FSA-Chg s,(x int_addr3 ),(len (s . (x coll_addr2 )))),(succ (IC s)) implies b1 = b2 ) & ( InsCode x = 12 & ex f being FinSequence of INT ex k being Element of NAT st
( k = abs (s . (x int_addr3 )) & f = k |-> 0 & b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x coll_addr2 ),f),(succ (IC s)) ) & ex f being FinSequence of INT ex k being Element of NAT st
( k = abs (s . (x int_addr3 )) & f = k |-> 0 & b2 = SCM+FSA-Chg (SCM+FSA-Chg s,(x coll_addr2 ),f),(succ (IC s)) ) implies b1 = b2 ) & ( not InsCode x <= 8 & not InsCode x = 9 & not InsCode x = 10 & not InsCode x = 11 & not InsCode x = 12 & b1 = s & b2 = s implies b1 = b2 ) ) ;
consistency
for b1 being SCM+FSA-State holds
( ( InsCode x <= 8 & InsCode x = 9 implies ( ex x' being Element of SCM-Instr ex s' being SCM-State st
( x = x' & s' = (s | SCM-Memory ) +* (NAT --> x') & b1 = (s +* (SCM-Exec-Res x',s')) +* (s | NAT ) ) iff ex i being Integer ex k being Element of NAT st
( k = abs (s . (x int_addr2 )) & i = (s . (x coll_addr1 )) /. k & b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x int_addr1 ),i),(succ (IC s)) ) ) ) & ( InsCode x <= 8 & InsCode x = 10 implies ( ex x' being Element of SCM-Instr ex s' being SCM-State st
( x = x' & s' = (s | SCM-Memory ) +* (NAT --> x') & b1 = (s +* (SCM-Exec-Res x',s')) +* (s | NAT ) ) iff ex f being FinSequence of INT ex k being Element of NAT st
( k = abs (s . (x int_addr2 )) & f = (s . (x coll_addr1 )) +* k,(s . (x int_addr1 )) & b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x coll_addr1 ),f),(succ (IC s)) ) ) ) & ( InsCode x <= 8 & InsCode x = 11 implies ( ex x' being Element of SCM-Instr ex s' being SCM-State st
( x = x' & s' = (s | SCM-Memory ) +* (NAT --> x') & b1 = (s +* (SCM-Exec-Res x',s')) +* (s | NAT ) ) iff b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x int_addr3 ),(len (s . (x coll_addr2 )))),(succ (IC s)) ) ) & ( InsCode x <= 8 & InsCode x = 12 implies ( ex x' being Element of SCM-Instr ex s' being SCM-State st
( x = x' & s' = (s | SCM-Memory ) +* (NAT --> x') & b1 = (s +* (SCM-Exec-Res x',s')) +* (s | NAT ) ) iff ex f being FinSequence of INT ex k being Element of NAT st
( k = abs (s . (x int_addr3 )) & f = k |-> 0 & b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x coll_addr2 ),f),(succ (IC s)) ) ) ) & ( InsCode x = 9 & InsCode x = 10 implies ( ex i being Integer ex k being Element of NAT st
( k = abs (s . (x int_addr2 )) & i = (s . (x coll_addr1 )) /. k & b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x int_addr1 ),i),(succ (IC s)) ) iff ex f being FinSequence of INT ex k being Element of NAT st
( k = abs (s . (x int_addr2 )) & f = (s . (x coll_addr1 )) +* k,(s . (x int_addr1 )) & b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x coll_addr1 ),f),(succ (IC s)) ) ) ) & ( InsCode x = 9 & InsCode x = 11 implies ( ex i being Integer ex k being Element of NAT st
( k = abs (s . (x int_addr2 )) & i = (s . (x coll_addr1 )) /. k & b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x int_addr1 ),i),(succ (IC s)) ) iff b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x int_addr3 ),(len (s . (x coll_addr2 )))),(succ (IC s)) ) ) & ( InsCode x = 9 & InsCode x = 12 implies ( ex i being Integer ex k being Element of NAT st
( k = abs (s . (x int_addr2 )) & i = (s . (x coll_addr1 )) /. k & b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x int_addr1 ),i),(succ (IC s)) ) iff ex f being FinSequence of INT ex k being Element of NAT st
( k = abs (s . (x int_addr3 )) & f = k |-> 0 & b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x coll_addr2 ),f),(succ (IC s)) ) ) ) & ( InsCode x = 10 & InsCode x = 11 implies ( ex f being FinSequence of INT ex k being Element of NAT st
( k = abs (s . (x int_addr2 )) & f = (s . (x coll_addr1 )) +* k,(s . (x int_addr1 )) & b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x coll_addr1 ),f),(succ (IC s)) ) iff b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x int_addr3 ),(len (s . (x coll_addr2 )))),(succ (IC s)) ) ) & ( InsCode x = 10 & InsCode x = 12 implies ( ex f being FinSequence of INT ex k being Element of NAT st
( k = abs (s . (x int_addr2 )) & f = (s . (x coll_addr1 )) +* k,(s . (x int_addr1 )) & b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x coll_addr1 ),f),(succ (IC s)) ) iff ex f being FinSequence of INT ex k being Element of NAT st
( k = abs (s . (x int_addr3 )) & f = k |-> 0 & b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x coll_addr2 ),f),(succ (IC s)) ) ) ) & ( InsCode x = 11 & InsCode x = 12 implies ( b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x int_addr3 ),(len (s . (x coll_addr2 )))),(succ (IC s)) iff ex f being FinSequence of INT ex k being Element of NAT st
( k = abs (s . (x int_addr3 )) & f = k |-> 0 & b1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x coll_addr2 ),f),(succ (IC s)) ) ) ) ) ;
end;

:: deftheorem defines SCM+FSA-Exec-Res SCMFSA_1:def 17 :
for x being Element of SCM+FSA-Instr
for s, b3 being SCM+FSA-State holds
( ( InsCode x <= 8 implies ( b3 = SCM+FSA-Exec-Res x,s iff ex x' being Element of SCM-Instr ex s' being SCM-State st
( x = x' & s' = (s | SCM-Memory ) +* (NAT --> x') & b3 = (s +* (SCM-Exec-Res x',s')) +* (s | NAT ) ) ) ) & ( InsCode x = 9 implies ( b3 = SCM+FSA-Exec-Res x,s iff ex i being Integer ex k being Element of NAT st
( k = abs (s . (x int_addr2 )) & i = (s . (x coll_addr1 )) /. k & b3 = SCM+FSA-Chg (SCM+FSA-Chg s,(x int_addr1 ),i),(succ (IC s)) ) ) ) & ( InsCode x = 10 implies ( b3 = SCM+FSA-Exec-Res x,s iff ex f being FinSequence of INT ex k being Element of NAT st
( k = abs (s . (x int_addr2 )) & f = (s . (x coll_addr1 )) +* k,(s . (x int_addr1 )) & b3 = SCM+FSA-Chg (SCM+FSA-Chg s,(x coll_addr1 ),f),(succ (IC s)) ) ) ) & ( InsCode x = 11 implies ( b3 = SCM+FSA-Exec-Res x,s iff b3 = SCM+FSA-Chg (SCM+FSA-Chg s,(x int_addr3 ),(len (s . (x coll_addr2 )))),(succ (IC s)) ) ) & ( InsCode x = 12 implies ( b3 = SCM+FSA-Exec-Res x,s iff ex f being FinSequence of INT ex k being Element of NAT st
( k = abs (s . (x int_addr3 )) & f = k |-> 0 & b3 = SCM+FSA-Chg (SCM+FSA-Chg s,(x coll_addr2 ),f),(succ (IC s)) ) ) ) & ( not InsCode x <= 8 & not InsCode x = 9 & not InsCode x = 10 & not InsCode x = 11 & not InsCode x = 12 implies ( b3 = SCM+FSA-Exec-Res x,s iff b3 = s ) ) );

definition
func SCM+FSA-Exec -> Function of SCM+FSA-Instr , Funcs (product SCM+FSA-OK ),(product SCM+FSA-OK ) means :: SCMFSA_1:def 18
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
ex b1 being Function of SCM+FSA-Instr , Funcs (product SCM+FSA-OK ),(product SCM+FSA-OK ) st
for x being Element of SCM+FSA-Instr
for y being SCM+FSA-State holds (b1 . x) . y = SCM+FSA-Exec-Res x,y
proof end;
uniqueness
for b1, b2 being Function of SCM+FSA-Instr , Funcs (product SCM+FSA-OK ),(product SCM+FSA-OK ) st ( for x being Element of SCM+FSA-Instr
for y being SCM+FSA-State holds (b1 . x) . y = SCM+FSA-Exec-Res x,y ) & ( for x being Element of SCM+FSA-Instr
for y being SCM+FSA-State holds (b2 . x) . y = SCM+FSA-Exec-Res x,y ) holds
b1 = b2
proof end;
end;

:: deftheorem defines SCM+FSA-Exec SCMFSA_1:def 18 :
for b1 being Function of SCM+FSA-Instr , Funcs (product SCM+FSA-OK ),(product SCM+FSA-OK ) holds
( b1 = SCM+FSA-Exec iff for x being Element of SCM+FSA-Instr
for y being SCM+FSA-State holds (b1 . x) . y = SCM+FSA-Exec-Res x,y );

theorem :: SCMFSA_1:20
for s being SCM+FSA-State
for u being Element of NAT holds (SCM+FSA-Chg s,u) . NAT = u
proof end;

theorem :: SCMFSA_1:21
for s being SCM+FSA-State
for u being Element of NAT
for mk being Element of SCM+FSA-Data-Loc holds (SCM+FSA-Chg s,u) . mk = s . mk
proof end;

theorem :: SCMFSA_1:22
for s being SCM+FSA-State
for u being Element of 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 u, v being Element of NAT holds (SCM+FSA-Chg s,u) . v = s . v
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) . NAT = s . NAT
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 holds (SCM+FSA-Chg s,t,u) . t = u
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 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:27
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
proof end;

theorem :: SCMFSA_1:28
for s being SCM+FSA-State
for t being Element of SCM+FSA-Data-Loc
for u being Integer
for v being Element of NAT holds (SCM+FSA-Chg s,t,u) . v = s . v
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 holds (SCM+FSA-Chg s,t,u) . t = u
proof end;

theorem :: SCMFSA_1:30
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
proof end;

theorem :: SCMFSA_1:31
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
proof end;

theorem :: SCMFSA_1:32
for s being SCM+FSA-State
for t being Element of SCM+FSA-Data*-Loc
for u being FinSequence of INT
for v being Element of NAT holds (SCM+FSA-Chg s,t,u) . v = s . v
proof end;

theorem :: SCMFSA_1:33
SCM+FSA-Data*-Loc misses SCM-Memory by Lm4;