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 +* (o,w)))) = 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 +* (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 ObjectKind o st I is sequential & o <> IC A 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 ObjectKind o st I is sequential & o <> IC A 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 ObjectKind o st I is sequential & o <> IC A holds
IC (Exec (I,(s +* (o,w)))) = 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 +* (o,w)))) = IC ((Exec (I,s)) +* (o,w)) )
assume that
A1: I is sequential and
A2: o <> IC A ; :: 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, Th6
.= IC ((Exec (I,s)) +* (o,w)) by A2, FUNCT_7:34 ; :: thesis: verum