let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of N
for I, J being Instruction of S st ex k being natural number st IncAddr I,k = IncAddr J,k holds
I = J
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of N; :: thesis: for I, J being Instruction of S st ex k being natural number st IncAddr I,k = IncAddr J,k holds
I = J
let I, J be Instruction of S; :: thesis: ( ex k being natural number st IncAddr I,k = IncAddr J,k implies I = J )
given k being natural number such that A1: IncAddr I,k = IncAddr J,k ; :: thesis: I = J
A2: InsCode I = InsCode (IncAddr I,k) by Def14
.= InsCode J by A1, Def14 ;
then A3: dom (AddressPart I) = dom (AddressPart J) by Def4;
for x being set st x in dom (AddressPart I) holds
(AddressPart I) . x = (AddressPart J) . x
proof
let x be set ; :: thesis: ( x in dom (AddressPart I) implies (AddressPart I) . x = (AddressPart J) . x )
assume A4: x in dom (AddressPart I) ; :: thesis: (AddressPart I) . x = (AddressPart J) . x
per cases ( (product" (AddressParts (InsCode I))) . x = NAT or (product" (AddressParts (InsCode I))) . x <> NAT ) ;
suppose A5: (product" (AddressParts (InsCode I))) . x = NAT ; :: thesis: (AddressPart I) . x = (AddressPart J) . x
then consider f being Element of NAT such that
A6: f = (AddressPart I) . x and
A7: (AddressPart (IncAddr I,k)) . x = il. S,(k + (locnum f,S)) by A4, Def14;
(product" (AddressParts (InsCode J))) . x = NAT by A1, A5, Th32;
then consider g being Element of NAT such that
A8: g = (AddressPart J) . x and
A9: (AddressPart (IncAddr J,k)) . x = il. S,(k + (locnum g,S)) by A3, A4, Def14;
k + (locnum f,S) = k + (locnum g,S) by A1, A7, A9, AMISTD_1:25;
hence (AddressPart I) . x = (AddressPart J) . x by A6, A8, AMISTD_1:27; :: thesis: verum
end;
end;
end;
hence I = J by A2, A3, FUNCT_1:9, MCART_1:95; :: thesis: verum