update in ground static_2 basic_2 apps_2

[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 263da6c13ed8dcd46fa1f595fb145eabfc050c6a..104d37c74dbf6c12e7d1f9d5470f514371833fb7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat.ma
@@ -39,14 +39,14 @@ interpretation
 (*** H_at_div *)
 definition H_pr_pat_div: relation4 pr_map pr_map pr_map pr_map ≝
            λf2,g2,f1,g1.
-           â\88\80jf,jg,j. @â\9dªjf,f2â\9d« â\89\98 j â\86\92 @â\9dªjg,g2â\9d« ≘ j →
-           â\88\83â\88\83j0. @â\9dªj0,f1â\9d« â\89\98 jf & @â\9dªj0,g1â\9d« ≘ jg.
+           â\88\80jf,jg,j. @â\9d¨jf,f2â\9d© â\89\98 j â\86\92 @â\9d¨jg,g2â\9d© ≘ j →
+           â\88\83â\88\83j0. @â\9d¨j0,f1â\9d© â\89\98 jf & @â\9d¨j0,g1â\9d© ≘ jg.
 
 (* Basic inversions *********************************************************)
 
 (*** at_inv_ppx *)
 lemma pr_pat_inv_unit_push (f) (i1) (i2):
-      @â\9dªi1,fâ\9d« ≘ i2 → ∀g. 𝟏 = i1 → ⫯g = f → 𝟏 = i2.
+      @â\9d¨i1,fâ\9d© ≘ 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):
-      @â\9dªi1,fâ\9d« ≘ i2 → ∀g,j1. ↑j1 = i1 → ⫯g = f →
-      â\88\83â\88\83j2. @â\9dªj1,gâ\9d« ≘ j2 & ↑j2 = i2.
+      @â\9d¨i1,fâ\9d© ≘ i2 → ∀g,j1. ↑j1 = i1 → ⫯g = f →
+      â\88\83â\88\83j2. @â\9d¨j1,gâ\9d© ≘ 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):
-      @â\9dªi1,fâ\9d« ≘ i2 → ∀g. ↑g = f →
-      â\88\83â\88\83j2. @â\9dªi1,gâ\9d« ≘ j2 & ↑j2 = i2.
+      @â\9d¨i1,fâ\9d© ≘ i2 → ∀g. ↑g = f →
+      â\88\83â\88\83j2. @â\9d¨i1,gâ\9d© ≘ 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):
-      @â\9dªi1,fâ\9d« ≘ i2 → ∀g,j2. 𝟏 = i1 → ⫯g = f → ↑j2 = i2 → ⊥.
+      @â\9d¨i1,fâ\9d© ≘ 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):
-      @â\9dªi1,fâ\9d« ≘ i2 → ∀g,j1. ↑j1 = i1 → ⫯g = f → 𝟏 = i2 → ⊥.
+      @â\9d¨i1,fâ\9d© ≘ 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):
-      @â\9dªi1,fâ\9d« â\89\98 i2 â\86\92 â\88\80g,j1,j2. â\86\91j1 = i1 â\86\92 ⫯g = f â\86\92 â\86\91j2 = i2 â\86\92 @â\9dªj1,gâ\9d« ≘ j2.
+      @â\9d¨i1,fâ\9d© â\89\98 i2 â\86\92 â\88\80g,j1,j2. â\86\91j1 = i1 â\86\92 ⫯g = f â\86\92 â\86\91j2 = i2 â\86\92 @â\9d¨j1,gâ\9d© ≘ 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):
-      @â\9dªi1,fâ\9d« ≘ i2 → ∀g. ↑g = f → 𝟏 = i2 → ⊥.
+      @â\9d¨i1,fâ\9d© ≘ 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):
-      @â\9dªi1,fâ\9d« â\89\98 i2 â\86\92 â\88\80g,j2. â\86\91g = f â\86\92 â\86\91j2 = i2 â\86\92 @â\9dªi1,gâ\9d« ≘ j2.
+      @â\9d¨i1,fâ\9d© â\89\98 i2 â\86\92 â\88\80g,j2. â\86\91g = f â\86\92 â\86\91j2 = i2 â\86\92 @â\9d¨i1,gâ\9d© ≘ 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):
-      @â\9dªi1,fâ\9d« ≘ i2 → 𝟏 = i1 → 𝟏 = i2 → ∃g. ⫯g = f.
+      @â\9d¨i1,fâ\9d© ≘ 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):
-      @â\9dªi1,fâ\9d« ≘ i2 → ∀j2. 𝟏 = i1 → ↑j2 = i2 →
-      â\88\83â\88\83g. @â\9dªi1,gâ\9d« ≘ j2 & ↑g = f.
+      @â\9d¨i1,fâ\9d© ≘ i2 → ∀j2. 𝟏 = i1 → ↑j2 = i2 →
+      â\88\83â\88\83g. @â\9d¨i1,gâ\9d© ≘ 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):
-      @â\9dªi1,fâ\9d« ≘ i2 → ∀j1. ↑j1 = i1 → 𝟏 = i2 → ⊥.
+      @â\9d¨i1,fâ\9d© ≘ 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):
-      @â\9dªi1,fâ\9d« ≘ i2 → ∀j1,j2. ↑j1 = i1 → ↑j2 = i2 →
-      â\88¨â\88¨ â\88\83â\88\83g. @â\9dªj1,gâ\9d« ≘ j2 & ⫯g = f
-       | â\88\83â\88\83g. @â\9dªi1,gâ\9d« ≘ j2 & ↑g = f.
+      @â\9d¨i1,fâ\9d© ≘ i2 → ∀j1,j2. ↑j1 = i1 → ↑j2 = i2 →
+      â\88¨â\88¨ â\88\83â\88\83g. @â\9d¨j1,gâ\9d© ≘ j2 & ⫯g = f
+       | â\88\83â\88\83g. @â\9d¨i1,gâ\9d© ≘ 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):
-      @â\9dªi1,fâ\9d« ≘ i2 → ∀g. ⫯g = f →
+      @â\9d¨i1,fâ\9d© ≘ i2 → ∀g. ⫯g = f →
       ∨∨ ∧∧ 𝟏 = i1 & 𝟏 = i2
-       | â\88\83â\88\83j1,j2. @â\9dªj1,gâ\9d« ≘ j2 & ↑j1 = i1 & ↑j2 = i2.
+       | â\88\83â\88\83j1,j2. @â\9d¨j1,gâ\9d© ≘ 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):
-      @â\9dªi1,fâ\9d« ≘ i2 → ∀g. ⫯g = f → 𝟏 = i2 → 𝟏 = i1.
+      @â\9d¨i1,fâ\9d© ≘ 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):
-      @â\9dªi1,fâ\9d« ≘ i2 → ∀g,j2. ⫯g = f → ↑j2 = i2 →
-      â\88\83â\88\83j1. @â\9dªj1,gâ\9d« ≘ j2 & ↑j1 = i1.
+      @â\9d¨i1,fâ\9d© ≘ i2 → ∀g,j2. ⫯g = f → ↑j2 = i2 →
+      â\88\83â\88\83j1. @â\9d¨j1,gâ\9d© ≘ 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):
-      @â\9dªi1,fâ\9d« ≘ i2 → 𝟏 = i2 →
+      @â\9d¨i1,fâ\9d© ≘ 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):
-      @â\9dªi1,fâ\9d« ≘ i2 → ∀j2.  ↑j2 = i2 →
-      â\88¨â\88¨ â\88\83â\88\83g,j1. @â\9dªj1,gâ\9d« ≘ j2 & ↑j1 = i1 & ⫯g = f
-       | â\88\83â\88\83g. @â\9dªi1,gâ\9d« ≘ j2 & ↑g = f.
+      @â\9d¨i1,fâ\9d© ≘ i2 → ∀j2.  ↑j2 = i2 →
+      â\88¨â\88¨ â\88\83â\88\83g,j1. @â\9d¨j1,gâ\9d© ≘ j2 & ↑j1 = i1 & ⫯g = f
+       | â\88\83â\88\83g. @â\9d¨i1,gâ\9d© ≘ 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/