helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift1/fwd.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 (* This file was automatically generated: do not edit *********************)
  16
  17 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/lift1/fwd".
  18
  19 include "lift1/defs.ma".
  20
  21 include "lift/fwd.ma".
  22
  23 theorem lift1_lref:
  24  \forall (hds: PList).(\forall (i: nat).(eq T (lift1 hds (TLRef i)) (TLRef
  25 (trans hds i))))
  26 \def
  27  \lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall (i: nat).(eq T
  28 (lift1 p (TLRef i)) (TLRef (trans p i))))) (\lambda (i: nat).(refl_equal T
  29 (TLRef (trans PNil i)))) (\lambda (h: nat).(\lambda (d: nat).(\lambda (p:
  30 PList).(\lambda (H: ((\forall (i: nat).(eq T (lift1 p (TLRef i)) (TLRef
  31 (trans p i)))))).(\lambda (i: nat).(eq_ind_r T (TLRef (trans p i)) (\lambda
  32 (t: T).(eq T (lift h d t) (TLRef (match (blt (trans p i) d) with [true
  33 \Rightarrow (trans p i) | false \Rightarrow (plus (trans p i) h)]))))
  34 (refl_equal T (TLRef (match (blt (trans p i) d) with [true \Rightarrow (trans
  35 p i) | false \Rightarrow (plus (trans p i) h)]))) (lift1 p (TLRef i)) (H
  36 i))))))) hds).
  37
  38 theorem lift1_bind:
  39  \forall (b: B).(\forall (hds: PList).(\forall (u: T).(\forall (t: T).(eq T
  40 (lift1 hds (THead (Bind b) u t)) (THead (Bind b) (lift1 hds u) (lift1 (Ss
  41 hds) t))))))
  42 \def
  43  \lambda (b: B).(\lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall
  44 (u: T).(\forall (t: T).(eq T (lift1 p (THead (Bind b) u t)) (THead (Bind b)
  45 (lift1 p u) (lift1 (Ss p) t)))))) (\lambda (u: T).(\lambda (t: T).(refl_equal
  46 T (THead (Bind b) (lift1 PNil u) (lift1 (Ss PNil) t))))) (\lambda (h:
  47 nat).(\lambda (d: nat).(\lambda (p: PList).(\lambda (H: ((\forall (u:
  48 T).(\forall (t: T).(eq T (lift1 p (THead (Bind b) u t)) (THead (Bind b)
  49 (lift1 p u) (lift1 (Ss p) t))))))).(\lambda (u: T).(\lambda (t: T).(eq_ind_r
  50 T (THead (Bind b) (lift1 p u) (lift1 (Ss p) t)) (\lambda (t0: T).(eq T (lift
  51 h d t0) (THead (Bind b) (lift h d (lift1 p u)) (lift h (S d) (lift1 (Ss p)
  52 t))))) (eq_ind_r T (THead (Bind b) (lift h d (lift1 p u)) (lift h (S d)
  53 (lift1 (Ss p) t))) (\lambda (t0: T).(eq T t0 (THead (Bind b) (lift h d (lift1
  54 p u)) (lift h (S d) (lift1 (Ss p) t))))) (refl_equal T (THead (Bind b) (lift
  55 h d (lift1 p u)) (lift h (S d) (lift1 (Ss p) t)))) (lift h d (THead (Bind b)
  56 (lift1 p u) (lift1 (Ss p) t))) (lift_bind b (lift1 p u) (lift1 (Ss p) t) h
  57 d)) (lift1 p (THead (Bind b) u t)) (H u t)))))))) hds)).
  58
  59 theorem lift1_flat:
  60  \forall (f: F).(\forall (hds: PList).(\forall (u: T).(\forall (t: T).(eq T
  61 (lift1 hds (THead (Flat f) u t)) (THead (Flat f) (lift1 hds u) (lift1 hds
  62 t))))))
  63 \def
  64  \lambda (f: F).(\lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall
  65 (u: T).(\forall (t: T).(eq T (lift1 p (THead (Flat f) u t)) (THead (Flat f)
  66 (lift1 p u) (lift1 p t)))))) (\lambda (u: T).(\lambda (t: T).(refl_equal T
  67 (THead (Flat f) (lift1 PNil u) (lift1 PNil t))))) (\lambda (h: nat).(\lambda
  68 (d: nat).(\lambda (p: PList).(\lambda (H: ((\forall (u: T).(\forall (t:
  69 T).(eq T (lift1 p (THead (Flat f) u t)) (THead (Flat f) (lift1 p u) (lift1 p
  70 t))))))).(\lambda (u: T).(\lambda (t: T).(eq_ind_r T (THead (Flat f) (lift1 p
  71 u) (lift1 p t)) (\lambda (t0: T).(eq T (lift h d t0) (THead (Flat f) (lift h
  72 d (lift1 p u)) (lift h d (lift1 p t))))) (eq_ind_r T (THead (Flat f) (lift h
  73 d (lift1 p u)) (lift h d (lift1 p t))) (\lambda (t0: T).(eq T t0 (THead (Flat
  74 f) (lift h d (lift1 p u)) (lift h d (lift1 p t))))) (refl_equal T (THead
  75 (Flat f) (lift h d (lift1 p u)) (lift h d (lift1 p t)))) (lift h d (THead
  76 (Flat f) (lift1 p u) (lift1 p t))) (lift_flat f (lift1 p u) (lift1 p t) h d))
  77 (lift1 p (THead (Flat f) u t)) (H u t)))))))) hds)).
  78
  79 theorem lift1_cons_tail:
  80  \forall (t: T).(\forall (h: nat).(\forall (d: nat).(\forall (hds: PList).(eq
  81 T (lift1 (PConsTail hds h d) t) (lift1 hds (lift h d t))))))
  82 \def
  83  \lambda (t: T).(\lambda (h: nat).(\lambda (d: nat).(\lambda (hds:
  84 PList).(PList_ind (\lambda (p: PList).(eq T (lift1 (PConsTail p h d) t)
  85 (lift1 p (lift h d t)))) (refl_equal T (lift h d t)) (\lambda (n:
  86 nat).(\lambda (n0: nat).(\lambda (p: PList).(\lambda (H: (eq T (lift1
  87 (PConsTail p h d) t) (lift1 p (lift h d t)))).(eq_ind_r T (lift1 p (lift h d
  88 t)) (\lambda (t0: T).(eq T (lift n n0 t0) (lift n n0 (lift1 p (lift h d
  89 t))))) (refl_equal T (lift n n0 (lift1 p (lift h d t)))) (lift1 (PConsTail p
  90 h d) t) H))))) hds)))).
  91
  92 theorem lifts1_flat:
  93  \forall (f: F).(\forall (hds: PList).(\forall (t: T).(\forall (ts:
  94 TList).(eq T (lift1 hds (THeads (Flat f) ts t)) (THeads (Flat f) (lifts1 hds
  95 ts) (lift1 hds t))))))
  96 \def
  97  \lambda (f: F).(\lambda (hds: PList).(\lambda (t: T).(\lambda (ts:
  98 TList).(TList_ind (\lambda (t0: TList).(eq T (lift1 hds (THeads (Flat f) t0
  99 t)) (THeads (Flat f) (lifts1 hds t0) (lift1 hds t)))) (refl_equal T (lift1
 100 hds t)) (\lambda (t0: T).(\lambda (t1: TList).(\lambda (H: (eq T (lift1 hds
 101 (THeads (Flat f) t1 t)) (THeads (Flat f) (lifts1 hds t1) (lift1 hds
 102 t)))).(eq_ind_r T (THead (Flat f) (lift1 hds t0) (lift1 hds (THeads (Flat f)
 103 t1 t))) (\lambda (t2: T).(eq T t2 (THead (Flat f) (lift1 hds t0) (THeads
 104 (Flat f) (lifts1 hds t1) (lift1 hds t))))) (eq_ind_r T (THeads (Flat f)
 105 (lifts1 hds t1) (lift1 hds t)) (\lambda (t2: T).(eq T (THead (Flat f) (lift1
 106 hds t0) t2) (THead (Flat f) (lift1 hds t0) (THeads (Flat f) (lifts1 hds t1)
 107 (lift1 hds t))))) (refl_equal T (THead (Flat f) (lift1 hds t0) (THeads (Flat
 108 f) (lifts1 hds t1) (lift1 hds t)))) (lift1 hds (THeads (Flat f) t1 t)) H)
 109 (lift1 hds (THead (Flat f) t0 (THeads (Flat f) t1 t))) (lift1_flat f hds t0
 110 (THeads (Flat f) t1 t)))))) ts)))).
 111
 112 theorem lifts1_nil:
 113  \forall (ts: TList).(eq TList (lifts1 PNil ts) ts)
 114 \def
 115  \lambda (ts: TList).(TList_ind (\lambda (t: TList).(eq TList (lifts1 PNil t)
 116 t)) (refl_equal TList TNil) (\lambda (t: T).(\lambda (t0: TList).(\lambda (H:
 117 (eq TList (lifts1 PNil t0) t0)).(eq_ind_r TList t0 (\lambda (t1: TList).(eq
 118 TList (TCons t t1) (TCons t t0))) (refl_equal TList (TCons t t0)) (lifts1
 119 PNil t0) H)))) ts).
 120
 121 theorem lifts1_cons:
 122  \forall (h: nat).(\forall (d: nat).(\forall (hds: PList).(\forall (ts:
 123 TList).(eq TList (lifts1 (PCons h d hds) ts) (lifts h d (lifts1 hds ts))))))
 124 \def
 125  \lambda (h: nat).(\lambda (d: nat).(\lambda (hds: PList).(\lambda (ts:
 126 TList).(TList_ind (\lambda (t: TList).(eq TList (lifts1 (PCons h d hds) t)
 127 (lifts h d (lifts1 hds t)))) (refl_equal TList TNil) (\lambda (t: T).(\lambda
 128 (t0: TList).(\lambda (H: (eq TList (lifts1 (PCons h d hds) t0) (lifts h d
 129 (lifts1 hds t0)))).(eq_ind_r TList (lifts h d (lifts1 hds t0)) (\lambda (t1:
 130 TList).(eq TList (TCons (lift h d (lift1 hds t)) t1) (TCons (lift h d (lift1
 131 hds t)) (lifts h d (lifts1 hds t0))))) (refl_equal TList (TCons (lift h d
 132 (lift1 hds t)) (lifts h d (lifts1 hds t0)))) (lifts1 (PCons h d hds) t0)
 133 H)))) ts)))).
 134