Yippeee! Completes proof of soundness of the universal machine

[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 f90e3af59a883e6a6eda2a733e25753ec5cde6b1..c4a5dd128296ed66ade25b630e40ea637dc35fb4 100644 (file)
--- a/matita/matita/lib/turing/multi_universal/unistep_aux.ma
+++ b/matita/matita/lib/turing/multi_universal/unistep_aux.ma
@@ -39,9 +39,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.