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


begin

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;

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

definition
func SCM+FSA-Instr -> non empty set equals :: SCMFSA_1:def 4
((SCM-Instr \/ { [J,{},<*c,f,b*>] where J is Element of Segm 14, 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 14, c1 is Element of SCM+FSA-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } ) \/ { [13,{},<*b1*>] where b1 is Element of SCM+FSA-Data-Loc : verum } ;
coherence
((SCM-Instr \/ { [J,{},<*c,f,b*>] where J is Element of Segm 14, 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 14, c1 is Element of SCM+FSA-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } ) \/ { [13,{},<*b1*>] where b1 is Element of SCM+FSA-Data-Loc : verum } is non empty set ;
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 14, 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 14, c1 is Element of SCM+FSA-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } ) \/ { [13,{},<*b1*>] where b1 is Element of SCM+FSA-Data-Loc : verum } ;

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;

Lm1: SCM+FSA-Instr c= [:NAT,(NAT *),(proj2 SCM+FSA-Instr):]
proof end;

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

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

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

Lm2: NAT c= SCM-Memory
by XBOOLE_1:7;

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

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

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

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

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

registration
cluster SCM-OK -> non-empty ;
coherence
SCM-OK is non-empty
proof end;
cluster SCM+FSA-OK -> non-empty ;
coherence
SCM+FSA-OK is non-empty
proof end;
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 s9 being SCM-State holds (s +* s9) +* (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 14 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 `3_3 & 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 `3_3 & 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 `3_3 & 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 `3_3 & 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 `3_3 & 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 `3_3 & 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 `3_3 & 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 `3_3 & 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 `3_3 & 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 `3_3 & 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 `3_3 & 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 `3_3 & 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 14 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 `3_3 & 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 14 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 `3_3 & 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 14 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 `3_3 & b2 = f ) );

definition
let x be Element of SCM+FSA-Instr ;
given c being Element of SCM+FSA-Data-Loc such that A1: x = [13,{},<*c*>] ;
func x int_addr -> Element of SCM+FSA-Data-Loc means :: SCMFSA_1:def 13
 ex c being Element of SCM+FSA-Data-Loc st
( <*c*> = x `3_3 & it = c );
existence
ex b1, c being Element of SCM+FSA-Data-Loc st
( <*c*> = x `3_3 & 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 st
( <*c*> = x `3_3 & b1 = c ) & ex c being Element of SCM+FSA-Data-Loc st
( <*c*> = x `3_3 & b2 = c ) holds
b1 = b2
proof end;
end;

:: deftheorem defines int_addr SCMFSA_1:def 13 :
for x being Element of SCM+FSA-Instr st ex c being Element of SCM+FSA-Data-Loc st x = [13,{},<*c*>] holds
for b2 being Element of SCM+FSA-Data-Loc holds
( b2 = x int_addr iff ex c being Element of SCM+FSA-Data-Loc st
( <*c*> = x `3_3 & b2 = c ) );

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 14 such that A1: x = [J,{},<*c,f*>] ;
func x int_addr3 -> 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 `3_3 & 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 `3_3 & 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 `3_3 & b1 = c ) & ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & b2 = c ) holds
b1 = b2
proof end;
func x coll_addr2 -> Element of SCM+FSA-Data*-Loc means :: SCMFSA_1:def 15
 ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & 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 `3_3 & 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 `3_3 & b1 = f ) & ex c being Element of SCM+FSA-Data-Loc ex f being Element of SCM+FSA-Data*-Loc st
( <*c,f*> = x `3_3 & b2 = f ) holds
b1 = b2;
proof end;
canceled;
end;

:: deftheorem defines int_addr3 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 14 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 `3_3 & b2 = c ) );

:: deftheorem defines coll_addr2 SCMFSA_1:def 15 :
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 14 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 `3_3 & b2 = f ) );

:: deftheorem SCMFSA_1:def 16 :
canceled;

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

:: deftheorem defines IC SCMFSA_1:def 17 :
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 18
 ex x9 being Element of SCM-Instr ex s9 being SCM-State st
( x = x9 & s9 = (s | SCM-Memory) +* (NAT --> x9) & it = (s +* (SCM-Exec-Res (x9,s9))) +* (s | NAT) ) if x `1_3 <= 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 x `1_3 = 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 x `1_3 = 10
it = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr3),(len (s . (x coll_addr2))))),(succ (IC s))) if x `1_3 = 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 x `1_3 = 12
ex i being Integer st
( i = 1 & it = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),(succ (IC s))) ) if x `1_3 = 13
otherwise it = s;
existence
( ( x `1_3 <= 8 implies ex b1 being SCM+FSA-State ex x9 being Element of SCM-Instr ex s9 being SCM-State st
( x = x9 & s9 = (s | SCM-Memory) +* (NAT --> x9) & b1 = (s +* (SCM-Exec-Res (x9,s9))) +* (s | NAT) ) ) & ( x `1_3 = 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))) ) ) & ( x `1_3 = 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))) ) ) & ( x `1_3 = 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))) ) & ( x `1_3 = 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))) ) ) & ( x `1_3 = 13 implies ex b1 being SCM+FSA-State ex i being Integer st
( i = 1 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),(succ (IC s))) ) ) & ( 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 b1 being SCM+FSA-State st b1 = s ) )
proof end;
uniqueness
for b1, b2 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) +* (NAT --> x9) & b1 = (s +* (SCM-Exec-Res (x9,s9))) +* (s | NAT) ) & ex x9 being Element of SCM-Instr ex s9 being SCM-State st
( x = x9 & s9 = (s | SCM-Memory) +* (NAT --> x9) & b2 = (s +* (SCM-Exec-Res (x9,s9))) +* (s | NAT) ) implies b1 = b2 ) & ( x `1_3 = 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 ) & ( x `1_3 = 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 ) & ( x `1_3 = 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 ) & ( x `1_3 = 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 ) & ( x `1_3 = 13 & ex i being Integer st
( i = 1 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),(succ (IC s))) ) & ex i being Integer st
( i = 1 & b2 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),(succ (IC s))) ) implies b1 = b2 ) & ( 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 & b1 = s & b2 = s implies b1 = b2 ) ) ;
consistency
for b1 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) +* (NAT --> x9) & b1 = (s +* (SCM-Exec-Res (x9,s9))) +* (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))) ) ) ) & ( 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) +* (NAT --> x9) & b1 = (s +* (SCM-Exec-Res (x9,s9))) +* (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))) ) ) ) & ( 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) +* (NAT --> x9) & b1 = (s +* (SCM-Exec-Res (x9,s9))) +* (s | NAT) ) iff b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr3),(len (s . (x coll_addr2))))),(succ (IC s))) ) ) & ( 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) +* (NAT --> x9) & b1 = (s +* (SCM-Exec-Res (x9,s9))) +* (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))) ) ) ) & ( 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) +* (NAT --> x9) & b1 = (s +* (SCM-Exec-Res (x9,s9))) +* (s | NAT) ) iff ex i being Integer st
( i = 1 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),(succ (IC s))) ) ) ) & ( x `1_3 = 9 & x `1_3 = 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))) ) ) ) & ( x `1_3 = 9 & x `1_3 = 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))) ) ) & ( x `1_3 = 9 & x `1_3 = 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))) ) ) ) & ( x `1_3 = 9 & x `1_3 = 13 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 i being Integer st
( i = 1 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),(succ (IC s))) ) ) ) & ( x `1_3 = 10 & x `1_3 = 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))) ) ) & ( x `1_3 = 10 & x `1_3 = 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))) ) ) ) & ( x `1_3 = 10 & x `1_3 = 13 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 i being Integer st
( i = 1 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),(succ (IC s))) ) ) ) & ( x `1_3 = 11 & x `1_3 = 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))) ) ) ) & ( x `1_3 = 11 & x `1_3 = 13 implies ( b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr3),(len (s . (x coll_addr2))))),(succ (IC s))) iff ex i being Integer st
( i = 1 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),(succ (IC s))) ) ) ) & ( x `1_3 = 12 & x `1_3 = 13 implies ( 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))) ) iff ex i being Integer st
( i = 1 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),(succ (IC s))) ) ) ) ) ;
end;

:: deftheorem defines SCM+FSA-Exec-Res SCMFSA_1:def 18 :
for x being Element of SCM+FSA-Instr
for s, b3 being SCM+FSA-State holds
( ( x `1_3 <= 8 implies ( b3 = 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) +* (NAT --> x9) & b3 = (s +* (SCM-Exec-Res (x9,s9))) +* (s | NAT) ) ) ) & ( x `1_3 = 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))) ) ) ) & ( x `1_3 = 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))) ) ) ) & ( x `1_3 = 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))) ) ) & ( x `1_3 = 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))) ) ) ) & ( x `1_3 = 13 implies ( b3 = SCM+FSA-Exec-Res (x,s) iff ex i being Integer st
( i = 1 & b3 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),(succ (IC s))) ) ) ) & ( 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 ( b3 = SCM+FSA-Exec-Res (x,s) iff b3 = s ) ) );

definition
func SCM+FSA-Exec -> Action of SCM+FSA-Instr,(product SCM+FSA-OK) means :: SCMFSA_1:def 19
 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 Action of SCM+FSA-Instr,(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 Action of SCM+FSA-Instr,(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 19 :
for b1 being Action of SCM+FSA-Instr,(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 Lm6;

theorem :: SCMFSA_1:34
SCM+FSA-Instr c= [:NAT,(NAT *),(proj2 SCM+FSA-Instr):] by Lm1;

registration
cluster proj2 SCM+FSA-Instr -> FinSequence-membered ;
coherence
proj2 SCM+FSA-Instr is FinSequence-membered
proof end;
end;

theorem :: SCMFSA_1:35
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:36
for c being Element of SCM+FSA-Data-Loc holds [13,{},<*c*>] in SCM+FSA-Instr
proof end;