let N be with_non-empty_elements set ; :: thesis: for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for f being Instruction-Location of T holds f <> NextLoc f
let T be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N; :: thesis: for f being Instruction-Location of T holds f <> NextLoc f
let f be Instruction-Location of T; :: thesis: f <> NextLoc f
assume f = NextLoc f ; :: thesis: contradiction
then locnum f = (locnum f) + 1 by Def13;
hence contradiction ; :: thesis: verum