[Noted that the small-step semantics is incorrect.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080522231008
 + With respect to the big-step semantics; it allows an infinite
   sequence of interrupts.
] hunk ./SmallStep.agda 4
+
+-- Note that this definition is incorrect: In the unblocked state it
+-- allows infinite transition sequences (interrupt, interrupt,
+-- interrupt…), also for total terms. This implies that the statement
+-- of the previous proof of equivalence between this semantics and the
+-- big-step semantics is incorrect.