high level semantics

diff --git a/matita/matita/lib/basics/vectors.ma b/matita/matita/lib/basics/vectors.ma
index e680e91a7170a48ce231d9c4408f7028f2bbe2e8..a48f04d0fe8dbbfa585262f441fd76a5e78d7c72 100644 (file)
--- a/matita/matita/lib/basics/vectors.ma
+++ b/matita/matita/lib/basics/vectors.ma
@@ -16,6 +16,9 @@ record Vector (A:Type[0]) (n:nat): Type[0] ≝
   len: length ? vec = n
 }.
 
+lemma Vector_of_list ≝ λA,l. 
+  mk_Vector A (|l|) l (refl ??).
+
 lemma Vector_eq : ∀A,n,v1,v2.
   vec A n v1 = vec A n v2 → v1 = v2.
 #A #n * #l1 #H1 * #l2 #H2 #eql1l2 generalize in match H1; 

diff --git a/matita/matita/lib/turing/multi_universal/unistep_aux.ma b/matita/matita/lib/turing/multi_universal/unistep_aux.ma
index 86f4427837a431b0e013beb209ac4f0bf499cbbc..7a8062ee34c198ae2726f16b54b16cdec9ff2e58 100644 (file)
--- 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