X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fif_machine.ma;h=6248ab7e7cfabcd0ae366162ff9268c272791e8a;hb=bd5d6160029247d8c4e3f8cec82f7acd7199d7d5;hp=2bc83c2616958d7de60924e740d35723d3ecb831;hpb=e37238b40356ee1b5e7859cf0eb6567918f2ebec;p=helm.git

diff --git a/matita/matita/lib/turing/if_machine.ma b/matita/matita/lib/turing/if_machine.ma
index 2bc83c261..6248ab7e7 100644
--- a/matita/matita/lib/turing/if_machine.ma
+++ b/matita/matita/lib/turing/if_machine.ma
@@ -152,7 +152,7 @@ qed.
 
 (******************************** semantics ***********************************)
 lemma sem_if: ∀sig.∀M1,M2,M3:TM sig.∀Rtrue,Rfalse,R2,R3,acc.
-  M1 ⊧ [acc: Rtrue,Rfalse] → M2 ⊨ R2 → M3 ⊨ R3 → 
+  M1 ⊨ [acc: Rtrue,Rfalse] → M2 ⊨ R2 → M3 ⊨ R3 → 
     ifTM sig M1 M2 M3 acc ⊨ (Rtrue ∘ R2) ∪ (Rfalse ∘ R3).
 #sig #M1 #M2 #M3 #Rtrue #Rfalse #R2 #R3 #acc #HaccR #HR2 #HR3 #t 
 cases (HaccR t) #k1 * #outc1 * * #Hloop1 #HMtrue #HMfalse