let k be natural number ; :: thesis: for S being standard-ins homogeneous regular J/A-independent COM-Struct
for I being Instruction of S st I is ins-loc-free holds
IncAddr (I,k) = I
let S be standard-ins homogeneous regular J/A-independent COM-Struct ; :: 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 16 :: thesis: IncAddr (I,k) = I
set f = IncAddr (I,k);
A2: InsCode (IncAddr (I,k)) = InsCode I by Def38;
A3: AddressPart (IncAddr (I,k)) = AddressPart I by Def38;
JumpPart (IncAddr (I,k)) = k + (JumpPart I) by Def38;
then A4: dom (JumpPart (IncAddr (I,k))) = dom (JumpPart I) by VALUED_1:def 2;
JumpPart (IncAddr (I,k)) = JumpPart I by A1, A4;
hence IncAddr (I,k) = I by A2, A3, Th7; :: thesis: verum