(* *)
(**************************************************************************)
-include "basic_2/computation/fpbs.ma".
+include "basic_2/rt_computation/fpbs.ma".
-(* "QRST" PARALLEL COMPUTATION FOR CLOSURES *********************************)
+(* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************)
(* Main properties **********************************************************)
-theorem fpbs_trans: ∀h,o. tri_transitive … (fpbs h o).
+theorem fpbs_trans:
+ tri_transitive … fpbs.
/2 width=5 by tri_TC_transitive/ qed-.