- fpbg can be reflexive (example given)

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma
index 1f52880ad8cd8e447a3a14e8d6a721e343bad486..57dd5ebb43b55effdbbd6801b59fbaeffc0b1b4a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma
@@ -12,10 +12,12 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/computation/fpbc_fpbs.ma".
-include "basic_2/computation/fpbg_fleq.ma".
+include "basic_2/computation/fpbs_fpbu.ma".
+include "basic_2/computation/fpbs_fpbc.ma".
+include "basic_2/computation/fpbs_fpbs.ma".
+include "basic_2/computation/fpbg_fpbs.ma".
 
-(* GENERAL "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **************)
+(* "QRST" PROPER PARALLEL COMPUTATION FOR CLOSURES **************************)
 
 (* Advanced inversion lemmas ************************************************)
 
@@ -25,7 +27,7 @@ lemma fpbg_inv_fpbu_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ >≡[h, g] 
 [ #G1 #L1 #T1 * /3 width=5 by fleq_fpbs, ex2_3_intro/
 | #G1 #G #L1 #L #T1 #T *
   #G0 #L0 #T0 #H10 #H0 #_ *
-  /5 width=9 by fpbu_fwd_fpbs, fpbs_trans, fleq_fpbs, ex2_3_intro/
+  /5 width=9 by fpbu_fpbs, fpbs_trans, fleq_fpbs, ex2_3_intro/
 ]
 qed-.
 
@@ -35,7 +37,7 @@ lemma fpbg_fwd_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2
                      ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
 #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbg_ind … H) -G2 -L2 -T2
 [2: #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 @(fpbs_trans … IH1) -IH1 ] (**) (* full auto fails *)
-/2 width=1 by fpbc_fwd_fpbs/
+/2 width=1 by fpbc_fpbs/
 qed-.
 
 (* Advanced properties ******************************************************)