X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Ffrees.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Ffrees.ma;h=4ab9974c54ab085265886bd69c4999f54a20e754;hb=8ec019202bff90959cf1a7158b309e7f83fa222e;hp=90155762bc9ca1dd8851f34027abafd691cd1ae8;hpb=33d0a7a9029859be79b25b5a495e0f30dab11f37;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/frees.ma b/matita/matita/contribs/lambdadelta/static_2/static/frees.ma
index 90155762b..4ab9974c5 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/frees.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/frees.ma
@@ -19,14 +19,14 @@ include "static_2/syntax/lenv.ma".
 (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
 
 inductive frees: relation3 lenv term pr_map ≝
-| frees_sort: ∀f,L,s. 𝐈❪f❫ → frees L (⋆s) f
-| frees_atom: ∀f,i. 𝐈❪f❫ → frees (⋆) (#i) (⫯*[i]↑f)
+| frees_sort: ∀f,L,s. 𝐈❨f❩ → frees L (⋆s) f
+| frees_atom: ∀f,i. 𝐈❨f❩ → frees (⋆) (#i) (⫯*[i]↑f)
 | frees_pair: ∀f,I,L,V. frees L V f →
               frees (L.ⓑ[I]V) (#0) (↑f)
-| frees_unit: ∀f,I,L. 𝐈❪f❫ → frees (L.ⓤ[I]) (#0) (↑f)
+| frees_unit: ∀f,I,L. 𝐈❨f❩ → frees (L.ⓤ[I]) (#0) (↑f)
 | frees_lref: ∀f,I,L,i. frees L (#i) f →
               frees (L.ⓘ[I]) (#↑i) (⫯f)
-| frees_gref: ∀f,L,l. 𝐈❪f❫ → frees L (§l) f
+| frees_gref: ∀f,L,l. 𝐈❨f❩ → 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 ⋓ ⫰f2 ≘ f → frees L (ⓑ[p,I]V.T) f
 | frees_flat: ∀f1,f2,f,I,L,V,T. frees L V f1 → frees L T f2 →
@@ -39,7 +39,7 @@ interpretation
 
 (* Basic inversion lemmas ***************************************************)
 
-fact frees_inv_sort_aux: ∀f,L,X. L ⊢ 𝐅+❪X❫ ≘ f → ∀x. X = ⋆x → 𝐈❪f❫.
+fact frees_inv_sort_aux: ∀f,L,X. L ⊢ 𝐅+❨X❩ ≘ f → ∀x. X = ⋆x → 𝐈❨f❩.
 #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: ∀f,L,s. L ⊢ 𝐅+❪⋆s❫ ≘ f → 𝐈❪f❫.
+lemma frees_inv_sort: ∀f,L,s. L ⊢ 𝐅+❨⋆s❩ ≘ f → 𝐈❨f❩.
 /2 width=5 by frees_inv_sort_aux/ qed-.
 
 fact frees_inv_atom_aux:
-     ∀f,L,X. L ⊢ 𝐅+❪X❫ ≘ f → ∀i. L = ⋆ → X = #i →
-     ∃∃g. 𝐈❪g❫ & f = ⫯*[i]↑g.
+     ∀f,L,X. L ⊢ 𝐅+❨X❩ ≘ f → ∀i. L = ⋆ → X = #i →
+     ∃∃g. 𝐈❨g❩ & 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: ∀f,i. ⋆ ⊢ 𝐅+❪#i❫ ≘ f → ∃∃g. 𝐈❪g❫ & f = ⫯*[i]↑g.
+lemma frees_inv_atom: ∀f,i. ⋆ ⊢ 𝐅+❨#i❩ ≘ f → ∃∃g. 𝐈❨g❩ & f = ⫯*[i]↑g.
 /2 width=5 by frees_inv_atom_aux/ qed-.
 
 fact frees_inv_pair_aux:
-     ∀f,L,X. L ⊢ 𝐅+❪X❫ ≘ f → ∀I,K,V. L = K.ⓑ[I]V → X = #0 →
-     ∃∃g. K ⊢ 𝐅+❪V❫ ≘ g & f = ↑g.
+     ∀f,L,X. L ⊢ 𝐅+❨X❩ ≘ f → ∀I,K,V. L = K.ⓑ[I]V → X = #0 →
+     ∃∃g. K ⊢ 𝐅+❨V❩ ≘ 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:
-     ∀f,L,X. L ⊢ 𝐅+❪X❫ ≘ f → ∀I,K. L = K.ⓤ[I] → X = #0 →
-     ∃∃g. 𝐈❪g❫ & f = ↑g.
+     ∀f,L,X. L ⊢ 𝐅+❨X❩ ≘ f → ∀I,K. L = K.ⓤ[I] → X = #0 →
+     ∃∃g. 𝐈❨g❩ & 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:
-     ∀f,L,X. L ⊢ 𝐅+❪X❫ ≘ f → ∀I,K,j. L = K.ⓘ[I] → X = #(↑j) →
-     ∃∃g. K ⊢ 𝐅+❪#j❫ ≘ g & f = ⫯g.
+     ∀f,L,X. L ⊢ 𝐅+❨X❩ ≘ f → ∀I,K,j. L = K.ⓘ[I] → X = #(↑j) →
+     ∃∃g. K ⊢ 𝐅+❨#j❩ ≘ 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 →
-      ∃∃g. K ⊢ 𝐅+❪#i❫ ≘ g & f = ⫯g.
+      ∀f,I,K,i. K.ⓘ[I] ⊢ 𝐅+❨#(↑i)❩ ≘ f →
+      ∃∃g. K ⊢ 𝐅+❨#i❩ ≘ g & f = ⫯g.
 /2 width=6 by frees_inv_lref_aux/ qed-.
 
-fact frees_inv_gref_aux: ∀f,L,X. L ⊢ 𝐅+❪X❫ ≘ f → ∀x. X = §x → 𝐈❪f❫.
+fact frees_inv_gref_aux: ∀f,L,X. L ⊢ 𝐅+❨X❩ ≘ f → ∀x. X = §x → 𝐈❨f❩.
 #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: ∀f,L,l. L ⊢ 𝐅+❪§l❫ ≘ f → 𝐈❪f❫.
+lemma frees_inv_gref: ∀f,L,l. L ⊢ 𝐅+❨§l❩ ≘ f → 𝐈❨f❩.
 /2 width=5 by frees_inv_gref_aux/ qed-.
 
 fact frees_inv_bind_aux:
-     ∀f,L,X. L ⊢ 𝐅+❪X❫ ≘ f → ∀p,I,V,T. X = ⓑ[p,I]V.T →
-     ∃∃f1,f2. L ⊢ 𝐅+❪V❫ ≘ f1 & L.ⓑ[I]V ⊢ 𝐅+❪T❫ ≘ f2 & f1 ⋓ ⫰f2 ≘ f.
+     ∀f,L,X. L ⊢ 𝐅+❨X❩ ≘ f → ∀p,I,V,T. X = ⓑ[p,I]V.T →
+     ∃∃f1,f2. L ⊢ 𝐅+❨V❩ ≘ f1 & L.ⓑ[I]V ⊢ 𝐅+❨T❩ ≘ f2 & f1 ⋓ ⫰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:
-      ∀f,p,I,L,V,T. L ⊢ 𝐅+❪ⓑ[p,I]V.T❫ ≘ f →
-      ∃∃f1,f2. L ⊢ 𝐅+❪V❫ ≘ f1 & L.ⓑ[I]V ⊢ 𝐅+❪T❫ ≘ f2 & f1 ⋓ ⫰f2 ≘ f.
+      ∀f,p,I,L,V,T. L ⊢ 𝐅+❨ⓑ[p,I]V.T❩ ≘ f →
+      ∃∃f1,f2. L ⊢ 𝐅+❨V❩ ≘ f1 & L.ⓑ[I]V ⊢ 𝐅+❨T❩ ≘ f2 & f1 ⋓ ⫰f2 ≘ f.
 /2 width=4 by frees_inv_bind_aux/ qed-.
 
-fact frees_inv_flat_aux: ∀f,L,X. L ⊢ 𝐅+❪X❫ ≘ f → ∀I,V,T. X = ⓕ[I]V.T →
-                         ∃∃f1,f2. L ⊢ 𝐅+❪V❫ ≘ f1 & L ⊢ 𝐅+❪T❫ ≘ f2 & f1 ⋓ f2 ≘ f.
+fact frees_inv_flat_aux: ∀f,L,X. L ⊢ 𝐅+❨X❩ ≘ f → ∀I,V,T. X = ⓕ[I]V.T →
+                         ∃∃f1,f2. L ⊢ 𝐅+❨V❩ ≘ f1 & L ⊢ 𝐅+❨T❩ ≘ 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,13 +176,13 @@ fact frees_inv_flat_aux: ∀f,L,X. L ⊢ 𝐅+❪X❫ ≘ f → ∀I,V,T. X = 
 qed-.
 
 lemma frees_inv_flat:
-      ∀f,I,L,V,T. L ⊢ 𝐅+❪ⓕ[I]V.T❫ ≘ f →
-      ∃∃f1,f2. L ⊢ 𝐅+❪V❫ ≘ f1 & L ⊢ 𝐅+❪T❫ ≘ f2 & f1 ⋓ f2 ≘ f.
+      ∀f,I,L,V,T. L ⊢ 𝐅+❨ⓕ[I]V.T❩ ≘ f →
+      ∃∃f1,f2. L ⊢ 𝐅+❨V❩ ≘ f1 & L ⊢ 𝐅+❨T❩ ≘ f2 & f1 ⋓ f2 ≘ f.
 /2 width=4 by frees_inv_flat_aux/ qed-.
 
 (* Basic properties ********************************************************)
 
-lemma frees_eq_repl_back: ∀L,T. pr_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, pr_isi_eq_repl_back/
 | #f1 #i #Hf1 #g2 #H
@@ -203,11 +203,11 @@ lemma frees_eq_repl_back: ∀L,T. pr_eq_repl_back … (λf. L ⊢ 𝐅+❪T❫ 
 ]
 qed-.
 
-lemma frees_eq_repl_fwd: ∀L,T. pr_eq_repl_fwd … (λf. L ⊢ 𝐅+❪T❫ ≘ f).
+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: ∀f,i. ⋆ ⊢ 𝐅+❪#i❫ ≘ f → ⋆ ⊢ 𝐅+❪#↑i❫ ≘ ⫯f.
+lemma frees_lref_push: ∀f,i. ⋆ ⊢ 𝐅+❨#i❩ ≘ f → ⋆ ⊢ 𝐅+❨#↑i❩ ≘ ⫯f.
 #f #i #H
 elim (frees_inv_atom … H) -H #g #Hg #H destruct
 /2 width=1 by frees_atom/
@@ -215,7 +215,7 @@ qed.
 
 (* Forward lemmas with test for finite colength *****************************)
 
-lemma frees_fwd_isfin: ∀f,L,T. L ⊢ 𝐅+❪T❫ ≘ f → 𝐅❪f❫.
+lemma frees_fwd_isfin: ∀f,L,T. L ⊢ 𝐅+❨T❩ ≘ f → 𝐅❨f❩.
 #f #L #T #H elim H -f -L -T
 /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-.