X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Frtmap_sdj.ma;h=330ad6e98104d133a058d4b940b828cd9a5960ab;hb=bd53c4e895203eb049e75434f638f26b5a161a2b;hp=99c6915dbcd38b8485a7bb20eedd2cf69b8a82fb;hpb=cafb43926d8553c5b7f8dafcb5d734783c19bbfb;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sdj.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sdj.ma
index 99c6915db..330ad6e98 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sdj.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sdj.ma
@@ -18,9 +18,9 @@ include "ground_2/relocation/rtmap_isid.ma".
 (* RELOCATION MAP ***********************************************************)
 
 coinductive sdj: relation rtmap ≝
-| sdj_pp: ∀f1,f2,g1,g2. sdj f1 f2 → ↑f1 = g1 → ↑f2 = g2 → sdj g1 g2
-| sdj_np: ∀f1,f2,g1,g2. sdj f1 f2 → ⫯f1 = g1 → ↑f2 = g2 → sdj g1 g2
-| sdj_pn: ∀f1,f2,g1,g2. sdj f1 f2 → ↑f1 = g1 → ⫯f2 = g2 → sdj g1 g2
+| sdj_pp: ∀f1,f2,g1,g2. sdj f1 f2 → ⫯f1 = g1 → ⫯f2 = g2 → sdj g1 g2
+| sdj_np: ∀f1,f2,g1,g2. sdj f1 f2 → ↑f1 = g1 → ⫯f2 = g2 → sdj g1 g2
+| sdj_pn: ∀f1,f2,g1,g2. sdj f1 f2 → ⫯f1 = g1 → ↑f2 = g2 → sdj g1 g2
 .
 
 interpretation "disjointness (rtmap)"
@@ -49,7 +49,7 @@ qed-.
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma sdj_inv_pp: ∀g1,g2. g1 ∥ g2 → ∀f1,f2. ↑f1 = g1 → ↑f2 = g2 → f1 ∥ f2.
+lemma sdj_inv_pp: ∀g1,g2. g1 ∥ g2 → ∀f1,f2. ⫯f1 = g1 → ⫯f2 = g2 → f1 ∥ f2.
 #g1 #g2 * -g1 -g2
 #f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #x2 #Hx1 #Hx2 destruct
 [ lapply (injective_push … Hx1) -Hx1
@@ -59,7 +59,7 @@ lemma sdj_inv_pp: ∀g1,g2. g1 ∥ g2 → ∀f1,f2. ↑f1 = g1 → ↑f2 = g2 
 ]
 qed-.
 
-lemma sdj_inv_np: ∀g1,g2. g1 ∥ g2 → ∀f1,f2. ⫯f1 = g1 → ↑f2 = g2 → f1 ∥ f2.
+lemma sdj_inv_np: ∀g1,g2. g1 ∥ g2 → ∀f1,f2. ↑f1 = g1 → ⫯f2 = g2 → f1 ∥ f2.
 #g1 #g2 * -g1 -g2
 #f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #x2 #Hx1 #Hx2 destruct
 [ elim (discr_next_push … Hx1)
@@ -69,7 +69,7 @@ lemma sdj_inv_np: ∀g1,g2. g1 ∥ g2 → ∀f1,f2. ⫯f1 = g1 → ↑f2 = g2 
 ]
 qed-.
 
-lemma sdj_inv_pn: ∀g1,g2. g1 ∥ g2 → ∀f1,f2. ↑f1 = g1 → ⫯f2 = g2 → f1 ∥ f2.
+lemma sdj_inv_pn: ∀g1,g2. g1 ∥ g2 → ∀f1,f2. ⫯f1 = g1 → ↑f2 = g2 → f1 ∥ f2.
 #g1 #g2 * -g1 -g2
 #f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #x2 #Hx1 #Hx2 destruct
 [ elim (discr_next_push … Hx2)
@@ -79,7 +79,7 @@ lemma sdj_inv_pn: ∀g1,g2. g1 ∥ g2 → ∀f1,f2. ↑f1 = g1 → ⫯f2 = g2 
 ]
 qed-.
 
-lemma sdj_inv_nn: ∀g1,g2. g1 ∥ g2 → ∀f1,f2. ⫯f1 = g1 → ⫯f2 = g2 → ⊥.
+lemma sdj_inv_nn: ∀g1,g2. g1 ∥ g2 → ∀f1,f2. ↑f1 = g1 → ↑f2 = g2 → ⊥.
 #g1 #g2 * -g1 -g2
 #f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #x2 #Hx1 #Hx2 destruct
 [ elim (discr_next_push … Hx1)
@@ -90,33 +90,33 @@ qed-.
 
 (* Advanced inversion lemmas ************************************************)
 
-lemma sdj_inv_nx: ∀g1,g2. g1 ∥ g2 → ∀f1. ⫯f1 = g1 →
-                  ∃∃f2. f1 ∥ f2 & ↑f2 = g2.
+lemma sdj_inv_nx: ∀g1,g2. g1 ∥ g2 → ∀f1. ↑f1 = g1 →
+                  ∃∃f2. f1 ∥ f2 & ⫯f2 = g2.
 #g1 #g2 elim (pn_split g2) * #f2 #H2 #H #f1 #H1
 [ lapply (sdj_inv_np … H … H1 H2) -H /2 width=3 by ex2_intro/
 | elim (sdj_inv_nn … H … H1 H2)
 ]
 qed-.
 
-lemma sdj_inv_xn: ∀g1,g2. g1 ∥ g2 → ∀f2. ⫯f2 = g2 →
-                  ∃∃f1. f1 ∥ f2 & ↑f1 = g1.
+lemma sdj_inv_xn: ∀g1,g2. g1 ∥ g2 → ∀f2. ↑f2 = g2 →
+                  ∃∃f1. f1 ∥ f2 & ⫯f1 = g1.
 #g1 #g2 elim (pn_split g1) * #f1 #H1 #H #f2 #H2
 [ lapply (sdj_inv_pn … H … H1 H2) -H /2 width=3 by ex2_intro/
 | elim (sdj_inv_nn … H … H1 H2)
 ]
 qed-.
 
-lemma sdj_inv_xp: ∀g1,g2. g1 ∥ g2 → ∀f2. ↑f2 = g2 →
-                  ∨∨ ∃∃f1. f1 ∥ f2 & ↑f1 = g1
-                   | ∃∃f1. f1 ∥ f2 & ⫯f1 = g1.
+lemma sdj_inv_xp: ∀g1,g2. g1 ∥ g2 → ∀f2. ⫯f2 = g2 →
+                  ∨∨ ∃∃f1. f1 ∥ f2 & ⫯f1 = g1
+                   | ∃∃f1. f1 ∥ f2 & ↑f1 = g1.
 #g1 #g2 elim (pn_split g1) * #f1 #H1 #H #f2 #H2
 [ lapply (sdj_inv_pp … H … H1 H2) | lapply (sdj_inv_np … H … H1 H2) ] -H -H2
 /3 width=3 by ex2_intro, or_introl, or_intror/
 qed-.
 
-lemma sdj_inv_px: ∀g1,g2. g1 ∥ g2 → ∀f1. ↑f1 = g1 →
-                  ∨∨ ∃∃f2. f1 ∥ f2 & ↑f2 = g2
-                   | ∃∃f2. f1 ∥ f2 & ⫯f2 = g2.
+lemma sdj_inv_px: ∀g1,g2. g1 ∥ g2 → ∀f1. ⫯f1 = g1 →
+                  ∨∨ ∃∃f2. f1 ∥ f2 & ⫯f2 = g2
+                   | ∃∃f2. f1 ∥ f2 & ↑f2 = g2.
 #g1 #g2 elim (pn_split g2) * #f2 #H2 #H #f1 #H1
 [ lapply (sdj_inv_pp … H … H1 H2) | lapply (sdj_inv_pn … H … H1 H2) ] -H -H1
 /3 width=3 by ex2_intro, or_introl, or_intror/
@@ -124,13 +124,13 @@ qed-.
 
 (* Properties with isid *****************************************************)
 
-corec lemma sdj_isid_dx: ∀f2. 𝐈⦃f2⦄ → ∀f1. f1 ∥ f2.
+corec lemma sdj_isid_dx: ∀f2. 𝐈❪f2❫ → ∀f1. f1 ∥ f2.
 #f2 * -f2
 #f2 #g2 #Hf2 #H2 #f1 cases (pn_split f1) *
 /3 width=5 by sdj_np, sdj_pp/
 qed.
 
-corec lemma sdj_isid_sn: ∀f1. 𝐈⦃f1⦄ → ∀f2. f1 ∥ f2.
+corec lemma sdj_isid_sn: ∀f1. 𝐈❪f1❫ → ∀f2. f1 ∥ f2.
 #f1 * -f1
 #f1 #g1 #Hf1 #H1 #f2 cases (pn_split f2) *
 /3 width=5 by sdj_pn, sdj_pp/
@@ -138,7 +138,7 @@ qed.
 
 (* Inversion lemmas with isid ***********************************************)
 
-corec lemma sdj_inv_refl: ∀f. f ∥ f →  𝐈⦃f⦄.
+corec lemma sdj_inv_refl: ∀f. f ∥ f →  𝐈❪f❫.
 #f cases (pn_split f) * #g #Hg #H
 [ lapply (sdj_inv_pp … H … Hg Hg) -H /3 width=3 by isid_push/
 | elim (sdj_inv_nn … H … Hg Hg)