update in ground static_2 basic_2 apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/ground/counters/rtc_ism_max_shift.ma b/matita/matita/contribs/lambdadelta/ground/counters/rtc_ism_max_shift.ma
index 8d9a4508a5d630a8cc7098519c3da753fa78622a..c8d491369090c2430e967094801cdba622ae0b8a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/counters/rtc_ism_max_shift.ma
+++ b/matita/matita/contribs/lambdadelta/ground/counters/rtc_ism_max_shift.ma
@@ -19,8 +19,8 @@ include "ground/counters/rtc_ism_max.ma".
 
 (* Inversions with rtc_max and rtc_shift ************************************)
 
-lemma rtc_ism_inv_max_shift_sn (n) (c1) (c2): ð\9d\90\8câ\9dªn,â\86\95*c1 â\88¨ c2â\9d« →
-      â\88§â\88§ ð\9d\90\8câ\9dªð\9d\9f\8e,c1â\9d« & ð\9d\90\8câ\9dªn,c2â\9d«.
+lemma rtc_ism_inv_max_shift_sn (n) (c1) (c2): ð\9d\90\8câ\9d¨n,â\86\95*c1 â\88¨ c2â\9d© →
+      â\88§â\88§ ð\9d\90\8câ\9d¨ð\9d\9f\8e,c1â\9d© & ð\9d\90\8câ\9d¨n,c2â\9d©.
 #n #c1 #c2 #H
 elim (rtc_ism_inv_max … H) -H #n1 #n2 #Hc1 #Hc2 #H destruct
 elim (rtc_ism_inv_shift … Hc1) -Hc1 #Hc1 * -n1 <nmax_zero_sn