From f5cd5870668ed096f6d93b005e2acd3bd555f3b0 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 5 Oct 2013 18:16:21 +0000
Subject: [PATCH] final na,e for big-tree rediction and computation

---
 .../basic_2/computation/{yprs.ma => fpbs.ma}  | 40 +++++++++----------
 .../{yprs_yprs.ma => fpbs_fpbs.ma}            |  8 ++--
 .../{yprs_lift.ma => fpbs_lift.ma}            |  6 +--
 .../lambdadelta/basic_2/computation/ygt.ma    | 24 +++++------
 .../basic_2/computation/ygt_lift.ma           |  2 +-
 .../basic_2/computation/ygt_ygt.ma            |  2 +-
 .../lambdadelta/basic_2/dynamic/snv_cpcs.ma   | 10 ++---
 .../lambdadelta/basic_2/dynamic/snv_da_lpr.ma |  2 +-
 .../lambdadelta/basic_2/dynamic/snv_lpr.ma    | 10 ++---
 .../basic_2/dynamic/snv_lsstas_lpr.ma         | 10 ++---
 .../contribs/lambdadelta/basic_2/names.txt    |  1 +
 .../basic_2/reduction/{ypr.ma => fpb.ma}      | 16 ++++----
 .../lambdadelta/basic_2/reduction/ysc.ma      |  8 ++--
 .../lambdadelta/basic_2/web/basic_2_src.tbl   |  4 +-
 14 files changed, 72 insertions(+), 71 deletions(-)
 rename matita/matita/contribs/lambdadelta/basic_2/computation/{yprs.ma => fpbs.ma} (74%)
 rename matita/matita/contribs/lambdadelta/basic_2/computation/{yprs_yprs.ma => fpbs_fpbs.ma} (88%)
 rename matita/matita/contribs/lambdadelta/basic_2/computation/{yprs_lift.ma => fpbs_lift.ma} (91%)
 rename matita/matita/contribs/lambdadelta/basic_2/reduction/{ypr.ma => fpb.ma} (71%)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/yprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma
similarity index 74%
rename from matita/matita/contribs/lambdadelta/basic_2/computation/yprs.ma
rename to matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma
index d3260bc65..361642dd1 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/yprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma
@@ -14,69 +14,69 @@
 
 include "basic_2/notation/relations/btpredstar_8.ma".
 include "basic_2/substitution/fsupp.ma".
-include "basic_2/reduction/ypr.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 yprs: ∀h. sd h → tri_relation genv lenv term ≝
-                 λh,g. tri_TC … (ypr h g).
+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 = (yprs h g G1 L1 T1 G2 L2 T2).
+   'BTPRedStar h g G1 L1 T1 G2 L2 T2 = (fpbs 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 →
+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 yprs_ind_dx: ∀h,g,G2,L2,T2. ∀R:relation3 genv lenv term. R G2 L2 T2 →
+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 yprs_refl: ∀h,g. tri_reflexive … (yprs h g).
+lemma fpbs_refl: ∀h,g. tri_reflexive … (fpbs 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⦄ →
+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 yprs_strap1: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ →
+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 yprs_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ →
+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_yprs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
+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 ypr_fsup, tri_step, ypr_yprs/
+/3 width=5 by fpb_fsup, tri_step, fpb_fpbs/
 qed.
 
-lemma cprs_yprs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄.
+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 ypr_cpr, yprs_strap1/
+/3 width=5 by fpb_cpr, fpbs_strap1/
 qed.
 
-lemma lprs_yprs: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1, T⦄ ≥[h, g] ⦃G, L2, T⦄.
+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 ypr_lpr, yprs_strap1/
+/3 width=5 by fpb_lpr, fpbs_strap1/
 qed.
 
-lemma cpr_lpr_yprs: ∀h,g,G,L1,L2,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L1⦄ ⊢ ➡ L2 →
+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 yprs_strap1, ypr_lpr, ypr_cpr/ qed.
+/4 width=5 by fpbs_strap1, fpb_lpr, fpb_cpr/ qed.
 
-lemma ssta_yprs: ∀h,g,G,L,T,U,l.
+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 ypr_yprs, ypr_ssta/ qed.
+/3 width=2 by fpb_fpbs, fpb_ssta/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/yprs_yprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma
similarity index 88%
rename from matita/matita/contribs/lambdadelta/basic_2/computation/yprs_yprs.ma
rename to matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma
index f28153053..1978f2ce6 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/yprs_yprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma
@@ -12,19 +12,19 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/computation/yprs.ma".
+include "basic_2/computation/fpbs.ma".
 
 (* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************)
 
 (* Main properties **********************************************************)
 
-theorem yprs_trans: ∀h,g. tri_transitive … (yprs h g).
+theorem fpbs_trans: ∀h,g. tri_transitive … (fpbs 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.
+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 yprs_trans, cpr_lpr_yprs, ssta_yprs/ qed.
+/3 width=5 by fpbs_trans, cpr_lpr_fpbs, ssta_fpbs/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/yprs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma
similarity index 91%
rename from matita/matita/contribs/lambdadelta/basic_2/computation/yprs_lift.ma
rename to matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma
index 2743f9c68..809bd3358 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/yprs_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma
@@ -13,18 +13,18 @@
 (**************************************************************************)
 
 include "basic_2/unfold/lsstas_lift.ma".
-include "basic_2/computation/yprs.ma".
+include "basic_2/computation/fpbs.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 →
+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 ypr_ssta, yprs_strap1/
+/3 width=5 by fpb_ssta, fpbs_strap1/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/ygt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/ygt.ma
index 03678e4a8..f6b0f6a5f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/ygt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/ygt.ma
@@ -14,7 +14,7 @@
 
 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 **********************)
 
@@ -29,10 +29,10 @@ interpretation "'big tree' proper parallel computation (closure)"
 
 (* 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 *********************************************************)
@@ -44,32 +44,32 @@ lemma ysc_ygt: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T
 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 → ⊥) →
@@ -80,7 +80,7 @@ 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.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/ygt_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/ygt_lift.ma
index 6b713bc91..1c75c8e3d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/ygt_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/ygt_lift.ma
@@ -31,7 +31,7 @@ lemma lsstas_ygt: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T2 → (
     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.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/ygt_ygt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/ygt_ygt.ma
index 5910f81ca..98fd435a3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/ygt_ygt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/ygt_ygt.ma
@@ -19,4 +19,4 @@ include "basic_2/computation/ygt.ma".
 (* 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-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma
index 28aa4a7a0..3679610d9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 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".
@@ -51,7 +51,7 @@ fact snv_cprs_lpr_aux: ∀h,g,G0,L0,T0.
                        ∀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.
@@ -61,7 +61,7 @@ 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.
@@ -103,7 +103,7 @@ elim (IHT1 L1) // -IHT1 #U #HTU #HU1
 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-.
@@ -149,7 +149,7 @@ elim (le_or_ge l2 l) #Hl2
 | 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-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma
index d706d6dc6..f65229f06 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma
@@ -73,7 +73,7 @@ fact da_cpr_lpr_aux: ∀h,g,G0,L0,T0.
     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
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma
index a69b20043..04fb88a60 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-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".
@@ -74,7 +74,7 @@ fact snv_cpr_lpr_aux: ∀h,g,G0,L0,T0.
     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
@@ -86,13 +86,13 @@ fact snv_cpr_lpr_aux: ∀h,g,G0,L0,T0.
     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
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma
index a9dd6ebd2..c5ffa5efb 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 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".
@@ -94,13 +94,13 @@ fact lsstas_cpr_lpr_aux: ∀h,g,G0,L0,T0.
     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
@@ -118,8 +118,8 @@ fact lsstas_cpr_lpr_aux: ∀h,g,G0,L0,T0.
       #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/
     ]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt
index 3e459a92d..4791fec7b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/names.txt
+++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt
@@ -67,6 +67,7 @@ s: sequential transformation
 
 - third letter
 
+b: "big tree" reduction
 c: conversion
 d: decomposed extended reduction
 e: decomposed extended conversion
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/ypr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma
similarity index 71%
rename from matita/matita/contribs/lambdadelta/basic_2/reduction/ypr.ma
rename to matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma
index 308f30095..06ff76ac9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/ypr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma
@@ -19,18 +19,18 @@ 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
+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 = (ypr h g G1 L1 T1 G2 L2 T2).
+   'BTPRed h g G1 L1 T1 G2 L2 T2 = (fpb 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.
+lemma fpb_refl: ∀h,g. tri_reflexive … (fpb h g).
+/2 width=1 by fpb_cpr/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/ysc.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/ysc.ma
index 290157d30..c6cc92643 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/ysc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/ysc.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 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 ************************)
 
@@ -29,15 +29,15 @@ interpretation
 
 (* 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
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 571d2e6de..dad2aa95a 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
@@ -86,7 +86,7 @@ table {
         ]
         [ { "\"big tree\" parallel computation" * } {
              [ "ygt ( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "ygt_lift" + "ygt_ygt" * ]
-             [ "yprs ( ? ⊢ ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "yprs_lift" + "yprs_yprs" * ]
+             [ "fpbs ( ? ⊢ ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fpbs" * ]
           }
         ]
         [ { "decomposed extended computation" * } {
@@ -116,7 +116,7 @@ table {
    class "water"
    [ { "reduction" * } {
         [ { "\"big tree\" parallel reduction" * } {
-             [ "ypr ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "ysc ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" * ]
+             [ "fpb ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "ysc ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" * ]
           }
         ]
         [ { "context-sensitive extended normal forms" * } {
-- 
2.39.2