let N be non empty with_non-empty_elements set ; :: thesis: for k being natural number
for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-Struct of N
for I being Instruction of S st I is ins-loc-free holds
IncAddr (I,k) = I
let k be natural number ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent COM-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 homogeneous regular J/A-independent COM-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 COMPOS_1:def 37 :: thesis: IncAddr (I,k) = I
set f = IncAddr (I,k);
A2: InsCode (IncAddr (I,k)) = InsCode I by Def38;
XX: AddressPart (IncAddr (I,k)) = AddressPart I by Def38;
JumpPart (IncAddr (I,k)) = k + (JumpPart I) by Def38;
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, Th7; :: thesis: verum