X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Fsteps%2Frtc_shift.ma;h=f5c00d822cbeb29bdf8b820d62273b6c3ff4e9ce;hb=25c634037771dff0138e5e8e3d4378183ff49b86;hp=6cb0a8b1a43c524ef5be0ee210d3fcc90b8e6068;hpb=e31ce850917b3e95f5158a687626c679e551fd25;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 6cb0a8b1a..f5c00d822 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_shift.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_shift.ma
@@ -12,13 +12,32 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/notation/functions/drop_1.ma".
+include "ground_2/xoa/ex_5_4.ma".
+include "ground_2/notation/functions/updownarrowstar_1.ma".
 include "ground_2/steps/rtc.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).
+   'UpDownArrowStar c = (shift c).
+
+(* Basic properties *********************************************************)
+
+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-.