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 (product" (AddressParts (InsCode J))) . x = NAT ; :: thesis: contradiction
then (product" (AddressParts (InsCode (IncAddr J,k)))) . x = NAT by Th31;
hence contradiction by A1, A2, Th31; :: thesis: verum