notational update in ground_2 and basic_2

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / steps / rtc_shift.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_shift.ma b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_shift.ma
index cb2c3828425b9902209891b7148d79899c5f6b0e..e2f739d69572e6405257b51420dcff6dd05674d9 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_shift.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_shift.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/notation/functions/drop_1.ma".
+include "ground_2/notation/functions/updownarrowstar_1.ma".
 include "ground_2/steps/rtc_isrt.ma".
 
 (* RT-TRANSITION COUNTER ****************************************************)
@@ -21,20 +21,20 @@ definition shift (c:rtc): rtc ≝ match c with
 [ mk_rtc ri rs ti ts ⇒ 〈ri∨rs, 0, ti∨ts, 0〉 ].
 
 interpretation "shift (rtc)"
-   'Drop c = (shift c).
+   'UpDownArrowStar c = (shift c).
 
 (* Basic properties *********************************************************)
 
-lemma shift_rew: â\88\80ri,rs,ti,ts. â\8c©riâ\88¨rs, 0, tiâ\88¨ts, 0â\8cª = â\86\93〈ri, rs, ti, ts〉.
+lemma shift_rew: â\88\80ri,rs,ti,ts. â\8c©riâ\88¨rs, 0, tiâ\88¨ts, 0â\8cª = â\86\95*〈ri, rs, ti, ts〉.
 normalize //
 qed.
 
-lemma shift_O: ð\9d\9f\98ð\9d\9f\98 = â\86\93𝟘𝟘.
+lemma shift_O: ð\9d\9f\98ð\9d\9f\98 = â\86\95*𝟘𝟘.
 // qed.
 
 (* Basic inversion properties ***********************************************)
 
-lemma shift_inv_dx: â\88\80ri,rs,ti,ts,c. â\8c©ri, rs, ti, tsâ\8cª = â\86\93c →
+lemma shift_inv_dx: â\88\80ri,rs,ti,ts,c. â\8c©ri, rs, ti, tsâ\8cª = â\86\95*c →
                     ∃∃ri0,rs0,ti0,ts0. (ri0∨rs0) = ri & 0 = rs & (ti0∨ts0) = ti & 0 = ts &
                                        〈ri0, rs0, ti0, ts0〉 = c.
 #ri #rs #ti #ts * #ri0 #rs0 #ti0 #ts0 <shift_rew #H destruct
@@ -43,18 +43,18 @@ qed-.
 
 (* Properties with test for costrained rt-transition counter ****************)
 
-lemma isr_shift: â\88\80c. ð\9d\90\91ð\9d\90\93â¦\830, câ¦\84 â\86\92 ð\9d\90\91ð\9d\90\93â¦\830, â\86\93c⦄.
+lemma isr_shift: â\88\80c. ð\9d\90\91ð\9d\90\93â¦\830, câ¦\84 â\86\92 ð\9d\90\91ð\9d\90\93â¦\830, â\86\95*c⦄.
 #c * #ri #rs #H destruct /2 width=3 by ex1_2_intro/
 qed.
 
 (* Inversion properties with test for costrained rt-counter *****************)
 
-lemma isrt_inv_shift: â\88\80n,c. ð\9d\90\91ð\9d\90\93â¦\83n, â\86\93c⦄ → 𝐑𝐓⦃0, c⦄ ∧ 0 = n.
+lemma isrt_inv_shift: â\88\80n,c. ð\9d\90\91ð\9d\90\93â¦\83n, â\86\95*c⦄ → 𝐑𝐓⦃0, c⦄ ∧ 0 = n.
 #n #c * #ri #rs #H
 elim (shift_inv_dx … H) -H #rt0 #rs0 #ti0 #ts0 #_ #_ #H1 #H2 #H3
 elim (max_inv_O3 … H1) -H1 /3 width=3 by ex1_2_intro, conj/
 qed-.
 
-lemma isr_inv_shift: â\88\80c. ð\9d\90\91ð\9d\90\93â¦\830, â\86\93c⦄ → 𝐑𝐓⦃0, c⦄.
+lemma isr_inv_shift: â\88\80c. ð\9d\90\91ð\9d\90\93â¦\830, â\86\95*c⦄ → 𝐑𝐓⦃0, c⦄.
 #c #H elim (isrt_inv_shift … H) -H //
 qed-.