From: Ferruccio Guidi Date: Mon, 28 Jan 2013 18:25:59 +0000 (+0000) Subject: - notation change for weight functions (following lambda) X-Git-Tag: make_still_working~1298 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=fba384e357ed3c8781fc018c2c16f2b40df144af - notation change for weight functions (following lambda) that used to clash with the lref construction - some parentheses added arround application arguments --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma index f4da11310..2ffff40df 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma @@ -31,7 +31,7 @@ theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP. #RR #RS #RP #H1RP #H2RP #L1 #T #A #H elim H -L1 -T -A [ #L #k #L0 #des #HL0 #X #H #L2 #HL20 >(lifts_inv_sort1 … H) -H - lapply (aacr_acr … H1RP H2RP ⓪) #HAtom + lapply (aacr_acr … H1RP H2RP (⓪)) #HAtom @(s2 … HAtom … ◊) // /2 width=2/ | #I #L1 #K1 #V1 #B #i #HLK1 #HKV1B #IHB #L0 #des #HL01 #X #H #L2 #HL20 lapply (aacr_acr … H1RP H2RP B) #HB diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta.ma index d96994e6c..ea04940d8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta.ma @@ -34,7 +34,7 @@ qed-. fact snv_ssta_conf_aux: ∀h,g,L,T. ( ∀L0,T0. ⦃h, L0⦄ ⊩ T0 :[g] → ∀U0,l. ⦃h, L0⦄ ⊢ T0 •[g, l + 1] U0 → - #{L0, T0} < #{L, T} → ⦃h, L0⦄ ⊩ U0 :[g] + ♯{L0, T0} < ♯{L, T} → ⦃h, L0⦄ ⊩ U0 :[g] ) → ∀L0,T0. ⦃h, L0⦄ ⊩ T0 :[g] → ∀U0,l. ⦃h, L0⦄ ⊢ T0 •[g, l + 1] U0 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma index fbe41b9d4..35796b6ba 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma @@ -17,42 +17,42 @@ include "basic_2/grammar/cl_shift.ma". (* WEIGHT OF A CLOSURE ******************************************************) -definition fw: lenv → term → ? ≝ λL,T. #{L} + #{T}. +definition fw: lenv → term → ? ≝ λL,T. ♯{L} + ♯{T}. interpretation "weight (closure)" 'Weight L T = (fw L T). (* Basic properties *********************************************************) (* Basic_1: was: flt_shift *) -lemma fw_shift: ∀a,K,I,V,T. #{K. ⓑ{I} V, T} < #{K, ⓑ{a,I} V. T}. +lemma fw_shift: ∀a,K,I,V,T. ♯{K. ⓑ{I} V, T} < ♯{K, ⓑ{a,I} V. T}. normalize // qed. -lemma tw_shift: ∀L,T. #{L, T} ≤ #{L @@ T}. +lemma tw_shift: ∀L,T. ♯{L, T} ≤ ♯{L @@ T}. #L elim L // #K #I #V #IHL #T @transitive_le [3: @IHL |2: /2 width=2/ | skip ] qed. -lemma fw_tpair_sn: ∀I,L,V,T. #{L, V} < #{L, ②{I}V.T}. +lemma fw_tpair_sn: ∀I,L,V,T. ♯{L, V} < ♯{L, ②{I}V.T}. normalize in ⊢ (?→?→?→?→?%%); // qed. -lemma fw_tpair_dx: ∀I,L,V,T. #{L, T} < #{L, ②{I}V.T}. +lemma fw_tpair_dx: ∀I,L,V,T. ♯{L, T} < ♯{L, ②{I}V.T}. normalize in ⊢ (?→?→?→?→?%%); // qed. -lemma fw_tpair_dx_sn: ∀I1,I2,L,V1,V2,T. #{L, V2} < #{L, ②{I1}V1.②{I2}V2.T}. +lemma fw_tpair_dx_sn: ∀I1,I2,L,V1,V2,T. ♯{L, V2} < ♯{L, ②{I1}V1.②{I2}V2.T}. normalize in ⊢ (?→?→?→?→?→?→?%%); /2 width=1/ qed. lemma fw_tpair_sn_sn_shift: ∀I,I1,I2,L,V1,V2,T. - #{L.ⓑ{I}V1, T} < #{L, ②{I1}V1.②{I2}V2.T}. -normalize in ⊢ (?→?→?→?→?→?→?→?%%); /3 width=1/ + ♯{L.ⓑ{I}V1, T} < ♯{L, ②{I1}V1.②{I2}V2.T}. +normalize in ⊢ (?→?→?→?→?→?→?→?%%); /3 width=1/ qed. lemma fw_tpair_sn_dx_shift: ∀I,I1,I2,L,V1,V2,T. - #{L.ⓑ{I}V2, T} < #{L, ②{I1}V1.②{I2}V2.T}. + ♯{L.ⓑ{I}V2, T} < ♯{L, ②{I1}V1.②{I2}V2.T}. normalize in ⊢ (?→?→?→?→?→?→?→?%%); /2 width=1/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma index ab90ddf29..0916ac9e3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma @@ -98,7 +98,7 @@ qed-. (* Basic_eliminators ********************************************************) -fact lenv_ind_dx_aux: ∀R:predicate lenv. R ⋆ → +fact lenv_ind_dx_aux: ∀R:predicate lenv. R (⋆) → (∀I,L,V. R L → R (⋆.ⓑ{I}V @@ L)) → ∀d,L. |L| = d → R L. #R #Hatom #Hpair #d @(nat_ind_plus … d) -d @@ -108,7 +108,7 @@ fact lenv_ind_dx_aux: ∀R:predicate lenv. R ⋆ → ] qed-. -lemma lenv_ind_dx: ∀R:predicate lenv. R ⋆ → +lemma lenv_ind_dx: ∀R:predicate lenv. R (⋆) → (∀I,L,V. R L → R (⋆.ⓑ{I}V @@ L)) → ∀L. R L. /3 width=2 by lenv_ind_dx_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_weight.ma index 537d32e56..7893bff32 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_weight.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_weight.ma @@ -19,14 +19,14 @@ include "basic_2/grammar/lenv.ma". let rec lw L ≝ match L with [ LAtom ⇒ 0 -| LPair L _ V ⇒ lw L + #{V} +| LPair L _ V ⇒ lw L + ♯{V} ]. interpretation "weight (local environment)" 'Weight L = (lw L). (* Basic properties *********************************************************) -lemma lw_pair: ∀I,L,V. #{L} < #{(L.ⓑ{I}V)}. +lemma lw_pair: ∀I,L,V. ♯{L} < ♯{L.ⓑ{I}V}. /3 width=1/ qed. (* Basic_1: removed theorems 2: clt_cong clt_head clt_thead *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/term_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_weight.ma index 3f9fbef87..2e3f96bc7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/term_weight.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_weight.ma @@ -26,7 +26,7 @@ interpretation "weight (term)" 'Weight T = (tw T). (* Basic properties *********************************************************) (* Basic_1: was: tweight_lt *) -lemma tw_pos: ∀T. 1 ≤ #{T}. +lemma tw_pos: ∀T. 1 ≤ ♯{T}. #T elim T -T // qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation.ma b/matita/matita/contribs/lambdadelta/basic_2/notation.ma index 728647926..e378dc719 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation.ma @@ -17,27 +17,27 @@ (* Grammar ******************************************************************) notation "⓪" - non associative with precedence 90 + non associative with precedence 55 for @{ 'Item0 }. notation "hvbox( ⓪ { term 46 I } )" - non associative with precedence 90 + non associative with precedence 55 for @{ 'Item0 $I }. notation "⋆" - non associative with precedence 90 + non associative with precedence 46 for @{ 'Star }. notation "hvbox( ⋆ term 90 k )" - non associative with precedence 90 + non associative with precedence 55 for @{ 'Star $k }. notation "hvbox( # term 90 i )" - non associative with precedence 90 + non associative with precedence 55 for @{ 'LRef $i }. notation "hvbox( § term 90 p )" - non associative with precedence 90 + non associative with precedence 55 for @{ 'GRef $p }. notation "hvbox( ② term 55 T1 . break term 55 T )" @@ -120,11 +120,11 @@ notation "hvbox( T . break ④ { term 46 I } break { term 46 T1 , break term 46 non associative with precedence 50 for @{ 'DxItem4 $T $I $T1 $T2 $T3 }. -notation "hvbox( # { term 46 x } )" +notation "hvbox( ♯ { term 46 x } )" non associative with precedence 90 for @{ 'Weight $x }. -notation "hvbox( # { term 46 x , break term 46 y } )" +notation "hvbox( ♯ { term 46 x , break term 46 y } )" non associative with precedence 90 for @{ 'Weight $x $y }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpr.ma index cf82cfc37..efe122261 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpr.ma @@ -23,7 +23,7 @@ fact tpr_conf_atom_atom: ∀I. ∃∃X. ⓪{I} ➡ X & ⓪{I} ➡ X. fact tpr_conf_flat_flat: ∀I,V0,V1,T0,T1,V2,T2. ( - ∀X0:term. #{X0} < #{V0} + #{T0} + 1 → + ∀X0:term. ♯{X0} < ♯{V0} + ♯{T0} + 1 → ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → ∃∃X. X1 ➡ X & X2 ➡ X ) → @@ -36,7 +36,7 @@ qed. fact tpr_conf_flat_beta: ∀a,V0,V1,T1,V2,W0,U0,T2. ( - ∀X0:term. #{X0} < #{V0} + (#{W0} + #{U0} + 1) + 1 → + ∀X0:term. ♯{X0} < ♯{V0} + (♯{W0} + ♯{U0} + 1) + 1 → ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → ∃∃X. X1 ➡ X & X2 ➡ X ) → @@ -55,7 +55,7 @@ qed. *) fact tpr_conf_flat_theta: ∀a,V0,V1,T1,V2,V,W0,W2,U0,U2. ( - ∀X0:term. #{X0} < #{V0} + (#{W0} + #{U0} + 1) + 1 → + ∀X0:term. ♯{X0} < ♯{V0} + (♯{W0} + ♯{U0} + 1) + 1 → ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → ∃∃X. X1 ➡ X & X2 ➡ X ) → @@ -87,7 +87,7 @@ qed. fact tpr_conf_flat_cast: ∀X2,V0,V1,T0,T1. ( - ∀X0:term. #{X0} < #{V0} + #{T0} + 1 → + ∀X0:term. ♯{X0} < ♯{V0} + ♯{T0} + 1 → ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → ∃∃X. X1 ➡ X & X2 ➡ X ) → @@ -99,7 +99,7 @@ qed. fact tpr_conf_beta_beta: ∀a. ∀W0:term. ∀V0,V1,T0,T1,V2,T2. ( - ∀X0:term. #{X0} < #{V0} + (#{W0} + #{T0} + 1) + 1 → + ∀X0:term. ♯{X0} < ♯{V0} + (♯{W0} + ♯{T0} + 1) + 1 → ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → ∃∃X. X1 ➡ X & X2 ➡ X ) → @@ -113,7 +113,7 @@ qed. (* Basic_1: was: pr0_cong_delta pr0_delta_delta *) fact tpr_conf_delta_delta: ∀a,I1,V0,V1,T0,T1,TT1,V2,T2,TT2. ( - ∀X0:term. #{X0} < #{V0} + #{T0} + 1 → + ∀X0:term. ♯{X0} < ♯{V0} + ♯{T0} + 1 → ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → ∃∃X. X1 ➡ X & X2 ➡ X ) → @@ -132,7 +132,7 @@ qed. fact tpr_conf_delta_zeta: ∀X2,V0,V1,T0,T1,TT1,T2. ( - ∀X0:term. #{X0} < #{V0} + #{T0} + 1 → + ∀X0:term. ♯{X0} < ♯{V0} + ♯{T0} + 1 → ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → ∃∃X. X1 ➡ X & X2 ➡ X ) → @@ -149,7 +149,7 @@ qed. (* Basic_1: was: pr0_upsilon_upsilon *) fact tpr_conf_theta_theta: ∀a,VV1,V0,V1,W0,W1,T0,T1,V2,VV2,W2,T2. ( - ∀X0:term. #{X0} < #{V0} + (#{W0} + #{T0} + 1) + 1 → + ∀X0:term. ♯{X0} < ♯{V0} + (♯{W0} + ♯{T0} + 1) + 1 → ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → ∃∃X. X1 ➡ X & X2 ➡ X ) → @@ -168,7 +168,7 @@ qed. fact tpr_conf_zeta_zeta: ∀V0:term. ∀X2,TT0,T0,T1,TT2. ( - ∀X0:term. #{X0} < #{V0} + #{TT0} + 1 → + ∀X0:term. ♯{X0} < ♯{V0} + ♯{TT0} + 1 → ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → ∃∃X. X1 ➡ X & X2 ➡ X ) → @@ -184,7 +184,7 @@ qed. fact tpr_conf_tau_tau: ∀V0,T0:term. ∀X2,T1. ( - ∀X0:term. #{X0} < #{V0} + #{T0} + 1 → + ∀X0:term. ♯{X0} < ♯{V0} + ♯{T0} + 1 → ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → ∃∃X. X1 ➡ X & X2 ➡ X ) → diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma index b5f416344..f9a98fec1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma @@ -18,7 +18,7 @@ include "basic_2/substitution/ldrop.ma". (* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************) inductive aaa: lenv → term → predicate aarity ≝ -| aaa_sort: ∀L,k. aaa L (⋆k) ⓪ +| aaa_sort: ∀L,k. aaa L (⋆k) (⓪) | aaa_lref: ∀I,L,K,V,B,i. ⇩[0, i] L ≡ K. ⓑ{I} V → aaa K V B → aaa L (#i) B | aaa_abbr: ∀a,L,V,T,B,A. aaa L V B → aaa (L. ⓓV) T A → aaa L (ⓓ{a}V. T) A diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/frsup.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/frsup.ma index 31d6c9fee..a561410d8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/frsup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/frsup.ma @@ -77,15 +77,15 @@ lemma frsup_inv_flat1: ∀J,L1,L2,W,U,T2. ⦃L1, ⓕ{J}W.U⦄ ⧁ ⦃L2, T2⦄ (* Basic forward lemmas *****************************************************) -lemma frsup_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → #{L2, T2} < #{L1, T1}. +lemma frsup_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → ♯{L2, T2} < ♯{L1, T1}. #L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 /width=1/ qed-. -lemma frsup_fwd_lw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → #{L1} ≤ #{L2}. +lemma frsup_fwd_lw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → ♯{L1} ≤ ♯{L2}. #L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 /width=1/ qed-. -lemma frsup_fwd_tw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → #{T2} < #{T1}. +lemma frsup_fwd_tw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → ♯{T2} < ♯{T1}. #L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 /width=1/ /2 width=1 by le_minus_to_plus/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma index 9511648aa..12b30e693 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma @@ -258,7 +258,7 @@ lemma ldrop_fwd_ldrop2: ∀L1,I2,K2,V2,e. ⇩[O, e] L1 ≡ K2. ⓑ{I2} V2 → ] qed-. -lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → #{L2} ≤ #{L1}. +lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ♯{L2} ≤ ♯{L1}. #L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize [ /2 width=3/ | #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12 @@ -267,7 +267,7 @@ lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → #{L2} ≤ #{L1}. qed-. lemma ldrop_pair2_fwd_fw: ∀I,L,K,V,d,e. ⇩[d, e] L ≡ K. ⓑ{I} V → - ∀T. #{K, V} < #{L, T}. + ∀T. ♯{K, V} < ♯{L, T}. #I #L #K #V #d #e #H #T lapply (ldrop_fwd_lw … H) -H #H @(le_to_lt_to_lt … H) -H /3 width=1/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma index 36c353ba9..bcc1db8b2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma @@ -275,7 +275,7 @@ qed-. (* Basic forward lemmas *****************************************************) -lemma tw_lift: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → #{T1} = #{T2}. +lemma tw_lift: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → ♯{T1} = ♯{T2}. #d #e #T1 #T2 #H elim H -d -e -T1 -T2 normalize // qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma index 6872e4b2b..38b1dfe7c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma @@ -253,7 +253,7 @@ lemma tps_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 ▶ [d, 0] T2 → T1 = T2. (* Basic forward lemmas *****************************************************) -lemma tps_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▶ [d, e] T2 → #{T1} ≤ #{T2}. +lemma tps_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▶ [d, e] T2 → ♯{T1} ≤ ♯{T2}. #L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e normalize /3 by monotonic_le_plus_l, le_plus/ (**) (* just /3 width=1/ is too slow *) qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift.ma index e8ac23dae..cde529122 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift.ma @@ -102,7 +102,7 @@ qed-. (* Basic forward lemmas *****************************************************) -lemma delift_fwd_tw: ∀L,T1,T2,d,e. L ⊢ ▼*[d, e] T1 ≡ T2 → #{T1} ≤ #{T2}. +lemma delift_fwd_tw: ∀L,T1,T2,d,e. L ⊢ ▼*[d, e] T1 ≡ T2 → ♯{T1} ≤ ♯{T2}. #L #T1 #T2 #d #e * #T #HT1 #HT2 ->(tw_lift … HT2) -T2 /2 width=4 by tpss_fwd_tw / +>(tw_lift … HT2) -T2 /2 width=4 by tpss_fwd_tw/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma index 6828b50b7..75ce09957 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma @@ -82,7 +82,7 @@ lemma delift_ind_alt: ∀R:ℕ→ℕ→lenv→relation term. (∀L,d,e,i. i < d → R d e L (#i) (#i)) → (∀L,K,V1,V2,W2,i,d,e. d ≤ i → i < d + e → ⇩[O, i] L ≡ K.ⓓV1 → K ⊢ ▼*[O, d + e - i - 1] V1 ≡ V2 → - ⇧[O, d] V2 ≡ W2 → R O (d+e-i-1) K V1 V2 → R d e L #i W2 + ⇧[O, d] V2 ≡ W2 → R O (d+e-i-1) K V1 V2 → R d e L (#i) W2 ) → (∀L,d,e,i. d + e ≤ i → R d e L (#i) (#(i - e))) → (∀L,d,e,p. R d e L (§p) (§p)) → diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/frsupp.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/frsupp.ma index 1fee98341..add56ba3d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/frsupp.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/frsupp.ma @@ -64,19 +64,19 @@ lemma frsupp_strap2: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⧁ ⦃L, T⦄ → ⦃L, T (* Basic forward lemmas *****************************************************) -lemma frsupp_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → #{L2, T2} < #{L1, T1}. +lemma frsupp_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ♯{L2, T2} < ♯{L1, T1}. #L1 #L2 #T1 #T2 #H @(frsupp_ind … H) -L2 -T2 /3 width=3 by frsup_fwd_fw, transitive_lt/ qed-. -lemma frsupp_fwd_lw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → #{L1} ≤ #{L2}. +lemma frsupp_fwd_lw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ♯{L1} ≤ ♯{L2}. #L1 #L2 #T1 #T2 #H @(frsupp_ind … H) -L2 -T2 /2 width=3 by frsup_fwd_lw/ (**) (* /3 width=5 by frsup_fwd_lw, transitive_le/ is too slow *) #L #T #L2 #T2 #_ #HL2 #HL1 lapply (frsup_fwd_lw … HL2) -HL2 /2 width=3 by transitive_le/ qed-. -lemma frsupp_fwd_tw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → #{T2} < #{T1}. +lemma frsupp_fwd_tw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ♯{T2} < ♯{T1}. #L1 #L2 #T1 #T2 #H @(frsupp_ind … H) -L2 -T2 /3 width=3 by frsup_fwd_tw, transitive_lt/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/frsups.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/frsups.ma index 5923d60a3..373454cf9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/frsups.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/frsups.ma @@ -73,17 +73,17 @@ qed-. (* Basic forward lemmas *****************************************************) -lemma frsups_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄ → #{L2, T2} ≤ #{L1, T1}. +lemma frsups_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄ → ♯{L2, T2} ≤ ♯{L1, T1}. #L1 #L2 #T1 #T2 #H elim (frsups_inv_all … H) -H [ * // ] /3 width=1 by frsupp_fwd_fw, lt_to_le/ qed-. -lemma frsups_fwd_lw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄ → #{L1} ≤ #{L2}. +lemma frsups_fwd_lw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄ → ♯{L1} ≤ ♯{L2}. #L1 #L2 #T1 #T2 #H elim (frsups_inv_all … H) -H [ * // ] /2 width=3 by frsupp_fwd_lw/ qed-. -lemma frsups_fwd_tw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄ → #{T2} ≤ #{T1}. +lemma frsups_fwd_tw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁* ⦃L2, T2⦄ → ♯{T2} ≤ ♯{T1}. #L1 #L2 #T1 #T2 #H elim (frsups_inv_all … H) -H [ * // ] /3 width=3 by frsupp_fwd_tw, lt_to_le/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ltpss_dx.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ltpss_dx.ma index 67867f8c8..ab281b92b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ltpss_dx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ltpss_dx.ma @@ -52,7 +52,7 @@ lemma ltpss_dx_tpss_trans_eq: ∀L1,T2,U2,d,e. L1 ⊢ T2 ▶* [d, e] U2 → elim (ltpss_dx_ldrop_trans_be … HL01 … HLK1 ? ?) -HL01 -HLK1 // /2 width=2/ #X #H #HLK0 elim (ltpss_dx_inv_tpss22 … H ?) -H /2 width=1/ #K0 #V0 #HK01 #HV01 #H destruct lapply (tpss_fwd_tw … HV01) #H2 - lapply (transitive_le (#{K1} + #{V0}) … H1) -H1 /2 width=1/ -H2 #H + lapply (transitive_le (♯{K1} + ♯{V0}) … H1) -H1 /2 width=1/ -H2 #H lapply (tpss_trans_eq … HV01 HV12) -V1 #HV02 lapply (IH … HV02 … HK01) -IH -HV02 -HK01 [ normalize /2 width=1/ | /2 width=6/ ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma index 93916208b..cc5be0eca 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma @@ -164,7 +164,7 @@ qed-. (* Basic forward lemmas *****************************************************) -lemma tpss_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e] T2 → #{T1} ≤ #{T2}. +lemma tpss_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e] T2 → ♯{T1} ≤ ♯{T2}. #L #T1 #T2 #d #e #H @(tpss_ind … H) -T2 // #T #T2 #_ #HT2 #IHT1 lapply (tps_fwd_tw … HT2) -HT2 #HT2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma index ae1dcf624..46e064ca9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma @@ -81,11 +81,11 @@ lemma tpssa_tpss: ∀L,T1,T2,d,e. L ⊢ T1 ▶▶* [d, e] T2 → L ⊢ T1 ▶* [ #L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e // /2 width=6/ qed-. -lemma tpss_ind_alt: ∀R:ℕ→ℕ→lenv→relation term. +lemma tpss_ind_alt: ∀R:nat→nat→lenv→relation term. (∀L,I,d,e. R d e L (⓪{I}) (⓪{I})) → (∀L,K,V1,V2,W2,i,d,e. d ≤ i → i < d + e → ⇩[O, i] L ≡ K.ⓓV1 → K ⊢ V1 ▶* [O, d + e - i - 1] V2 → - ⇧[O, i + 1] V2 ≡ W2 → R O (d+e-i-1) K V1 V2 → R d e L #i W2 + ⇧[O, i + 1] V2 ≡ W2 → R O (d+e-i-1) K V1 V2 → R d e L (#i) W2 ) → (∀L,a,I,V1,V2,T1,T2,d,e. L ⊢ V1 ▶* [d, e] V2 → L.ⓑ{I}V2 ⊢ T1 ▶* [d + 1, e] T2 → R d e L V1 V2 →