X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Ffpbg_fqup.ma;h=7acceab10134ebc9ccb84d48159e62d9254fa6f8;hb=b118146b97959e6a6dde18fdd014b8e1e676a2d1;hp=ce02c890aa3a096ad3b30a74ce42bb50d3ad4ff8;hpb=9aa2722ff4aa7868ffd14e5a820cd6dc79e2c8a6;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma index ce02c890a..7acceab10 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma @@ -17,16 +17,18 @@ include "basic_2/rt_computation/fpbg.ma". (* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************) -(* Advanced properties with degree-based equivalence for terms **************) +(* Advanced properties with sort-irrelevant equivalence for terms ***********) -lemma fpbg_tdeq_div: ∀h,o,G1,G2,L1,L2,T1,T. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T⦄ → - ∀T2. T2 ≛[h, o] T → ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄. -/4 width=5 by fpbg_fdeq_trans, tdeq_fdeq, tdeq_sym/ qed-. +lemma fpbg_teqx_div: + ∀G1,G2,L1,L2,T1,T. ❪G1,L1,T1❫ > ❪G2,L2,T❫ → + ∀T2. T2 ≅ T → ❪G1,L1,T1❫ > ❪G2,L2,T2❫. +/4 width=5 by fpbg_feqx_trans, teqg_feqg, teqx_sym/ qed-. (* Properties with plus-iterated structural successor for closures **********) (* Note: this is used in the closure proof *) -lemma fqup_fpbg: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fqup_inv_step_sn … H) -H +lemma fqup_fpbg: + ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂+ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫. +#G1 #G2 #L1 #L2 #T1 #T2 #H elim (fqup_inv_step_sn … H) -H /3 width=5 by fqus_fpbs, fpb_fqu, ex2_3_intro/ qed.