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 +* (o,w)))) = 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 +* (o,w)))) = 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 +* (o,w)))) = 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 +* (o,w)))) = 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 +* (o,w)))) = IC ((Exec (I,s)) +* (o,w))
let w be Element of Values o; :: thesis: ( I is sequential & o <> IC implies IC (Exec (I,(s +* (o,w)))) = IC ((Exec (I,s)) +* (o,w)) )
assume that
A1: I is sequential and
A2: o <> IC ; :: thesis: IC (Exec (I,(s +* (o,w)))) = IC ((Exec (I,s)) +* (o,w))
thus IC (Exec (I,(s +* (o,w)))) = IC (Exec (I,s)) by A1, A2, Th1
.= IC ((Exec (I,s)) +* (o,w)) by A2, FUNCT_7:32 ; :: thesis: verum