partial commit in static_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / static / frees.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/frees.ma b/matita/matita/contribs/lambdadelta/static_2/static/frees.ma
index 2a72515f43b41c1b7a3fc5646be71e8db39e7733..90155762bc9ca1dd8851f34027abafd691cd1ae8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/static/frees.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/frees.ma
@@ -12,25 +12,25 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/relocation/rtmap_sor.ma".
+include "ground/relocation/rtmap_sor.ma".
 include "static_2/notation/relations/freeplus_3.ma".
 include "static_2/syntax/lenv.ma".
 
 (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
 
-inductive frees: relation3 lenv term rtmap ≝
-| frees_sort: â\88\80f,L,s. ð\9d\90\88â¦\83fâ¦\84 → frees L (⋆s) f
-| frees_atom: â\88\80f,i. ð\9d\90\88â¦\83fâ¦\84 → frees (⋆) (#i) (⫯*[i]↑f)
+inductive frees: relation3 lenv term pr_map ≝
+| frees_sort: â\88\80f,L,s. ð\9d\90\88â\9dªfâ\9d« → frees L (⋆s) f
+| frees_atom: â\88\80f,i. ð\9d\90\88â\9dªfâ\9d« → frees (⋆) (#i) (⫯*[i]↑f)
 | frees_pair: ∀f,I,L,V. frees L V f →
-              frees (L.ⓑ{I}V) (#0) (↑f)
-| frees_unit: â\88\80f,I,L. ð\9d\90\88â¦\83fâ¦\84 â\86\92 frees (L.â\93¤{I}) (#0) (↑f)
+              frees (L.ⓑ[I]V) (#0) (↑f)
+| frees_unit: â\88\80f,I,L. ð\9d\90\88â\9dªfâ\9d« â\86\92 frees (L.â\93¤[I]) (#0) (↑f)
 | frees_lref: ∀f,I,L,i. frees L (#i) f →
-              frees (L.ⓘ{I}) (#↑i) (⫯f)
-| frees_gref: â\88\80f,L,l. ð\9d\90\88â¦\83fâ¦\84 → frees L (§l) f
-| frees_bind: ∀f1,f2,f,p,I,L,V,T. frees L V f1 → frees (L.ⓑ{I}V) T f2 →
-              f1 â\8b\93 ⫱f2 â\89\98 f â\86\92 frees L (â\93\91{p,I}V.T) f
+              frees (L.ⓘ[I]) (#↑i) (⫯f)
+| frees_gref: â\88\80f,L,l. ð\9d\90\88â\9dªfâ\9d« → frees L (§l) f
+| frees_bind: ∀f1,f2,f,p,I,L,V,T. frees L V f1 → frees (L.ⓑ[I]V) T f2 →
+              f1 â\8b\93 â«°f2 â\89\98 f â\86\92 frees L (â\93\91[p,I]V.T) f
 | frees_flat: ∀f1,f2,f,I,L,V,T. frees L V f1 → frees L T f2 →
-              f1 ⋓ f2 ≘ f → frees L (ⓕ{I}V.T) f
+              f1 ⋓ f2 ≘ f → frees L (ⓕ[I]V.T) f
 .
 
 interpretation
@@ -39,7 +39,7 @@ interpretation
 
 (* Basic inversion lemmas ***************************************************)
 
-fact frees_inv_sort_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85+â¦\83Xâ¦\84 â\89\98 f â\86\92 â\88\80x. X = â\8b\86x â\86\92 ð\9d\90\88â¦\83fâ¦\84.
+fact frees_inv_sort_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85+â\9dªXâ\9d« â\89\98 f â\86\92 â\88\80x. X = â\8b\86x â\86\92 ð\9d\90\88â\9dªfâ\9d«.
 #L #X #f #H elim H -f -L -X //
 [ #f #i #_ #x #H destruct
 | #f #_ #L #V #_ #_ #x #H destruct
@@ -50,12 +50,12 @@ fact frees_inv_sort_aux: ∀f,L,X. L ⊢ 𝐅+⦃X⦄ ≘ f → ∀x. X = ⋆x 
 ]
 qed-.
 
-lemma frees_inv_sort: â\88\80f,L,s. L â\8a¢ ð\9d\90\85+â¦\83â\8b\86sâ¦\84 â\89\98 f â\86\92 ð\9d\90\88â¦\83fâ¦\84.
+lemma frees_inv_sort: â\88\80f,L,s. L â\8a¢ ð\9d\90\85+â\9dªâ\8b\86sâ\9d« â\89\98 f â\86\92 ð\9d\90\88â\9dªfâ\9d«.
 /2 width=5 by frees_inv_sort_aux/ qed-.
 
 fact frees_inv_atom_aux:
-     â\88\80f,L,X. L â\8a¢ ð\9d\90\85+â¦\83Xâ¦\84 ≘ f → ∀i. L = ⋆ → X = #i →
-     â\88\83â\88\83g. ð\9d\90\88â¦\83gâ¦\84 & f = ⫯*[i]↑g.
+     â\88\80f,L,X. L â\8a¢ ð\9d\90\85+â\9dªXâ\9d« ≘ f → ∀i. L = ⋆ → X = #i →
+     â\88\83â\88\83g. ð\9d\90\88â\9dªgâ\9d« & f = ⫯*[i]↑g.
 #f #L #X #H elim H -f -L -X
 [ #f #L #s #_ #j #_ #H destruct
 | #f #i #Hf #j #_ #H destruct /2 width=3 by ex2_intro/
@@ -68,12 +68,12 @@ fact frees_inv_atom_aux:
 ]
 qed-.
 
-lemma frees_inv_atom: â\88\80f,i. â\8b\86 â\8a¢ ð\9d\90\85+â¦\83#iâ¦\84 â\89\98 f â\86\92 â\88\83â\88\83g. ð\9d\90\88â¦\83gâ¦\84 & f = ⫯*[i]↑g.
+lemma frees_inv_atom: â\88\80f,i. â\8b\86 â\8a¢ ð\9d\90\85+â\9dª#iâ\9d« â\89\98 f â\86\92 â\88\83â\88\83g. ð\9d\90\88â\9dªgâ\9d« & f = ⫯*[i]↑g.
 /2 width=5 by frees_inv_atom_aux/ qed-.
 
 fact frees_inv_pair_aux:
-     â\88\80f,L,X. L â\8a¢ ð\9d\90\85+â¦\83Xâ¦\84 â\89\98 f â\86\92 â\88\80I,K,V. L = K.â\93\91{I}V → X = #0 →
-     â\88\83â\88\83g. K â\8a¢ ð\9d\90\85+â¦\83Vâ¦\84 ≘ g & f = ↑g.
+     â\88\80f,L,X. L â\8a¢ ð\9d\90\85+â\9dªXâ\9d« â\89\98 f â\86\92 â\88\80I,K,V. L = K.â\93\91[I]V → X = #0 →
+     â\88\83â\88\83g. K â\8a¢ ð\9d\90\85+â\9dªVâ\9d« ≘ g & f = ↑g.
 #f #L #X * -f -L -X
 [ #f #L #s #_ #Z #Y #X #_ #H destruct
 | #f #i #_ #Z #Y #X #H destruct
@@ -86,12 +86,12 @@ fact frees_inv_pair_aux:
 ]
 qed-.
 
-lemma frees_inv_pair: ∀f,I,K,V. K.ⓑ{I}V ⊢ 𝐅+⦃#0⦄ ≘ f → ∃∃g. K ⊢ 𝐅+⦃V⦄ ≘ g & f = ↑g.
+lemma frees_inv_pair: ∀f,I,K,V. K.ⓑ[I]V ⊢ 𝐅+❪#0❫ ≘ f → ∃∃g. K ⊢ 𝐅+❪V❫ ≘ g & f = ↑g.
 /2 width=6 by frees_inv_pair_aux/ qed-.
 
 fact frees_inv_unit_aux:
-     â\88\80f,L,X. L â\8a¢ ð\9d\90\85+â¦\83Xâ¦\84 â\89\98 f â\86\92 â\88\80I,K. L = K.â\93¤{I} → X = #0 →
-     â\88\83â\88\83g. ð\9d\90\88â¦\83gâ¦\84 & f = ↑g.
+     â\88\80f,L,X. L â\8a¢ ð\9d\90\85+â\9dªXâ\9d« â\89\98 f â\86\92 â\88\80I,K. L = K.â\93¤[I] → X = #0 →
+     â\88\83â\88\83g. ð\9d\90\88â\9dªgâ\9d« & f = ↑g.
 #f #L #X * -f -L -X
 [ #f #L #s #_ #Z #Y #_ #H destruct
 | #f #i #_ #Z #Y #H destruct
@@ -104,12 +104,12 @@ fact frees_inv_unit_aux:
 ]
 qed-.
 
-lemma frees_inv_unit: ∀f,I,K. K.ⓤ{I} ⊢ 𝐅+⦃#0⦄ ≘ f → ∃∃g. 𝐈⦃g⦄ & f = ↑g.
+lemma frees_inv_unit: ∀f,I,K. K.ⓤ[I] ⊢ 𝐅+❪#0❫ ≘ f → ∃∃g. 𝐈❪g❫ & f = ↑g.
 /2 width=7 by frees_inv_unit_aux/ qed-.
 
 fact frees_inv_lref_aux:
-     â\88\80f,L,X. L â\8a¢ ð\9d\90\85+â¦\83Xâ¦\84 â\89\98 f â\86\92 â\88\80I,K,j. L = K.â\93\98{I} → X = #(↑j) →
-     â\88\83â\88\83g. K â\8a¢ ð\9d\90\85+â¦\83#jâ¦\84 ≘ g & f = ⫯g.
+     â\88\80f,L,X. L â\8a¢ ð\9d\90\85+â\9dªXâ\9d« â\89\98 f â\86\92 â\88\80I,K,j. L = K.â\93\98[I] → X = #(↑j) →
+     â\88\83â\88\83g. K â\8a¢ ð\9d\90\85+â\9dª#jâ\9d« ≘ g & f = ⫯g.
 #f #L #X * -f -L -X
 [ #f #L #s #_ #Z #Y #j #_ #H destruct
 | #f #i #_ #Z #Y #j #H destruct
@@ -123,11 +123,11 @@ fact frees_inv_lref_aux:
 qed-.
 
 lemma frees_inv_lref:
-      ∀f,I,K,i. K.ⓘ{I} ⊢ 𝐅+⦃#(↑i)⦄ ≘ f →
-      â\88\83â\88\83g. K â\8a¢ ð\9d\90\85+â¦\83#iâ¦\84 ≘ g & f = ⫯g.
+      ∀f,I,K,i. K.ⓘ[I] ⊢ 𝐅+❪#(↑i)❫ ≘ f →
+      â\88\83â\88\83g. K â\8a¢ ð\9d\90\85+â\9dª#iâ\9d« ≘ g & f = ⫯g.
 /2 width=6 by frees_inv_lref_aux/ qed-.
 
-fact frees_inv_gref_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85+â¦\83Xâ¦\84 â\89\98 f â\86\92 â\88\80x. X = §x â\86\92 ð\9d\90\88â¦\83fâ¦\84.
+fact frees_inv_gref_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85+â\9dªXâ\9d« â\89\98 f â\86\92 â\88\80x. X = §x â\86\92 ð\9d\90\88â\9dªfâ\9d«.
 #f #L #X #H elim H -f -L -X //
 [ #f #i #_ #x #H destruct
 | #f #_ #L #V #_ #_ #x #H destruct
@@ -138,12 +138,12 @@ fact frees_inv_gref_aux: ∀f,L,X. L ⊢ 𝐅+⦃X⦄ ≘ f → ∀x. X = §x 
 ]
 qed-.
 
-lemma frees_inv_gref: â\88\80f,L,l. L â\8a¢ ð\9d\90\85+â¦\83§lâ¦\84 â\89\98 f â\86\92 ð\9d\90\88â¦\83fâ¦\84.
+lemma frees_inv_gref: â\88\80f,L,l. L â\8a¢ ð\9d\90\85+â\9dªÂ§lâ\9d« â\89\98 f â\86\92 ð\9d\90\88â\9dªfâ\9d«.
 /2 width=5 by frees_inv_gref_aux/ qed-.
 
 fact frees_inv_bind_aux:
-     â\88\80f,L,X. L â\8a¢ ð\9d\90\85+â¦\83Xâ¦\84 â\89\98 f â\86\92 â\88\80p,I,V,T. X = â\93\91{p,I}V.T →
-     â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85+â¦\83Vâ¦\84 â\89\98 f1 & L.â\93\91{I}V â\8a¢ ð\9d\90\85+â¦\83Tâ¦\84 â\89\98 f2 & f1 â\8b\93 ⫱f2 ≘ f.
+     â\88\80f,L,X. L â\8a¢ ð\9d\90\85+â\9dªXâ\9d« â\89\98 f â\86\92 â\88\80p,I,V,T. X = â\93\91[p,I]V.T →
+     â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f1 & L.â\93\91[I]V â\8a¢ ð\9d\90\85+â\9dªTâ\9d« â\89\98 f2 & f1 â\8b\93 â«°f2 ≘ f.
 #f #L #X * -f -L -X
 [ #f #L #s #_ #q #J #W #U #H destruct
 | #f #i #_ #q #J #W #U #H destruct
@@ -157,12 +157,12 @@ fact frees_inv_bind_aux:
 qed-.
 
 lemma frees_inv_bind:
-      â\88\80f,p,I,L,V,T. L â\8a¢ ð\9d\90\85+â¦\83â\93\91{p,I}V.Tâ¦\84 ≘ f →
-      â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85+â¦\83Vâ¦\84 â\89\98 f1 & L.â\93\91{I}V â\8a¢ ð\9d\90\85+â¦\83Tâ¦\84 â\89\98 f2 & f1 â\8b\93 ⫱f2 ≘ f.
+      â\88\80f,p,I,L,V,T. L â\8a¢ ð\9d\90\85+â\9dªâ\93\91[p,I]V.Tâ\9d« ≘ f →
+      â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f1 & L.â\93\91[I]V â\8a¢ ð\9d\90\85+â\9dªTâ\9d« â\89\98 f2 & f1 â\8b\93 â«°f2 ≘ f.
 /2 width=4 by frees_inv_bind_aux/ qed-.
 
-fact frees_inv_flat_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85+â¦\83Xâ¦\84 â\89\98 f â\86\92 â\88\80I,V,T. X = â\93\95{I}V.T →
-                         â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85+â¦\83Vâ¦\84 â\89\98 f1 & L â\8a¢ ð\9d\90\85+â¦\83Tâ¦\84 ≘ f2 & f1 ⋓ f2 ≘ f.
+fact frees_inv_flat_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85+â\9dªXâ\9d« â\89\98 f â\86\92 â\88\80I,V,T. X = â\93\95[I]V.T →
+                         â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f1 & L â\8a¢ ð\9d\90\85+â\9dªTâ\9d« ≘ f2 & f1 ⋓ f2 ≘ f.
 #f #L #X * -f -L -X
 [ #f #L #s #_ #J #W #U #H destruct
 | #f #i #_ #J #W #U #H destruct
@@ -176,38 +176,38 @@ fact frees_inv_flat_aux: ∀f,L,X. L ⊢ 𝐅+⦃X⦄ ≘ f → ∀I,V,T. X = 
 qed-.
 
 lemma frees_inv_flat:
-      â\88\80f,I,L,V,T. L â\8a¢ ð\9d\90\85+â¦\83â\93\95{I}V.Tâ¦\84 ≘ f →
-      â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85+â¦\83Vâ¦\84 â\89\98 f1 & L â\8a¢ ð\9d\90\85+â¦\83Tâ¦\84 ≘ f2 & f1 ⋓ f2 ≘ f.
+      â\88\80f,I,L,V,T. L â\8a¢ ð\9d\90\85+â\9dªâ\93\95[I]V.Tâ\9d« ≘ f →
+      â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f1 & L â\8a¢ ð\9d\90\85+â\9dªTâ\9d« ≘ f2 & f1 ⋓ f2 ≘ f.
 /2 width=4 by frees_inv_flat_aux/ qed-.
 
 (* Basic properties ********************************************************)
 
-lemma frees_eq_repl_back: ∀L,T. eq_repl_back … (λf. L ⊢ 𝐅+⦃T⦄ ≘ f).
+lemma frees_eq_repl_back: ∀L,T. pr_eq_repl_back … (λf. L ⊢ 𝐅+❪T❫ ≘ f).
 #L #T #f1 #H elim H -f1 -L -T
-[ /3 width=3 by frees_sort, isid_eq_repl_back/
+[ /3 width=3 by frees_sort, pr_isi_eq_repl_back/
 | #f1 #i #Hf1 #g2 #H
-  elim (eq_inv_pushs_sn … H) -H #g #Hg #H destruct
+  elim (pr_eq_inv_pushs_sn … H) -H #g #Hg #H destruct
   elim (eq_inv_nx … Hg) -Hg
-  /3 width=3 by frees_atom, isid_eq_repl_back/
+  /3 width=3 by frees_atom, pr_isi_eq_repl_back/
 | #f1 #I #L #V #_ #IH #g2 #H
   elim (eq_inv_nx … H) -H
   /3 width=3 by frees_pair/
 | #f1 #I #L #Hf1 #g2 #H
   elim (eq_inv_nx … H) -H
-  /3 width=3 by frees_unit, isid_eq_repl_back/
+  /3 width=3 by frees_unit, pr_isi_eq_repl_back/
 | #f1 #I #L #i #_ #IH #g2 #H
   elim (eq_inv_px … H) -H /3 width=3 by frees_lref/
-| /3 width=3 by frees_gref, isid_eq_repl_back/
-| /3 width=7 by frees_bind, sor_eq_repl_back3/
-| /3 width=7 by frees_flat, sor_eq_repl_back3/
+| /3 width=3 by frees_gref, pr_isi_eq_repl_back/
+| /3 width=7 by frees_bind, pr_sor_eq_repl_back/
+| /3 width=7 by frees_flat, pr_sor_eq_repl_back/
 ]
 qed-.
 
-lemma frees_eq_repl_fwd: ∀L,T. eq_repl_fwd … (λf. L ⊢ 𝐅+⦃T⦄ ≘ f).
-#L #T @eq_repl_sym /2 width=3 by frees_eq_repl_back/
+lemma frees_eq_repl_fwd: ∀L,T. pr_eq_repl_fwd … (λf. L ⊢ 𝐅+❪T❫ ≘ f).
+#L #T @pr_eq_repl_sym /2 width=3 by frees_eq_repl_back/
 qed-.
 
-lemma frees_lref_push: â\88\80f,i. â\8b\86 â\8a¢ ð\9d\90\85+â¦\83#iâ¦\84 â\89\98 f â\86\92 â\8b\86 â\8a¢ ð\9d\90\85+â¦\83#â\86\91iâ¦\84 ≘ ⫯f.
+lemma frees_lref_push: â\88\80f,i. â\8b\86 â\8a¢ ð\9d\90\85+â\9dª#iâ\9d« â\89\98 f â\86\92 â\8b\86 â\8a¢ ð\9d\90\85+â\9dª#â\86\91iâ\9d« ≘ ⫯f.
 #f #i #H
 elim (frees_inv_atom … H) -H #g #Hg #H destruct
 /2 width=1 by frees_atom/
@@ -215,9 +215,9 @@ qed.
 
 (* Forward lemmas with test for finite colength *****************************)
 
-lemma frees_fwd_isfin: â\88\80f,L,T. L â\8a¢ ð\9d\90\85+â¦\83Tâ¦\84 â\89\98 f â\86\92 ð\9d\90\85â¦\83fâ¦\84.
+lemma frees_fwd_isfin: â\88\80f,L,T. L â\8a¢ ð\9d\90\85+â\9dªTâ\9d« â\89\98 f â\86\92 ð\9d\90\85â\9dªfâ\9d«.
 #f #L #T #H elim H -f -L -T
-/4 width=5 by sor_isfin, isfin_isid, isfin_tl, isfin_pushs, isfin_push, isfin_next/
+/4 width=5 by pr_sor_inv_isf_bi, pr_isf_isi, pr_isf_tl, pr_isf_pushs, pr_isf_push, pr_isf_next/
 qed-.
 
 (* Basic_2A1: removed theorems 30: