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 set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified/SUB/Lift/defs".
18 - Usage: invoke with positive polarity
21 include "SUB/Switch/defs.ma".
22 include "SUB/Inc/defs.ma".
24 inductive Lift: Bool \to Nat \to Nat \to Term \to Term \to Prop \def
25 | lift_sort : \forall l,q,i,h.
26 Lift q l i (leaf (sort h)) (leaf (sort h))
27 | lift_skip : \forall l,i,j.
28 Lift false l i (leaf (lref j)) (leaf (lref j))
29 | lift_lref_lt: \forall l,i,j. j < i \to
30 Lift true l i (leaf (lref j)) (leaf (lref j))
31 | lift_lref_ge: \forall l,i,j1. i <= j1 \to
32 \forall j2. (j1 + l == j2) \to
33 Lift true l i (leaf (lref j1)) (leaf (lref j2))
34 | lift_head : \forall l,qt,qu,z. Switch qt z qu \to
35 \forall iu,it. Inc qt iu z it \to
36 \forall u1,u2. Lift qu l iu u1 u2 \to
37 \forall t1,t2. Lift qt l it t1 t2 \to
38 Lift qt l iu (head z u1 t1) (head z u2 t2)