X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Fsteps%2Frtc_plus.ma;h=24b261949a4065a2d114d8c2442cd8d75525b99e;hb=1fd63df4c77f5c24024769432ea8492748b4ac79;hp=41f0e8a273e59ffc1875150bcb2311110cb1649c;hpb=c3904c007394068ed823575e3be3d73a9ad92cce;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_plus.ma b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_plus.ma
index 41f0e8a27..24b261949 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_plus.ma
@@ -12,25 +12,45 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground_2/xoa/ex_6_8.ma".
 include "ground_2/steps/rtc.ma".
 
 (* RT-TRANSITION COUNTER ****************************************************)
 
-definition plus (r1:rtc) (r2:rtc): rtc ≝ match r1 with [
-   mk_rtc ri1 rh1 ti1 th1 ⇒ match r2 with [
-      mk_rtc ri2 rh2 ti2 th2 ⇒ 〈ri1+ri2, rh1+rh2, ti1+ti2, th1+th2〉
+definition plus (c1:rtc) (c2:rtc): rtc ≝ match c1 with [
+   mk_rtc ri1 rs1 ti1 ts1 ⇒ match c2 with [
+      mk_rtc ri2 rs2 ti2 ts2 ⇒ 〈ri1+ri2,rs1+rs2,ti1+ti2,ts1+ts2〉
    ]
 ].
 
 interpretation "plus (rtc)"
-   'plus r1 r2 = (plus r1 r2).
+   'plus c1 c2 = (plus c1 c2).
 
 (* Basic properties *********************************************************)
 
-lemma plus_OO_r: ∀r. r = 𝟘𝟘 + r.
-* normalize //
+(**) (* plus is not disambiguated parentheses *)
+lemma plus_rew: ∀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 plus_O_dx: ∀c. c = c + 𝟘𝟘.
+* #ri #rs #ti #ts <plus_rew //
 qed.
 
-lemma plus_r_OO: ∀r. r = r + 𝟘𝟘.
-* normalize //
+(* Basic inversion properties ***********************************************)
+
+lemma plus_inv_dx: ∀ri,rs,ti,ts,c1,c2. 〈ri,rs,ti,ts〉 = c1 + c2 →
+                   ∃∃ri1,rs1,ti1,ts1,ri2,rs2,ti2,ts2.
+                   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
+<plus_rew #H destruct /2 width=14 by ex6_8_intro/
+qed-.
+
+(* Main Properties **********************************************************)
+
+theorem plus_assoc: associative … plus.
+* #ri1 #rs1 #ti1 #ts1 * #ri2 #rs2 #ti2 #ts2 * #ri3 #rs3 #ti3 #ts3
+<plus_rew //
 qed.