X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fwhile_machine.ma;h=24e3cfd55a095931062acf5a5e6161d6c3605d29;hb=45f2accd093c8d10eb692266f4c3c0c59cb22d8b;hp=6bde5396bd76fd1cf02e54daf507b2bce6118d2c;hpb=bed400cf37906a25129907986b10f24cb499dbb4;p=helm.git

diff --git a/matita/matita/lib/turing/while_machine.ma b/matita/matita/lib/turing/while_machine.ma
index 6bde5396b..24e3cfd55 100644
--- 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.