From 89ea663d91904f483f8248cfaeaed5eda8715da2 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 25 Jul 2016 18:40:47 +0000
Subject: [PATCH] we count rt parallel steps in a different way: we use the
 maximum, that is idempotent, rather than the sum

---
 .../lambdadelta/basic_2/rt_transition/cpg.ma  | 37 ++++++++++---------
 .../basic_2/rt_transition/cpg_simple.ma       |  2 +-
 .../lambdadelta/basic_2/rt_transition/cpm.ma  | 36 +++++++++---------
 .../lambdadelta/ground_2/lib/arith.ma         | 14 +++++++
 .../lambdadelta/ground_2/steps/rtc_max.ma     | 16 ++++++--
 .../lambdadelta/ground_2/steps/rtc_plus.ma    |  9 +----
 .../lambdadelta/ground_2/steps/rtc_shift.ma   |  8 ++--
 .../lambdadelta/ground_2/web/ground_2_src.tbl |  2 +-
 8 files changed, 71 insertions(+), 53 deletions(-)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma
index fd44b81fd..e322f490f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground_2/steps/rtc_max.ma".
 include "ground_2/steps/rtc_plus.ma".
 include "basic_2/notation/relations/predty_6.ma".
 include "basic_2/grammar/lenv.ma".
@@ -33,21 +34,21 @@ inductive cpg (h): rtc → relation4 genv lenv term term ≝
              ⬆*[1] T ≡ U → cpg h c G (L.ⓑ{I}V) (#⫯i) U
 | cpg_bind : ∀cV,cT,p,I,G,L,V1,V2,T1,T2.
              cpg h cV G L V1 V2 → cpg h cT G (L.ⓑ{I}V1) T1 T2 →
-             cpg h ((↓cV)+cT) G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
+             cpg h ((↓cV)∨cT) G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
 | cpg_flat : ∀cV,cT,I,G,L,V1,V2,T1,T2.
              cpg h cV G L V1 V2 → cpg h cT G L T1 T2 →
-             cpg h ((↓cV)+cT) G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
+             cpg h ((↓cV)∨cT) G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
 | cpg_zeta : ∀c,G,L,V,T1,T,T2. cpg h c G (L.ⓓV) T1 T →
              ⬆*[1] T2 ≡ T → cpg h (c+𝟙𝟘) G L (+ⓓV.T1) T2
 | cpg_eps  : ∀c,G,L,V,T1,T2. cpg h c G L T1 T2 → cpg h (c+𝟙𝟘) G L (ⓝV.T1) T2
 | cpg_ee   : ∀c,G,L,V1,V2,T. cpg h c G L V1 V2 → cpg h (c+𝟘𝟙) G L (ⓝV1.T) V2
 | cpg_beta : ∀cV,cW,cT,p,G,L,V1,V2,W1,W2,T1,T2.
              cpg h cV G L V1 V2 → cpg h cW G L W1 W2 → cpg h cT G (L.ⓛW1) T1 T2 →
-             cpg h ((↓cV)+(↓cW)+cT+𝟙𝟘) G L (ⓐV1.ⓛ{p}W1.T1) (ⓓ{p}ⓝW2.V2.T2)
+             cpg h (((↓cV)∨(↓cW)∨cT)+𝟙𝟘) G L (ⓐV1.ⓛ{p}W1.T1) (ⓓ{p}ⓝW2.V2.T2)
 | cpg_theta: ∀cV,cW,cT,p,G,L,V1,V,V2,W1,W2,T1,T2.
              cpg h cV G L V1 V → ⬆*[1] V ≡ V2 → cpg h cW G L W1 W2 →
              cpg h cT G (L.ⓓW1) T1 T2 →
-             cpg h ((↓cV)+(↓cW)+cT+𝟙𝟘) G L (ⓐV1.ⓓ{p}W1.T1) (ⓓ{p}W2.ⓐV2.T2)
+             cpg h (((↓cV)∨(↓cW)∨cT)+𝟙𝟘) G L (ⓐV1.ⓓ{p}W1.T1) (ⓓ{p}W2.ⓐV2.T2)
 .
 
 interpretation
@@ -151,7 +152,7 @@ qed-.
 fact cpg_inv_bind1_aux: ∀c,h,G,L,U,U2. ⦃G, L⦄ ⊢ U ⬈[c, h] U2 →
                         ∀p,J,V1,U1. U = ⓑ{p,J}V1.U1 → (
                         ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L.ⓑ{J}V1⦄ ⊢ U1 ⬈[cT, h] T2 &
-                                       U2 = ⓑ{p,J}V2.T2 & c = (↓cV)+cT
+                                       U2 = ⓑ{p,J}V2.T2 & c = ((↓cV)∨cT)
                         ) ∨
                         ∃∃cT,T. ⦃G, L.ⓓV1⦄ ⊢ U1 ⬈[cT, h] T & ⬆*[1] U2 ≡ T &
                                 p = true & J = Abbr & c = cT+𝟙𝟘.
@@ -173,7 +174,7 @@ qed-.
 
 lemma cpg_inv_bind1: ∀c,h,p,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈[c, h] U2 → (
                      ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬈[cT, h] T2 &
-                                    U2 = ⓑ{p,I}V2.T2 & c = (↓cV)+cT
+                                    U2 = ⓑ{p,I}V2.T2 & c = ((↓cV)∨cT)
                      ) ∨
                      ∃∃cT,T. ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[cT, h] T & ⬆*[1] U2 ≡ T &
                              p = true & I = Abbr & c = cT+𝟙𝟘.
@@ -181,7 +182,7 @@ lemma cpg_inv_bind1: ∀c,h,p,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈[c
 
 lemma cpg_inv_abbr1: ∀c,h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ⬈[c, h] U2 → (
                      ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[cT, h] T2 &
-                                    U2 = ⓓ{p}V2.T2 & c = (↓cV)+cT
+                                    U2 = ⓓ{p}V2.T2 & c = ((↓cV)∨cT)
                      ) ∨
                      ∃∃cT,T. ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[cT, h] T & ⬆*[1] U2 ≡ T &
                              p = true & c = cT+𝟙𝟘.
@@ -191,7 +192,7 @@ qed-.
 
 lemma cpg_inv_abst1: ∀c,h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{p}V1.T1 ⬈[c, h] U2 →
                      ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ⬈[cT, h] T2 &
-                                    U2 = ⓛ{p}V2.T2 & c = (↓cV)+cT.
+                                    U2 = ⓛ{p}V2.T2 & c = ((↓cV)∨cT).
 #c #h #p #G #L #V1 #T1 #U2 #H elim (cpg_inv_bind1 … H) -H * 
 [ /3 width=8 by ex4_4_intro/
 | #c #T #_ #_ #_ #H destruct
@@ -201,13 +202,13 @@ qed-.
 fact cpg_inv_flat1_aux: ∀c,h,G,L,U,U2. ⦃G, L⦄ ⊢ U ⬈[c, h] U2 →
                         ∀J,V1,U1. U = ⓕ{J}V1.U1 →
                         ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[cT, h] T2 &
-                                          U2 = ⓕ{J}V2.T2 & c = (↓cV)+cT
+                                          U2 = ⓕ{J}V2.T2 & c = ((↓cV)∨cT)
                          | ∃∃cT. ⦃G, L⦄ ⊢ U1 ⬈[cT, h] U2 & J = Cast & c = cT+𝟙𝟘
                          | ∃∃cV. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] U2 & J = Cast & c = cV+𝟘𝟙
                          | ∃∃cV,cW,cT,p,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ W1 ⬈[cW, h] W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈[cT, h] T2 &
-                                                        J = Appl & U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = (↓cV)+(↓cW)+cT+𝟙𝟘
+                                                        J = Appl & U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = ((↓cV)∨(↓cW)∨cT)+𝟙𝟘
                          | ∃∃cV,cW,cT,p,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V & ⬆*[1] V ≡ V2 & ⦃G, L⦄ ⊢ W1 ⬈[cW, h] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈[cT, h] T2 &
-                                                          J = Appl & U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = (↓cV)+(↓cW)+cT+𝟙𝟘.
+                                                          J = Appl & U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = ((↓cV)∨(↓cW)∨cT)+𝟙𝟘.
 #c #h #G #L #U #U2 * -c -G -L -U -U2
 [ #I #G #L #J #W #U1 #H destruct
 | #G #L #s #J #W #U1 #H destruct
@@ -226,22 +227,22 @@ qed-.
 
 lemma cpg_inv_flat1: ∀c,h,I,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓕ{I}V1.U1 ⬈[c, h] U2 →
                      ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[cT, h] T2 &
-                                       U2 = ⓕ{I}V2.T2 & c = (↓cV)+cT
+                                       U2 = ⓕ{I}V2.T2 & c = ((↓cV)∨cT)
                       | ∃∃cT. ⦃G, L⦄ ⊢ U1 ⬈[cT, h] U2 & I = Cast & c = cT+𝟙𝟘
                       | ∃∃cV. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] U2 & I = Cast & c = cV+𝟘𝟙
                       | ∃∃cV,cW,cT,p,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ W1 ⬈[cW, h] W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈[cT, h] T2 &
-                                                     I = Appl & U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = (↓cV)+(↓cW)+cT+𝟙𝟘
+                                                     I = Appl & U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = ((↓cV)∨(↓cW)∨cT)+𝟙𝟘
                       | ∃∃cV,cW,cT,p,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V & ⬆*[1] V ≡ V2 & ⦃G, L⦄ ⊢ W1 ⬈[cW, h] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈[cT, h] T2 &
-                                                       I = Appl & U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = (↓cV)+(↓cW)+cT+𝟙𝟘.
+                                                       I = Appl & U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = ((↓cV)∨(↓cW)∨cT)+𝟙𝟘.
 /2 width=3 by cpg_inv_flat1_aux/ qed-.
 
 lemma cpg_inv_appl1: ∀c,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓐV1.U1 ⬈[c, h] U2 →
                      ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[cT, h] T2 &
-                                       U2 = ⓐV2.T2 & c = (↓cV)+cT
+                                       U2 = ⓐV2.T2 & c = ((↓cV)∨cT)
                       | ∃∃cV,cW,cT,p,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ W1 ⬈[cW, h] W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈[cT, h] T2 &
-                                                     U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = (↓cV)+(↓cW)+cT+𝟙𝟘
+                                                     U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = ((↓cV)∨(↓cW)∨cT)+𝟙𝟘
                       | ∃∃cV,cW,cT,p,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V & ⬆*[1] V ≡ V2 & ⦃G, L⦄ ⊢ W1 ⬈[cW, h] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈[cT, h] T2 &
-                                                       U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = (↓cV)+(↓cW)+cT+𝟙𝟘.
+                                                       U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = ((↓cV)∨(↓cW)∨cT)+𝟙𝟘.
 #c #h #G #L #V1 #U1 #U2 #H elim (cpg_inv_flat1 … H) -H *
 [ /3 width=8 by or3_intro0, ex4_4_intro/
 |2,3: #c #_ #H destruct
@@ -252,7 +253,7 @@ qed-.
 
 lemma cpg_inv_cast1: ∀c,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓝV1.U1 ⬈[c, h] U2 →
                      ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[cT, h] T2 &
-                                       U2 = ⓝV2.T2 & c = (↓cV)+cT
+                                       U2 = ⓝV2.T2 & c = ((↓cV)∨cT)
                       | ∃∃cT. ⦃G, L⦄ ⊢ U1 ⬈[cT, h] U2 & c = cT+𝟙𝟘
                       | ∃∃cV. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] U2 & c = cV+𝟘𝟙.
 #c #h #G #L #V1 #U1 #U2 #H elim (cpg_inv_flat1 … H) -H *
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_simple.ma
index a53be69b0..b03705a2e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_simple.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_simple.ma
@@ -22,7 +22,7 @@ include "basic_2/rt_transition/cpg.ma".
 (* Note: the main property of simple terms *)
 lemma cpg_inv_appl1_simple: ∀c,h,G,L,V1,T1,U. ⦃G, L⦄ ⊢ ⓐV1.T1 ⬈[c, h] U → 𝐒⦃T1⦄ →
                             ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ T1 ⬈[cT, h] T2 &
-                                           U = ⓐV2.T2 & c = (↓cV)+cT.
+                                           U = ⓐV2.T2 & c = ((↓cV)∨cT).
 #c #h #G #L #V1 #T1 #U #H #HT1 elim (cpg_inv_appl1 … H) -H *
 [ /2 width=8 by ex4_4_intro/
 | #cV #cW #cT #p #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #H destruct
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma
index 7138b3210..870f93598 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma
@@ -58,7 +58,7 @@ lemma cpm_bind: ∀n,h,p,I,G,L,V1,V2,T1,T2.
                 ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡[n, h] T2 →
                 ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ➡[n, h] ⓑ{p,I}V2.T2.
 #n #h #p #I #G #L #V1 #V2 #T1 #T2 * #riV #rhV #HV12 *
-/5 width=5 by cpg_bind, isrt_plus_O1, isr_shift, ex2_intro/
+/5 width=5 by cpg_bind, isrt_max_O1, isr_shift, ex2_intro/
 qed.
 
 (* Note: cpr_flat: does not hold in basic_1 *)
@@ -68,7 +68,7 @@ lemma cpm_flat: ∀n,h,I,G,L,V1,V2,T1,T2.
                 ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 →
                 ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ➡[n, h] ⓕ{I}V2.T2.
 #n #h #I #G #L #V1 #V2 #T1 #T2 * #riV #rhV #HV12 *
-/5 width=5 by isrt_plus_O1, isr_shift, cpg_flat, ex2_intro/
+/5 width=5 by isrt_max_O1, isr_shift, cpg_flat, ex2_intro/
 qed.
 
 (* Basic_2A1: includes: cpr_zeta *)
@@ -94,7 +94,7 @@ lemma cpm_beta: ∀n,h,p,G,L,V1,V2,W1,W2,T1,T2.
                 ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ W1 ➡[h] W2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ➡[n, h] T2 →
                 ⦃G, L⦄ ⊢ ⓐV1.ⓛ{p}W1.T1 ➡[n, h] ⓓ{p}ⓝW2.V2.T2.
 #n #h #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 * #riV #rhV #HV12 * #riW #rhW #HW12 *
-/6 width=7 by cpg_beta, isrt_plus_O2, isrt_plus, isr_shift, ex2_intro/
+/6 width=7 by cpg_beta, isrt_plus_O2, isrt_max, isr_shift, ex2_intro/
 qed.
 
 (* Basic_2A1: includes: cpr_theta *)
@@ -103,7 +103,7 @@ lemma cpm_theta: ∀n,h,p,G,L,V1,V,V2,W1,W2,T1,T2.
                  ⦃G, L.ⓓW1⦄ ⊢ T1 ➡[n, h] T2 →
                  ⦃G, L⦄ ⊢ ⓐV1.ⓓ{p}W1.T1 ➡[n, h] ⓓ{p}W2.ⓐV2.T2.
 #n #h #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 * #riV #rhV #HV1 #HV2 * #riW #rhW #HW12 *
-/6 width=9 by cpg_theta, isrt_plus_O2, isrt_plus, isr_shift, ex2_intro/
+/6 width=9 by cpg_theta, isrt_plus_O2, isrt_max, isr_shift, ex2_intro/
 qed.
 
 (* Basic properties on r-transition *****************************************)
@@ -192,7 +192,7 @@ lemma cpm_inv_bind1: ∀n,h,p,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ➡[n
                           p = true & I = Abbr.
 #n #h #p #I #G #L #V1 #T1 #U2 * #c #Hc #H elim (cpg_inv_bind1 … H) -H *
 [ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct
-  elim (isrt_inv_plus … Hc) -Hc #nV #nT #HcV #HcT #H destruct
+  elim (isrt_inv_max … Hc) -Hc #nV #nT #HcV #HcT #H destruct
   elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct
   /4 width=5 by ex3_2_intro, ex2_intro, or_introl/
 | #cT #T2 #HT12 #HUT2 #H1 #H2 #H3 destruct
@@ -209,7 +209,7 @@ lemma cpm_inv_abbr1: ∀n,h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ➡[n, h]
                      ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡[n, h] T & ⬆*[1] U2 ≡ T & p = true.
 #n #h #p #G #L #V1 #T1 #U2 * #c #Hc #H elim (cpg_inv_abbr1 … H) -H *
 [ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct
-  elim (isrt_inv_plus … Hc) -Hc #nV #nT #HcV #HcT #H destruct
+  elim (isrt_inv_max … Hc) -Hc #nV #nT #HcV #HcT #H destruct
   elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct
   /4 width=5 by ex3_2_intro, ex2_intro, or_introl/
 | #cT #T2 #HT12 #HUT2 #H1 #H2 destruct
@@ -224,7 +224,7 @@ lemma cpm_inv_abst1: ∀n,h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{p}V1.T1 ➡[n, h]
                               U2 = ⓛ{p}V2.T2.
 #n #h #p #G #L #V1 #T1 #U2 * #c #Hc #H elim (cpg_inv_abst1 … H) -H
 #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct
-elim (isrt_inv_plus … Hc) -Hc #nV #nT #HcV #HcT #H destruct
+elim (isrt_inv_max … Hc) -Hc #nV #nT #HcV #HcT #H destruct
 elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct
 /3 width=5 by ex3_2_intro, ex2_intro/
 qed-.
@@ -244,7 +244,7 @@ lemma cpm_inv_flat1: ∀n,h,I,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓕ{I}V1.U1 ➡[n, h]
                                               U2 = ⓓ{p}W2.ⓐV2.T2 & I = Appl.
 #n #h #I #G #L #V1 #U1 #U2 * #c #Hc #H elim (cpg_inv_flat1 … H) -H *
 [ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct
-  elim (isrt_inv_plus … Hc) -Hc #nV #nT #HcV #HcT #H destruct
+  elim (isrt_inv_max … Hc) -Hc #nV #nT #HcV #HcT #H destruct
   elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct
   /4 width=5 by or5_intro0, ex3_2_intro, ex2_intro/
 | #cU #U12 #H1 #H2 destruct
@@ -254,15 +254,15 @@ lemma cpm_inv_flat1: ∀n,h,I,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓕ{I}V1.U1 ➡[n, h]
   /4 width=3 by or5_intro2, ex3_intro, ex2_intro/
 | #cV #cW #cT #p #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #H1 #H2 #H3 #H4 destruct
   lapply (isrt_inv_plus_O_dx … Hc ?) -Hc // #Hc
-  elim (isrt_inv_plus … Hc) -Hc #n0 #nT #Hc #HcT #H destruct
-  elim (isrt_inv_plus … Hc) -Hc #nV #nW #HcV #HcW #H destruct
+  elim (isrt_inv_max … Hc) -Hc #n0 #nT #Hc #HcT #H destruct
+  elim (isrt_inv_max … Hc) -Hc #nV #nW #HcV #HcW #H destruct
   elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct
   elim (isrt_inv_shift … HcW) -HcW #HcW #H destruct
   /4 width=11 by or5_intro3, ex6_6_intro, ex2_intro/
 | #cV #cW #cT #p #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HW12 #HT12 #H1 #H2 #H3 #H4 destruct
   lapply (isrt_inv_plus_O_dx … Hc ?) -Hc // #Hc
-  elim (isrt_inv_plus … Hc) -Hc #n0 #nT #Hc #HcT #H destruct
-  elim (isrt_inv_plus … Hc) -Hc #nV #nW #HcV #HcW #H destruct
+  elim (isrt_inv_max … Hc) -Hc #n0 #nT #Hc #HcT #H destruct
+  elim (isrt_inv_max … Hc) -Hc #nV #nW #HcV #HcW #H destruct
   elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct
   elim (isrt_inv_shift … HcW) -HcW #HcW #H destruct
   /4 width=13 by or5_intro4, ex7_7_intro, ex2_intro/
@@ -282,20 +282,20 @@ lemma cpm_inv_appl1: ∀n,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓐ V1.U1 ➡[n, h] U2
                                               U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2.
 #n #h #G #L #V1 #U1 #U2 * #c #Hc #H elim (cpg_inv_appl1 … H) -H *
 [ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct
-  elim (isrt_inv_plus … Hc) -Hc #nV #nT #HcV #HcT #H destruct
+  elim (isrt_inv_max … Hc) -Hc #nV #nT #HcV #HcT #H destruct
   elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct
   /4 width=5 by or3_intro0, ex3_2_intro, ex2_intro/
 | #cV #cW #cT #p #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #H1 #H2 #H3 destruct
   lapply (isrt_inv_plus_O_dx … Hc ?) -Hc // #Hc
-  elim (isrt_inv_plus … Hc) -Hc #n0 #nT #Hc #HcT #H destruct
-  elim (isrt_inv_plus … Hc) -Hc #nV #nW #HcV #HcW #H destruct
+  elim (isrt_inv_max … Hc) -Hc #n0 #nT #Hc #HcT #H destruct
+  elim (isrt_inv_max … Hc) -Hc #nV #nW #HcV #HcW #H destruct
   elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct
   elim (isrt_inv_shift … HcW) -HcW #HcW #H destruct
   /4 width=11 by or3_intro1, ex5_6_intro, ex2_intro/
 | #cV #cW #cT #p #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HW12 #HT12 #H1 #H2 #H3 destruct
   lapply (isrt_inv_plus_O_dx … Hc ?) -Hc // #Hc
-  elim (isrt_inv_plus … Hc) -Hc #n0 #nT #Hc #HcT #H destruct
-  elim (isrt_inv_plus … Hc) -Hc #nV #nW #HcV #HcW #H destruct
+  elim (isrt_inv_max … Hc) -Hc #n0 #nT #Hc #HcT #H destruct
+  elim (isrt_inv_max … Hc) -Hc #nV #nW #HcV #HcW #H destruct
   elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct
   elim (isrt_inv_shift … HcW) -HcW #HcW #H destruct
   /4 width=13 by or3_intro2, ex6_7_intro, ex2_intro/
@@ -309,7 +309,7 @@ lemma cpm_inv_cast1: ∀n,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓝV1.U1 ➡[n, h] U2 
                       | ∃∃m. ⦃G, L⦄ ⊢ V1 ➡[m, h] U2 & n = ⫯m.
 #n #h #G #L #V1 #U1 #U2 * #c #Hc #H elim (cpg_inv_cast1 … H) -H *
 [ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct
-  elim (isrt_inv_plus … Hc) -Hc #nV #nT #HcV #HcT #H destruct
+  elim (isrt_inv_max … Hc) -Hc #nV #nT #HcV #HcT #H destruct
   elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct
   /4 width=5 by or3_intro0, ex3_2_intro, ex2_intro/
 | #cU #U12 #H destruct
diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
index 83322f4d8..dad1f9382 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
@@ -96,6 +96,20 @@ qed.
 lemma arith_i: ∀x,y,z. y < x → x+z-y-1 = x-y-1+z.
 /2 width=1 by plus_minus/ qed-.
 
+lemma idempotent_max: ∀n:nat. n = (n ∨ n).
+#n normalize >le_to_leb_true //
+qed.
+
+lemma associative_max: associative … max.
+#x #y #z normalize
+@(leb_elim x y) normalize #Hxy
+@(leb_elim y z) normalize #Hyz //
+[1,2: >le_to_leb_true /2 width=3 by transitive_le/
+| >not_le_to_leb_false /4 width=3 by lt_to_not_le, not_le_to_lt, transitive_lt/
+  >not_le_to_leb_false //
+]
+qed.
+
 (* Properties ***************************************************************)
 
 lemma eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2).
diff --git a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_max.ma b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_max.ma
index 1c8861fa8..46f457536 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_max.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_max.ma
@@ -36,6 +36,10 @@ lemma max_O_dx: ∀c. c = (c ∨ 𝟘𝟘).
 * #ri #rs #ti #ts <max_rew //
 qed.
 
+lemma max_idem: ∀c. c = (c ∨ c).
+* #ri #rs #ti #ts <max_rew //
+qed.
+
 (* Basic inversion properties ***********************************************)
 
 lemma max_inv_dx: ∀ri,rs,ti,ts,c1,c2. 〈ri,rs,ti,ts〉 = (c1 ∨ c2) →
@@ -46,6 +50,13 @@ lemma max_inv_dx: ∀ri,rs,ti,ts,c1,c2. 〈ri,rs,ti,ts〉 = (c1 ∨ c2) →
 <max_rew #H destruct /2 width=14 by ex6_8_intro/
 qed-.
 
+(* Main Properties **********************************************************)
+
+theorem max_assoc: associative … max.
+* #ri1 #rs1 #ti1 #ts1 * #ri2 #rs2 #ti2 #ts2 * #ri3 #rs3 #ti3 #ts3
+<max_rew <max_rew //
+qed.
+
 (* Properties with test for constrained rt-transition counter ***************)
 
 lemma isrt_max: ∀n1,n2,c1,c2. 𝐑𝐓⦃n1, c1⦄ → 𝐑𝐓⦃n2, c2⦄ → 𝐑𝐓⦃n1∨n2, c1∨c2⦄.
@@ -76,9 +87,8 @@ lapply (isrt_mono … Hn2 H2) -c2 #H destruct //
 qed-.
 
 (* Properties with shift ****************************************************)
-(*
-lemma max_shift: ∀c1,c2. (↓c1) ∨ (↓c2) = ↓(c1∨c2).
+
+lemma max_shift: ∀c1,c2. ((↓c1) ∨ (↓c2)) = ↓(c1∨c2).
 * #ri1 #rs1 #ti1 #ts1 * #ri2 #rs2 #ti2 #ts2
 <shift_rew <shift_rew <shift_rew <max_rew //
 qed.
-*)
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 87adfee3a..b0b529240 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_plus.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/steps/rtc_shift.ma".
+include "ground_2/steps/rtc_isrt.ma".
 
 (* RT-TRANSITION COUNTER ****************************************************)
 
@@ -93,10 +93,3 @@ elim (isrt_inv_plus … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct
 lapply (isrt_mono … Hn2 H2) -c2 #H destruct
 /2 width=3 by ex2_intro/
 qed-.
-
-(* Properties with shift ****************************************************)
-
-lemma plus_shift: ∀c1,c2. (↓c1) + (↓c2) = ↓(c1+c2).
-* #ri1 #rs1 #ti1 #ts1 * #ri2 #rs2 #ti2 #ts2
-<shift_rew <shift_rew <shift_rew <plus_rew //
-qed.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_shift.ma b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_shift.ma
index f7c56a3e1..cb2c38284 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_shift.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_shift.ma
@@ -18,14 +18,14 @@ include "ground_2/steps/rtc_isrt.ma".
 (* RT-TRANSITION COUNTER ****************************************************)
 
 definition shift (c:rtc): rtc ≝ match c with
-[ mk_rtc ri rs ti ts ⇒ 〈ri+rs, 0, ti+ts, 0〉 ].
+[ mk_rtc ri rs ti ts ⇒ 〈ri∨rs, 0, ti∨ts, 0〉 ].
 
 interpretation "shift (rtc)"
    'Drop c = (shift c).
 
 (* Basic properties *********************************************************)
 
-lemma shift_rew: ∀ri,rs,ti,ts. 〈ri+rs, 0, ti+ts, 0〉 = ↓〈ri, rs, ti, ts〉.
+lemma shift_rew: ∀ri,rs,ti,ts. 〈ri∨rs, 0, ti∨ts, 0〉 = ↓〈ri, rs, ti, ts〉.
 normalize //
 qed.
 
@@ -35,7 +35,7 @@ lemma shift_O: 𝟘𝟘 = ↓𝟘𝟘.
 (* Basic inversion properties ***********************************************)
 
 lemma shift_inv_dx: ∀ri,rs,ti,ts,c. 〈ri, rs, ti, ts〉 = ↓c →
-                    ∃∃ri0,rs0,ti0,ts0. ri0+rs0 = ri & 0 = rs & ti0+ts0 = ti & 0 = ts &
+                    ∃∃ri0,rs0,ti0,ts0. (ri0∨rs0) = ri & 0 = rs & (ti0∨ts0) = ti & 0 = ts &
                                        〈ri0, rs0, ti0, ts0〉 = c.
 #ri #rs #ti #ts * #ri0 #rs0 #ti0 #ts0 <shift_rew #H destruct
 /2 width=7 by ex5_4_intro/
@@ -52,7 +52,7 @@ qed.
 lemma isrt_inv_shift: ∀n,c. 𝐑𝐓⦃n, ↓c⦄ → 𝐑𝐓⦃0, c⦄ ∧ 0 = n.
 #n #c * #ri #rs #H
 elim (shift_inv_dx … H) -H #rt0 #rs0 #ti0 #ts0 #_ #_ #H1 #H2 #H3
-elim (plus_inv_O3 … H1) -H1 /3 width=3 by ex1_2_intro, conj/
+elim (max_inv_O3 … H1) -H1 /3 width=3 by ex1_2_intro, conj/
 qed-.
 
 lemma isr_inv_shift: ∀c. 𝐑𝐓⦃0, ↓c⦄ → 𝐑𝐓⦃0, c⦄.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
index 7e76ce4e1..a5d4181ed 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
@@ -12,7 +12,7 @@ table {
    class "water"
    [ { "generic rt-transition counter" * } {
         [ { "" * } {
-             [ "rtc ( 〈?,?,?,?〉 ) ( 𝟘𝟘 ) ( 𝟙𝟘 ) ( 𝟘𝟙 )" "rtc_isrc ( 𝐑𝐓⦃?, ?⦄ )" "rtc_shift ( ↓? )" "rtc_plus ( ? + ? )" * ]
+             [ "rtc ( 〈?,?,?,?〉 ) ( 𝟘𝟘 ) ( 𝟙𝟘 ) ( 𝟘𝟙 )" "rtc_isrc ( 𝐑𝐓⦃?, ?⦄ )" "rtc_shift ( ↓? )" "rtc_max ( ? ∨ ? )" "rtc_plus ( ? + ? )" * ]
           }
         ]
      }
-- 
2.39.2