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

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