matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/nf2/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/nf2/dec".
  18
  19 include "nf2/defs.ma".
  20
  21 include "pr2/clen.ma".
  22
  23 include "pr2/fwd.ma".
  24
  25 include "pr0/dec.ma".
  26
  27 include "C/props.ma".
  28
  29 theorem nf2_dec:
  30  \forall (c: C).(\forall (t1: T).(or (nf2 c t1) (ex2 T (\lambda (t2: T).((eq
  31 T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 c t1 t2)))))
  32 \def
  33  \lambda (c: C).(c_tail_ind (\lambda (c0: C).(\forall (t1: T).(or (\forall
  34 (t2: T).((pr2 c0 t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1
  35 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 c0 t1 t2)))))) (\lambda
  36 (n: nat).(\lambda (t1: T).(let H_x \def (nf0_dec t1) in (let H \def H_x in
  37 (or_ind (\forall (t2: T).((pr0 t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2:
  38 T).((eq T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 t1 t2)))
  39 (or (\forall (t2: T).((pr2 (CSort n) t1 t2) \to (eq T t1 t2))) (ex2 T
  40 (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2:
  41 T).(pr2 (CSort n) t1 t2)))) (\lambda (H0: ((\forall (t2: T).((pr0 t1 t2) \to
  42 (eq T t1 t2))))).(or_introl (\forall (t2: T).((pr2 (CSort n) t1 t2) \to (eq T
  43 t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P)))
  44 (\lambda (t2: T).(pr2 (CSort n) t1 t2))) (\lambda (t2: T).(\lambda (H1: (pr2
  45 (CSort n) t1 t2)).(let H_y \def (pr2_gen_csort t1 t2 n H1) in (H0 t2
  46 H_y)))))) (\lambda (H0: (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall
  47 (P: Prop).P))) (\lambda (t2: T).(pr0 t1 t2)))).(ex2_ind T (\lambda (t2:
  48 T).((eq T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 t1 t2))
  49 (or (\forall (t2: T).((pr2 (CSort n) t1 t2) \to (eq T t1 t2))) (ex2 T
  50 (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2:
  51 T).(pr2 (CSort n) t1 t2)))) (\lambda (x: T).(\lambda (H1: (((eq T t1 x) \to
  52 (\forall (P: Prop).P)))).(\lambda (H2: (pr0 t1 x)).(or_intror (\forall (t2:
  53 T).((pr2 (CSort n) t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2: T).((eq T
  54 t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 (CSort n) t1 t2)))
  55 (ex_intro2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P)))
  56 (\lambda (t2: T).(pr2 (CSort n) t1 t2)) x H1 (pr2_free (CSort n) t1 x
  57 H2)))))) H0)) H))))) (\lambda (c0: C).(\lambda (H: ((\forall (t1: T).(or
  58 (\forall (t2: T).((pr2 c0 t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2:
  59 T).((eq T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 c0 t1
  60 t2))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (t1: T).(let H_x \def (H
  61 t1) in (let H0 \def H_x in (or_ind (\forall (t2: T).((pr2 c0 t1 t2) \to (eq T
  62 t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P)))
  63 (\lambda (t2: T).(pr2 c0 t1 t2))) (or (\forall (t2: T).((pr2 (CTail k t c0)
  64 t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall
  65 (P: Prop).P))) (\lambda (t2: T).(pr2 (CTail k t c0) t1 t2)))) (\lambda (H1:
  66 ((\forall (t2: T).((pr2 c0 t1 t2) \to (eq T t1 t2))))).(match k in K return
  67 (\lambda (k0: K).(or (\forall (t2: T).((pr2 (CTail k0 t c0) t1 t2) \to (eq T
  68 t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P)))
  69 (\lambda (t2: T).(pr2 (CTail k0 t c0) t1 t2))))) with [(Bind b) \Rightarrow
  70 (match b in B return (\lambda (b0: B).(or (\forall (t2: T).((pr2 (CTail (Bind
  71 b0) t c0) t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to
  72 (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 (CTail (Bind b0) t c0) t1
  73 t2))))) with [Abbr \Rightarrow (let H_x0 \def (dnf_dec t t1 (clen c0)) in
  74 (let H2 \def H_x0 in (ex_ind T (\lambda (v: T).(or (subst0 (clen c0) t t1
  75 (lift (S O) (clen c0) v)) (eq T t1 (lift (S O) (clen c0) v)))) (or (\forall
  76 (t2: T).((pr2 (CTail (Bind Abbr) t c0) t1 t2) \to (eq T t1 t2))) (ex2 T
  77 (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2:
  78 T).(pr2 (CTail (Bind Abbr) t c0) t1 t2)))) (\lambda (x: T).(\lambda (H3: (or
  79 (subst0 (clen c0) t t1 (lift (S O) (clen c0) x)) (eq T t1 (lift (S O) (clen
  80 c0) x)))).(or_ind (subst0 (clen c0) t t1 (lift (S O) (clen c0) x)) (eq T t1
  81 (lift (S O) (clen c0) x)) (or (\forall (t2: T).((pr2 (CTail (Bind Abbr) t c0)
  82 t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall
  83 (P: Prop).P))) (\lambda (t2: T).(pr2 (CTail (Bind Abbr) t c0) t1 t2))))
  84 (\lambda (H4: (subst0 (clen c0) t t1 (lift (S O) (clen c0) x))).(let H_x1
  85 \def (getl_ctail_clen Abbr t c0) in (let H5 \def H_x1 in (ex_ind nat (\lambda
  86 (n: nat).(getl (clen c0) (CTail (Bind Abbr) t c0) (CHead (CSort n) (Bind
  87 Abbr) t))) (or (\forall (t2: T).((pr2 (CTail (Bind Abbr) t c0) t1 t2) \to (eq
  88 T t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P)))
  89 (\lambda (t2: T).(pr2 (CTail (Bind Abbr) t c0) t1 t2)))) (\lambda (x0:
  90 nat).(\lambda (H6: (getl (clen c0) (CTail (Bind Abbr) t c0) (CHead (CSort x0)
  91 (Bind Abbr) t))).(or_intror (\forall (t2: T).((pr2 (CTail (Bind Abbr) t c0)
  92 t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall
  93 (P: Prop).P))) (\lambda (t2: T).(pr2 (CTail (Bind Abbr) t c0) t1 t2)))
  94 (ex_intro2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P)))
  95 (\lambda (t2: T).(pr2 (CTail (Bind Abbr) t c0) t1 t2)) (lift (S O) (clen c0)
  96 x) (\lambda (H7: (eq T t1 (lift (S O) (clen c0) x))).(\lambda (P: Prop).(let
  97 H8 \def (eq_ind T t1 (\lambda (t0: T).(subst0 (clen c0) t t0 (lift (S O)
  98 (clen c0) x))) H4 (lift (S O) (clen c0) x) H7) in (subst0_gen_lift_false x t
  99 (lift (S O) (clen c0) x) (S O) (clen c0) (clen c0) (le_n (clen c0)) (eq_ind_r
 100 nat (plus (S O) (clen c0)) (\lambda (n: nat).(lt (clen c0) n)) (le_n (plus (S
 101 O) (clen c0))) (plus (clen c0) (S O)) (plus_comm (clen c0) (S O))) H8 P))))
 102 (pr2_delta (CTail (Bind Abbr) t c0) (CSort x0) t (clen c0) H6 t1 t1 (pr0_refl
 103 t1) (lift (S O) (clen c0) x) H4))))) H5)))) (\lambda (H4: (eq T t1 (lift (S
 104 O) (clen c0) x))).(let H5 \def (eq_ind T t1 (\lambda (t0: T).(\forall (t2:
 105 T).((pr2 c0 t0 t2) \to (eq T t0 t2)))) H1 (lift (S O) (clen c0) x) H4) in
 106 (eq_ind_r T (lift (S O) (clen c0) x) (\lambda (t0: T).(or (\forall (t2:
 107 T).((pr2 (CTail (Bind Abbr) t c0) t0 t2) \to (eq T t0 t2))) (ex2 T (\lambda
 108 (t2: T).((eq T t0 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2
 109 (CTail (Bind Abbr) t c0) t0 t2))))) (or_introl (\forall (t2: T).((pr2 (CTail
 110 (Bind Abbr) t c0) (lift (S O) (clen c0) x) t2) \to (eq T (lift (S O) (clen
 111 c0) x) t2))) (ex2 T (\lambda (t2: T).((eq T (lift (S O) (clen c0) x) t2) \to
 112 (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 (CTail (Bind Abbr) t c0) (lift
 113 (S O) (clen c0) x) t2))) (\lambda (t2: T).(\lambda (H6: (pr2 (CTail (Bind
 114 Abbr) t c0) (lift (S O) (clen c0) x) t2)).(let H_x1 \def (pr2_gen_ctail (Bind
 115 Abbr) c0 t (lift (S O) (clen c0) x) t2 H6) in (let H7 \def H_x1 in (or_ind
 116 (pr2 c0 (lift (S O) (clen c0) x) t2) (ex3 T (\lambda (_: T).(eq K (Bind Abbr)
 117 (Bind Abbr))) (\lambda (t0: T).(pr0 (lift (S O) (clen c0) x) t0)) (\lambda
 118 (t0: T).(subst0 (clen c0) t t0 t2))) (eq T (lift (S O) (clen c0) x) t2)
 119 (\lambda (H8: (pr2 c0 (lift (S O) (clen c0) x) t2)).(H5 t2 H8)) (\lambda (H8:
 120 (ex3 T (\lambda (_: T).(eq K (Bind Abbr) (Bind Abbr))) (\lambda (t0: T).(pr0
 121 (lift (S O) (clen c0) x) t0)) (\lambda (t0: T).(subst0 (clen c0) t t0
 122 t2)))).(ex3_ind T (\lambda (_: T).(eq K (Bind Abbr) (Bind Abbr))) (\lambda
 123 (t0: T).(pr0 (lift (S O) (clen c0) x) t0)) (\lambda (t0: T).(subst0 (clen c0)
 124 t t0 t2)) (eq T (lift (S O) (clen c0) x) t2) (\lambda (x0: T).(\lambda (_:
 125 (eq K (Bind Abbr) (Bind Abbr))).(\lambda (H10: (pr0 (lift (S O) (clen c0) x)
 126 x0)).(\lambda (H11: (subst0 (clen c0) t x0 t2)).(ex2_ind T (\lambda (t3:
 127 T).(eq T x0 (lift (S O) (clen c0) t3))) (\lambda (t3: T).(pr0 x t3)) (eq T
 128 (lift (S O) (clen c0) x) t2) (\lambda (x1: T).(\lambda (H12: (eq T x0 (lift
 129 (S O) (clen c0) x1))).(\lambda (_: (pr0 x x1)).(let H14 \def (eq_ind T x0
 130 (\lambda (t0: T).(subst0 (clen c0) t t0 t2)) H11 (lift (S O) (clen c0) x1)
 131 H12) in (subst0_gen_lift_false x1 t t2 (S O) (clen c0) (clen c0) (le_n (clen
 132 c0)) (eq_ind_r nat (plus (S O) (clen c0)) (\lambda (n: nat).(lt (clen c0) n))
 133 (le_n (plus (S O) (clen c0))) (plus (clen c0) (S O)) (plus_comm (clen c0) (S
 134 O))) H14 (eq T (lift (S O) (clen c0) x) t2)))))) (pr0_gen_lift x x0 (S O)
 135 (clen c0) H10)))))) H8)) H7)))))) t1 H4))) H3))) H2))) | Abst \Rightarrow
 136 (or_introl (\forall (t2: T).((pr2 (CTail (Bind Abst) t c0) t1 t2) \to (eq T
 137 t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P)))
 138 (\lambda (t2: T).(pr2 (CTail (Bind Abst) t c0) t1 t2))) (\lambda (t2:
 139 T).(\lambda (H2: (pr2 (CTail (Bind Abst) t c0) t1 t2)).(let H_x0 \def
 140 (pr2_gen_ctail (Bind Abst) c0 t t1 t2 H2) in (let H3 \def H_x0 in (or_ind
 141 (pr2 c0 t1 t2) (ex3 T (\lambda (_: T).(eq K (Bind Abst) (Bind Abbr)))
 142 (\lambda (t0: T).(pr0 t1 t0)) (\lambda (t0: T).(subst0 (clen c0) t t0 t2)))
 143 (eq T t1 t2) (\lambda (H4: (pr2 c0 t1 t2)).(H1 t2 H4)) (\lambda (H4: (ex3 T
 144 (\lambda (_: T).(eq K (Bind Abst) (Bind Abbr))) (\lambda (t0: T).(pr0 t1 t0))
 145 (\lambda (t0: T).(subst0 (clen c0) t t0 t2)))).(ex3_ind T (\lambda (_: T).(eq
 146 K (Bind Abst) (Bind Abbr))) (\lambda (t0: T).(pr0 t1 t0)) (\lambda (t0:
 147 T).(subst0 (clen c0) t t0 t2)) (eq T t1 t2) (\lambda (x0: T).(\lambda (H5:
 148 (eq K (Bind Abst) (Bind Abbr))).(\lambda (_: (pr0 t1 x0)).(\lambda (_:
 149 (subst0 (clen c0) t x0 t2)).(let H8 \def (eq_ind K (Bind Abst) (\lambda (ee:
 150 K).(match ee in K return (\lambda (_: K).Prop) with [(Bind b0) \Rightarrow
 151 (match b0 in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow False |
 152 Abst \Rightarrow True | Void \Rightarrow False]) | (Flat _) \Rightarrow
 153 False])) I (Bind Abbr) H5) in (False_ind (eq T t1 t2) H8)))))) H4)) H3))))))
 154 | Void \Rightarrow (or_introl (\forall (t2: T).((pr2 (CTail (Bind Void) t c0)
 155 t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall
 156 (P: Prop).P))) (\lambda (t2: T).(pr2 (CTail (Bind Void) t c0) t1 t2)))
 157 (\lambda (t2: T).(\lambda (H2: (pr2 (CTail (Bind Void) t c0) t1 t2)).(let
 158 H_x0 \def (pr2_gen_ctail (Bind Void) c0 t t1 t2 H2) in (let H3 \def H_x0 in
 159 (or_ind (pr2 c0 t1 t2) (ex3 T (\lambda (_: T).(eq K (Bind Void) (Bind Abbr)))
 160 (\lambda (t0: T).(pr0 t1 t0)) (\lambda (t0: T).(subst0 (clen c0) t t0 t2)))
 161 (eq T t1 t2) (\lambda (H4: (pr2 c0 t1 t2)).(H1 t2 H4)) (\lambda (H4: (ex3 T
 162 (\lambda (_: T).(eq K (Bind Void) (Bind Abbr))) (\lambda (t0: T).(pr0 t1 t0))
 163 (\lambda (t0: T).(subst0 (clen c0) t t0 t2)))).(ex3_ind T (\lambda (_: T).(eq
 164 K (Bind Void) (Bind Abbr))) (\lambda (t0: T).(pr0 t1 t0)) (\lambda (t0:
 165 T).(subst0 (clen c0) t t0 t2)) (eq T t1 t2) (\lambda (x0: T).(\lambda (H5:
 166 (eq K (Bind Void) (Bind Abbr))).(\lambda (_: (pr0 t1 x0)).(\lambda (_:
 167 (subst0 (clen c0) t x0 t2)).(let H8 \def (eq_ind K (Bind Void) (\lambda (ee:
 168 K).(match ee in K return (\lambda (_: K).Prop) with [(Bind b0) \Rightarrow
 169 (match b0 in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow False |
 170 Abst \Rightarrow False | Void \Rightarrow True]) | (Flat _) \Rightarrow
 171 False])) I (Bind Abbr) H5) in (False_ind (eq T t1 t2) H8)))))) H4))
 172 H3))))))]) | (Flat f) \Rightarrow (or_introl (\forall (t2: T).((pr2 (CTail
 173 (Flat f) t c0) t1 t2) \to (eq T t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1
 174 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 (CTail (Flat f) t c0)
 175 t1 t2))) (\lambda (t2: T).(\lambda (H2: (pr2 (CTail (Flat f) t c0) t1
 176 t2)).(let H_x0 \def (pr2_gen_ctail (Flat f) c0 t t1 t2 H2) in (let H3 \def
 177 H_x0 in (or_ind (pr2 c0 t1 t2) (ex3 T (\lambda (_: T).(eq K (Flat f) (Bind
 178 Abbr))) (\lambda (t0: T).(pr0 t1 t0)) (\lambda (t0: T).(subst0 (clen c0) t t0
 179 t2))) (eq T t1 t2) (\lambda (H4: (pr2 c0 t1 t2)).(H1 t2 H4)) (\lambda (H4:
 180 (ex3 T (\lambda (_: T).(eq K (Flat f) (Bind Abbr))) (\lambda (t0: T).(pr0 t1
 181 t0)) (\lambda (t0: T).(subst0 (clen c0) t t0 t2)))).(ex3_ind T (\lambda (_:
 182 T).(eq K (Flat f) (Bind Abbr))) (\lambda (t0: T).(pr0 t1 t0)) (\lambda (t0:
 183 T).(subst0 (clen c0) t t0 t2)) (eq T t1 t2) (\lambda (x0: T).(\lambda (H5:
 184 (eq K (Flat f) (Bind Abbr))).(\lambda (_: (pr0 t1 x0)).(\lambda (_: (subst0
 185 (clen c0) t x0 t2)).(let H8 \def (eq_ind K (Flat f) (\lambda (ee: K).(match
 186 ee in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat
 187 _) \Rightarrow True])) I (Bind Abbr) H5) in (False_ind (eq T t1 t2) H8))))))
 188 H4)) H3))))))])) (\lambda (H1: (ex2 T (\lambda (t2: T).((eq T t1 t2) \to
 189 (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 c0 t1 t2)))).(ex2_ind T
 190 (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2:
 191 T).(pr2 c0 t1 t2)) (or (\forall (t2: T).((pr2 (CTail k t c0) t1 t2) \to (eq T
 192 t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P)))
 193 (\lambda (t2: T).(pr2 (CTail k t c0) t1 t2)))) (\lambda (x: T).(\lambda (H2:
 194 (((eq T t1 x) \to (\forall (P: Prop).P)))).(\lambda (H3: (pr2 c0 t1
 195 x)).(or_intror (\forall (t2: T).((pr2 (CTail k t c0) t1 t2) \to (eq T t1
 196 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: Prop).P)))
 197 (\lambda (t2: T).(pr2 (CTail k t c0) t1 t2))) (ex_intro2 T (\lambda (t2:
 198 T).((eq T t1 t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr2 (CTail k t
 199 c0) t1 t2)) x H2 (pr2_ctail c0 t1 x H3 k t)))))) H1)) H0)))))))) c).
 200