let N be with_zero set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: according to AMISTD_1:def 8 :: thesis: 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 ; :: thesis: verum