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