let N be non empty with_non-empty_elements set ; :: thesis: for A being non empty stored-program IC-Ins-separated definite standard-ins AMI-Struct of N
for I being Instruction of A
for o being Object of A st I is jump-only & o in Output I holds
o = IC A
let A be non empty stored-program IC-Ins-separated definite standard-ins AMI-Struct of N; :: thesis: for I being Instruction of A
for o being Object of A st I is jump-only & o in Output I holds
o = IC A
let I be Instruction of A; :: thesis: for o being Object of A st I is jump-only & o in Output I holds
o = IC A
let o be Object of A; :: thesis: ( I is jump-only & o in Output I implies o = IC A )
assume A1: for s being State of A
for o being Object of A
for J being Instruction of A st InsCode I = InsCode J & o <> IC A holds
(Exec J,s) . o = s . o ; :: according to AMISTD_1:def 3,AMISTD_1:def 4 :: thesis: ( not o in Output I or o = IC A )
assume o in Output I ; :: thesis: o = IC A
then ex s being State of A st s . o <> (Exec I,s) . o by Def3;
hence o = IC A by A1; :: thesis: verum