let N be with_zero set ; :: thesis: for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over 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
let A be non empty with_non-empty_values IC-Ins-separated AMI-Struct over 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
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
let o be Object of A; :: thesis: ( I is jump-only & o in Output I implies o = IC )
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 in Data-Locations holds
(Exec (J,s)) . o = s . o ; :: according to AMISTD_1:def 1,AMISTD_1:def 2 :: thesis: ( not o in Output I or o = IC )
assume o in Output I ; :: thesis: o = IC
then ex s being State of A st s . o <> (Exec (I,s)) . o by Def3;
then A2: not o in Data-Locations by A1;
o in the carrier of A ;
then o in {(IC )} \/ (Data-Locations ) by STRUCT_0:4;
then o in {(IC )} by A2, XBOOLE_0:def 3;
hence o = IC by TARSKI:def 1; :: thesis: verum