matita/matita/contribs/lambdadelta/basic_1/wf3/ty3.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/wf3/getl.ma".
  18
  19 theorem wf3_pr2_conf:
  20  \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((pr2 c1
  21 t1 t2) \to (\forall (c2: C).((wf3 g c1 c2) \to (\forall (u: T).((ty3 g c1 t1
  22 u) \to (pr2 c2 t1 t2)))))))))
  23 \def
  24  \lambda (g: G).(\lambda (c1: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda
  25 (H: (pr2 c1 t1 t2)).(let TMP_1 \def (\lambda (c: C).(\lambda (t: T).(\lambda
  26 (t0: T).(\forall (c2: C).((wf3 g c c2) \to (\forall (u: T).((ty3 g c t u) \to
  27 (pr2 c2 t t0)))))))) in (let TMP_2 \def (\lambda (c: C).(\lambda (t3:
  28 T).(\lambda (t4: T).(\lambda (H0: (pr0 t3 t4)).(\lambda (c2: C).(\lambda (_:
  29 (wf3 g c c2)).(\lambda (u: T).(\lambda (_: (ty3 g c t3 u)).(pr2_free c2 t3 t4
  30 H0))))))))) in (let TMP_12 \def (\lambda (c: C).(\lambda (d: C).(\lambda (u:
  31 T).(\lambda (i: nat).(\lambda (H0: (getl i c (CHead d (Bind Abbr)
  32 u))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H1: (pr0 t3 t4)).(\lambda
  33 (t: T).(\lambda (H2: (subst0 i u t4 t)).(\lambda (c2: C).(\lambda (H3: (wf3 g
  34 c c2)).(\lambda (u0: T).(\lambda (H4: (ty3 g c t3 u0)).(let H_y \def
  35 (ty3_sred_pr0 t3 t4 H1 g c u0 H4) in (let H_x \def (ty3_getl_subst0 g c t4 u0
  36 H_y u t i H2 Abbr d u H0) in (let H5 \def H_x in (let TMP_3 \def (\lambda (w:
  37 T).(ty3 g d u w)) in (let TMP_4 \def (pr2 c2 t3 t) in (let TMP_11 \def
  38 (\lambda (x: T).(\lambda (H6: (ty3 g d u x)).(let H_x0 \def (wf3_getl_conf
  39 Abbr i c d u H0 g c2 H3 x H6) in (let H7 \def H_x0 in (let TMP_7 \def
  40 (\lambda (d2: C).(let TMP_5 \def (Bind Abbr) in (let TMP_6 \def (CHead d2
  41 TMP_5 u) in (getl i c2 TMP_6)))) in (let TMP_8 \def (\lambda (d2: C).(wf3 g d
  42 d2)) in (let TMP_9 \def (pr2 c2 t3 t) in (let TMP_10 \def (\lambda (x0:
  43 C).(\lambda (H8: (getl i c2 (CHead x0 (Bind Abbr) u))).(\lambda (_: (wf3 g d
  44 x0)).(pr2_delta c2 x0 u i H8 t3 t4 H1 t H2)))) in (ex2_ind C TMP_7 TMP_8
  45 TMP_9 TMP_10 H7))))))))) in (ex_ind T TMP_3 TMP_4 TMP_11
  46 H5))))))))))))))))))))) in (pr2_ind TMP_1 TMP_2 TMP_12 c1 t1 t2 H)))))))).
  47
  48 theorem wf3_pr3_conf:
  49  \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((pr3 c1
  50 t1 t2) \to (\forall (c2: C).((wf3 g c1 c2) \to (\forall (u: T).((ty3 g c1 t1
  51 u) \to (pr3 c2 t1 t2)))))))))
  52 \def
  53  \lambda (g: G).(\lambda (c1: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda
  54 (H: (pr3 c1 t1 t2)).(let TMP_1 \def (\lambda (t: T).(\lambda (t0: T).(\forall
  55 (c2: C).((wf3 g c1 c2) \to (\forall (u: T).((ty3 g c1 t u) \to (pr3 c2 t
  56 t0))))))) in (let TMP_2 \def (\lambda (t: T).(\lambda (c2: C).(\lambda (_:
  57 (wf3 g c1 c2)).(\lambda (u: T).(\lambda (_: (ty3 g c1 t u)).(pr3_refl c2
  58 t)))))) in (let TMP_6 \def (\lambda (t3: T).(\lambda (t4: T).(\lambda (H0:
  59 (pr2 c1 t4 t3)).(\lambda (t5: T).(\lambda (_: (pr3 c1 t3 t5)).(\lambda (H2:
  60 ((\forall (c2: C).((wf3 g c1 c2) \to (\forall (u: T).((ty3 g c1 t3 u) \to
  61 (pr3 c2 t3 t5))))))).(\lambda (c2: C).(\lambda (H3: (wf3 g c1 c2)).(\lambda
  62 (u: T).(\lambda (H4: (ty3 g c1 t4 u)).(let TMP_3 \def (wf3_pr2_conf g c1 t4
  63 t3 H0 c2 H3 u H4) in (let TMP_4 \def (ty3_sred_pr2 c1 t4 t3 H0 g u H4) in
  64 (let TMP_5 \def (H2 c2 H3 u TMP_4) in (pr3_sing c2 t3 t4 TMP_3 t5
  65 TMP_5)))))))))))))) in (pr3_ind c1 TMP_1 TMP_2 TMP_6 t1 t2 H)))))))).
  66
  67 theorem wf3_pc3_conf:
  68  \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((pc3 c1
  69 t1 t2) \to (\forall (c2: C).((wf3 g c1 c2) \to (\forall (u1: T).((ty3 g c1 t1
  70 u1) \to (\forall (u2: T).((ty3 g c1 t2 u2) \to (pc3 c2 t1 t2)))))))))))
  71 \def
  72  \lambda (g: G).(\lambda (c1: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda
  73 (H: (pc3 c1 t1 t2)).(\lambda (c2: C).(\lambda (H0: (wf3 g c1 c2)).(\lambda
  74 (u1: T).(\lambda (H1: (ty3 g c1 t1 u1)).(\lambda (u2: T).(\lambda (H2: (ty3 g
  75 c1 t2 u2)).(let H3 \def H in (let TMP_1 \def (\lambda (t: T).(pr3 c1 t1 t))
  76 in (let TMP_2 \def (\lambda (t: T).(pr3 c1 t2 t)) in (let TMP_3 \def (pc3 c2
  77 t1 t2) in (let TMP_6 \def (\lambda (x: T).(\lambda (H4: (pr3 c1 t1
  78 x)).(\lambda (H5: (pr3 c1 t2 x)).(let TMP_4 \def (wf3_pr3_conf g c1 t1 x H4
  79 c2 H0 u1 H1) in (let TMP_5 \def (wf3_pr3_conf g c1 t2 x H5 c2 H0 u2 H2) in
  80 (pc3_pr3_t c2 t1 x TMP_4 t2 TMP_5)))))) in (ex2_ind T TMP_1 TMP_2 TMP_3 TMP_6
  81 H3)))))))))))))))).
  82
  83 theorem wf3_ty3_conf:
  84  \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((ty3 g c1
  85 t1 t2) \to (\forall (c2: C).((wf3 g c1 c2) \to (ty3 g c2 t1 t2)))))))
  86 \def
  87  \lambda (g: G).(\lambda (c1: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda
  88 (H: (ty3 g c1 t1 t2)).(let TMP_1 \def (\lambda (c: C).(\lambda (t:
  89 T).(\lambda (t0: T).(\forall (c2: C).((wf3 g c c2) \to (ty3 g c2 t t0))))))
  90 in (let TMP_9 \def (\lambda (c: C).(\lambda (t3: T).(\lambda (t: T).(\lambda
  91 (H0: (ty3 g c t3 t)).(\lambda (H1: ((\forall (c2: C).((wf3 g c c2) \to (ty3 g
  92 c2 t3 t))))).(\lambda (u: T).(\lambda (t4: T).(\lambda (H2: (ty3 g c u
  93 t4)).(\lambda (H3: ((\forall (c2: C).((wf3 g c c2) \to (ty3 g c2 u
  94 t4))))).(\lambda (H4: (pc3 c t4 t3)).(\lambda (c2: C).(\lambda (H5: (wf3 g c
  95 c2)).(let TMP_2 \def (\lambda (t0: T).(ty3 g c t4 t0)) in (let TMP_3 \def
  96 (ty3 g c2 u t3) in (let TMP_7 \def (\lambda (x: T).(\lambda (H6: (ty3 g c t4
  97 x)).(let TMP_4 \def (H1 c2 H5) in (let TMP_5 \def (H3 c2 H5) in (let TMP_6
  98 \def (wf3_pc3_conf g c t4 t3 H4 c2 H5 x H6 t H0) in (ty3_conv g c2 t3 t TMP_4
  99 u t4 TMP_5 TMP_6)))))) in (let TMP_8 \def (ty3_correct g c u t4 H2) in
 100 (ex_ind T TMP_2 TMP_3 TMP_7 TMP_8))))))))))))))))) in (let TMP_10 \def
 101 (\lambda (c: C).(\lambda (m: nat).(\lambda (c2: C).(\lambda (_: (wf3 g c
 102 c2)).(ty3_sort g c2 m))))) in (let TMP_21 \def (\lambda (n: nat).(\lambda (c:
 103 C).(\lambda (d: C).(\lambda (u: T).(\lambda (H0: (getl n c (CHead d (Bind
 104 Abbr) u))).(\lambda (t: T).(\lambda (H1: (ty3 g d u t)).(\lambda (H2:
 105 ((\forall (c2: C).((wf3 g d c2) \to (ty3 g c2 u t))))).(\lambda (c2:
 106 C).(\lambda (H3: (wf3 g c c2)).(let H_x \def (wf3_getl_conf Abbr n c d u H0 g
 107 c2 H3 t H1) in (let H4 \def H_x in (let TMP_13 \def (\lambda (d2: C).(let
 108 TMP_11 \def (Bind Abbr) in (let TMP_12 \def (CHead d2 TMP_11 u) in (getl n c2
 109 TMP_12)))) in (let TMP_14 \def (\lambda (d2: C).(wf3 g d d2)) in (let TMP_15
 110 \def (TLRef n) in (let TMP_16 \def (S n) in (let TMP_17 \def (lift TMP_16 O
 111 t) in (let TMP_18 \def (ty3 g c2 TMP_15 TMP_17) in (let TMP_20 \def (\lambda
 112 (x: C).(\lambda (H5: (getl n c2 (CHead x (Bind Abbr) u))).(\lambda (H6: (wf3
 113 g d x)).(let TMP_19 \def (H2 x H6) in (ty3_abbr g n c2 x u H5 t TMP_19)))))
 114 in (ex2_ind C TMP_13 TMP_14 TMP_18 TMP_20 H4)))))))))))))))))))) in (let
 115 TMP_32 \def (\lambda (n: nat).(\lambda (c: C).(\lambda (d: C).(\lambda (u:
 116 T).(\lambda (H0: (getl n c (CHead d (Bind Abst) u))).(\lambda (t: T).(\lambda
 117 (H1: (ty3 g d u t)).(\lambda (H2: ((\forall (c2: C).((wf3 g d c2) \to (ty3 g
 118 c2 u t))))).(\lambda (c2: C).(\lambda (H3: (wf3 g c c2)).(let H_x \def
 119 (wf3_getl_conf Abst n c d u H0 g c2 H3 t H1) in (let H4 \def H_x in (let
 120 TMP_24 \def (\lambda (d2: C).(let TMP_22 \def (Bind Abst) in (let TMP_23 \def
 121 (CHead d2 TMP_22 u) in (getl n c2 TMP_23)))) in (let TMP_25 \def (\lambda
 122 (d2: C).(wf3 g d d2)) in (let TMP_26 \def (TLRef n) in (let TMP_27 \def (S n)
 123 in (let TMP_28 \def (lift TMP_27 O u) in (let TMP_29 \def (ty3 g c2 TMP_26
 124 TMP_28) in (let TMP_31 \def (\lambda (x: C).(\lambda (H5: (getl n c2 (CHead x
 125 (Bind Abst) u))).(\lambda (H6: (wf3 g d x)).(let TMP_30 \def (H2 x H6) in
 126 (ty3_abst g n c2 x u H5 t TMP_30))))) in (ex2_ind C TMP_24 TMP_25 TMP_29
 127 TMP_31 H4)))))))))))))))))))) in (let TMP_38 \def (\lambda (c: C).(\lambda
 128 (u: T).(\lambda (t: T).(\lambda (H0: (ty3 g c u t)).(\lambda (H1: ((\forall
 129 (c2: C).((wf3 g c c2) \to (ty3 g c2 u t))))).(\lambda (b: B).(\lambda (t3:
 130 T).(\lambda (t4: T).(\lambda (_: (ty3 g (CHead c (Bind b) u) t3 t4)).(\lambda
 131 (H3: ((\forall (c2: C).((wf3 g (CHead c (Bind b) u) c2) \to (ty3 g c2 t3
 132 t4))))).(\lambda (c2: C).(\lambda (H4: (wf3 g c c2)).(let TMP_33 \def (H1 c2
 133 H4) in (let TMP_34 \def (Bind b) in (let TMP_35 \def (CHead c2 TMP_34 u) in
 134 (let TMP_36 \def (wf3_bind g c c2 H4 u t H0 b) in (let TMP_37 \def (H3 TMP_35
 135 TMP_36) in (ty3_bind g c2 u t TMP_33 b t3 t4 TMP_37)))))))))))))))))) in (let
 136 TMP_41 \def (\lambda (c: C).(\lambda (w: T).(\lambda (u: T).(\lambda (_: (ty3
 137 g c w u)).(\lambda (H1: ((\forall (c2: C).((wf3 g c c2) \to (ty3 g c2 w
 138 u))))).(\lambda (v: T).(\lambda (t: T).(\lambda (_: (ty3 g c v (THead (Bind
 139 Abst) u t))).(\lambda (H3: ((\forall (c2: C).((wf3 g c c2) \to (ty3 g c2 v
 140 (THead (Bind Abst) u t)))))).(\lambda (c2: C).(\lambda (H4: (wf3 g c
 141 c2)).(let TMP_39 \def (H1 c2 H4) in (let TMP_40 \def (H3 c2 H4) in (ty3_appl
 142 g c2 w u TMP_39 v t TMP_40)))))))))))))) in (let TMP_44 \def (\lambda (c:
 143 C).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (ty3 g c t3 t4)).(\lambda
 144 (H1: ((\forall (c2: C).((wf3 g c c2) \to (ty3 g c2 t3 t4))))).(\lambda (t0:
 145 T).(\lambda (_: (ty3 g c t4 t0)).(\lambda (H3: ((\forall (c2: C).((wf3 g c
 146 c2) \to (ty3 g c2 t4 t0))))).(\lambda (c2: C).(\lambda (H4: (wf3 g c
 147 c2)).(let TMP_42 \def (H1 c2 H4) in (let TMP_43 \def (H3 c2 H4) in (ty3_cast
 148 g c2 t3 t4 TMP_42 t0 TMP_43))))))))))))) in (ty3_ind g TMP_1 TMP_9 TMP_10
 149 TMP_21 TMP_32 TMP_38 TMP_41 TMP_44 c1 t1 t2 H))))))))))))).
 150