let N be non empty with_non-empty_elements set ; :: thesis: for S being standard-ins homogeneous regular J/A-independent non empty IC-Ins-separated AMI-Struct of N
for I being Instruction of S st I is jump-only holds
for k being Element of NAT holds IncAddr (I,k) is jump-only
let S be standard-ins homogeneous regular J/A-independent non empty IC-Ins-separated AMI-Struct of N; :: thesis: for I being Instruction of S st I is jump-only holds
for k being Element of NAT holds IncAddr (I,k) is jump-only
let I be Instruction of S; :: thesis: ( I is jump-only implies for k being Element of NAT holds IncAddr (I,k) is jump-only )
assume A1: I is jump-only ; :: thesis: for k being Element of NAT holds IncAddr (I,k) is jump-only
let k be Element of NAT ; :: thesis: IncAddr (I,k) is jump-only
A2: InsCode I = InsCode (IncAddr (I,k)) by COMPOS_1:def 17;
InsCode I is jump-only by A1, AMISTD_1:def 2;
hence IncAddr (I,k) is jump-only by A2, AMISTD_1:def 2; :: thesis: verum