X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fif_machine.ma;h=3d6675d02b5dd4087affdaaf58901935d28c3ceb;hb=c62c83d3be87bfb0744902a5998e5708bc698cd7;hp=03d49d4b6a750836908e9d3ad70f3f0afb851ff7;hpb=35e0d9c8c27601b93413f4e9cbf1558404f24a41;p=helm.git

diff --git a/matita/matita/lib/turing/if_machine.ma b/matita/matita/lib/turing/if_machine.ma
index 03d49d4b6..3d6675d02 100644
--- a/matita/matita/lib/turing/if_machine.ma
+++ b/matita/matita/lib/turing/if_machine.ma
@@ -77,7 +77,7 @@ axiom acc_sem_if: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,acc.
   accRealize sig M1 acc Rtrue Rfalse → Realize sig M2 R2 → Realize sig M3 R3 → 
     accRealize sig 
      (ifTM sig M1 (single_finalTM … M2) M3 acc) 
-     (inr … (inl … (inr … 0)))
+     (inr … (inl … (inr … start_nop)))
      (Rtrue ∘ R2) 
      (Rfalse ∘ R3).
      
@@ -87,7 +87,7 @@ lemma acc_sem_if_app: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,R4,R5,acc.
     (∀t1,t2,t3. Rfalse t1 t3 → R3 t3 t2 → R5 t1 t2) → 
     accRealize sig 
      (ifTM sig M1 (single_finalTM … M2) M3 acc) 
-     (inr … (inl … (inr … 0)))
+     (inr … (inl … (inr … start_nop)))
      R4 R5.    
 #sig #M1 #M2 #M3 #Rtrue #Rfalse #R2 #R3 #R4 #R5 #acc
 #HRacc #HRtrue #HRfalse #Hsub1 #Hsub2