let k be natural number ; :: thesis: for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N
for I being Instruction of S st I is ins-loc-free holds
IncAddr I,k = I
let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N
for I being Instruction of S st I is ins-loc-free holds
IncAddr I,k = I
let S be non empty stored-program IC-Ins-separated definite standard-ins standard homogeneous regular J/A-independent AMI-Struct of N; :: thesis: for I being Instruction of S st I is ins-loc-free holds
IncAddr I,k = I
let I be Instruction of S; :: thesis: ( I is ins-loc-free implies IncAddr I,k = I )
assume A1: JumpPart I is empty ; :: according to AMISTD_2:def 13 :: thesis: IncAddr I,k = I
set f = IncAddr I,k;
A2: InsCode (IncAddr I,k) = InsCode I by Def14;
XX: AddressPart (IncAddr I,k) = AddressPart I by Def14;
JumpPart (IncAddr I,k) = k + (JumpPart I) by Def14;
then A3: dom (JumpPart (IncAddr I,k)) = dom (JumpPart I) by VALUED_1:def 2;
JumpPart (IncAddr I,k) = JumpPart I by A1, A3;
hence IncAddr I,k = I by A2, XX, COMPOS_1:7; :: thesis: verum