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