X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Fsteps%2Frtc_shift.ma;h=f7c56a3e1f50438a7734b09959d12295237626b7;hb=f6b452b9c9be141740d4058dfbcf81a4b75fd00b;hp=a2746366cc458cf0f925767862f12d510a507fa1;hpb=88dd0e28758c693660a93ee0a9a5202c61ca09a0;p=helm.git

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 a2746366c..f7c56a3e1 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_shift.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_shift.ma
@@ -13,18 +13,48 @@
 (**************************************************************************)
 
 include "ground_2/notation/functions/drop_1.ma".
-include "ground_2/steps/rtc.ma".
+include "ground_2/steps/rtc_isrt.ma".
 
 (* RT-TRANSITION COUNTER ****************************************************)
 
-definition shift (r:rtc): rtc ≝ match r with
-[ mk_rtc ri rh ti th ⇒ 〈ri+rh, 0, ti+th, 0〉 ].
+definition shift (c:rtc): rtc ≝ match c with
+[ mk_rtc ri rs ti ts ⇒ 〈ri+rs, 0, ti+ts, 0〉 ].
 
 interpretation "shift (rtc)"
-   'Drop r = (shift r).
+   'Drop c = (shift c).
 
 (* Basic properties *********************************************************)
 
-lemma shift_refl: ∀ri,ti. 〈ri, 0, ti, 0〉 = ↓〈ri, 0, ti, 0〉.
+lemma shift_rew: ∀ri,rs,ti,ts. 〈ri+rs, 0, ti+ts, 0〉 = ↓〈ri, rs, ti, ts〉.
 normalize //
 qed.
+
+lemma shift_O: 𝟘𝟘 = ↓𝟘𝟘.
+// qed.
+
+(* Basic inversion properties ***********************************************)
+
+lemma shift_inv_dx: ∀ri,rs,ti,ts,c. 〈ri, rs, ti, ts〉 = ↓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
+/2 width=7 by ex5_4_intro/
+qed-.
+
+(* Properties with test for costrained rt-transition counter ****************)
+
+lemma isr_shift: ∀c. 𝐑𝐓⦃0, c⦄ → 𝐑𝐓⦃0, ↓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: ∀n,c. 𝐑𝐓⦃n, ↓c⦄ → 𝐑𝐓⦃0, c⦄ ∧ 0 = n.
+#n #c * #ri #rs #H
+elim (shift_inv_dx … H) -H #rt0 #rs0 #ti0 #ts0 #_ #_ #H1 #H2 #H3
+elim (plus_inv_O3 … H1) -H1 /3 width=3 by ex1_2_intro, conj/
+qed-.
+
+lemma isr_inv_shift: ∀c. 𝐑𝐓⦃0, ↓c⦄ → 𝐑𝐓⦃0, c⦄.
+#c #H elim (isrt_inv_shift … H) -H //
+qed-.