X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fmulti_universal%2Funistep_aux.ma;fp=matita%2Fmatita%2Flib%2Fturing%2Fmulti_universal%2Funistep_aux.ma;h=7a8062ee34c198ae2726f16b54b16cdec9ff2e58;hb=f4047107dfd976f173151174269f356b1f431ab7;hp=86f4427837a431b0e013beb209ac4f0bf499cbbc;hpb=b2e4273cdfa45add6110a81626dcb3e25928a0d4;p=helm.git

diff --git a/matita/matita/lib/turing/multi_universal/unistep_aux.ma b/matita/matita/lib/turing/multi_universal/unistep_aux.ma
index 86f442783..7a8062ee3 100644
--- a/matita/matita/lib/turing/multi_universal/unistep_aux.ma
+++ b/matita/matita/lib/turing/multi_universal/unistep_aux.ma
@@ -329,9 +329,18 @@ definition R_unistep ≝ λn,l,h.λt1,t2: Vector ? 3.
       change_vec ??
         (change_vec ?? t1 (midtape ? [ ] bar (nstate@[nchar])) cfg)
         (tape_move_mono ? (nth obj ? t1 (niltape ?)) 〈Some ? nchar,char_to_move m〉) obj.
-    
-  
+
+definition tape_map ≝ λA,B:FinSet.λf:A→B.λt.
+  mk_tape B (map ?? f (left ? t)) 
+    (option_map ?? f (current ? t)) 
+    (map ?? f (right ? t)).
+
+definition low ≝ λM:normalTM.λc:nconfig (no_states M).Vector_of_list ?
+  [tape_map ?? bit (ctape ?? c);
+   midtape ? [ ] bar (bits_of_state ? (nhalt M) (cstate ?? c));
+   ?].
+
   
   
   
-  
\ No newline at end of file
+  .
\ No newline at end of file