matita/matita/contribs/lambdadelta/basic_1/subst1/fwd.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_gen_sort:
  22  \forall (v: T).(\forall (x: T).(\forall (i: nat).(\forall (n: nat).((subst1
  23 i v (TSort n) x) \to (eq T x (TSort n))))))
  24 \def
  25  \lambda (v: T).(\lambda (x: T).(\lambda (i: nat).(\lambda (n: nat).(\lambda
  26 (H: (subst1 i v (TSort n) x)).(subst1_ind i v (TSort n) (\lambda (t: T).(eq T
  27 t (TSort n))) (refl_equal T (TSort n)) (\lambda (t2: T).(\lambda (H0: (subst0
  28 i v (TSort n) t2)).(subst0_gen_sort v t2 i n H0 (eq T t2 (TSort n))))) x
  29 H))))).
  30 (* COMMENTS
  31 Initial nodes: 89
  32 END *)
  33
  34 theorem subst1_gen_lref:
  35  \forall (v: T).(\forall (x: T).(\forall (i: nat).(\forall (n: nat).((subst1
  36 i v (TLRef n) x) \to (or (eq T x (TLRef n)) (land (eq nat n i) (eq T x (lift
  37 (S n) O v))))))))
  38 \def
  39  \lambda (v: T).(\lambda (x: T).(\lambda (i: nat).(\lambda (n: nat).(\lambda
  40 (H: (subst1 i v (TLRef n) x)).(subst1_ind i v (TLRef n) (\lambda (t: T).(or
  41 (eq T t (TLRef n)) (land (eq nat n i) (eq T t (lift (S n) O v))))) (or_introl
  42 (eq T (TLRef n) (TLRef n)) (land (eq nat n i) (eq T (TLRef n) (lift (S n) O
  43 v))) (refl_equal T (TLRef n))) (\lambda (t2: T).(\lambda (H0: (subst0 i v
  44 (TLRef n) t2)).(land_ind (eq nat n i) (eq T t2 (lift (S n) O v)) (or (eq T t2
  45 (TLRef n)) (land (eq nat n i) (eq T t2 (lift (S n) O v)))) (\lambda (H1: (eq
  46 nat n i)).(\lambda (H2: (eq T t2 (lift (S n) O v))).(or_intror (eq T t2
  47 (TLRef n)) (land (eq nat n i) (eq T t2 (lift (S n) O v))) (conj (eq nat n i)
  48 (eq T t2 (lift (S n) O v)) H1 H2)))) (subst0_gen_lref v t2 i n H0)))) x
  49 H))))).
  50 (* COMMENTS
  51 Initial nodes: 305
  52 END *)
  53
  54 theorem subst1_gen_head:
  55  \forall (k: K).(\forall (v: T).(\forall (u1: T).(\forall (t1: T).(\forall
  56 (x: T).(\forall (i: nat).((subst1 i v (THead k u1 t1) x) \to (ex3_2 T T
  57 (\lambda (u2: T).(\lambda (t2: T).(eq T x (THead k u2 t2)))) (\lambda (u2:
  58 T).(\lambda (_: T).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (t2:
  59 T).(subst1 (s k i) v t1 t2))))))))))
  60 \def
  61  \lambda (k: K).(\lambda (v: T).(\lambda (u1: T).(\lambda (t1: T).(\lambda
  62 (x: T).(\lambda (i: nat).(\lambda (H: (subst1 i v (THead k u1 t1)
  63 x)).(subst1_ind i v (THead k u1 t1) (\lambda (t: T).(ex3_2 T T (\lambda (u2:
  64 T).(\lambda (t2: T).(eq T t (THead k u2 t2)))) (\lambda (u2: T).(\lambda (_:
  65 T).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (t2: T).(subst1 (s k i) v t1
  66 t2))))) (ex3_2_intro T T (\lambda (u2: T).(\lambda (t2: T).(eq T (THead k u1
  67 t1) (THead k u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(subst1 i v u1 u2)))
  68 (\lambda (_: T).(\lambda (t2: T).(subst1 (s k i) v t1 t2))) u1 t1 (refl_equal
  69 T (THead k u1 t1)) (subst1_refl i v u1) (subst1_refl (s k i) v t1)) (\lambda
  70 (t2: T).(\lambda (H0: (subst0 i v (THead k u1 t1) t2)).(or3_ind (ex2 T
  71 (\lambda (u2: T).(eq T t2 (THead k u2 t1))) (\lambda (u2: T).(subst0 i v u1
  72 u2))) (ex2 T (\lambda (t3: T).(eq T t2 (THead k u1 t3))) (\lambda (t3:
  73 T).(subst0 (s k i) v t1 t3))) (ex3_2 T T (\lambda (u2: T).(\lambda (t3:
  74 T).(eq T t2 (THead k u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i v
  75 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(subst0 (s k i) v t1 t3)))) (ex3_2
  76 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead k u2 t3)))) (\lambda
  77 (u2: T).(\lambda (_: T).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (t3:
  78 T).(subst1 (s k i) v t1 t3)))) (\lambda (H1: (ex2 T (\lambda (u2: T).(eq T t2
  79 (THead k u2 t1))) (\lambda (u2: T).(subst0 i v u1 u2)))).(ex2_ind T (\lambda
  80 (u2: T).(eq T t2 (THead k u2 t1))) (\lambda (u2: T).(subst0 i v u1 u2))
  81 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead k u2 t3))))
  82 (\lambda (u2: T).(\lambda (_: T).(subst1 i v u1 u2))) (\lambda (_:
  83 T).(\lambda (t3: T).(subst1 (s k i) v t1 t3)))) (\lambda (x0: T).(\lambda
  84 (H2: (eq T t2 (THead k x0 t1))).(\lambda (H3: (subst0 i v u1
  85 x0)).(ex3_2_intro T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead k u2
  86 t3)))) (\lambda (u2: T).(\lambda (_: T).(subst1 i v u1 u2))) (\lambda (_:
  87 T).(\lambda (t3: T).(subst1 (s k i) v t1 t3))) x0 t1 H2 (subst1_single i v u1
  88 x0 H3) (subst1_refl (s k i) v t1))))) H1)) (\lambda (H1: (ex2 T (\lambda (t3:
  89 T).(eq T t2 (THead k u1 t3))) (\lambda (t3: T).(subst0 (s k i) v t1
  90 t3)))).(ex2_ind T (\lambda (t3: T).(eq T t2 (THead k u1 t3))) (\lambda (t3:
  91 T).(subst0 (s k i) v t1 t3)) (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq
  92 T t2 (THead k u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(subst1 i v u1 u2)))
  93 (\lambda (_: T).(\lambda (t3: T).(subst1 (s k i) v t1 t3)))) (\lambda (x0:
  94 T).(\lambda (H2: (eq T t2 (THead k u1 x0))).(\lambda (H3: (subst0 (s k i) v
  95 t1 x0)).(ex3_2_intro T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead k
  96 u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(subst1 i v u1 u2))) (\lambda (_:
  97 T).(\lambda (t3: T).(subst1 (s k i) v t1 t3))) u1 x0 H2 (subst1_refl i v u1)
  98 (subst1_single (s k i) v t1 x0 H3))))) H1)) (\lambda (H1: (ex3_2 T T (\lambda
  99 (u2: T).(\lambda (t3: T).(eq T t2 (THead k u2 t3)))) (\lambda (u2:
 100 T).(\lambda (_: T).(subst0 i v u1 u2))) (\lambda (_: T).(\lambda (t3:
 101 T).(subst0 (s k i) v t1 t3))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t3:
 102 T).(eq T t2 (THead k u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i v
 103 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(subst0 (s k i) v t1 t3))) (ex3_2 T
 104 T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead k u2 t3)))) (\lambda (u2:
 105 T).(\lambda (_: T).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (t3:
 106 T).(subst1 (s k i) v t1 t3)))) (\lambda (x0: T).(\lambda (x1: T).(\lambda
 107 (H2: (eq T t2 (THead k x0 x1))).(\lambda (H3: (subst0 i v u1 x0)).(\lambda
 108 (H4: (subst0 (s k i) v t1 x1)).(ex3_2_intro T T (\lambda (u2: T).(\lambda
 109 (t3: T).(eq T t2 (THead k u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(subst1
 110 i v u1 u2))) (\lambda (_: T).(\lambda (t3: T).(subst1 (s k i) v t1 t3))) x0
 111 x1 H2 (subst1_single i v u1 x0 H3) (subst1_single (s k i) v t1 x1 H4)))))))
 112 H1)) (subst0_gen_head k v u1 t1 t2 i H0)))) x H))))))).
 113 (* COMMENTS
 114 Initial nodes: 1199
 115 END *)
 116
 117 theorem subst1_gen_lift_lt:
 118  \forall (u: T).(\forall (t1: T).(\forall (x: T).(\forall (i: nat).(\forall
 119 (h: nat).(\forall (d: nat).((subst1 i (lift h d u) (lift h (S (plus i d)) t1)
 120 x) \to (ex2 T (\lambda (t2: T).(eq T x (lift h (S (plus i d)) t2))) (\lambda
 121 (t2: T).(subst1 i u t1 t2)))))))))
 122 \def
 123  \lambda (u: T).(\lambda (t1: T).(\lambda (x: T).(\lambda (i: nat).(\lambda
 124 (h: nat).(\lambda (d: nat).(\lambda (H: (subst1 i (lift h d u) (lift h (S
 125 (plus i d)) t1) x)).(subst1_ind i (lift h d u) (lift h (S (plus i d)) t1)
 126 (\lambda (t: T).(ex2 T (\lambda (t2: T).(eq T t (lift h (S (plus i d)) t2)))
 127 (\lambda (t2: T).(subst1 i u t1 t2)))) (ex_intro2 T (\lambda (t2: T).(eq T
 128 (lift h (S (plus i d)) t1) (lift h (S (plus i d)) t2))) (\lambda (t2:
 129 T).(subst1 i u t1 t2)) t1 (refl_equal T (lift h (S (plus i d)) t1))
 130 (subst1_refl i u t1)) (\lambda (t2: T).(\lambda (H0: (subst0 i (lift h d u)
 131 (lift h (S (plus i d)) t1) t2)).(ex2_ind T (\lambda (t3: T).(eq T t2 (lift h
 132 (S (plus i d)) t3))) (\lambda (t3: T).(subst0 i u t1 t3)) (ex2 T (\lambda
 133 (t3: T).(eq T t2 (lift h (S (plus i d)) t3))) (\lambda (t3: T).(subst1 i u t1
 134 t3))) (\lambda (x0: T).(\lambda (H1: (eq T t2 (lift h (S (plus i d))
 135 x0))).(\lambda (H2: (subst0 i u t1 x0)).(ex_intro2 T (\lambda (t3: T).(eq T
 136 t2 (lift h (S (plus i d)) t3))) (\lambda (t3: T).(subst1 i u t1 t3)) x0 H1
 137 (subst1_single i u t1 x0 H2))))) (subst0_gen_lift_lt u t1 t2 i h d H0)))) x
 138 H))))))).
 139 (* COMMENTS
 140 Initial nodes: 395
 141 END *)
 142
 143 theorem subst1_gen_lift_eq:
 144  \forall (t: T).(\forall (u: T).(\forall (x: T).(\forall (h: nat).(\forall
 145 (d: nat).(\forall (i: nat).((le d i) \to ((lt i (plus d h)) \to ((subst1 i u
 146 (lift h d t) x) \to (eq T x (lift h d t))))))))))
 147 \def
 148  \lambda (t: T).(\lambda (u: T).(\lambda (x: T).(\lambda (h: nat).(\lambda
 149 (d: nat).(\lambda (i: nat).(\lambda (H: (le d i)).(\lambda (H0: (lt i (plus d
 150 h))).(\lambda (H1: (subst1 i u (lift h d t) x)).(subst1_ind i u (lift h d t)
 151 (\lambda (t0: T).(eq T t0 (lift h d t))) (refl_equal T (lift h d t)) (\lambda
 152 (t2: T).(\lambda (H2: (subst0 i u (lift h d t) t2)).(subst0_gen_lift_false t
 153 u t2 h d i H H0 H2 (eq T t2 (lift h d t))))) x H1))))))))).
 154 (* COMMENTS
 155 Initial nodes: 141
 156 END *)
 157
 158 theorem subst1_gen_lift_ge:
 159  \forall (u: T).(\forall (t1: T).(\forall (x: T).(\forall (i: nat).(\forall
 160 (h: nat).(\forall (d: nat).((subst1 i u (lift h d t1) x) \to ((le (plus d h)
 161 i) \to (ex2 T (\lambda (t2: T).(eq T x (lift h d t2))) (\lambda (t2:
 162 T).(subst1 (minus i h) u t1 t2))))))))))
 163 \def
 164  \lambda (u: T).(\lambda (t1: T).(\lambda (x: T).(\lambda (i: nat).(\lambda
 165 (h: nat).(\lambda (d: nat).(\lambda (H: (subst1 i u (lift h d t1)
 166 x)).(\lambda (H0: (le (plus d h) i)).(subst1_ind i u (lift h d t1) (\lambda
 167 (t: T).(ex2 T (\lambda (t2: T).(eq T t (lift h d t2))) (\lambda (t2:
 168 T).(subst1 (minus i h) u t1 t2)))) (ex_intro2 T (\lambda (t2: T).(eq T (lift
 169 h d t1) (lift h d t2))) (\lambda (t2: T).(subst1 (minus i h) u t1 t2)) t1
 170 (refl_equal T (lift h d t1)) (subst1_refl (minus i h) u t1)) (\lambda (t2:
 171 T).(\lambda (H1: (subst0 i u (lift h d t1) t2)).(ex2_ind T (\lambda (t3:
 172 T).(eq T t2 (lift h d t3))) (\lambda (t3: T).(subst0 (minus i h) u t1 t3))
 173 (ex2 T (\lambda (t3: T).(eq T t2 (lift h d t3))) (\lambda (t3: T).(subst1
 174 (minus i h) u t1 t3))) (\lambda (x0: T).(\lambda (H2: (eq T t2 (lift h d
 175 x0))).(\lambda (H3: (subst0 (minus i h) u t1 x0)).(ex_intro2 T (\lambda (t3:
 176 T).(eq T t2 (lift h d t3))) (\lambda (t3: T).(subst1 (minus i h) u t1 t3)) x0
 177 H2 (subst1_single (minus i h) u t1 x0 H3))))) (subst0_gen_lift_ge u t1 t2 i h
 178 d H1 H0)))) x H)))))))).
 179 (* COMMENTS
 180 Initial nodes: 355
 181 END *)
 182