X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Funiversal%2Funiversal.ma;h=2b8618213bbd673e160fc57b076bcd08d54f6d59;hb=4d5f398cd2818b9eee57d6efdbb49a51d4a97a76;hp=3ed3015bec83c38932ce359c20faa37218c31815;hpb=31cb2f0b374657eb5acb95708443e2c1b8481891;p=helm.git

diff --git a/matita/matita/lib/turing/universal/universal.ma b/matita/matita/lib/turing/universal/universal.ma
index 3ed3015be..2b8618213 100644
--- a/matita/matita/lib/turing/universal/universal.ma
+++ b/matita/matita/lib/turing/universal/universal.ma
@@ -344,7 +344,7 @@ qed.
 definition universalTM ≝ whileTM ? uni_step us_acc.
 
 theorem sem_universal: ∀M:normalTM. ∀qstart.
-  WRealize ? universalTM (low_R M qstart (R_TM FinBool M qstart)).
+  universalTM ⊫ (low_R M qstart (R_TM FinBool M qstart)).
 #M #q #intape #i #outc #Hloop
 lapply (sem_while … sem_uni_step1 intape i outc Hloop)
   [@daemon] -Hloop 
@@ -371,7 +371,7 @@ lapply (sem_while … sem_uni_step1 intape i outc Hloop)
     [%
       [cases HRTM #k * #outc1 * #Hloop #Houtc1
        @(ex_intro … (S k)) @(ex_intro … outc1) % 
-        [>loop_S_false [2://] whd in match (step FinBool ??); 
+        [>loopM_unfold >loop_S_false [2://] whd in match (step FinBool ??); 
          >(eq_pair_fst_snd ?? (trans ???)) @Hloop
         |@Houtc1
         ]
@@ -382,10 +382,13 @@ lapply (sem_while … sem_uni_step1 intape i outc Hloop)
 qed.
 
 theorem sem_universal2: ∀M:normalTM. ∀R.
-  WRealize ? M R → WRealize ? universalTM (low_R M (start ? M) R).
+  M ⊫ R → universalTM ⊫ (low_R M (start ? M) R).
 #M #R #HMR lapply (sem_universal … M (start ? M)) @WRealize_to_WRealize
 #t1 #t2 whd in ⊢ (%→%); #H #tape1 #Htape1 cases (H ? Htape1)
 #q * #tape2 * * #HRTM #Hhalt #Ht2 @(ex_intro … q) @(ex_intro … tape2)
 % [% [@(R_TM_to_R … HRTM) @HMR | //] | //]
 qed.
  
+axiom terminate_UTM: ∀M:normalTM.∀t. 
+  M ↓ t → universalTM ↓ (low_config M (mk_config ?? (start ? M) t)).
+