milestone update in ground

[helm.git] / matita / matita / contribs / lambdadelta / ground / counters / rtc_max.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/counters/rtc_max.ma b/matita/matita/contribs/lambdadelta/ground/counters/rtc_max.ma
index 10fbce4efe1848cf73b8d4f88070cd24bc99d1dd..d38f016bf42e8f2995536f97f0e533668f97e8ef 100644 (file)
--- 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.