update in ground

[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / pr_pat.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat.ma
index 104d37c74dbf6c12e7d1f9d5470f514371833fb7..0eee75321d6d5c3a40da8f1ae68b9535ff7a9d77 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/notation/relations/rat_3.ma".
+include "ground/notation/relations/ratsharp_3.ma".
 include "ground/xoa/ex_3_2.ma".
 include "ground/arith/pnat.ma".
 include "ground/relocation/pr_tl.ma".
@@ -34,19 +34,19 @@ coinductive pr_pat: relation3 pr_map pnat pnat ≝
 
 interpretation
   "relational positive application (partial relocation maps)"
-  'RAt i1 f i2 = (pr_pat f i1 i2).
+  'RAtSharp i1 f i2 = (pr_pat f i1 i2).
 
 (*** H_at_div *)
 definition H_pr_pat_div: relation4 pr_map pr_map pr_map pr_map ≝
            λf2,g2,f1,g1.
-           ∀jf,jg,j. @❨jf,f2❩ ≘ j → @❨jg,g2❩ ≘ j →
-           ∃∃j0. @❨j0,f1❩ ≘ jf & @❨j0,g1❩ ≘ jg.
+           ∀jf,jg,j. ＠⧣❨jf,f2❩ ≘ j → ＠⧣❨jg,g2❩ ≘ j →
+           ∃∃j0. ＠⧣❨j0,f1❩ ≘ jf & ＠⧣❨j0,g1❩ ≘ jg.
 
 (* Basic inversions *********************************************************)
 
 (*** at_inv_ppx *)
 lemma pr_pat_inv_unit_push (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → ∀g. 𝟏 = i1 → ⫯g = f → 𝟏 = i2.
+      ＠⧣❨i1,f❩ ≘ i2 → ∀g. 𝟏 = i1 → ⫯g = f → 𝟏 = i2.
 #f #i1 #i2 * -f -i1 -i2 //
 [ #f #i1 #i2 #_ #g #j1 #j2 #_ * #_ #x #H destruct
 | #f #i1 #i2 #_ #g #j2 * #_ #x #_ #H elim (eq_inv_pr_push_next … H)
@@ -55,8 +55,8 @@ qed-.
 
 (*** at_inv_npx *)
 lemma pr_pat_inv_succ_push (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → ∀g,j1. ↑j1 = i1 → ⫯g = f →
-      ∃∃j2. @❨j1,g❩ ≘ j2 & ↑j2 = i2.
+      ＠⧣❨i1,f❩ ≘ i2 → ∀g,j1. ↑j1 = i1 → ⫯g = f →
+      ∃∃j2. ＠⧣❨j1,g❩ ≘ j2 & ↑j2 = i2.
 #f #i1 #i2 * -f -i1 -i2
 [ #f #g #j1 #j2 #_ * #_ #x #x1 #H destruct
 | #f #i1 #i2 #Hi #g #j1 #j2 * * * #x #x1 #H #Hf >(eq_inv_pr_push_bi … Hf) -g destruct /2 width=3 by ex2_intro/
@@ -66,8 +66,8 @@ qed-.
 
 (*** at_inv_xnx *)
 lemma pr_pat_inv_next (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → ∀g. ↑g = f →
-      ∃∃j2. @❨i1,g❩ ≘ j2 & ↑j2 = i2.
+      ＠⧣❨i1,f❩ ≘ i2 → ∀g. ↑g = f →
+      ∃∃j2. ＠⧣❨i1,g❩ ≘ j2 & ↑j2 = i2.
 #f #i1 #i2 * -f -i1 -i2
 [ #f #g #j1 #j2 * #_ #_ #x #H elim (eq_inv_pr_next_push … H)
 | #f #i1 #i2 #_ #g #j1 #j2 * #_ #_ #x #H elim (eq_inv_pr_next_push … H)
@@ -79,50 +79,50 @@ qed-.
 
 (*** at_inv_ppn *)
 lemma pr_pat_inv_unit_push_succ (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → ∀g,j2. 𝟏 = i1 → ⫯g = f → ↑j2 = i2 → ⊥.
+      ＠⧣❨i1,f❩ ≘ i2 → ∀g,j2. 𝟏 = i1 → ⫯g = f → ↑j2 = i2 → ⊥.
 #f #i1 #i2 #Hf #g #j2 #H1 #H <(pr_pat_inv_unit_push … Hf … H1 H) -f -g -i1 -i2
 #H destruct
 qed-.
 
 (*** at_inv_npp *)
 lemma pr_pat_inv_succ_push_unit (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → ∀g,j1. ↑j1 = i1 → ⫯g = f → 𝟏 = i2 → ⊥.
+      ＠⧣❨i1,f❩ ≘ i2 → ∀g,j1. ↑j1 = i1 → ⫯g = f → 𝟏 = i2 → ⊥.
 #f #i1 #i2 #Hf #g #j1 #H1 #H elim (pr_pat_inv_succ_push … Hf … H1 H) -f -i1
 #x2 #Hg * -i2 #H destruct
 qed-.
 
 (*** at_inv_npn *)
 lemma pr_pat_inv_succ_push_succ (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → ∀g,j1,j2. ↑j1 = i1 → ⫯g = f → ↑j2 = i2 → @❨j1,g❩ ≘ j2.
+      ＠⧣❨i1,f❩ ≘ i2 → ∀g,j1,j2. ↑j1 = i1 → ⫯g = f → ↑j2 = i2 → ＠⧣❨j1,g❩ ≘ j2.
 #f #i1 #i2 #Hf #g #j1 #j2 #H1 #H elim (pr_pat_inv_succ_push … Hf … H1 H) -f -i1
 #x2 #Hg * -i2 #H destruct //
 qed-.
 
 (*** at_inv_xnp *)
 lemma pr_pat_inv_next_unit (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → ∀g. ↑g = f → 𝟏 = i2 → ⊥.
+      ＠⧣❨i1,f❩ ≘ i2 → ∀g. ↑g = f → 𝟏 = i2 → ⊥.
 #f #i1 #i2 #Hf #g #H elim (pr_pat_inv_next … Hf … H) -f
 #x2 #Hg * -i2 #H destruct
 qed-.
 
 (*** at_inv_xnn *)
 lemma pr_pat_inv_next_succ (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → ∀g,j2. ↑g = f → ↑j2 = i2 → @❨i1,g❩ ≘ j2.
+      ＠⧣❨i1,f❩ ≘ i2 → ∀g,j2. ↑g = f → ↑j2 = i2 → ＠⧣❨i1,g❩ ≘ j2.
 #f #i1 #i2 #Hf #g #j2 #H elim (pr_pat_inv_next … Hf … H) -f
 #x2 #Hg * -i2 #H destruct //
 qed-.
 
 (*** at_inv_pxp *)
 lemma pr_pat_inv_unit_bi (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → 𝟏 = i1 → 𝟏 = i2 → ∃g. ⫯g = f.
+      ＠⧣❨i1,f❩ ≘ i2 → 𝟏 = i1 → 𝟏 = i2 → ∃g. ⫯g = f.
 #f elim (pr_map_split_tl … f) /2 width=2 by ex_intro/
 #H #i1 #i2 #Hf #H1 #H2 cases (pr_pat_inv_next_unit … Hf … H H2)
 qed-.
 
 (*** at_inv_pxn *)
 lemma pr_pat_inv_unit_succ (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → ∀j2. 𝟏 = i1 → ↑j2 = i2 →
-      ∃∃g. @❨i1,g❩ ≘ j2 & ↑g = f.
+      ＠⧣❨i1,f❩ ≘ i2 → ∀j2. 𝟏 = i1 → ↑j2 = i2 →
+      ∃∃g. ＠⧣❨i1,g❩ ≘ j2 & ↑g = f.
 #f elim (pr_map_split_tl … f)
 #H #i1 #i2 #Hf #j2 #H1 #H2
 [ elim (pr_pat_inv_unit_push_succ … Hf … H1 H H2)
@@ -132,7 +132,7 @@ qed-.
 
 (*** at_inv_nxp *)
 lemma pr_pat_inv_succ_unit (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → ∀j1. ↑j1 = i1 → 𝟏 = i2 → ⊥.
+      ＠⧣❨i1,f❩ ≘ i2 → ∀j1. ↑j1 = i1 → 𝟏 = i2 → ⊥.
 #f elim (pr_map_split_tl f)
 #H #i1 #i2 #Hf #j1 #H1 #H2
 [ elim (pr_pat_inv_succ_push_unit … Hf … H1 H H2)
@@ -142,9 +142,9 @@ qed-.
 
 (*** at_inv_nxn *)
 lemma pr_pat_inv_succ_bi (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → ∀j1,j2. ↑j1 = i1 → ↑j2 = i2 →
-      ∨∨ ∃∃g. @❨j1,g❩ ≘ j2 & ⫯g = f
-       | ∃∃g. @❨i1,g❩ ≘ j2 & ↑g = f.
+      ＠⧣❨i1,f❩ ≘ i2 → ∀j1,j2. ↑j1 = i1 → ↑j2 = i2 →
+      ∨∨ ∃∃g. ＠⧣❨j1,g❩ ≘ j2 & ⫯g = f
+       | ∃∃g. ＠⧣❨i1,g❩ ≘ j2 & ↑g = f.
 #f elim (pr_map_split_tl f) *
 /4 width=7 by pr_pat_inv_next_succ, pr_pat_inv_succ_push_succ, ex2_intro, or_intror, or_introl/
 qed-.
@@ -152,9 +152,9 @@ qed-.
 (* Note: the following inversion lemmas must be checked *)
 (*** at_inv_xpx *)
 lemma pr_pat_inv_push (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → ∀g. ⫯g = f →
+      ＠⧣❨i1,f❩ ≘ i2 → ∀g. ⫯g = f →
       ∨∨ ∧∧ 𝟏 = i1 & 𝟏 = i2
-       | ∃∃j1,j2. @❨j1,g❩ ≘ j2 & ↑j1 = i1 & ↑j2 = i2.
+       | ∃∃j1,j2. ＠⧣❨j1,g❩ ≘ j2 & ↑j1 = i1 & ↑j2 = i2.
 #f * [2: #i1 ] #i2 #Hf #g #H
 [ elim (pr_pat_inv_succ_push … Hf … H) -f /3 width=5 by or_intror, ex3_2_intro/
 | >(pr_pat_inv_unit_push … Hf … H) -f /3 width=1 by conj, or_introl/
@@ -163,15 +163,15 @@ qed-.
 
 (*** at_inv_xpp *)
 lemma pr_pat_inv_push_unit (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → ∀g. ⫯g = f → 𝟏 = i2 → 𝟏 = i1.
+      ＠⧣❨i1,f❩ ≘ i2 → ∀g. ⫯g = f → 𝟏 = i2 → 𝟏 = i1.
 #f #i1 #i2 #Hf #g #H elim (pr_pat_inv_push … Hf … H) -f * //
 #j1 #j2 #_ #_ * -i2 #H destruct
 qed-.
 
 (*** at_inv_xpn *)
 lemma pr_pat_inv_push_succ (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → ∀g,j2. ⫯g = f → ↑j2 = i2 →
-      ∃∃j1. @❨j1,g❩ ≘ j2 & ↑j1 = i1.
+      ＠⧣❨i1,f❩ ≘ i2 → ∀g,j2. ⫯g = f → ↑j2 = i2 →
+      ∃∃j1. ＠⧣❨j1,g❩ ≘ j2 & ↑j1 = i1.
 #f #i1 #i2 #Hf #g #j2 #H elim (pr_pat_inv_push … Hf … H) -f *
 [ #_ * -i2 #H destruct
 | #x1 #x2 #Hg #H1 * -i2 #H destruct /2 width=3 by ex2_intro/
@@ -180,7 +180,7 @@ qed-.
 
 (*** at_inv_xxp *)
 lemma pr_pat_inv_unit_dx (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → 𝟏 = i2 →
+      ＠⧣❨i1,f❩ ≘ i2 → 𝟏 = i2 →
       ∃∃g. 𝟏 = i1 & ⫯g = f.
 #f elim (pr_map_split_tl f)
 #H #i1 #i2 #Hf #H2
@@ -191,9 +191,9 @@ qed-.
 
 (*** at_inv_xxn *)
 lemma pr_pat_inv_succ_dx (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → ∀j2.  ↑j2 = i2 →
-      ∨∨ ∃∃g,j1. @❨j1,g❩ ≘ j2 & ↑j1 = i1 & ⫯g = f
-       | ∃∃g. @❨i1,g❩ ≘ j2 & ↑g = f.
+      ＠⧣❨i1,f❩ ≘ i2 → ∀j2.  ↑j2 = i2 →
+      ∨∨ ∃∃g,j1. ＠⧣❨j1,g❩ ≘ j2 & ↑j1 = i1 & ⫯g = f
+       | ∃∃g. ＠⧣❨i1,g❩ ≘ j2 & ↑g = f.
 #f elim (pr_map_split_tl f)
 #H #i1 #i2 #Hf #j2 #H2
 [ elim (pr_pat_inv_push_succ … Hf … H H2) -i2 /3 width=5 by or_introl, ex3_2_intro/