(**************************************************************************)
(*       ___                                                              *)
(*      ||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 "basic_2/substitution/lift.ma".

(* BASIC TERM RELOCATION ****************************************************)

(* Properties on negated basic relocation ***********************************)

lemma nlift_lref_be_SO: ∀X,j. j < ∞ → ⬆[j, 1] X ≡ #j → ⊥.
#X #j #Hj #H elim (lift_inv_lref2 … H) -H *
[ #H elim (ylt_yle_false … H) -H //
| #i #Hij #_ #H1 #H2 destruct
  elim (ylt_inv_plus_Y … Hj) -Hj #Hi #_
  elim (ylt_yle_false … Hij) -Hij /2 width=1 by monotonic_ylt_plus_sn/
]
qed-.

lemma nlift_bind_sn: ∀W,l,m. (∀V. ⬆[l, m] V ≡ W → ⊥) →
                     ∀a,I,U. (∀X. ⬆[l, m] X ≡ ⓑ{a,I}W.U → ⊥).
#W #l #m #HW #a #I #U #X #H elim (lift_inv_bind2 … H) -H /2 width=2 by/
qed-.

lemma nlift_bind_dx: ∀U,l,m. (∀T. ⬆[⫯l, m] T ≡ U → ⊥) →
                     ∀a,I,W. (∀X. ⬆[l, m] X ≡ ⓑ{a,I}W.U → ⊥).
#U #l #m #HU #a #I #W #X #H elim (lift_inv_bind2 … H) -H /2 width=2 by/
qed-.

lemma nlift_flat_sn: ∀W,l,m. (∀V. ⬆[l, m] V ≡ W → ⊥) →
                     ∀I,U. (∀X. ⬆[l, m] X ≡ ⓕ{I}W.U → ⊥).
#W #l #m #HW #I #U #X #H elim (lift_inv_flat2 … H) -H /2 width=2 by/
qed-.

lemma nlift_flat_dx: ∀U,l,m. (∀T. ⬆[l, m] T ≡ U → ⊥) →
                     ∀I,W. (∀X. ⬆[l, m] X ≡ ⓕ{I}W.U → ⊥).
#U #l #m #HU #I #W #X #H elim (lift_inv_flat2 … H) -H /2 width=2 by/
qed-.

(* Inversion lemmas on negated basic relocation *****************************)

lemma nlift_inv_lref_be_SO: ∀i,j. (∀X. ⬆[i, 1] X ≡ #j → ⊥) → j = i ∧ j < ∞.
#i #j elim (ylt_split_eq i j) #Hij #H destruct 
[ elim (H (#⫰j)) -H /2 width=1 by lift_lref_pred/
| elim (yle_split_eq i (∞)) /2 width=1 by conj/ #H0 destruct
  elim (H (#∞)) -H /2 width=1 by lift_lref_plus, ylt_Y/
| elim (H (#j)) -H /2 width=1 by lift_lref_lt/
]
qed-.

lemma nlift_inv_bind: ∀a,I,W,U,l,m. (∀X. ⬆[l, m] X ≡ ⓑ{a,I}W.U → ⊥) →
                      (∀V. ⬆[l, m] V ≡ W → ⊥) ∨ (∀T. ⬆[⫯l, m] T ≡ U → ⊥).
#a #I #W #U #l #m #H elim (is_lift_dec W l m)
[ * /4 width=2 by lift_bind, or_intror/
| /4 width=2 by ex_intro, or_introl/
]
qed-.

lemma nlift_inv_flat: ∀I,W,U,l,m. (∀X. ⬆[l, m] X ≡ ⓕ{I}W.U → ⊥) →
                      (∀V. ⬆[l, m] V ≡ W → ⊥) ∨ (∀T. ⬆[l, m] T ≡ U → ⊥).
#I #W #U #l #m #H elim (is_lift_dec W l m)
[ * /4 width=2 by lift_flat, or_intror/
| /4 width=2 by ex_intro, or_introl/
]
qed-.