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/relocation/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_bind: ∀a,I,W,U,d,e. (∀X. ⇧[d, e] X ≡ ⓑ{a,I}W.U → ⊥) →
47 (∀V. ⇧[d, e] V ≡ W → ⊥) ∨ (∀T. ⇧[d+1, e] T ≡ U → ⊥).
48 #a #I #W #U #d #e #H elim (is_lift_dec W d e)
49 [ * /4 width=2 by lift_bind, or_intror/
50 | /4 width=2 by ex_intro, or_introl/
54 lemma nlift_inv_flat: ∀I,W,U,d,e. (∀X. ⇧[d, e] X ≡ ⓕ{I}W.U → ⊥) →
55 (∀V. ⇧[d, e] V ≡ W → ⊥) ∨ (∀T. ⇧[d, e] T ≡ U → ⊥).
56 #I #W #U #d #e #H elim (is_lift_dec W d e)
57 [ * /4 width=2 by lift_flat, or_intror/
58 | /4 width=2 by ex_intro, or_introl/