let N be non empty with_non-empty_elements set ; :: thesis: for A being non empty stored-program IC-Ins-separated definite standard AMI-Struct of N
for I being Instruction of A
for s being State of A
for o being Object of A
for w being Element of ObjectKind o st I is sequential & o <> IC A holds
IC (Exec I,s) = IC (Exec I,(s +* o,w))
let A be non empty stored-program IC-Ins-separated definite standard AMI-Struct of N; :: thesis: for I being Instruction of A
for s being State of A
for o being Object of A
for w being Element of ObjectKind o st I is sequential & o <> IC A holds
IC (Exec I,s) = IC (Exec I,(s +* o,w))
let I be Instruction of A; :: thesis: for s being State of A
for o being Object of A
for w being Element of ObjectKind o st I is sequential & o <> IC A holds
IC (Exec I,s) = IC (Exec I,(s +* o,w))
let s be State of A; :: thesis: for o being Object of A
for w being Element of ObjectKind o st I is sequential & o <> IC A holds
IC (Exec I,s) = IC (Exec I,(s +* o,w))
let o be Object of A; :: thesis: for w being Element of ObjectKind o st I is sequential & o <> IC A holds
IC (Exec I,s) = IC (Exec I,(s +* o,w))
let w be Element of ObjectKind o; :: thesis: ( I is sequential & o <> IC A implies IC (Exec I,s) = IC (Exec I,(s +* o,w)) )
assume that
A1: for s being State of A holds (Exec I,s) . (IC A) = succ (IC s) and
A2: o <> IC A ; :: according to AMISTD_1:def 16 :: thesis: IC (Exec I,s) = IC (Exec I,(s +* o,w))
thus IC (Exec I,s) = succ (IC s) by A1
.= succ (IC (s +* o,w)) by A2, FUNCT_7:34
.= IC (Exec I,(s +* o,w)) by A1 ; :: thesis: verum