partial commit in static_2

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

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/frees_fqup.ma b/matita/matita/contribs/lambdadelta/static_2/static/frees_fqup.ma
index feb74eb263f4fc3d49639e1d98d91c8c9b114005..6868962e64f6782e5a0dacd64b41f796a7408610 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/static/frees_fqup.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/frees_fqup.ma
@@ -20,7 +20,7 @@ include "static_2/static/lsubf_lsubr.ma".
 (* Advanced properties ******************************************************)
 
 (* Note: this replaces lemma 1400 concluding the "big tree" theorem *)
-lemma frees_total: â\88\80L,T. â\88\83f. L â\8a¢ ð\9d\90\85+â¦\83Tâ¦\84 ≘ f.
+lemma frees_total: â\88\80L,T. â\88\83f. L â\8a¢ ð\9d\90\85+â\9dªTâ\9d« ≘ f.
 #L #T @(fqup_wf_ind_eq (Ⓣ) … (⋆) L T) -L -T
 #G0 #L0 #T0 #IH #G #L * *
 [ /3 width=2 by frees_sort, ex_intro/
@@ -38,13 +38,13 @@ lemma frees_total: ∀L,T. ∃f. L ⊢ 𝐅+⦃T⦄ ≘ f.
 | /3 width=2 by frees_gref, ex_intro/
 | #p #I #V #T #HG #HL #HT destruct
   elim (IH G L V) // #f1 #HV
-  elim (IH G (L.ⓑ{I}V) T) -IH // #f2 #HT
-  elim (sor_isfin_ex f1 (⫱f2))
-  /3 width=6 by frees_fwd_isfin, frees_bind, isfin_tl, ex_intro/
+  elim (IH G (L.ⓑ[I]V) T) -IH // #f2 #HT
+  elim (pr_sor_isf_bi f1 (⫰f2))
+  /3 width=6 by frees_fwd_isfin, frees_bind, pr_isf_tl, ex_intro/
 | #I #V #T #HG #HL #HT destruct
   elim (IH G L V) // #f1 #HV
   elim (IH G L T) -IH // #f2 #HT
-  elim (sor_isfin_ex f1 f2)
+  elim (pr_sor_isf_bi f1 f2)
   /3 width=6 by frees_fwd_isfin, frees_flat, ex_intro/
 ]
 qed-.
@@ -52,81 +52,81 @@ qed-.
 (* Advanced main properties *************************************************)
 
 theorem frees_bind_void:
-        â\88\80f1,L,V. L â\8a¢ ð\9d\90\85+â¦\83Vâ¦\84 â\89\98 f1 â\86\92 â\88\80f2,T. L.â\93§ â\8a¢ ð\9d\90\85+â¦\83Tâ¦\84 ≘ f2 →
-        â\88\80f. f1 â\8b\93 ⫱f2 â\89\98 f â\86\92 â\88\80p,I. L â\8a¢ ð\9d\90\85+â¦\83â\93\91{p,I}V.Tâ¦\84 ≘ f.
+        â\88\80f1,L,V. L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f1 â\86\92 â\88\80f2,T. L.â\93§ â\8a¢ ð\9d\90\85+â\9dªTâ\9d« ≘ f2 →
+        â\88\80f. f1 â\8b\93 â«°f2 â\89\98 f â\86\92 â\88\80p,I. L â\8a¢ ð\9d\90\85+â\9dªâ\93\91[p,I]V.Tâ\9d« ≘ f.
 #f1 #L #V #Hf1 #f2 #T #Hf2 #f #Hf #p #I
-elim (frees_total (L.ⓑ{I}V) T) #f0 #Hf0
+elim (frees_total (L.ⓑ[I]V) T) #f0 #Hf0
 lapply (lsubr_lsubf … Hf2 … Hf0) -Hf2 /2 width=5 by lsubr_unit/ #H02
-elim (pn_split f2) * #g2 #H destruct
+elim (pr_map_split_tl f2) * #g2 #H destruct
 [ elim (lsubf_inv_push2 … H02) -H02 #g0 #Z #Y #H02 #H0 #H destruct
   lapply (lsubf_inv_refl … H02) -H02 #H02
-  lapply (sor_eq_repl_fwd2 … Hf … H02) -g2 #Hf
+  lapply (pr_sor_eq_repl_fwd_dx … Hf … H02) -g2 #Hf
   /2 width=5 by frees_bind/
 | elim (lsubf_inv_unit2 … H02) -H02 * [ #g0 #Y #_ #_ #H destruct ]
   #z1 #g0 #z #Z #Y #X #H02 #Hz1 #Hz #H0 #H destruct
   lapply (lsubf_inv_refl … H02) -H02 #H02
   lapply (frees_mono … Hz1 … Hf1) -Hz1 #H1
-  lapply (sor_eq_repl_back1 … Hz … H02) -g0 #Hz
-  lapply (sor_eq_repl_back2 … Hz … H1) -z1 #Hz
-  lapply (sor_comm … Hz) -Hz #Hz
-  lapply (sor_mono … f Hz ?) // -Hz #H
-  lapply (sor_inv_sle_sn … Hf) -Hf #Hf
-  lapply (frees_eq_repl_back … Hf0 (↑f) ?) /2 width=5 by eq_next/ -z #Hf0
+  lapply (pr_sor_eq_repl_back_sn … Hz … H02) -g0 #Hz
+  lapply (pr_sor_eq_repl_back_dx … Hz … H1) -z1 #Hz
+  lapply (pr_sor_comm … Hz) -Hz #Hz
+  lapply (pr_sor_mono … f Hz ?) // -Hz #H
+  lapply (pr_sor_inv_sle_sn … Hf) -Hf #Hf
+  lapply (frees_eq_repl_back … Hf0 (↑f) ?) /2 width=5 by pr_eq_next/ -z #Hf0
   @(frees_bind … Hf1 Hf0) -Hf1 -Hf0 (**) (* constructor needed *)
-  /2 width=1 by sor_sle_dx/
+  /2 width=1 by pr_sor_sle_dx/
 ]
 qed-.
 
 (* Advanced inversion lemmas ************************************************)
 
 lemma frees_inv_bind_void:
-      â\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§ â\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§ â\8a¢ ð\9d\90\85+â\9dªTâ\9d« â\89\98 f2 & f1 â\8b\93 â«°f2 ≘ f.
 #f #p #I #L #V #T #H
 elim (frees_inv_bind … H) -H #f1 #f2 #Hf1 #Hf2 #Hf
 elim (frees_total (L.ⓧ) T) #f0 #Hf0
 lapply (lsubr_lsubf … Hf0 … Hf2) -Hf2 /2 width=5 by lsubr_unit/ #H20
-elim (pn_split f0) * #g0 #H destruct
+elim (pr_map_split_tl f0) * #g0 #H destruct
 [ elim (lsubf_inv_push2 … H20) -H20 #g2 #I #Y #H20 #H2 #H destruct
   lapply (lsubf_inv_refl … H20) -H20 #H20
-  lapply (sor_eq_repl_back2 … Hf … H20) -g2 #Hf
+  lapply (pr_sor_eq_repl_back_dx … Hf … H20) -g2 #Hf
   /2 width=5 by ex3_2_intro/
 | elim (lsubf_inv_unit2 … H20) -H20 * [ #g2 #Y #_ #_ #H destruct ]
   #z1 #z0 #g2 #Z #Y #X #H20 #Hz1 #Hg2 #H2 #H destruct
   lapply (lsubf_inv_refl … H20) -H20 #H0
   lapply (frees_mono … Hz1 … Hf1) -Hz1 #H1
-  lapply (sor_eq_repl_back1 … Hg2 … H0) -z0 #Hg2
-  lapply (sor_eq_repl_back2 … Hg2 … H1) -z1 #Hg2
+  lapply (pr_sor_eq_repl_back_sn … Hg2 … H0) -z0 #Hg2
+  lapply (pr_sor_eq_repl_back_dx … Hg2 … H1) -z1 #Hg2
   @(ex3_2_intro … Hf1 Hf0) -Hf1 -Hf0 (**) (* constructor needed *)
-  /2 width=3 by sor_comm_23_idem/
+  /2 width=3 by pr_sor_comm_23_idem/
 ]
 qed-.
 
 lemma frees_ind_void (Q:relation3 …):
       (
-        â\88\80f,L,s. ð\9d\90\88â¦\83fâ¦\84 →  Q L (⋆s) f
+        â\88\80f,L,s. ð\9d\90\88â\9dªfâ\9d« →  Q L (⋆s) f
       ) → (
-        â\88\80f,i. ð\9d\90\88â¦\83fâ¦\84 →  Q (⋆) (#i) (⫯*[i]↑f)
+        â\88\80f,i. ð\9d\90\88â\9dªfâ\9d« →  Q (⋆) (#i) (⫯*[i]↑f)
       ) → (
         ∀f,I,L,V.
-        L â\8a¢ ð\9d\90\85+â¦\83Vâ¦\84 â\89\98 f â\86\92  Q L V fâ\86\92 Q (L.â\93\91{I}V) (#O) (â\86\91f) 
+        L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f â\86\92  Q L V fâ\86\92 Q (L.â\93\91[I]V) (#O) (â\86\91f)
       ) → (
-        â\88\80f,I,L. ð\9d\90\88â¦\83fâ¦\84 â\86\92  Q (L.â\93¤{I}) (#O) (↑f)
+        â\88\80f,I,L. ð\9d\90\88â\9dªfâ\9d« â\86\92  Q (L.â\93¤[I]) (#O) (↑f)
       ) → (
         ∀f,I,L,i.
-        L â\8a¢ ð\9d\90\85+â¦\83#iâ¦\84 â\89\98 f â\86\92  Q L (#i) f â\86\92 Q (L.â\93\98{I}) (#(↑i)) (⫯f)
+        L â\8a¢ ð\9d\90\85+â\9dª#iâ\9d« â\89\98 f â\86\92  Q L (#i) f â\86\92 Q (L.â\93\98[I]) (#(↑i)) (⫯f)
       ) → (
-        â\88\80f,L,l. ð\9d\90\88â¦\83fâ¦\84 →  Q L (§l) f
+        â\88\80f,L,l. ð\9d\90\88â\9dªfâ\9d« →  Q L (§l) f
       ) → (
         ∀f1,f2,f,p,I,L,V,T.
-        L â\8a¢ ð\9d\90\85+â¦\83Vâ¦\84 â\89\98 f1 â\86\92 L.â\93§ â\8a¢ð\9d\90\85+â¦\83Tâ¦\84â\89\98 f2 â\86\92 f1 â\8b\93 ⫱f2 ≘ f →
-        Q L V f1 → Q (L.ⓧ) T f2 → Q L (ⓑ{p,I}V.T) f
+        L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f1 â\86\92 L.â\93§ â\8a¢ð\9d\90\85+â\9dªTâ\9d«â\89\98 f2 â\86\92 f1 â\8b\93 â«°f2 ≘ f →
+        Q L V f1 → Q (L.ⓧ) T f2 → Q L (ⓑ[p,I]V.T) f
       ) → (
         ∀f1,f2,f,I,L,V,T.
-        L â\8a¢ ð\9d\90\85+â¦\83Vâ¦\84 â\89\98 f1 â\86\92 L â\8a¢ð\9d\90\85+â¦\83Tâ¦\84 ≘ f2 → f1 ⋓ f2 ≘ f →
-        Q L V f1 → Q L T f2 → Q L (ⓕ{I}V.T) f
+        L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f1 â\86\92 L â\8a¢ð\9d\90\85+â\9dªTâ\9d« ≘ f2 → f1 ⋓ f2 ≘ f →
+        Q L V f1 → Q L T f2 → Q L (ⓕ[I]V.T) f
       ) →
-      â\88\80L,T,f. L â\8a¢ ð\9d\90\85+â¦\83Tâ¦\84 ≘ f →  Q L T f.
+      â\88\80L,T,f. L â\8a¢ ð\9d\90\85+â\9dªTâ\9d« ≘ f →  Q L T f.
 #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #L #T
 @(fqup_wf_ind_eq (Ⓕ) … (⋆) L T) -L -T #G0 #L0 #T0 #IH #G #L * *
 [ #s #HG #HL #HT #f #H destruct -IH