X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Ffpbs.ma;h=64277054e8743037228017ba317762f90ea05864;hp=19584074fcd97867efbbc21355f73ca1af241dc0;hb=bd53c4e895203eb049e75434f638f26b5a161a2b;hpb=3b7b8afcb429a60d716d5226a5b6ab0d003228b1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma index 19584074f..64277054e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma @@ -27,13 +27,13 @@ interpretation "parallel rst-computation (closure)" (* Basic eliminators ********************************************************) lemma fpbs_ind: ∀h,G1,L1,T1. ∀Q:relation3 genv lenv term. Q G1 L1 T1 → - (∀G,G2,L,L2,T,T2. ⦃G1,L1,T1⦄ ≥[h] ⦃G,L,T⦄ → ⦃G,L,T⦄ ≽[h] ⦃G2,L2,T2⦄ → Q G L T → Q G2 L2 T2) → - ∀G2,L2,T2. ⦃G1,L1,T1⦄ ≥[h] ⦃G2,L2,T2⦄ → Q G2 L2 T2. + (∀G,G2,L,L2,T,T2. ❪G1,L1,T1❫ ≥[h] ❪G,L,T❫ → ❪G,L,T❫ ≽[h] ❪G2,L2,T2❫ → Q G L T → Q G2 L2 T2) → + ∀G2,L2,T2. ❪G1,L1,T1❫ ≥[h] ❪G2,L2,T2❫ → Q G2 L2 T2. /3 width=8 by tri_TC_star_ind/ qed-. lemma fpbs_ind_dx: ∀h,G2,L2,T2. ∀Q:relation3 genv lenv term. Q G2 L2 T2 → - (∀G1,G,L1,L,T1,T. ⦃G1,L1,T1⦄ ≽[h] ⦃G,L,T⦄ → ⦃G,L,T⦄ ≥[h] ⦃G2,L2,T2⦄ → Q G L T → Q G1 L1 T1) → - ∀G1,L1,T1. ⦃G1,L1,T1⦄ ≥[h] ⦃G2,L2,T2⦄ → Q G1 L1 T1. + (∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ≽[h] ❪G,L,T❫ → ❪G,L,T❫ ≥[h] ❪G2,L2,T2❫ → Q G L T → Q G1 L1 T1) → + ∀G1,L1,T1. ❪G1,L1,T1❫ ≥[h] ❪G2,L2,T2❫ → Q G1 L1 T1. /3 width=8 by tri_TC_star_ind_dx/ qed-. (* Basic properties *********************************************************) @@ -41,34 +41,34 @@ lemma fpbs_ind_dx: ∀h,G2,L2,T2. ∀Q:relation3 genv lenv term. Q G2 L2 T2 → lemma fpbs_refl: ∀h. tri_reflexive … (fpbs h). /2 width=1 by tri_inj/ qed. -lemma fpbq_fpbs: ∀h,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ≽[h] ⦃G2,L2,T2⦄ → - ⦃G1,L1,T1⦄ ≥[h] ⦃G2,L2,T2⦄. +lemma fpbq_fpbs: ∀h,G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≽[h] ❪G2,L2,T2❫ → + ❪G1,L1,T1❫ ≥[h] ❪G2,L2,T2❫. /2 width=1 by tri_inj/ qed. -lemma fpbs_strap1: ∀h,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1,L1,T1⦄ ≥[h] ⦃G,L,T⦄ → - ⦃G,L,T⦄ ≽[h] ⦃G2,L2,T2⦄ → ⦃G1,L1,T1⦄ ≥[h] ⦃G2,L2,T2⦄. +lemma fpbs_strap1: ∀h,G1,G,G2,L1,L,L2,T1,T,T2. ❪G1,L1,T1❫ ≥[h] ❪G,L,T❫ → + ❪G,L,T❫ ≽[h] ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥[h] ❪G2,L2,T2❫. /2 width=5 by tri_step/ qed-. -lemma fpbs_strap2: ∀h,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1,L1,T1⦄ ≽[h] ⦃G,L,T⦄ → - ⦃G,L,T⦄ ≥[h] ⦃G2,L2,T2⦄ → ⦃G1,L1,T1⦄ ≥[h] ⦃G2,L2,T2⦄. +lemma fpbs_strap2: ∀h,G1,G,G2,L1,L,L2,T1,T,T2. ❪G1,L1,T1❫ ≽[h] ❪G,L,T❫ → + ❪G,L,T❫ ≥[h] ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥[h] ❪G2,L2,T2❫. /2 width=5 by tri_TC_strap/ qed-. (* Basic_2A1: uses: lleq_fpbs fleq_fpbs *) -lemma feqx_fpbs: ∀h,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ≛ ⦃G2,L2,T2⦄ → ⦃G1,L1,T1⦄ ≥[h] ⦃G2,L2,T2⦄. +lemma feqx_fpbs: ∀h,G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥[h] ❪G2,L2,T2❫. /3 width=1 by fpbq_fpbs, fpbq_feqx/ qed. (* Basic_2A1: uses: fpbs_lleq_trans *) -lemma fpbs_feqx_trans: ∀h,G1,G,L1,L,T1,T. ⦃G1,L1,T1⦄ ≥[h] ⦃G,L,T⦄ → - ∀G2,L2,T2. ⦃G,L,T⦄ ≛ ⦃G2,L2,T2⦄ → ⦃G1,L1,T1⦄ ≥[h] ⦃G2,L2,T2⦄. +lemma fpbs_feqx_trans: ∀h,G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ≥[h] ❪G,L,T❫ → + ∀G2,L2,T2. ❪G,L,T❫ ≛ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥[h] ❪G2,L2,T2❫. /3 width=9 by fpbs_strap1, fpbq_feqx/ qed-. (* Basic_2A1: uses: lleq_fpbs_trans *) -lemma feqx_fpbs_trans: ∀h,G,G2,L,L2,T,T2. ⦃G,L,T⦄ ≥[h] ⦃G2,L2,T2⦄ → - ∀G1,L1,T1. ⦃G1,L1,T1⦄ ≛ ⦃G,L,T⦄ → ⦃G1,L1,T1⦄ ≥[h] ⦃G2,L2,T2⦄. +lemma feqx_fpbs_trans: ∀h,G,G2,L,L2,T,T2. ❪G,L,T❫ ≥[h] ❪G2,L2,T2❫ → + ∀G1,L1,T1. ❪G1,L1,T1❫ ≛ ❪G,L,T❫ → ❪G1,L1,T1❫ ≥[h] ❪G2,L2,T2❫. /3 width=5 by fpbs_strap2, fpbq_feqx/ qed-. lemma teqx_reqx_lpx_fpbs: ∀h,T1,T2. T1 ≛ T2 → ∀L1,L0. L1 ≛[T2] L0 → - ∀G,L2. ⦃G,L0⦄ ⊢ ⬈[h] L2 → ⦃G,L1,T1⦄ ≥[h] ⦃G,L2,T2⦄. + ∀G,L2. ❪G,L0❫ ⊢ ⬈[h] L2 → ❪G,L1,T1❫ ≥[h] ❪G,L2,T2❫. /4 width=5 by feqx_fpbs, fpbs_strap1, fpbq_lpx, feqx_intro_dx/ qed. (* Basic_2A1: removed theorems 3: