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