From: Ferruccio Guidi Date: Sun, 26 Jan 2014 10:08:33 +0000 (+0000) Subject: - nat: some additions, plus_minus_commutative renamed plus_minus_associative X-Git-Tag: make_still_working~991 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cdf346ea9e5dd3842c67e0f0595e110a07c0094c;p=helm.git - nat: some additions, plus_minus_commutative renamed plus_minus_associative - lambda: we study terms in which references are by "level" rather than by "depth" aiming at establishing a bijection between the two representations, we start the support for distributed notation as in lambdadelta --- diff --git a/matita/matita/lib/arithmetics/chebyshev/bertrand.ma b/matita/matita/lib/arithmetics/chebyshev/bertrand.ma index 082008d68..99770436b 100644 --- a/matita/matita/lib/arithmetics/chebyshev/bertrand.ma +++ b/matita/matita/lib/arithmetics/chebyshev/bertrand.ma @@ -414,7 +414,7 @@ cut (0(eq_log_exp … (le_n ?)) >(eq_log_exp … (le_n ?)) - >plus_minus_commutative [2:@lt_O_log //] + >plus_minus_associative [2:@lt_O_log //] cut (2+3 ≤ 2+log 2 m) [@monotonic_le_plus_r @(le_exp_to_le 2) [@le_n|>Hclog @lt_to_le @lt8m]] generalize in match (2+log 2 m); #a #Hle >(commutative_times 2 a) diff --git a/matita/matita/lib/arithmetics/chebyshev/psi_bounds.ma b/matita/matita/lib/arithmetics/chebyshev/psi_bounds.ma index a1b5a62dd..985ccd82d 100644 --- a/matita/matita/lib/arithmetics/chebyshev/psi_bounds.ma +++ b/matita/matita/lib/arithmetics/chebyshev/psi_bounds.ma @@ -190,7 +190,7 @@ theorem le_Psi_exp1: ∀n. ] #Hcut @le_S_S_to_le cut(∀a,b. S a + b = S (a+b)) [//] #Hplus S_pred [>eq_minus_S_pred in ⊢ (??%); >S_pred - [>plus_minus_commutative + [>plus_minus_associative [@monotonic_le_minus_l cut (∀a. 2*a = a + a) [//] #times2 commutative_times @le_n @@ -263,7 +263,7 @@ theorem le_Psi_exp4: ∀n. 1 < n → [@lt_O_S |@(transitive_le ? (m+(m-3))) [@monotonic_le_plus_l // - |normalize plus_minus_commutative + |normalize plus_minus_associative [@le_n |>Hm @(transitive_le ? (2*2) ? (le_n_Sn 3)) @monotonic_le_times_r // @@ -297,7 +297,7 @@ theorem le_Psi_exp4: ∀n. 1 < n → >commutative_times in ⊢ (? (? (? % ?) ?) ?); >associative_times @monotonic_le_times_r plus_minus_commutative + >plus_minus_associative [normalize >(plus_n_O (a+(a+0))) in ⊢ (?(?(??%)?)?); @le_n |@le_S_S >(times_n_1 2) in ⊢ (?%?); @monotonic_le_times_r @Ha ] @@ -353,7 +353,7 @@ cases (decidable_le 9 m) [@lt_O_S |@(le_times_to_le 2) [@lt_O_S |commutative_times plus_n_Sm #H lapply (IHx … H) -x -z #H destruct ] qed-. @@ -197,68 +197,69 @@ qed-. (* Negated equalities *******************************************************) theorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m. -/2/ qed. +/2 width=3 by not_to_not/ qed. theorem not_eq_O_S : ∀n:nat. 0 ≠ S n. -#n @nmk #eqOS (change with (not_zero O)) >eqOS // qed. +#n @nmk #eqOS change with (not_zero 0) >eqOS // qed. theorem not_eq_n_Sn: ∀n:nat. n ≠ S n. -#n (elim n) /2/ qed. +#n elim n /2 width=1 by not_eq_S/ qed. (* Atomic conclusion *******************************************************) (* not_zero *) theorem lt_to_not_zero : ∀n,m:nat. n < m → not_zero m. -#n #m #Hlt (elim Hlt) // qed. +#n #m #Hlt elim Hlt // qed. (* le *) theorem le_S_S: ∀n,m:nat. n ≤ m → S n ≤ S m. -#n #m #lenm (elim lenm) /2/ qed. +#n #m #lenm elim lenm /2 width=1 by le_S/ qed. theorem le_O_n : ∀n:nat. 0 ≤ n. -#n (elim n) /2/ qed. +#n elim n /2 width=1 by le_S/ qed. theorem le_n_Sn : ∀n:nat. n ≤ S n. -/2/ qed. +/2 width=1 by le_S/ qed. theorem transitive_le : transitive nat le. -#a #b #c #leab #lebc (elim lebc) /2/ +#a #b #c #leab #lebc elim lebc /2 width=1 by le_S/ qed. theorem le_pred_n : ∀n:nat. pred n ≤ n. -#n (elim n) // qed. +#n elim n // qed. theorem monotonic_pred: monotonic ? le pred. -#n #m #lenm (elim lenm) /2/ qed. +#n #m #lenm elim lenm /2 width=3 by transitive_le/ qed. theorem le_S_S_to_le: ∀n,m:nat. S n ≤ S m → n ≤ m. (* demo *) -/2/ qed-. +/2 width=1 by monotonic_pred/ qed-. theorem monotonic_le_plus_r: ∀n:nat.monotonic nat le (λm.n + m). -#n #a #b (elim n) normalize // -#m #H #leab @le_S_S /2/ qed. +#n #a #b elim n normalize // +#m #H #leab /3 width=1 by le_S_S/ +qed. theorem monotonic_le_plus_l: ∀m:nat.monotonic nat le (λn.n + m). -/2/ qed. +/2 width=1 by monotonic_le_plus_r/ qed. theorem le_plus: ∀n1,n2,m1,m2:nat. n1 ≤ n2 → m1 ≤ m2 → n1 + m1 ≤ n2 + m2. #n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1+m2)) -/2/ qed. +/2 width=1 by monotonic_le_plus_l, monotonic_le_plus_r/ qed. theorem le_plus_n :∀n,m:nat. m ≤ n + m. -/2/ qed. +/2 width=1 by monotonic_le_plus_l/ qed. lemma le_plus_a: ∀a,n,m. n ≤ m → n ≤ a + m. -/2/ qed. +/2 width=1 by le_plus/ qed. lemma le_plus_b: ∀b,n,m. n + b ≤ m → n ≤ m. -/2/ qed. +/2 width=3 by transitive_le/ qed. theorem le_plus_n_r :∀n,m:nat. m ≤ m + n. /2/ qed. @@ -267,47 +268,46 @@ theorem eq_plus_to_le: ∀n,m,p:nat.n=m+p → m ≤ n. // qed-. theorem le_plus_to_le: ∀a,n,m. a + n ≤ a + m → n ≤ m. -#a (elim a) normalize /3/ qed. +#a elim a normalize /3 width=1 by monotonic_pred/ qed. theorem le_plus_to_le_r: ∀a,n,m. n + a ≤ m +a → n ≤ m. -/2/ qed-. +/2 width=2 by le_plus_to_le/ qed-. theorem monotonic_le_times_r: ∀n:nat.monotonic nat le (λm. n * m). -#n #x #y #lexy (elim n) normalize//(* lento /2/*) -#a #lea @le_plus // +#n #x #y #lexy elim n normalize /2 width=1 by le_plus/ qed. theorem le_times: ∀n1,n2,m1,m2:nat. n1 ≤ n2 → m1 ≤ m2 → n1*m1 ≤ n2*m2. -#n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1*m2)) /2/ +#n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1*m2)) +/2 width=1 by monotonic_le_times_r/ qed. (* interessante *) theorem lt_times_n: ∀n,m:nat. O < n → m ≤ n*m. -#n #m #H /2/ qed. +/2 width=1 by monotonic_le_times_r/ qed. theorem le_times_to_le: ∀a,n,m. O < a → a * n ≤ a * m → n ≤ m. #a @nat_elim2 normalize [// |#n #H1 #H2 - @(transitive_le ? (a*S n)) /2/ - |#n #m #H #lta #le - @le_S_S @H /2/ + @(transitive_le ? (a*S n)) /2 width=1 by monotonic_le_times_r/ + |#n #m #H #lta #le /4 width=2 by le_plus_to_le, le_S_S/ ] qed-. theorem le_plus_minus_m_m: ∀n,m:nat. n ≤ (n-m)+m. -#n (elim n) // #a #Hind #m (cases m) // normalize #n/2/ +#n elim n // #a #Hind #m cases m // normalize #n /2 width=1 by le_S_S/ qed. theorem le_plus_to_minus_r: ∀a,b,c. a + b ≤ c → a ≤ c -b. -#a #b #c #H @(le_plus_to_le_r … b) /2/ +#a #b #c #H @(le_plus_to_le_r … b) /2 width=3 by transitive_le/ qed. lemma lt_to_le: ∀x,y. x < y → x ≤ y. -/2 width=2/ qed. +/2 width=2 by le_plus_b/ qed. lemma inv_eq_minus_O: ∀x,y. x - y = 0 → x ≤ y. // qed-. @@ -319,84 +319,84 @@ qed. (* lt *) theorem transitive_lt: transitive nat lt. -#a #b #c #ltab #ltbc (elim ltbc) /2/ +#a #b #c #ltab #ltbc elim ltbc /2 width=1 by le_S/ qed. theorem lt_to_le_to_lt: ∀n,m,p:nat. n < m → m ≤ p → n < p. -#n #m #p #H #H1 (elim H1) /2/ qed. +#n #m #p #H #H1 elim H1 /2 width=3 by transitive_lt/ qed. theorem le_to_lt_to_lt: ∀n,m,p:nat. n ≤ m → m < p → n < p. -#n #m #p #H (elim H) /3/ qed. +#n #m #p #H elim H /3 width=3 by transitive_lt/ qed. theorem lt_S_to_lt: ∀n,m. S n < m → n < m. -/2/ qed. +/2 width=3 by transitive_lt/ qed. theorem ltn_to_ltO: ∀n,m:nat. n < m → 0 < m. -/2/ qed. +/2 width=3 by lt_to_le_to_lt/ qed. theorem lt_O_S : ∀n:nat. O < S n. -/2/ qed. +/2 width=1 by ltn_to_ltO/ qed. theorem monotonic_lt_plus_r: ∀n:nat.monotonic nat lt (λm.n+m). -/2/ qed. +/2 width=1 by monotonic_le_plus_r/ qed. theorem monotonic_lt_plus_l: ∀n:nat.monotonic nat lt (λm.m+n). -/2/ qed. +/2 width=1 by monotonic_le_plus_r/ qed. theorem lt_plus: ∀n,m,p,q:nat. n < m → p < q → n + p < m + q. #n #m #p #q #ltnm #ltpq -@(transitive_lt ? (n+q))/2/ qed. +@(transitive_lt ? (n+q)) /2 width=1 by monotonic_lt_plus_l, monotonic_le_plus_r/ qed. theorem lt_plus_to_lt_l :∀n,p,q:nat. p+n < q+n → p(plus_minus_m_m … Hlecb) /2/ +#a #b #c #Hlecb #H >(plus_minus_m_m … Hlecb) /2 width=1 by monotonic_le_plus_l/ qed. theorem le_plus_to_minus: ∀n,m,p. n ≤ p+m → n-m ≤ p. -#n #m #p #lep /2/ qed. +/2 width=1 by monotonic_le_minus_l/ qed. theorem monotonic_le_minus_r: ∀p,q,n:nat. q ≤ p → n-p ≤ n-q. #p #q #n #lepq @le_plus_to_minus -@(transitive_le … (le_plus_minus_m_m ? q)) /2/ +@(transitive_le … (le_plus_minus_m_m ? q)) /2 width=1 by monotonic_le_plus_r/ qed. theorem increasing_to_le: ∀f:nat → nat. increasing f → ∀m:nat.∃i.m ≤ f i. -#f #incr #m (elim m) /2/#n * #a #lenfa -@(ex_intro ?? (S a)) /2/ +#f #incr #m elim m /2 width=2 by ex_intro/ +#n * #a #lenfa +@(ex_intro ?? (S a)) /2 width=3 by le_to_lt_to_lt/ qed. -(* thus is le_plus -lemma le_plus_compatible: ∀x1,x2,y1,y2. x1 ≤ y1 → x2 ≤ y2 → x1 + x2 ≤ y1 + y2. -#x1 #y1 #x2 #y2 #H1 #H2 /2/ @le_plus // /2/ /3 by le_minus_to_plus, monotonic_le_plus_r, transitive_le/ qed. -*) - lemma minus_le: ∀x,y. x - y ≤ x. -/2 width=1/ qed. +/2 width=1 by monotonic_le_minus_l/ qed. (* lt *) theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n eq_minus_O [2:/2/] >eq_minus_O // - @monotonic_le_times_r /2/ + [>eq_minus_O [ >eq_minus_O // @monotonic_le_times_r ] + /2 width=1 by lt_to_le/ |@sym_eq (applyS plus_to_minus) eq_minus_O /2/ (* >eq_minus_O // *) + #H >eq_minus_O /2 width=1 by eq_minus_O, monotonic_le_minus_l/ (* >eq_minus_O // *) ] qed. @@ -748,19 +752,25 @@ theorem minus_minus: ∀n,m,p:nat. p ≤ m → m ≤ n → (plus_minus_m_m b c) in ⊢ (? ? ?%); // qed. lemma minus_minus_m_m: ∀m,n. n ≤ m → m - (m - n) = n. -/2 width=1/ qed. +/2 width=1 by minus_le_minus_minus_comm/ qed. lemma minus_plus_plus_l: ∀x,y,h. (x + h) - (y + h) = x - y. // qed. +lemma plus_minus_plus_plus_l: ∀z,x,y,h. z + (x + h) - (y + h) = z + x - y. +// qed. + (* Stilll more atomic conclusion ********************************************) (* le *) diff --git a/matita/matita/lib/lambda/background/notation.ma b/matita/matita/lib/lambda/background/notation.ma index 62b8b2dca..fdfffb346 100644 --- a/matita/matita/lib/lambda/background/notation.ma +++ b/matita/matita/lib/lambda/background/notation.ma @@ -37,14 +37,18 @@ notation "hvbox( { term 46 b } # break term 90 i )" non associative with precedence 46 for @{ 'VariableReferenceByIndex $b $i }. -notation "hvbox( 𝛌 . term 46 A )" +notation "hvbox( 𝛌 . term 46 A )" non associative with precedence 46 for @{ 'Abstraction $A }. -notation "hvbox( { term 46 b } 𝛌 . break term 46 T)" +notation "hvbox( { term 46 b } 𝛌 . break term 46 T)" non associative with precedence 46 for @{ 'Abstraction $b $T }. +notation "hvbox( 𝛌 term 46 d . break term 46 A )" + non associative with precedence 46 + for @{ 'AnnotatedAbstraction $d $A }. + notation "hvbox( @ term 46 C . break term 46 A )" non associative with precedence 46 for @{ 'Application $C $A }. diff --git a/matita/matita/lib/lambda/levels/interpretations.ma b/matita/matita/lib/lambda/levels/interpretations.ma new file mode 100644 index 000000000..0c06ab442 --- /dev/null +++ b/matita/matita/lib/lambda/levels/interpretations.ma @@ -0,0 +1,70 @@ +(**************************************************************************) +(* ___ *) +(* ||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/notation/functions/forward_1.ma". +include "lambda/notation/functions/forward_3.ma". +include "lambda/notation/functions/backward_1.ma". +include "lambda/notation/functions/backward_3.ma". +include "lambda/terms/iterated_abstraction.ma". +include "lambda/levels/term.ma". + +(* INTERPRETATIONS **********************************************************) + +let rec bylevel h d M on M ≝ match M with +[ VRef i ⇒ {h}§(tri … i d (d-i-1) i i) +| Abst A ⇒ bylevel (h+1) (d+1) A +| Appl C A ⇒ {h}@(bylevel 0 d C).(bylevel 0 d A) +]. + +interpretation "forward interpretation (term by depth) general" + 'Forward h d M = (bylevel h d M). + +interpretation "forward interpretation (term by depth)" + 'Forward M = (bylevel O O M). + +let rec bydepth h d M on M ≝ match M with +[ LVRef i e ⇒ 𝛌i.#(tri … e (d+i-h) (d+i-h-e-1) e e) +| LAppl i C A ⇒ 𝛌i.@(bydepth h (d+i) C).(bydepth h (d+i) A) +]. + +interpretation "backward interpretation (term by level) general" + 'Backward h d M = (bydepth h d M). + +interpretation "backward interpretation (term by level)" + 'Backward M = (bydepth O O M). + +theorem by_depth_level_gen: ∀M,e,d,h. d ≤ e + h → ⇓[e, e+h-d] ⇑[d, h] M = 𝛌h.M. +#M elim M -M normalize +[ #i #e #d #h #Hdeh >(minus_minus_m_m … Hdeh) + elim (lt_or_eq_or_gt i d) #Hid + [ >(tri_lt ???? … Hid) >(tri_lt ???? d (d-i-1)) + [ >minus_minus_associative /2 width=1 by monotonic_le_minus_r/ + minus_minus_associative /2 width=1 by lt_to_le/ + | /2 width=1 by monotonic_lt_minus_l/ + ] + | destruct >(tri_eq ???? …) >(tri_eq ???? …) // + | >(tri_gt ???? … Hid) >(tri_gt ???? … Hid) // + ] +| #A #IHA #e #d #h #Hdeh lapply (IHA e (d+1) (h+1) ?) -IHA + /2 width=1 by le_S_S, eq_f2/ +| #C #A #IHC #IHA #e #d #h #Hdeh + lapply (IHC (e+h) d 0 ?) -IHC + lapply (IHA (e+h) d 0 ?) -IHA + normalize /2 width=1 by/ +] +qed. + +lemma by_depth_level: ∀M. ⇓⇑M = M. +#M lapply (by_depth_level_gen M 0 0 0 ?) normalize // +qed. diff --git a/matita/matita/lib/lambda/levels/term.ma b/matita/matita/lib/lambda/levels/term.ma new file mode 100644 index 000000000..593e2b648 --- /dev/null +++ b/matita/matita/lib/lambda/levels/term.ma @@ -0,0 +1,37 @@ +(**************************************************************************) +(* ___ *) +(* ||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/background/preamble.ma". + +(* PER LEVEL TERM STRUCTURE *************************************************) + +(* Policy: term metavariables : A, B, C, D, M, N + relative level metavariables: i, j + absolute level metavariables: d, e +*) +(* Bote: first argument: relative level of the term *) +inductive lterm: Type[0] ≝ +| LVRef: nat → nat → lterm (* variable reference by level *) +| LAppl: nat → lterm → lterm → lterm (* function application *) +. + +interpretation "stratified term construction (variable reference by level)" + 'VariableReferenceByLevel i d = (LVRef i d). + +interpretation "stratified term construction (application)" + 'Application i C A = (LAppl i C A). + +notation "hvbox( { term 46 b } § break term 90 d )" + non associative with precedence 46 + for @{ 'VariableReferenceByLevel $b $d }. diff --git a/matita/matita/lib/lambda/notation/functions/backward_1.ma b/matita/matita/lib/lambda/notation/functions/backward_1.ma new file mode 100644 index 000000000..08ee2b3cd --- /dev/null +++ b/matita/matita/lib/lambda/notation/functions/backward_1.ma @@ -0,0 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +notation "hvbox( ⇓ term 46 M )" + non associative with precedence 46 + for @{ 'Backward $M }. diff --git a/matita/matita/lib/lambda/notation/functions/backward_3.ma b/matita/matita/lib/lambda/notation/functions/backward_3.ma new file mode 100644 index 000000000..bfdbfb8a6 --- /dev/null +++ b/matita/matita/lib/lambda/notation/functions/backward_3.ma @@ -0,0 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +notation "hvbox( ⇓ [ term 46 d , break term 46 h ] break term 46 M )" + non associative with precedence 46 + for @{ 'Backward $h $d $M }. diff --git a/matita/matita/lib/lambda/notation/functions/forward_1.ma b/matita/matita/lib/lambda/notation/functions/forward_1.ma new file mode 100644 index 000000000..32abbf60d --- /dev/null +++ b/matita/matita/lib/lambda/notation/functions/forward_1.ma @@ -0,0 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +notation "hvbox( ⇑ term 46 M )" + non associative with precedence 46 + for @{ 'Forward $M }. diff --git a/matita/matita/lib/lambda/notation/functions/forward_3.ma b/matita/matita/lib/lambda/notation/functions/forward_3.ma new file mode 100644 index 000000000..ba48d17eb --- /dev/null +++ b/matita/matita/lib/lambda/notation/functions/forward_3.ma @@ -0,0 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +notation "hvbox( ⇑ [ term 46 d, break term 46 h ] break term 46 M )" + non associative with precedence 46 + for @{ 'Forward $h $d $M }. diff --git a/matita/matita/lib/lambda/terms/iterated_abstraction.ma b/matita/matita/lib/lambda/terms/iterated_abstraction.ma new file mode 100644 index 000000000..78d150ba3 --- /dev/null +++ b/matita/matita/lib/lambda/terms/iterated_abstraction.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||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/terms/term.ma". + +(* GENERALIZED ABSTRACTION **************************************************) + +let rec abst d M on d ≝ match d with +[ O ⇒ M +| S e ⇒ 𝛌. (abst e M) +]. + +interpretation "iterated abstraction (term)" + 'AnnotatedAbstraction d M = (abst d M). + +lemma abst_plus: ∀A,m,n. 𝛌m+n.A = 𝛌m.𝛌n.A. +#A #m elim m -m normalize // +qed.