update in basic_2 + web page

+ csx completed
+ notational change to lreq and lfeq to reduce overloading

diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_drops.ma
index 13aec62e424b36c8023c58c9a31989ea2611cbc4..2122b053332e4571e8de261620f14022b13c86af 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_drops.ma
@@ -21,7 +21,7 @@ include "basic_2/i_static/tc_lfxs.ma".
 definition tc_dedropable_sn: predicate (relation3 lenv term term) ≝
                              λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 →
                              ∀K2,T. K1 ⪤**[R, T] K2 → ∀U. ⬆*[f] T ≡ U →
-                             â\88\83â\88\83L2. L1 ⪤**[R, U] L2 & â¬\87*[b, f] L2 â\89¡ K2 & L1 â\89¡[f] L2.
+                             â\88\83â\88\83L2. L1 ⪤**[R, U] L2 & â¬\87*[b, f] L2 â\89¡ K2 & L1 â\89\90[f] L2.
 
 definition tc_dropable_sn: predicate (relation3 lenv term term) ≝
                            λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 → 𝐔⦃f⦄ →

diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lex.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lex.ma
index e38f9f796fcf236ed370ae53c6593127be0d261b..cb32e58b0703ebe2801c132203dbfa8e07c58810 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lex.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lex.ma
@@ -28,7 +28,7 @@ lemma tc_lfxs_lex: ∀R. c_reflexive … R →
 qed.
 
 lemma tc_lfxs_lex_lfeq: ∀R. c_reflexive … R →
-                        â\88\80L1,L. L1 ⪤[LTC â\80¦ R] L â\86\92 â\88\80L2,T. L â\89¡[T] L2 →
+                        â\88\80L1,L. L1 ⪤[LTC â\80¦ R] L â\86\92 â\88\80L2,T. L â\89\90[T] L2 →
                         L1 ⪤**[R, T] L2.
 /3 width=3 by tc_lfxs_lex, tc_lfxs_step_dx, lfeq_fwd_lfxs/ qed.
 
@@ -40,7 +40,7 @@ lemma tc_lfxs_inv_lex_lfeq: ∀R. c_reflexive … R →
                             s_rs_transitive … R (λ_.lex R) →
                             lfeq_transitive R →
                             ∀L1,L2,T. L1 ⪤**[R, T] L2 →
-                            â\88\83â\88\83L. L1 ⪤[LTC â\80¦ R] L & L â\89¡[T] L2.
+                            â\88\83â\88\83L. L1 ⪤[LTC â\80¦ R] L & L â\89\90[T] L2.
 #R #H1R #H2R #H3R #H4R #L1 #L2 #T #H
 lapply (s_rs_transitive_lex_inv_isid … H3R) -H3R #H3R
 @(tc_lfxs_ind_sn … H1R … H) -H -L2

diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/doteqsn_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/doteqsn_3.ma
new file mode 100644 (file)
index 0000000..96060d5
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/doteqsn_3.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( L1 ≐ [ break term 46 f ] break term 46 L2 )"
+   non associative with precedence 45
+   for @{ 'DotEqSn $f $L1 $L2 }.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeqsn_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeqsn_3.ma
deleted file mode 100644 (file)
index 24b7250..0000000
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeqsn_3.ma
+++ /dev/null
@@ -1,19 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( L1 ≡ [ break term 46 f ] break term 46 L2 )"
-   non associative with precedence 45
-   for @{ 'LazyEqSn $f $L1 $L2 }.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
index 5e8cfaeaacc6823246e51cbe5b8451ea49fa77bf..57bf1bfe510eabe95e007e54f0d34a45b5fee7d0 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
@@ -92,7 +92,7 @@ definition co_dropable_dx: predicate (rtmap → relation lenv) ≝
 definition co_dedropable_sn: predicate (rtmap → relation lenv) ≝
                              λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 → ∀f1,K2. R f1 K1 K2 →
                              ∀f2. f ~⊚ f1 ≡ f2 →
-                             â\88\83â\88\83L2. R f2 L1 L2 & â¬\87*[b, f] L2 â\89¡ K2 & L1 â\89¡[f] L2.
+                             â\88\83â\88\83L2. R f2 L1 L2 & â¬\87*[b, f] L2 â\89¡ K2 & L1 â\89\90[f] L2.
 
 (* Basic properties *********************************************************)
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma
index 7cfbf82c03a0827e94ea132587c8fa700e3b99ef..a3ff3cdac86b2dc6bf93d54c0457427437e1ec8d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma
@@ -163,7 +163,7 @@ lemma drops_lexs_trans_next: ∀RN,RP. (∀L. reflexive ? (RN L)) → (∀L. ref
                              ∀f1,K1,K2. K1 ⪤*[RN, RP, f1] K2 →
                              ∀b,f,I1,L1. ⬇*[b, f] L1.ⓘ{I1} ≡ K1 →
                              ∀f2. f ~⊚ f1 ≡ ⫯f2 →
-                             â\88\83â\88\83I2,L2. â¬\87*[b, f] L2.â\93\98{I2} â\89¡ K2 & L1 ⪤*[RN, RP, f2] L2 & RN L1 I1 I2 & L1.â\93\98{I1} â\89¡[f] L2.ⓘ{I2}.
+                             â\88\83â\88\83I2,L2. â¬\87*[b, f] L2.â\93\98{I2} â\89¡ K2 & L1 ⪤*[RN, RP, f2] L2 & RN L1 I1 I2 & L1.â\93\98{I1} â\89\90[f] L2.ⓘ{I2}.
 #RN #RP #H1RN #H1RP #H2RN #H2RP #f1 #K1 #K2 #HK12 #b #f #I1 #L1 #HLK1 #f2 #Hf2
 elim (lexs_liftable_co_dedropable_sn … H1RN H1RP H2RN H2RP … HLK1 … HK12 … Hf2) -K1 -f1 -H1RN -H1RP -H2RN -H2RP
 #X #HX #HLK2 #H1L12 elim (lexs_inv_next1 … HX) -HX
@@ -175,7 +175,7 @@ lemma drops_lexs_trans_push: ∀RN,RP. (∀L. reflexive ? (RN L)) → (∀L. ref
                              ∀f1,K1,K2. K1 ⪤*[RN, RP, f1] K2 →
                              ∀b,f,I1,L1. ⬇*[b, f] L1.ⓘ{I1} ≡ K1 →
                              ∀f2. f ~⊚ f1 ≡ ↑f2 →
-                             â\88\83â\88\83I2,L2. â¬\87*[b, f] L2.â\93\98{I2} â\89¡ K2 & L1 ⪤*[RN, RP, f2] L2 & RP L1 I1 I2 & L1.â\93\98{I1} â\89¡[f] L2.ⓘ{I2}.
+                             â\88\83â\88\83I2,L2. â¬\87*[b, f] L2.â\93\98{I2} â\89¡ K2 & L1 ⪤*[RN, RP, f2] L2 & RP L1 I1 I2 & L1.â\93\98{I1} â\89\90[f] L2.ⓘ{I2}.
 #RN #RP #H1RN #H1RP #H2RN #H2RP #f1 #K1 #K2 #HK12 #b #f #I1 #L1 #HLK1 #f2 #Hf2
 elim (lexs_liftable_co_dedropable_sn … H1RN H1RP H2RN H2RP … HLK1 … HK12 … Hf2) -K1 -f1 -H1RN -H1RP -H2RN -H2RP
 #X #HX #HLK2 #H1L12 elim (lexs_inv_push1 … HX) -HX

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma
index a1ca60e4c5f018e5be41b6e4c09e94ed805e72eb..bc32717b6fd7b453dea41e9d91637548bcaa2bd4 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma
@@ -29,10 +29,10 @@ lemma lreq_co_dropable_dx: co_dropable_dx lreq.
 @lexs_co_dropable_dx qed-.
 
 (* Basic_2A1: includes: lreq_drop_trans_be *)
-lemma lreq_drops_trans_next: â\88\80f2,L1,L2. L1 â\89¡[f2] L2 →
+lemma lreq_drops_trans_next: â\88\80f2,L1,L2. L1 â\89\90[f2] L2 →
                              ∀b,f,I,K2. ⬇*[b, f] L2 ≡ K2.ⓘ{I} → 𝐔⦃f⦄ →
                              ∀f1. f ~⊚ ⫯f1 ≡ f2 →
-                             â\88\83â\88\83K1. â¬\87*[b, f] L1 â\89¡ K1.â\93\98{I} & K1 â\89¡[f1] K2.
+                             â\88\83â\88\83K1. â¬\87*[b, f] L1 â\89¡ K1.â\93\98{I} & K1 â\89\90[f1] K2.
 #f2 #L1 #L2 #HL12 #b #f #I2 #K2 #HLK2 #Hf #f1 #Hf2
 elim (lexs_drops_trans_next … HL12 … HLK2 Hf … Hf2) -f2 -L2 -Hf
 #I1 #K1 #HLK1 #HK12 #H <(ceq_ext_inv_eq … H) -I2
@@ -40,19 +40,19 @@ elim (lexs_drops_trans_next … HL12 … HLK2 Hf … Hf2) -f2 -L2 -Hf
 qed-.
 
 (* Basic_2A1: includes: lreq_drop_conf_be *)
-lemma lreq_drops_conf_next: â\88\80f2,L1,L2. L1 â\89¡[f2] L2 →
+lemma lreq_drops_conf_next: â\88\80f2,L1,L2. L1 â\89\90[f2] L2 →
                             ∀b,f,I,K1. ⬇*[b, f] L1 ≡ K1.ⓘ{I} → 𝐔⦃f⦄ →
                             ∀f1. f ~⊚ ⫯f1 ≡ f2 →
-                            â\88\83â\88\83K2. â¬\87*[b, f] L2 â\89¡ K2.â\93\98{I} & K1 â\89¡[f1] K2.
+                            â\88\83â\88\83K2. â¬\87*[b, f] L2 â\89¡ K2.â\93\98{I} & K1 â\89\90[f1] K2.
 #f2 #L1 #L2 #HL12 #b #f #I1 #K1 #HLK1 #Hf #f1 #Hf2
 elim (lreq_drops_trans_next … (lreq_sym … HL12) … HLK1 … Hf2) // -f2 -L1 -Hf
 /3 width=3 by lreq_sym, ex2_intro/
 qed-.
 
-lemma drops_lreq_trans_next: â\88\80f1,K1,K2. K1 â\89¡[f1] K2 →
+lemma drops_lreq_trans_next: â\88\80f1,K1,K2. K1 â\89\90[f1] K2 →
                              ∀b,f,I,L1. ⬇*[b, f] L1.ⓘ{I} ≡ K1 →
                              ∀f2. f ~⊚ f1 ≡ ⫯f2 →
-                             â\88\83â\88\83L2. â¬\87*[b, f] L2.â\93\98{I} â\89¡ K2 & L1 â\89¡[f2] L2 & L1.â\93\98{I} â\89¡[f] L2.ⓘ{I}.
+                             â\88\83â\88\83L2. â¬\87*[b, f] L2.â\93\98{I} â\89¡ K2 & L1 â\89\90[f2] L2 & L1.â\93\98{I} â\89\90[f] L2.ⓘ{I}.
 #f1 #K1 #K2 #HK12 #b #f #I1 #L1 #HLK1 #f2 #Hf2
 elim (drops_lexs_trans_next … HK12 … HLK1 … Hf2) -f1 -K1
 /2 width=6 by cfull_lift_sn, ceq_lift_sn/

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma
index cc3e75b0a5107964bdd5b503c9e8904aca6fa0d4..1ec062b82f3d048edea7b52cddde230137ae75fb 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/notation/relations/lazyeqsn_3.ma".
+include "basic_2/notation/relations/doteqsn_3.ma".
 include "basic_2/syntax/ceq_ext.ma".
 include "basic_2/relocation/lexs.ma".
 
@@ -23,18 +23,18 @@ definition lreq: relation3 rtmap lenv lenv ≝ lexs ceq_ext cfull.
 
 interpretation
   "ranged equivalence (local environment)"
-  'LazyEqSn f L1 L2 = (lreq f L1 L2).
+  'DotEqSn f L1 L2 = (lreq f L1 L2).
 
 (* Basic properties *********************************************************)
 
-lemma lreq_eq_repl_back: â\88\80L1,L2. eq_repl_back â\80¦ (λf. L1 â\89¡[f] L2).
+lemma lreq_eq_repl_back: â\88\80L1,L2. eq_repl_back â\80¦ (λf. L1 â\89\90[f] L2).
 /2 width=3 by lexs_eq_repl_back/ qed-.
 
-lemma lreq_eq_repl_fwd: â\88\80L1,L2. eq_repl_fwd â\80¦ (λf. L1 â\89¡[f] L2).
+lemma lreq_eq_repl_fwd: â\88\80L1,L2. eq_repl_fwd â\80¦ (λf. L1 â\89\90[f] L2).
 /2 width=3 by lexs_eq_repl_fwd/ qed-.
 
-lemma sle_lreq_trans: â\88\80f2,L1,L2. L1 â\89¡[f2] L2 →
-                      â\88\80f1. f1 â\8a\86 f2 â\86\92 L1 â\89¡[f1] L2.
+lemma sle_lreq_trans: â\88\80f2,L1,L2. L1 â\89\90[f2] L2 →
+                      â\88\80f1. f1 â\8a\86 f2 â\86\92 L1 â\89\90[f1] L2.
 /2 width=3 by sle_lexs_trans/ qed-.
 
 (* Basic_2A1: includes: lreq_refl *)
@@ -48,54 +48,54 @@ lemma lreq_sym: ∀f. symmetric … (lreq f).
 (* Basic inversion lemmas ***************************************************)
 
 (* Basic_2A1: includes: lreq_inv_atom1 *)
-lemma lreq_inv_atom1: â\88\80f,Y. â\8b\86 â\89¡[f] Y → Y = ⋆.
+lemma lreq_inv_atom1: â\88\80f,Y. â\8b\86 â\89\90[f] Y → Y = ⋆.
 /2 width=4 by lexs_inv_atom1/ qed-.
 
 (* Basic_2A1: includes: lreq_inv_pair1 *)
-lemma lreq_inv_next1: â\88\80g,J,K1,Y. K1.â\93\98{J} â\89¡[⫯g] Y →
-                      â\88\83â\88\83K2. K1 â\89¡[g] K2 & Y = K2.ⓘ{J}.
+lemma lreq_inv_next1: â\88\80g,J,K1,Y. K1.â\93\98{J} â\89\90[⫯g] Y →
+                      â\88\83â\88\83K2. K1 â\89\90[g] K2 & Y = K2.ⓘ{J}.
 #g #J #K1 #Y #H
 elim (lexs_inv_next1 … H) -H #Z #K2 #HK12 #H1 #H2 destruct
 <(ceq_ext_inv_eq … H1) -Z /2 width=3 by ex2_intro/
 qed-.
 
 (* Basic_2A1: includes: lreq_inv_zero1 lreq_inv_succ1 *)
-lemma lreq_inv_push1: â\88\80g,J1,K1,Y. K1.â\93\98{J1} â\89¡[↑g] Y →
-                      â\88\83â\88\83J2,K2. K1 â\89¡[g] K2 & Y = K2.ⓘ{J2}.
+lemma lreq_inv_push1: â\88\80g,J1,K1,Y. K1.â\93\98{J1} â\89\90[↑g] Y →
+                      â\88\83â\88\83J2,K2. K1 â\89\90[g] K2 & Y = K2.ⓘ{J2}.
 #g #J1 #K1 #Y #H elim (lexs_inv_push1 … H) -H /2 width=4 by ex2_2_intro/
 qed-.
 
 (* Basic_2A1: includes: lreq_inv_atom2 *)
-lemma lreq_inv_atom2: â\88\80f,X. X â\89¡[f] ⋆ → X = ⋆.
+lemma lreq_inv_atom2: â\88\80f,X. X â\89\90[f] ⋆ → X = ⋆.
 /2 width=4 by lexs_inv_atom2/ qed-.
 
 (* Basic_2A1: includes: lreq_inv_pair2 *)
-lemma lreq_inv_next2: â\88\80g,J,X,K2. X â\89¡[⫯g] K2.ⓘ{J} →
-                      â\88\83â\88\83K1. K1 â\89¡[g] K2 & X = K1.ⓘ{J}.
+lemma lreq_inv_next2: â\88\80g,J,X,K2. X â\89\90[⫯g] K2.ⓘ{J} →
+                      â\88\83â\88\83K1. K1 â\89\90[g] K2 & X = K1.ⓘ{J}.
 #g #J #X #K2 #H
 elim (lexs_inv_next2 … H) -H #Z #K1 #HK12 #H1 #H2 destruct
 <(ceq_ext_inv_eq … H1) -J /2 width=3 by ex2_intro/
 qed-.
 
 (* Basic_2A1: includes: lreq_inv_zero2 lreq_inv_succ2 *)
-lemma lreq_inv_push2: â\88\80g,J2,X,K2. X â\89¡[↑g] K2.ⓘ{J2} →
-                      â\88\83â\88\83J1,K1. K1 â\89¡[g] K2 & X = K1.ⓘ{J1}.
+lemma lreq_inv_push2: â\88\80g,J2,X,K2. X â\89\90[↑g] K2.ⓘ{J2} →
+                      â\88\83â\88\83J1,K1. K1 â\89\90[g] K2 & X = K1.ⓘ{J1}.
 #g #J2 #X #K2 #H elim (lexs_inv_push2 … H) -H /2 width=4 by ex2_2_intro/
 qed-.
 
 (* Basic_2A1: includes: lreq_inv_pair *)
-lemma lreq_inv_next: â\88\80f,I1,I2,L1,L2. L1.â\93\98{I1} â\89¡[⫯f] L2.ⓘ{I2} →
-                     L1 â\89¡[f] L2 ∧ I1 = I2.
+lemma lreq_inv_next: â\88\80f,I1,I2,L1,L2. L1.â\93\98{I1} â\89\90[⫯f] L2.ⓘ{I2} →
+                     L1 â\89\90[f] L2 ∧ I1 = I2.
 #f #I1 #I2 #L1 #L2 #H elim (lexs_inv_next … H) -H
 /3 width=3 by ceq_ext_inv_eq, conj/
 qed-.
 
 (* Basic_2A1: includes: lreq_inv_succ *)
-lemma lreq_inv_push: â\88\80f,I1,I2,L1,L2. L1.â\93\98{I1} â\89¡[â\86\91f] L2.â\93\98{I2} â\86\92 L1 â\89¡[f] L2.
+lemma lreq_inv_push: â\88\80f,I1,I2,L1,L2. L1.â\93\98{I1} â\89\90[â\86\91f] L2.â\93\98{I2} â\86\92 L1 â\89\90[f] L2.
 #f #I1 #I2 #L1 #L2 #H elim (lexs_inv_push … H) -H /2 width=1 by conj/
 qed-.
 
-lemma lreq_inv_tl: â\88\80f,I,L1,L2. L1 â\89¡[⫱f] L2 â\86\92 L1.â\93\98{I} â\89¡[f] L2.ⓘ{I}.
+lemma lreq_inv_tl: â\88\80f,I,L1,L2. L1 â\89\90[⫱f] L2 â\86\92 L1.â\93\98{I} â\89\90[f] L2.ⓘ{I}.
 /2 width=1 by lexs_inv_tl/ qed-.
 
 (* Basic_2A1: removed theorems 5:

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_length.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_length.ma
index fcb54e71ac4f9ddea73abe5e844a632977b9eba3..69c4efa31120341bc33d5c31ea0968f5db4ad64f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_length.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_length.ma
@@ -20,5 +20,5 @@ include "basic_2/relocation/lreq.ma".
 (* Forward lemmas with length for local environments ************************)
 
 (* Basic_2A1: includes: lreq_fwd_length *)
-lemma lreq_fwd_length: â\88\80f,L1,L2. L1 â\89¡[f] L2 → |L1| = |L2|.
+lemma lreq_fwd_length: â\88\80f,L1,L2. L1 â\89\90[f] L2 → |L1| = |L2|.
 /2 width=4 by lexs_fwd_length/ qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_lreq.ma
index ec166cb7d772edf5c4d93d4e33ea9b629b4ba362..b2bf0385a202cd8e6f21c299d29828848bd0c11e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_lreq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_lreq.ma
@@ -28,10 +28,10 @@ theorem lreq_canc_sn: ∀f. left_cancellable … (lreq f).
 theorem lreq_canc_dx: ∀f. right_cancellable … (lreq f).
 /3 width=3 by lexs_canc_dx, lreq_trans, lreq_sym/ qed-.
 
-theorem lreq_join: â\88\80f1,L1,L2. L1 â\89¡[f1] L2 â\86\92 â\88\80f2. L1 â\89¡[f2] L2 →
-                   â\88\80f. f1 â\8b\93 f2 â\89¡ f â\86\92 L1 â\89¡[f] L2.
+theorem lreq_join: â\88\80f1,L1,L2. L1 â\89\90[f1] L2 â\86\92 â\88\80f2. L1 â\89\90[f2] L2 →
+                   â\88\80f. f1 â\8b\93 f2 â\89¡ f â\86\92 L1 â\89\90[f] L2.
 /2 width=5 by lexs_join/ qed-.
 
-theorem lreq_meet: â\88\80f1,L1,L2. L1 â\89¡[f1] L2 â\86\92 â\88\80f2. L1 â\89¡[f2] L2 →
-                   â\88\80f. f1 â\8b\92 f2 â\89¡ f â\86\92 L1 â\89¡[f] L2.
+theorem lreq_meet: â\88\80f1,L1,L2. L1 â\89\90[f1] L2 â\86\92 â\88\80f2. L1 â\89\90[f2] L2 →
+                   â\88\80f. f1 â\8b\92 f2 â\89¡ f â\86\92 L1 â\89\90[f] L2.
 /2 width=5 by lexs_meet/ qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fqus.ma
index 4ea05ba435a0a13cba117b42aeededdf133a62f9..9515e64b9401e95d2fcd636ebe3c874bf96d0a49 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fqus.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fqus.ma
@@ -1,28 +1,50 @@
-lemma csx_fqu_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
-                    ⦃G1, L1⦄ ⊢ ⬈*[h, o] T1 → ⦃G2, L2⦄ ⊢ ⬈*[h, o] T2.
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-/2 width=8 by csx_inv_lref_bind, csx_inv_lift, csx_fwd_flat_dx, csx_fwd_bind_dx, csx_fwd_pair_sn/
-qed-.
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/s_computation/fqus.ma".
+include "basic_2/rt_computation/csx_lsubr.ma".
+
+(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********)
 
-lemma csx_fquq_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
-                     ⦃G1, L1⦄ ⊢ ⬈*[h, o] T1 → ⦃G2, L2⦄ ⊢ ⬈*[h, o] T2.
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H12 #H elim (fquq_inv_gen … H12) -H12
-[ /2 width=5 by csx_fqu_conf/
-| * #HG #HL #HT destruct //
+(* Properties with extended supclosure **************************************)
+
+lemma csx_fqu_conf: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ →
+                    ⦃G1, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → ⦃G2, L2⦄ ⊢ ⬈*[h, o] 𝐒⦃T2⦄.
+#h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+[ /3 width=5 by csx_inv_lref_pair, drops_refl/
+| /2 width=3 by csx_fwd_pair_sn/
+| /2 width=2 by csx_fwd_bind_dx/
+| /2 width=4 by csx_fwd_bind_dx_unit/
+| /2 width=3 by csx_fwd_flat_dx/
+| /4 width=7 by csx_inv_lifts, drops_refl, drops_drop/
 ]
 qed-.
 
-lemma csx_fqup_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ →
-                     ⦃G1, L1⦄ ⊢ ⬈*[h, o] T1 → ⦃G2, L2⦄ ⊢ ⬈*[h, o] T2.
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
-/3 width=5 by csx_fqu_conf/
+lemma csx_fquq_conf: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮[b] ⦃G2, L2, T2⦄ →
+                     ⦃G1, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → ⦃G2, L2⦄ ⊢ ⬈*[h, o] 𝐒⦃T2⦄.
+#h #o #b #G1 #G2 #L1 #L2 #T1 #T2 * /2 width=6 by csx_fqu_conf/
+* #HG #HL #HT destruct //
 qed-.
 
-lemma csx_fqus_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ →
-                     ⦃G1, L1⦄ ⊢ ⬈*[h, o] T1 → ⦃G2, L2⦄ ⊢ ⬈*[h, o] T2.
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H12 #H elim (fqus_inv_gen … H12) -H12
-[ /2 width=5 by csx_fqup_conf/
-| * #HG #HL #HT destruct //
-]
+lemma csx_fqup_conf: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ →
+                     ⦃G1, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → ⦃G2, L2⦄ ⊢ ⬈*[h, o] 𝐒⦃T2⦄.
+#h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
+/3 width=6 by csx_fqu_conf/
 qed-.
 
+lemma csx_fqus_conf: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄ →
+                     ⦃G1, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → ⦃G2, L2⦄ ⊢ ⬈*[h, o] 𝐒⦃T2⦄.
+#h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -H
+/3 width=6 by csx_fquq_conf/
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma
index 79b41f785807c24e5a94485bc426ce22da2fc5fe..21beea53bf176b66b4e92bef5f43cc3f44be5d06 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma
@@ -26,11 +26,11 @@ lemma lfpxs_lpxs: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → ⦃G, L1⦄ ⊢
 /2 width=1 by tc_lfxs_lex/ qed.
 
 lemma lfpxs_lpxs_lfeq: ∀h,G,L1,L. ⦃G, L1⦄ ⊢ ⬈*[h] L →
-                       â\88\80L2,T. L â\89¡[T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2.
+                       â\88\80L2,T. L â\89\90[T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2.
 /2 width=3 by tc_lfxs_lex_lfeq/ qed.
 
 (* Inversion lemmas with uncounted parallel rt-computation for local envs ***)
 
 lemma lfpxs_inv_lpxs_lfeq: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 →
-                           â\88\83â\88\83L. â¦\83G, L1â¦\84 â\8a¢ â¬\88*[h] L & L â\89¡[T] L2.
+                           â\88\83â\88\83L. â¦\83G, L1â¦\84 â\8a¢ â¬\88*[h] L & L â\89\90[T] L2.
 /3 width=5 by lfpx_fsge_comp, lpx_cpxs_trans, lfeq_cpx_trans, tc_lfxs_inv_lex_lfeq/ qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt
index a5cc2eae9009fd448d361c09b52af5d4d63a155b..85df1293965722366eeae58c0ca7d48c772b0807 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt
@@ -2,7 +2,7 @@ cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_fqus.ma
 cpxs_ext.ma
 lpxs.ma lpxs_length.ma lpxs_lpx.ma lpxs_cpxs.ma
 lfpxs.ma lfpxs_length.ma lfpxs_drops.ma lfpxs_fqup.ma lfpxs_lfdeq.ma lfpxs_aaa.ma lfpxs_cpxs.ma lfpxs_lpxs.ma lfpxs_lfpxs.ma
-csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_lsubr.ma csx_lfdeq.ma csx_aaa.ma csx_gcp.ma csx_gcr.ma csx_lfpx.ma csx_cnx.ma csx_cpxs.ma csx_lfpxs.ma csx_csx.ma
+csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_fqus.ma csx_lsubr.ma csx_lfdeq.ma csx_aaa.ma csx_gcp.ma csx_gcr.ma csx_lfpx.ma csx_cnx.ma csx_cpxs.ma csx_lfpxs.ma csx_csx.ma
 csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma 
 lfsx.ma lfsx_drops.ma lfsx_fqup.ma lfsx_lpx.ma lfsx_lpxs.ma lfsx_lfpxs.ma lfsx_csx.ma lfsx_lfsx.ma
 lsubsx.ma lsubsx_lfsx.ma lsubsx_lsubsx.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lpx.ma
index 034ce9c7e938a8ab52a423c20cff19fa459bfe12..a616027336b4306029108d72855f7b7effa4de02 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lpx.ma
@@ -26,5 +26,5 @@ lemma lfpx_lpx: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈[h] L2 → ⦃G, L1⦄ ⊢ 
 (* Inversion lemmas with uncounted parallel rt-transition for local envs ****)
 
 lemma lfpx_inv_lpx_lfeq: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 →
-                         â\88\83â\88\83L. â¦\83G, L1â¦\84 â\8a¢ â¬\88[h] L & L â\89¡[T] L2.
+                         â\88\83â\88\83L. â¦\83G, L1â¦\84 â\8a¢ â¬\88[h] L & L â\89\90[T] L2.
 /3 width=3 by lfpx_fsge_comp, lfxs_inv_lex_lfeq/ qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfeq.ma
index 41b2c033e5b1cdfa693067b102f1d866d146b1a4..5682e7218068f124656b32ee613b3a2468b769d1 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfeq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfeq.ma
@@ -19,5 +19,5 @@ include "basic_2/static/lfdeq.ma".
 
 (* Properties with syntactic equivalence on referred entries ****************)
 
-lemma lfeq_lfdeq: â\88\80h,o,L1,L2,T. L1 â\89¡[T] L2 → L1 ≛[h, o, T] L2.
+lemma lfeq_lfdeq: â\88\80h,o,L1,L2,T. L1 â\89\90[T] L2 → L1 ≛[h, o, T] L2.
 /2 width=3 by lfxs_co/ qed.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma
index 684e57370908a1ac8abdd71a4b1b5b0c4d225043..c248d2acb2516510535d804e041ab95ede00091d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/notation/relations/lazyeqsn_3.ma".
+include "basic_2/notation/relations/doteqsn_3.ma".
 include "basic_2/static/lfxs.ma".
 
 (* SYNTACTIC EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *********)
@@ -23,45 +23,45 @@ definition lfeq: relation3 term lenv lenv ≝
 
 interpretation
    "syntactic equivalence on referred entries (local environment)"
-   'LazyEqSn T L1 L2 = (lfeq T L1 L2).
+   'DotEqSn T L1 L2 = (lfeq T L1 L2).
 
 (* Note: "lfeq_transitive R" is equivalent to "lfxs_transitive ceq R R" *)
 (* Basic_2A1: uses: lleq_transitive *)
 definition lfeq_transitive: predicate (relation3 lenv term term) ≝
-           λR. â\88\80L2,T1,T2. R L2 T1 T2 â\86\92 â\88\80L1. L1 â\89¡[T1] L2 → R L1 T1 T2.
+           λR. â\88\80L2,T1,T2. R L2 T1 T2 â\86\92 â\88\80L1. L1 â\89\90[T1] L2 → R L1 T1 T2.
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma lfeq_inv_bind: â\88\80p,I,L1,L2,V,T. L1 â\89¡[ⓑ{p,I}V.T] L2 →
-                     â\88§â\88§ L1 â\89¡[V] L2 & L1.â\93\91{I}V â\89¡[T] L2.ⓑ{I}V.
+lemma lfeq_inv_bind: â\88\80p,I,L1,L2,V,T. L1 â\89\90[ⓑ{p,I}V.T] L2 →
+                     â\88§â\88§ L1 â\89\90[V] L2 & L1.â\93\91{I}V â\89\90[T] L2.ⓑ{I}V.
 /2 width=2 by lfxs_inv_bind/ qed-.
 
-lemma lfeq_inv_flat: â\88\80I,L1,L2,V,T. L1 â\89¡[ⓕ{I}V.T] L2 →
-                     â\88§â\88§ L1 â\89¡[V] L2 & L1 â\89¡[T] L2.
+lemma lfeq_inv_flat: â\88\80I,L1,L2,V,T. L1 â\89\90[ⓕ{I}V.T] L2 →
+                     â\88§â\88§ L1 â\89\90[V] L2 & L1 â\89\90[T] L2.
 /2 width=2 by lfxs_inv_flat/ qed-.
 
 (* Advanced inversion lemmas ************************************************)
 
-lemma lfeq_inv_zero_pair_sn: â\88\80I,L2,K1,V. K1.â\93\91{I}V â\89¡[#0] L2 →
-                             â\88\83â\88\83K2. K1 â\89¡[V] K2 & L2 = K2.ⓑ{I}V.
+lemma lfeq_inv_zero_pair_sn: â\88\80I,L2,K1,V. K1.â\93\91{I}V â\89\90[#0] L2 →
+                             â\88\83â\88\83K2. K1 â\89\90[V] K2 & L2 = K2.ⓑ{I}V.
 #I #L2 #K1 #V #H
 elim (lfxs_inv_zero_pair_sn … H) -H #K2 #X #HK12 #HX #H destruct
 /2 width=3 by ex2_intro/
 qed-.
 
-lemma lfeq_inv_zero_pair_dx: â\88\80I,L1,K2,V. L1 â\89¡[#0] K2.ⓑ{I}V →
-                             â\88\83â\88\83K1. K1 â\89¡[V] K2 & L1 = K1.ⓑ{I}V.
+lemma lfeq_inv_zero_pair_dx: â\88\80I,L1,K2,V. L1 â\89\90[#0] K2.ⓑ{I}V →
+                             â\88\83â\88\83K1. K1 â\89\90[V] K2 & L1 = K1.ⓑ{I}V.
 #I #L1 #K2 #V #H
 elim (lfxs_inv_zero_pair_dx … H) -H #K1 #X #HK12 #HX #H destruct
 /2 width=3 by ex2_intro/
 qed-.
 
-lemma lfeq_inv_lref_bind_sn: â\88\80I1,K1,L2,i. K1.â\93\98{I1} â\89¡[#⫯i] L2 →
-                             â\88\83â\88\83I2,K2. K1 â\89¡[#i] K2 & L2 = K2.ⓘ{I2}.
+lemma lfeq_inv_lref_bind_sn: â\88\80I1,K1,L2,i. K1.â\93\98{I1} â\89\90[#⫯i] L2 →
+                             â\88\83â\88\83I2,K2. K1 â\89\90[#i] K2 & L2 = K2.ⓘ{I2}.
 /2 width=2 by lfxs_inv_lref_bind_sn/ qed-.
 
-lemma lfeq_inv_lref_bind_dx: â\88\80I2,K2,L1,i. L1 â\89¡[#⫯i] K2.ⓘ{I2} →
-                             â\88\83â\88\83I1,K1. K1 â\89¡[#i] K2 & L1 = K1.ⓘ{I1}.
+lemma lfeq_inv_lref_bind_dx: â\88\80I2,K2,L1,i. L1 â\89\90[#⫯i] K2.ⓘ{I2} →
+                             â\88\83â\88\83I1,K1. K1 â\89\90[#i] K2 & L1 = K1.ⓘ{I1}.
 /2 width=2 by lfxs_inv_lref_bind_dx/ qed-.
 
 (* Basic forward lemmas *****************************************************)
@@ -69,7 +69,7 @@ lemma lfeq_inv_lref_bind_dx: ∀I2,K2,L1,i. L1 ≡[#⫯i] K2.ⓘ{I2} →
 (* Basic_2A1: was: llpx_sn_lrefl *)
 (* Note: this should have been lleq_fwd_llpx_sn *)
 lemma lfeq_fwd_lfxs: ∀R. c_reflexive … R →
-                     â\88\80L1,L2,T. L1 â\89¡[T] L2 → L1 ⪤*[R, T] L2.
+                     â\88\80L1,L2,T. L1 â\89\90[T] L2 → L1 ⪤*[R, T] L2.
 #R #HR #L1 #L2 #T * #f #Hf #HL12
 /4 width=7 by lexs_co, cext2_co, ex2_intro/
 qed-.
@@ -77,7 +77,7 @@ qed-.
 (* Basic_properties *********************************************************)
 
 lemma frees_lfeq_conf: ∀f,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≡ f →
-                       â\88\80L2. L1 â\89¡[T] L2 → L2 ⊢ 𝐅*⦃T⦄ ≡ f.
+                       â\88\80L2. L1 â\89\90[T] L2 → L2 ⊢ 𝐅*⦃T⦄ ≡ f.
 #f #L1 #T #H elim H -f -L1 -T
 [ /2 width=3 by frees_sort/
 | #f #i #Hf #L2 #H2

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_fsle.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_fsle.ma
index 0f80c977289f687fb8d248bb612c443df284c606..bb67cd3254a57b9a853704a05da6aab88a87bd99 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_fsle.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_fsle.ma
@@ -29,5 +29,5 @@ qed.
 (* Forward lemmas with free variables inclusion for restricted closures *****)
 
 lemma lfeq_lfxs_trans: ∀R. lfeq_transitive R →
-                       â\88\80L1,L,T. L1 â\89¡[T] L → ∀L2. L ⪤*[R, T] L2 → L1 ⪤*[R, T] L2.
+                       â\88\80L1,L,T. L1 â\89\90[T] L → ∀L2. L ⪤*[R, T] L2 → L1 ⪤*[R, T] L2.
 /4 width=16 by lfeq_fsle_comp, lfxs_trans_fsle, lfxs_trans_next/ qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma
index 03772d98c9195bb7bfe04f588b14debc9ca36ae6..9e334565f386fc740e66a8f1bf9b6b19c905300e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma
@@ -22,7 +22,7 @@ include "basic_2/static/lfxs.ma".
 definition dedropable_sn: predicate (relation3 lenv term term) ≝
                           λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 →
                           ∀K2,T. K1 ⪤*[R, T] K2 → ∀U. ⬆*[f] T ≡ U →
-                          â\88\83â\88\83L2. L1 ⪤*[R, U] L2 & â¬\87*[b, f] L2 â\89¡ K2 & L1 â\89¡[f] L2.
+                          â\88\83â\88\83L2. L1 ⪤*[R, U] L2 & â¬\87*[b, f] L2 â\89¡ K2 & L1 â\89\90[f] L2.
 
 definition dropable_sn: predicate (relation3 lenv term term) ≝
                         λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 → 𝐔⦃f⦄ →

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lex.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lex.ma
index 01f578f4eb581a764f2436e6f75bfa99604cb4ff..2957ac1c3460d3c10c86a753533866fcba250952 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lex.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lex.ma
@@ -31,7 +31,7 @@ qed.
 lemma lfxs_inv_lex_lfeq: ∀R. c_reflexive … R →
                          lfxs_fsge_compatible R →
                          ∀L1,L2,T. L1 ⪤*[R, T] L2 →
-                         â\88\83â\88\83L. L1 ⪤[R] L & L â\89¡[T] L2.
+                         â\88\83â\88\83L. L1 ⪤[R] L & L â\89\90[T] L2.
 #R #H1R #H2R #L1 #L2 #T * #f1 #Hf1 #HL
 elim (lexs_sdj_split … ceq_ext … HL 𝐈𝐝 ?) -HL
 [ #L0 #HL10 #HL02 |*: /2 width=1 by ext2_refl, sdj_isid_dx/ ] -H1R

diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
index 64c160295550e55a8020b3c91d92308adc20b60f..40e94b86ffa7b7422823debc7494b6f94e798891 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -110,7 +110,7 @@ table {
              [ [ "refinement for lenvs" ] "lsubsx" + "( ? ⊢ ? ⊆ⓧ[?,?,?] ? )" "lsubsx_lfsx" + "lsubsx_lsubsx" * ]
              [ [ "strongly normalizing for lenvs on referred entries" ] "lfsx" + "( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_drops" + "lfsx_fqup" + "lfsx_cpx" + "lfsx_cpxs" + "lfsx_lfpxs" + "lfsx_lfsx" * ]
              [ [ "strongly normalizing for term vectors" ] "csx_vector" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ]
-             [ [ "strongly normalizing for terms" ] "csx" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_lfdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_lfpxs" + "csx_csx" * ]
+             [ [ "strongly normalizing for terms" ] "csx" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_fqus" + "csx_lsubr" + "csx_lfdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_lfpxs" + "csx_csx" * ]
              [ [ "for lenvs on referred entries" ] "lfpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lpxs" + "lfpxs_lfpxs" * ]
              [ [ "for lenvs on all entries" ] "lpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?] ? )" "lpxs_length" + "lpxs_lpx" + "lpxs_cpxs" * ]
              [ [ "for binders" ] "cpxs_ext" + "( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" * ]