let I be Instruction of SCMPDS; :: thesis: ( I = [0,{},{}] implies I is halting )
assume I = [0,{},{}] ; :: thesis: I is halting
then A1: InsCode I = 0 ;
let s be State of SCMPDS; :: according to EXTPRO_1:def 3 :: thesis: Exec (I,s) = s
thus Exec (I,s) = s by A1, Lm11; :: thesis: verum