X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Funiversal%2Fmove_char_l.ma;h=57ba67bdcde1d07ada92fd0e95b8b40ede91386d;hb=7d58d5dc7f897622f2010326023b17c6592d5f03;hp=a35d714d8928b3d9b3ac985413cc598981fd118f;hpb=5c1794aba0652c0b0bce80a9ffc426192327709f;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 a35d714d8..57ba67bdc 100644
--- a/matita/matita/lib/turing/universal/move_char_l.ma
+++ b/matita/matita/lib/turing/universal/move_char_l.ma
@@ -62,7 +62,7 @@ definition mcl_step ≝
   〈0,sep〉
   (λq.let 〈q',a〉 ≝ q in q' == 3 ∨ q' == 4).
 
-lemma mcc_q0_q1 : 
+lemma mcl_q0_q1 : 
   ∀alpha:FinSet.∀sep,a,ls,a0,rs.
   a0 == sep = false → 
   step alpha (mcl_step alpha sep)
@@ -145,12 +145,13 @@ lemma sem_mcl_step :
   | @(ex_intro ?? 4) cases rt
     [ @ex_intro
       [|% [ %
-            [ >loop_S_false // >mcc_q0_q1 //
+            [ >loop_S_false // >mcl_q0_q1 //
             | normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
           | normalize in ⊢ (%→?); #_ #H1 @False_ind @(absurd ?? H1) % ] ]
-    | #r0 #rt0 @ex_intro
+ 
+   | #r0 #rt0 @ex_intro
       [| % [ %
-             [ >loop_S_false // >mcc_q0_q1 //
+             [ >loop_S_false // >mcl_q0_q1 //
              | #_ #a #b #ls #rs #Hb destruct (Hb) % 
                [ @(\Pf Hc)
                | >mcl_q1_q2 >mcl_q2_q3 cases ls normalize // ] ]