:: 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 proofend; 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 proofend; 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 proofend; 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 proofend; Lm2: dom SCM-OK c= dom SCM+FSA-OK proofend; Lm3: NAT in dom SCM+FSA-OK proofend; Lm4: SCM+FSA-OK . NAT = 0 proofend; theorem Th9: :: SCMFSA_1:9 (SCM*-VAL * SCM+FSA-OK) . NAT = NAT proofend; Lm5: for b being Element of SCM+FSA-Data-Loc holds SCM+FSA-OK . b = 1 proofend; theorem Th10: :: SCMFSA_1:10 for b being Element of SCM+FSA-Data-Loc holds (SCM*-VAL * SCM+FSA-OK) . b = INT proofend; Lm6: for f being Element of SCM+FSA-Data*-Loc holds SCM+FSA-OK . f = 2 proofend; theorem Th11: :: SCMFSA_1:11 for f being Element of SCM+FSA-Data*-Loc holds (SCM*-VAL * SCM+FSA-OK) . f = INT * proofend; 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 clusterSCM+FSA-OK * SCM*-VAL -> non-empty ; coherence SCM*-VAL * SCM+FSA-OK is non-empty proofend; 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 proofend; theorem Th18: :: SCMFSA_1:18 for s being SCM+FSA-State for s1 being SCM-State holds s +* s1 is SCM+FSA-State proofend; 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 proofend; 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 proofend; 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 proofend; 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 ; clusters . a -> integer ; coherence s . a is integer proofend; end; definition let s be SCM+FSA-State; let a be Element of SCM+FSA-Data*-Loc ; :: original:. redefine funcs . a -> FinSequence of INT ; coherence s . a is FinSequence of INT proofend; 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 proofend; 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 ) ) proofend; 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) proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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;