Many changes

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

diff --git a/matita/matita/lib/turing/while_machine.ma b/matita/matita/lib/turing/while_machine.ma
index 6bde5396bd76fd1cf02e54daf507b2bce6118d2c..24e3cfd55a095931062acf5a5e6161d6c3605d29 100644 (file)
--- a/matita/matita/lib/turing/while_machine.ma
+++ b/matita/matita/lib/turing/while_machine.ma
@@ -18,7 +18,7 @@ distinguished final state $q$ to the initial state. *)
 
 definition while_trans ≝ λsig. λM : TM sig. λq:states sig M. λp.
   let 〈s,a〉 ≝ p in
-  if s == q then 〈start ? M, None ?〉
+  if s == q then 〈start ? M, None ?,N〉
   else trans ? M p.
   
 definition whileTM ≝ λsig. λM : TM sig. λqacc: states ? M.