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