matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/dec.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
  18
  19 include "subst0/defs.ma".
  20
  21 include "lift/props.ma".
  22
  23 theorem dnf_dec2:
  24  \forall (t: T).(\forall (d: nat).(or (\forall (w: T).(ex T (\lambda (v:
  25 T).(subst0 d w t (lift (S O) d v))))) (ex T (\lambda (v: T).(eq T t (lift (S
  26 O) d v))))))
  27 \def
  28  \lambda (t: T).(T_ind (\lambda (t0: T).(\forall (d: nat).(or (\forall (w:
  29 T).(ex T (\lambda (v: T).(subst0 d w t0 (lift (S O) d v))))) (ex T (\lambda
  30 (v: T).(eq T t0 (lift (S O) d v))))))) (\lambda (n: nat).(\lambda (d:
  31 nat).(or_intror (\forall (w: T).(ex T (\lambda (v: T).(subst0 d w (TSort n)
  32 (lift (S O) d v))))) (ex T (\lambda (v: T).(eq T (TSort n) (lift (S O) d
  33 v)))) (ex_intro T (\lambda (v: T).(eq T (TSort n) (lift (S O) d v))) (TSort
  34 n) (eq_ind_r T (TSort n) (\lambda (t0: T).(eq T (TSort n) t0)) (refl_equal T
  35 (TSort n)) (lift (S O) d (TSort n)) (lift_sort n (S O) d)))))) (\lambda (n:
  36 nat).(\lambda (d: nat).(lt_eq_gt_e n d (or (\forall (w: T).(ex T (\lambda (v:
  37 T).(subst0 d w (TLRef n) (lift (S O) d v))))) (ex T (\lambda (v: T).(eq T
  38 (TLRef n) (lift (S O) d v))))) (\lambda (H: (lt n d)).(or_intror (\forall (w:
  39 T).(ex T (\lambda (v: T).(subst0 d w (TLRef n) (lift (S O) d v))))) (ex T
  40 (\lambda (v: T).(eq T (TLRef n) (lift (S O) d v)))) (ex_intro T (\lambda (v:
  41 T).(eq T (TLRef n) (lift (S O) d v))) (TLRef n) (eq_ind_r T (TLRef n)
  42 (\lambda (t0: T).(eq T (TLRef n) t0)) (refl_equal T (TLRef n)) (lift (S O) d
  43 (TLRef n)) (lift_lref_lt n (S O) d H))))) (\lambda (H: (eq nat n d)).(eq_ind
  44 nat n (\lambda (n0: nat).(or (\forall (w: T).(ex T (\lambda (v: T).(subst0 n0
  45 w (TLRef n) (lift (S O) n0 v))))) (ex T (\lambda (v: T).(eq T (TLRef n) (lift
  46 (S O) n0 v)))))) (or_introl (\forall (w: T).(ex T (\lambda (v: T).(subst0 n w
  47 (TLRef n) (lift (S O) n v))))) (ex T (\lambda (v: T).(eq T (TLRef n) (lift (S
  48 O) n v)))) (\lambda (w: T).(ex_intro T (\lambda (v: T).(subst0 n w (TLRef n)
  49 (lift (S O) n v))) (lift n O w) (eq_ind_r T (lift (plus (S O) n) O w)
  50 (\lambda (t0: T).(subst0 n w (TLRef n) t0)) (subst0_lref w n) (lift (S O) n
  51 (lift n O w)) (lift_free w n (S O) O n (le_n (plus O n)) (le_O_n n)))))) d
  52 H)) (\lambda (H: (lt d n)).(or_intror (\forall (w: T).(ex T (\lambda (v:
  53 T).(subst0 d w (TLRef n) (lift (S O) d v))))) (ex T (\lambda (v: T).(eq T
  54 (TLRef n) (lift (S O) d v)))) (ex_intro T (\lambda (v: T).(eq T (TLRef n)
  55 (lift (S O) d v))) (TLRef (pred n)) (eq_ind_r T (TLRef n) (\lambda (t0:
  56 T).(eq T (TLRef n) t0)) (refl_equal T (TLRef n)) (lift (S O) d (TLRef (pred
  57 n))) (lift_lref_gt d n H)))))))) (\lambda (k: K).(\lambda (t0: T).(\lambda
  58 (H: ((\forall (d: nat).(or (\forall (w: T).(ex T (\lambda (v: T).(subst0 d w
  59 t0 (lift (S O) d v))))) (ex T (\lambda (v: T).(eq T t0 (lift (S O) d
  60 v)))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (d: nat).(or (\forall (w:
  61 T).(ex T (\lambda (v: T).(subst0 d w t1 (lift (S O) d v))))) (ex T (\lambda
  62 (v: T).(eq T t1 (lift (S O) d v)))))))).(\lambda (d: nat).(let H_x \def (H d)
  63 in (let H1 \def H_x in (or_ind (\forall (w: T).(ex T (\lambda (v: T).(subst0
  64 d w t0 (lift (S O) d v))))) (ex T (\lambda (v: T).(eq T t0 (lift (S O) d
  65 v)))) (or (\forall (w: T).(ex T (\lambda (v: T).(subst0 d w (THead k t0 t1)
  66 (lift (S O) d v))))) (ex T (\lambda (v: T).(eq T (THead k t0 t1) (lift (S O)
  67 d v))))) (\lambda (H2: ((\forall (w: T).(ex T (\lambda (v: T).(subst0 d w t0
  68 (lift (S O) d v))))))).(let H_x0 \def (H0 (s k d)) in (let H3 \def H_x0 in
  69 (or_ind (\forall (w: T).(ex T (\lambda (v: T).(subst0 (s k d) w t1 (lift (S
  70 O) (s k d) v))))) (ex T (\lambda (v: T).(eq T t1 (lift (S O) (s k d) v))))
  71 (or (\forall (w: T).(ex T (\lambda (v: T).(subst0 d w (THead k t0 t1) (lift
  72 (S O) d v))))) (ex T (\lambda (v: T).(eq T (THead k t0 t1) (lift (S O) d
  73 v))))) (\lambda (H4: ((\forall (w: T).(ex T (\lambda (v: T).(subst0 (s k d) w
  74 t1 (lift (S O) (s k d) v))))))).(or_introl (\forall (w: T).(ex T (\lambda (v:
  75 T).(subst0 d w (THead k t0 t1) (lift (S O) d v))))) (ex T (\lambda (v: T).(eq
  76 T (THead k t0 t1) (lift (S O) d v)))) (\lambda (w: T).(let H_x1 \def (H4 w)
  77 in (let H5 \def H_x1 in (ex_ind T (\lambda (v: T).(subst0 (s k d) w t1 (lift
  78 (S O) (s k d) v))) (ex T (\lambda (v: T).(subst0 d w (THead k t0 t1) (lift (S
  79 O) d v)))) (\lambda (x: T).(\lambda (H6: (subst0 (s k d) w t1 (lift (S O) (s
  80 k d) x))).(let H_x2 \def (H2 w) in (let H7 \def H_x2 in (ex_ind T (\lambda
  81 (v: T).(subst0 d w t0 (lift (S O) d v))) (ex T (\lambda (v: T).(subst0 d w
  82 (THead k t0 t1) (lift (S O) d v)))) (\lambda (x0: T).(\lambda (H8: (subst0 d
  83 w t0 (lift (S O) d x0))).(ex_intro T (\lambda (v: T).(subst0 d w (THead k t0
  84 t1) (lift (S O) d v))) (THead k x0 x) (eq_ind_r T (THead k (lift (S O) d x0)
  85 (lift (S O) (s k d) x)) (\lambda (t2: T).(subst0 d w (THead k t0 t1) t2))
  86 (subst0_both w t0 (lift (S O) d x0) d H8 k t1 (lift (S O) (s k d) x) H6)
  87 (lift (S O) d (THead k x0 x)) (lift_head k x0 x (S O) d))))) H7))))) H5))))))
  88 (\lambda (H4: (ex T (\lambda (v: T).(eq T t1 (lift (S O) (s k d)
  89 v))))).(ex_ind T (\lambda (v: T).(eq T t1 (lift (S O) (s k d) v))) (or
  90 (\forall (w: T).(ex T (\lambda (v: T).(subst0 d w (THead k t0 t1) (lift (S O)
  91 d v))))) (ex T (\lambda (v: T).(eq T (THead k t0 t1) (lift (S O) d v)))))
  92 (\lambda (x: T).(\lambda (H5: (eq T t1 (lift (S O) (s k d) x))).(eq_ind_r T
  93 (lift (S O) (s k d) x) (\lambda (t2: T).(or (\forall (w: T).(ex T (\lambda
  94 (v: T).(subst0 d w (THead k t0 t2) (lift (S O) d v))))) (ex T (\lambda (v:
  95 T).(eq T (THead k t0 t2) (lift (S O) d v)))))) (or_introl (\forall (w: T).(ex
  96 T (\lambda (v: T).(subst0 d w (THead k t0 (lift (S O) (s k d) x)) (lift (S O)
  97 d v))))) (ex T (\lambda (v: T).(eq T (THead k t0 (lift (S O) (s k d) x))
  98 (lift (S O) d v)))) (\lambda (w: T).(let H_x1 \def (H2 w) in (let H6 \def
  99 H_x1 in (ex_ind T (\lambda (v: T).(subst0 d w t0 (lift (S O) d v))) (ex T
 100 (\lambda (v: T).(subst0 d w (THead k t0 (lift (S O) (s k d) x)) (lift (S O) d
 101 v)))) (\lambda (x0: T).(\lambda (H7: (subst0 d w t0 (lift (S O) d
 102 x0))).(ex_intro T (\lambda (v: T).(subst0 d w (THead k t0 (lift (S O) (s k d)
 103 x)) (lift (S O) d v))) (THead k x0 x) (eq_ind_r T (THead k (lift (S O) d x0)
 104 (lift (S O) (s k d) x)) (\lambda (t2: T).(subst0 d w (THead k t0 (lift (S O)
 105 (s k d) x)) t2)) (subst0_fst w (lift (S O) d x0) t0 d H7 (lift (S O) (s k d)
 106 x) k) (lift (S O) d (THead k x0 x)) (lift_head k x0 x (S O) d))))) H6))))) t1
 107 H5))) H4)) H3)))) (\lambda (H2: (ex T (\lambda (v: T).(eq T t0 (lift (S O) d
 108 v))))).(ex_ind T (\lambda (v: T).(eq T t0 (lift (S O) d v))) (or (\forall (w:
 109 T).(ex T (\lambda (v: T).(subst0 d w (THead k t0 t1) (lift (S O) d v))))) (ex
 110 T (\lambda (v: T).(eq T (THead k t0 t1) (lift (S O) d v))))) (\lambda (x:
 111 T).(\lambda (H3: (eq T t0 (lift (S O) d x))).(let H_x0 \def (H0 (s k d)) in
 112 (let H4 \def H_x0 in (or_ind (\forall (w: T).(ex T (\lambda (v: T).(subst0 (s
 113 k d) w t1 (lift (S O) (s k d) v))))) (ex T (\lambda (v: T).(eq T t1 (lift (S
 114 O) (s k d) v)))) (or (\forall (w: T).(ex T (\lambda (v: T).(subst0 d w (THead
 115 k t0 t1) (lift (S O) d v))))) (ex T (\lambda (v: T).(eq T (THead k t0 t1)
 116 (lift (S O) d v))))) (\lambda (H5: ((\forall (w: T).(ex T (\lambda (v:
 117 T).(subst0 (s k d) w t1 (lift (S O) (s k d) v))))))).(eq_ind_r T (lift (S O)
 118 d x) (\lambda (t2: T).(or (\forall (w: T).(ex T (\lambda (v: T).(subst0 d w
 119 (THead k t2 t1) (lift (S O) d v))))) (ex T (\lambda (v: T).(eq T (THead k t2
 120 t1) (lift (S O) d v)))))) (or_introl (\forall (w: T).(ex T (\lambda (v:
 121 T).(subst0 d w (THead k (lift (S O) d x) t1) (lift (S O) d v))))) (ex T
 122 (\lambda (v: T).(eq T (THead k (lift (S O) d x) t1) (lift (S O) d v))))
 123 (\lambda (w: T).(let H_x1 \def (H5 w) in (let H6 \def H_x1 in (ex_ind T
 124 (\lambda (v: T).(subst0 (s k d) w t1 (lift (S O) (s k d) v))) (ex T (\lambda
 125 (v: T).(subst0 d w (THead k (lift (S O) d x) t1) (lift (S O) d v)))) (\lambda
 126 (x0: T).(\lambda (H7: (subst0 (s k d) w t1 (lift (S O) (s k d)
 127 x0))).(ex_intro T (\lambda (v: T).(subst0 d w (THead k (lift (S O) d x) t1)
 128 (lift (S O) d v))) (THead k x x0) (eq_ind_r T (THead k (lift (S O) d x) (lift
 129 (S O) (s k d) x0)) (\lambda (t2: T).(subst0 d w (THead k (lift (S O) d x) t1)
 130 t2)) (subst0_snd k w (lift (S O) (s k d) x0) t1 d H7 (lift (S O) d x)) (lift
 131 (S O) d (THead k x x0)) (lift_head k x x0 (S O) d))))) H6))))) t0 H3))
 132 (\lambda (H5: (ex T (\lambda (v: T).(eq T t1 (lift (S O) (s k d)
 133 v))))).(ex_ind T (\lambda (v: T).(eq T t1 (lift (S O) (s k d) v))) (or
 134 (\forall (w: T).(ex T (\lambda (v: T).(subst0 d w (THead k t0 t1) (lift (S O)
 135 d v))))) (ex T (\lambda (v: T).(eq T (THead k t0 t1) (lift (S O) d v)))))
 136 (\lambda (x0: T).(\lambda (H6: (eq T t1 (lift (S O) (s k d) x0))).(eq_ind_r T
 137 (lift (S O) (s k d) x0) (\lambda (t2: T).(or (\forall (w: T).(ex T (\lambda
 138 (v: T).(subst0 d w (THead k t0 t2) (lift (S O) d v))))) (ex T (\lambda (v:
 139 T).(eq T (THead k t0 t2) (lift (S O) d v)))))) (eq_ind_r T (lift (S O) d x)
 140 (\lambda (t2: T).(or (\forall (w: T).(ex T (\lambda (v: T).(subst0 d w (THead
 141 k t2 (lift (S O) (s k d) x0)) (lift (S O) d v))))) (ex T (\lambda (v: T).(eq
 142 T (THead k t2 (lift (S O) (s k d) x0)) (lift (S O) d v)))))) (or_intror
 143 (\forall (w: T).(ex T (\lambda (v: T).(subst0 d w (THead k (lift (S O) d x)
 144 (lift (S O) (s k d) x0)) (lift (S O) d v))))) (ex T (\lambda (v: T).(eq T
 145 (THead k (lift (S O) d x) (lift (S O) (s k d) x0)) (lift (S O) d v))))
 146 (ex_intro T (\lambda (v: T).(eq T (THead k (lift (S O) d x) (lift (S O) (s k
 147 d) x0)) (lift (S O) d v))) (THead k x x0) (eq_ind_r T (THead k (lift (S O) d
 148 x) (lift (S O) (s k d) x0)) (\lambda (t2: T).(eq T (THead k (lift (S O) d x)
 149 (lift (S O) (s k d) x0)) t2)) (refl_equal T (THead k (lift (S O) d x) (lift
 150 (S O) (s k d) x0))) (lift (S O) d (THead k x x0)) (lift_head k x x0 (S O)
 151 d)))) t0 H3) t1 H6))) H5)) H4))))) H2)) H1))))))))) t).
 152
 153 theorem dnf_dec:
 154  \forall (w: T).(\forall (t: T).(\forall (d: nat).(ex T (\lambda (v: T).(or
 155 (subst0 d w t (lift (S O) d v)) (eq T t (lift (S O) d v)))))))
 156 \def
 157  \lambda (w: T).(\lambda (t: T).(\lambda (d: nat).(let H_x \def (dnf_dec2 t
 158 d) in (let H \def H_x in (or_ind (\forall (w0: T).(ex T (\lambda (v:
 159 T).(subst0 d w0 t (lift (S O) d v))))) (ex T (\lambda (v: T).(eq T t (lift (S
 160 O) d v)))) (ex T (\lambda (v: T).(or (subst0 d w t (lift (S O) d v)) (eq T t
 161 (lift (S O) d v))))) (\lambda (H0: ((\forall (w0: T).(ex T (\lambda (v:
 162 T).(subst0 d w0 t (lift (S O) d v))))))).(let H_x0 \def (H0 w) in (let H1
 163 \def H_x0 in (ex_ind T (\lambda (v: T).(subst0 d w t (lift (S O) d v))) (ex T
 164 (\lambda (v: T).(or (subst0 d w t (lift (S O) d v)) (eq T t (lift (S O) d
 165 v))))) (\lambda (x: T).(\lambda (H2: (subst0 d w t (lift (S O) d
 166 x))).(ex_intro T (\lambda (v: T).(or (subst0 d w t (lift (S O) d v)) (eq T t
 167 (lift (S O) d v)))) x (or_introl (subst0 d w t (lift (S O) d x)) (eq T t
 168 (lift (S O) d x)) H2)))) H1)))) (\lambda (H0: (ex T (\lambda (v: T).(eq T t
 169 (lift (S O) d v))))).(ex_ind T (\lambda (v: T).(eq T t (lift (S O) d v))) (ex
 170 T (\lambda (v: T).(or (subst0 d w t (lift (S O) d v)) (eq T t (lift (S O) d
 171 v))))) (\lambda (x: T).(\lambda (H1: (eq T t (lift (S O) d x))).(eq_ind_r T
 172 (lift (S O) d x) (\lambda (t0: T).(ex T (\lambda (v: T).(or (subst0 d w t0
 173 (lift (S O) d v)) (eq T t0 (lift (S O) d v)))))) (ex_intro T (\lambda (v:
 174 T).(or (subst0 d w (lift (S O) d x) (lift (S O) d v)) (eq T (lift (S O) d x)
 175 (lift (S O) d v)))) x (or_intror (subst0 d w (lift (S O) d x) (lift (S O) d
 176 x)) (eq T (lift (S O) d x) (lift (S O) d x)) (refl_equal T (lift (S O) d
 177 x)))) t H1))) H0)) H))))).
 178