for k being Nat
for S being COM-Struct holds Shift ((Stop S),k) = k .--> (halt S)