let N be with_zero set ; for A being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N
for I being Instruction of A
for s being State of A
for o being Object of A
for w being Element of Values o st I is sequential & o <> IC holds
IC (Exec (I,s)) = IC (Exec (I,(s +* (o,w))))
let A be non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N; for I being Instruction of A
for s being State of A
for o being Object of A
for w being Element of Values o st I is sequential & o <> IC holds
IC (Exec (I,s)) = IC (Exec (I,(s +* (o,w))))
let I be Instruction of A; for s being State of A
for o being Object of A
for w being Element of Values o st I is sequential & o <> IC holds
IC (Exec (I,s)) = IC (Exec (I,(s +* (o,w))))
let s be State of A; for o being Object of A
for w being Element of Values o st I is sequential & o <> IC holds
IC (Exec (I,s)) = IC (Exec (I,(s +* (o,w))))
let o be Object of A; for w being Element of Values o st I is sequential & o <> IC holds
IC (Exec (I,s)) = IC (Exec (I,(s +* (o,w))))
let w be Element of Values o; ( I is sequential & o <> IC 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 ) = (IC s) + 1
and
A2:
o <> IC
; AMISTD_1:def 8 IC (Exec (I,s)) = IC (Exec (I,(s +* (o,w))))
thus IC (Exec (I,s)) =
(IC s) + 1
by A1
.=
(IC (s +* (o,w))) + 1
by A2, FUNCT_7:32
.=
IC (Exec (I,(s +* (o,w))))
by A1
; verum