matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/nf2.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/ty3/nf2".
  18
  19 include "ty3/arity.ma".
  20
  21 include "nf2/arity.ma".
  22
  23 theorem ty3_nf2_inv_all:
  24  \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (u: T).((ty3 g c t
  25 u) \to ((nf2 c t) \to (or3 (ex3_2 T T (\lambda (w: T).(\lambda (u0: T).(eq T
  26 t (THead (Bind Abst) w u0)))) (\lambda (w: T).(\lambda (_: T).(nf2 c w)))
  27 (\lambda (w: T).(\lambda (u0: T).(nf2 (CHead c (Bind Abst) w) u0)))) (ex nat
  28 (\lambda (n: nat).(eq T t (TSort n)))) (ex3_2 TList nat (\lambda (ws:
  29 TList).(\lambda (i: nat).(eq T t (THeads (Flat Appl) ws (TLRef i)))))
  30 (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c ws))) (\lambda (_:
  31 TList).(\lambda (i: nat).(nf2 c (TLRef i)))))))))))
  32 \def
  33  \lambda (g: G).(\lambda (c: C).(\lambda (t: T).(\lambda (u: T).(\lambda (H:
  34 (ty3 g c t u)).(\lambda (H0: (nf2 c t)).(let H_x \def (ty3_arity g c t u H)
  35 in (let H1 \def H_x in (ex2_ind A (\lambda (a1: A).(arity g c t a1)) (\lambda
  36 (a1: A).(arity g c u (asucc g a1))) (or3 (ex3_2 T T (\lambda (w: T).(\lambda
  37 (u0: T).(eq T t (THead (Bind Abst) w u0)))) (\lambda (w: T).(\lambda (_:
  38 T).(nf2 c w))) (\lambda (w: T).(\lambda (u0: T).(nf2 (CHead c (Bind Abst) w)
  39 u0)))) (ex nat (\lambda (n: nat).(eq T t (TSort n)))) (ex3_2 TList nat
  40 (\lambda (ws: TList).(\lambda (i: nat).(eq T t (THeads (Flat Appl) ws (TLRef
  41 i))))) (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c ws))) (\lambda (_:
  42 TList).(\lambda (i: nat).(nf2 c (TLRef i)))))) (\lambda (x: A).(\lambda (H2:
  43 (arity g c t x)).(\lambda (_: (arity g c u (asucc g x))).(arity_nf2_inv_all g
  44 c t x H2 H0)))) H1)))))))).
  45
  46 theorem ty3_nf2_inv_sort:
  47  \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (m: nat).((ty3 g c t
  48 (TSort m)) \to ((nf2 c t) \to (or (ex2 nat (\lambda (n: nat).(eq T t (TSort
  49 n))) (\lambda (n: nat).(eq nat m (next g n)))) (ex3_2 TList nat (\lambda (ws:
  50 TList).(\lambda (i: nat).(eq T t (THeads (Flat Appl) ws (TLRef i)))))
  51 (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c ws))) (\lambda (_:
  52 TList).(\lambda (i: nat).(nf2 c (TLRef i)))))))))))
  53 \def
  54  \lambda (g: G).(\lambda (c: C).(\lambda (t: T).(\lambda (m: nat).(\lambda
  55 (H: (ty3 g c t (TSort m))).(\lambda (H0: (nf2 c t)).(let H_x \def
  56 (ty3_nf2_inv_all g c t (TSort m) H H0) in (let H1 \def H_x in (or3_ind (ex3_2
  57 T T (\lambda (w: T).(\lambda (u: T).(eq T t (THead (Bind Abst) w u))))
  58 (\lambda (w: T).(\lambda (_: T).(nf2 c w))) (\lambda (w: T).(\lambda (u:
  59 T).(nf2 (CHead c (Bind Abst) w) u)))) (ex nat (\lambda (n: nat).(eq T t
  60 (TSort n)))) (ex3_2 TList nat (\lambda (ws: TList).(\lambda (i: nat).(eq T t
  61 (THeads (Flat Appl) ws (TLRef i))))) (\lambda (ws: TList).(\lambda (_:
  62 nat).(nfs2 c ws))) (\lambda (_: TList).(\lambda (i: nat).(nf2 c (TLRef i)))))
  63 (or (ex2 nat (\lambda (n: nat).(eq T t (TSort n))) (\lambda (n: nat).(eq nat
  64 m (next g n)))) (ex3_2 TList nat (\lambda (ws: TList).(\lambda (i: nat).(eq T
  65 t (THeads (Flat Appl) ws (TLRef i))))) (\lambda (ws: TList).(\lambda (_:
  66 nat).(nfs2 c ws))) (\lambda (_: TList).(\lambda (i: nat).(nf2 c (TLRef
  67 i)))))) (\lambda (H2: (ex3_2 T T (\lambda (w: T).(\lambda (u: T).(eq T t
  68 (THead (Bind Abst) w u)))) (\lambda (w: T).(\lambda (_: T).(nf2 c w)))
  69 (\lambda (w: T).(\lambda (u: T).(nf2 (CHead c (Bind Abst) w)
  70 u))))).(ex3_2_ind T T (\lambda (w: T).(\lambda (u: T).(eq T t (THead (Bind
  71 Abst) w u)))) (\lambda (w: T).(\lambda (_: T).(nf2 c w))) (\lambda (w:
  72 T).(\lambda (u: T).(nf2 (CHead c (Bind Abst) w) u))) (or (ex2 nat (\lambda
  73 (n: nat).(eq T t (TSort n))) (\lambda (n: nat).(eq nat m (next g n)))) (ex3_2
  74 TList nat (\lambda (ws: TList).(\lambda (i: nat).(eq T t (THeads (Flat Appl)
  75 ws (TLRef i))))) (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c ws)))
  76 (\lambda (_: TList).(\lambda (i: nat).(nf2 c (TLRef i)))))) (\lambda (x0:
  77 T).(\lambda (x1: T).(\lambda (H3: (eq T t (THead (Bind Abst) x0
  78 x1))).(\lambda (_: (nf2 c x0)).(\lambda (_: (nf2 (CHead c (Bind Abst) x0)
  79 x1)).(let H6 \def (eq_ind T t (\lambda (t0: T).(ty3 g c t0 (TSort m))) H
  80 (THead (Bind Abst) x0 x1) H3) in (eq_ind_r T (THead (Bind Abst) x0 x1)
  81 (\lambda (t0: T).(or (ex2 nat (\lambda (n: nat).(eq T t0 (TSort n))) (\lambda
  82 (n: nat).(eq nat m (next g n)))) (ex3_2 TList nat (\lambda (ws:
  83 TList).(\lambda (i: nat).(eq T t0 (THeads (Flat Appl) ws (TLRef i)))))
  84 (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c ws))) (\lambda (_:
  85 TList).(\lambda (i: nat).(nf2 c (TLRef i))))))) (ex4_3_ind T T T (\lambda
  86 (t2: T).(\lambda (_: T).(\lambda (_: T).(pc3 c (THead (Bind Abst) x0 t2)
  87 (TSort m))))) (\lambda (_: T).(\lambda (t0: T).(\lambda (_: T).(ty3 g c x0
  88 t0)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c (Bind
  89 Abst) x0) x1 t2)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (t1: T).(ty3 g
  90 (CHead c (Bind Abst) x0) t2 t1)))) (or (ex2 nat (\lambda (n: nat).(eq T
  91 (THead (Bind Abst) x0 x1) (TSort n))) (\lambda (n: nat).(eq nat m (next g
  92 n)))) (ex3_2 TList nat (\lambda (ws: TList).(\lambda (i: nat).(eq T (THead
  93 (Bind Abst) x0 x1) (THeads (Flat Appl) ws (TLRef i))))) (\lambda (ws:
  94 TList).(\lambda (_: nat).(nfs2 c ws))) (\lambda (_: TList).(\lambda (i:
  95 nat).(nf2 c (TLRef i)))))) (\lambda (x2: T).(\lambda (x3: T).(\lambda (x4:
  96 T).(\lambda (H7: (pc3 c (THead (Bind Abst) x0 x2) (TSort m))).(\lambda (_:
  97 (ty3 g c x0 x3)).(\lambda (_: (ty3 g (CHead c (Bind Abst) x0) x1
  98 x2)).(\lambda (_: (ty3 g (CHead c (Bind Abst) x0) x2 x4)).(pc3_gen_sort_abst
  99 c x0 x2 m (pc3_s c (TSort m) (THead (Bind Abst) x0 x2) H7) (or (ex2 nat
 100 (\lambda (n: nat).(eq T (THead (Bind Abst) x0 x1) (TSort n))) (\lambda (n:
 101 nat).(eq nat m (next g n)))) (ex3_2 TList nat (\lambda (ws: TList).(\lambda
 102 (i: nat).(eq T (THead (Bind Abst) x0 x1) (THeads (Flat Appl) ws (TLRef i)))))
 103 (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c ws))) (\lambda (_:
 104 TList).(\lambda (i: nat).(nf2 c (TLRef i)))))))))))))) (ty3_gen_bind g Abst c
 105 x0 x1 (TSort m) H6)) t H3))))))) H2)) (\lambda (H2: (ex nat (\lambda (n:
 106 nat).(eq T t (TSort n))))).(ex_ind nat (\lambda (n: nat).(eq T t (TSort n)))
 107 (or (ex2 nat (\lambda (n: nat).(eq T t (TSort n))) (\lambda (n: nat).(eq nat
 108 m (next g n)))) (ex3_2 TList nat (\lambda (ws: TList).(\lambda (i: nat).(eq T
 109 t (THeads (Flat Appl) ws (TLRef i))))) (\lambda (ws: TList).(\lambda (_:
 110 nat).(nfs2 c ws))) (\lambda (_: TList).(\lambda (i: nat).(nf2 c (TLRef
 111 i)))))) (\lambda (x: nat).(\lambda (H3: (eq T t (TSort x))).(let H4 \def
 112 (eq_ind T t (\lambda (t0: T).(ty3 g c t0 (TSort m))) H (TSort x) H3) in
 113 (eq_ind_r T (TSort x) (\lambda (t0: T).(or (ex2 nat (\lambda (n: nat).(eq T
 114 t0 (TSort n))) (\lambda (n: nat).(eq nat m (next g n)))) (ex3_2 TList nat
 115 (\lambda (ws: TList).(\lambda (i: nat).(eq T t0 (THeads (Flat Appl) ws (TLRef
 116 i))))) (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c ws))) (\lambda (_:
 117 TList).(\lambda (i: nat).(nf2 c (TLRef i))))))) (eq_ind nat (next g x)
 118 (\lambda (n: nat).(or (ex2 nat (\lambda (n0: nat).(eq T (TSort x) (TSort
 119 n0))) (\lambda (n0: nat).(eq nat n (next g n0)))) (ex3_2 TList nat (\lambda
 120 (ws: TList).(\lambda (i: nat).(eq T (TSort x) (THeads (Flat Appl) ws (TLRef
 121 i))))) (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c ws))) (\lambda (_:
 122 TList).(\lambda (i: nat).(nf2 c (TLRef i))))))) (or_introl (ex2 nat (\lambda
 123 (n: nat).(eq T (TSort x) (TSort n))) (\lambda (n: nat).(eq nat (next g x)
 124 (next g n)))) (ex3_2 TList nat (\lambda (ws: TList).(\lambda (i: nat).(eq T
 125 (TSort x) (THeads (Flat Appl) ws (TLRef i))))) (\lambda (ws: TList).(\lambda
 126 (_: nat).(nfs2 c ws))) (\lambda (_: TList).(\lambda (i: nat).(nf2 c (TLRef
 127 i))))) (ex_intro2 nat (\lambda (n: nat).(eq T (TSort x) (TSort n))) (\lambda
 128 (n: nat).(eq nat (next g x) (next g n))) x (refl_equal T (TSort x))
 129 (refl_equal nat (next g x)))) m (pc3_gen_sort c (next g x) m (ty3_gen_sort g
 130 c (TSort m) x H4))) t H3)))) H2)) (\lambda (H2: (ex3_2 TList nat (\lambda
 131 (ws: TList).(\lambda (i: nat).(eq T t (THeads (Flat Appl) ws (TLRef i)))))
 132 (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c ws))) (\lambda (_:
 133 TList).(\lambda (i: nat).(nf2 c (TLRef i)))))).(ex3_2_ind TList nat (\lambda
 134 (ws: TList).(\lambda (i: nat).(eq T t (THeads (Flat Appl) ws (TLRef i)))))
 135 (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c ws))) (\lambda (_:
 136 TList).(\lambda (i: nat).(nf2 c (TLRef i)))) (or (ex2 nat (\lambda (n:
 137 nat).(eq T t (TSort n))) (\lambda (n: nat).(eq nat m (next g n)))) (ex3_2
 138 TList nat (\lambda (ws: TList).(\lambda (i: nat).(eq T t (THeads (Flat Appl)
 139 ws (TLRef i))))) (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c ws)))
 140 (\lambda (_: TList).(\lambda (i: nat).(nf2 c (TLRef i)))))) (\lambda (x0:
 141 TList).(\lambda (x1: nat).(\lambda (H3: (eq T t (THeads (Flat Appl) x0 (TLRef
 142 x1)))).(\lambda (H4: (nfs2 c x0)).(\lambda (H5: (nf2 c (TLRef x1))).(let H6
 143 \def (eq_ind T t (\lambda (t0: T).(ty3 g c t0 (TSort m))) H (THeads (Flat
 144 Appl) x0 (TLRef x1)) H3) in (eq_ind_r T (THeads (Flat Appl) x0 (TLRef x1))
 145 (\lambda (t0: T).(or (ex2 nat (\lambda (n: nat).(eq T t0 (TSort n))) (\lambda
 146 (n: nat).(eq nat m (next g n)))) (ex3_2 TList nat (\lambda (ws:
 147 TList).(\lambda (i: nat).(eq T t0 (THeads (Flat Appl) ws (TLRef i)))))
 148 (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c ws))) (\lambda (_:
 149 TList).(\lambda (i: nat).(nf2 c (TLRef i))))))) (or_intror (ex2 nat (\lambda
 150 (n: nat).(eq T (THeads (Flat Appl) x0 (TLRef x1)) (TSort n))) (\lambda (n:
 151 nat).(eq nat m (next g n)))) (ex3_2 TList nat (\lambda (ws: TList).(\lambda
 152 (i: nat).(eq T (THeads (Flat Appl) x0 (TLRef x1)) (THeads (Flat Appl) ws
 153 (TLRef i))))) (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c ws))) (\lambda
 154 (_: TList).(\lambda (i: nat).(nf2 c (TLRef i))))) (ex3_2_intro TList nat
 155 (\lambda (ws: TList).(\lambda (i: nat).(eq T (THeads (Flat Appl) x0 (TLRef
 156 x1)) (THeads (Flat Appl) ws (TLRef i))))) (\lambda (ws: TList).(\lambda (_:
 157 nat).(nfs2 c ws))) (\lambda (_: TList).(\lambda (i: nat).(nf2 c (TLRef i))))
 158 x0 x1 (refl_equal T (THeads (Flat Appl) x0 (TLRef x1))) H4 H5)) t H3)))))))
 159 H2)) H1)))))))).
 160