matita/matita/contribs/lambdadelta/basic_1/pc1/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/pc1/defs.ma".
  18
  19 include "Basic-1/pr1/pr1.ma".
  20
  21 theorem pc1_pr0_r:
  22  \forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to (pc1 t1 t2)))
  23 \def
  24  \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr0 t1 t2)).(ex_intro2 T
  25 (\lambda (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t2 t)) t2 (pr1_pr0 t1 t2 H)
  26 (pr1_refl t2)))).
  27 (* COMMENTS
  28 Initial nodes: 43
  29 END *)
  30
  31 theorem pc1_pr0_x:
  32  \forall (t1: T).(\forall (t2: T).((pr0 t2 t1) \to (pc1 t1 t2)))
  33 \def
  34  \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr0 t2 t1)).(ex_intro2 T
  35 (\lambda (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t2 t)) t1 (pr1_refl t1)
  36 (pr1_pr0 t2 t1 H)))).
  37 (* COMMENTS
  38 Initial nodes: 43
  39 END *)
  40
  41 theorem pc1_refl:
  42  \forall (t: T).(pc1 t t)
  43 \def
  44  \lambda (t: T).(ex_intro2 T (\lambda (t0: T).(pr1 t t0)) (\lambda (t0:
  45 T).(pr1 t t0)) t (pr1_refl t) (pr1_refl t)).
  46 (* COMMENTS
  47 Initial nodes: 31
  48 END *)
  49
  50 theorem pc1_pr0_u:
  51  \forall (t2: T).(\forall (t1: T).((pr0 t1 t2) \to (\forall (t3: T).((pc1 t2
  52 t3) \to (pc1 t1 t3)))))
  53 \def
  54  \lambda (t2: T).(\lambda (t1: T).(\lambda (H: (pr0 t1 t2)).(\lambda (t3:
  55 T).(\lambda (H0: (pc1 t2 t3)).(let H1 \def H0 in (ex2_ind T (\lambda (t:
  56 T).(pr1 t2 t)) (\lambda (t: T).(pr1 t3 t)) (pc1 t1 t3) (\lambda (x:
  57 T).(\lambda (H2: (pr1 t2 x)).(\lambda (H3: (pr1 t3 x)).(ex_intro2 T (\lambda
  58 (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t3 t)) x (pr1_sing t2 t1 H x H2)
  59 H3)))) H1)))))).
  60 (* COMMENTS
  61 Initial nodes: 97
  62 END *)
  63
  64 theorem pc1_s:
  65  \forall (t2: T).(\forall (t1: T).((pc1 t1 t2) \to (pc1 t2 t1)))
  66 \def
  67  \lambda (t2: T).(\lambda (t1: T).(\lambda (H: (pc1 t1 t2)).(let H0 \def H in
  68 (ex2_ind T (\lambda (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t2 t)) (pc1 t2
  69 t1) (\lambda (x: T).(\lambda (H1: (pr1 t1 x)).(\lambda (H2: (pr1 t2
  70 x)).(ex_intro2 T (\lambda (t: T).(pr1 t2 t)) (\lambda (t: T).(pr1 t1 t)) x H2
  71 H1)))) H0)))).
  72 (* COMMENTS
  73 Initial nodes: 79
  74 END *)
  75
  76 theorem pc1_head_1:
  77  \forall (u1: T).(\forall (u2: T).((pc1 u1 u2) \to (\forall (t: T).(\forall
  78 (k: K).(pc1 (THead k u1 t) (THead k u2 t))))))
  79 \def
  80  \lambda (u1: T).(\lambda (u2: T).(\lambda (H: (pc1 u1 u2)).(\lambda (t:
  81 T).(\lambda (k: K).(let H0 \def H in (ex2_ind T (\lambda (t0: T).(pr1 u1 t0))
  82 (\lambda (t0: T).(pr1 u2 t0)) (pc1 (THead k u1 t) (THead k u2 t)) (\lambda
  83 (x: T).(\lambda (H1: (pr1 u1 x)).(\lambda (H2: (pr1 u2 x)).(ex_intro2 T
  84 (\lambda (t0: T).(pr1 (THead k u1 t) t0)) (\lambda (t0: T).(pr1 (THead k u2
  85 t) t0)) (THead k x t) (pr1_head_1 u1 x H1 t k) (pr1_head_1 u2 x H2 t k)))))
  86 H0)))))).
  87 (* COMMENTS
  88 Initial nodes: 133
  89 END *)
  90
  91 theorem pc1_head_2:
  92  \forall (t1: T).(\forall (t2: T).((pc1 t1 t2) \to (\forall (u: T).(\forall
  93 (k: K).(pc1 (THead k u t1) (THead k u t2))))))
  94 \def
  95  \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pc1 t1 t2)).(\lambda (u:
  96 T).(\lambda (k: K).(let H0 \def H in (ex2_ind T (\lambda (t: T).(pr1 t1 t))
  97 (\lambda (t: T).(pr1 t2 t)) (pc1 (THead k u t1) (THead k u t2)) (\lambda (x:
  98 T).(\lambda (H1: (pr1 t1 x)).(\lambda (H2: (pr1 t2 x)).(ex_intro2 T (\lambda
  99 (t: T).(pr1 (THead k u t1) t)) (\lambda (t: T).(pr1 (THead k u t2) t)) (THead
 100 k u x) (pr1_head_2 t1 x H1 u k) (pr1_head_2 t2 x H2 u k))))) H0)))))).
 101 (* COMMENTS
 102 Initial nodes: 133
 103 END *)
 104
 105 theorem pc1_t:
 106  \forall (t2: T).(\forall (t1: T).((pc1 t1 t2) \to (\forall (t3: T).((pc1 t2
 107 t3) \to (pc1 t1 t3)))))
 108 \def
 109  \lambda (t2: T).(\lambda (t1: T).(\lambda (H: (pc1 t1 t2)).(\lambda (t3:
 110 T).(\lambda (H0: (pc1 t2 t3)).(let H1 \def H0 in (ex2_ind T (\lambda (t:
 111 T).(pr1 t2 t)) (\lambda (t: T).(pr1 t3 t)) (pc1 t1 t3) (\lambda (x:
 112 T).(\lambda (H2: (pr1 t2 x)).(\lambda (H3: (pr1 t3 x)).(let H4 \def H in
 113 (ex2_ind T (\lambda (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t2 t)) (pc1 t1
 114 t3) (\lambda (x0: T).(\lambda (H5: (pr1 t1 x0)).(\lambda (H6: (pr1 t2
 115 x0)).(ex2_ind T (\lambda (t: T).(pr1 x0 t)) (\lambda (t: T).(pr1 x t)) (pc1
 116 t1 t3) (\lambda (x1: T).(\lambda (H7: (pr1 x0 x1)).(\lambda (H8: (pr1 x
 117 x1)).(ex_intro2 T (\lambda (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t3 t)) x1
 118 (pr1_t x0 t1 H5 x1 H7) (pr1_t x t3 H3 x1 H8))))) (pr1_confluence t2 x0 H6 x
 119 H2))))) H4))))) H1)))))).
 120 (* COMMENTS
 121 Initial nodes: 203
 122 END *)
 123
 124 theorem pc1_pr0_u2:
 125  \forall (t0: T).(\forall (t1: T).((pr0 t0 t1) \to (\forall (t2: T).((pc1 t0
 126 t2) \to (pc1 t1 t2)))))
 127 \def
 128  \lambda (t0: T).(\lambda (t1: T).(\lambda (H: (pr0 t0 t1)).(\lambda (t2:
 129 T).(\lambda (H0: (pc1 t0 t2)).(pc1_t t0 t1 (pc1_pr0_x t1 t0 H) t2 H0))))).
 130 (* COMMENTS
 131 Initial nodes: 35
 132 END *)
 133
 134 theorem pc1_head:
 135  \forall (u1: T).(\forall (u2: T).((pc1 u1 u2) \to (\forall (t1: T).(\forall
 136 (t2: T).((pc1 t1 t2) \to (\forall (k: K).(pc1 (THead k u1 t1) (THead k u2
 137 t2))))))))
 138 \def
 139  \lambda (u1: T).(\lambda (u2: T).(\lambda (H: (pc1 u1 u2)).(\lambda (t1:
 140 T).(\lambda (t2: T).(\lambda (H0: (pc1 t1 t2)).(\lambda (k: K).(pc1_t (THead
 141 k u2 t1) (THead k u1 t1) (pc1_head_1 u1 u2 H t1 k) (THead k u2 t2)
 142 (pc1_head_2 t1 t2 H0 u2 k)))))))).
 143 (* COMMENTS
 144 Initial nodes: 71
 145 END *)
 146