dependences update

[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 2bc83c2616958d7de60924e740d35723d3ecb831..6248ab7e7cfabcd0ae366162ff9268c272791e8a 100644 (file)
--- 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 â\8a§ [acc: Rtrue,Rfalse] → M2 ⊨ R2 → M3 ⊨ R3 → 
+  M1 â\8a¨ [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