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 "basic_2/substitution/lift.ma".
17 (* BASIC TERM RELOCATION ****************************************************)
19 (* Properties on negated basic relocation ***********************************)
21 lemma nlift_lref_be_SO: ∀X,i. ⬆[i, 1] X ≡ #i → ⊥.
22 /2 width=7 by lift_inv_lref2_be/ qed-.
24 lemma nlift_bind_sn: ∀W,d,e. (∀V. ⬆[d, e] V ≡ W → ⊥) →
25 ∀a,I,U. (∀X. ⬆[d, e] X ≡ ⓑ{a,I}W.U → ⊥).
26 #W #d #e #HW #a #I #U #X #H elim (lift_inv_bind2 … H) -H /2 width=2 by/
29 lemma nlift_bind_dx: ∀U,d,e. (∀T. ⬆[d+1, e] T ≡ U → ⊥) →
30 ∀a,I,W. (∀X. ⬆[d, e] X ≡ ⓑ{a,I}W.U → ⊥).
31 #U #d #e #HU #a #I #W #X #H elim (lift_inv_bind2 … H) -H /2 width=2 by/
34 lemma nlift_flat_sn: ∀W,d,e. (∀V. ⬆[d, e] V ≡ W → ⊥) →
35 ∀I,U. (∀X. ⬆[d, e] X ≡ ⓕ{I}W.U → ⊥).
36 #W #d #e #HW #I #U #X #H elim (lift_inv_flat2 … H) -H /2 width=2 by/
39 lemma nlift_flat_dx: ∀U,d,e. (∀T. ⬆[d, e] T ≡ U → ⊥) →
40 ∀I,W. (∀X. ⬆[d, e] X ≡ ⓕ{I}W.U → ⊥).
41 #U #d #e #HU #I #W #X #H elim (lift_inv_flat2 … H) -H /2 width=2 by/
44 (* Inversion lemmas on negated basic relocation *****************************)
46 lemma nlift_inv_lref_be_SO: ∀i,j. (∀X. ⬆[i, 1] X ≡ #j → ⊥) → j = i.
47 #i #j elim (lt_or_eq_or_gt i j) // #Hij #H
48 [ elim (H (#(j-1))) -H /2 width=1 by lift_lref_ge_minus/
49 | elim (H (#j)) -H /2 width=1 by lift_lref_lt/
53 lemma nlift_inv_bind: ∀a,I,W,U,d,e. (∀X. ⬆[d, e] X ≡ ⓑ{a,I}W.U → ⊥) →
54 (∀V. ⬆[d, e] V ≡ W → ⊥) ∨ (∀T. ⬆[d+1, e] T ≡ U → ⊥).
55 #a #I #W #U #d #e #H elim (is_lift_dec W d e)
56 [ * /4 width=2 by lift_bind, or_intror/
57 | /4 width=2 by ex_intro, or_introl/
61 lemma nlift_inv_flat: ∀I,W,U,d,e. (∀X. ⬆[d, e] X ≡ ⓕ{I}W.U → ⊥) →
62 (∀V. ⬆[d, e] V ≡ W → ⊥) ∨ (∀T. ⬆[d, e] T ≡ U → ⊥).
63 #I #W #U #d #e #H elim (is_lift_dec W d e)
64 [ * /4 width=2 by lift_flat, or_intror/
65 | /4 width=2 by ex_intro, or_introl/