From 520d60c708a792bb77f8e290f35ec51f7dbfa29a Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 18 Mar 2013 19:10:19 +0000
Subject: [PATCH] - more understanding of the "big tree" reduction step

---
 .../lambdadelta/basic_2/dynamic/snv_ltpr.ma   |  2 +-
 .../basic_2/dynamic/snv_ssta_ltpr.ma          |  4 +-
 .../lambdadelta/basic_2/etc/ygt/zgt.ma        | 43 +++++++++++++++++++
 3 files changed, 47 insertions(+), 2 deletions(-)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/ygt/zgt.ma

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 17ae5d326..6a0be5953 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma
@@ -71,7 +71,7 @@ fact snv_ltpr_tpr_aux: ∀h,g,L0,T0.
     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/
+    |4: /4 width=4 by ygt_yprs_trans, fw_ygt, sstas_yprs, ssta_sstas/
     ] #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
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_ltpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_ltpr.ma
index d7a40613e..e7f402513 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_ltpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_ltpr.ma
@@ -83,7 +83,9 @@ fact ssta_ltpr_tpr_aux: ∀h,g,L0,T0.
     elim (snv_fwd_ssta … HW) #l1 #V #HWV
     lapply (IH3 … HVW1) -IH3 // [ /2 width=1/ ] #HW1
     elim (ssta_ltpr_cpcs_aux … IH2 IH1 … HWX1 … HWV …) -IH2 -HWX1 //
-    [2: /2 width=1/ |3: /3 width=4 by ygt_strap1, fw_ygt, ypr_ssta/ ] #H #_ destruct -X1
+    [2: /2 width=1/
+    |3: /4 width=4 by ygt_yprs_trans, fw_ygt, sstas_yprs, ssta_sstas/
+    ] #H #_ destruct -X1
     elim (IH1 … HVW1 … HL12 … HV12) -HVW1 // -HV1 [2: /2 width=1/ ] #W2 #HVW2 #HW12
     elim (IH1 … HWV … HL12 W) -HWV // -HW [2: /2 width=1/ ] #V0 #HWV0 #_
     elim (IH1 … HTU2 (L2.ⓛW) … HT20) -IH1 -HTU2 -HT20 // [2,3: /2 width=1/ ] -HT2 #U20 #HTU20 #HU20
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/ygt/zgt.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/ygt/zgt.ma
new file mode 100644
index 000000000..ce6c973fd
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/ygt/zgt.ma
@@ -0,0 +1,43 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/computation/ltprs.ma".
+include "basic_2/dynamic/lsubsv.ma".
+
+(* "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **********************)
+
+axiom yprs: ∀h. sd h → bi_relation lenv term.
+
+interpretation "'big tree' parallel computation (closure)"
+   'BTPRedStar h g L1 T1 L2 T2 = (yprs h g L1 T1 L2 T2).
+
+axiom cprs_yprs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → h ⊢ ⦃L, T1⦄ ≥[g] ⦃L, T2⦄.
+
+axiom sstas_yprs: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 •*[g] T2 →
+                  h ⊢ ⦃L, T1⦄ ≥[g] ⦃L, T2⦄.
+
+axiom lsubsv_yprs: ∀h,g,L1,L2,T. h ⊢ L2 ¡⊑[g] L1 → h ⊢ ⦃L1, T⦄ ≥[g] ⦃L2, T⦄.
+
+axiom ltpr_cprs_yprs: ∀h,g,L1,L2,T1,T2. L1 ➡ L2 → L2 ⊢ T1 ➡* T2 →
+                      h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄.
+
+axiom ygt: ∀h. sd h → bi_relation lenv term.
+
+interpretation "'big tree' proper parallel computation (closure)"
+   'BTPRedStarProper h g L1 T1 L2 T2 = (ygt h g L1 T1 L2 T2).
+
+axiom fw_ygt: ∀h,g,L1,L2,T1,T2. ♯{L2, T2} < ♯{L1, T1} → h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄.
+
+axiom ygt_yprs_trans: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ >[g] ⦃L, T⦄ →
+                      h ⊢ ⦃L, T⦄ ≥[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄.
-- 
2.39.2