From 13935d33cc0899b9555648a4d49586e17274c748 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 14 Jun 2011 19:00:26 +0000 Subject: [PATCH] some restructuring --- .../reduction/{pr.ma => pr_defs.ma} | 2 +- .../substitution/{lift.ma => lift_defs.ma} | 98 ---------------- .../lib/lambda-delta/substitution/lift_fun.ma | 25 ++++ .../lambda-delta/substitution/lift_main.ma | 111 ++++++++++++++++++ .../substitution/{subst.ma => subst_defs.ma} | 4 +- .../substitution/{thin.ma => thin_defs.ma} | 19 +-- .../lambda-delta/substitution/thin_main.ma | 34 ++++++ 7 files changed, 175 insertions(+), 118 deletions(-) rename matita/matita/lib/lambda-delta/reduction/{pr.ma => pr_defs.ma} (97%) rename matita/matita/lib/lambda-delta/substitution/{lift.ma => lift_defs.ma} (60%) create mode 100644 matita/matita/lib/lambda-delta/substitution/lift_fun.ma create mode 100644 matita/matita/lib/lambda-delta/substitution/lift_main.ma rename matita/matita/lib/lambda-delta/substitution/{subst.ma => subst_defs.ma} (93%) rename matita/matita/lib/lambda-delta/substitution/{thin.ma => thin_defs.ma} (64%) create mode 100644 matita/matita/lib/lambda-delta/substitution/thin_main.ma diff --git a/matita/matita/lib/lambda-delta/reduction/pr.ma b/matita/matita/lib/lambda-delta/reduction/pr_defs.ma similarity index 97% rename from matita/matita/lib/lambda-delta/reduction/pr.ma rename to matita/matita/lib/lambda-delta/reduction/pr_defs.ma index 3c5f4ca96..e1cd216c2 100644 --- a/matita/matita/lib/lambda-delta/reduction/pr.ma +++ b/matita/matita/lib/lambda-delta/reduction/pr_defs.ma @@ -9,7 +9,7 @@ \ / V_______________________________________________________________ *) -include "lambda-delta/substitution/thin.ma". +include "lambda-delta/substitution/thin_defs.ma". (* SINGLE STEP PARALLEL REDUCTION ON TERMS **********************************) diff --git a/matita/matita/lib/lambda-delta/substitution/lift.ma b/matita/matita/lib/lambda-delta/substitution/lift_defs.ma similarity index 60% rename from matita/matita/lib/lambda-delta/substitution/lift.ma rename to matita/matita/lib/lambda-delta/substitution/lift_defs.ma index 60b1b62e7..86e1b7511 100644 --- a/matita/matita/lib/lambda-delta/substitution/lift.ma +++ b/matita/matita/lib/lambda-delta/substitution/lift_defs.ma @@ -166,101 +166,3 @@ lemma lift_inv_flat2: ∀d,e,T1,I,V2,U2. ↑[d,e] T1 ≡ 𝕗{I} V2. U2 → T1 = 𝕗{I} V1. U1. #d #e #T1 #I #V2 #U2 #H lapply (lift_inv_flat2_aux … H) /2/ qed. - -(* the main properies *******************************************************) - -axiom lift_total: ∀d,e,T1. ∃T2. ↑[d,e] T1 ≡ T2. - -axiom lift_mono: ∀d,e,T,U1. ↑[d,e] T ≡ U1 → ∀U2. ↑[d,e] T ≡ U2 → U1 = U2. - -theorem lift_conf_rev: ∀d1,e1,T1,T. ↑[d1,e1] T1 ≡ T → - ∀d2,e2,T2. ↑[d2 + e1, e2] T2 ≡ T → - d1 ≤ d2 → - ∃∃T0. ↑[d1, e1] T0 ≡ T2 & ↑[d2, e2] T0 ≡ T1. -#d1 #e1 #T1 #T #H elim H -H d1 e1 T1 T -[ #k #d1 #e1 #d2 #e2 #T2 #Hk #Hd12 - lapply (lift_inv_sort2 … Hk) -Hk #Hk destruct -T2 /3/ -| #i #d1 #e1 #Hid1 #d2 #e2 #T2 #Hi #Hd12 - lapply (lift_inv_lref2 … Hi) -Hi * * #Hid2 #H destruct -T2 - [ -Hid2 /4/ - | elim (lt_false d1 ?) - @(le_to_lt_to_lt … Hd12) -Hd12 @(le_to_lt_to_lt … Hid1) -Hid1 /2/ - ] -| #i #d1 #e1 #Hid1 #d2 #e2 #T2 #Hi #Hd12 - lapply (lift_inv_lref2 … Hi) -Hi * * #Hid2 #H destruct -T2 - [ -Hd12; lapply (lt_plus_to_lt_l … Hid2) -Hid2 #Hid2 /3/ - | -Hid1; lapply (arith1 … Hid2) -Hid2 #Hid2 - @(ex2_1_intro … #(i - e2)) - [ >le_plus_minus_comm [ @lift_lref_ge @(transitive_le … Hd12) -Hd12 /2/ | -Hd12 /2/ ] - | -Hd12 >(plus_minus_m_m i e2) in ⊢ (? ? ? ? %) /3/ - ] - ] -| #I #W1 #W #U1 #U #d1 #e1 #_ #_ #IHW #IHU #d2 #e2 #T2 #H #Hd12 - lapply (lift_inv_bind2 … H) -H * #W2 #U2 #HW2 #HU2 #H destruct -T2; - elim (IHW … HW2 ?) // -IHW HW2 #W0 #HW2 #HW1 - >plus_plus_comm_23 in HU2 #HU2 elim (IHU … HU2 ?) /3 width = 5/ -| #I #W1 #W #U1 #U #d1 #e1 #_ #_ #IHW #IHU #d2 #e2 #T2 #H #Hd12 - lapply (lift_inv_flat2 … H) -H * #W2 #U2 #HW2 #HU2 #H destruct -T2; - elim (IHW … HW2 ?) // -IHW HW2 #W0 #HW2 #HW1 - elim (IHU … HU2 ?) /3 width = 5/ -] -qed. - -theorem lift_free: ∀d1,e2,T1,T2. ↑[d1, e2] T1 ≡ T2 → ∀d2,e1. - d1 ≤ d2 → d2 ≤ d1 + e1 → e1 ≤ e2 → - ∃∃T. ↑[d1, e1] T1 ≡ T & ↑[d2, e2 - e1] T ≡ T2. -#d1 #e2 #T1 #T2 #H elim H -H d1 e2 T1 T2 -[ /3/ -| #i #d1 #e2 #Hid1 #d2 #e1 #Hd12 #_ #_ - lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 /4/ -| #i #d1 #e2 #Hid1 #d2 #e1 #_ #Hd21 #He12 - lapply (transitive_le …(i+e1) Hd21 ?) /2/ -Hd21 #Hd21 - <(plus_plus_minus_m_m e1 e2 i) /3/ -| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12 - elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b - elim (IHT (d2+1) … ? ? He12) /3 width = 5/ -| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12 - elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b - elim (IHT d2 … ? ? He12) /3 width = 5/ -] -qed. - -theorem lift_trans: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → - ∀d2,e2,T2. ↑[d2, e2] T ≡ T2 → - d1 ≤ d2 → d2 ≤ d1 + e1 → ↑[d1, e1 + e2] T1 ≡ T2. -#d1 #e1 #T1 #T #H elim H -d1 e1 T1 T -[ #k #d1 #e1 #d2 #e2 #T2 #HT2 #_ #_ - >(lift_inv_sort1 … HT2) -HT2 // -| #i #d1 #e1 #Hid1 #d2 #e2 #T2 #HT2 #Hd12 #_ - lapply (lift_inv_lref1 … HT2) -HT2 * * #Hid2 #H destruct -T2 - [ -Hd12 Hid2 /2/ - | lapply (le_to_lt_to_lt … d1 Hid2 ?) // -Hid1 Hid2 #Hd21 - lapply (le_to_lt_to_lt … d1 Hd12 ?) // -Hd12 Hd21 #Hd11 - elim (lt_false … Hd11) - ] -| #i #d1 #e1 #Hid1 #d2 #e2 #T2 #HT2 #_ #Hd21 - lapply (lift_inv_lref1 … HT2) -HT2 * * #Hid2 #H destruct -T2 - [ lapply (lt_to_le_to_lt … (d1+e1) Hid2 ?) // -Hid2 Hd21 #H - lapply (lt_plus_to_lt_l … H) -H #H - lapply (le_to_lt_to_lt … d1 Hid1 ?) // -Hid1 H #Hd11 - elim (lt_false … Hd11) - | -Hd21 Hid2 /2/ - ] -| #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd12 #Hd21 - lapply (lift_inv_bind1 … HX) -HX * #V0 #T0 #HV20 #HT20 #HX destruct -X; - lapply (IHV12 … HV20 ? ?) // -IHV12 HV20 #HV10 - lapply (IHT12 … HT20 ? ?) /2/ -| #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd12 #Hd21 - lapply (lift_inv_flat1 … HX) -HX * #V0 #T0 #HV20 #HT20 #HX destruct -X; - lapply (IHV12 … HV20 ? ?) // -IHV12 HV20 #HV10 - lapply (IHT12 … HT20 ? ?) /2/ -] -qed. - -axiom lift_trans_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → - ∀d2,e2,T2. ↑[d2, e2] T ≡ T2 → d2 ≤ d1 → - ∃∃T0. ↑[d2, e2] T1 ≡ T0 & ↑[d1 + e2, e1] T0 ≡ T2. - -axiom lift_trans_ge: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → - ∀d2,e2,T2. ↑[d2, e2] T ≡ T2 → d1 + e1 ≤ d2 → - ∃∃T0. ↑[d2 - e1, e2] T1 ≡ T0 & ↑[d1, e1] T0 ≡ T2. diff --git a/matita/matita/lib/lambda-delta/substitution/lift_fun.ma b/matita/matita/lib/lambda-delta/substitution/lift_fun.ma new file mode 100644 index 000000000..ee54dede2 --- /dev/null +++ b/matita/matita/lib/lambda-delta/substitution/lift_fun.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "lambda-delta/substitution/lift_defs.ma". + +(* RELOCATION ***************************************************************) + +(* the functional properties **************************************************) + +axiom lift_total: ∀d,e,T1. ∃T2. ↑[d,e] T1 ≡ T2. + +axiom lift_mono: ∀d,e,T,U1. ↑[d,e] T ≡ U1 → ∀U2. ↑[d,e] T ≡ U2 → U1 = U2. + +axiom lift_inj: ∀d,e,T1,U. ↑[d,e] T1 ≡ U → ∀T2. ↑[d,e] T2 ≡ U → T1 = T2. diff --git a/matita/matita/lib/lambda-delta/substitution/lift_main.ma b/matita/matita/lib/lambda-delta/substitution/lift_main.ma new file mode 100644 index 000000000..2f588c1a6 --- /dev/null +++ b/matita/matita/lib/lambda-delta/substitution/lift_main.ma @@ -0,0 +1,111 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "lambda-delta/substitution/lift_defs.ma". + +(* RELOCATION ***************************************************************) + +(* the main properies *******************************************************) + +theorem lift_conf_rev: ∀d1,e1,T1,T. ↑[d1,e1] T1 ≡ T → + ∀d2,e2,T2. ↑[d2 + e1, e2] T2 ≡ T → + d1 ≤ d2 → + ∃∃T0. ↑[d1, e1] T0 ≡ T2 & ↑[d2, e2] T0 ≡ T1. +#d1 #e1 #T1 #T #H elim H -H d1 e1 T1 T +[ #k #d1 #e1 #d2 #e2 #T2 #Hk #Hd12 + lapply (lift_inv_sort2 … Hk) -Hk #Hk destruct -T2 /3/ +| #i #d1 #e1 #Hid1 #d2 #e2 #T2 #Hi #Hd12 + lapply (lift_inv_lref2 … Hi) -Hi * * #Hid2 #H destruct -T2 + [ -Hid2 /4/ + | elim (lt_false d1 ?) + @(le_to_lt_to_lt … Hd12) -Hd12 @(le_to_lt_to_lt … Hid1) -Hid1 /2/ + ] +| #i #d1 #e1 #Hid1 #d2 #e2 #T2 #Hi #Hd12 + lapply (lift_inv_lref2 … Hi) -Hi * * #Hid2 #H destruct -T2 + [ -Hd12; lapply (lt_plus_to_lt_l … Hid2) -Hid2 #Hid2 /3/ + | -Hid1; lapply (arith1 … Hid2) -Hid2 #Hid2 + @(ex2_1_intro … #(i - e2)) + [ >le_plus_minus_comm [ @lift_lref_ge @(transitive_le … Hd12) -Hd12 /2/ | -Hd12 /2/ ] + | -Hd12 >(plus_minus_m_m i e2) in ⊢ (? ? ? ? %) /3/ + ] + ] +| #I #W1 #W #U1 #U #d1 #e1 #_ #_ #IHW #IHU #d2 #e2 #T2 #H #Hd12 + lapply (lift_inv_bind2 … H) -H * #W2 #U2 #HW2 #HU2 #H destruct -T2; + elim (IHW … HW2 ?) // -IHW HW2 #W0 #HW2 #HW1 + >plus_plus_comm_23 in HU2 #HU2 elim (IHU … HU2 ?) /3 width = 5/ +| #I #W1 #W #U1 #U #d1 #e1 #_ #_ #IHW #IHU #d2 #e2 #T2 #H #Hd12 + lapply (lift_inv_flat2 … H) -H * #W2 #U2 #HW2 #HU2 #H destruct -T2; + elim (IHW … HW2 ?) // -IHW HW2 #W0 #HW2 #HW1 + elim (IHU … HU2 ?) /3 width = 5/ +] +qed. + +theorem lift_free: ∀d1,e2,T1,T2. ↑[d1, e2] T1 ≡ T2 → ∀d2,e1. + d1 ≤ d2 → d2 ≤ d1 + e1 → e1 ≤ e2 → + ∃∃T. ↑[d1, e1] T1 ≡ T & ↑[d2, e2 - e1] T ≡ T2. +#d1 #e2 #T1 #T2 #H elim H -H d1 e2 T1 T2 +[ /3/ +| #i #d1 #e2 #Hid1 #d2 #e1 #Hd12 #_ #_ + lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 /4/ +| #i #d1 #e2 #Hid1 #d2 #e1 #_ #Hd21 #He12 + lapply (transitive_le …(i+e1) Hd21 ?) /2/ -Hd21 #Hd21 + <(plus_plus_minus_m_m e1 e2 i) /3/ +| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12 + elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b + elim (IHT (d2+1) … ? ? He12) /3 width = 5/ +| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12 + elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b + elim (IHT d2 … ? ? He12) /3 width = 5/ +] +qed. + +theorem lift_trans: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → + ∀d2,e2,T2. ↑[d2, e2] T ≡ T2 → + d1 ≤ d2 → d2 ≤ d1 + e1 → ↑[d1, e1 + e2] T1 ≡ T2. +#d1 #e1 #T1 #T #H elim H -d1 e1 T1 T +[ #k #d1 #e1 #d2 #e2 #T2 #HT2 #_ #_ + >(lift_inv_sort1 … HT2) -HT2 // +| #i #d1 #e1 #Hid1 #d2 #e2 #T2 #HT2 #Hd12 #_ + lapply (lift_inv_lref1 … HT2) -HT2 * * #Hid2 #H destruct -T2 + [ -Hd12 Hid2 /2/ + | lapply (le_to_lt_to_lt … d1 Hid2 ?) // -Hid1 Hid2 #Hd21 + lapply (le_to_lt_to_lt … d1 Hd12 ?) // -Hd12 Hd21 #Hd11 + elim (lt_false … Hd11) + ] +| #i #d1 #e1 #Hid1 #d2 #e2 #T2 #HT2 #_ #Hd21 + lapply (lift_inv_lref1 … HT2) -HT2 * * #Hid2 #H destruct -T2 + [ lapply (lt_to_le_to_lt … (d1+e1) Hid2 ?) // -Hid2 Hd21 #H + lapply (lt_plus_to_lt_l … H) -H #H + lapply (le_to_lt_to_lt … d1 Hid1 ?) // -Hid1 H #Hd11 + elim (lt_false … Hd11) + | -Hd21 Hid2 /2/ + ] +| #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd12 #Hd21 + lapply (lift_inv_bind1 … HX) -HX * #V0 #T0 #HV20 #HT20 #HX destruct -X; + lapply (IHV12 … HV20 ? ?) // -IHV12 HV20 #HV10 + lapply (IHT12 … HT20 ? ?) /2/ +| #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd12 #Hd21 + lapply (lift_inv_flat1 … HX) -HX * #V0 #T0 #HV20 #HT20 #HX destruct -X; + lapply (IHV12 … HV20 ? ?) // -IHV12 HV20 #HV10 + lapply (IHT12 … HT20 ? ?) /2/ +] +qed. + +axiom lift_trans_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → + ∀d2,e2,T2. ↑[d2, e2] T ≡ T2 → d2 ≤ d1 → + ∃∃T0. ↑[d2, e2] T1 ≡ T0 & ↑[d1 + e2, e1] T0 ≡ T2. + +axiom lift_trans_ge: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → + ∀d2,e2,T2. ↑[d2, e2] T ≡ T2 → d1 + e1 ≤ d2 → + ∃∃T0. ↑[d2 - e1, e2] T1 ≡ T0 & ↑[d1, e1] T0 ≡ T2. diff --git a/matita/matita/lib/lambda-delta/substitution/subst.ma b/matita/matita/lib/lambda-delta/substitution/subst_defs.ma similarity index 93% rename from matita/matita/lib/lambda-delta/substitution/subst.ma rename to matita/matita/lib/lambda-delta/substitution/subst_defs.ma index 18eb6c526..5ef343857 100644 --- a/matita/matita/lib/lambda-delta/substitution/subst.ma +++ b/matita/matita/lib/lambda-delta/substitution/subst_defs.ma @@ -10,7 +10,7 @@ V_______________________________________________________________ *) include "lambda-delta/syntax/lenv.ma". -include "lambda-delta/substitution/lift.ma". +include "lambda-delta/substitution/lift_defs.ma". (* TELESCOPIC SUBSTITUTION **************************************************) @@ -33,6 +33,8 @@ inductive subst: lenv → term → nat → nat → term → Prop ≝ interpretation "telescopic substritution" 'RSubst L T1 d e T2 = (subst L T1 d e T2). +(* The basic properties *****************************************************) + lemma subst_lift_inv: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀L. L ⊢ ↓[d,e] T2 ≡ T1. #d #e #T1 #T2 #H elim H -H d e T1 T2 /2/ #i #d #e #Hdi #L >(minus_plus_m_m i e) in ⊢ (? ? ? ? ? %) /3/ (**) (* use \ldots *) diff --git a/matita/matita/lib/lambda-delta/substitution/thin.ma b/matita/matita/lib/lambda-delta/substitution/thin_defs.ma similarity index 64% rename from matita/matita/lib/lambda-delta/substitution/thin.ma rename to matita/matita/lib/lambda-delta/substitution/thin_defs.ma index be7957422..1e7847603 100644 --- a/matita/matita/lib/lambda-delta/substitution/thin.ma +++ b/matita/matita/lib/lambda-delta/substitution/thin_defs.ma @@ -9,7 +9,7 @@ \ / V_______________________________________________________________ *) -include "lambda-delta/substitution/subst.ma". +include "lambda-delta/substitution/subst_defs.ma". (* THINNING *****************************************************************) @@ -42,20 +42,3 @@ lemma thin_inv_skip2: ∀d,e,I,L1,K2,V2. ↓[d, e] L1 ≡ K2. 𝕓{I} V2 → 0 < ∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 & K1 ⊢ ↓[d - 1, e] V1 ≡ V2 & L1 = K1. 𝕓{I} V1. /2/ qed. - -(* the main properties ******************************************************) - -axiom thin_conf_ge: ∀d1,e1,L,L1. ↓[d1,e1] L ≡ L1 → - ∀e2,L2. ↓[0,e2] L ≡ L2 → d1 + e1 ≤ e2 → ↓[0,e2-e1] L1 ≡ L2. - -axiom thin_conf_lt: ∀d1,e1,L,L1. ↓[d1,e1] L ≡ L1 → - ∀e2,K2,I,V2. ↓[0,e2] L ≡ K2. 𝕓{I} V2 → - e2 < d1 → let d ≝ d1 - e2 - 1 in - ∃∃K1,V1. ↓[0,e2] L1 ≡ K1. 𝕓{I} V1 & ↓[d,e1] K2 ≡ K1 & ↑[d,e1] V1 ≡ V2. - -axiom thin_trans_le: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L → - ∀e2,L2. ↓[0, e2] L ≡ L2 → e2 ≤ d1 → - ∃∃L0. ↓[0, e2] L1 ≡ L0 & ↓[d1 - e2, e1] L0 ≡ L2. - -axiom thin_trans_ge: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L → - ∀e2,L2. ↓[0, e2] L ≡ L2 → d1 ≤ e2 → ↓[0, e1 + e2] L1 ≡ L2. diff --git a/matita/matita/lib/lambda-delta/substitution/thin_main.ma b/matita/matita/lib/lambda-delta/substitution/thin_main.ma new file mode 100644 index 000000000..f16fb3a48 --- /dev/null +++ b/matita/matita/lib/lambda-delta/substitution/thin_main.ma @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "lambda-delta/substitution/thin_defs.ma". + +(* THINNING *****************************************************************) + +(* the main properties ******************************************************) + +axiom thin_conf_ge: ∀d1,e1,L,L1. ↓[d1,e1] L ≡ L1 → + ∀e2,L2. ↓[0,e2] L ≡ L2 → d1 + e1 ≤ e2 → ↓[0,e2-e1] L1 ≡ L2. + +axiom thin_conf_lt: ∀d1,e1,L,L1. ↓[d1,e1] L ≡ L1 → + ∀e2,K2,I,V2. ↓[0,e2] L ≡ K2. 𝕓{I} V2 → + e2 < d1 → let d ≝ d1 - e2 - 1 in + ∃∃K1,V1. ↓[0,e2] L1 ≡ K1. 𝕓{I} V1 & ↓[d,e1] K2 ≡ K1 & ↑[d,e1] V1 ≡ V2. + +axiom thin_trans_le: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L → + ∀e2,L2. ↓[0, e2] L ≡ L2 → e2 ≤ d1 → + ∃∃L0. ↓[0, e2] L1 ≡ L0 & ↓[d1 - e2, e1] L0 ≡ L2. + +axiom thin_trans_ge: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L → + ∀e2,L2. ↓[0, e2] L ≡ L2 → d1 ≤ e2 → ↓[0, e1 + e2] L1 ≡ L2. -- 2.39.2