X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Flib%2Fturing%2Fmulti_universal%2Funistep_aux.ma;h=8033c222627b6123481c324d528aab44652260aa;hb=21de0d35017656c5a55528390b54b0b2ae395b44;hp=f90e3af59a883e6a6eda2a733e25753ec5cde6b1;hpb=3026dfea8eae158433ed13df5156a733fa926794;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 f90e3af59..8033c2226 100644
--- a/matita/matita/lib/turing/multi_universal/unistep_aux.ma
+++ b/matita/matita/lib/turing/multi_universal/unistep_aux.ma
@@ -9,9 +9,8 @@
      \ /   GNU General Public License Version 2   
       V_____________________________________________________________*)
 
-include "turing/multi_universal/moves_2.ma".
-include "turing/multi_universal/match.ma".
-include "turing/multi_universal/copy.ma".
+include "turing/auxiliary_machines.ma".
+include "turing/auxiliary_multi_machines.ma".
 include "turing/multi_universal/alphabet.ma".
 include "turing/multi_universal/tuples.ma".
 
@@ -39,9 +38,11 @@ definition R_obj_to_cfg ≝ λt1,t2:Vector (tape FSUnialpha) 3.
          (mk_tape ? [ ] (option_hd FSUnialpha (reverse ? (null::ls))) 
            (tail ? (reverse ? (null::ls)))) cfg).
 
+(*
 axiom accRealize_to_Realize :
   ∀sig,n.∀M:mTM sig n.∀Rtrue,Rfalse,acc.
   M ⊨ [ acc: Rtrue, Rfalse ] →  M ⊨ Rtrue ∪ Rfalse.
+*)
   
 lemma eq_mk_tape_rightof :
  ∀alpha,a,al.mk_tape alpha (a::al) (None ?) [ ] = rightof ? a al.