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