X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fmono.ma;h=1508c6c9eaf8a28580463d023c6155c53ab84e37;hb=be80aa40b9a66d5b12f92d03c2aa7b1dd8e49893;hp=39ecff800e79b11143e0db2d901a8112beaf4d65;hpb=77bf99a9ac05a61573d621d576e269870668f076;p=helm.git

diff --git a/matita/matita/lib/turing/mono.ma b/matita/matita/lib/turing/mono.ma
index 39ecff800..1508c6c9e 100644
--- a/matita/matita/lib/turing/mono.ma
+++ b/matita/matita/lib/turing/mono.ma
@@ -109,6 +109,10 @@ definition tape_move ≝ λsig.λt: tape sig.λm:move.
     | N ⇒ t
     ].
 
+definition tape_move_mono ≝ 
+  λsig,t,mv.
+  tape_move sig (tape_write sig t (\fst mv)) (\snd mv).
+
 record config (sig,states:FinSet): Type[0] ≝ 
 { cstate : states;
   ctape: tape sig
@@ -130,6 +134,16 @@ definition step ≝ λsig.λM:TM sig.λc:config sig (states sig M).
   let 〈news,a,mv〉 ≝ trans sig M 〈cstate ?? c,current_char〉 in
   mk_config ?? news (tape_move sig (tape_write ? (ctape ?? c) a) mv).
 
+(*
+lemma step_eq : ∀sig,M,c. 
+  let current_char ≝ current ? (ctape ?? c) in
+  let 〈news,a,mv〉 ≝ trans sig M 〈cstate ?? c,current_char〉 in
+  step sig M c = 
+    mk_config ?? news (tape_move sig (tape_write ? (ctape ?? c) a) mv).
+#sig #M #c  
+ whd in match (tape_move_mono sig ??);
+*)
+  
 (******************************** loop ****************************************)
 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
   match n with