X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fsubstitution%2Fltps_ldrop.ma;h=bf4e1f7117d82104fe9e47bbe9911a0916f2ce4f;hb=ef3bdc4be26f6518a82a79c64e986253f7aeaa3c;hp=f777d1cd77c1111797a04a7e4db84915e725d19f;hpb=9aa9a54946719d3fdb4cadb7c7d33fd13956c083;p=helm.git diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_ldrop.ma index f777d1cd7..bf4e1f711 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_ldrop.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_ldrop.ma @@ -16,9 +16,9 @@ include "Basic_2/substitution/ltps.ma". (* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************) -lemma ltps_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 → - ∀L2,e2. ↓[0, e2] L0 ≡ L2 → - d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2. +lemma ltps_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ▶ L1 → + ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → + d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2. #L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H // | // @@ -33,9 +33,9 @@ lemma ltps_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 → ] qed. -lemma ltps_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 → - ∀L2,e2. ↓[0, e2] L0 ≡ L2 → - d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2. +lemma ltps_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ▶ L0 → + ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → + d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2. #L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H // | // @@ -50,9 +50,9 @@ lemma ltps_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 → ] qed. -lemma ltps_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 → - ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 → - ∃∃L. L2 [0, d1 + e1 - e2] ≫ L & ↓[0, e2] L1 ≡ L. +lemma ltps_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ▶ L1 → + ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 → + ∃∃L. L2 [0, d1 + e1 - e2] ▶ L & ⇩[0, e2] L1 ≡ L. #L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/ | normalize #L #I #V #L2 #e2 #HL2 #_ #He2 @@ -72,9 +72,9 @@ lemma ltps_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 → ] qed. -lemma ltps_ldrop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 → - ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 → - ∃∃L. L [0, d1 + e1 - e2] ≫ L2 & ↓[0, e2] L1 ≡ L. +lemma ltps_ldrop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ▶ L0 → + ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 → + ∃∃L. L [0, d1 + e1 - e2] ▶ L2 & ⇩[0, e2] L1 ≡ L. #L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/ | normalize #L #I #V #L2 #e2 #HL2 #_ #He2 @@ -94,9 +94,9 @@ lemma ltps_ldrop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 → ] qed. -lemma ltps_ldrop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 → - ∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 → - ∃∃L. L2 [d1 - e2, e1] ≫ L & ↓[0, e2] L1 ≡ L. +lemma ltps_ldrop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ▶ L1 → + ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 → + ∃∃L. L2 [d1 - e2, e1] ▶ L & ⇩[0, e2] L1 ≡ L. #L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/ | /2 width=3/ @@ -112,9 +112,9 @@ lemma ltps_ldrop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 → ] qed. -lemma ltps_ldrop_trans_le: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 → - ∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 → - ∃∃L. L [d1 - e2, e1] ≫ L2 & ↓[0, e2] L1 ≡ L. +lemma ltps_ldrop_trans_le: ∀L1,L0,d1,e1. L1 [d1, e1] ▶ L0 → + ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 → + ∃∃L. L [d1 - e2, e1] ▶ L2 & ⇩[0, e2] L1 ≡ L. #L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/ | /2 width=3/