- fpbg can be reflexive (example given)

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / fpbg.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma
index 5d7ce1cb342f0b56d17fe9f783c248ef4fce6c10..574c35e106c1cb87b101ab0f7df3c9be3f6e93f7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma
@@ -13,14 +13,14 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/lazybtpredstarproper_8.ma".
-include "basic_2/computation/fpbc.ma".
+include "basic_2/reduction/fpbc.ma".
 
-(* GENEARAL "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES *************)
+(* "QRST" PROPER PARALLEL COMPUTATION FOR CLOSURES **************************)
 
 definition fpbg: ∀h. sd h → tri_relation genv lenv term ≝
                  λh,g. tri_TC … (fpbc h g).
 
-interpretation "general 'big tree' proper parallel computation (closure)"
+interpretation "'qrst' proper parallel computation (closure)"
    'LazyBTPRedStarProper h g G1 L1 T1 G2 L2 T2 = (fpbg h g G1 L1 T1 G2 L2 T2).
 
 (* Basic properties *********************************************************)
@@ -39,9 +39,8 @@ lemma fpbg_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2.
                    ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄.
 /2 width=5 by tri_TC_strap/ qed.
 
-(* Note: this is used in the closure proof *)
-lemma fqup_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄.
-/4 width=1 by fpbc_fpbg, fpbu_fpbc, fpbu_fqup/ qed.
+lemma fpbu_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h,g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄.
+/3 width=1 by fpbu_fpbc, fpbc_fpbg/ qed.
 
 (* Basic eliminators ********************************************************)