From 0bcf2dc1a27e38cb6cd3d44eb838d652926841e0 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 29 May 2021 10:40:29 +0200
Subject: [PATCH] update in ground

+ some renaming
---
 .../contribs/lambdadelta/ground/arith/nat_minus.ma |  2 +-
 .../contribs/lambdadelta/ground/arith/nat_plus.ma  |  4 ++--
 .../contribs/lambdadelta/ground/arith/nat_pred.ma  |  4 ++--
 .../contribs/lambdadelta/ground/arith/pnat_plus.ma |  6 +++---
 .../lambdadelta/ground/arith/ynat_lminus.ma        |  2 +-
 .../contribs/lambdadelta/ground/arith/ynat_plus.ma |  2 +-
 .../lambdadelta/ground/counters/rtc_ism_plus.ma    |  2 +-
 .../lambdadelta/ground/counters/rtc_ist_plus.ma    |  4 ++--
 .../lambdadelta/ground/relocation/gr_after_ist.ma  |  2 +-
 .../ground/relocation/gr_after_ist_isi.ma          |  6 +++---
 ...gr_after_nat_uni.ma => gr_after_nat_uni_tls.ma} |  4 ++--
 ...gr_after_pat_uni.ma => gr_after_pat_uni_tls.ma} | 14 +++++++-------
 .../contribs/lambdadelta/ground/web/ground_src.tbl |  2 +-
 13 files changed, 27 insertions(+), 27 deletions(-)
 rename matita/matita/contribs/lambdadelta/ground/relocation/{gr_after_nat_uni.ma => gr_after_nat_uni_tls.ma} (97%)
 rename matita/matita/contribs/lambdadelta/ground/relocation/{gr_after_pat_uni.ma => gr_after_pat_uni_tls.ma} (91%)

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma
index d5d1c13fe..e4ccf83f4 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma
@@ -32,7 +32,7 @@ lemma nminus_zero_dx (m): m = m - 𝟎.
 // qed.
 
 (*** minus_SO_dx *)
-lemma nminus_one_dx (m): ↓m = m - 𝟏 .
+lemma nminus_unit_dx (m): ↓m = m - 𝟏 .
 // qed.
 
 (*** eq_minus_S_pred *)
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
index f1dffc51d..a9894fc62 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
@@ -31,7 +31,7 @@ lemma nplus_zero_dx (m): m = m + 𝟎.
 // qed.
 
 (*** plus_SO_dx *)
-lemma nplus_one_dx (n): ↑n = n + 𝟏.
+lemma nplus_unit_dx (n): ↑n = n + 𝟏.
 // qed.
 
 (*** plus_n_Sm *)
@@ -76,7 +76,7 @@ qed.
 (* Helper constructions *****************************************************)
 
 (*** plus_SO_sn *)
-lemma nplus_one_sn (n): ↑n = 𝟏 + n.
+lemma nplus_unit_sn (n): ↑n = 𝟏 + n.
 #n <nplus_comm // qed.
 
 lemma nplus_succ_shift (m) (n): ↑m + n = m + ↑n.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_pred.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_pred.ma
index d7f79d76b..3367fe66a 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_pred.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_pred.ma
@@ -44,7 +44,7 @@ lemma npred_zero: 𝟎 = ↓𝟎.
 lemma npred_inj (p): ↓p = ↓(ninj p).
 // qed.
 
-lemma npred_one: 𝟎 = ↓𝟏.
+lemma npred_unit: 𝟎 = ↓𝟏.
 // qed.
 
 lemma npred_psucc (p): ninj p = ↓↑p.
@@ -54,7 +54,7 @@ lemma npred_psucc (p): ninj p = ↓↑p.
 
 lemma npred_pnat_inv_refl (p): ninj p = ↓p → ⊥.
 *
-[ <npred_one #H destruct
+[ <npred_unit #H destruct
 | #p /3 width=2 by psucc_inv_refl, eq_inv_ninj_bi/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
index 8096e849b..af5bd0943 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
@@ -25,7 +25,7 @@ interpretation
 
 (* Basic constructions ******************************************************)
 
-lemma pplus_one_dx (p): ↑p = p + 𝟏.
+lemma pplus_unit_dx (p): ↑p = p + 𝟏.
 // qed.
 
 lemma pplus_succ_dx (p) (q): ↑(p+q) = p + ↑q.
@@ -37,7 +37,7 @@ lemma pplus_succ_sn (p) (q): ↑(p+q) = ↑p + q.
 #p #q @(piter_appl … psucc)
 qed.
 
-lemma pplus_one_sn (p): ↑p = 𝟏 + p.
+lemma pplus_unit_sn (p): ↑p = 𝟏 + p.
 #p elim p -p //
 qed.
 
@@ -54,7 +54,7 @@ qed.
 
 lemma eq_inv_unit_pplus (p) (q): 𝟏 = p + q → ⊥.
 #p #q elim q -q
-[ <pplus_one_dx #H destruct
+[ <pplus_unit_dx #H destruct
 | #q #_ <pplus_succ_dx #H destruct
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus.ma
index 6a2e4dbee..b1dee6cef 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus.ma
@@ -42,7 +42,7 @@ lemma ylminus_succ_dx (x:ynat) (n): ↓(x-n) = x - ↑n.
 qed.
 
 (*** yminus_SO2 *)
-lemma ylminus_one_dx (x): ↓x = x - (𝟏).
+lemma ylminus_unit_dx (x): ↓x = x - (𝟏).
 // qed.
 
 (*** yminus_Y_inj *)
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.ma
index bc75d92d1..f002081e4 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.ma
@@ -47,7 +47,7 @@ lemma yplus_zero_dx (x): x = x + 𝟎.
 (* Constructions with ysucc *************************************************)
 
 (*** yplus_SO2 *)
-lemma yplus_one_dx (x): ↑x = x + 𝟏.
+lemma yplus_unit_dx (x): ↑x = x + 𝟏.
 // qed.
 
 (*** yplus_S2 yplus_succ2 *)
diff --git a/matita/matita/contribs/lambdadelta/ground/counters/rtc_ism_plus.ma b/matita/matita/contribs/lambdadelta/ground/counters/rtc_ism_plus.ma
index 5453b63fb..4451820f9 100644
--- a/matita/matita/contribs/lambdadelta/ground/counters/rtc_ism_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/counters/rtc_ism_plus.ma
@@ -33,7 +33,7 @@ lemma rtc_ism_plus_zero_dx (n) (c1) (c2): 𝐌❪n,c1❫ → 𝐌❪𝟎,c2❫ 
 /2 width=1 by rtc_ism_plus/ qed.
 
 lemma rtc_ism_succ (n) (c): 𝐌❪n,c❫ → 𝐌❪↑n,c+𝟘𝟙❫.
-#n #c #H >nplus_one_dx
+#n #c #H >nplus_unit_dx
 /2 width=1 by rtc_ism_plus/
 qed.
 
diff --git a/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist_plus.ma b/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist_plus.ma
index 08bb3b772..5156acb85 100644
--- a/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist_plus.ma
@@ -33,7 +33,7 @@ lemma rtc_ist_plus_zero_dx (n) (c1) (c2): 𝐓❪n,c1❫ → 𝐓❪𝟎,c2❫ 
 /2 width=1 by rtc_ist_plus/ qed.
 
 lemma rtc_ist_succ (n) (c): 𝐓❪n,c❫ → 𝐓❪↑n,c+𝟘𝟙❫.
-#n #c #H >nplus_one_dx
+#n #c #H >nplus_unit_dx
 /2 width=1 by rtc_ist_plus/
 qed.
 
@@ -54,7 +54,7 @@ lemma rtc_ist_inv_plus_zero_dx (n) (c1) (c2): 𝐓❪n,c1 + c2❫ → 𝐓❪
 elim (rtc_ist_inv_plus … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct //
 qed-.
 
-lemma rtc_ist_inv_plus_one_dx:
+lemma rtc_ist_inv_plus_unit_dx:
       ∀n,c1,c2. 𝐓❪n,c1 + c2❫ → 𝐓❪𝟏,c2❫ →
       ∃∃m. 𝐓❪m,c1❫ & n = ↑m.
 #n #c1 #c2 #H #H2 destruct
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_ist.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_ist.ma
index e3f8acfcd..97780f1c6 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_ist.ma
@@ -45,7 +45,7 @@ lemma gr_after_des_ist_sn:
 qed-.
 
 (*** after_at1_fwd *)
-lemma gr_after_pat_sn_des:
+lemma gr_after_des_ist_pat:
       ∀f1,i1,i2. @❪i1, f1❫ ≘ i2 → ∀f2. 𝐓❪f2❫ → ∀f. f2 ⊚ f1 ≘ f →
       ∃∃i. @❪i2, f2❫ ≘ i & @❪i1, f❫ ≘ i.
 #f1 #i1 #i2 #Hf1 #f2 #Hf2 #f #Hf elim (Hf2 i2) -Hf2
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_ist_isi.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_ist_isi.ma
index 93077d253..fd325b4d7 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_ist_isi.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_ist_isi.ma
@@ -20,7 +20,7 @@ include "ground/relocation/gr_after_ist.ma".
 (* Forward lemmas on istot and isid **************************************************)
 
 (*** after_fwd_isid_sn *)
-lemma gr_after_des_isi_sn:
+lemma gr_after_des_ist_eq_sn:
       ∀f2,f1,f. 𝐓❪f❫ → f2 ⊚ f1 ≘ f → f1 ≡ f → 𝐈❪f2❫.
 #f2 #f1 #f #H #Hf elim (gr_after_inv_ist … Hf H) -H
 #Hf2 #Hf1 #H @gr_isi_pat_total // -Hf2
@@ -31,10 +31,10 @@ lemma gr_after_des_isi_sn:
 qed-.
 
 (*** after_fwd_isid_dx *)
-lemma gr_after_des_isi_dx:
+lemma gr_after_des_ist_eq_dx:
       ∀f2,f1,f.  𝐓❪f❫ → f2 ⊚ f1 ≘ f → f2 ≡ f → 𝐈❪f1❫.
 #f2 #f1 #f #H #Hf elim (gr_after_inv_ist … Hf H) -H
 #Hf2 #Hf1 #H2 @gr_isi_pat_total // -Hf1
-#i1 #i2 #Hi12 elim (gr_after_pat_sn_des … Hi12 … Hf) -f1
+#i1 #i2 #Hi12 elim (gr_after_des_ist_pat … Hi12 … Hf) -f1
 /3 width=8 by gr_pat_inj, gr_pat_eq_repl_back/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_nat_uni.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_nat_uni_tls.ma
similarity index 97%
rename from matita/matita/contribs/lambdadelta/ground/relocation/gr_after_nat_uni.ma
rename to matita/matita/contribs/lambdadelta/ground/relocation/gr_after_nat_uni_tls.ma
index 489e820f6..04be0911d 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_nat_uni.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_nat_uni_tls.ma
@@ -22,7 +22,7 @@ include "ground/relocation/gr_after_isi.ma".
 (* Properties with gr_nat and uni *)
 
 (*** after_uni_dx *)
-lemma gr_after_uni_dx (l2) (l1):
+lemma gr_after_nat_uni (l2) (l1):
       ∀f2. @↑❪l1, f2❫ ≘ l2 →
       ∀f. f2 ⊚ 𝐮❨l1❩ ≘ f → 𝐮❨l2❩ ⊚ ⫱*[l2] f2 ≘ f.
 #l2 @(nat_ind_succ … l2) -l2
@@ -43,7 +43,7 @@ lemma gr_after_uni_dx (l2) (l1):
 qed.
 
 (*** after_uni_sn *)
-lemma gr_after_uni_sn (l2) (l1):
+lemma gr_nat_after_uni_tls (l2) (l1):
       ∀f2. @↑❪l1, f2❫ ≘ l2 →
       ∀f. 𝐮❨l2❩ ⊚ ⫱*[l2] f2 ≘ f → f2 ⊚ 𝐮❨l1❩ ≘ f.
 #l2 @(nat_ind_succ … l2) -l2
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_pat_uni.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_pat_uni_tls.ma
similarity index 91%
rename from matita/matita/contribs/lambdadelta/ground/relocation/gr_after_pat_uni.ma
rename to matita/matita/contribs/lambdadelta/ground/relocation/gr_after_pat_uni_tls.ma
index 52765a6bb..e8104fd3e 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_pat_uni.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_pat_uni_tls.ma
@@ -20,10 +20,10 @@ include "ground/relocation/gr_after_isi.ma".
 
 (* RELATIONAL COMPOSITION FOR GENERIC RELOCATION MAPS ***********************************************************)
 
-(* Properties with pat and uni *******************************************************)
+(* Properties with pat and uni and tls *******************************************************)
 
 (*** after_uni_succ_dx *)
-lemma gr_after_uni_dx (i2) (i1):
+lemma gr_after_pat_uni (i2) (i1):
       ∀f2. @❪i1, f2❫ ≘ i2 →
       ∀f. f2 ⊚ 𝐮❨i1❩ ≘ f → 𝐮❨i2❩ ⊚ ⫱*[i2] f2 ≘ f.
 #i2 elim i2 -i2
@@ -45,7 +45,7 @@ lemma gr_after_uni_dx (i2) (i1):
 qed.
 
 (*** after_uni_succ_sn *)
-lemma gr_after_uni_sn (i2) (i1):
+lemma gr_pat_after_uni_tls (i2) (i1):
       ∀f2. @❪i1, f2❫ ≘ i2 →
       ∀f. 𝐮❨i2❩ ⊚ ⫱*[i2] f2 ≘ f → f2 ⊚ 𝐮❨i1❩ ≘ f.
 #i2 elim i2 -i2
@@ -66,14 +66,14 @@ qed-.
 (* Advanced properties with uni *)
 
 (*** after_uni_one_dx *)
-lemma gr_after_uni_one_dx:
+lemma gr_after_push_unit:
       ∀f2,f. ⫯f2 ⊚ 𝐮❨𝟏❩ ≘ f → 𝐮❨𝟏❩ ⊚ f2 ≘ f.
 #f2 #f #H
-@(gr_after_uni_dx … (⫯f2))
+@(gr_after_pat_uni … (⫯f2))
 /2 width=3 by gr_pat_refl/
 qed.
 
 (*** after_uni_one_sn *)
-lemma gr_after_uni_one_sn:
+lemma gr_after_unit_sn:
       ∀f1,f. 𝐮❨𝟏❩ ⊚ f1 ≘ f → ⫯f1 ⊚ 𝐮❨𝟏❩ ≘ f.
-/3 width=3 by gr_after_uni_sn, gr_pat_refl/ qed-.
+/3 width=3 by gr_pat_after_uni_tls, gr_pat_refl/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
index 7078e2afc..6c57ebf67 100644
--- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
@@ -34,7 +34,7 @@ table {
           [ "gr_sdj ( ? ∥ ? )" "gr_sdj_eq" "gr_sdj_isi" * ]
           [ "gr_sle ( ? ⊆ ? )" "gr_sle_eq" "gr_sle_pushs" "gr_sle_tls" "gr_sle_isi" "gr_sle_isd" "gr_sle_sle" * ]
           [ "gr_coafter ( ? ~⊚ ? ≘ ? )" "gr_coafter_eq" "gr_coafter_uni_pushs" "gr_coafter_pat_tls" "gr_coafter_nat_tls" "gr_coafter_nat_tls_pushs" "gr_coafter_isi" "gr_coafter_isu" "gr_coafter_ist_isi" "gr_coafter_ist_isf" "gr_coafter_coafter" "gr_coafter_coafter_ist" * ]
-          [ "gr_after ( ? ⊚ ? ≘ ? )" "gr_after_eq" "gr_after_uni" "gr_after_basic" "gr_after_pat" "gr_after_pat_tls" "gr_after_pat_uni" "gr_after_nat_uni" "gr_after_isi" "gr_after_isu" "gr_after_ist" "gr_after_ist_isi" "gr_after_after" "gr_after_after_ist" * ]
+          [ "gr_after ( ? ⊚ ? ≘ ? )" "gr_after_eq" "gr_after_uni" "gr_after_basic" "gr_after_pat" "gr_after_pat_tls" "gr_after_pat_uni_tls" "gr_after_nat_uni_tls" "gr_after_isi" "gr_after_isu" "gr_after_ist" "gr_after_ist_isi" "gr_after_after" "gr_after_after_ist" * ]
           [ "gr_isd ( 𝛀❪?❫ )" "gr_isd_eq" "gr_isd_tl" "gr_isd_nexts" "gr_isd_tls" * ]
           [ "gr_ist ( 𝐓❪?❫ )" "gr_ist_tls" "gr_ist_isi" "gr_ist_ist" * ]
           [ "gr_isf ( 𝐅❪?❫ )" "gr_isf_eq" "gr_isf_tl" "gr_isf_pushs" "fr_isf_tls" "gr_ifs_uni" "gr_isf_isu" * ]
-- 
2.39.2