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 7854b2a69a6323058937fdf2fa9b1908c5b83ccc..5114c745b99757450aa38bfe5fef681e484b0d44 100644 (file)
--- 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 7d678a7f304117e6fc996f224a1fe8bc8f9967da..ac8128153d640c0575a86ccf36733bd17a57c640 100644 (file)
--- 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 670dbd8ca85cce480c69ae016636bba47d57eab3..9dfe0c18e4a8c58babe2773923d10b8116a05719 100644 (file)
--- 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 42d83888241c60b92640f3b6558c85939aa4b026..543231681807de21fc17868dd28a9ffc12ab91c4 100644 (file)
--- 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 da8ea1519527fc2299f606b796ea0a4ae5b1496c..ef36b6f3388519015fcad8b8127c97b8bbfda9ad 100644 (file)
--- 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.