high level semantics

[helm.git] / matita / matita / lib / turing / multi_universal / unistep_aux.ma

diff --git a/matita/matita/lib/turing/multi_universal/unistep_aux.ma b/matita/matita/lib/turing/multi_universal/unistep_aux.ma
index 7a8062ee34c198ae2726f16b54b16cdec9ff2e58..aa4dbc7ab6a86387ee0a98c85b495f4441f7a9af 100644 (file)
--- a/matita/matita/lib/turing/multi_universal/unistep_aux.ma
+++ b/matita/matita/lib/turing/multi_universal/unistep_aux.ma
@@ -338,9 +338,10 @@ definition tape_map ≝ λA,B:FinSet.λf:A→B.λ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));
-   ?].
+   midtape ? [ ] bar (table_TM ? (graph_enum ?? (ntrans M)) (nhalt M))
+  ].
 
   
   
   
-  .
\ No newline at end of file
+ 
\ No newline at end of file