helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/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/LambdaDelta-1/pc3/dec".
  18
  19 include "ty3/arity_props.ma".
  20
  21 include "ty3/pr3.ma".
  22
  23 include "nf2/fwd.ma".
  24
  25 theorem pc3_dec:
  26  \forall (g: G).(\forall (c: C).(\forall (u1: T).(\forall (t1: T).((ty3 g c
  27 u1 t1) \to (\forall (u2: T).(\forall (t2: T).((ty3 g c u2 t2) \to (or (pc3 c
  28 u1 u2) ((pc3 c u1 u2) \to False)))))))))
  29 \def
  30  \lambda (g: G).(\lambda (c: C).(\lambda (u1: T).(\lambda (t1: T).(\lambda
  31 (H: (ty3 g c u1 t1)).(\lambda (u2: T).(\lambda (t2: T).(\lambda (H0: (ty3 g c
  32 u2 t2)).(let H_y \def (ty3_sn3 g c u1 t1 H) in (let H_y0 \def (ty3_sn3 g c u2
  33 t2 H0) in (let H_x \def (nf2_sn3 c u1 H_y) in (let H1 \def H_x in (ex2_ind T
  34 (\lambda (u: T).(pr3 c u1 u)) (\lambda (u: T).(nf2 c u)) (or (pc3 c u1 u2)
  35 ((pc3 c u1 u2) \to False)) (\lambda (x: T).(\lambda (H2: (pr3 c u1
  36 x)).(\lambda (H3: (nf2 c x)).(let H_x0 \def (nf2_sn3 c u2 H_y0) in (let H4
  37 \def H_x0 in (ex2_ind T (\lambda (u: T).(pr3 c u2 u)) (\lambda (u: T).(nf2 c
  38 u)) (or (pc3 c u1 u2) ((pc3 c u1 u2) \to False)) (\lambda (x0: T).(\lambda
  39 (H5: (pr3 c u2 x0)).(\lambda (H6: (nf2 c x0)).(let H_x1 \def (term_dec x x0)
  40 in (let H7 \def H_x1 in (or_ind (eq T x x0) ((eq T x x0) \to (\forall (P:
  41 Prop).P)) (or (pc3 c u1 u2) ((pc3 c u1 u2) \to False)) (\lambda (H8: (eq T x
  42 x0)).(let H9 \def (eq_ind_r T x0 (\lambda (t: T).(nf2 c t)) H6 x H8) in (let
  43 H10 \def (eq_ind_r T x0 (\lambda (t: T).(pr3 c u2 t)) H5 x H8) in (or_introl
  44 (pc3 c u1 u2) ((pc3 c u1 u2) \to False) (pc3_pr3_t c u1 x H2 u2 H10)))))
  45 (\lambda (H8: (((eq T x x0) \to (\forall (P: Prop).P)))).(or_intror (pc3 c u1
  46 u2) ((pc3 c u1 u2) \to False) (\lambda (H9: (pc3 c u1 u2)).(let H10 \def H9
  47 in (ex2_ind T (\lambda (t: T).(pr3 c u1 t)) (\lambda (t: T).(pr3 c u2 t))
  48 False (\lambda (x1: T).(\lambda (H11: (pr3 c u1 x1)).(\lambda (H12: (pr3 c u2
  49 x1)).(let H_x2 \def (pr3_confluence c u2 x0 H5 x1 H12) in (let H13 \def H_x2
  50 in (ex2_ind T (\lambda (t: T).(pr3 c x0 t)) (\lambda (t: T).(pr3 c x1 t))
  51 False (\lambda (x2: T).(\lambda (H14: (pr3 c x0 x2)).(\lambda (H15: (pr3 c x1
  52 x2)).(let H_y1 \def (nf2_pr3_unfold c x0 x2 H14 H6) in (let H16 \def
  53 (eq_ind_r T x2 (\lambda (t: T).(pr3 c x1 t)) H15 x0 H_y1) in (let H17 \def
  54 (nf2_pr3_confluence c x H3 x0 H6 u1 H2) in (H8 (H17 (pr3_t x1 u1 c H11 x0
  55 H16)) False))))))) H13)))))) H10))))) H7)))))) H4)))))) H1)))))))))))).
  56
  57 theorem pc3_abst_dec:
  58  \forall (g: G).(\forall (c: C).(\forall (u1: T).(\forall (t1: T).((ty3 g c
  59 u1 t1) \to (\forall (u2: T).(\forall (t2: T).((ty3 g c u2 t2) \to (or (ex4_2
  60 T T (\lambda (u: T).(\lambda (_: T).(pc3 c u1 (THead (Bind Abst) u2 u))))
  61 (\lambda (u: T).(\lambda (v2: T).(ty3 g c (THead (Bind Abst) v2 u) t1)))
  62 (\lambda (_: T).(\lambda (v2: T).(pr3 c u2 v2))) (\lambda (_: T).(\lambda
  63 (v2: T).(nf2 c v2)))) (\forall (u: T).((pc3 c u1 (THead (Bind Abst) u2 u))
  64 \to False))))))))))
  65 \def
  66  \lambda (g: G).(\lambda (c: C).(\lambda (u1: T).(\lambda (t1: T).(\lambda
  67 (H: (ty3 g c u1 t1)).(\lambda (u2: T).(\lambda (t2: T).(\lambda (H0: (ty3 g c
  68 u2 t2)).(let H1 \def (ty3_sn3 g c u1 t1 H) in (let H2 \def (ty3_sn3 g c u2 t2
  69 H0) in (let H_x \def (nf2_sn3 c u1 H1) in (let H3 \def H_x in (ex2_ind T
  70 (\lambda (u: T).(pr3 c u1 u)) (\lambda (u: T).(nf2 c u)) (or (ex4_2 T T
  71 (\lambda (u: T).(\lambda (_: T).(pc3 c u1 (THead (Bind Abst) u2 u))))
  72 (\lambda (u: T).(\lambda (v2: T).(ty3 g c (THead (Bind Abst) v2 u) t1)))
  73 (\lambda (_: T).(\lambda (v2: T).(pr3 c u2 v2))) (\lambda (_: T).(\lambda
  74 (v2: T).(nf2 c v2)))) (\forall (u: T).((pc3 c u1 (THead (Bind Abst) u2 u))
  75 \to False))) (\lambda (x: T).(\lambda (H4: (pr3 c u1 x)).(\lambda (H5: (nf2 c
  76 x)).(let H_x0 \def (nf2_sn3 c u2 H2) in (let H6 \def H_x0 in (ex2_ind T
  77 (\lambda (u: T).(pr3 c u2 u)) (\lambda (u: T).(nf2 c u)) (or (ex4_2 T T
  78 (\lambda (u: T).(\lambda (_: T).(pc3 c u1 (THead (Bind Abst) u2 u))))
  79 (\lambda (u: T).(\lambda (v2: T).(ty3 g c (THead (Bind Abst) v2 u) t1)))
  80 (\lambda (_: T).(\lambda (v2: T).(pr3 c u2 v2))) (\lambda (_: T).(\lambda
  81 (v2: T).(nf2 c v2)))) (\forall (u: T).((pc3 c u1 (THead (Bind Abst) u2 u))
  82 \to False))) (\lambda (x0: T).(\lambda (H7: (pr3 c u2 x0)).(\lambda (H8: (nf2
  83 c x0)).(let H_x1 \def (abst_dec x x0) in (let H9 \def H_x1 in (or_ind (ex T
  84 (\lambda (t: T).(eq T x (THead (Bind Abst) x0 t)))) (\forall (t: T).((eq T x
  85 (THead (Bind Abst) x0 t)) \to (\forall (P: Prop).P))) (or (ex4_2 T T (\lambda
  86 (u: T).(\lambda (_: T).(pc3 c u1 (THead (Bind Abst) u2 u)))) (\lambda (u:
  87 T).(\lambda (v2: T).(ty3 g c (THead (Bind Abst) v2 u) t1))) (\lambda (_:
  88 T).(\lambda (v2: T).(pr3 c u2 v2))) (\lambda (_: T).(\lambda (v2: T).(nf2 c
  89 v2)))) (\forall (u: T).((pc3 c u1 (THead (Bind Abst) u2 u)) \to False)))
  90 (\lambda (H10: (ex T (\lambda (t: T).(eq T x (THead (Bind Abst) x0
  91 t))))).(ex_ind T (\lambda (t: T).(eq T x (THead (Bind Abst) x0 t))) (or
  92 (ex4_2 T T (\lambda (u: T).(\lambda (_: T).(pc3 c u1 (THead (Bind Abst) u2
  93 u)))) (\lambda (u: T).(\lambda (v2: T).(ty3 g c (THead (Bind Abst) v2 u)
  94 t1))) (\lambda (_: T).(\lambda (v2: T).(pr3 c u2 v2))) (\lambda (_:
  95 T).(\lambda (v2: T).(nf2 c v2)))) (\forall (u: T).((pc3 c u1 (THead (Bind
  96 Abst) u2 u)) \to False))) (\lambda (x1: T).(\lambda (H11: (eq T x (THead
  97 (Bind Abst) x0 x1))).(let H12 \def (eq_ind T x (\lambda (t: T).(nf2 c t)) H5
  98 (THead (Bind Abst) x0 x1) H11) in (let H13 \def (eq_ind T x (\lambda (t:
  99 T).(pr3 c u1 t)) H4 (THead (Bind Abst) x0 x1) H11) in (let H_y \def
 100 (ty3_sred_pr3 c u1 (THead (Bind Abst) x0 x1) H13 g t1 H) in (or_introl (ex4_2
 101 T T (\lambda (u: T).(\lambda (_: T).(pc3 c u1 (THead (Bind Abst) u2 u))))
 102 (\lambda (u: T).(\lambda (v2: T).(ty3 g c (THead (Bind Abst) v2 u) t1)))
 103 (\lambda (_: T).(\lambda (v2: T).(pr3 c u2 v2))) (\lambda (_: T).(\lambda
 104 (v2: T).(nf2 c v2)))) (\forall (u: T).((pc3 c u1 (THead (Bind Abst) u2 u))
 105 \to False)) (ex4_2_intro T T (\lambda (u: T).(\lambda (_: T).(pc3 c u1 (THead
 106 (Bind Abst) u2 u)))) (\lambda (u: T).(\lambda (v2: T).(ty3 g c (THead (Bind
 107 Abst) v2 u) t1))) (\lambda (_: T).(\lambda (v2: T).(pr3 c u2 v2))) (\lambda
 108 (_: T).(\lambda (v2: T).(nf2 c v2))) x1 x0 (pc3_pr3_t c u1 (THead (Bind Abst)
 109 x0 x1) H13 (THead (Bind Abst) u2 x1) (pr3_head_12 c u2 x0 H7 (Bind Abst) x1
 110 x1 (pr3_refl (CHead c (Bind Abst) x0) x1))) H_y H7 H8))))))) H10)) (\lambda
 111 (H10: ((\forall (t: T).((eq T x (THead (Bind Abst) x0 t)) \to (\forall (P:
 112 Prop).P))))).(or_intror (ex4_2 T T (\lambda (u: T).(\lambda (_: T).(pc3 c u1
 113 (THead (Bind Abst) u2 u)))) (\lambda (u: T).(\lambda (v2: T).(ty3 g c (THead
 114 (Bind Abst) v2 u) t1))) (\lambda (_: T).(\lambda (v2: T).(pr3 c u2 v2)))
 115 (\lambda (_: T).(\lambda (v2: T).(nf2 c v2)))) (\forall (u: T).((pc3 c u1
 116 (THead (Bind Abst) u2 u)) \to False)) (\lambda (u: T).(\lambda (H11: (pc3 c
 117 u1 (THead (Bind Abst) u2 u))).(let H12 \def H11 in (ex2_ind T (\lambda (t:
 118 T).(pr3 c u1 t)) (\lambda (t: T).(pr3 c (THead (Bind Abst) u2 u) t)) False
 119 (\lambda (x1: T).(\lambda (H13: (pr3 c u1 x1)).(\lambda (H14: (pr3 c (THead
 120 (Bind Abst) u2 u) x1)).(ex2_ind T (\lambda (t: T).(pr3 c x1 t)) (\lambda (t:
 121 T).(pr3 c x t)) False (\lambda (x2: T).(\lambda (H15: (pr3 c x1 x2)).(\lambda
 122 (H16: (pr3 c x x2)).(let H_y \def (nf2_pr3_unfold c x x2 H16 H5) in (let H17
 123 \def (eq_ind_r T x2 (\lambda (t: T).(pr3 c x1 t)) H15 x H_y) in (let H18 \def
 124 (pr3_gen_abst c u2 u x1 H14) in (ex3_2_ind T T (\lambda (u3: T).(\lambda (t3:
 125 T).(eq T x1 (THead (Bind Abst) u3 t3)))) (\lambda (u3: T).(\lambda (_:
 126 T).(pr3 c u2 u3))) (\lambda (_: T).(\lambda (t3: T).(\forall (b: B).(\forall
 127 (u0: T).(pr3 (CHead c (Bind b) u0) u t3))))) False (\lambda (x3: T).(\lambda
 128 (x4: T).(\lambda (H19: (eq T x1 (THead (Bind Abst) x3 x4))).(\lambda (H20:
 129 (pr3 c u2 x3)).(\lambda (_: ((\forall (b: B).(\forall (u0: T).(pr3 (CHead c
 130 (Bind b) u0) u x4))))).(let H22 \def (eq_ind T x1 (\lambda (t: T).(pr3 c t
 131 x)) H17 (THead (Bind Abst) x3 x4) H19) in (let H23 \def (pr3_gen_abst c x3 x4
 132 x H22) in (ex3_2_ind T T (\lambda (u3: T).(\lambda (t3: T).(eq T x (THead
 133 (Bind Abst) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr3 c x3 u3)))
 134 (\lambda (_: T).(\lambda (t3: T).(\forall (b: B).(\forall (u0: T).(pr3 (CHead
 135 c (Bind b) u0) x4 t3))))) False (\lambda (x5: T).(\lambda (x6: T).(\lambda
 136 (H24: (eq T x (THead (Bind Abst) x5 x6))).(\lambda (H25: (pr3 c x3
 137 x5)).(\lambda (_: ((\forall (b: B).(\forall (u0: T).(pr3 (CHead c (Bind b)
 138 u0) x4 x6))))).(let H27 \def (eq_ind T x (\lambda (t: T).(\forall (t0:
 139 T).((eq T t (THead (Bind Abst) x0 t0)) \to (\forall (P: Prop).P)))) H10
 140 (THead (Bind Abst) x5 x6) H24) in (let H28 \def (eq_ind T x (\lambda (t:
 141 T).(nf2 c t)) H5 (THead (Bind Abst) x5 x6) H24) in (let H29 \def
 142 (nf2_gen_abst c x5 x6 H28) in (and_ind (nf2 c x5) (nf2 (CHead c (Bind Abst)
 143 x5) x6) False (\lambda (H30: (nf2 c x5)).(\lambda (_: (nf2 (CHead c (Bind
 144 Abst) x5) x6)).(let H32 \def (nf2_pr3_confluence c x0 H8 x5 H30 u2 H7) in
 145 (H27 x6 (sym_eq T (THead (Bind Abst) x0 x6) (THead (Bind Abst) x5 x6)
 146 (f_equal3 K T T T THead (Bind Abst) (Bind Abst) x0 x5 x6 x6 (refl_equal K
 147 (Bind Abst)) (H32 (pr3_t x3 u2 c H20 x5 H25)) (refl_equal T x6))) False))))
 148 H29))))))))) H23)))))))) H18))))))) (pr3_confluence c u1 x1 H13 x H4)))))
 149 H12)))))) H9)))))) H6)))))) H3)))))))))))).
 150