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