More conjectures proved.

[helm.git] / matita / matita / lib / turing / universal / move_char_l.ma

diff --git a/matita/matita/lib/turing/universal/move_char_l.ma b/matita/matita/lib/turing/universal/move_char_l.ma
index ea9afc8d8ebe7c4679291b83ccc5b5e77e528454..bed0ba5960e6654ca999cf67f5defd9d35e12c75 100644 (file)
--- 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).