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


begin

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

definition
canceled;
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 SCMFSA_1:def 1 :
canceled;

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

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

definition
canceled;
func SCM+FSA-OK -> Function of SCM+FSA-Memory,3 equals :: SCMFSA_1:def 4
(SCM+FSA-Memory --> 2) +* SCM-OK;
coherence
(SCM+FSA-Memory --> 2) +* SCM-OK is Function of SCM+FSA-Memory,3
proof end;
end;

:: deftheorem SCMFSA_1:def 3 :
canceled;

:: deftheorem defines SCM+FSA-OK SCMFSA_1:def 4 :
SCM+FSA-OK = (SCM+FSA-Memory --> 2) +* SCM-OK;

theorem :: SCMFSA_1:2
canceled;

theorem :: SCMFSA_1:3
canceled;

theorem :: SCMFSA_1:4
canceled;

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

theorem :: SCMFSA_1:6
canceled;

theorem :: SCMFSA_1:7
canceled;

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

definition
func SCM*-VAL -> ManySortedSet of 3 equals :: SCMFSA_1:def 5
<%NAT,INT,(INT *)%>;
coherence
<%NAT,INT,(INT *)%> is ManySortedSet of 3
;
end;

:: deftheorem defines SCM*-VAL SCMFSA_1:def 5 :
SCM*-VAL = <%NAT,INT,(INT *)%>;

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;

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

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

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

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

theorem Th11: :: SCMFSA_1:11
for f being Element of SCM+FSA-Data*-Loc holds (SCM*-VAL * SCM+FSA-OK) . f = INT *
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;

registration
cluster SCM+FSA-OK * SCM*-VAL -> non-empty ;
coherence
SCM*-VAL * SCM+FSA-OK is non-empty
proof end;
end;

definition
mode SCM+FSA-State is Element of product (SCM*-VAL * SCM+FSA-OK);
end;

theorem :: SCMFSA_1:12
canceled;

theorem :: SCMFSA_1:13
canceled;

theorem :: SCMFSA_1:14
canceled;

theorem :: SCMFSA_1:15
canceled;

theorem :: SCMFSA_1:16
canceled;

theorem Th17: :: SCMFSA_1:17
for s being SCM+FSA-State
for I being Element of SCM-Instr holds s | SCM-Memory is SCM-State
proof end;

theorem Th18: :: SCMFSA_1:18
for s being SCM+FSA-State
for s1 being SCM-State holds s +* s1 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 6
s +* (NAT .--> u);
coherence
s +* (NAT .--> u) is SCM+FSA-State
proof end;
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);

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 7
s +* (t .--> u);
coherence
s +* (t .--> u) is SCM+FSA-State
proof end;
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);

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 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 FinSequence of INT holds SCM+FSA-Chg (s,t,u) = s +* (t .--> u);

registration
let s be SCM+FSA-State;
let a be Element of SCM+FSA-Data-Loc ;
cluster 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
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
let s be SCM+FSA-State;
func IC s -> Element of NAT equals :: SCMFSA_1:def 15
s . NAT;
coherence
s . NAT is Element of NAT
proof end;
end;

:: deftheorem SCMFSA_1:def 9 :
canceled;

:: deftheorem SCMFSA_1:def 10 :
canceled;

:: deftheorem SCMFSA_1:def 11 :
canceled;

:: deftheorem SCMFSA_1:def 12 :
canceled;

:: deftheorem SCMFSA_1:def 13 :
canceled;

:: deftheorem SCMFSA_1:def 14 :
canceled;

:: deftheorem defines IC SCMFSA_1:def 15 :
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 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 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 & b1 = s +* (SCM-Exec-Res (x9,s9)) ) ) & ( 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 & b1 = 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 & b2 = s +* (SCM-Exec-Res (x9,s9)) ) 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 & b1 = s +* (SCM-Exec-Res (x9,s9)) ) 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 & b1 = s +* (SCM-Exec-Res (x9,s9)) ) 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 & b1 = s +* (SCM-Exec-Res (x9,s9)) ) 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 & b1 = s +* (SCM-Exec-Res (x9,s9)) ) 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 & b1 = s +* (SCM-Exec-Res (x9,s9)) ) 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 16 :
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 & b3 = s +* (SCM-Exec-Res (x9,s9)) ) ) ) & ( 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*-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
ex b1 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 (b1 . x) . y = SCM+FSA-Exec-Res (x,y)
proof end;
uniqueness
for b1, b2 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 (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 17 :
for b1 being Action of SCM+FSA-Instr,(product (SCM*-VAL * 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:19
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:20
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:21
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:22
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: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
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
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
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
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
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
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
proof end;

theorem :: SCMFSA_1:30
SCM+FSA-Data*-Loc misses SCM-Memory by Lm1;

theorem :: SCMFSA_1:31
canceled;

theorem :: SCMFSA_1:32
dom (SCM*-VAL * SCM+FSA-OK) = SCM+FSA-Memory by Lm8;

theorem :: SCMFSA_1:33
for s being SCM+FSA-State holds dom s = SCM+FSA-Memory by Lm8, CARD_3:9;