for s being State of SCMPDS
for P, Q being Instruction-Sequence of SCMPDS st Q = P +* (((IC s),((IC s) + 1)) --> ((goto 1),(goto (- 1)))) holds
not Q halts_on s