- main proof case closed in the 4th component of preservation

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / web / basic_2_src.tbl

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 ee1b110eb9d2dafb8f57b50ba97a5357420bbca5..8a80df07e0f7df1eaa3c51bd6bb51b0459f0dfd7 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
@@ -3,7 +3,7 @@ name "basic_2_src"
 table {
    class "grey"
    [ { "component" * } {
-        [ { "plane" * } { 
+        [ { "plane" * } {
              [ "files" * ]
           }
         ]
@@ -29,7 +29,7 @@ table {
 *)
    class "prune"
    [ { "dynamic typing" * } {
-(*        
+(*
         [ { "local env. ref. for native type assignment" * } {
              [ "lsubn ( ? ⊢ ? :⊑ ? )" "lsubn_ldrop" "lsubn_cpcs" "lsubn_nta" * ]
           }
@@ -39,8 +39,16 @@ table {
           }
         ]
 *)
+        [ { "\"big tree\" parallel computation" * } {
+             [ "yprs ( ? ⊢ ⦃?,?⦄ ≥[g] ⦃?,?⦄ )" "yprs_yprs"  "ygt ( ? ⊢ ⦃?,?⦄ >[g] ⦃?,?⦄ )" "ygt_ygt" * ]
+          }
+        ]
+        [ { "\"big tree\" parallel reduction" * } {
+             [ "ypr ( ? ⊢ ⦃?,?⦄ ≽[g] ⦃?,?⦄ )" "ysc ( ? ⊢ ⦃?,?⦄ ≻[g] ⦃?,?⦄ )" * ]
+          }
+        ]
         [ { "local env. ref. for stratified native validity" * } {
-             [ "lsubsv ( ? ⊢ ? ⊩:⊑[?] ? )" "lsubsv_ldrop" "lsubsv_snv" * ]
+             [ "lsubsv ( ? ⊢ ? ⊩:⊑[?] ? )" "lsubsv_ldrop" + "lsubsv_lsuba" + "lsubsv_ssta" + "lsubsv_dxprs" + "lsubsv_cpcs" + "lsubsv_snv" * ]
           }
         ]
         [ { "stratified native validity" * } {
@@ -86,12 +94,8 @@ table {
              [ "fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ )" "fprs_aaa" + "fprs_fprs" * ]
           }
         ]
-        [ { "\"big tree\" parallel computation" * } {
-             [ "yprs ( ? ⊢ ⦃?,?⦄ ≥[g] ⦃?,?⦄ )" "yprs_yprs"  "ygt ( ? ⊢ ⦃?,?⦄ >[g] ⦃?,?⦄ )" "ygt_ygt" * ]
-          }
-        ]
         [ { "decomposed extended computation" * } {
-             [ "dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )" "dxprs_lift" + "dxprs_ltpss_dx" + "dxprs_ltpss_sn" + "dxprs_aaa" + "dxpr_lsubss" + "dxprs_dxprs" * ]
+             [ "dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )" "dxprs_lift" + "dxprs_ltpss_dx" + "dxprs_ltpss_sn" + "dxprs_aaa" + "dxprs_dxprs" * ]
           }
         ]
         [ { "weakly normalizing computation" * } {
@@ -123,7 +127,7 @@ table {
      }
    ]
    class "water"
-   [ { "reducibility" * } {        
+   [ { "reducibility" * } {
         [ { "context-sensitive focalized reduction" * } {
              [ "cfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ )" "cnfpr_ltpss" + "cfpr_aaa" + "cfpr_cpr" + "cfpr_cfpr" * ]
           }
@@ -133,14 +137,10 @@ table {
              [ "fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )" "fpr_cpr" + "fpr_fpr" * ]
           }
         ]
-        [ { "\"big tree\" parallel reduction" * } {
-             [ "ypr ( ? ⊢ ⦃?,?⦄ ≽[g] ⦃?,?⦄ )" "ysc ( ? ⊢ ⦃?,?⦄ ≻[g] ⦃?,?⦄ )" * ]
-          }
-        ]
         [ { "context-sensitive normal forms" * } {
              [ "cnf ( ? ⊢ 𝐍⦃?⦄ )" "cnf_lift" + "cnf_cif" * ]
           }
-        ]       
+        ]
         [ { "context-sensitive reduction" * } {
              [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" + "cpr_tpss" + "cpr_ltpss_dx" + "cpr_ltpss_sn" + "cpr_delift" + "cpr_aaa" + "cpr_ltpr" + "cpr_cpr" * ]
           }
@@ -163,17 +163,19 @@ table {
    class "green"
    [ { "unwind" * } {
         [ { "iterated stratified static type assignment" * } {
-             [ "sstas ( ⦃?,?⦄ ⊢ ? •*[?] ? )" "sstas_lift" + "sstas_ltpss_dx" + "sstas_ltpss_sn" + "sstas_aaa" + "sstas_lsubss" + "sstas_sstas" * ]
+             [ "sstas ( ⦃?,?⦄ ⊢ ? •*[?] ? )" "sstas_lift" + "sstas_ltpss_dx" + "sstas_ltpss_sn" + "sstas_aaa" + "sstas_sstas" * ]
           }
         ]
      }
    ]
    class "grass"
    [ { "static typing" * } {
-        [ { "local env. ref. for stratified static type assignment" * } {
+(*        
+       [ { "local env. ref. for stratified static type assignment" * } {
              [ "lsubss ( ? •⊑[?] ? )" "lsubss_ldrop" + "lsubss_ssta" + "lsubss_lsubss" * ]
           }
         ]
+*)
         [ { "stratified static type assignment" * } {
              [ "ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )" "ssta_lift" + "ssta_ltpss_dx" + "ssta_ltpss_sn" + "ssta_aaa" + "ssta_ssta" * ]
           }
@@ -197,7 +199,7 @@ table {
         [ { "basic local env. thinning" * } {
              [ "thin ( ? ▼*[?,?] ≡ ? )" "thin_ldrop" + "thin_delift" * ]
           }
-        ]        
+        ]
         [ { "inverse basic term relocation" * } {
              [ "delift ( ? ⊢ ? ▼*[?,?] ≡ ? )" "delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? )" "delift_lift" + "delift_tpss" + "delift_ltpss" + "delift_delift" * ]
           }
@@ -208,7 +210,7 @@ table {
              [ "tpss ( ? ⊢ ? ▶*[?,?] ? )" "tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? )" "tpss_lift" "tpss_tpss" * ]
           }
         ]
-        [ { "generic local env. slicing" * } { 
+        [ { "generic local env. slicing" * } {
              [ "ldrops ( ⇩*[?] ? ≡ ? )" "ldrops_ldrop" + "ldrops_ldrops" * ]
           }
         ]
@@ -219,17 +221,17 @@ table {
         ]
         [ { "generic term relocation" * } {
              [ "lifts_vector ( ⇧*[?] ? ≡ ? )" "lifts_lift_vector" * ]
-             [ "lifts ( ⇧*[?] ? ≡ ? )" "lifts_lift" + "lifts_lifts" * ] 
+             [ "lifts ( ⇧*[?] ? ≡ ? )" "lifts_lift" + "lifts_lifts" * ]
           }
         ]
-        [ { "support for generic relocation" * } { 
+        [ { "support for generic relocation" * } {
              [ "gr2 ( @⦃?,?⦄ ≡ ? )" "gr2_plus ( ? + ? )" "gr2_minus ( ? ▭ ? ≡ ? )" "gr2_gr2" * ]
           }
         ]
      }
    ]
-   class "orange"   
-   [ { "substitution" * } { 
+   class "orange"
+   [ { "substitution" * } {
         [ { "parallel substitution" * } {
              [ "tps ( ? ⊢ ? ▶[?,?] ? )" "tps_lift" + "tps_tps" * ]
           }
@@ -257,7 +259,7 @@ table {
         ]
      }
    ]
-   class "red"   
+   class "red"
    [ { "grammar" * } {
         [ { "same head term form" * } {
              [ "tshf ( ? ≈ ? )" "(tshf_tshf)" * ]
@@ -277,11 +279,11 @@ table {
              [ "term" "term_weight ( ♯{?} )" "term_simple ( 𝐒⦃?⦄ )" "term_vector" * ]
              [ "item" * ]
           }
-        ] 
+        ]
         [ { "external syntax" * } {
              [ "aarity" * ]
           }
-        ] 
+        ]
      }
    ]
 }