matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/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 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/dec".
  18
  19 include "subst0/defs.ma".
  20
  21 include "lift/props.ma".
  22
  23 theorem dnf_dec:
  24  \forall (w: T).(\forall (t: T).(\forall (d: nat).(ex T (\lambda (v: T).(or
  25 (subst0 d w t (lift (S O) d v)) (eq T t (lift (S O) d v)))))))
  26 \def
  27  \lambda (w: T).(\lambda (t: T).(T_ind (\lambda (t0: T).(\forall (d: nat).(ex
  28 T (\lambda (v: T).(or (subst0 d w t0 (lift (S O) d v)) (eq T t0 (lift (S O) d
  29 v))))))) (\lambda (n: nat).(\lambda (d: nat).(ex_intro T (\lambda (v: T).(or
  30 (subst0 d w (TSort n) (lift (S O) d v)) (eq T (TSort n) (lift (S O) d v))))
  31 (TSort n) (eq_ind_r T (TSort n) (\lambda (t0: T).(or (subst0 d w (TSort n)
  32 t0) (eq T (TSort n) t0))) (or_intror (subst0 d w (TSort n) (TSort n)) (eq T
  33 (TSort n) (TSort n)) (refl_equal T (TSort n))) (lift (S O) d (TSort n))
  34 (lift_sort n (S O) d))))) (\lambda (n: nat).(\lambda (d: nat).(lt_eq_gt_e n d
  35 (ex T (\lambda (v: T).(or (subst0 d w (TLRef n) (lift (S O) d v)) (eq T
  36 (TLRef n) (lift (S O) d v))))) (\lambda (H: (lt n d)).(ex_intro T (\lambda
  37 (v: T).(or (subst0 d w (TLRef n) (lift (S O) d v)) (eq T (TLRef n) (lift (S
  38 O) d v)))) (TLRef n) (eq_ind_r T (TLRef n) (\lambda (t0: T).(or (subst0 d w
  39 (TLRef n) t0) (eq T (TLRef n) t0))) (or_intror (subst0 d w (TLRef n) (TLRef
  40 n)) (eq T (TLRef n) (TLRef n)) (refl_equal T (TLRef n))) (lift (S O) d (TLRef
  41 n)) (lift_lref_lt n (S O) d H)))) (\lambda (H: (eq nat n d)).(eq_ind nat n
  42 (\lambda (n0: nat).(ex T (\lambda (v: T).(or (subst0 n0 w (TLRef n) (lift (S
  43 O) n0 v)) (eq T (TLRef n) (lift (S O) n0 v)))))) (ex_intro T (\lambda (v:
  44 T).(or (subst0 n w (TLRef n) (lift (S O) n v)) (eq T (TLRef n) (lift (S O) n
  45 v)))) (lift n O w) (eq_ind_r T (lift (plus (S O) n) O w) (\lambda (t0: T).(or
  46 (subst0 n w (TLRef n) t0) (eq T (TLRef n) t0))) (or_introl (subst0 n w (TLRef
  47 n) (lift (S n) O w)) (eq T (TLRef n) (lift (S n) O w)) (subst0_lref w n))
  48 (lift (S O) n (lift n O w)) (lift_free w n (S O) O n (le_n (plus O n))
  49 (le_O_n n)))) d H)) (\lambda (H: (lt d n)).(ex_intro T (\lambda (v: T).(or
  50 (subst0 d w (TLRef n) (lift (S O) d v)) (eq T (TLRef n) (lift (S O) d v))))
  51 (TLRef (pred n)) (eq_ind_r T (TLRef n) (\lambda (t0: T).(or (subst0 d w
  52 (TLRef n) t0) (eq T (TLRef n) t0))) (or_intror (subst0 d w (TLRef n) (TLRef
  53 n)) (eq T (TLRef n) (TLRef n)) (refl_equal T (TLRef n))) (lift (S O) d (TLRef
  54 (pred n))) (lift_lref_gt d n H))))))) (\lambda (k: K).(\lambda (t0:
  55 T).(\lambda (H: ((\forall (d: nat).(ex T (\lambda (v: T).(or (subst0 d w t0
  56 (lift (S O) d v)) (eq T t0 (lift (S O) d v)))))))).(\lambda (t1: T).(\lambda
  57 (H0: ((\forall (d: nat).(ex T (\lambda (v: T).(or (subst0 d w t1 (lift (S O)
  58 d v)) (eq T t1 (lift (S O) d v)))))))).(\lambda (d: nat).(let H_x \def (H d)
  59 in (let H1 \def H_x in (ex_ind T (\lambda (v: T).(or (subst0 d w t0 (lift (S
  60 O) d v)) (eq T t0 (lift (S O) d v)))) (ex T (\lambda (v: T).(or (subst0 d w
  61 (THead k t0 t1) (lift (S O) d v)) (eq T (THead k t0 t1) (lift (S O) d v)))))
  62 (\lambda (x: T).(\lambda (H2: (or (subst0 d w t0 (lift (S O) d x)) (eq T t0
  63 (lift (S O) d x)))).(or_ind (subst0 d w t0 (lift (S O) d x)) (eq T t0 (lift
  64 (S O) d x)) (ex T (\lambda (v: T).(or (subst0 d w (THead k t0 t1) (lift (S O)
  65 d v)) (eq T (THead k t0 t1) (lift (S O) d v))))) (\lambda (H3: (subst0 d w t0
  66 (lift (S O) d x))).(let H_x0 \def (H0 (s k d)) in (let H4 \def H_x0 in
  67 (ex_ind T (\lambda (v: T).(or (subst0 (s k d) w t1 (lift (S O) (s k d) v))
  68 (eq T t1 (lift (S O) (s k d) v)))) (ex T (\lambda (v: T).(or (subst0 d w
  69 (THead k t0 t1) (lift (S O) d v)) (eq T (THead k t0 t1) (lift (S O) d v)))))
  70 (\lambda (x0: T).(\lambda (H5: (or (subst0 (s k d) w t1 (lift (S O) (s k d)
  71 x0)) (eq T t1 (lift (S O) (s k d) x0)))).(or_ind (subst0 (s k d) w t1 (lift
  72 (S O) (s k d) x0)) (eq T t1 (lift (S O) (s k d) x0)) (ex T (\lambda (v:
  73 T).(or (subst0 d w (THead k t0 t1) (lift (S O) d v)) (eq T (THead k t0 t1)
  74 (lift (S O) d v))))) (\lambda (H6: (subst0 (s k d) w t1 (lift (S O) (s k d)
  75 x0))).(ex_intro T (\lambda (v: T).(or (subst0 d w (THead k t0 t1) (lift (S O)
  76 d v)) (eq T (THead k t0 t1) (lift (S O) d v)))) (THead k x x0) (eq_ind_r T
  77 (THead k (lift (S O) d x) (lift (S O) (s k d) x0)) (\lambda (t2: T).(or
  78 (subst0 d w (THead k t0 t1) t2) (eq T (THead k t0 t1) t2))) (or_introl
  79 (subst0 d w (THead k t0 t1) (THead k (lift (S O) d x) (lift (S O) (s k d)
  80 x0))) (eq T (THead k t0 t1) (THead k (lift (S O) d x) (lift (S O) (s k d)
  81 x0))) (subst0_both w t0 (lift (S O) d x) d H3 k t1 (lift (S O) (s k d) x0)
  82 H6)) (lift (S O) d (THead k x x0)) (lift_head k x x0 (S O) d)))) (\lambda
  83 (H6: (eq T t1 (lift (S O) (s k d) x0))).(eq_ind_r T (lift (S O) (s k d) x0)
  84 (\lambda (t2: T).(ex T (\lambda (v: T).(or (subst0 d w (THead k t0 t2) (lift
  85 (S O) d v)) (eq T (THead k t0 t2) (lift (S O) d v)))))) (ex_intro T (\lambda
  86 (v: T).(or (subst0 d w (THead k t0 (lift (S O) (s k d) x0)) (lift (S O) d v))
  87 (eq T (THead k t0 (lift (S O) (s k d) x0)) (lift (S O) d v)))) (THead k x x0)
  88 (eq_ind_r T (THead k (lift (S O) d x) (lift (S O) (s k d) x0)) (\lambda (t2:
  89 T).(or (subst0 d w (THead k t0 (lift (S O) (s k d) x0)) t2) (eq T (THead k t0
  90 (lift (S O) (s k d) x0)) t2))) (or_introl (subst0 d w (THead k t0 (lift (S O)
  91 (s k d) x0)) (THead k (lift (S O) d x) (lift (S O) (s k d) x0))) (eq T (THead
  92 k t0 (lift (S O) (s k d) x0)) (THead k (lift (S O) d x) (lift (S O) (s k d)
  93 x0))) (subst0_fst w (lift (S O) d x) t0 d H3 (lift (S O) (s k d) x0) k))
  94 (lift (S O) d (THead k x x0)) (lift_head k x x0 (S O) d))) t1 H6)) H5)))
  95 H4)))) (\lambda (H3: (eq T t0 (lift (S O) d x))).(let H_x0 \def (H0 (s k d))
  96 in (let H4 \def H_x0 in (ex_ind T (\lambda (v: T).(or (subst0 (s k d) w t1
  97 (lift (S O) (s k d) v)) (eq T t1 (lift (S O) (s k d) v)))) (ex T (\lambda (v:
  98 T).(or (subst0 d w (THead k t0 t1) (lift (S O) d v)) (eq T (THead k t0 t1)
  99 (lift (S O) d v))))) (\lambda (x0: T).(\lambda (H5: (or (subst0 (s k d) w t1
 100 (lift (S O) (s k d) x0)) (eq T t1 (lift (S O) (s k d) x0)))).(or_ind (subst0
 101 (s k d) w t1 (lift (S O) (s k d) x0)) (eq T t1 (lift (S O) (s k d) x0)) (ex T
 102 (\lambda (v: T).(or (subst0 d w (THead k t0 t1) (lift (S O) d v)) (eq T
 103 (THead k t0 t1) (lift (S O) d v))))) (\lambda (H6: (subst0 (s k d) w t1 (lift
 104 (S O) (s k d) x0))).(eq_ind_r T (lift (S O) d x) (\lambda (t2: T).(ex T
 105 (\lambda (v: T).(or (subst0 d w (THead k t2 t1) (lift (S O) d v)) (eq T
 106 (THead k t2 t1) (lift (S O) d v)))))) (ex_intro T (\lambda (v: T).(or (subst0
 107 d w (THead k (lift (S O) d x) t1) (lift (S O) d v)) (eq T (THead k (lift (S
 108 O) d x) t1) (lift (S O) d v)))) (THead k x x0) (eq_ind_r T (THead k (lift (S
 109 O) d x) (lift (S O) (s k d) x0)) (\lambda (t2: T).(or (subst0 d w (THead k
 110 (lift (S O) d x) t1) t2) (eq T (THead k (lift (S O) d x) t1) t2))) (or_introl
 111 (subst0 d w (THead k (lift (S O) d x) t1) (THead k (lift (S O) d x) (lift (S
 112 O) (s k d) x0))) (eq T (THead k (lift (S O) d x) t1) (THead k (lift (S O) d
 113 x) (lift (S O) (s k d) x0))) (subst0_snd k w (lift (S O) (s k d) x0) t1 d H6
 114 (lift (S O) d x))) (lift (S O) d (THead k x x0)) (lift_head k x x0 (S O) d)))
 115 t0 H3)) (\lambda (H6: (eq T t1 (lift (S O) (s k d) x0))).(eq_ind_r T (lift (S
 116 O) (s k d) x0) (\lambda (t2: T).(ex T (\lambda (v: T).(or (subst0 d w (THead
 117 k t0 t2) (lift (S O) d v)) (eq T (THead k t0 t2) (lift (S O) d v))))))
 118 (eq_ind_r T (lift (S O) d x) (\lambda (t2: T).(ex T (\lambda (v: T).(or
 119 (subst0 d w (THead k t2 (lift (S O) (s k d) x0)) (lift (S O) d v)) (eq T
 120 (THead k t2 (lift (S O) (s k d) x0)) (lift (S O) d v)))))) (ex_intro T
 121 (\lambda (v: T).(or (subst0 d w (THead k (lift (S O) d x) (lift (S O) (s k d)
 122 x0)) (lift (S O) d v)) (eq T (THead k (lift (S O) d x) (lift (S O) (s k d)
 123 x0)) (lift (S O) d v)))) (THead k x x0) (eq_ind_r T (THead k (lift (S O) d x)
 124 (lift (S O) (s k d) x0)) (\lambda (t2: T).(or (subst0 d w (THead k (lift (S
 125 O) d x) (lift (S O) (s k d) x0)) t2) (eq T (THead k (lift (S O) d x) (lift (S
 126 O) (s k d) x0)) t2))) (or_intror (subst0 d w (THead k (lift (S O) d x) (lift
 127 (S O) (s k d) x0)) (THead k (lift (S O) d x) (lift (S O) (s k d) x0))) (eq T
 128 (THead k (lift (S O) d x) (lift (S O) (s k d) x0)) (THead k (lift (S O) d x)
 129 (lift (S O) (s k d) x0))) (refl_equal T (THead k (lift (S O) d x) (lift (S O)
 130 (s k d) x0)))) (lift (S O) d (THead k x x0)) (lift_head k x x0 (S O) d))) t0
 131 H3) t1 H6)) H5))) H4)))) H2))) H1))))))))) t)).
 132