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/Lift/defs".
18 - Usage: invoke with positive polarity
21 include "logic/equality.ma".
22 include "../../RELATIONAL/NPlus/defs.ma".
23 include "../../RELATIONAL/NLE/defs.ma".
24 include "../../RELATIONAL/BEq/defs.ma".
27 include "Inc/defs.ma".
29 inductive Lift (l: Nat): Nat \to Bool \to P \to P \to Prop \def
30 | lift_sort : \forall i,a,h. Lift l i a (sort h) (sort h)
31 | lift_lref_neg: \forall i,j. Lift l i false (lref j) (lref j)
32 | lift_lref_lt : \forall i,j.
33 j < i \to Lift l i true (lref j) (lref j)
34 | lift_lref_ge : \forall i,j1,j2.
35 i <= j1 \to (j1 + l == j2) \to
36 Lift l i true (lref j1) (lref j2)
37 | lift_head : \forall i,i',a,b,a',z,q1,q2,p1,p2.
38 (a * b == a') \to Inc i a' z i' \to
39 Lift l i a' q1 q2 \to Lift l i' a p1 p2 \to
40 Lift l i a (head b z q1 p1) (head b z q2 p2)