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)).(let TMP_1 \def
  25 (\lambda (t: T).(pr1 t1 t)) in (let TMP_2 \def (\lambda (t: T).(pr1 t2 t)) in
  26 (let TMP_3 \def (pr1_pr0 t1 t2 H) in (let TMP_4 \def (pr1_refl t2) in
  27 (ex_intro2 T TMP_1 TMP_2 t2 TMP_3 TMP_4))))))).
  28
  29 theorem pc1_pr0_x:
  30  \forall (t1: T).(\forall (t2: T).((pr0 t2 t1) \to (pc1 t1 t2)))
  31 \def
  32  \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr0 t2 t1)).(let TMP_1 \def
  33 (\lambda (t: T).(pr1 t1 t)) in (let TMP_2 \def (\lambda (t: T).(pr1 t2 t)) in
  34 (let TMP_3 \def (pr1_refl t1) in (let TMP_4 \def (pr1_pr0 t2 t1 H) in
  35 (ex_intro2 T TMP_1 TMP_2 t1 TMP_3 TMP_4))))))).
  36
  37 theorem pc1_refl:
  38  \forall (t: T).(pc1 t t)
  39 \def
  40  \lambda (t: T).(let TMP_1 \def (\lambda (t0: T).(pr1 t t0)) in (let TMP_2
  41 \def (\lambda (t0: T).(pr1 t t0)) in (let TMP_3 \def (pr1_refl t) in (let
  42 TMP_4 \def (pr1_refl t) in (ex_intro2 T TMP_1 TMP_2 t TMP_3 TMP_4))))).
  43
  44 theorem pc1_pr0_u:
  45  \forall (t2: T).(\forall (t1: T).((pr0 t1 t2) \to (\forall (t3: T).((pc1 t2
  46 t3) \to (pc1 t1 t3)))))
  47 \def
  48  \lambda (t2: T).(\lambda (t1: T).(\lambda (H: (pr0 t1 t2)).(\lambda (t3:
  49 T).(\lambda (H0: (pc1 t2 t3)).(let H1 \def H0 in (let TMP_1 \def (\lambda (t:
  50 T).(pr1 t2 t)) in (let TMP_2 \def (\lambda (t: T).(pr1 t3 t)) in (let TMP_3
  51 \def (pc1 t1 t3) in (let TMP_7 \def (\lambda (x: T).(\lambda (H2: (pr1 t2
  52 x)).(\lambda (H3: (pr1 t3 x)).(let TMP_4 \def (\lambda (t: T).(pr1 t1 t)) in
  53 (let TMP_5 \def (\lambda (t: T).(pr1 t3 t)) in (let TMP_6 \def (pr1_sing t2
  54 t1 H x H2) in (ex_intro2 T TMP_4 TMP_5 x TMP_6 H3))))))) in (ex2_ind T TMP_1
  55 TMP_2 TMP_3 TMP_7 H1)))))))))).
  56
  57 theorem pc1_s:
  58  \forall (t2: T).(\forall (t1: T).((pc1 t1 t2) \to (pc1 t2 t1)))
  59 \def
  60  \lambda (t2: T).(\lambda (t1: T).(\lambda (H: (pc1 t1 t2)).(let H0 \def H in
  61 (let TMP_1 \def (\lambda (t: T).(pr1 t1 t)) in (let TMP_2 \def (\lambda (t:
  62 T).(pr1 t2 t)) in (let TMP_3 \def (pc1 t2 t1) in (let TMP_6 \def (\lambda (x:
  63 T).(\lambda (H1: (pr1 t1 x)).(\lambda (H2: (pr1 t2 x)).(let TMP_4 \def
  64 (\lambda (t: T).(pr1 t2 t)) in (let TMP_5 \def (\lambda (t: T).(pr1 t1 t)) in
  65 (ex_intro2 T TMP_4 TMP_5 x H2 H1)))))) in (ex2_ind T TMP_1 TMP_2 TMP_3 TMP_6
  66 H0)))))))).
  67
  68 theorem pc1_head_1:
  69  \forall (u1: T).(\forall (u2: T).((pc1 u1 u2) \to (\forall (t: T).(\forall
  70 (k: K).(pc1 (THead k u1 t) (THead k u2 t))))))
  71 \def
  72  \lambda (u1: T).(\lambda (u2: T).(\lambda (H: (pc1 u1 u2)).(\lambda (t:
  73 T).(\lambda (k: K).(let H0 \def H in (let TMP_1 \def (\lambda (t0: T).(pr1 u1
  74 t0)) in (let TMP_2 \def (\lambda (t0: T).(pr1 u2 t0)) in (let TMP_3 \def
  75 (THead k u1 t) in (let TMP_4 \def (THead k u2 t) in (let TMP_5 \def (pc1
  76 TMP_3 TMP_4) in (let TMP_13 \def (\lambda (x: T).(\lambda (H1: (pr1 u1
  77 x)).(\lambda (H2: (pr1 u2 x)).(let TMP_7 \def (\lambda (t0: T).(let TMP_6
  78 \def (THead k u1 t) in (pr1 TMP_6 t0))) in (let TMP_9 \def (\lambda (t0:
  79 T).(let TMP_8 \def (THead k u2 t) in (pr1 TMP_8 t0))) in (let TMP_10 \def
  80 (THead k x t) in (let TMP_11 \def (pr1_head_1 u1 x H1 t k) in (let TMP_12
  81 \def (pr1_head_1 u2 x H2 t k) in (ex_intro2 T TMP_7 TMP_9 TMP_10 TMP_11
  82 TMP_12))))))))) in (ex2_ind T TMP_1 TMP_2 TMP_5 TMP_13 H0)))))))))))).
  83
  84 theorem pc1_head_2:
  85  \forall (t1: T).(\forall (t2: T).((pc1 t1 t2) \to (\forall (u: T).(\forall
  86 (k: K).(pc1 (THead k u t1) (THead k u t2))))))
  87 \def
  88  \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pc1 t1 t2)).(\lambda (u:
  89 T).(\lambda (k: K).(let H0 \def H in (let TMP_1 \def (\lambda (t: T).(pr1 t1
  90 t)) in (let TMP_2 \def (\lambda (t: T).(pr1 t2 t)) in (let TMP_3 \def (THead
  91 k u t1) in (let TMP_4 \def (THead k u t2) in (let TMP_5 \def (pc1 TMP_3
  92 TMP_4) in (let TMP_13 \def (\lambda (x: T).(\lambda (H1: (pr1 t1 x)).(\lambda
  93 (H2: (pr1 t2 x)).(let TMP_7 \def (\lambda (t: T).(let TMP_6 \def (THead k u
  94 t1) in (pr1 TMP_6 t))) in (let TMP_9 \def (\lambda (t: T).(let TMP_8 \def
  95 (THead k u t2) in (pr1 TMP_8 t))) in (let TMP_10 \def (THead k u x) in (let
  96 TMP_11 \def (pr1_head_2 t1 x H1 u k) in (let TMP_12 \def (pr1_head_2 t2 x H2
  97 u k) in (ex_intro2 T TMP_7 TMP_9 TMP_10 TMP_11 TMP_12))))))))) in (ex2_ind T
  98 TMP_1 TMP_2 TMP_5 TMP_13 H0)))))))))))).
  99
 100 theorem pc1_t:
 101  \forall (t2: T).(\forall (t1: T).((pc1 t1 t2) \to (\forall (t3: T).((pc1 t2
 102 t3) \to (pc1 t1 t3)))))
 103 \def
 104  \lambda (t2: T).(\lambda (t1: T).(\lambda (H: (pc1 t1 t2)).(\lambda (t3:
 105 T).(\lambda (H0: (pc1 t2 t3)).(let H1 \def H0 in (let TMP_1 \def (\lambda (t:
 106 T).(pr1 t2 t)) in (let TMP_2 \def (\lambda (t: T).(pr1 t3 t)) in (let TMP_3
 107 \def (pc1 t1 t3) in (let TMP_17 \def (\lambda (x: T).(\lambda (H2: (pr1 t2
 108 x)).(\lambda (H3: (pr1 t3 x)).(let H4 \def H in (let TMP_4 \def (\lambda (t:
 109 T).(pr1 t1 t)) in (let TMP_5 \def (\lambda (t: T).(pr1 t2 t)) in (let TMP_6
 110 \def (pc1 t1 t3) in (let TMP_16 \def (\lambda (x0: T).(\lambda (H5: (pr1 t1
 111 x0)).(\lambda (H6: (pr1 t2 x0)).(let TMP_7 \def (\lambda (t: T).(pr1 x0 t))
 112 in (let TMP_8 \def (\lambda (t: T).(pr1 x t)) in (let TMP_9 \def (pc1 t1 t3)
 113 in (let TMP_14 \def (\lambda (x1: T).(\lambda (H7: (pr1 x0 x1)).(\lambda (H8:
 114 (pr1 x x1)).(let TMP_10 \def (\lambda (t: T).(pr1 t1 t)) in (let TMP_11 \def
 115 (\lambda (t: T).(pr1 t3 t)) in (let TMP_12 \def (pr1_t x0 t1 H5 x1 H7) in
 116 (let TMP_13 \def (pr1_t x t3 H3 x1 H8) in (ex_intro2 T TMP_10 TMP_11 x1
 117 TMP_12 TMP_13)))))))) in (let TMP_15 \def (pr1_confluence t2 x0 H6 x H2) in
 118 (ex2_ind T TMP_7 TMP_8 TMP_9 TMP_14 TMP_15))))))))) in (ex2_ind T TMP_4 TMP_5
 119 TMP_6 TMP_16 H4))))))))) in (ex2_ind T TMP_1 TMP_2 TMP_3 TMP_17 H1)))))))))).
 120
 121 theorem pc1_pr0_u2:
 122  \forall (t0: T).(\forall (t1: T).((pr0 t0 t1) \to (\forall (t2: T).((pc1 t0
 123 t2) \to (pc1 t1 t2)))))
 124 \def
 125  \lambda (t0: T).(\lambda (t1: T).(\lambda (H: (pr0 t0 t1)).(\lambda (t2:
 126 T).(\lambda (H0: (pc1 t0 t2)).(let TMP_1 \def (pc1_pr0_x t1 t0 H) in (pc1_t
 127 t0 t1 TMP_1 t2 H0)))))).
 128
 129 theorem pc1_head:
 130  \forall (u1: T).(\forall (u2: T).((pc1 u1 u2) \to (\forall (t1: T).(\forall
 131 (t2: T).((pc1 t1 t2) \to (\forall (k: K).(pc1 (THead k u1 t1) (THead k u2
 132 t2))))))))
 133 \def
 134  \lambda (u1: T).(\lambda (u2: T).(\lambda (H: (pc1 u1 u2)).(\lambda (t1:
 135 T).(\lambda (t2: T).(\lambda (H0: (pc1 t1 t2)).(\lambda (k: K).(let TMP_1
 136 \def (THead k u2 t1) in (let TMP_2 \def (THead k u1 t1) in (let TMP_3 \def
 137 (pc1_head_1 u1 u2 H t1 k) in (let TMP_4 \def (THead k u2 t2) in (let TMP_5
 138 \def (pc1_head_2 t1 t2 H0 u2 k) in (pc1_t TMP_1 TMP_2 TMP_3 TMP_4
 139 TMP_5)))))))))))).
 140