X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Fcounters%2Frtc_max.ma;h=d38f016bf42e8f2995536f97f0e533668f97e8ef;hb=55c768d7e45babb300b5010463ba3196a68f1bbe;hp=10fbce4efe1848cf73b8d4f88070cd24bc99d1dd;hpb=15212e44902f25536f6e2de4bec4cedcd9a9804d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/counters/rtc_max.ma b/matita/matita/contribs/lambdadelta/ground/counters/rtc_max.ma
index 10fbce4ef..d38f016bf 100644
--- a/matita/matita/contribs/lambdadelta/ground/counters/rtc_max.ma
+++ b/matita/matita/contribs/lambdadelta/ground/counters/rtc_max.ma
@@ -27,22 +27,23 @@ match c1 with
 ].
 
 interpretation
-  "maximum (rtc)"
+  "maximum (rt-transition counters)"
   'or c1 c2 = (rtc_max c1 c2).
 
 (* Basic constructions ******************************************************)
 
-lemma rtc_max_rew (ri1) (ri2) (rs1) (rs2) (ti1) (ti2) (ts1) (ts2):
+(*** rtc_max_rew *)
+lemma rtc_max_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_max_zz_dx (c): c = (c ∨ 𝟘𝟘).
-* #ri #rs #ti #ts <rtc_max_rew //
+* #ri #rs #ti #ts <rtc_max_unfold //
 qed.
 
 lemma rtc_max_idem (c): c = (c ∨ c).
-* #ri #rs #ti #ts <rtc_max_rew //
+* #ri #rs #ti #ts <rtc_max_unfold //
 qed.
 
 (* Basic inversions *********************************************************)
@@ -53,12 +54,12 @@ lemma rtc_max_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_max_rew #H destruct /2 width=14 by ex6_8_intro/
+<rtc_max_unfold #H destruct /2 width=14 by ex6_8_intro/
 qed-.
 
 (* Main constructions *******************************************************)
 
 theorem rtc_max_assoc: associative … rtc_max.
 * #ri1 #rs1 #ti1 #ts1 * #ri2 #rs2 #ti2 #ts2 * #ri3 #rs3 #ti3 #ts3
-<rtc_max_rew <rtc_max_rew //
+<rtc_max_unfold <rtc_max_unfold //
 qed.