theorem Th16: :: COMPOS_1:26

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