--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/btpredstar_8.ma".
+include "basic_2/substitution/fsupp.ma".
+include "basic_2/reduction/fpb.ma".
+include "basic_2/computation/cprs.ma".
+include "basic_2/computation/lprs.ma".
+
+(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************)
+
+definition fpbs: ∀h. sd h → tri_relation genv lenv term ≝
+ λh,g. tri_TC … (fpb h g).
+
+interpretation "'big tree' parallel computation (closure)"
+ 'BTPRedStar h g G1 L1 T1 G2 L2 T2 = (fpbs h g G1 L1 T1 G2 L2 T2).
+
+(* Basic eliminators ********************************************************)
+
+lemma fpbs_ind: ∀h,g,G1,L1,T1. ∀R:relation3 genv lenv term. R G1 L1 T1 →
+ (∀L,G2,G,L2,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) →
+ ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2.
+/3 width=8 by tri_TC_star_ind/ qed-.
+
+lemma fpbs_ind_dx: ∀h,g,G2,L2,T2. ∀R:relation3 genv lenv term. R G2 L2 T2 →
+ (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) →
+ ∀G1,L1,T1. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → R G1 L1 T1.
+/3 width=8 by tri_TC_star_ind_dx/ qed-.
+
+(* Basic properties *********************************************************)
+
+lemma fpbs_refl: ∀h,g. tri_reflexive … (fpbs h g).
+/2 width=1 by tri_inj/ qed.
+
+lemma fpb_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+/2 width=1 by tri_inj/ qed.
+
+lemma fpbs_strap1: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ →
+ ⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+/2 width=5 by tri_step/ qed-.
+
+lemma fpbs_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ →
+ ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+/2 width=5 by tri_TC_strap/ qed-.
+
+(* Note: this is a general property of bi_TC *)
+lemma fsupp_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsupp_ind … L2 T2 H) -G2 -L2 -T2
+/3 width=5 by fpb_fsup, tri_step, fpb_fpbs/
+qed.
+
+lemma cprs_fpbs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄.
+#h #g #G #L #T1 #T2 #H @(cprs_ind … H) -T2
+/3 width=5 by fpb_cpr, fpbs_strap1/
+qed.
+
+lemma lprs_fpbs: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1, T⦄ ≥[h, g] ⦃G, L2, T⦄.
+#h #g #G #L1 #L2 #T #H @(lprs_ind … H) -L2
+/3 width=5 by fpb_lpr, fpbs_strap1/
+qed.
+
+lemma cpr_lpr_fpbs: ∀h,g,G,L1,L2,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L1⦄ ⊢ ➡ L2 →
+ ⦃G, L1, T1⦄ ≥[h, g] ⦃G, L2, T2⦄.
+/4 width=5 by fpbs_strap1, fpb_lpr, fpb_cpr/ qed.
+
+lemma ssta_fpbs: ∀h,g,G,L,T,U,l.
+ ⦃G, L⦄ ⊢ T ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T •[h, g] U →
+ ⦃G, L, T⦄ ≥[h, g] ⦃G, L, U⦄.
+/3 width=2 by fpb_fpbs, fpb_ssta/ qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/fpbs.ma".
+
+(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************)
+
+(* Main properties **********************************************************)
+
+theorem fpbs_trans: ∀h,g. tri_transitive … (fpbs h g).
+/2 width=5 by tri_TC_transitive/ qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma cpr_lpr_ssta_fpbs: ∀h,g,G,L1,L2,T1,T2,U2,l2.
+ ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L1⦄ ⊢ ➡ L2 →
+ ⦃G, L2⦄ ⊢ T2 ▪[h, g] l2+1 → ⦃G, L2⦄ ⊢ T2 •[h, g] U2 →
+ ⦃G, L1, T1⦄ ≥[h, g] ⦃G, L2, U2⦄.
+/3 width=5 by fpbs_trans, cpr_lpr_fpbs, ssta_fpbs/ qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/unfold/lsstas_lift.ma".
+include "basic_2/computation/fpbs.ma".
+
+(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************)
+
+(* Advanced properties ******************************************************)
+
+lemma lsstas_fpbs: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T2 →
+ ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄.
+#h #g #G #L #T1 #T2 #l2 #H @(lsstas_ind_dx … H) -l2 -T2 //
+#l2 #T #T2 #HT1 #HT2 #IHT1 #l1 >commutative_plus #Hl21 #Hl1
+elim (le_inv_plus_l … Hl21) -Hl21 #Hl12 #Hl21
+lapply (lsstas_da_conf … HT1 … Hl1) -HT1
+>(plus_minus_m_m … Hl12) -Hl12
+/3 width=5 by fpb_ssta, fpbs_strap1/
+qed.
include "basic_2/notation/relations/btpredstarproper_8.ma".
include "basic_2/reduction/ysc.ma".
-include "basic_2/computation/yprs.ma".
+include "basic_2/computation/fpbs.ma".
(* "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **********************)
(* Basic forvard lemmas *****************************************************)
-lemma ygt_fwd_yprs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄ →
+lemma ygt_fwd_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄ →
⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G2 -L2 -T2
-/3 width=5 by yprs_strap1, ysc_ypr, ypr_lpr/
+/3 width=5 by fpbs_strap1, ysc_fpb, fpb_lpr/
qed-.
(* Basic properties *********************************************************)
lemma ygt_strap1: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G, L, T⦄ →
⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄.
#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2
-lapply (ygt_fwd_yprs … H1) #H0
-elim (ypr_inv_ysc … H2) -H2 [| * #HG2 #HL2 #HT2 destruct ]
+lapply (ygt_fwd_fpbs … H1) #H0
+elim (fpb_inv_ysc … H2) -H2 [| * #HG2 #HL2 #HT2 destruct ]
/2 width=5 by ygt_inj, ygt_step/
qed-.
lemma ygt_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ →
⦃G, L, T⦄ >[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄.
#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 elim H2 -G2 -L2 -T2
-/3 width=5 by ygt_step, ygt_inj, yprs_strap2/
+/3 width=5 by ygt_step, ygt_inj, fpbs_strap2/
qed-.
-lemma ygt_yprs_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G, L, T⦄ →
+lemma ygt_fpbs_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G, L, T⦄ →
⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #HT1 #HT2 @(yprs_ind … HT2) -G2 -L2 -T2
+#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #HT1 #HT2 @(fpbs_ind … HT2) -G2 -L2 -T2
/2 width=5 by ygt_strap1/
qed-.
-lemma yprs_ygt_trans: ∀h,g,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ →
+lemma fpbs_ygt_trans: ∀h,g,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ →
∀G2,L2,T2. ⦃G, L, T⦄ >[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G #L1 #L #T1 #T #HT1 @(yprs_ind … HT1) -G -L -T
+#h #g #G1 #G #L1 #L #T1 #T #HT1 @(fpbs_ind … HT1) -G -L -T
/3 width=5 by ygt_strap2/
qed-.
lemma fsupp_ygt: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄.
#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsupp_ind … L2 T2 H) -G2 -L2 -T2
-/3 width=5 by fsupp_yprs, ysc_fsup, ysc_ygt, ygt_inj/
+/3 width=5 by fsupp_fpbs, ysc_fsup, ysc_ygt, ygt_inj/
qed.
lemma cprs_ygt: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) →
elim (term_eq_dec T1 T) #H destruct
[ -IHT1 /4 width=1/
| lapply (IHT1 … H) -IHT1 -H -HT12 #HT1
- @(ygt_strap1 … HT1) -HT1 /2 width=1 by ypr_cpr/
+ @(ygt_strap1 … HT1) -HT1 /2 width=1 by fpb_cpr/
]
]
qed.
elim (le_inv_plus_l … Hl21) -Hl21 #Hl12 #Hl21
lapply (lsstas_da_conf … HT1 … Hl1) -HT1
>(plus_minus_m_m … Hl12) -Hl12
- /4 width=5 by ypr_ssta, ygt_strap1/
+ /4 width=5 by fpb_ssta, ygt_strap1/
]
]
qed.
(* Main properties **********************************************************)
theorem ygt_trans: ∀h,g. tri_transitive … (ygt h g).
-/3 width=5 by ygt_fwd_yprs, ygt_yprs_trans/ qed-.
+/3 width=5 by ygt_fwd_fpbs, ygt_fpbs_trans/ qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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/btpredstar_8.ma".
-include "basic_2/substitution/fsupp.ma".
-include "basic_2/reduction/ypr.ma".
-include "basic_2/computation/cprs.ma".
-include "basic_2/computation/lprs.ma".
-
-(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************)
-
-definition yprs: ∀h. sd h → tri_relation genv lenv term ≝
- λh,g. tri_TC … (ypr h g).
-
-interpretation "'big tree' parallel computation (closure)"
- 'BTPRedStar h g G1 L1 T1 G2 L2 T2 = (yprs h g G1 L1 T1 G2 L2 T2).
-
-(* Basic eliminators ********************************************************)
-
-lemma yprs_ind: ∀h,g,G1,L1,T1. ∀R:relation3 genv lenv term. R G1 L1 T1 →
- (∀L,G2,G,L2,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) →
- ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2.
-/3 width=8 by tri_TC_star_ind/ qed-.
-
-lemma yprs_ind_dx: ∀h,g,G2,L2,T2. ∀R:relation3 genv lenv term. R G2 L2 T2 →
- (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) →
- ∀G1,L1,T1. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → R G1 L1 T1.
-/3 width=8 by tri_TC_star_ind_dx/ qed-.
-
-(* Basic properties *********************************************************)
-
-lemma yprs_refl: ∀h,g. tri_reflexive … (yprs h g).
-/2 width=1 by tri_inj/ qed.
-
-lemma ypr_yprs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ →
- ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
-/2 width=1 by tri_inj/ qed.
-
-lemma yprs_strap1: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ →
- ⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
-/2 width=5 by tri_step/ qed-.
-
-lemma yprs_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ →
- ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
-/2 width=5 by tri_TC_strap/ qed-.
-
-(* Note: this is a general property of bi_TC *)
-lemma fsupp_yprs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
- ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsupp_ind … L2 T2 H) -G2 -L2 -T2
-/3 width=5 by ypr_fsup, tri_step, ypr_yprs/
-qed.
-
-lemma cprs_yprs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄.
-#h #g #G #L #T1 #T2 #H @(cprs_ind … H) -T2
-/3 width=5 by ypr_cpr, yprs_strap1/
-qed.
-
-lemma lprs_yprs: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1, T⦄ ≥[h, g] ⦃G, L2, T⦄.
-#h #g #G #L1 #L2 #T #H @(lprs_ind … H) -L2
-/3 width=5 by ypr_lpr, yprs_strap1/
-qed.
-
-lemma cpr_lpr_yprs: ∀h,g,G,L1,L2,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L1⦄ ⊢ ➡ L2 →
- ⦃G, L1, T1⦄ ≥[h, g] ⦃G, L2, T2⦄.
-/4 width=5 by yprs_strap1, ypr_lpr, ypr_cpr/ qed.
-
-lemma ssta_yprs: ∀h,g,G,L,T,U,l.
- ⦃G, L⦄ ⊢ T ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T •[h, g] U →
- ⦃G, L, T⦄ ≥[h, g] ⦃G, L, U⦄.
-/3 width=2 by ypr_yprs, ypr_ssta/ qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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/unfold/lsstas_lift.ma".
-include "basic_2/computation/yprs.ma".
-
-(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************)
-
-(* Advanced properties ******************************************************)
-
-lemma lsstas_yprs: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T2 →
- ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄.
-#h #g #G #L #T1 #T2 #l2 #H @(lsstas_ind_dx … H) -l2 -T2 //
-#l2 #T #T2 #HT1 #HT2 #IHT1 #l1 >commutative_plus #Hl21 #Hl1
-elim (le_inv_plus_l … Hl21) -Hl21 #Hl12 #Hl21
-lapply (lsstas_da_conf … HT1 … Hl1) -HT1
->(plus_minus_m_m … Hl12) -Hl12
-/3 width=5 by ypr_ssta, yprs_strap1/
-qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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/yprs.ma".
-
-(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************)
-
-(* Main properties **********************************************************)
-
-theorem yprs_trans: ∀h,g. tri_transitive … (yprs h g).
-/2 width=5 by tri_TC_transitive/ qed-.
-
-(* Advanced properties ******************************************************)
-
-lemma cpr_lpr_ssta_yprs: ∀h,g,G,L1,L2,T1,T2,U2,l2.
- ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L1⦄ ⊢ ➡ L2 →
- ⦃G, L2⦄ ⊢ T2 ▪[h, g] l2+1 → ⦃G, L2⦄ ⊢ T2 •[h, g] U2 →
- ⦃G, L1, T1⦄ ≥[h, g] ⦃G, L2, U2⦄.
-/3 width=5 by yprs_trans, cpr_lpr_yprs, ssta_yprs/ qed.
(**************************************************************************)
include "basic_2/unfold/lsstas_lsstas.ma".
-include "basic_2/computation/yprs_lift.ma".
+include "basic_2/computation/fpbs_lift.ma".
include "basic_2/computation/ygt.ma".
include "basic_2/equivalence/cpes_cpds.ma".
include "basic_2/dynamic/snv.ma".
∀G,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g].
#h #g #G0 #L0 #T0 #IH #G #L1 #T1 #HLT0 #HT1 #T2 #H
-@(cprs_ind … H) -T2 /4 width=6 by ygt_yprs_trans, cprs_yprs/
+@(cprs_ind … H) -T2 /4 width=6 by ygt_fpbs_trans, cprs_fpbs/
qed-.
fact da_cprs_lpr_aux: ∀h,g,G0,L0,T0.
∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l →
∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, g] l.
#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #HLT0 #HT1 #l #Hl #T2 #H
-@(cprs_ind … H) -T2 /4 width=10 by snv_cprs_lpr_aux, ygt_yprs_trans, cprs_yprs/
+@(cprs_ind … H) -T2 /4 width=10 by snv_cprs_lpr_aux, ygt_fpbs_trans, cprs_fpbs/
qed-.
fact da_cpcs_aux: ∀h,g,G0,L0,T0.
elim (IH1 … Hl21 … HTU … HTT2 … HL12) -IH1 -HTU -HTT2
[2: /3 width=12 by da_cprs_lpr_aux/
|3: /3 width=10 by snv_cprs_lpr_aux/
-|4: /3 width=5 by ygt_yprs_trans, cprs_yprs/
+|4: /3 width=5 by ygt_fpbs_trans, cprs_fpbs/
] -G0 -L0 -T0 -T1 -T -l1 #U2 #HTU2 #HU2
/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/
qed-.
| lapply (lsstas_da_conf … HT1T … Hl1) #Hl1l
lapply (lsstas_conf_le … HT1T … HTU1) -HTU1 // #HTU1
elim (lsstas_cprs_lpr_aux … IH3 IH2 IH1 … Hl1l … HTU1 … HTT2 L)
- /3 width=8 by ygt_yprs_trans, lsstas_yprs, monotonic_le_minus_l/ -T #U2 #HTU2 #HU12
+ /3 width=8 by ygt_fpbs_trans, lsstas_fpbs, monotonic_le_minus_l/ -T #U2 #HTU2 #HU12
/3 width=5 by cpcs_cpes, ex3_2_intro/
]
qed-.
elim (snv_fwd_da … HW) #l1 #Hl1
lapply (IH3 … HV1 … 1 … Hl0 W1 ?) /2 width=2 by fsupp_ygt, ssta_lsstas/ #HW1
lapply (da_cpcs_aux … IH2 IH1 … Hl1 … H … HWW1) -H
- /3 width=5 by ygt_yprs_trans, fsupp_ygt, ssta_yprs/ #H destruct
+ /3 width=5 by ygt_fpbs_trans, fsupp_ygt, ssta_fpbs/ #H destruct
lapply (IH1 … HV1 … Hl0 … HV12 … HL12) -HV1 -Hl0 -HV12 [ /2 by fsupp_ygt/ ] #Hl0
lapply (IH1 … Hl1 … HW2 … HL12) -Hl1 // /2 width=1 by fsupp_ygt/ -HW
lapply (IH1 … HU1 … Hl … HU12 (L2.ⓛW2) ?) -IH1 -HU1 -Hl -HU12 [1,2: /2 by fsupp_ygt, lpr_pair/ ] -HL12 -HW2
(* *)
(**************************************************************************)
-include "basic_2/computation/yprs_yprs.ma".
+include "basic_2/computation/fpbs_fpbs.ma".
include "basic_2/dynamic/snv_lift.ma".
include "basic_2/dynamic/snv_cpcs.ma".
include "basic_2/dynamic/lsubsv_snv.ma".
lapply (ssta_da_conf … HVW1 … Hl0) <minus_plus_m_m #HlW10
elim (snv_fwd_da … HW20) #l #Hl
lapply (da_cpcs_aux … IH1 IH2 … HlW10 … Hl … HW120) // -HlW10
- /3 width=5 by ygt_yprs_trans, fsupp_ygt, ssta_yprs/ #H destruct
+ /3 width=5 by ygt_fpbs_trans, fsupp_ygt, ssta_fpbs/ #H destruct
lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fsupp_ygt/ #HlV2
lapply (IH2 … Hl … HW202 … HL12) /2 width=1 by fsupp_ygt/ #HlW2
elim (ssta_cpr_lpr_aux … IH3 … Hl0 … HVW1 … HV12 … HL12) /2 width=1 by fsupp_ygt/ #W3 #HV2W3 #HW103
lapply (IH1 … HW202 … HL12) /2 width=1 by fsupp_ygt/ -HW20 #HW2
lapply (IH1 … HT20 … HT202 … (L2.ⓛW2) ?) /2 width=1 by fsupp_ygt, lpr_pair/ -HT20 #HT2
lapply (snv_ssta_aux … IH4 … HlV2 … HV2W3)
- /3 width=5 by ygt_yprs_trans, fsupp_ygt, cpr_lpr_yprs/ #HW3
+ /3 width=5 by ygt_fpbs_trans, fsupp_ygt, cpr_lpr_fpbs/ #HW3
lapply (lsubsv_snv_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /3 width=3 by snv_bind, snv_cast/
@(lsubsv_abbr … l) /3 width=7 by fsupp_ygt/ #W #W0 #l0 #Hl0 #HV2W #HW20
lapply (lsstas_ssta_conf_pos … HV2W3 … HV2W) -HV2W #HW3W
@(lsstas_cpcs_lpr_aux … IH1 IH2 IH3 … HlW3 … HW3W … HlW2 … HW20 … HW32) //
- [ /3 width=9 by ygt_yprs_trans, fsupp_ygt, cpr_lpr_ssta_yprs/
- | /3 width=5 by ygt_yprs_trans, fsupp_ygt, cpr_lpr_yprs/
+ [ /3 width=9 by ygt_fpbs_trans, fsupp_ygt, cpr_lpr_ssta_fpbs/
+ | /3 width=5 by ygt_fpbs_trans, fsupp_ygt, cpr_lpr_fpbs/
]
| #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HV02 #HW02 #HT02 #H1 #H2 destruct -IH4
elim (snv_inv_bind … HT1) -HT1 #HW0 #HT0
(**************************************************************************)
include "basic_2/computation/cpds_cpds.ma".
-include "basic_2/computation/yprs_yprs.ma".
+include "basic_2/computation/fpbs_fpbs.ma".
include "basic_2/dynamic/snv_aaa.ma".
include "basic_2/dynamic/snv_cpcs.ma".
include "basic_2/dynamic/lsubsv_lsstas.ma".
elim (snv_fwd_da … HW2) #l #Hl
lapply (IH4 … HV1 … 1 … Hl0 W1 ?) /2 width=1 by fsupp_ygt, ssta_lsstas/ #HW1
lapply (da_cpcs_aux … IH3 IH2 … H … Hl … HW12) // -H
- /3 width=5 by ygt_yprs_trans, fsupp_ygt, ssta_yprs/ #H destruct
+ /3 width=5 by ygt_fpbs_trans, fsupp_ygt, ssta_fpbs/ #H destruct
lapply (IH3 … HV12 … HL12) /2 width=1 by fsupp_ygt/ #HV2
lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fsupp_ygt/ #HV2l
elim (IH1 … 1 … Hl0 … W1 … HV12 … HL12) /2 width=1 by fsupp_ygt, ssta_lsstas/ -HVW1 #W4 #H #HW14
lapply (lsstas_inv_SO … H) #HV2W4
lapply (ssta_da_conf … HV2W4 … HV2l) <minus_plus_m_m #HW4l
- lapply (IH4 … HV2 … HV2l … H) -H /3 width=5 by ygt_yprs_trans, fsupp_ygt, cpr_lpr_yprs/ #HW4
+ lapply (IH4 … HV2 … HV2l … H) -H /3 width=5 by ygt_fpbs_trans, fsupp_ygt, cpr_lpr_fpbs/ #HW4
lapply (IH3 … HW23 … HL12) /2 width=1 by fsupp_ygt/ #HW3
lapply (IH2 … Hl … HW23 … HL12) /2 width=1 by fsupp_ygt/ #HW3l
elim (IH1 … Hl1 … HTU2 … HT23 (L2.ⓛW3)) -HTU2 /2 width=1 by fsupp_ygt, lpr_pair/ #U3 #HTU3 #HU23
#W #W0 #l0 #Hl0 #HV2W #HW30
lapply (lsstas_ssta_conf_pos … HV2W4 … HV2W) -HV2W #HW4W
@(lsstas_cpcs_lpr_aux … IH3 IH2 IH1 … Hl0 … HW4W … Hl0 … HW30 … HW43) //
- [ /3 width=9 by ygt_yprs_trans, fsupp_ygt, cpr_lpr_ssta_yprs/
- | /3 width=5 by ygt_yprs_trans, fsupp_ygt, cpr_lpr_yprs/
+ [ /3 width=9 by ygt_fpbs_trans, fsupp_ygt, cpr_lpr_ssta_fpbs/
+ | /3 width=5 by ygt_fpbs_trans, fsupp_ygt, cpr_lpr_fpbs/
]
| -IH1 -IH3 -IH4 /3 width=9 by fsupp_ygt, lpr_pair/
]
- third letter
+b: "big tree" reduction
c: conversion
d: decomposed extended reduction
e: decomposed extended conversion
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/btpred_8.ma".
+include "basic_2/relocation/fsup.ma".
+include "basic_2/static/ssta.ma".
+include "basic_2/reduction/lpr.ma".
+
+(* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************)
+
+inductive fpb (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝
+| fpb_fsup : ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → fpb h g G1 L1 T1 G2 L2 T2
+| fpb_lpr : ∀L2. ⦃G1, L1⦄ ⊢ ➡ L2 → fpb h g G1 L1 T1 G1 L2 T1
+| fpb_cpr : ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡ T2 → fpb h g G1 L1 T1 G1 L1 T2
+| fpb_ssta : ∀T2,l. ⦃G1, L1⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G1, L1⦄ ⊢ T1 •[h, g] T2 → fpb h g G1 L1 T1 G1 L1 T2
+.
+
+interpretation
+ "'big tree' parallel reduction (closure)"
+ 'BTPRed h g G1 L1 T1 G2 L2 T2 = (fpb h g G1 L1 T1 G2 L2 T2).
+
+(* Basic properties *********************************************************)
+
+lemma fpb_refl: ∀h,g. tri_reflexive … (fpb h g).
+/2 width=1 by fpb_cpr/ qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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/btpred_8.ma".
-include "basic_2/relocation/fsup.ma".
-include "basic_2/static/ssta.ma".
-include "basic_2/reduction/lpr.ma".
-
-(* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************)
-
-inductive ypr (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝
-| ypr_fsup : ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ypr h g G1 L1 T1 G2 L2 T2
-| ypr_lpr : ∀L2. ⦃G1, L1⦄ ⊢ ➡ L2 → ypr h g G1 L1 T1 G1 L2 T1
-| ypr_cpr : ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡ T2 → ypr h g G1 L1 T1 G1 L1 T2
-| ypr_ssta : ∀T2,l. ⦃G1, L1⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G1, L1⦄ ⊢ T1 •[h, g] T2 → ypr h g G1 L1 T1 G1 L1 T2
-.
-
-interpretation
- "'big tree' parallel reduction (closure)"
- 'BTPRed h g G1 L1 T1 G2 L2 T2 = (ypr h g G1 L1 T1 G2 L2 T2).
-
-(* Basic properties *********************************************************)
-
-lemma ypr_refl: ∀h,g. tri_reflexive … (ypr h g).
-/2 width=1 by ypr_cpr/ qed.
(**************************************************************************)
include "basic_2/notation/relations/btpredproper_8.ma".
-include "basic_2/reduction/ypr.ma".
+include "basic_2/reduction/fpb.ma".
(* "BIG TREE" PROPER PARALLEL REDUCTION FOR CLOSURES ************************)
(* Basic properties *********************************************************)
-lemma ysc_ypr: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ →
+lemma ysc_fpb: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ →
⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄.
#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2
-/2 width=2 by ypr_fsup, ypr_cpr, ypr_ssta/
+/2 width=2 by fpb_fsup, fpb_cpr, fpb_ssta/
qed.
(* Inversion lemmas on "big tree" parallel reduction for closures ***********)
-lemma ypr_inv_ysc: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ →
+lemma fpb_inv_ysc: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ →
⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ ∨
∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡ L2 & T1 = T2.
#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2
]
[ { "\"big tree\" parallel computation" * } {
[ "ygt ( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "ygt_lift" + "ygt_ygt" * ]
- [ "yprs ( ? ⊢ ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "yprs_lift" + "yprs_yprs" * ]
+ [ "fpbs ( ? ⊢ ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fpbs" * ]
}
]
[ { "decomposed extended computation" * } {
class "water"
[ { "reduction" * } {
[ { "\"big tree\" parallel reduction" * } {
- [ "ypr ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "ysc ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" * ]
+ [ "fpb ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "ysc ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" * ]
}
]
[ { "context-sensitive extended normal forms" * } {
projects / helm.git / commitdiff