Finally a correct atomicity theorem, maybe?
Finally a correct atomicity theorem, maybe?

we need a step constraint on `star tsmstep_fail`, otherwise
the program might go beyond the high-level instruction
we are considering.

proved the trivial Halt case by induction on step n.
This is easy because the step constraint does not matter for Halt.
For other cases, we need to bound the step by showing that
when n is too big, then the NS premise will no longer hold.

mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl