matita/contribs/LOGIC/Lift/defs.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15
  16
  17 (* PROOF RELOCATION
  18 *)
  19
  20 include "datatypes_defs/Proof.ma".
  21
  22 inductive Lift: Nat \to Nat \to Proof \to Proof \to Prop \def
  23    | lift_lref_lt: \forall jd,jh,i. i < jd \to Lift jd jh (lref i) (lref i)
  24    | lift_lref_ge: \forall jd,jh,i1,i2. jd <= i1 \to (i1 + jh == i2) \to
  25                    Lift jd jh (lref i1) (lref i2)
  26    | lift_prin   : \forall jd,jh,h. Lift jd jh (prin h) (prin h)
  27    | lift_impw   : \forall jd,jh,p1,p2.
  28                    Lift jd jh p1 p2 \to Lift jd jh (impw p1) (impw p2)
  29    | lift_impr   : \forall jd,jh,p1,p2.
  30                    Lift jd jh p1 p2 \to Lift jd jh (impr p1) (impr p2)
  31    | lift_impi   : \forall jd,jh,p1,p2. Lift jd jh p1 p2 \to
  32                    \forall q1,q2. Lift jd jh q1 q2 \to
  33                    \forall r1,r2. Lift (succ jd) jh r1 r2 \to
  34                    Lift jd jh (impi p1 q1 r1) (impi p2 q2 r2)
  35    | lift_scut   : \forall jd,jh,p1,p2. Lift jd jh p1 p2 \to
  36                    \forall q1,q2. Lift jd jh q1 q2 \to
  37                    Lift jd jh (scut p1 q1) (scut p2 q2)
  38 .