X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Flib%2Fturing%2Funiversal%2Fmove_char_l.ma;h=bed0ba5960e6654ca999cf67f5defd9d35e12c75;hb=bc02962ed23518a09e7f4ed875d7d967a33de135;hp=ea9afc8d8ebe7c4679291b83ccc5b5e77e528454;hpb=aa45ebcc7a3bb09ae75a69620732b2544ac3ea4a;p=helm.git

diff --git a/matita/matita/lib/turing/universal/move_char_l.ma b/matita/matita/lib/turing/universal/move_char_l.ma
index ea9afc8d8..bed0ba596 100644
--- a/matita/matita/lib/turing/universal/move_char_l.ma
+++ b/matita/matita/lib/turing/universal/move_char_l.ma
@@ -73,9 +73,9 @@ lemma sem_mcl_step :
   ]
 qed.
     
-(* the move_char (variant c) machine *)
+(* the move_char (variant left) machine *)
 definition move_char_l ≝ 
-  λalpha,sep.whileTM alpha (mcl_step alpha sep) 〈mcl3,sep〉.
+  λalpha,sep.whileTM alpha (mcl_step alpha sep) (inr … (inl … (inr … start_nop))).
 
 definition R_move_char_l ≝ 
   λalpha,sep,t1,t2.
@@ -150,4 +150,17 @@ lemma terminate_move_char_l :
       [#Hb @False_ind /2/ | #Hmemb cases (orb_true_l … Hmemb)
         [#eqsep %1 >(\P eqsep) // | #H %2 //]
   ]
-qed.
\ No newline at end of file
+qed.
+
+(* NO GOOD: we must stop if current = None too!!! 
+lemma ssem_move_char_l :
+  ∀alpha,sep.
+  Realize alpha (move_char_l alpha sep) (R_move_char_l alpha sep).
+#alpha #sep *
+[ %{5} % [| % [whd in ⊢ (??%?);
+ @WRealize_to_Realize // @terminate_move_char_l
+*)
+
+axiom ssem_move_char_l :
+  ∀alpha,sep.
+  Realize alpha (move_char_l alpha sep) (R_move_char_l alpha sep).