X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fmono.ma;h=748f08612442cc6e8aa5a240b2037f14e20e51c7;hb=fc803c84d8d99e1bf1f5f655312e120dcd87d90e;hp=1508c6c9eaf8a28580463d023c6155c53ab84e37;hpb=00101d30f0bf914a26ed2ec61a1aa38598b05209;p=helm.git

diff --git a/matita/matita/lib/turing/mono.ma b/matita/matita/lib/turing/mono.ma
index 1508c6c9e..748f08612 100644
--- a/matita/matita/lib/turing/mono.ma
+++ b/matita/matita/lib/turing/mono.ma
@@ -47,6 +47,21 @@ definition mk_tape :
       | cons r0 rs0 ⇒ leftof ? r0 rs0 ]
     | cons l0 ls0 ⇒ rightof ? l0 ls0 ] ].
 
+lemma right_mk_tape : 
+  ∀sig,ls,c,rs.(c = None ? → ls = [ ] ∨ rs = [ ]) → right ? (mk_tape sig ls c rs) = rs.
+#sig #ls #c #rs cases c // cases ls 
+[ cases rs // 
+| #l0 #ls0 #H normalize cases (H (refl ??)) #H1 [ destruct (H1) | >H1 % ] ]
+qed-.
+
+lemma left_mk_tape : ∀sig,ls,c,rs.left ? (mk_tape sig ls c rs) = ls.
+#sig #ls #c #rs cases c // cases ls // cases rs //
+qed.
+
+lemma current_mk_tape : ∀sig,ls,c,rs.current ? (mk_tape sig ls c rs) = c.
+#sig #ls #c #rs cases c // cases ls // cases rs //
+qed.
+
 lemma current_to_midtape: ∀sig,t,c. current sig t = Some ? c →
   ∃ls,rs. t = midtape ? ls c rs.
 #sig *