X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Ffpbg.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Ffpbg.ma;h=c1e2b94c1cbca338c80ecd6d8c171b05faa39e26;hb=e9f96fa56226dfd74de214c89d827de0c5018ac7;hp=0000000000000000000000000000000000000000;hpb=ad3ca38634cfae29e8c26d0ab23cb466407eca5e;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma new file mode 100644 index 000000000..c1e2b94c1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma @@ -0,0 +1,39 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lazybtpredstarproper_8.ma". +include "basic_2/reduction/fpb.ma". +include "basic_2/computation/fpbs.ma". + +(* "QRST" PROPER PARALLEL COMPUTATION FOR CLOSURES **************************) + +definition fpbg: ∀h. sd h → tri_relation genv lenv term ≝ + λh,o,G1,L1,T1,G2,L2,T2. + ∃∃G,L,T. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G, L, T⦄ & ⦃G, L, T⦄ ≥[h, o] ⦃G2, L2, T2⦄. + +interpretation "'qrst' proper parallel computation (closure)" + 'LazyBTPRedStarProper h o G1 L1 T1 G2 L2 T2 = (fpbg h o G1 L1 T1 G2 L2 T2). + +(* Basic properties *********************************************************) + +lemma fpb_fpbg: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ >≡[h, o] ⦃G2, L2, T2⦄. +/2 width=5 by ex2_3_intro/ qed. + +lemma fpbg_fpbq_trans: ∀h,o,G1,G,G2,L1,L,L2,T1,T,T2. + ⦃G1, L1, T1⦄ >≡[h, o] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≽[h, o] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ >≡[h, o] ⦃G2, L2, T2⦄. +#h #o #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 * +/3 width=9 by fpbs_strap1, ex2_3_intro/ +qed-.