let N be non empty with_non-empty_elements set ; :: thesis: for A being non empty stored-program IC-Ins-separated definite steady-programmed AMI-Struct of N
for s being State of A
for o being Object of A
for f being Element of NAT
for I being Instruction of A
for w being Element of ObjectKind o st f <> o holds
(Exec I,s) . f = (Exec I,(s +* o,w)) . f
let A be non empty stored-program IC-Ins-separated definite steady-programmed AMI-Struct of N; :: thesis: for s being State of A
for o being Object of A
for f being Element of NAT
for I being Instruction of A
for w being Element of ObjectKind o st f <> o holds
(Exec I,s) . f = (Exec I,(s +* o,w)) . f
let s be State of A; :: thesis: for o being Object of A
for f being Element of NAT
for I being Instruction of A
for w being Element of ObjectKind o st f <> o holds
(Exec I,s) . f = (Exec I,(s +* o,w)) . f
let o be Object of A; :: thesis: for f being Element of NAT
for I being Instruction of A
for w being Element of ObjectKind o st f <> o holds
(Exec I,s) . f = (Exec I,(s +* o,w)) . f
let f be Element of NAT ; :: thesis: for I being Instruction of A
for w being Element of ObjectKind o st f <> o holds
(Exec I,s) . f = (Exec I,(s +* o,w)) . f
let I be Instruction of A; :: thesis: for w being Element of ObjectKind o st f <> o holds
(Exec I,s) . f = (Exec I,(s +* o,w)) . f
let w be Element of ObjectKind o; :: thesis: ( f <> o implies (Exec I,s) . f = (Exec I,(s +* o,w)) . f )
assume A1: f <> o ; :: thesis: (Exec I,s) . f = (Exec I,(s +* o,w)) . f
thus (Exec I,s) . f = s . f by AMI_1:def 13
.= (s +* o,w) . f by A1, FUNCT_7:34
.= (Exec I,(s +* o,w)) . f by AMI_1:def 13 ; :: thesis: verum