take Stop S ; :: thesis: not Stop S is halt-free
thus not Stop S is halt-free ; :: thesis: verum