Porting to the new defintion of finset

[helm.git] / matita / matita / lib / turing / if_machine.ma

diff --git a/matita/matita/lib/turing/if_machine.ma b/matita/matita/lib/turing/if_machine.ma
index 03d49d4b6a750836908e9d3ad70f3f0afb851ff7..3d6675d02b5dd4087affdaaf58901935d28c3ceb 100644 (file)
--- 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