matita/matita/contribs/lambdadelta/basic_1/pr1/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/pr1/defs.ma".
  18
  19 include "Basic-1/pr0/subst1.ma".
  20
  21 include "Basic-1/subst1/props.ma".
  22
  23 include "Basic-1/T/props.ma".
  24
  25 theorem pr1_pr0:
  26  \forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to (pr1 t1 t2)))
  27 \def
  28  \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr0 t1 t2)).(pr1_sing t2 t1 H
  29 t2 (pr1_refl t2)))).
  30 (* COMMENTS
  31 Initial nodes: 23
  32 END *)
  33
  34 theorem pr1_t:
  35  \forall (t2: T).(\forall (t1: T).((pr1 t1 t2) \to (\forall (t3: T).((pr1 t2
  36 t3) \to (pr1 t1 t3)))))
  37 \def
  38  \lambda (t2: T).(\lambda (t1: T).(\lambda (H: (pr1 t1 t2)).(pr1_ind (\lambda
  39 (t: T).(\lambda (t0: T).(\forall (t3: T).((pr1 t0 t3) \to (pr1 t t3)))))
  40 (\lambda (t: T).(\lambda (t3: T).(\lambda (H0: (pr1 t t3)).H0))) (\lambda
  41 (t0: T).(\lambda (t3: T).(\lambda (H0: (pr0 t3 t0)).(\lambda (t4: T).(\lambda
  42 (_: (pr1 t0 t4)).(\lambda (H2: ((\forall (t5: T).((pr1 t4 t5) \to (pr1 t0
  43 t5))))).(\lambda (t5: T).(\lambda (H3: (pr1 t4 t5)).(pr1_sing t0 t3 H0 t5 (H2
  44 t5 H3)))))))))) t1 t2 H))).
  45 (* COMMENTS
  46 Initial nodes: 103
  47 END *)
  48
  49 theorem pr1_head_1:
  50  \forall (u1: T).(\forall (u2: T).((pr1 u1 u2) \to (\forall (t: T).(\forall
  51 (k: K).(pr1 (THead k u1 t) (THead k u2 t))))))
  52 \def
  53  \lambda (u1: T).(\lambda (u2: T).(\lambda (H: (pr1 u1 u2)).(\lambda (t:
  54 T).(\lambda (k: K).(pr1_ind (\lambda (t0: T).(\lambda (t1: T).(pr1 (THead k
  55 t0 t) (THead k t1 t)))) (\lambda (t0: T).(pr1_refl (THead k t0 t))) (\lambda
  56 (t2: T).(\lambda (t1: T).(\lambda (H0: (pr0 t1 t2)).(\lambda (t3: T).(\lambda
  57 (_: (pr1 t2 t3)).(\lambda (H2: (pr1 (THead k t2 t) (THead k t3 t))).(pr1_sing
  58 (THead k t2 t) (THead k t1 t) (pr0_comp t1 t2 H0 t t (pr0_refl t) k) (THead k
  59 t3 t) H2))))))) u1 u2 H))))).
  60 (* COMMENTS
  61 Initial nodes: 137
  62 END *)
  63
  64 theorem pr1_head_2:
  65  \forall (t1: T).(\forall (t2: T).((pr1 t1 t2) \to (\forall (u: T).(\forall
  66 (k: K).(pr1 (THead k u t1) (THead k u t2))))))
  67 \def
  68  \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr1 t1 t2)).(\lambda (u:
  69 T).(\lambda (k: K).(pr1_ind (\lambda (t: T).(\lambda (t0: T).(pr1 (THead k u
  70 t) (THead k u t0)))) (\lambda (t: T).(pr1_refl (THead k u t))) (\lambda (t0:
  71 T).(\lambda (t3: T).(\lambda (H0: (pr0 t3 t0)).(\lambda (t4: T).(\lambda (_:
  72 (pr1 t0 t4)).(\lambda (H2: (pr1 (THead k u t0) (THead k u t4))).(pr1_sing
  73 (THead k u t0) (THead k u t3) (pr0_comp u u (pr0_refl u) t3 t0 H0 k) (THead k
  74 u t4) H2))))))) t1 t2 H))))).
  75 (* COMMENTS
  76 Initial nodes: 137
  77 END *)
  78
  79 theorem pr1_comp:
  80  \forall (v: T).(\forall (w: T).((pr1 v w) \to (\forall (t: T).(\forall (u:
  81 T).((pr1 t u) \to (\forall (k: K).(pr1 (THead k v t) (THead k w u))))))))
  82 \def
  83  \lambda (v: T).(\lambda (w: T).(\lambda (H: (pr1 v w)).(pr1_ind (\lambda (t:
  84 T).(\lambda (t0: T).(\forall (t1: T).(\forall (u: T).((pr1 t1 u) \to (\forall
  85 (k: K).(pr1 (THead k t t1) (THead k t0 u)))))))) (\lambda (t: T).(\lambda
  86 (t0: T).(\lambda (u: T).(\lambda (H0: (pr1 t0 u)).(\lambda (k: K).(pr1_head_2
  87 t0 u H0 t k)))))) (\lambda (t2: T).(\lambda (t1: T).(\lambda (H0: (pr0 t1
  88 t2)).(\lambda (t3: T).(\lambda (H1: (pr1 t2 t3)).(\lambda (_: ((\forall (t:
  89 T).(\forall (u: T).((pr1 t u) \to (\forall (k: K).(pr1 (THead k t2 t) (THead
  90 k t3 u)))))))).(\lambda (t: T).(\lambda (u: T).(\lambda (H3: (pr1 t
  91 u)).(\lambda (k: K).(pr1_ind (\lambda (t0: T).(\lambda (t4: T).(pr1 (THead k
  92 t1 t0) (THead k t3 t4)))) (\lambda (t0: T).(pr1_head_1 t1 t3 (pr1_sing t2 t1
  93 H0 t3 H1) t0 k)) (\lambda (t0: T).(\lambda (t4: T).(\lambda (H4: (pr0 t4
  94 t0)).(\lambda (t5: T).(\lambda (_: (pr1 t0 t5)).(\lambda (H6: (pr1 (THead k
  95 t1 t0) (THead k t3 t5))).(pr1_sing (THead k t1 t0) (THead k t1 t4) (pr0_comp
  96 t1 t1 (pr0_refl t1) t4 t0 H4 k) (THead k t3 t5) H6))))))) t u H3))))))))))) v
  97 w H))).
  98 (* COMMENTS
  99 Initial nodes: 273
 100 END *)
 101
 102 theorem pr1_eta:
 103  \forall (w: T).(\forall (u: T).(let t \def (THead (Bind Abst) w u) in
 104 (\forall (v: T).((pr1 v w) \to (pr1 (THead (Bind Abst) v (THead (Flat Appl)
 105 (TLRef O) (lift (S O) O t))) t)))))
 106 \def
 107  \lambda (w: T).(\lambda (u: T).(let t \def (THead (Bind Abst) w u) in
 108 (\lambda (v: T).(\lambda (H: (pr1 v w)).(eq_ind_r T (THead (Bind Abst) (lift
 109 (S O) O w) (lift (S O) (S O) u)) (\lambda (t0: T).(pr1 (THead (Bind Abst) v
 110 (THead (Flat Appl) (TLRef O) t0)) (THead (Bind Abst) w u))) (pr1_comp v w H
 111 (THead (Flat Appl) (TLRef O) (THead (Bind Abst) (lift (S O) O w) (lift (S O)
 112 (S O) u))) u (pr1_sing (THead (Bind Abbr) (TLRef O) (lift (S O) (S O) u))
 113 (THead (Flat Appl) (TLRef O) (THead (Bind Abst) (lift (S O) O w) (lift (S O)
 114 (S O) u))) (pr0_beta (lift (S O) O w) (TLRef O) (TLRef O) (pr0_refl (TLRef
 115 O)) (lift (S O) (S O) u) (lift (S O) (S O) u) (pr0_refl (lift (S O) (S O)
 116 u))) u (pr1_sing (THead (Bind Abbr) (TLRef O) (lift (S O) O u)) (THead (Bind
 117 Abbr) (TLRef O) (lift (S O) (S O) u)) (pr0_delta1 (TLRef O) (TLRef O)
 118 (pr0_refl (TLRef O)) (lift (S O) (S O) u) (lift (S O) (S O) u) (pr0_refl
 119 (lift (S O) (S O) u)) (lift (S O) O u) (subst1_lift_S u O O (le_n O))) u
 120 (pr1_pr0 (THead (Bind Abbr) (TLRef O) (lift (S O) O u)) u (pr0_zeta Abbr
 121 not_abbr_abst u u (pr0_refl u) (TLRef O))))) (Bind Abst)) (lift (S O) O
 122 (THead (Bind Abst) w u)) (lift_bind Abst w u (S O) O)))))).
 123 (* COMMENTS
 124 Initial nodes: 463
 125 END *)
 126