From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 19 Dec 2022 22:16:18 +0000 (+0100)
Subject: update in ground
X-Git-Tag: make_still_working~19
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=73cc0c523c5264f2883c25f6735be325e5cfd1da

update in ground

+ some renaming
---

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pap.ma
index 7854b2a69..5114c745b 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pap.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pap.ma
@@ -24,8 +24,8 @@ lemma tr_compose_pap (i) (f1) (f2):
       f2＠⧣❨f1＠⧣❨i❩❩ = (f2∘f1)＠⧣❨i❩.
 #i elim i -i
 [ * #p1 #f1 #f2
-  <tr_compose_unfold <tr_pap_unit <tr_pap_unit //
+  <tr_compose_unfold <tr_cons_pap_unit <tr_cons_pap_unit //
 | #i #IH * #p1 #f1 #f2
-  <tr_compose_unfold <tr_pap_succ <tr_pap_succ //
+  <tr_compose_unfold <tr_cons_pap_succ <tr_cons_pap_succ //
 ]
 qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_tls.ma
index 7d678a7f3..ac8128153 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_tls.ma
@@ -24,7 +24,7 @@ include "ground/arith/nat_rplus_pplus.ma".
 lemma tr_compose_tls (p) (f1) (f2):
       (⇂*[f1＠⧣❨p❩]f2)∘(⇂*[p]f1) = ⇂*[p](f2∘f1).
 #p elim p -p [| #p #IH ] * #q1 #f1 #f2 //
-<tr_compose_unfold <tr_pap_succ
+<tr_compose_unfold <tr_cons_pap_succ
 >nsucc_inj <stream_tls_succ_lcons <stream_tls_succ_lcons
 <IH -IH >nrplus_inj_dx >nrplus_inj_sn <stream_tls_plus //
 qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap.ma
index 670dbd8ca..9dfe0c18e 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap.ma
@@ -34,11 +34,11 @@ interpretation
 (* Basic constructions ******************************************************)
 
 (*** apply_O1 *)
-lemma tr_pap_unit (f):
+lemma tr_cons_pap_unit (f):
       ∀p. p = (p⨮f)＠⧣❨𝟏❩.
 // qed.
 
 (*** apply_S1 *)
-lemma tr_pap_succ (f):
+lemma tr_cons_pap_succ (f):
       ∀p,i. f＠⧣❨i❩+p = (p⨮f)＠⧣❨↑i❩.
 // qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_eq.ma
index 42d838882..543231681 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_eq.ma
@@ -24,7 +24,7 @@ theorem tr_pap_eq_repl (i):
         stream_eq_repl … (λf1,f2. f1＠⧣❨i❩ = f2＠⧣❨i❩).
 #i elim i -i [2: #i #IH ] * #p1 #f1 * #p2 #f2 #H
 elim (stream_eq_inv_cons_bi … H) -H [1,8: |*: // ] #Hp #Hf //
-<tr_pap_succ <tr_pap_succ /3 width=1 by eq_f2/
+<tr_cons_pap_succ <tr_cons_pap_succ /3 width=1 by eq_f2/
 qed.
 
 (* Main inversions with stream_eq *******************************************)
@@ -34,8 +34,8 @@ corec theorem nstream_eq_inv_ext:
 * #p1 #f1 * #p2 #f2 #Hf @stream_eq_cons
 [ @(Hf (𝟏))
 | @nstream_eq_inv_ext -nstream_eq_inv_ext #i
-  lapply (Hf (𝟏)) <tr_pap_unit <tr_pap_unit #H destruct
-  lapply (Hf (↑i)) <tr_pap_succ <tr_pap_succ #H
+  lapply (Hf (𝟏)) <tr_cons_pap_unit <tr_cons_pap_unit #H destruct
+  lapply (Hf (↑i)) <tr_cons_pap_succ <tr_cons_pap_succ #H
   /3 width=2 by eq_inv_pplus_bi_dx, eq_inv_psucc_bi/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_tls.ma
index da8ea1519..ef36b6f33 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_tls.ma
@@ -24,7 +24,7 @@ lemma tr_pap_plus (p1) (p2) (f):
 #p1 #p2 elim p2 -p2
 [ * #p #f //
 | #i #IH * #p #f
-  <pplus_succ_dx <tr_pap_succ <tr_pap_succ
+  <pplus_succ_dx <tr_cons_pap_succ <tr_cons_pap_succ
   <IH -IH >nsucc_inj //
 ]
 qed.