matita/matita/contribs/lambdadelta/basic_1/pc3/props.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/pc3/defs.ma".
  18
  19 include "Basic-1/pr3/pr3.ma".
  20
  21 theorem clear_pc3_trans:
  22  \forall (c2: C).(\forall (t1: T).(\forall (t2: T).((pc3 c2 t1 t2) \to
  23 (\forall (c1: C).((clear c1 c2) \to (pc3 c1 t1 t2))))))
  24 \def
  25  \lambda (c2: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pc3 c2 t1
  26 t2)).(\lambda (c1: C).(\lambda (H0: (clear c1 c2)).(let H1 \def H in (ex2_ind
  27 T (\lambda (t: T).(pr3 c2 t1 t)) (\lambda (t: T).(pr3 c2 t2 t)) (pc3 c1 t1
  28 t2) (\lambda (x: T).(\lambda (H2: (pr3 c2 t1 x)).(\lambda (H3: (pr3 c2 t2
  29 x)).(ex_intro2 T (\lambda (t: T).(pr3 c1 t1 t)) (\lambda (t: T).(pr3 c1 t2
  30 t)) x (clear_pr3_trans c2 t1 x H2 c1 H0) (clear_pr3_trans c2 t2 x H3 c1
  31 H0))))) H1))))))).
  32 (* COMMENTS
  33 Initial nodes: 129
  34 END *)
  35
  36 theorem pc3_pr2_r:
  37  \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr2 c t1 t2) \to (pc3 c
  38 t1 t2))))
  39 \def
  40  \lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr2 c t1
  41 t2)).(ex_intro2 T (\lambda (t: T).(pr3 c t1 t)) (\lambda (t: T).(pr3 c t2 t))
  42 t2 (pr3_pr2 c t1 t2 H) (pr3_refl c t2))))).
  43 (* COMMENTS
  44 Initial nodes: 55
  45 END *)
  46
  47 theorem pc3_pr2_x:
  48  \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr2 c t2 t1) \to (pc3 c
  49 t1 t2))))
  50 \def
  51  \lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr2 c t2
  52 t1)).(ex_intro2 T (\lambda (t: T).(pr3 c t1 t)) (\lambda (t: T).(pr3 c t2 t))
  53 t1 (pr3_refl c t1) (pr3_pr2 c t2 t1 H))))).
  54 (* COMMENTS
  55 Initial nodes: 55
  56 END *)
  57
  58 theorem pc3_pr3_r:
  59  \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr3 c t1 t2) \to (pc3 c
  60 t1 t2))))
  61 \def
  62  \lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr3 c t1
  63 t2)).(ex_intro2 T (\lambda (t: T).(pr3 c t1 t)) (\lambda (t: T).(pr3 c t2 t))
  64 t2 H (pr3_refl c t2))))).
  65 (* COMMENTS
  66 Initial nodes: 47
  67 END *)
  68
  69 theorem pc3_pr3_x:
  70  \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr3 c t2 t1) \to (pc3 c
  71 t1 t2))))
  72 \def
  73  \lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr3 c t2
  74 t1)).(ex_intro2 T (\lambda (t: T).(pr3 c t1 t)) (\lambda (t: T).(pr3 c t2 t))
  75 t1 (pr3_refl c t1) H)))).
  76 (* COMMENTS
  77 Initial nodes: 47
  78 END *)
  79
  80 theorem pc3_pr3_t:
  81  \forall (c: C).(\forall (t1: T).(\forall (t0: T).((pr3 c t1 t0) \to (\forall
  82 (t2: T).((pr3 c t2 t0) \to (pc3 c t1 t2))))))
  83 \def
  84  \lambda (c: C).(\lambda (t1: T).(\lambda (t0: T).(\lambda (H: (pr3 c t1
  85 t0)).(\lambda (t2: T).(\lambda (H0: (pr3 c t2 t0)).(ex_intro2 T (\lambda (t:
  86 T).(pr3 c t1 t)) (\lambda (t: T).(pr3 c t2 t)) t0 H H0)))))).
  87 (* COMMENTS
  88 Initial nodes: 53
  89 END *)
  90
  91 theorem pc3_refl:
  92  \forall (c: C).(\forall (t: T).(pc3 c t t))
  93 \def
  94  \lambda (c: C).(\lambda (t: T).(ex_intro2 T (\lambda (t0: T).(pr3 c t t0))
  95 (\lambda (t0: T).(pr3 c t t0)) t (pr3_refl c t) (pr3_refl c t))).
  96 (* COMMENTS
  97 Initial nodes: 41
  98 END *)
  99
 100 theorem pc3_s:
 101  \forall (c: C).(\forall (t2: T).(\forall (t1: T).((pc3 c t1 t2) \to (pc3 c
 102 t2 t1))))
 103 \def
 104  \lambda (c: C).(\lambda (t2: T).(\lambda (t1: T).(\lambda (H: (pc3 c t1
 105 t2)).(let H0 \def H in (ex2_ind T (\lambda (t: T).(pr3 c t1 t)) (\lambda (t:
 106 T).(pr3 c t2 t)) (pc3 c t2 t1) (\lambda (x: T).(\lambda (H1: (pr3 c t1
 107 x)).(\lambda (H2: (pr3 c t2 x)).(ex_intro2 T (\lambda (t: T).(pr3 c t2 t))
 108 (\lambda (t: T).(pr3 c t1 t)) x H2 H1)))) H0))))).
 109 (* COMMENTS
 110 Initial nodes: 97
 111 END *)
 112
 113 theorem pc3_thin_dx:
 114  \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pc3 c t1 t2) \to (\forall
 115 (u: T).(\forall (f: F).(pc3 c (THead (Flat f) u t1) (THead (Flat f) u
 116 t2)))))))
 117 \def
 118  \lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pc3 c t1
 119 t2)).(\lambda (u: T).(\lambda (f: F).(let H0 \def H in (ex2_ind T (\lambda
 120 (t: T).(pr3 c t1 t)) (\lambda (t: T).(pr3 c t2 t)) (pc3 c (THead (Flat f) u
 121 t1) (THead (Flat f) u t2)) (\lambda (x: T).(\lambda (H1: (pr3 c t1
 122 x)).(\lambda (H2: (pr3 c t2 x)).(ex_intro2 T (\lambda (t: T).(pr3 c (THead
 123 (Flat f) u t1) t)) (\lambda (t: T).(pr3 c (THead (Flat f) u t2) t)) (THead
 124 (Flat f) u x) (pr3_thin_dx c t1 x H1 u f) (pr3_thin_dx c t2 x H2 u f)))))
 125 H0))))))).
 126 (* COMMENTS
 127 Initial nodes: 165
 128 END *)
 129
 130 theorem pc3_head_1:
 131  \forall (c: C).(\forall (u1: T).(\forall (u2: T).((pc3 c u1 u2) \to (\forall
 132 (k: K).(\forall (t: T).(pc3 c (THead k u1 t) (THead k u2 t)))))))
 133 \def
 134  \lambda (c: C).(\lambda (u1: T).(\lambda (u2: T).(\lambda (H: (pc3 c u1
 135 u2)).(\lambda (k: K).(\lambda (t: T).(let H0 \def H in (ex2_ind T (\lambda
 136 (t0: T).(pr3 c u1 t0)) (\lambda (t0: T).(pr3 c u2 t0)) (pc3 c (THead k u1 t)
 137 (THead k u2 t)) (\lambda (x: T).(\lambda (H1: (pr3 c u1 x)).(\lambda (H2:
 138 (pr3 c u2 x)).(ex_intro2 T (\lambda (t0: T).(pr3 c (THead k u1 t) t0))
 139 (\lambda (t0: T).(pr3 c (THead k u2 t) t0)) (THead k x t) (pr3_head_12 c u1 x
 140 H1 k t t (pr3_refl (CHead c k x) t)) (pr3_head_12 c u2 x H2 k t t (pr3_refl
 141 (CHead c k x) t)))))) H0))))))).
 142 (* COMMENTS
 143 Initial nodes: 183
 144 END *)
 145
 146 theorem pc3_head_2:
 147  \forall (c: C).(\forall (u: T).(\forall (t1: T).(\forall (t2: T).(\forall
 148 (k: K).((pc3 (CHead c k u) t1 t2) \to (pc3 c (THead k u t1) (THead k u
 149 t2)))))))
 150 \def
 151  \lambda (c: C).(\lambda (u: T).(\lambda (t1: T).(\lambda (t2: T).(\lambda
 152 (k: K).(\lambda (H: (pc3 (CHead c k u) t1 t2)).(let H0 \def H in (ex2_ind T
 153 (\lambda (t: T).(pr3 (CHead c k u) t1 t)) (\lambda (t: T).(pr3 (CHead c k u)
 154 t2 t)) (pc3 c (THead k u t1) (THead k u t2)) (\lambda (x: T).(\lambda (H1:
 155 (pr3 (CHead c k u) t1 x)).(\lambda (H2: (pr3 (CHead c k u) t2 x)).(ex_intro2
 156 T (\lambda (t: T).(pr3 c (THead k u t1) t)) (\lambda (t: T).(pr3 c (THead k u
 157 t2) t)) (THead k u x) (pr3_head_12 c u u (pr3_refl c u) k t1 x H1)
 158 (pr3_head_12 c u u (pr3_refl c u) k t2 x H2))))) H0))))))).
 159 (* COMMENTS
 160 Initial nodes: 201
 161 END *)
 162
 163 theorem pc3_pr2_u:
 164  \forall (c: C).(\forall (t2: T).(\forall (t1: T).((pr2 c t1 t2) \to (\forall
 165 (t3: T).((pc3 c t2 t3) \to (pc3 c t1 t3))))))
 166 \def
 167  \lambda (c: C).(\lambda (t2: T).(\lambda (t1: T).(\lambda (H: (pr2 c t1
 168 t2)).(\lambda (t3: T).(\lambda (H0: (pc3 c t2 t3)).(let H1 \def H0 in
 169 (ex2_ind T (\lambda (t: T).(pr3 c t2 t)) (\lambda (t: T).(pr3 c t3 t)) (pc3 c
 170 t1 t3) (\lambda (x: T).(\lambda (H2: (pr3 c t2 x)).(\lambda (H3: (pr3 c t3
 171 x)).(ex_intro2 T (\lambda (t: T).(pr3 c t1 t)) (\lambda (t: T).(pr3 c t3 t))
 172 x (pr3_sing c t2 t1 H x H2) H3)))) H1))))))).
 173 (* COMMENTS
 174 Initial nodes: 119
 175 END *)
 176
 177 theorem pc3_t:
 178  \forall (t2: T).(\forall (c: C).(\forall (t1: T).((pc3 c t1 t2) \to (\forall
 179 (t3: T).((pc3 c t2 t3) \to (pc3 c t1 t3))))))
 180 \def
 181  \lambda (t2: T).(\lambda (c: C).(\lambda (t1: T).(\lambda (H: (pc3 c t1
 182 t2)).(\lambda (t3: T).(\lambda (H0: (pc3 c t2 t3)).(let H1 \def H0 in
 183 (ex2_ind T (\lambda (t: T).(pr3 c t2 t)) (\lambda (t: T).(pr3 c t3 t)) (pc3 c
 184 t1 t3) (\lambda (x: T).(\lambda (H2: (pr3 c t2 x)).(\lambda (H3: (pr3 c t3
 185 x)).(let H4 \def H in (ex2_ind T (\lambda (t: T).(pr3 c t1 t)) (\lambda (t:
 186 T).(pr3 c t2 t)) (pc3 c t1 t3) (\lambda (x0: T).(\lambda (H5: (pr3 c t1
 187 x0)).(\lambda (H6: (pr3 c t2 x0)).(ex2_ind T (\lambda (t: T).(pr3 c x0 t))
 188 (\lambda (t: T).(pr3 c x t)) (pc3 c t1 t3) (\lambda (x1: T).(\lambda (H7:
 189 (pr3 c x0 x1)).(\lambda (H8: (pr3 c x x1)).(pc3_pr3_t c t1 x1 (pr3_t x0 t1 c
 190 H5 x1 H7) t3 (pr3_t x t3 c H3 x1 H8))))) (pr3_confluence c t2 x0 H6 x H2)))))
 191 H4))))) H1))))))).
 192 (* COMMENTS
 193 Initial nodes: 233
 194 END *)
 195
 196 theorem pc3_pr2_u2:
 197  \forall (c: C).(\forall (t0: T).(\forall (t1: T).((pr2 c t0 t1) \to (\forall
 198 (t2: T).((pc3 c t0 t2) \to (pc3 c t1 t2))))))
 199 \def
 200  \lambda (c: C).(\lambda (t0: T).(\lambda (t1: T).(\lambda (H: (pr2 c t0
 201 t1)).(\lambda (t2: T).(\lambda (H0: (pc3 c t0 t2)).(pc3_t t0 c t1 (pc3_pr2_x
 202 c t1 t0 H) t2 H0)))))).
 203 (* COMMENTS
 204 Initial nodes: 45
 205 END *)
 206
 207 theorem pc3_pr3_conf:
 208  \forall (c: C).(\forall (t: T).(\forall (t1: T).((pc3 c t t1) \to (\forall
 209 (t2: T).((pr3 c t t2) \to (pc3 c t2 t1))))))
 210 \def
 211  \lambda (c: C).(\lambda (t: T).(\lambda (t1: T).(\lambda (H: (pc3 c t
 212 t1)).(\lambda (t2: T).(\lambda (H0: (pr3 c t t2)).(pc3_t t c t2 (pc3_pr3_x c
 213 t2 t H0) t1 H)))))).
 214 (* COMMENTS
 215 Initial nodes: 45
 216 END *)
 217
 218 theorem pc3_head_12:
 219  \forall (c: C).(\forall (u1: T).(\forall (u2: T).((pc3 c u1 u2) \to (\forall
 220 (k: K).(\forall (t1: T).(\forall (t2: T).((pc3 (CHead c k u2) t1 t2) \to (pc3
 221 c (THead k u1 t1) (THead k u2 t2)))))))))
 222 \def
 223  \lambda (c: C).(\lambda (u1: T).(\lambda (u2: T).(\lambda (H: (pc3 c u1
 224 u2)).(\lambda (k: K).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H0: (pc3
 225 (CHead c k u2) t1 t2)).(pc3_t (THead k u2 t1) c (THead k u1 t1) (pc3_head_1 c
 226 u1 u2 H k t1) (THead k u2 t2) (pc3_head_2 c u2 t1 t2 k H0))))))))).
 227 (* COMMENTS
 228 Initial nodes: 89
 229 END *)
 230
 231 theorem pc3_head_21:
 232  \forall (c: C).(\forall (u1: T).(\forall (u2: T).((pc3 c u1 u2) \to (\forall
 233 (k: K).(\forall (t1: T).(\forall (t2: T).((pc3 (CHead c k u1) t1 t2) \to (pc3
 234 c (THead k u1 t1) (THead k u2 t2)))))))))
 235 \def
 236  \lambda (c: C).(\lambda (u1: T).(\lambda (u2: T).(\lambda (H: (pc3 c u1
 237 u2)).(\lambda (k: K).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H0: (pc3
 238 (CHead c k u1) t1 t2)).(pc3_t (THead k u1 t2) c (THead k u1 t1) (pc3_head_2 c
 239 u1 t1 t2 k H0) (THead k u2 t2) (pc3_head_1 c u1 u2 H k t2))))))))).
 240 (* COMMENTS
 241 Initial nodes: 89
 242 END *)
 243
 244 theorem pc3_pr0_pr2_t:
 245  \forall (u1: T).(\forall (u2: T).((pr0 u2 u1) \to (\forall (c: C).(\forall
 246 (t1: T).(\forall (t2: T).(\forall (k: K).((pr2 (CHead c k u2) t1 t2) \to (pc3
 247 (CHead c k u1) t1 t2))))))))
 248 \def
 249  \lambda (u1: T).(\lambda (u2: T).(\lambda (H: (pr0 u2 u1)).(\lambda (c:
 250 C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (k: K).(\lambda (H0: (pr2
 251 (CHead c k u2) t1 t2)).(insert_eq C (CHead c k u2) (\lambda (c0: C).(pr2 c0
 252 t1 t2)) (\lambda (_: C).(pc3 (CHead c k u1) t1 t2)) (\lambda (y: C).(\lambda
 253 (H1: (pr2 y t1 t2)).(pr2_ind (\lambda (c0: C).(\lambda (t: T).(\lambda (t0:
 254 T).((eq C c0 (CHead c k u2)) \to (pc3 (CHead c k u1) t t0))))) (\lambda (c0:
 255 C).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H2: (pr0 t3 t4)).(\lambda (H3:
 256 (eq C c0 (CHead c k u2))).(let H4 \def (f_equal C C (\lambda (e: C).e) c0
 257 (CHead c k u2) H3) in (pc3_pr2_r (CHead c k u1) t3 t4 (pr2_free (CHead c k
 258 u1) t3 t4 H2)))))))) (\lambda (c0: C).(\lambda (d: C).(\lambda (u:
 259 T).(\lambda (i: nat).(\lambda (H2: (getl i c0 (CHead d (Bind Abbr)
 260 u))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H3: (pr0 t3 t4)).(\lambda
 261 (t: T).(\lambda (H4: (subst0 i u t4 t)).(\lambda (H5: (eq C c0 (CHead c k
 262 u2))).(let H6 \def (f_equal C C (\lambda (e: C).e) c0 (CHead c k u2) H5) in
 263 (let H7 \def (eq_ind C c0 (\lambda (c1: C).(getl i c1 (CHead d (Bind Abbr)
 264 u))) H2 (CHead c k u2) H6) in (nat_ind (\lambda (n: nat).((getl n (CHead c k
 265 u2) (CHead d (Bind Abbr) u)) \to ((subst0 n u t4 t) \to (pc3 (CHead c k u1)
 266 t3 t)))) (\lambda (H8: (getl O (CHead c k u2) (CHead d (Bind Abbr)
 267 u))).(\lambda (H9: (subst0 O u t4 t)).(K_ind (\lambda (k0: K).((clear (CHead
 268 c k0 u2) (CHead d (Bind Abbr) u)) \to (pc3 (CHead c k0 u1) t3 t))) (\lambda
 269 (b: B).(\lambda (H10: (clear (CHead c (Bind b) u2) (CHead d (Bind Abbr)
 270 u))).(let H11 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda
 271 (_: C).C) with [(CSort _) \Rightarrow d | (CHead c1 _ _) \Rightarrow c1]))
 272 (CHead d (Bind Abbr) u) (CHead c (Bind b) u2) (clear_gen_bind b c (CHead d
 273 (Bind Abbr) u) u2 H10)) in ((let H12 \def (f_equal C B (\lambda (e: C).(match
 274 e in C return (\lambda (_: C).B) with [(CSort _) \Rightarrow Abbr | (CHead _
 275 k0 _) \Rightarrow (match k0 in K return (\lambda (_: K).B) with [(Bind b0)
 276 \Rightarrow b0 | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr) u)
 277 (CHead c (Bind b) u2) (clear_gen_bind b c (CHead d (Bind Abbr) u) u2 H10)) in
 278 ((let H13 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_:
 279 C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) (CHead
 280 d (Bind Abbr) u) (CHead c (Bind b) u2) (clear_gen_bind b c (CHead d (Bind
 281 Abbr) u) u2 H10)) in (\lambda (H14: (eq B Abbr b)).(\lambda (_: (eq C d
 282 c)).(let H16 \def (eq_ind T u (\lambda (t0: T).(subst0 O t0 t4 t)) H9 u2 H13)
 283 in (eq_ind B Abbr (\lambda (b0: B).(pc3 (CHead c (Bind b0) u1) t3 t))
 284 (ex2_ind T (\lambda (t0: T).(subst0 O u1 t4 t0)) (\lambda (t0: T).(pr0 t t0))
 285 (pc3 (CHead c (Bind Abbr) u1) t3 t) (\lambda (x: T).(\lambda (H17: (subst0 O
 286 u1 t4 x)).(\lambda (H18: (pr0 t x)).(pc3_pr3_t (CHead c (Bind Abbr) u1) t3 x
 287 (pr3_pr2 (CHead c (Bind Abbr) u1) t3 x (pr2_delta (CHead c (Bind Abbr) u1) c
 288 u1 O (getl_refl Abbr c u1) t3 t4 H3 x H17)) t (pr3_pr2 (CHead c (Bind Abbr)
 289 u1) t x (pr2_free (CHead c (Bind Abbr) u1) t x H18)))))) (pr0_subst0_fwd u2
 290 t4 t O H16 u1 H)) b H14))))) H12)) H11)))) (\lambda (f: F).(\lambda (H10:
 291 (clear (CHead c (Flat f) u2) (CHead d (Bind Abbr) u))).(clear_pc3_trans
 292 (CHead d (Bind Abbr) u) t3 t (pc3_pr2_r (CHead d (Bind Abbr) u) t3 t
 293 (pr2_delta (CHead d (Bind Abbr) u) d u O (getl_refl Abbr d u) t3 t4 H3 t H9))
 294 (CHead c (Flat f) u1) (clear_flat c (CHead d (Bind Abbr) u) (clear_gen_flat f
 295 c (CHead d (Bind Abbr) u) u2 H10) f u1)))) k (getl_gen_O (CHead c k u2)
 296 (CHead d (Bind Abbr) u) H8)))) (\lambda (i0: nat).(\lambda (IHi: (((getl i0
 297 (CHead c k u2) (CHead d (Bind Abbr) u)) \to ((subst0 i0 u t4 t) \to (pc3
 298 (CHead c k u1) t3 t))))).(\lambda (H8: (getl (S i0) (CHead c k u2) (CHead d
 299 (Bind Abbr) u))).(\lambda (H9: (subst0 (S i0) u t4 t)).(K_ind (\lambda (k0:
 300 K).((((getl i0 (CHead c k0 u2) (CHead d (Bind Abbr) u)) \to ((subst0 i0 u t4
 301 t) \to (pc3 (CHead c k0 u1) t3 t)))) \to ((getl (r k0 i0) c (CHead d (Bind
 302 Abbr) u)) \to (pc3 (CHead c k0 u1) t3 t)))) (\lambda (b: B).(\lambda (_:
 303 (((getl i0 (CHead c (Bind b) u2) (CHead d (Bind Abbr) u)) \to ((subst0 i0 u
 304 t4 t) \to (pc3 (CHead c (Bind b) u1) t3 t))))).(\lambda (H10: (getl (r (Bind
 305 b) i0) c (CHead d (Bind Abbr) u))).(pc3_pr2_r (CHead c (Bind b) u1) t3 t
 306 (pr2_delta (CHead c (Bind b) u1) d u (S i0) (getl_head (Bind b) i0 c (CHead d
 307 (Bind Abbr) u) H10 u1) t3 t4 H3 t H9))))) (\lambda (f: F).(\lambda (_:
 308 (((getl i0 (CHead c (Flat f) u2) (CHead d (Bind Abbr) u)) \to ((subst0 i0 u
 309 t4 t) \to (pc3 (CHead c (Flat f) u1) t3 t))))).(\lambda (H10: (getl (r (Flat
 310 f) i0) c (CHead d (Bind Abbr) u))).(pc3_pr2_r (CHead c (Flat f) u1) t3 t
 311 (pr2_cflat c t3 t (pr2_delta c d u (r (Flat f) i0) H10 t3 t4 H3 t H9) f
 312 u1))))) k IHi (getl_gen_S k c (CHead d (Bind Abbr) u) u2 i0 H8)))))) i H7
 313 H4)))))))))))))) y t1 t2 H1))) H0)))))))).
 314 (* COMMENTS
 315 Initial nodes: 1533
 316 END *)
 317
 318 theorem pc3_pr2_pr2_t:
 319  \forall (c: C).(\forall (u1: T).(\forall (u2: T).((pr2 c u2 u1) \to (\forall
 320 (t1: T).(\forall (t2: T).(\forall (k: K).((pr2 (CHead c k u2) t1 t2) \to (pc3
 321 (CHead c k u1) t1 t2))))))))
 322 \def
 323  \lambda (c: C).(\lambda (u1: T).(\lambda (u2: T).(\lambda (H: (pr2 c u2
 324 u1)).(pr2_ind (\lambda (c0: C).(\lambda (t: T).(\lambda (t0: T).(\forall (t1:
 325 T).(\forall (t2: T).(\forall (k: K).((pr2 (CHead c0 k t) t1 t2) \to (pc3
 326 (CHead c0 k t0) t1 t2)))))))) (\lambda (c0: C).(\lambda (t1: T).(\lambda (t2:
 327 T).(\lambda (H0: (pr0 t1 t2)).(\lambda (t0: T).(\lambda (t3: T).(\lambda (k:
 328 K).(\lambda (H1: (pr2 (CHead c0 k t1) t0 t3)).(pc3_pr0_pr2_t t2 t1 H0 c0 t0
 329 t3 k H1))))))))) (\lambda (c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda
 330 (i: nat).(\lambda (H0: (getl i c0 (CHead d (Bind Abbr) u))).(\lambda (t1:
 331 T).(\lambda (t2: T).(\lambda (H1: (pr0 t1 t2)).(\lambda (t: T).(\lambda (H2:
 332 (subst0 i u t2 t)).(\lambda (t0: T).(\lambda (t3: T).(\lambda (k: K).(\lambda
 333 (H3: (pr2 (CHead c0 k t1) t0 t3)).(insert_eq C (CHead c0 k t1) (\lambda (c1:
 334 C).(pr2 c1 t0 t3)) (\lambda (_: C).(pc3 (CHead c0 k t) t0 t3)) (\lambda (y:
 335 C).(\lambda (H4: (pr2 y t0 t3)).(pr2_ind (\lambda (c1: C).(\lambda (t4:
 336 T).(\lambda (t5: T).((eq C c1 (CHead c0 k t1)) \to (pc3 (CHead c0 k t) t4
 337 t5))))) (\lambda (c1: C).(\lambda (t4: T).(\lambda (t5: T).(\lambda (H5: (pr0
 338 t4 t5)).(\lambda (_: (eq C c1 (CHead c0 k t1))).(pc3_pr2_r (CHead c0 k t) t4
 339 t5 (pr2_free (CHead c0 k t) t4 t5 H5))))))) (\lambda (c1: C).(\lambda (d0:
 340 C).(\lambda (u0: T).(\lambda (i0: nat).(\lambda (H5: (getl i0 c1 (CHead d0
 341 (Bind Abbr) u0))).(\lambda (t4: T).(\lambda (t5: T).(\lambda (H6: (pr0 t4
 342 t5)).(\lambda (t6: T).(\lambda (H7: (subst0 i0 u0 t5 t6)).(\lambda (H8: (eq C
 343 c1 (CHead c0 k t1))).(let H9 \def (eq_ind C c1 (\lambda (c2: C).(getl i0 c2
 344 (CHead d0 (Bind Abbr) u0))) H5 (CHead c0 k t1) H8) in (nat_ind (\lambda (n:
 345 nat).((getl n (CHead c0 k t1) (CHead d0 (Bind Abbr) u0)) \to ((subst0 n u0 t5
 346 t6) \to (pc3 (CHead c0 k t) t4 t6)))) (\lambda (H10: (getl O (CHead c0 k t1)
 347 (CHead d0 (Bind Abbr) u0))).(\lambda (H11: (subst0 O u0 t5 t6)).(K_ind
 348 (\lambda (k0: K).((clear (CHead c0 k0 t1) (CHead d0 (Bind Abbr) u0)) \to (pc3
 349 (CHead c0 k0 t) t4 t6))) (\lambda (b: B).(\lambda (H12: (clear (CHead c0
 350 (Bind b) t1) (CHead d0 (Bind Abbr) u0))).(let H13 \def (f_equal C C (\lambda
 351 (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d0
 352 | (CHead c2 _ _) \Rightarrow c2])) (CHead d0 (Bind Abbr) u0) (CHead c0 (Bind
 353 b) t1) (clear_gen_bind b c0 (CHead d0 (Bind Abbr) u0) t1 H12)) in ((let H14
 354 \def (f_equal C B (\lambda (e: C).(match e in C return (\lambda (_: C).B)
 355 with [(CSort _) \Rightarrow Abbr | (CHead _ k0 _) \Rightarrow (match k0 in K
 356 return (\lambda (_: K).B) with [(Bind b0) \Rightarrow b0 | (Flat _)
 357 \Rightarrow Abbr])])) (CHead d0 (Bind Abbr) u0) (CHead c0 (Bind b) t1)
 358 (clear_gen_bind b c0 (CHead d0 (Bind Abbr) u0) t1 H12)) in ((let H15 \def
 359 (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with
 360 [(CSort _) \Rightarrow u0 | (CHead _ _ t7) \Rightarrow t7])) (CHead d0 (Bind
 361 Abbr) u0) (CHead c0 (Bind b) t1) (clear_gen_bind b c0 (CHead d0 (Bind Abbr)
 362 u0) t1 H12)) in (\lambda (H16: (eq B Abbr b)).(\lambda (_: (eq C d0 c0)).(let
 363 H18 \def (eq_ind T u0 (\lambda (t7: T).(subst0 O t7 t5 t6)) H11 t1 H15) in
 364 (eq_ind B Abbr (\lambda (b0: B).(pc3 (CHead c0 (Bind b0) t) t4 t6)) (ex2_ind
 365 T (\lambda (t7: T).(subst0 O t2 t5 t7)) (\lambda (t7: T).(pr0 t6 t7)) (pc3
 366 (CHead c0 (Bind Abbr) t) t4 t6) (\lambda (x: T).(\lambda (H19: (subst0 O t2
 367 t5 x)).(\lambda (H20: (pr0 t6 x)).(ex2_ind T (\lambda (t7: T).(subst0 O t t5
 368 t7)) (\lambda (t7: T).(subst0 (S (plus i O)) u x t7)) (pc3 (CHead c0 (Bind
 369 Abbr) t) t4 t6) (\lambda (x0: T).(\lambda (H21: (subst0 O t t5 x0)).(\lambda
 370 (H22: (subst0 (S (plus i O)) u x x0)).(let H23 \def (f_equal nat nat S (plus
 371 i O) i (sym_eq nat i (plus i O) (plus_n_O i))) in (let H24 \def (eq_ind nat
 372 (S (plus i O)) (\lambda (n: nat).(subst0 n u x x0)) H22 (S i) H23) in
 373 (pc3_pr2_u (CHead c0 (Bind Abbr) t) x0 t4 (pr2_delta (CHead c0 (Bind Abbr) t)
 374 c0 t O (getl_refl Abbr c0 t) t4 t5 H6 x0 H21) t6 (pc3_pr2_x (CHead c0 (Bind
 375 Abbr) t) x0 t6 (pr2_delta (CHead c0 (Bind Abbr) t) d u (S i) (getl_head (Bind
 376 Abbr) i c0 (CHead d (Bind Abbr) u) H0 t) t6 x H20 x0 H24))))))))
 377 (subst0_subst0_back t5 x t2 O H19 t u i H2))))) (pr0_subst0_fwd t1 t5 t6 O
 378 H18 t2 H1)) b H16))))) H14)) H13)))) (\lambda (f: F).(\lambda (H12: (clear
 379 (CHead c0 (Flat f) t1) (CHead d0 (Bind Abbr) u0))).(clear_pc3_trans (CHead d0
 380 (Bind Abbr) u0) t4 t6 (pc3_pr2_r (CHead d0 (Bind Abbr) u0) t4 t6 (pr2_delta
 381 (CHead d0 (Bind Abbr) u0) d0 u0 O (getl_refl Abbr d0 u0) t4 t5 H6 t6 H11))
 382 (CHead c0 (Flat f) t) (clear_flat c0 (CHead d0 (Bind Abbr) u0)
 383 (clear_gen_flat f c0 (CHead d0 (Bind Abbr) u0) t1 H12) f t)))) k (getl_gen_O
 384 (CHead c0 k t1) (CHead d0 (Bind Abbr) u0) H10)))) (\lambda (i1: nat).(\lambda
 385 (_: (((getl i1 (CHead c0 k t1) (CHead d0 (Bind Abbr) u0)) \to ((subst0 i1 u0
 386 t5 t6) \to (pc3 (CHead c0 k t) t4 t6))))).(\lambda (H10: (getl (S i1) (CHead
 387 c0 k t1) (CHead d0 (Bind Abbr) u0))).(\lambda (H11: (subst0 (S i1) u0 t5
 388 t6)).(K_ind (\lambda (k0: K).((getl (r k0 i1) c0 (CHead d0 (Bind Abbr) u0))
 389 \to (pc3 (CHead c0 k0 t) t4 t6))) (\lambda (b: B).(\lambda (H12: (getl (r
 390 (Bind b) i1) c0 (CHead d0 (Bind Abbr) u0))).(pc3_pr2_r (CHead c0 (Bind b) t)
 391 t4 t6 (pr2_delta (CHead c0 (Bind b) t) d0 u0 (S i1) (getl_head (Bind b) i1 c0
 392 (CHead d0 (Bind Abbr) u0) H12 t) t4 t5 H6 t6 H11)))) (\lambda (f: F).(\lambda
 393 (H12: (getl (r (Flat f) i1) c0 (CHead d0 (Bind Abbr) u0))).(pc3_pr2_r (CHead
 394 c0 (Flat f) t) t4 t6 (pr2_cflat c0 t4 t6 (pr2_delta c0 d0 u0 (r (Flat f) i1)
 395 H12 t4 t5 H6 t6 H11) f t)))) k (getl_gen_S k c0 (CHead d0 (Bind Abbr) u0) t1
 396 i1 H10)))))) i0 H9 H7))))))))))))) y t0 t3 H4))) H3))))))))))))))) c u2 u1
 397 H)))).
 398 (* COMMENTS
 399 Initial nodes: 1671
 400 END *)
 401
 402 theorem pc3_pr2_pr3_t:
 403  \forall (c: C).(\forall (u2: T).(\forall (t1: T).(\forall (t2: T).(\forall
 404 (k: K).((pr3 (CHead c k u2) t1 t2) \to (\forall (u1: T).((pr2 c u2 u1) \to
 405 (pc3 (CHead c k u1) t1 t2))))))))
 406 \def
 407  \lambda (c: C).(\lambda (u2: T).(\lambda (t1: T).(\lambda (t2: T).(\lambda
 408 (k: K).(\lambda (H: (pr3 (CHead c k u2) t1 t2)).(pr3_ind (CHead c k u2)
 409 (\lambda (t: T).(\lambda (t0: T).(\forall (u1: T).((pr2 c u2 u1) \to (pc3
 410 (CHead c k u1) t t0))))) (\lambda (t: T).(\lambda (u1: T).(\lambda (_: (pr2 c
 411 u2 u1)).(pc3_refl (CHead c k u1) t)))) (\lambda (t0: T).(\lambda (t3:
 412 T).(\lambda (H0: (pr2 (CHead c k u2) t3 t0)).(\lambda (t4: T).(\lambda (_:
 413 (pr3 (CHead c k u2) t0 t4)).(\lambda (H2: ((\forall (u1: T).((pr2 c u2 u1)
 414 \to (pc3 (CHead c k u1) t0 t4))))).(\lambda (u1: T).(\lambda (H3: (pr2 c u2
 415 u1)).(pc3_t t0 (CHead c k u1) t3 (pc3_pr2_pr2_t c u1 u2 H3 t3 t0 k H0) t4 (H2
 416 u1 H3)))))))))) t1 t2 H)))))).
 417 (* COMMENTS
 418 Initial nodes: 199
 419 END *)
 420
 421 theorem pc3_pr3_pc3_t:
 422  \forall (c: C).(\forall (u1: T).(\forall (u2: T).((pr3 c u2 u1) \to (\forall
 423 (t1: T).(\forall (t2: T).(\forall (k: K).((pc3 (CHead c k u2) t1 t2) \to (pc3
 424 (CHead c k u1) t1 t2))))))))
 425 \def
 426  \lambda (c: C).(\lambda (u1: T).(\lambda (u2: T).(\lambda (H: (pr3 c u2
 427 u1)).(pr3_ind c (\lambda (t: T).(\lambda (t0: T).(\forall (t1: T).(\forall
 428 (t2: T).(\forall (k: K).((pc3 (CHead c k t) t1 t2) \to (pc3 (CHead c k t0) t1
 429 t2))))))) (\lambda (t: T).(\lambda (t1: T).(\lambda (t2: T).(\lambda (k:
 430 K).(\lambda (H0: (pc3 (CHead c k t) t1 t2)).H0))))) (\lambda (t2: T).(\lambda
 431 (t1: T).(\lambda (H0: (pr2 c t1 t2)).(\lambda (t3: T).(\lambda (_: (pr3 c t2
 432 t3)).(\lambda (H2: ((\forall (t4: T).(\forall (t5: T).(\forall (k: K).((pc3
 433 (CHead c k t2) t4 t5) \to (pc3 (CHead c k t3) t4 t5))))))).(\lambda (t0:
 434 T).(\lambda (t4: T).(\lambda (k: K).(\lambda (H3: (pc3 (CHead c k t1) t0
 435 t4)).(H2 t0 t4 k (let H4 \def H3 in (ex2_ind T (\lambda (t: T).(pr3 (CHead c
 436 k t1) t0 t)) (\lambda (t: T).(pr3 (CHead c k t1) t4 t)) (pc3 (CHead c k t2)
 437 t0 t4) (\lambda (x: T).(\lambda (H5: (pr3 (CHead c k t1) t0 x)).(\lambda (H6:
 438 (pr3 (CHead c k t1) t4 x)).(pc3_t x (CHead c k t2) t0 (pc3_pr2_pr3_t c t1 t0
 439 x k H5 t2 H0) t4 (pc3_s (CHead c k t2) x t4 (pc3_pr2_pr3_t c t1 t4 x k H6 t2
 440 H0)))))) H4))))))))))))) u2 u1 H)))).
 441 (* COMMENTS
 442 Initial nodes: 319
 443 END *)
 444
 445 theorem pc3_lift:
 446  \forall (c: C).(\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h
 447 d c e) \to (\forall (t1: T).(\forall (t2: T).((pc3 e t1 t2) \to (pc3 c (lift
 448 h d t1) (lift h d t2)))))))))
 449 \def
 450  \lambda (c: C).(\lambda (e: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda
 451 (H: (drop h d c e)).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H0: (pc3 e t1
 452 t2)).(let H1 \def H0 in (ex2_ind T (\lambda (t: T).(pr3 e t1 t)) (\lambda (t:
 453 T).(pr3 e t2 t)) (pc3 c (lift h d t1) (lift h d t2)) (\lambda (x: T).(\lambda
 454 (H2: (pr3 e t1 x)).(\lambda (H3: (pr3 e t2 x)).(pc3_pr3_t c (lift h d t1)
 455 (lift h d x) (pr3_lift c e h d H t1 x H2) (lift h d t2) (pr3_lift c e h d H
 456 t2 x H3))))) H1))))))))).
 457 (* COMMENTS
 458 Initial nodes: 159
 459 END *)
 460
 461 theorem pc3_eta:
 462  \forall (c: C).(\forall (t: T).(\forall (w: T).(\forall (u: T).((pc3 c t
 463 (THead (Bind Abst) w u)) \to (\forall (v: T).((pc3 c v w) \to (pc3 c (THead
 464 (Bind Abst) v (THead (Flat Appl) (TLRef O) (lift (S O) O t))) t)))))))
 465 \def
 466  \lambda (c: C).(\lambda (t: T).(\lambda (w: T).(\lambda (u: T).(\lambda (H:
 467 (pc3 c t (THead (Bind Abst) w u))).(\lambda (v: T).(\lambda (H0: (pc3 c v
 468 w)).(pc3_t (THead (Bind Abst) w (THead (Flat Appl) (TLRef O) (lift (S O) O
 469 (THead (Bind Abst) w u)))) c (THead (Bind Abst) v (THead (Flat Appl) (TLRef
 470 O) (lift (S O) O t))) (pc3_head_21 c v w H0 (Bind Abst) (THead (Flat Appl)
 471 (TLRef O) (lift (S O) O t)) (THead (Flat Appl) (TLRef O) (lift (S O) O (THead
 472 (Bind Abst) w u))) (pc3_thin_dx (CHead c (Bind Abst) v) (lift (S O) O t)
 473 (lift (S O) O (THead (Bind Abst) w u)) (pc3_lift (CHead c (Bind Abst) v) c (S
 474 O) O (drop_drop (Bind Abst) O c c (drop_refl c) v) t (THead (Bind Abst) w u)
 475 H) (TLRef O) Appl)) t (pc3_t (THead (Bind Abst) w u) c (THead (Bind Abst) w
 476 (THead (Flat Appl) (TLRef O) (lift (S O) O (THead (Bind Abst) w u))))
 477 (pc3_pr3_r c (THead (Bind Abst) w (THead (Flat Appl) (TLRef O) (lift (S O) O
 478 (THead (Bind Abst) w u)))) (THead (Bind Abst) w u) (pr3_eta c w u w (pr3_refl
 479 c w))) t (pc3_s c (THead (Bind Abst) w u) t H))))))))).
 480 (* COMMENTS
 481 Initial nodes: 399
 482 END *)
 483