X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Fcounters%2Frtc_shift.ma;h=46856cc98bf72995a73ea1d084920eb1e8412cf1;hb=632dfd0a57c9951d0efbd769d6f433c4ef68a314;hp=b2f1ed005227eaa089d51a9d57370ba7ea57e95c;hpb=dbc57c92512c04b3fd88f8289bb8dbe99b2f90e0;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/counters/rtc_shift.ma b/matita/matita/contribs/lambdadelta/ground/counters/rtc_shift.ma
index b2f1ed005..46856cc98 100644
--- a/matita/matita/contribs/lambdadelta/ground/counters/rtc_shift.ma
+++ b/matita/matita/contribs/lambdadelta/ground/counters/rtc_shift.ma
@@ -25,12 +25,13 @@ match c with
 ].
 
 interpretation
-  "shift (rtc)"
+  "shift (rt-transition counters)"
   'UpDownArrowStar c = (rtc_shift c).
 
 (* Basic constructions ******************************************************)
 
-lemma rtc_shift_rew (ri) (rs) (ti) (ts):
+(*** rtc_shift_rew *)
+lemma rtc_shift_unfold (ri) (rs) (ti) (ts):
       〈ri ∨ rs, 𝟎, ti ∨ ts, 𝟎〉 = ↕*〈ri,rs,ti,ts〉.
 //
 qed.
@@ -44,6 +45,6 @@ lemma rtc_shift_inv_dx (ri) (rs) (ti) (ts) (c):
       〈ri,rs,ti,ts〉 = ↕*c →
       ∃∃ri0,rs0,ti0,ts0.
       (ri0∨rs0) = ri & 𝟎 = rs & (ti0∨ts0) = ti & 𝟎 = ts & 〈ri0,rs0,ti0,ts0〉 = c.
-#ri #rs #ti #ts * #ri0 #rs0 #ti0 #ts0 <rtc_shift_rew #H destruct
+#ri #rs #ti #ts * #ri0 #rs0 #ti0 #ts0 <rtc_shift_unfold #H destruct
 /2 width=7 by ex5_4_intro/
 qed-.