Sys.Break no longer catched

[helm.git] / matita / matita / lib / turing / mono.ma

diff --git a/matita/matita/lib/turing/mono.ma b/matita/matita/lib/turing/mono.ma
index 8d772af34beb2cbda26d5987a6ee7a59b9820c50..e559c88dbc7970375f6a6b41bfe50ac62e2d825b 100644 (file)
--- a/matita/matita/lib/turing/mono.ma
+++ b/matita/matita/lib/turing/mono.ma
@@ -214,6 +214,10 @@ qed.
 definition loopM ≝ λsig,M,i,cin.
   loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) cin.
 
+lemma loopM_unfold : ∀sig,M,i,cin.
+  loopM sig M i cin = loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) cin.
+// qed.
+
 definition initc ≝ λsig.λM:TM sig.λt.
   mk_config sig (states sig M) (start sig M) t.