let k be Nat; :: thesis: 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 ; :: thesis: for I being Element of S st I is ins-loc-free holds
IncAddr (I,k) = I
let I be Element of S; :: thesis: ( I is ins-loc-free implies IncAddr (I,k) = I )
assume A1: JumpPart I is empty ; :: according to COMPOS_0:def 8 :: thesis: 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; :: thesis: verum