X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Funiversal%2Funiversal.ma;h=20e35ca3ffb18096222d7459d362d75206d7be34;hb=dae251c38e392d180110a5e3d93522333747296c;hp=2b8618213bbd673e160fc57b076bcd08d54f6d59;hpb=c31d09808ffd3866e984c009eb8fc6930fa5e7dc;p=helm.git

diff --git a/matita/matita/lib/turing/universal/universal.ma b/matita/matita/lib/turing/universal/universal.ma
index 2b8618213..20e35ca3f 100644
--- a/matita/matita/lib/turing/universal/universal.ma
+++ b/matita/matita/lib/turing/universal/universal.ma
@@ -337,14 +337,17 @@ definition low_R ≝ λM,qstart,R,t1,t2.
 
 lemma sem_uni_step1: 
   uni_step ⊨ [us_acc: low_step_R_true, low_step_R_false].
+@daemon (* this no longer works: TODO *) (*
 @(acc_Realize_to_acc_Realize … sem_uni_step) 
   [@unistep_true_to_low_step | @unistep_false_to_low_step ]
+*)
 qed. 
 
 definition universalTM ≝ whileTM ? uni_step us_acc.
 
 theorem sem_universal: ∀M:normalTM. ∀qstart.
   universalTM ⊫ (low_R M qstart (R_TM FinBool M qstart)).
+@daemon (* this no longer works: TODO *) (*
 #M #q #intape #i #outc #Hloop
 lapply (sem_while … sem_uni_step1 intape i outc Hloop)
   [@daemon] -Hloop 
@@ -379,6 +382,7 @@ lapply (sem_while … sem_uni_step1 intape i outc Hloop)
     |@Houtc
     ]
   ]
+*)  
 qed.
 
 theorem sem_universal2: ∀M:normalTM. ∀R.