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 Lm11;
hence I = halt SCMPDS by Lm11; :: thesis: verum