let k be Nat; for S being non empty standard-ins homogeneous J/A-independent set
for I being Element of S st I is ins-loc-free holds
IncAddr (I,k) = I
let S be non empty standard-ins homogeneous J/A-independent set ; for I being Element of S st I is ins-loc-free holds
IncAddr (I,k) = I
let I be Element of S; ( I is ins-loc-free implies IncAddr (I,k) = I )
assume A1:
JumpPart I is empty
; COMPOS_0:def 8 IncAddr (I,k) = I
set f = IncAddr (I,k);
A2:
InsCode (IncAddr (I,k)) = InsCode I
by Def8;
A3:
AddressPart (IncAddr (I,k)) = AddressPart I
by Def8;
A4:
JumpPart (IncAddr (I,k)) = k + (JumpPart I)
by Def8;
JumpPart (IncAddr (I,k)) = JumpPart I
by A1, A4;
hence
IncAddr (I,k) = I
by A2, A3, Th1; verum