more results towards the "big-tree" theorem ...

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma
index d951e4154b1c41c0f2ab2e0bd8c61961e5a550b5..43e4d3ad5a34d8806199ba51eb82f72d60d43ff9 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma
@@ -17,7 +17,7 @@ include "basic_2/computation/csx_tstc_vector.ma".
 
 (* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
 
-(* Main properties concerning atomic arity assignment ***********************)
+(* Main properties on atomic arity assignment *******************************)
 
 theorem aaa_csx: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⬊*[h, g] T.
 #h #g #G #L #T #A #H

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma
index 0ad3212fc9a796610ad45e9bbea49b379d3b13fe..f8996e4a9145e539c17dd127792c1b797d24d308 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma
@@ -14,12 +14,13 @@
 
 include "basic_2/notation/relations/btsn_5.ma".
 include "basic_2/reduction/fpbc.ma".
+include "basic_2/computation/csx.ma".
 
 (* "BIG TREE" STRONGLY NORMALIZING TERMS ************************************)
 
 inductive fsb (h) (g): relation3 genv lenv term ≝
 | fsb_intro: ∀G1,L1,T1. (
-                ∀G2,L2,T2.  ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → fsb h g G2 L2 T2
+                ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → fsb h g G2 L2 T2
              ) → fsb h g G1 L1 T1
 .
 
@@ -41,3 +42,9 @@ theorem fsb_ind_alt: ∀h,g. ∀R: relation3 …. (
                      ∀G,L,T. ⦃G, L⦄ ⊢ ⦥[h, g] T → R G L T.
 #h #g #R #IH #G #L #T #H elim H -G -L -T /5 width=1 by fpb_fpbc/
 qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma fsb_inv_csx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⦥[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] T.
+#h #g #G #L #T #H elim H -G -L -T /5 width=1 by csx_intro, fpbc_cpx/
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq.ma
new file mode 100644 (file)
index 0000000..73e04e3
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq.ma
@@ -0,0 +1,46 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/notation/relations/bteq_6.ma".
+include "basic_2/grammar/lenv_length.ma".
+include "basic_2/grammar/genv.ma".
+
+(* EQUIVALENT "BIG TREE" NORMAL FORMS ***************************************)
+
+definition bteq: tri_relation genv lenv term ≝
+                 λG1,L1,T1,G2,L2,T2.
+                 ∧∧ G1 = G2 & |L1| = |L2| & T1 = T2.
+
+interpretation
+   "equivalent 'big tree' normal forms (closure)"
+   'BTEq G1 L1 T1 G2 L2 T2 = (bteq G1 L1 T1 G2 L2 T2).
+
+(* Basic_properties *********************************************************)
+
+lemma bteq_refl: tri_reflexive … bteq.
+/2 width=1 by and3_intro/ qed.
+
+lemma bteq_sym: tri_symmetric … bteq.
+#G1 #G2 #L1 #L2 #T1 #T2 * //
+qed-.
+
+lemma bteq_dec: ∀G1,G2,L1,L2,T1,T2. Decidable (⦃G1, L1, T1⦄ ⪴ ⦃G2, L2, T2⦄).
+#G1 #G2 #L1 #L2 #T1 #T2 elim (genv_eq_dec G1 G2)
+#H1G [2: @or_intror * #H2G #H2L #H2T destruct /2 width=1 by/ ]
+elim (eq_nat_dec (|L1|) (|L2|))
+#H1L [2: @or_intror * #H2G #H2L #H2T destruct /2 width=1 by/ ]
+elim (term_eq_dec T1 T2)
+#H1T [2: @or_intror * #H2G #H2L #H2T destruct /2 width=1 by/ ]
+/3 width=1 by and3_intro, or_introl/
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq_bteq.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq_bteq.ma
new file mode 100644 (file)
index 0000000..4dad596
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq_bteq.ma
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/grammar/bteq.ma".
+
+(* EQUIVALENT "BIG TREE" NORMAL FORMS ***************************************)
+
+(* Main properties **********************************************************)
+
+theorem bteq_trans: tri_transitive … bteq.
+#G1 #G #L1 #L #T1 #T * //
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/bteq_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/bteq_6.ma
new file mode 100644 (file)
index 0000000..a417d0a
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/bteq_6.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( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⪴ break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+   non associative with precedence 45
+   for @{ 'BTEq $G1 $L1 $T1 $G2 $L2 $T2 }.

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 c4338500950f4140a623cb54edccf5babb47db10..e7a665c668736d3f005cdc40d2063b162ddd1b1d 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
@@ -254,6 +254,7 @@ table {
           }
         ]
         [ { "closures" * } {
+             [ "bteq ( ⦃?,?,?⦄ ⪴ ⦃?,?,?⦄ )" "bteq_bteq" * ]
              [ "cl_shift ( ? @@ ? )" "cl_weight ( ♯{?,?,?} )" * ]
           }
         ]

diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index 6cf8ab99f741ec47c27a325b99bb8dde5291a284..32e7509735b84e446357d95a4c1bb75a20d71cec 100644 (file)
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1528,7 +1528,7 @@ let predefined_classes = [
  ["□"; "◽"; "▪"; "◾"; ];
  ["◊"; "♢"; "⧫"; "♦"; "⟐"; "⟠"; ] ;
  [">"; "⭃"; "⧁"; "〉"; "»"; "❭"; "❯"; "❱"; "▸"; "►"; "▶"; ] ;
- ["≥"; "⪀"; "≽"; "⥸"; ]; 
+ ["â\89¥"; "âª\80"; "â\89½"; "⪴"; "⥸"; ]; 
  ["a"; "α"; "𝕒"; "𝐚"; "𝛂"; "ⓐ"; ] ;
  ["A"; "ℵ"; "𝔸"; "𝐀"; "Ⓐ"; ] ;
  ["b"; "β"; "ß"; "𝕓"; "𝐛"; "𝛃"; "ⓑ"; ] ;