let x be set ; :: thesis: for N being non empty with_non-empty_elements set
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 & (product" (AddressParts (InsCode I))) . x = NAT holds
(product" (AddressParts (InsCode J))) . x = NAT
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 & (product" (AddressParts (InsCode I))) . x = NAT holds
(product" (AddressParts (InsCode J))) . x = NAT
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 & (product" (AddressParts (InsCode I))) . x = NAT holds
(product" (AddressParts (InsCode J))) . x = NAT
let I, J be Instruction of S; :: thesis: ( ex k being natural number st IncAddr I,k = IncAddr J,k & (product" (AddressParts (InsCode I))) . x = NAT implies (product" (AddressParts (InsCode J))) . x = NAT )
given k being natural number such that A1: IncAddr I,k = IncAddr J,k ; :: thesis: ( not (product" (AddressParts (InsCode I))) . x = NAT or (product" (AddressParts (InsCode J))) . x = NAT )
assume A2: (product" (AddressParts (InsCode I))) . x = NAT ; :: thesis: (product" (AddressParts (InsCode J))) . x = NAT
assume A3: (product" (AddressParts (InsCode J))) . x <> NAT ; :: thesis: contradiction
(product" (AddressParts (InsCode (IncAddr I,k)))) . x = NAT by A2, Th31;
hence contradiction by A1, A3, Def14; :: thesis: verum