1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "lambda/terms/relocating_substitution.ma".
16 include "lambda/subterms/relocating_substitution.ma".
18 include "lambda/notation/functions/projectdown_1.ma".
20 include "lambda/xoa/ex_2_2.ma".
22 (* CARRIER (UNDERLYING TERM) ************************************************)
24 let rec carrier F on F ≝ match F with
26 | SAbst _ T ⇒ 𝛌.(carrier T)
27 | SAppl _ V T ⇒ @(carrier V).(carrier T)
30 interpretation "carrier (subterms)"
31 'ProjectDown F = (carrier F).
33 lemma carrier_inv_vref: ∀j,F. ⇓F = #j → ∃b. F = {b}#j.
35 [ #b #i #H destruct /2 width=2/
37 | #b #V #T #H destruct
41 lemma carrier_inv_abst: ∀C,F. ⇓F = 𝛌.C → ∃∃b,U. ⇓U = C & F = {b}𝛌.U.
44 | #b #T #H destruct /2 width=4/
45 | #b #V #T #H destruct
49 lemma carrier_inv_appl: ∀D,C,F. ⇓F = @D.C →
50 ∃∃b,W,U. ⇓W = D & ⇓U = C & F = {b}@W.U.
54 | #b #V #T #H destruct /2 width=6/
58 lemma carrier_lift: ∀h,F,d. ⇓ ↑[d, h] F = ↑[d, h] ⇓F.
59 #h #F elim F -F normalize //
62 lemma carrier_dsubst: ∀G,F,d. ⇓ [d ↙ G] F = [d ↙ ⇓G] ⇓F.
63 #G #F elim F -F [2,3: normalize // ]
64 #b #i #d elim (lt_or_eq_or_gt i d) #Hid
65 [ >(sdsubst_vref_lt … Hid) >(dsubst_vref_lt … Hid) //
66 | destruct normalize //
67 | >(sdsubst_vref_gt … Hid) >(dsubst_vref_gt … Hid) //