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

diff --git a/matita/matita/contribs/lambdadelta/ground/counters/rtc_plus.ma b/matita/matita/contribs/lambdadelta/ground/counters/rtc_plus.ma
index 9c6d7e795..8ac147c98 100644
--- a/matita/matita/contribs/lambdadelta/ground/counters/rtc_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/counters/rtc_plus.ma
@@ -27,17 +27,18 @@ match c1 with
 ].
 
 interpretation
-  "plus (rtc)"
+  "addition (rt-transition counters)"
   'plus c1 c2 = (rtc_plus c1 c2).
 
 (* Basic constructions ******************************************************)
 
-lemma rtc_plus_rew (ri1) (ri2) (rs1) (rs2) (ti1) (ti2) (ts1) (ts2):
+(*** rtc_plus_rew *)
+lemma rtc_plus_unfold (ri1) (ri2) (rs1) (rs2) (ti1) (ti2) (ts1) (ts2):
       〈ri1+ri2,rs1+rs2,ti1+ti2,ts1+ts2〉 = 〈ri1,rs1,ti1,ts1〉+〈ri2,rs2,ti2,ts2〉.
 // qed.
 
 lemma rtc_plus_zz_dx (c): c = c + 𝟘𝟘.
-* #ri #rs #ti #ts <rtc_plus_rew //
+* #ri #rs #ti #ts <rtc_plus_unfold //
 qed.
 
 (* Basic inversions *********************************************************)
@@ -48,12 +49,12 @@ lemma rtc_plus_inv_dx (ri) (rs) (ti) (ts) (c1) (c2):
       ri1+ri2 = ri & rs1+rs2 = rs & ti1+ti2 = ti & ts1+ts2 = ts &
       〈ri1,rs1,ti1,ts1〉 = c1 & 〈ri2,rs2,ti2,ts2〉 = c2.
 #ri #rs #ti #ts * #ri1 #rs1 #ti1 #ts1 * #ri2 #rs2 #ti2 #ts2
-<rtc_plus_rew #H destruct /2 width=14 by ex6_8_intro/
+<rtc_plus_unfold #H destruct /2 width=14 by ex6_8_intro/
 qed-.
 
 (* Main constructions *******************************************************)
 
 theorem rtc_plus_assoc: associative … rtc_plus.
 * #ri1 #rs1 #ti1 #ts1 * #ri2 #rs2 #ti2 #ts2 * #ri3 #rs3 #ti3 #ts3
-<rtc_plus_rew //
+<rtc_plus_unfold //
 qed.