From 132d053caaeb9f8311fb0c807a9d7fd8d7acc827 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 14 Mar 2013 23:06:19 +0000
Subject: [PATCH] - main proof case closed in the 4th component of preservation
 - bug fix in Makefile: now both xoa and probe receive both configuration
 files - useless notion lsubss removed (to be replaced by lsubse)

---
 matita/matita/contribs/lambdadelta/Makefile   | 10 +++++----
 .../lambdadelta/basic_2/dynamic/snv_ltpr.ma   | 21 +++++++++----------
 .../lsubss/dxprs_lsubss.etc}                  |  0
 .../lsubss.ma => etc/lsubss/lsubss.etc}       |  1 -
 .../lsubss/lsubss_ldrop.etc}                  |  0
 .../lsubss/lsubss_lsubss.etc}                 |  0
 .../lsubss/lsubss_ssta.etc}                   |  0
 .../lsubss/sstas_lsubss.etc}                  |  0
 .../lambdadelta/basic_2/web/basic_2_src.tbl   |  8 ++++---
 9 files changed, 21 insertions(+), 19 deletions(-)
 rename matita/matita/contribs/lambdadelta/basic_2/{computation/dxprs_lsubss.ma => etc/lsubss/dxprs_lsubss.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{static/lsubss.ma => etc/lsubss/lsubss.etc} (99%)
 rename matita/matita/contribs/lambdadelta/basic_2/{static/lsubss_ldrop.ma => etc/lsubss/lsubss_ldrop.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{static/lsubss_lsubss.ma => etc/lsubss/lsubss_lsubss.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{static/lsubss_ssta.ma => etc/lsubss/lsubss_ssta.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{unwind/sstas_lsubss.ma => etc/lsubss/sstas_lsubss.etc} (100%)

diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile
index 3e5b74eaf..8493b47c0 100644
--- a/matita/matita/contribs/lambdadelta/Makefile
+++ b/matita/matita/contribs/lambdadelta/Makefile
@@ -3,11 +3,13 @@ H    := @
 
 TRIM := sed "s/ \\+$$//"
 
-XOA_DIR     := ../../../components/binaries/xoa
-XOA         := xoa.native
 XOA_CONF    := ground_2/xoa.conf.xml
 XOA_TARGETS := ground_2/xoa_notation.ma ground_2/xoa.ma
 
+XOA_DIR     := ../../../components/binaries/xoa
+XOA         := xoa.native
+XOA_OPTS    := ../../matita.conf.xml $(XOA_CONF)
+
 DEP_DIR     := ../../../components/binaries/matitadep
 DEP         := matitadep.native
 
@@ -16,7 +18,7 @@ MAC         := mac.native
 
 PRB_DIR     := ../../../components/binaries/probe
 PRB         := probe.native
-PRB_OPTS    := ../../matita.conf.xml $(XOA_CONF) -g 
+PRB_OPTS    := $(XOA_OPTS) -g 
 
 ORIG        := . ./orig.sh 
 ORIGS       := basic_2/basic_1.orig
@@ -50,7 +52,7 @@ xoa: $(XOA_TARGETS)
 
 $(XOA_TARGETS): $(XOA_CONF)
 	@echo "  EXEC $(XOA) $(XOA_CONF)"
-	$(H)MATITA_RT_BASE_DIR=../.. $(XOA_DIR)/$(XOA) $(XOA_CONF)
+	$(H)MATITA_RT_BASE_DIR=../.. $(XOA_DIR)/$(XOA) $(XOA_OPTS)
 
 # orig #######################################################################
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma
index f3238fbd9..2afaa8e06 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma
@@ -66,15 +66,14 @@ fact snv_ltpr_tpr_aux: ∀h,g,L0,T0.
   | #b #V2 #W20 #T20 #T2 #HV12 #HT202 #H1 #H2 destruct
     elim (snv_inv_bind … HT1) -HT1 #HW20 #HT20
     elim (dxprs_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW230 #_ #H destruct -T30
-    lapply (cprs_div … HW230 … HW10) -W30 #HW210
-    lapply (ltpr_cpcs_conf … HL12 … HW210) -HW210 #HW210
+    lapply (cprs_div … HW10 … HW230) -W30 #HW120
+    elim (snv_fwd_ssta … HW20) #U20 #l0 #HWU20
+    elim (ssta_fwd_correct … HVW1) <minus_plus_m_m #U10 #HWU10
+    elim (ssta_ltpr_cpcs_aux … IH1 IH3 … HW20 … HWU10 … HWU20) // -IH3 -HWU10
+    [2: /3 width=5/ |3: /2 width=1/
+    |4: /4 width=4 by ygt_yprs_trans, ypr_yprs, ypr_ssta, fw_ygt/
+    ] #H #_ -IH2 -U10 destruct
+    lapply (IH4 … HT20 (L1.ⓓV1) ?) [ /2 width=6/ | /2 width=1/ ] -U20 -W10 -l0 -IH4 -HT20 -HW20 #HT20
     lapply (IH1 … HL12 … HV12) // [ /2 width=1/ ] #HV2
-    lapply (IH1 … HW20 … HL12 W20 ?) // [ /2 width=1/ ] -HW20 #HW20
-    lapply (IH1 … HT20 … (L2.ⓛW20) … HT202) [1,2: /2 width=1/ ] -IH1 -HT20 -HT202 #HT2
-    elim (IH3 … HVW1 … HL12 … HV12) // [2: /2 width=1/ ] -HV1 -HVW1 -HV12 #W200 #HVW200 #H
-    lapply (cpcs_trans … HW210 … H) -W10 #HW200
-    lapply (IH4 … HT2 (L2.ⓓV2) ?) -HT2
-    [ (* /2 width=4/ *)
-    |
-    | /2 width=1/
-    ] 
+    lapply (IH1 … HT20 … (L2.ⓓV2) … HT202) [1,2: /2 width=1/ ] -L1 -V1 -W20 -T20 /2 width=1/
+  |
\ No newline at end of file
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lsubss.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/dxprs_lsubss.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lsubss.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/dxprs_lsubss.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubss.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/lsubss.etc
similarity index 99%
rename from matita/matita/contribs/lambdadelta/basic_2/static/lsubss.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/lsubss.etc
index 356d7fe11..7e9751a9f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/lsubss.etc
@@ -16,7 +16,6 @@ include "basic_2/static/ssta.ma".
 
 (* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED STATIC TYPE ASSIGNMENT *******)
 
-(* Note: may not be transitive *)
 inductive lsubss (h:sh) (g:sd h): relation lenv ≝
 | lsubss_atom: lsubss h g (⋆) (⋆)
 | lsubss_pair: ∀I,L1,L2,W. lsubss h g L1 L2 →
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubss_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/lsubss_ldrop.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/static/lsubss_ldrop.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/lsubss_ldrop.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubss_lsubss.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/lsubss_lsubss.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/static/lsubss_lsubss.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/lsubss_lsubss.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubss_ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/lsubss_ssta.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/static/lsubss_ssta.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/lsubss_ssta.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lsubss.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/sstas_lsubss.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lsubss.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/sstas_lsubss.etc
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 ea981eaa5..8a80df07e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -95,7 +95,7 @@ table {
           }
         ]
         [ { "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" * } {
@@ -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" * ]
           }
-- 
2.39.2