let I be Instruction of SCMPDS ; :: thesis: ( I is halting implies I = halt SCMPDS )
assume I is halting ; :: thesis: I = halt SCMPDS
then I = goto 0 by Lm10;
hence I = halt SCMPDS by Lm10; :: thesis: verum