matita/matita/contribs/lambdadelta/basic_1/subst1/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/subst1/defs.ma".
  18
  19 include "Basic-1/subst0/props.ma".
  20
  21 theorem subst1_head:
  22  \forall (v: T).(\forall (u1: T).(\forall (u2: T).(\forall (i: nat).((subst1
  23 i v u1 u2) \to (\forall (k: K).(\forall (t1: T).(\forall (t2: T).((subst1 (s
  24 k i) v t1 t2) \to (subst1 i v (THead k u1 t1) (THead k u2 t2))))))))))
  25 \def
  26  \lambda (v: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (i: nat).(\lambda
  27 (H: (subst1 i v u1 u2)).(subst1_ind i v u1 (\lambda (t: T).(\forall (k:
  28 K).(\forall (t1: T).(\forall (t2: T).((subst1 (s k i) v t1 t2) \to (subst1 i
  29 v (THead k u1 t1) (THead k t t2))))))) (\lambda (k: K).(\lambda (t1:
  30 T).(\lambda (t2: T).(\lambda (H0: (subst1 (s k i) v t1 t2)).(subst1_ind (s k
  31 i) v t1 (\lambda (t: T).(subst1 i v (THead k u1 t1) (THead k u1 t)))
  32 (subst1_refl i v (THead k u1 t1)) (\lambda (t3: T).(\lambda (H1: (subst0 (s k
  33 i) v t1 t3)).(subst1_single i v (THead k u1 t1) (THead k u1 t3) (subst0_snd k
  34 v t3 t1 i H1 u1)))) t2 H0))))) (\lambda (t2: T).(\lambda (H0: (subst0 i v u1
  35 t2)).(\lambda (k: K).(\lambda (t1: T).(\lambda (t0: T).(\lambda (H1: (subst1
  36 (s k i) v t1 t0)).(subst1_ind (s k i) v t1 (\lambda (t: T).(subst1 i v (THead
  37 k u1 t1) (THead k t2 t))) (subst1_single i v (THead k u1 t1) (THead k t2 t1)
  38 (subst0_fst v t2 u1 i H0 t1 k)) (\lambda (t3: T).(\lambda (H2: (subst0 (s k
  39 i) v t1 t3)).(subst1_single i v (THead k u1 t1) (THead k t2 t3) (subst0_both
  40 v u1 t2 i H0 k t1 t3 H2)))) t0 H1))))))) u2 H))))).
  41 (* COMMENTS
  42 Initial nodes: 369
  43 END *)
  44
  45 theorem subst1_lift_lt:
  46  \forall (t1: T).(\forall (t2: T).(\forall (u: T).(\forall (i: nat).((subst1
  47 i u t1 t2) \to (\forall (d: nat).((lt i d) \to (\forall (h: nat).(subst1 i
  48 (lift h (minus d (S i)) u) (lift h d t1) (lift h d t2)))))))))
  49 \def
  50  \lambda (t1: T).(\lambda (t2: T).(\lambda (u: T).(\lambda (i: nat).(\lambda
  51 (H: (subst1 i u t1 t2)).(subst1_ind i u t1 (\lambda (t: T).(\forall (d:
  52 nat).((lt i d) \to (\forall (h: nat).(subst1 i (lift h (minus d (S i)) u)
  53 (lift h d t1) (lift h d t)))))) (\lambda (d: nat).(\lambda (_: (lt i
  54 d)).(\lambda (h: nat).(subst1_refl i (lift h (minus d (S i)) u) (lift h d
  55 t1))))) (\lambda (t3: T).(\lambda (H0: (subst0 i u t1 t3)).(\lambda (d:
  56 nat).(\lambda (H1: (lt i d)).(\lambda (h: nat).(subst1_single i (lift h
  57 (minus d (S i)) u) (lift h d t1) (lift h d t3) (subst0_lift_lt t1 t3 u i H0 d
  58 H1 h))))))) t2 H))))).
  59 (* COMMENTS
  60 Initial nodes: 185
  61 END *)
  62
  63 theorem subst1_lift_ge:
  64  \forall (t1: T).(\forall (t2: T).(\forall (u: T).(\forall (i: nat).(\forall
  65 (h: nat).((subst1 i u t1 t2) \to (\forall (d: nat).((le d i) \to (subst1
  66 (plus i h) u (lift h d t1) (lift h d t2)))))))))
  67 \def
  68  \lambda (t1: T).(\lambda (t2: T).(\lambda (u: T).(\lambda (i: nat).(\lambda
  69 (h: nat).(\lambda (H: (subst1 i u t1 t2)).(subst1_ind i u t1 (\lambda (t:
  70 T).(\forall (d: nat).((le d i) \to (subst1 (plus i h) u (lift h d t1) (lift h
  71 d t))))) (\lambda (d: nat).(\lambda (_: (le d i)).(subst1_refl (plus i h) u
  72 (lift h d t1)))) (\lambda (t3: T).(\lambda (H0: (subst0 i u t1 t3)).(\lambda
  73 (d: nat).(\lambda (H1: (le d i)).(subst1_single (plus i h) u (lift h d t1)
  74 (lift h d t3) (subst0_lift_ge t1 t3 u i h H0 d H1)))))) t2 H)))))).
  75 (* COMMENTS
  76 Initial nodes: 157
  77 END *)
  78
  79 theorem subst1_ex:
  80  \forall (u: T).(\forall (t1: T).(\forall (d: nat).(ex T (\lambda (t2:
  81 T).(subst1 d u t1 (lift (S O) d t2))))))
  82 \def
  83  \lambda (u: T).(\lambda (t1: T).(T_ind (\lambda (t: T).(\forall (d: nat).(ex
  84 T (\lambda (t2: T).(subst1 d u t (lift (S O) d t2)))))) (\lambda (n:
  85 nat).(\lambda (d: nat).(ex_intro T (\lambda (t2: T).(subst1 d u (TSort n)
  86 (lift (S O) d t2))) (TSort n) (eq_ind_r T (TSort n) (\lambda (t: T).(subst1 d
  87 u (TSort n) t)) (subst1_refl d u (TSort n)) (lift (S O) d (TSort n))
  88 (lift_sort n (S O) d))))) (\lambda (n: nat).(\lambda (d: nat).(lt_eq_gt_e n d
  89 (ex T (\lambda (t2: T).(subst1 d u (TLRef n) (lift (S O) d t2)))) (\lambda
  90 (H: (lt n d)).(ex_intro T (\lambda (t2: T).(subst1 d u (TLRef n) (lift (S O)
  91 d t2))) (TLRef n) (eq_ind_r T (TLRef n) (\lambda (t: T).(subst1 d u (TLRef n)
  92 t)) (subst1_refl d u (TLRef n)) (lift (S O) d (TLRef n)) (lift_lref_lt n (S
  93 O) d H)))) (\lambda (H: (eq nat n d)).(eq_ind nat n (\lambda (n0: nat).(ex T
  94 (\lambda (t2: T).(subst1 n0 u (TLRef n) (lift (S O) n0 t2))))) (ex_intro T
  95 (\lambda (t2: T).(subst1 n u (TLRef n) (lift (S O) n t2))) (lift n O u)
  96 (eq_ind_r T (lift (plus (S O) n) O u) (\lambda (t: T).(subst1 n u (TLRef n)
  97 t)) (subst1_single n u (TLRef n) (lift (S n) O u) (subst0_lref u n)) (lift (S
  98 O) n (lift n O u)) (lift_free u n (S O) O n (le_n (plus O n)) (le_O_n n)))) d
  99 H)) (\lambda (H: (lt d n)).(ex_intro T (\lambda (t2: T).(subst1 d u (TLRef n)
 100 (lift (S O) d t2))) (TLRef (pred n)) (eq_ind_r T (TLRef n) (\lambda (t:
 101 T).(subst1 d u (TLRef n) t)) (subst1_refl d u (TLRef n)) (lift (S O) d (TLRef
 102 (pred n))) (lift_lref_gt d n H))))))) (\lambda (k: K).(\lambda (t:
 103 T).(\lambda (H: ((\forall (d: nat).(ex T (\lambda (t2: T).(subst1 d u t (lift
 104 (S O) d t2))))))).(\lambda (t0: T).(\lambda (H0: ((\forall (d: nat).(ex T
 105 (\lambda (t2: T).(subst1 d u t0 (lift (S O) d t2))))))).(\lambda (d:
 106 nat).(let H_x \def (H d) in (let H1 \def H_x in (ex_ind T (\lambda (t2:
 107 T).(subst1 d u t (lift (S O) d t2))) (ex T (\lambda (t2: T).(subst1 d u
 108 (THead k t t0) (lift (S O) d t2)))) (\lambda (x: T).(\lambda (H2: (subst1 d u
 109 t (lift (S O) d x))).(let H_x0 \def (H0 (s k d)) in (let H3 \def H_x0 in
 110 (ex_ind T (\lambda (t2: T).(subst1 (s k d) u t0 (lift (S O) (s k d) t2))) (ex
 111 T (\lambda (t2: T).(subst1 d u (THead k t t0) (lift (S O) d t2)))) (\lambda
 112 (x0: T).(\lambda (H4: (subst1 (s k d) u t0 (lift (S O) (s k d)
 113 x0))).(ex_intro T (\lambda (t2: T).(subst1 d u (THead k t t0) (lift (S O) d
 114 t2))) (THead k x x0) (eq_ind_r T (THead k (lift (S O) d x) (lift (S O) (s k
 115 d) x0)) (\lambda (t2: T).(subst1 d u (THead k t t0) t2)) (subst1_head u t
 116 (lift (S O) d x) d H2 k t0 (lift (S O) (s k d) x0) H4) (lift (S O) d (THead k
 117 x x0)) (lift_head k x x0 (S O) d))))) H3))))) H1))))))))) t1)).
 118 (* COMMENTS
 119 Initial nodes: 925
 120 END *)
 121
 122 theorem subst1_lift_S:
 123  \forall (u: T).(\forall (i: nat).(\forall (h: nat).((le h i) \to (subst1 i
 124 (TLRef h) (lift (S h) (S i) u) (lift (S h) i u)))))
 125 \def
 126  \lambda (u: T).(T_ind (\lambda (t: T).(\forall (i: nat).(\forall (h:
 127 nat).((le h i) \to (subst1 i (TLRef h) (lift (S h) (S i) t) (lift (S h) i
 128 t)))))) (\lambda (n: nat).(\lambda (i: nat).(\lambda (h: nat).(\lambda (_:
 129 (le h i)).(eq_ind_r T (TSort n) (\lambda (t: T).(subst1 i (TLRef h) t (lift
 130 (S h) i (TSort n)))) (eq_ind_r T (TSort n) (\lambda (t: T).(subst1 i (TLRef
 131 h) (TSort n) t)) (subst1_refl i (TLRef h) (TSort n)) (lift (S h) i (TSort n))
 132 (lift_sort n (S h) i)) (lift (S h) (S i) (TSort n)) (lift_sort n (S h) (S
 133 i))))))) (\lambda (n: nat).(\lambda (i: nat).(\lambda (h: nat).(\lambda (H:
 134 (le h i)).(lt_eq_gt_e n i (subst1 i (TLRef h) (lift (S h) (S i) (TLRef n))
 135 (lift (S h) i (TLRef n))) (\lambda (H0: (lt n i)).(eq_ind_r T (TLRef n)
 136 (\lambda (t: T).(subst1 i (TLRef h) t (lift (S h) i (TLRef n)))) (eq_ind_r T
 137 (TLRef n) (\lambda (t: T).(subst1 i (TLRef h) (TLRef n) t)) (subst1_refl i
 138 (TLRef h) (TLRef n)) (lift (S h) i (TLRef n)) (lift_lref_lt n (S h) i H0))
 139 (lift (S h) (S i) (TLRef n)) (lift_lref_lt n (S h) (S i) (le_S (S n) i H0))))
 140 (\lambda (H0: (eq nat n i)).(let H1 \def (eq_ind_r nat i (\lambda (n0:
 141 nat).(le h n0)) H n H0) in (eq_ind nat n (\lambda (n0: nat).(subst1 n0 (TLRef
 142 h) (lift (S h) (S n0) (TLRef n)) (lift (S h) n0 (TLRef n)))) (eq_ind_r T
 143 (TLRef n) (\lambda (t: T).(subst1 n (TLRef h) t (lift (S h) n (TLRef n))))
 144 (eq_ind_r T (TLRef (plus n (S h))) (\lambda (t: T).(subst1 n (TLRef h) (TLRef
 145 n) t)) (eq_ind nat (S (plus n h)) (\lambda (n0: nat).(subst1 n (TLRef h)
 146 (TLRef n) (TLRef n0))) (eq_ind_r nat (plus h n) (\lambda (n0: nat).(subst1 n
 147 (TLRef h) (TLRef n) (TLRef (S n0)))) (eq_ind nat (plus h (S n)) (\lambda (n0:
 148 nat).(subst1 n (TLRef h) (TLRef n) (TLRef n0))) (eq_ind T (lift (S n) O
 149 (TLRef h)) (\lambda (t: T).(subst1 n (TLRef h) (TLRef n) t)) (subst1_single n
 150 (TLRef h) (TLRef n) (lift (S n) O (TLRef h)) (subst0_lref (TLRef h) n))
 151 (TLRef (plus h (S n))) (lift_lref_ge h (S n) O (le_O_n h))) (S (plus h n))
 152 (sym_eq nat (S (plus h n)) (plus h (S n)) (plus_n_Sm h n))) (plus n h)
 153 (plus_sym n h)) (plus n (S h)) (plus_n_Sm n h)) (lift (S h) n (TLRef n))
 154 (lift_lref_ge n (S h) n (le_n n))) (lift (S h) (S n) (TLRef n)) (lift_lref_lt
 155 n (S h) (S n) (le_n (S n)))) i H0))) (\lambda (H0: (lt i n)).(eq_ind_r T
 156 (TLRef (plus n (S h))) (\lambda (t: T).(subst1 i (TLRef h) t (lift (S h) i
 157 (TLRef n)))) (eq_ind_r T (TLRef (plus n (S h))) (\lambda (t: T).(subst1 i
 158 (TLRef h) (TLRef (plus n (S h))) t)) (subst1_refl i (TLRef h) (TLRef (plus n
 159 (S h)))) (lift (S h) i (TLRef n)) (lift_lref_ge n (S h) i (le_S_n i n (le_S
 160 (S i) n H0)))) (lift (S h) (S i) (TLRef n)) (lift_lref_ge n (S h) (S i)
 161 H0)))))))) (\lambda (k: K).(\lambda (t: T).(\lambda (H: ((\forall (i:
 162 nat).(\forall (h: nat).((le h i) \to (subst1 i (TLRef h) (lift (S h) (S i) t)
 163 (lift (S h) i t))))))).(\lambda (t0: T).(\lambda (H0: ((\forall (i:
 164 nat).(\forall (h: nat).((le h i) \to (subst1 i (TLRef h) (lift (S h) (S i)
 165 t0) (lift (S h) i t0))))))).(\lambda (i: nat).(\lambda (h: nat).(\lambda (H1:
 166 (le h i)).(eq_ind_r T (THead k (lift (S h) (S i) t) (lift (S h) (s k (S i))
 167 t0)) (\lambda (t1: T).(subst1 i (TLRef h) t1 (lift (S h) i (THead k t t0))))
 168 (eq_ind_r T (THead k (lift (S h) i t) (lift (S h) (s k i) t0)) (\lambda (t1:
 169 T).(subst1 i (TLRef h) (THead k (lift (S h) (S i) t) (lift (S h) (s k (S i))
 170 t0)) t1)) (subst1_head (TLRef h) (lift (S h) (S i) t) (lift (S h) i t) i (H i
 171 h H1) k (lift (S h) (s k (S i)) t0) (lift (S h) (s k i) t0) (eq_ind_r nat (S
 172 (s k i)) (\lambda (n: nat).(subst1 (s k i) (TLRef h) (lift (S h) n t0) (lift
 173 (S h) (s k i) t0))) (H0 (s k i) h (le_trans h i (s k i) H1 (s_inc k i))) (s k
 174 (S i)) (s_S k i))) (lift (S h) i (THead k t t0)) (lift_head k t t0 (S h) i))
 175 (lift (S h) (S i) (THead k t t0)) (lift_head k t t0 (S h) (S i))))))))))) u).
 176 (* COMMENTS
 177 Initial nodes: 1421
 178 END *)
 179