progress

[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 43f99d64441ef461825fed34bb9e588527e9e45e..4be6e129f3a7f5f37d4c41312a040093f7a88780 100644 (file)
--- a/matita/matita/lib/turing/multi_universal/unistep_aux.ma
+++ b/matita/matita/lib/turing/multi_universal/unistep_aux.ma
@@ -280,5 +280,7 @@ definition tape_move_obj : mTM FSUnialpha 2 ≝
    tc_true.
 
 definition unistep ≝ 
-  obj_to_cfg · match_m cfg prg FSUnialpha 2 · copy prg cfg FSUnialpha 2 ·
-   cfg_to_obj · tape_move_obj.
\ No newline at end of file
+  obj_to_cfg · match_m cfg prg FSUnialpha 2 · 
+  inject_TM ? (move_to_end FSUnialpha L) 2 cfg ·
+  mmove cfg FSUnialpha 2 R · copy prg cfg FSUnialpha 2 ·
+  cfg_to_obj · tape_move_obj.
\ No newline at end of file