:: deftheorem defines SCM+FSA-Exec-Res SCMFSA_1:def 16 :
for x being Element of SCM+FSA-Instr
for s, b₃ being SCM+FSA-State holds
( ( x `1_3 <= 8 implies ( b<sub>3</sub> = SCM+FSA-Exec-Res (x,s) iff ex x9 being Element of SCM-Instr ex s9 being SCM-State st
( x = x9 & s9 = s | SCM-Memory & b<sub>3</sub> = s +* (SCM-Exec-Res (x9,s9)) ) ) ) & ( x `1_3 = 9 implies ( b₃ = SCM+FSA-Exec-Res (x,s) iff ex i being Integer ex k being Nat st
( k = |.(s . (x int_addr2)).| & i = (s . (x coll_addr1)) /. k & b₃ = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr1),i)),((IC s) + 1)) ) ) ) & ( x `1_3 = 10 implies ( b<sub>3</sub> = SCM+FSA-Exec-Res (x,s) iff ex f being FinSequence of INT ex k being Nat st
( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & b<sub>3</sub> = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),((IC s) + 1)) ) ) ) & ( x `1_3 = 11 implies ( b₃ = SCM+FSA-Exec-Res (x,s) iff b₃ = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr3),(len (s . (x coll_addr2))))),((IC s) + 1)) ) ) & ( x `1_3 = 12 implies ( b<sub>3</sub> = SCM+FSA-Exec-Res (x,s) iff ex f being FinSequence of INT ex k being Nat st
( k = |.(s . (x int_addr3)).| & f = k |-> 0 & b<sub>3</sub> = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr2),f)),((IC s) + 1)) ) ) ) & ( x `1_3 = 13 implies ( b₃ = SCM+FSA-Exec-Res (x,s) iff ex i being Integer st
( i = 1 & b₃ = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),((IC s) + 1)) ) ) ) & ( not x `1_3 <= 8 & not x `1_3 = 9 & not x `1_3 = 10 & not x `1_3 = 11 & not x `1_3 = 12 & not x `1_3 = 13 implies ( b₃ = SCM+FSA-Exec-Res (x,s) iff b₃ = s ) ) );