update in ground static_2 basic_2 apps_2

[helm.git] / matita / matita / contribs / lambdadelta / ground / counters / rtc_ism.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/counters/rtc_ism.ma b/matita/matita/contribs/lambdadelta/ground/counters/rtc_ism.ma
index 3b8cbfe9c7c8485ca0ae179b29d6ee4f230c21a2..af50363fead4bf1f2b55b1c62c8ce0c6ba0471c4 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/counters/rtc_ism.ma
+++ b/matita/matita/contribs/lambdadelta/ground/counters/rtc_ism.ma
@@ -26,40 +26,40 @@ interpretation
 
 (* Basic constructions ******************************************************)
 
-lemma rtc_ism_zz: ð\9d\90\8câ\9dªð\9d\9f\8e,ð\9d\9f\98ð\9d\9f\98â\9d«.
+lemma rtc_ism_zz: ð\9d\90\8câ\9d¨ð\9d\9f\8e,ð\9d\9f\98ð\9d\9f\98â\9d©.
 /2 width=3 by ex1_2_intro/ qed.
 
-lemma rtc_ism_zu: ð\9d\90\8câ\9dªð\9d\9f\8e,ð\9d\9f\99ð\9d\9f\98â\9d«.
+lemma rtc_ism_zu: ð\9d\90\8câ\9d¨ð\9d\9f\8e,ð\9d\9f\99ð\9d\9f\98â\9d©.
 /2 width=3 by ex1_2_intro/ qed.
 
-lemma rtc_ism_uz: ð\9d\90\8câ\9dªð\9d\9f\8f,ð\9d\9f\98ð\9d\9f\99â\9d«.
+lemma rtc_ism_uz: ð\9d\90\8câ\9d¨ð\9d\9f\8f,ð\9d\9f\98ð\9d\9f\99â\9d©.
 /2 width=3 by ex1_2_intro/ qed.
 
-lemma rtc_ism_eq_t_trans (n) (c1) (c2): ð\9d\90\8câ\9dªn,c1â\9d« â\86\92 rtc_eq_t c1 c2 â\86\92 ð\9d\90\8câ\9dªn,c2â\9d«.
+lemma rtc_ism_eq_t_trans (n) (c1) (c2): ð\9d\90\8câ\9d¨n,c1â\9d© â\86\92 rtc_eq_t c1 c2 â\86\92 ð\9d\90\8câ\9d¨n,c2â\9d©.
 #n #c1 #c2 * #ri1 #rs1 #H destruct
 #H elim (rtc_eq_t_inv_dx … H) -H /2 width=3 by ex1_2_intro/
 qed-.
 
 (* Basic destructions *******************************************************)
 
-lemma rtc_ism_des_zz (n): ð\9d\90\8câ\9dªn,ð\9d\9f\98ð\9d\9f\98â\9d« → 𝟎 = n.
+lemma rtc_ism_des_zz (n): ð\9d\90\8câ\9d¨n,ð\9d\9f\98ð\9d\9f\98â\9d© → 𝟎 = n.
 #n * #ri #rs #H destruct //
 qed-.
 
-lemma rtc_ism_des_uz (n): ð\9d\90\8câ\9dªn,ð\9d\9f\99ð\9d\9f\98â\9d« → 𝟎 = n.
+lemma rtc_ism_des_uz (n): ð\9d\90\8câ\9d¨n,ð\9d\9f\99ð\9d\9f\98â\9d© → 𝟎 = n.
 #n * #ri #rs #H destruct //
 qed-.
 
-lemma rtc_ism_des_01 (n): ð\9d\90\8câ\9dªn,ð\9d\9f\98ð\9d\9f\99â\9d« → ninj (𝟏) = n.
+lemma rtc_ism_des_01 (n): ð\9d\90\8câ\9d¨n,ð\9d\9f\98ð\9d\9f\99â\9d© → ninj (𝟏) = n.
 #n * #ri #rs #H destruct //
 qed-.
 
 (* Main inversions **********************************************************)
 
-theorem rtc_ism_inj (n1) (n2) (c): ð\9d\90\8câ\9dªn1,câ\9d« â\86\92 ð\9d\90\8câ\9dªn2,câ\9d« → n1 = n2.
+theorem rtc_ism_inj (n1) (n2) (c): ð\9d\90\8câ\9d¨n1,câ\9d© â\86\92 ð\9d\90\8câ\9d¨n2,câ\9d© → n1 = n2.
 #n1 #n2 #c * #ri1 #rs1 #H1 * #ri2 #rs2 #H2 destruct //
 qed-.
 
-theorem rtc_ism_mono (n) (c1) (c2): ð\9d\90\8câ\9dªn,c1â\9d« â\86\92 ð\9d\90\8câ\9dªn,c2â\9d« → rtc_eq_t c1 c2.
+theorem rtc_ism_mono (n) (c1) (c2): ð\9d\90\8câ\9d¨n,c1â\9d© â\86\92 ð\9d\90\8câ\9d¨n,c2â\9d© → rtc_eq_t c1 c2.
 #n #c1 #c2 * #ri1 #rs1 #H1 * #ri2 #rs2 #H2 destruct //
 qed-.