let S be non empty standard-ins homogeneous J/A-independent set ; :: thesis: for I, J being Element of S st ex k being Nat st IncAddr (I,k) = IncAddr (J,k) holds

I = J

let I, J be Element of S; :: thesis: ( ex k being Nat st IncAddr (I,k) = IncAddr (J,k) implies I = J )

given k being Nat such that A1: IncAddr (I,k) = IncAddr (J,k) ; :: thesis: I = J

A2: InsCode I = InsCode (IncAddr (I,k)) by Def8

.= InsCode J by A1, Def8 ;

A3: AddressPart I = AddressPart (IncAddr (I,k)) by Def8

.= AddressPart J by A1, Def8 ;

A4: JumpPart (IncAddr (I,k)) = k + (JumpPart I) by Def8;

then A5: dom (JumpPart I) = dom (JumpPart (IncAddr (I,k))) by VALUED_1:def 2;

A6: JumpPart (IncAddr (J,k)) = k + (JumpPart J) by Def8;

then A7: dom (JumpPart J) = dom (JumpPart (IncAddr (J,k))) by VALUED_1:def 2;

A8: dom (JumpPart I) = dom (JumpPart J) by A2, Def5;

for x being object st x in dom (JumpPart I) holds

(JumpPart I) . x = (JumpPart J) . x

hence I = J by A2, A3, Th1; :: thesis: verum

I = J

let I, J be Element of S; :: thesis: ( ex k being Nat st IncAddr (I,k) = IncAddr (J,k) implies I = J )

given k being Nat such that A1: IncAddr (I,k) = IncAddr (J,k) ; :: thesis: I = J

A2: InsCode I = InsCode (IncAddr (I,k)) by Def8

.= InsCode J by A1, Def8 ;

A3: AddressPart I = AddressPart (IncAddr (I,k)) by Def8

.= AddressPart J by A1, Def8 ;

A4: JumpPart (IncAddr (I,k)) = k + (JumpPart I) by Def8;

then A5: dom (JumpPart I) = dom (JumpPart (IncAddr (I,k))) by VALUED_1:def 2;

A6: JumpPart (IncAddr (J,k)) = k + (JumpPart J) by Def8;

then A7: dom (JumpPart J) = dom (JumpPart (IncAddr (J,k))) by VALUED_1:def 2;

A8: dom (JumpPart I) = dom (JumpPart J) by A2, Def5;

for x being object st x in dom (JumpPart I) holds

(JumpPart I) . x = (JumpPart J) . x

proof

then
JumpPart I = JumpPart J
by A8;
let x be object ; :: thesis: ( x in dom (JumpPart I) implies (JumpPart I) . x = (JumpPart J) . x )

assume A9: x in dom (JumpPart I) ; :: thesis: (JumpPart I) . x = (JumpPart J) . x

A10: (JumpPart (IncAddr (I,k))) . x = k + ((JumpPart I) . x) by A4, A5, A9, VALUED_1:def 2;

A11: (JumpPart (IncAddr (J,k))) . x = k + ((JumpPart J) . x) by A6, A8, A9, A7, VALUED_1:def 2;

thus (JumpPart I) . x = (JumpPart J) . x by A1, A10, A11; :: thesis: verum

end;assume A9: x in dom (JumpPart I) ; :: thesis: (JumpPart I) . x = (JumpPart J) . x

A10: (JumpPart (IncAddr (I,k))) . x = k + ((JumpPart I) . x) by A4, A5, A9, VALUED_1:def 2;

A11: (JumpPart (IncAddr (J,k))) . x = k + ((JumpPart J) . x) by A6, A8, A9, A7, VALUED_1:def 2;

thus (JumpPart I) . x = (JumpPart J) . x by A1, A10, A11; :: thesis: verum

hence I = J by A2, A3, Th1; :: thesis: verum