From: Wilmer Ricciotti Date: Thu, 17 Jan 2013 16:01:27 +0000 (+0000) Subject: progress X-Git-Tag: make_still_working~1332 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fb2e8dec0355fff87420b587dd091a372f1f7b7c;p=helm.git progress --- diff --git a/matita/matita/lib/turing/multi_universal/unistep_aux.ma b/matita/matita/lib/turing/multi_universal/unistep_aux.ma index 43f99d644..4be6e129f 100644 --- 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