update in ground

+ notation update and renaming

diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/apply_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/apply_2.ma
deleted file mode 100644 (file)
index 2baa23e..0000000
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/apply_2.ma
+++ /dev/null
@@ -1,19 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* GROUND NOTATION **********************************************************)
-
-notation "hvbox( f ＠❨ break term 46 a ❩ )"
-  non associative with precedence 60
-  for @{ 'Apply $f $a }.

diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/applysucc_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/applysucc_2.ma
deleted file mode 100644 (file)
index 177d043..0000000
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/applysucc_2.ma
+++ /dev/null
@@ -1,19 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* GROUND NOTATION **********************************************************)
-
-notation "hvbox( f @↑❨ break term 46 a ❩ )"
-  non associative with precedence 60
-  for @{ 'ApplySucc $f $a }.

diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/at_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/at_2.ma
new file mode 100644 (file)
index 0000000..af60609
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/at_2.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* GROUND NOTATION **********************************************************)
+
+notation "hvbox( f ＠❨ break term 46 a ❩ )"
+  non associative with precedence 60
+  for @{ 'At $f $a }.

diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/atsection_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/atsection_2.ma
new file mode 100644 (file)
index 0000000..7867ea5
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/atsection_2.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* GROUND NOTATION **********************************************************)
+
+notation "hvbox( f ＠§❨ break term 46 a ❩ )"
+  non associative with precedence 60
+  for @{ 'AtSection $f $a }.

diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/ratsection_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/ratsection_3.ma
new file mode 100644 (file)
index 0000000..688b638
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/ratsection_3.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* GROUND NOTATION **********************************************************)
+
+notation "hvbox( ＠§❨ term 46 T1 , break term 46 f ❩ ≘ break term 46 T2 )"
+  non associative with precedence 45
+  for @{ 'RAtSection $T1 $f $T2 }.

diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/ratsucc_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/ratsucc_3.ma
deleted file mode 100644 (file)
index b5a43f6..0000000
--- a/matita/matita/contribs/lambdadelta/ground/notation/relations/ratsucc_3.ma
+++ /dev/null
@@ -1,19 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* GROUND NOTATION **********************************************************)
-
-notation "hvbox( @↑❨ term 46 T1 , break term 46 f ❩ ≘ break term 46 T2 )"
-  non associative with precedence 45
-  for @{ 'RAtSucc $T1 $f $T2 }.

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat.ma
index 0a70d2f452cf2f39ac825a6cf39d333ca2d396d2..59e8c9fe6a32db046bcf79b54d1de98ec83dbf36 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/notation/relations/ratsucc_3.ma".
+include "ground/notation/relations/ratsection_3.ma".
 include "ground/arith/nat_plus.ma".
 include "ground/arith/nat_lt.ma".
 include "ground/relocation/fr2_map.ma".
@@ -34,13 +34,13 @@ inductive fr2_nat: fr2_map → relation nat ≝
 
 interpretation
   "non-negative relational application (finite relocation maps with pairs)"
-  'RAtSucc l1 f l2 = (fr2_nat f l1 l2).
+  'RAtSection l1 f l2 = (fr2_nat f l1 l2).
 
 (* Basic inversions *********************************************************)
 
 (*** at_inv_nil *)
 lemma fr2_nat_inv_empty (l1) (l2):
-      @↑❨l1, 𝐞❩ ≘ l2 → l1 = l2.
+      ＠§❨l1, 𝐞❩ ≘ l2 → l1 = l2.
 #l1 #l2 @(insert_eq_1 … (𝐞))
 #f * -f -l1 -l2
 [ //
@@ -51,9 +51,9 @@ qed-.
 
 (*** at_inv_cons *)
 lemma fr2_nat_inv_lcons (f) (d) (h) (l1) (l2):
-      @↑❨l1, ❨d,h❩◗f❩ ≘ l2 →
-      ∨∨ ∧∧ l1 < d & @↑❨l1, f❩ ≘ l2 
-       | ∧∧ d ≤ l1 & @↑❨l1+h, f❩ ≘ l2.
+      ＠§❨l1, ❨d,h❩◗f❩ ≘ l2 →
+      ∨∨ ∧∧ l1 < d & ＠§❨l1, f❩ ≘ l2 
+       | ∧∧ d ≤ l1 & ＠§❨l1+h, f❩ ≘ l2.
 #g #d #h #l1 #l2 @(insert_eq_1 … (❨d, h❩◗g))
 #f * -f -l1 -l2
 [ #l #H destruct
@@ -64,7 +64,7 @@ qed-.
 
 (*** at_inv_cons *)
 lemma fr2_nat_inv_lcons_lt (f) (d) (h) (l1) (l2):
-      @↑❨l1, ❨d,h❩◗f❩ ≘ l2 → l1 < d → @↑❨l1, f❩ ≘ l2.
+      ＠§❨l1, ❨d,h❩◗f❩ ≘ l2 → l1 < d → ＠§❨l1, f❩ ≘ l2.
 #f #d #h #l1 #h2 #H
 elim (fr2_nat_inv_lcons … H) -H * // #Hdl1 #_ #Hl1d
 elim (nlt_ge_false … Hl1d Hdl1)
@@ -72,7 +72,7 @@ qed-.
 
 (*** at_inv_cons *)
 lemma fr2_nat_inv_lcons_ge (f) (d) (h) (l1) (l2):
-      @↑❨l1, ❨d,h❩◗f❩ ≘ l2 → d ≤ l1 → @↑❨l1+h, f❩ ≘ l2.
+      ＠§❨l1, ❨d,h❩◗f❩ ≘ l2 → d ≤ l1 → ＠§❨l1+h, f❩ ≘ l2.
 #f #d #h #l1 #h2 #H
 elim (fr2_nat_inv_lcons … H) -H * // #Hl1d #_ #Hdl1
 elim (nlt_ge_false … Hl1d Hdl1)

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat_nat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat_nat.ma
index c84990142f8c73b4661697b94c15d3b00168a327..287e6cd58df32dd124d00eaad8e5c92168aeac89 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat_nat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat_nat.ma
@@ -20,7 +20,7 @@ include "ground/relocation/fr2_nat.ma".
 
 (*** at_mono *)
 theorem fr2_nat_mono (f) (l):
-        ∀l1. @↑❨l, f❩ ≘ l1 → ∀l2. @↑❨l, f❩ ≘ l2 → l1 = l2.
+        ∀l1. ＠§❨l, f❩ ≘ l1 → ∀l2. ＠§❨l, f❩ ≘ l2 → l1 = l2.
 #f #l #l1 #H elim H -f -l -l1
 [ #l #x #H <(fr2_nat_inv_empty … H) -x //
 | #f #d #h #l #l1 #Hld #_ #IH #x #H

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/nap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/nap.ma
index a5ab2dcb79ee66d5e70a91ac731e4b18968b7f79..921863e5065948b5b73449c61337a28d4c04ea85 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/nap.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/nap.ma
@@ -1,7 +1,7 @@
 include "ground/relocation/tr_uni_pap.ma".
 include "ground/relocation/tr_compose_pap.ma".
 include "ground/relocation/tr_pap_eq.ma".
-include "ground/notation/functions/applysucc_2.ma".
+include "ground/notation/functions/atsection_2.ma".
 include "ground/arith/nat_lt.ma".
 include "ground/arith/nat_plus_rplus.ma".
 include "ground/arith/nat_pred_succ.ma".
@@ -17,46 +17,46 @@ definition tr_nap (f) (l:nat): nat ≝
 
 interpretation
   "functional non-negative application (total relocation maps)"
-  'ApplySucc f l = (tr_nap f l).
+  'AtSection f l = (tr_nap f l).
 
 lemma tr_nap_unfold (f) (l):
-      ↓(f＠⧣❨↑l❩) = f@↑❨l❩.
+      ↓(f＠⧣❨↑l❩) = f＠§❨l❩.
 // qed.
 
 lemma tr_pap_succ_nap (f) (l):
-      ↑(f@↑❨l❩) = f＠⧣❨↑l❩.
+      ↑(f＠§❨l❩) = f＠⧣❨↑l❩.
 // qed.
 
 lemma tr_compose_nap (f2) (f1) (l):
-      f2@↑❨f1@↑❨l❩❩ = (f2∘f1)@↑❨l❩.
+      f2＠§❨f1＠§❨l❩❩ = (f2∘f1)＠§❨l❩.
 #f2 #f1 #l
 <tr_nap_unfold <tr_nap_unfold <tr_nap_unfold
 <tr_compose_pap <npsucc_pred //
 qed.
 
 lemma tr_uni_nap (n) (m):
-      m + n = 𝐮❨n❩@↑❨m❩.
+      m + n = 𝐮❨n❩＠§❨m❩.
 #n #m
 <tr_nap_unfold
 <tr_uni_pap <nrplus_npsucc_sn //
 qed.
 
 lemma tr_nap_push (f):
-      ∀l. ↑(f@↑❨l❩) = (⫯f)@↑❨↑l❩.
+      ∀l. ↑(f＠§❨l❩) = (⫯f)＠§❨↑l❩.
 #f #l
 <tr_nap_unfold <tr_nap_unfold
 <tr_pap_push <pnpred_psucc //
 qed.
 
 lemma tr_nap_pushs_lt (f) (n) (m):
-      m < n → m = (⫯*[n]f)@↑❨m❩.
+      m < n → m = (⫯*[n]f)＠§❨m❩.
 #f #n #m #Hmn
 <tr_nap_unfold <tr_pap_pushs_le
 /2 width=1 by nlt_npsucc_bi/
 qed-.
 
 theorem tr_nap_eq_repl (i):
-        stream_eq_repl … (λf1,f2. f1@↑❨i❩ = f2@↑❨i❩).
+        stream_eq_repl … (λf1,f2. f1＠§❨i❩ = f2＠§❨i❩).
 #i #f1 #f2 #Hf
 <tr_nap_unfold <tr_nap_unfold
 /3 width=1 by tr_pap_eq_repl, eq_f/

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist.ma
index 62c9f79bd79bc7808792b2f820608cd61b1c2fb9..3973bad47340856096ea50605f08e27a942727c5 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist.ma
@@ -54,8 +54,8 @@ lemma pr_after_des_ist_pat:
 qed-.
 
 lemma pr_after_des_ist_nat:
-      ∀f1,l1,l2. @↑❨l1, f1❩ ≘ l2 → ∀f2. 𝐓❨f2❩ → ∀f. f2 ⊚ f1 ≘ f →
-      ∃∃l. @↑❨l2, f2❩ ≘ l & @↑❨l1, f❩ ≘ l.
+      ∀f1,l1,l2. ＠§❨l1, f1❩ ≘ l2 → ∀f2. 𝐓❨f2❩ → ∀f. f2 ⊚ f1 ≘ f →
+      ∃∃l. ＠§❨l2, f2❩ ≘ l & ＠§❨l1, f❩ ≘ l.
 #f1 #l1 #l2 #H1 #f2 #H2 #f #Hf
 elim (pr_after_des_ist_pat … H1 … H2 … Hf) -f1 -H2
 /2 width=3 by ex2_intro/

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_nat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_nat.ma
index d236932028fdfd1ded4c8c7643a3f3ab1df9d813..e1faddd22d63aef3e9e0b604625a1d6b200a8f48 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_nat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_nat.ma
@@ -20,24 +20,24 @@ include "ground/relocation/pr_after_pat.ma".
 (* Destructions with pr_nat *************************************************)
 
 lemma pr_after_nat_des (l) (l1):
-      ∀f. @↑❨l1, f❩ ≘ l → ∀f2,f1. f2 ⊚ f1 ≘ f →
-      ∃∃l2. @↑❨l1, f1❩ ≘ l2 & @↑❨l2, f2❩ ≘ l.
+      ∀f. ＠§❨l1, f❩ ≘ l → ∀f2,f1. f2 ⊚ f1 ≘ f →
+      ∃∃l2. ＠§❨l1, f1❩ ≘ l2 & ＠§❨l2, f2❩ ≘ l.
 #l #l1 #f #H1 #f2 #f1 #Hf
 elim (pr_after_pat_des … H1 … Hf) -f #i2 #H1 #H2
 /2 width=3 by ex2_intro/
 qed-.
 
 lemma pr_after_des_nat (l) (l2) (l1):
-      ∀f1,f2. @↑❨l1, f1❩ ≘ l2 → @↑❨l2, f2❩ ≘ l →
-      ∀f. f2 ⊚ f1 ≘ f → @↑❨l1, f❩ ≘ l.
+      ∀f1,f2. ＠§❨l1, f1❩ ≘ l2 → ＠§❨l2, f2❩ ≘ l →
+      ∀f. f2 ⊚ f1 ≘ f → ＠§❨l1, f❩ ≘ l.
 /2 width=6 by pr_after_des_pat/ qed-.
 
 lemma pr_after_des_nat_sn (l1) (l):
-      ∀f. @↑❨l1, f❩ ≘ l → ∀f1,l2. @↑❨l1, f1❩ ≘ l2 →
-      ∀f2. f2 ⊚ f1 ≘ f → @↑❨l2, f2❩ ≘ l.
+      ∀f. ＠§❨l1, f❩ ≘ l → ∀f1,l2. ＠§❨l1, f1❩ ≘ l2 →
+      ∀f2. f2 ⊚ f1 ≘ f → ＠§❨l2, f2❩ ≘ l.
 /2 width=6 by pr_after_des_pat_sn/ qed-.
 
 lemma pr_after_des_nat_dx (l) (l2) (l1):
-      ∀f,f2. @↑❨l1, f❩ ≘ l → @↑❨l2, f2❩ ≘ l →
-      ∀f1. f2 ⊚ f1 ≘ f → @↑❨l1, f1❩ ≘ l2.
+      ∀f,f2. ＠§❨l1, f❩ ≘ l → ＠§❨l2, f2❩ ≘ l →
+      ∀f1. f2 ⊚ f1 ≘ f → ＠§❨l1, f1❩ ≘ l2.
 /2 width=6 by pr_after_des_pat_dx/ qed-.

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_nat_uni_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_nat_uni_tls.ma
index 3ef1f5096bd4ae40e8ccff9a68e917f9e78798ae..55ddd62879eaced0f0e70c7f5ea444e58a7fe2de 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_nat_uni_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_nat_uni_tls.ma
@@ -23,7 +23,7 @@ include "ground/relocation/pr_after_isi.ma".
 
 (*** after_uni_dx *)
 lemma pr_after_nat_uni (l2) (l1):
-      ∀f2. @↑❨l1, f2❩ ≘ l2 →
+      ∀f2. ＠§❨l1, f2❩ ≘ l2 →
       ∀f. f2 ⊚ 𝐮❨l1❩ ≘ f → 𝐮❨l2❩ ⊚ ⫰*[l2] f2 ≘ f.
 #l2 @(nat_ind_succ … l2) -l2
 [ #l1 #f2 #Hf2 #f #Hf
@@ -44,7 +44,7 @@ qed.
 
 (*** after_uni_sn *)
 lemma pr_nat_after_uni_tls (l2) (l1):
-      ∀f2. @↑❨l1, f2❩ ≘ l2 →
+      ∀f2. ＠§❨l1, f2❩ ≘ l2 →
       ∀f. 𝐮❨l2❩ ⊚ ⫰*[l2] f2 ≘ f → f2 ⊚ 𝐮❨l1❩ ≘ f.
 #l2 @(nat_ind_succ … l2) -l2
 [ #l1 #f2 #Hf2 #f #Hf

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_nat_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_nat_tls.ma
index 421e8a0b40ce2bc8814d7e83493b4d0c9dc091b0..0aee27910bc86d1d7626c6c902fd4fe9a9f93b80 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_nat_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_nat_tls.ma
@@ -22,7 +22,7 @@ include "ground/relocation/pr_coafter.ma".
 
 (*** coafter_tls *)
 lemma pr_coafter_tls_bi_tls (n2) (n1):
-      ∀f1,f2,f. @↑❨n1, f1❩ ≘ n2 →
+      ∀f1,f2,f. ＠§❨n1, f1❩ ≘ n2 →
       f1 ~⊚ f2 ≘ f → ⫰*[n2]f1 ~⊚ ⫰*[n1]f2 ≘ ⫰*[n2]f.
 #n2 @(nat_ind_succ … n2) -n2 [ #n1 | #n2 #IH * [| #n1 ] ] #f1 #f2 #f #Hf1 #Hf
 [ elim (pr_nat_inv_zero_dx … Hf1) -Hf1 [ |*: // ] #g1 #Hg1 #H1 destruct //
@@ -40,6 +40,6 @@ qed.
 
 (*** coafter_tls_O *)
 lemma pr_coafter_tls_sn_tls:
-      ∀n,f1,f2,f. @↑❨𝟎, f1❩ ≘ n →
+      ∀n,f1,f2,f. ＠§❨𝟎, f1❩ ≘ n →
       f1 ~⊚ f2 ≘ f → ⫰*[n]f1 ~⊚ f2 ≘ ⫰*[n]f.
 /2 width=1 by pr_coafter_tls_bi_tls/ qed.

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_nat_tls_pushs.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_nat_tls_pushs.ma
index 1690ffe91ccc8a1798d636a6e789dd498fa00bb0..0dc77fb28e6fad96be997e5af71daa2f90ecf9b7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_nat_tls_pushs.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_nat_tls_pushs.ma
@@ -23,7 +23,7 @@ include "ground/relocation/pr_coafter.ma".
 
 (*** coafter_fwd_pushs *)
 lemma pr_coafter_des_pushs_dx (n) (m):
-      ∀g2,f1,g. g2 ~⊚ ⫯*[m]f1 ≘ g → @↑❨m, g2❩ ≘ n →
+      ∀g2,f1,g. g2 ~⊚ ⫯*[m]f1 ≘ g → ＠§❨m, g2❩ ≘ n →
       ∃∃f. ⫰*[n]g2 ~⊚ f1 ≘ f & ⫯*[n] f = g.
 #n @(nat_ind_succ … n) -n
 [ #m #g2 #f1 #g #Hg #H

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_nat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_nat.ma
index 2ca0a9f331ac00d35006f4cd085dff397c5710c7..d92d6cfcb91ad1a14560d4c39feb18d0b486ba24 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_nat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_nat.ma
@@ -19,15 +19,15 @@ include "ground/relocation/pr_isi_pat.ma".
 
 (* Advanced constructions with pr_isi and pr_nat ****************************)
 
-lemma pr_isi_nat (f): (∀l. @↑❨l,f❩ ≘ l) → 𝐈❨f❩.
+lemma pr_isi_nat (f): (∀l. ＠§❨l,f❩ ≘ l) → 𝐈❨f❩.
 /2 width=1 by pr_isi_pat/ qed.
 
 (* Inversions with pr_nat ***************************************************)
 
-lemma pr_isi_inv_nat (f) (l): 𝐈❨f❩ → @↑❨l,f❩ ≘ l.
+lemma pr_isi_inv_nat (f) (l): 𝐈❨f❩ → ＠§❨l,f❩ ≘ l.
 /2 width=1 by pr_isi_inv_pat/ qed-.
 
 (* Destructions with pr_nat *************************************************)
 
-lemma pr_isi_nat_des (f) (l1) (l2): 𝐈❨f❩ → @↑❨l1,f❩ ≘ l2 → l1 = l2.
+lemma pr_isi_nat_des (f) (l1) (l2): 𝐈❨f❩ → ＠§❨l1,f❩ ≘ l2 → l1 = l2.
 /3 width=3 by pr_isi_pat_des, eq_inv_npsucc_bi/ qed-.

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.ma
index a65f972bb89d9bb5dbd561c8094d3e30e88fdd13..dd2380cb726b1fbd8b532aa0e2e30c55a033769e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.ma
@@ -70,7 +70,7 @@ qed-.
 
 (* Advanced constructions with pr_nat ***************************************)
 
-lemma is_pr_nat_dec (f) (l2): 𝐓❨f❩ → Decidable (∃l1. @↑❨l1,f❩ ≘ l2).
+lemma is_pr_nat_dec (f) (l2): 𝐓❨f❩ → Decidable (∃l1. ＠§❨l1,f❩ ≘ l2).
 #f #l2 #Hf elim (is_pr_pat_dec … (↑l2) Hf)
 [ * /3 width=2 by ex_intro, or_introl/
 | #H @or_intror * /3 width=2 by ex_intro/

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat.ma
index 13154a1bb7249d1775c4c65771216de4f896d5c8..afe21c5e5ee896e3c025687a186702ea23a7cfdb 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/notation/relations/ratsucc_3.ma".
+include "ground/notation/relations/ratsection_3.ma".
 include "ground/arith/nat_pred_succ.ma".
 include "ground/relocation/pr_pat.ma".
 
@@ -23,30 +23,30 @@ definition pr_nat: relation3 pr_map nat nat ≝
 
 interpretation
   "relational non-negative application (partial relocation maps)"
-  'RAtSucc l1 f l2 = (pr_nat f l1 l2).
+  'RAtSection l1 f l2 = (pr_nat f l1 l2).
 
 (* Basic constructions ******************************************************)
 
 lemma pr_nat_refl (f) (g) (k1) (k2):
-      (⫯f) = g → 𝟎 = k1 → 𝟎 = k2 → @↑❨k1,g❩ ≘ k2.
+      (⫯f) = g → 𝟎 = k1 → 𝟎 = k2 → ＠§❨k1,g❩ ≘ k2.
 #f #g #k1 #k2 #H1 #H2 #H3 destruct
 /2 width=2 by pr_pat_refl/
 qed.
 
 lemma pr_nat_push (f) (l1) (l2) (g) (k1) (k2):
-      @↑❨l1,f❩ ≘ l2 → ⫯f = g → ↑l1 = k1 → ↑l2 = k2 → @↑❨k1,g❩ ≘ k2.
+      ＠§❨l1,f❩ ≘ l2 → ⫯f = g → ↑l1 = k1 → ↑l2 = k2 → ＠§❨k1,g❩ ≘ k2.
 #f #l1 #l2 #g #k1 #k2 #Hf #H1 #H2 #H3 destruct
 /2 width=7 by pr_pat_push/
 qed.
 
 lemma pr_nat_next (f) (l1) (l2) (g) (k2):
-      @↑❨l1,f❩ ≘ l2 → ↑f = g → ↑l2 = k2 → @↑❨l1,g❩ ≘ k2.
+      ＠§❨l1,f❩ ≘ l2 → ↑f = g → ↑l2 = k2 → ＠§❨l1,g❩ ≘ k2.
 #f #l1 #l2 #g #k2 #Hf #H1 #H2 destruct
 /2 width=5 by pr_pat_next/
 qed.
 
 lemma pr_nat_pred_bi (f) (i1) (i2):
-      ＠⧣❨i1,f❩ ≘ i2 → @↑❨↓i1,f❩ ≘ ↓i2.
+      ＠⧣❨i1,f❩ ≘ i2 → ＠§❨↓i1,f❩ ≘ ↓i2.
 #f #i1 #i2
 >(npsucc_pred i1) in ⊢ (%→?); >(npsucc_pred i2) in ⊢ (%→?);
 //
@@ -56,7 +56,7 @@ qed.
 
 (*** pr_nat_inv_ppx *)
 lemma pr_nat_inv_zero_push (f) (l1) (l2):
-      @↑❨l1,f❩ ≘ l2 → ∀g. 𝟎 = l1 → ⫯g = f → 𝟎 = l2.
+      ＠§❨l1,f❩ ≘ l2 → ∀g. 𝟎 = l1 → ⫯g = f → 𝟎 = l2.
 #f #l1 #l2 #H #g #H1 #H2 destruct
 lapply (pr_pat_inv_unit_push … H ???) -H
 /2 width=2 by eq_inv_npsucc_bi/
@@ -64,8 +64,8 @@ qed-.
 
 (*** pr_nat_inv_npx *)
 lemma pr_nat_inv_succ_push (f) (l1) (l2):
-      @↑❨l1,f❩ ≘ l2 → ∀g,k1. ↑k1 = l1 → ⫯g = f →
-      ∃∃k2. @↑❨k1,g❩ ≘ k2 & ↑k2 = l2.
+      ＠§❨l1,f❩ ≘ l2 → ∀g,k1. ↑k1 = l1 → ⫯g = f →
+      ∃∃k2. ＠§❨k1,g❩ ≘ k2 & ↑k2 = l2.
 #f #l1 #l2 #H #g #k1 #H1 #H2 destruct
 elim (pr_pat_inv_succ_push … H) -H [|*: // ] #k2 #Hg
 >(npsucc_pred (↑l2)) #H
@@ -74,8 +74,8 @@ qed-.
 
 (*** pr_nat_inv_xnx *)
 lemma pr_nat_inv_next (f) (l1) (l2):
-      @↑❨l1,f❩ ≘ l2 → ∀g. ↑g = f →
-      ∃∃k2. @↑❨l1,g❩ ≘ k2 & ↑k2 = l2.
+      ＠§❨l1,f❩ ≘ l2 → ∀g. ↑g = f →
+      ∃∃k2. ＠§❨l1,g❩ ≘ k2 & ↑k2 = l2.
 #f #l1 #l2 #H #g #H1 destruct
 elim (pr_pat_inv_next … H) -H [|*: // ] #k2
 >(npsucc_pred (k2)) in ⊢ (%→?→?); #Hg #H
@@ -86,50 +86,50 @@ qed-.
 
 (*** pr_nat_inv_ppn *)
 lemma pr_nat_inv_zero_push_succ (f) (l1) (l2):
-      @↑❨l1,f❩ ≘ l2 → ∀g,k2. 𝟎 = l1 → ⫯g = f → ↑k2 = l2 → ⊥.
+      ＠§❨l1,f❩ ≘ l2 → ∀g,k2. 𝟎 = l1 → ⫯g = f → ↑k2 = l2 → ⊥.
 #f #l1 #l2 #Hf #g #k2 #H1 #H <(pr_nat_inv_zero_push … Hf … H1 H) -f -g -l1 -l2
 /2 width=3 by eq_inv_nsucc_zero/
 qed-.
 
 (*** pr_nat_inv_npp *)
 lemma pr_nat_inv_succ_push_zero (f) (l1) (l2):
-      @↑❨l1,f❩ ≘ l2 → ∀g,k1. ↑k1 = l1 → ⫯g = f → 𝟎 = l2 → ⊥.
+      ＠§❨l1,f❩ ≘ l2 → ∀g,k1. ↑k1 = l1 → ⫯g = f → 𝟎 = l2 → ⊥.
 #f #l1 #l2 #Hf #g #k1 #H1 #H elim (pr_nat_inv_succ_push … Hf … H1 H) -f -l1
 #x2 #Hg * -l2 /2 width=3 by eq_inv_zero_nsucc/
 qed-.
 
 (*** pr_nat_inv_npn *)
 lemma pr_nat_inv_succ_push_succ (f) (l1) (l2):
-      @↑❨l1,f❩ ≘ l2 → ∀g,k1,k2. ↑k1 = l1 → ⫯g = f → ↑k2 = l2 → @↑❨k1,g❩ ≘ k2.
+      ＠§❨l1,f❩ ≘ l2 → ∀g,k1,k2. ↑k1 = l1 → ⫯g = f → ↑k2 = l2 → ＠§❨k1,g❩ ≘ k2.
 #f #l1 #l2 #Hf #g #k1 #k2 #H1 #H elim (pr_nat_inv_succ_push … Hf … H1 H) -f -l1
 #x2 #Hg * -l2 #H >(eq_inv_nsucc_bi … H) -k2 //
 qed-.
 
 (*** pr_nat_inv_xnp *)
 lemma pr_nat_inv_next_zero (f) (l1) (l2):
-      @↑❨l1,f❩ ≘ l2 → ∀g. ↑g = f → 𝟎 = l2 → ⊥.
+      ＠§❨l1,f❩ ≘ l2 → ∀g. ↑g = f → 𝟎 = l2 → ⊥.
 #f #l1 #l2 #Hf #g #H elim (pr_nat_inv_next … Hf … H) -f
 #x2 #Hg * -l2 /2 width=3 by eq_inv_zero_nsucc/
 qed-.
 
 (*** pr_nat_inv_xnn *)
 lemma pr_nat_inv_next_succ (f) (l1) (l2):
-      @↑❨l1,f❩ ≘ l2 → ∀g,k2. ↑g = f → ↑k2 = l2 → @↑❨l1,g❩ ≘ k2.
+      ＠§❨l1,f❩ ≘ l2 → ∀g,k2. ↑g = f → ↑k2 = l2 → ＠§❨l1,g❩ ≘ k2.
 #f #l1 #l2 #Hf #g #k2 #H elim (pr_nat_inv_next … Hf … H) -f
 #x2 #Hg * -l2 #H >(eq_inv_nsucc_bi … H) -k2 //
 qed-.
 
 (*** pr_nat_inv_pxp *)
 lemma pr_nat_inv_zero_bi (f) (l1) (l2):
-      @↑❨l1,f❩ ≘ l2 → 𝟎 = l1 → 𝟎 = l2 → ∃g. ⫯g = f.
+      ＠§❨l1,f❩ ≘ l2 → 𝟎 = l1 → 𝟎 = l2 → ∃g. ⫯g = f.
 #f elim (pr_map_split_tl … f) /2 width=2 by ex_intro/
 #H #l1 #l2 #Hf #H1 #H2 cases (pr_nat_inv_next_zero … Hf … H H2)
 qed-.
 
 (*** pr_nat_inv_pxn *)
 lemma pr_nat_inv_zero_succ (f) (l1) (l2):
-      @↑❨l1,f❩ ≘ l2 → ∀k2. 𝟎 = l1 → ↑k2 = l2 →
-      ∃∃g. @↑❨l1,g❩ ≘ k2 & ↑g = f.
+      ＠§❨l1,f❩ ≘ l2 → ∀k2. 𝟎 = l1 → ↑k2 = l2 →
+      ∃∃g. ＠§❨l1,g❩ ≘ k2 & ↑g = f.
 #f elim (pr_map_split_tl … f)
 #H #l1 #l2 #Hf #k2 #H1 #H2
 [ elim (pr_nat_inv_zero_push_succ … Hf … H1 H H2)
@@ -139,7 +139,7 @@ qed-.
 
 (*** pr_nat_inv_nxp *)
 lemma pr_nat_inv_succ_zero (f) (l1) (l2):
-      @↑❨l1,f❩ ≘ l2 → ∀k1. ↑k1 = l1 → 𝟎 = l2 → ⊥.
+      ＠§❨l1,f❩ ≘ l2 → ∀k1. ↑k1 = l1 → 𝟎 = l2 → ⊥.
 #f elim (pr_map_split_tl f)
 #H #l1 #l2 #Hf #k1 #H1 #H2
 [ elim (pr_nat_inv_succ_push_zero … Hf … H1 H H2)
@@ -149,9 +149,9 @@ qed-.
 
 (*** pr_nat_inv_nxn *)
 lemma pr_nat_inv_succ_bi (f) (l1) (l2):
-      @↑❨l1,f❩ ≘ l2 → ∀k1,k2. ↑k1 = l1 → ↑k2 = l2 →
-      ∨∨ ∃∃g. @↑❨k1,g❩ ≘ k2 & ⫯g = f
-       | ∃∃g. @↑❨l1,g❩ ≘ k2 & ↑g = f.
+      ＠§❨l1,f❩ ≘ l2 → ∀k1,k2. ↑k1 = l1 → ↑k2 = l2 →
+      ∨∨ ∃∃g. ＠§❨k1,g❩ ≘ k2 & ⫯g = f
+       | ∃∃g. ＠§❨l1,g❩ ≘ k2 & ↑g = f.
 #f elim (pr_map_split_tl f) *
 /4 width=7 by pr_nat_inv_next_succ, pr_nat_inv_succ_push_succ, ex2_intro, or_intror, or_introl/
 qed-.
@@ -159,9 +159,9 @@ qed-.
 (* Note: the following inversion lemmas must be checked *)
 (*** pr_nat_inv_xpx *)
 lemma pr_nat_inv_push (f) (l1) (l2):
-      @↑❨l1,f❩ ≘ l2 → ∀g. ⫯g = f →
+      ＠§❨l1,f❩ ≘ l2 → ∀g. ⫯g = f →
       ∨∨ ∧∧ 𝟎 = l1 & 𝟎 = l2
-       | ∃∃k1,k2. @↑❨k1,g❩ ≘ k2 & ↑k1 = l1 & ↑k2 = l2.
+       | ∃∃k1,k2. ＠§❨k1,g❩ ≘ k2 & ↑k1 = l1 & ↑k2 = l2.
 #f * [2: #l1 ] #l2 #Hf #g #H
 [ elim (pr_nat_inv_succ_push … Hf … H) -f /3 width=5 by or_intror, ex3_2_intro/
 | >(pr_nat_inv_zero_push … Hf … H) -f /3 width=1 by conj, or_introl/
@@ -170,15 +170,15 @@ qed-.
 
 (*** pr_nat_inv_xpp *)
 lemma pr_nat_inv_push_zero (f) (l1) (l2):
-      @↑❨l1,f❩ ≘ l2 → ∀g. ⫯g = f → 𝟎 = l2 → 𝟎 = l1.
+      ＠§❨l1,f❩ ≘ l2 → ∀g. ⫯g = f → 𝟎 = l2 → 𝟎 = l1.
 #f #l1 #l2 #Hf #g #H elim (pr_nat_inv_push … Hf … H) -f * //
 #k1 #k2 #_ #_ * -l2 #H elim (eq_inv_zero_nsucc … H)
 qed-.
 
 (*** pr_nat_inv_xpn *)
 lemma pr_nat_inv_push_succ (f) (l1) (l2):
-      @↑❨l1,f❩ ≘ l2 → ∀g,k2. ⫯g = f → ↑k2 = l2 →
-      ∃∃k1. @↑❨k1,g❩ ≘ k2 & ↑k1 = l1.
+      ＠§❨l1,f❩ ≘ l2 → ∀g,k2. ⫯g = f → ↑k2 = l2 →
+      ∃∃k1. ＠§❨k1,g❩ ≘ k2 & ↑k1 = l1.
 #f #l1 #l2 #Hf #g #k2 #H elim (pr_nat_inv_push … Hf … H) -f *
 [ #_ * -l2 #H elim (eq_inv_nsucc_zero … H)
 | #x1 #x2 #Hg #H1 * -l2 #H
@@ -189,7 +189,7 @@ qed-.
 
 (*** pr_nat_inv_xxp *)
 lemma pr_nat_inv_zero_dx (f) (l1) (l2):
-      @↑❨l1,f❩ ≘ l2 → 𝟎 = l2 → ∃∃g. 𝟎 = l1 & ⫯g = f.
+      ＠§❨l1,f❩ ≘ l2 → 𝟎 = l2 → ∃∃g. 𝟎 = l1 & ⫯g = f.
 #f elim (pr_map_split_tl f)
 #H #l1 #l2 #Hf #H2
 [ /3 width=6 by pr_nat_inv_push_zero, ex2_intro/
@@ -198,9 +198,9 @@ lemma pr_nat_inv_zero_dx (f) (l1) (l2):
 qed-.
 
 (*** pr_nat_inv_xxn *)
-lemma pr_nat_inv_succ_dx (f) (l1) (l2): @↑❨l1,f❩ ≘ l2 → ∀k2.  ↑k2 = l2 →
-      ∨∨ ∃∃g,k1. @↑❨k1,g❩ ≘ k2 & ↑k1 = l1 & ⫯g = f
-       | ∃∃g. @↑❨l1,g❩ ≘ k2 & ↑g = f.
+lemma pr_nat_inv_succ_dx (f) (l1) (l2): ＠§❨l1,f❩ ≘ l2 → ∀k2.  ↑k2 = l2 →
+      ∨∨ ∃∃g,k1. ＠§❨k1,g❩ ≘ k2 & ↑k1 = l1 & ⫯g = f
+       | ∃∃g. ＠§❨l1,g❩ ≘ k2 & ↑g = f.
 #f elim (pr_map_split_tl f)
 #H #l1 #l2 #Hf #k2 #H2
 [ elim (pr_nat_inv_push_succ … Hf … H H2) -l2 /3 width=5 by or_introl, ex3_2_intro/

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat_basic.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat_basic.ma
index edb5117aa928a021feca82f3d0df7c7036f993d2..9c93c6e237ba2d9d61e995106780d17337675547 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat_basic.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat_basic.ma
@@ -20,7 +20,7 @@ include "ground/relocation/pr_nat_uni.ma".
 (* Constructions with pr_basic **********************************************)
 
 lemma pr_nat_basic_lt (m) (n) (l):
-      l < m → @↑❨l, 𝐛❨m,n❩❩ ≘ l.
+      l < m → ＠§❨l, 𝐛❨m,n❩❩ ≘ l.
 #m @(nat_ind_succ … m) -m
 [ #n #i #H elim (nlt_inv_zero_dx … H)
 | #m #IH #n #l @(nat_ind_succ … l) -l
@@ -33,7 +33,7 @@ lemma pr_nat_basic_lt (m) (n) (l):
 qed.
 
 lemma pr_nat_basic_ge (m) (n) (l):
-      m ≤ l → @↑❨l, 𝐛❨m,n❩❩ ≘ l+n.
+      m ≤ l → ＠§❨l, 𝐛❨m,n❩❩ ≘ l+n.
 #m @(nat_ind_succ … m) -m //
 #m #IH #n #l #H
 elim (nle_inv_succ_sn … H) -H #Hml #H >H -H
@@ -43,9 +43,9 @@ qed.
 (* Inversions with pr_basic *************************************************)
 
 lemma pr_nat_basic_inv_lt (m) (n) (l) (k):
-      l < m → @↑❨l, 𝐛❨m,n❩❩ ≘ k → l = k.
+      l < m → ＠§❨l, 𝐛❨m,n❩❩ ≘ k → l = k.
 /3 width=4 by pr_nat_basic_lt, pr_nat_mono/ qed-.
 
 lemma pr_nat_basic_inv_ge (m) (n) (l) (k):
-      m ≤ l → @↑❨l, 𝐛❨m,n❩❩ ≘ k → l+n = k.
+      m ≤ l → ＠§❨l, 𝐛❨m,n❩❩ ≘ k → l+n = k.
 /3 width=4 by pr_nat_basic_ge, pr_nat_mono/ qed-.

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat_nat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat_nat.ma
index 481ff1517b32ba7b414dd34db594ea48217ab985..cfba24b077b43cc774bd4c86a18f2f377166468a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat_nat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat_nat.ma
@@ -20,7 +20,7 @@ include "ground/relocation/pr_nat.ma".
 (* Main destructions ********************************************************)
 
 theorem pr_nat_monotonic (k2) (l2) (f):
-        @↑❨l2,f❩ ≘ k2 → ∀k1,l1. @↑❨l1,f❩ ≘ k1 → l1 < l2 → k1 < k2.
+        ＠§❨l2,f❩ ≘ k2 → ∀k1,l1. ＠§❨l1,f❩ ≘ k1 → l1 < l2 → k1 < k2.
 #k2 @(nat_ind_succ … k2) -k2
 [ #l2 #f #H2f elim (pr_nat_inv_zero_dx … H2f) -H2f //
   #g #H21 #_ #k1 #l1 #_ #Hi destruct
@@ -37,7 +37,7 @@ theorem pr_nat_monotonic (k2) (l2) (f):
 qed-.
 
 theorem pr_nat_inv_monotonic (k1) (l1) (f):
-        @↑❨l1,f❩ ≘ k1 → ∀k2,l2. @↑❨l2,f❩ ≘ k2 → k1 < k2 → l1 < l2.
+        ＠§❨l1,f❩ ≘ k1 → ∀k2,l2. ＠§❨l2,f❩ ≘ k2 → k1 < k2 → l1 < l2.
 #k1 @(nat_ind_succ … k1) -k1
 [ #l1 #f #H1f elim (pr_nat_inv_zero_dx … H1f) -H1f //
   #g * -l1 #H #k2 #l2 #H2f #Hk
@@ -59,14 +59,14 @@ theorem pr_nat_inv_monotonic (k1) (l1) (f):
 qed-.
 
 theorem pr_nat_mono (f) (l) (l1) (l2):
-        @↑❨l,f❩ ≘ l1 → @↑❨l,f❩ ≘ l2 → l2 = l1.
+        ＠§❨l,f❩ ≘ l1 → ＠§❨l,f❩ ≘ l2 → l2 = l1.
 #f #l #l1 #l2 #H1 #H2 elim (nat_split_lt_eq_gt l2 l1) //
 #Hi elim (nlt_ge_false l l)
 /2 width=6 by pr_nat_inv_monotonic/
 qed-.
 
 theorem pr_nat_inj (f) (l1) (l2) (l):
-        @↑❨l1,f❩ ≘ l → @↑❨l2,f❩ ≘ l → l1 = l2.
+        ＠§❨l1,f❩ ≘ l → ＠§❨l2,f❩ ≘ l → l1 = l2.
 #f #l1 #l2 #l #H1 #H2 elim (nat_split_lt_eq_gt l2 l1) //
 #Hi elim (nlt_ge_false l l)
 /2 width=6 by pr_nat_monotonic/

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat_uni.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat_uni.ma
index 11428480504ce46de89427c3f86d98efd2fb9b8a..8b0f308417321504c0335c544e5cb549dcce96b5 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat_uni.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat_uni.ma
@@ -21,12 +21,12 @@ include "ground/relocation/pr_nat_nat.ma".
 (* Constructions with pr_uni ************************************************)
 
 lemma pr_nat_uni (n) (l):
-      @↑❨l,𝐮❨n❩❩ ≘ l+n.
+      ＠§❨l,𝐮❨n❩❩ ≘ l+n.
 /2 width=1 by pr_nat_pred_bi/
 qed.
 
 (* Inversions with pr_uni ***************************************************)
 
 lemma pr_nat_inv_uni (n) (l) (k):
-      @↑❨l,𝐮❨n❩❩ ≘ k → k = l+n.
+      ＠§❨l,𝐮❨n❩❩ ≘ k → k = l+n.
 /2 width=4 by pr_nat_mono/ qed-.

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma
index 073ffed7f560ae726941a9a370d576d02d81381d..aef0c26e158b9db9e18d6d6be952a6c6a385a17e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma
@@ -1,20 +1,19 @@
-
 (**) (* reverse include *)
 include "ground/arith/nat_rplus_pplus.ma".
 include "ground/relocation/tr_pn_eq.ma".
 include "ground/relocation/tr_compose_pn.ma".
 include "ground/relocation/nap.ma".
-include "ground/notation/functions/apply_2.ma".
+include "ground/notation/functions/at_2.ma".
 
 definition tr_xap (f) (l:nat): nat ≝
-           (⫯f)@↑❨l❩.
+           (⫯f)＠§❨l❩.
 
 interpretation
   "functional extended application (total relocation maps)"
-  'Apply f l = (tr_xap f l).
+  'At f l = (tr_xap f l).
 
 lemma tr_xap_unfold (f) (l):
-      (⫯f)@↑❨l❩ = f＠❨l❩.
+      (⫯f)＠§❨l❩ = f＠❨l❩.
 // qed.
 
 lemma tr_xap_zero (f):
@@ -26,7 +25,7 @@ lemma tr_xap_ninj (f) (p):
 // qed.
 
 lemma tr_xap_succ_nap (f) (n):
-      ↑(f@↑❨n❩) = f＠❨↑n❩.
+      ↑(f＠§❨n❩) = f＠❨↑n❩.
 #f #n
 <tr_xap_ninj //
 qed.

diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
index 9fed47266cd5eb7ba39dc1bd477eb20c89280916..80d76fbe080bb36c23b8bf8843154458454e9945 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
@@ -52,7 +52,7 @@ table {
           [ "pr_fcla ( 𝐂❨?❩ ≘ ? )" "pr_fcla_eq" "fcla_uni" "pr_fcla_fcla" * ]
           [ "pr_isu ( 𝐔❨?❩ )" "pr_isu_tl" "pr_isu_uni" * ]
           [ "pr_isi ( 𝐈❨?❩ )" "pr_isi_eq" "pr_isi_tl" "pr_isi_pushs" "pr_isi_tls" "pr_isi_id" "pr_isi_uni" "pr_isi_pat" "pr_isi_nat" * ]
-          [ "pr_nat ( @↑❨?,?❩ ≘ ? )" "pr_nat_uni" "pr_nat_basic" "pr_nat_nat" * ]
+          [ "pr_nat ( ＠§❨?,?❩ ≘ ? )" "pr_nat_uni" "pr_nat_basic" "pr_nat_nat" * ]
           [ "pr_pat ( ＠⧣❨?,?❩ ≘ ? )" "pr_pat_lt" "pr_pat_eq" "pr_pat_tls" "pr_pat_id" "pr_pat_uni" "pr_pat_basic" "pr_pat_pat" "pr_pat_pat_id" * ]
           [ "pr_basic ( 𝐛❨?,?❩ )" * ]
           [ "pr_uni ( 𝐮❨?❩ )" "pr_uni_eq" * ]