matita/matita/contribs/lambdadelta/basic_1/drop1/getl.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/drop1/fwd.ma".
  18
  19 include "basic_1/getl/drop.ma".
  20
  21 theorem drop1_getl_trans:
  22  \forall (hds: PList).(\forall (c1: C).(\forall (c2: C).((drop1 hds c2 c1)
  23 \to (\forall (b: B).(\forall (e1: C).(\forall (v: T).(\forall (i: nat).((getl
  24 i c1 (CHead e1 (Bind b) v)) \to (ex2 C (\lambda (e2: C).(drop1 (ptrans hds i)
  25 e2 e1)) (\lambda (e2: C).(getl (trans hds i) c2 (CHead e2 (Bind b) (lift1
  26 (ptrans hds i) v)))))))))))))
  27 \def
  28  \lambda (hds: PList).(let TMP_9 \def (\lambda (p: PList).(\forall (c1:
  29 C).(\forall (c2: C).((drop1 p c2 c1) \to (\forall (b: B).(\forall (e1:
  30 C).(\forall (v: T).(\forall (i: nat).((getl i c1 (CHead e1 (Bind b) v)) \to
  31 (let TMP_2 \def (\lambda (e2: C).(let TMP_1 \def (ptrans p i) in (drop1 TMP_1
  32 e2 e1))) in (let TMP_8 \def (\lambda (e2: C).(let TMP_3 \def (trans p i) in
  33 (let TMP_4 \def (Bind b) in (let TMP_5 \def (ptrans p i) in (let TMP_6 \def
  34 (lift1 TMP_5 v) in (let TMP_7 \def (CHead e2 TMP_4 TMP_6) in (getl TMP_3 c2
  35 TMP_7))))))) in (ex2 C TMP_2 TMP_8)))))))))))) in (let TMP_21 \def (\lambda
  36 (c1: C).(\lambda (c2: C).(\lambda (H: (drop1 PNil c2 c1)).(\lambda (b:
  37 B).(\lambda (e1: C).(\lambda (v: T).(\lambda (i: nat).(\lambda (H0: (getl i
  38 c1 (CHead e1 (Bind b) v))).(let H_y \def (drop1_gen_pnil c2 c1 H) in (let
  39 TMP_14 \def (\lambda (c: C).(let TMP_10 \def (\lambda (e2: C).(drop1 PNil e2
  40 e1)) in (let TMP_13 \def (\lambda (e2: C).(let TMP_11 \def (Bind b) in (let
  41 TMP_12 \def (CHead e2 TMP_11 v) in (getl i c TMP_12)))) in (ex2 C TMP_10
  42 TMP_13)))) in (let TMP_15 \def (\lambda (e2: C).(drop1 PNil e2 e1)) in (let
  43 TMP_18 \def (\lambda (e2: C).(let TMP_16 \def (Bind b) in (let TMP_17 \def
  44 (CHead e2 TMP_16 v) in (getl i c1 TMP_17)))) in (let TMP_19 \def (drop1_nil
  45 e1) in (let TMP_20 \def (ex_intro2 C TMP_15 TMP_18 e1 TMP_19 H0) in (eq_ind_r
  46 C c1 TMP_14 TMP_20 c2 H_y))))))))))))))) in (let TMP_210 \def (\lambda (h:
  47 nat).(\lambda (d: nat).(\lambda (hds0: PList).(\lambda (H: ((\forall (c1:
  48 C).(\forall (c2: C).((drop1 hds0 c2 c1) \to (\forall (b: B).(\forall (e1:
  49 C).(\forall (v: T).(\forall (i: nat).((getl i c1 (CHead e1 (Bind b) v)) \to
  50 (ex2 C (\lambda (e2: C).(drop1 (ptrans hds0 i) e2 e1)) (\lambda (e2: C).(getl
  51 (trans hds0 i) c2 (CHead e2 (Bind b) (lift1 (ptrans hds0 i)
  52 v))))))))))))))).(\lambda (c1: C).(\lambda (c2: C).(\lambda (H0: (drop1
  53 (PCons h d hds0) c2 c1)).(\lambda (b: B).(\lambda (e1: C).(\lambda (v:
  54 T).(\lambda (i: nat).(\lambda (H1: (getl i c1 (CHead e1 (Bind b) v))).(let
  55 H_x \def (drop1_gen_pcons c2 c1 hds0 h d H0) in (let H2 \def H_x in (let
  56 TMP_22 \def (\lambda (c3: C).(drop h d c2 c3)) in (let TMP_23 \def (\lambda
  57 (c3: C).(drop1 hds0 c3 c1)) in (let TMP_31 \def (\lambda (e2: C).(let TMP_24
  58 \def (trans hds0 i) in (let TMP_25 \def (blt TMP_24 d) in (let TMP_30 \def
  59 (match TMP_25 with [true \Rightarrow (let TMP_26 \def (trans hds0 i) in (let
  60 TMP_27 \def (S TMP_26) in (let TMP_28 \def (minus d TMP_27) in (let TMP_29
  61 \def (ptrans hds0 i) in (PCons h TMP_28 TMP_29))))) | false \Rightarrow
  62 (ptrans hds0 i)]) in (drop1 TMP_30 e2 e1))))) in (let TMP_46 \def (\lambda
  63 (e2: C).(let TMP_32 \def (trans hds0 i) in (let TMP_33 \def (blt TMP_32 d) in
  64 (let TMP_35 \def (match TMP_33 with [true \Rightarrow (trans hds0 i) | false
  65 \Rightarrow (let TMP_34 \def (trans hds0 i) in (plus TMP_34 h))]) in (let
  66 TMP_36 \def (Bind b) in (let TMP_37 \def (trans hds0 i) in (let TMP_38 \def
  67 (blt TMP_37 d) in (let TMP_43 \def (match TMP_38 with [true \Rightarrow (let
  68 TMP_39 \def (trans hds0 i) in (let TMP_40 \def (S TMP_39) in (let TMP_41 \def
  69 (minus d TMP_40) in (let TMP_42 \def (ptrans hds0 i) in (PCons h TMP_41
  70 TMP_42))))) | false \Rightarrow (ptrans hds0 i)]) in (let TMP_44 \def (lift1
  71 TMP_43 v) in (let TMP_45 \def (CHead e2 TMP_36 TMP_44) in (getl TMP_35 c2
  72 TMP_45))))))))))) in (let TMP_47 \def (ex2 C TMP_31 TMP_46) in (let TMP_209
  73 \def (\lambda (x: C).(\lambda (H3: (drop h d c2 x)).(\lambda (H4: (drop1 hds0
  74 x c1)).(let TMP_48 \def (trans hds0 i) in (let TMP_49 \def (blt TMP_48 d) in
  75 (let TMP_67 \def (\lambda (b0: bool).(let TMP_55 \def (\lambda (e2: C).(let
  76 TMP_54 \def (match b0 with [true \Rightarrow (let TMP_50 \def (trans hds0 i)
  77 in (let TMP_51 \def (S TMP_50) in (let TMP_52 \def (minus d TMP_51) in (let
  78 TMP_53 \def (ptrans hds0 i) in (PCons h TMP_52 TMP_53))))) | false
  79 \Rightarrow (ptrans hds0 i)]) in (drop1 TMP_54 e2 e1))) in (let TMP_66 \def
  80 (\lambda (e2: C).(let TMP_57 \def (match b0 with [true \Rightarrow (trans
  81 hds0 i) | false \Rightarrow (let TMP_56 \def (trans hds0 i) in (plus TMP_56
  82 h))]) in (let TMP_58 \def (Bind b) in (let TMP_63 \def (match b0 with [true
  83 \Rightarrow (let TMP_59 \def (trans hds0 i) in (let TMP_60 \def (S TMP_59) in
  84 (let TMP_61 \def (minus d TMP_60) in (let TMP_62 \def (ptrans hds0 i) in
  85 (PCons h TMP_61 TMP_62))))) | false \Rightarrow (ptrans hds0 i)]) in (let
  86 TMP_64 \def (lift1 TMP_63 v) in (let TMP_65 \def (CHead e2 TMP_58 TMP_64) in
  87 (getl TMP_57 c2 TMP_65))))))) in (ex2 C TMP_55 TMP_66)))) in (let TMP_208
  88 \def (\lambda (x_x: bool).(let TMP_85 \def (\lambda (b0: bool).((eq bool (blt
  89 (trans hds0 i) d) b0) \to (let TMP_73 \def (\lambda (e2: C).(let TMP_72 \def
  90 (match b0 with [true \Rightarrow (let TMP_68 \def (trans hds0 i) in (let
  91 TMP_69 \def (S TMP_68) in (let TMP_70 \def (minus d TMP_69) in (let TMP_71
  92 \def (ptrans hds0 i) in (PCons h TMP_70 TMP_71))))) | false \Rightarrow
  93 (ptrans hds0 i)]) in (drop1 TMP_72 e2 e1))) in (let TMP_84 \def (\lambda (e2:
  94 C).(let TMP_75 \def (match b0 with [true \Rightarrow (trans hds0 i) | false
  95 \Rightarrow (let TMP_74 \def (trans hds0 i) in (plus TMP_74 h))]) in (let
  96 TMP_76 \def (Bind b) in (let TMP_81 \def (match b0 with [true \Rightarrow
  97 (let TMP_77 \def (trans hds0 i) in (let TMP_78 \def (S TMP_77) in (let TMP_79
  98 \def (minus d TMP_78) in (let TMP_80 \def (ptrans hds0 i) in (PCons h TMP_79
  99 TMP_80))))) | false \Rightarrow (ptrans hds0 i)]) in (let TMP_82 \def (lift1
 100 TMP_81 v) in (let TMP_83 \def (CHead e2 TMP_76 TMP_82) in (getl TMP_75 c2
 101 TMP_83))))))) in (ex2 C TMP_73 TMP_84))))) in (let TMP_170 \def (\lambda (H5:
 102 (eq bool (blt (trans hds0 i) d) true)).(let H_x0 \def (H c1 x H4 b e1 v i H1)
 103 in (let H6 \def H_x0 in (let TMP_87 \def (\lambda (e2: C).(let TMP_86 \def
 104 (ptrans hds0 i) in (drop1 TMP_86 e2 e1))) in (let TMP_93 \def (\lambda (e2:
 105 C).(let TMP_88 \def (trans hds0 i) in (let TMP_89 \def (Bind b) in (let
 106 TMP_90 \def (ptrans hds0 i) in (let TMP_91 \def (lift1 TMP_90 v) in (let
 107 TMP_92 \def (CHead e2 TMP_89 TMP_91) in (getl TMP_88 x TMP_92))))))) in (let
 108 TMP_99 \def (\lambda (e2: C).(let TMP_94 \def (trans hds0 i) in (let TMP_95
 109 \def (S TMP_94) in (let TMP_96 \def (minus d TMP_95) in (let TMP_97 \def
 110 (ptrans hds0 i) in (let TMP_98 \def (PCons h TMP_96 TMP_97) in (drop1 TMP_98
 111 e2 e1))))))) in (let TMP_109 \def (\lambda (e2: C).(let TMP_100 \def (trans
 112 hds0 i) in (let TMP_101 \def (Bind b) in (let TMP_102 \def (trans hds0 i) in
 113 (let TMP_103 \def (S TMP_102) in (let TMP_104 \def (minus d TMP_103) in (let
 114 TMP_105 \def (ptrans hds0 i) in (let TMP_106 \def (PCons h TMP_104 TMP_105)
 115 in (let TMP_107 \def (lift1 TMP_106 v) in (let TMP_108 \def (CHead e2 TMP_101
 116 TMP_107) in (getl TMP_100 c2 TMP_108))))))))))) in (let TMP_110 \def (ex2 C
 117 TMP_99 TMP_109) in (let TMP_169 \def (\lambda (x0: C).(\lambda (H7: (drop1
 118 (ptrans hds0 i) x0 e1)).(\lambda (H8: (getl (trans hds0 i) x (CHead x0 (Bind
 119 b) (lift1 (ptrans hds0 i) v)))).(let TMP_111 \def (trans hds0 i) in (let
 120 TMP_112 \def (trans hds0 i) in (let TMP_113 \def (blt_lt d TMP_112 H5) in
 121 (let TMP_114 \def (ptrans hds0 i) in (let TMP_115 \def (lift1 TMP_114 v) in
 122 (let H_x1 \def (drop_getl_trans_lt TMP_111 d TMP_113 c2 x h H3 b x0 TMP_115
 123 H8) in (let H9 \def H_x1 in (let TMP_125 \def (\lambda (e2: C).(let TMP_116
 124 \def (trans hds0 i) in (let TMP_117 \def (Bind b) in (let TMP_118 \def (trans
 125 hds0 i) in (let TMP_119 \def (S TMP_118) in (let TMP_120 \def (minus d
 126 TMP_119) in (let TMP_121 \def (ptrans hds0 i) in (let TMP_122 \def (lift1
 127 TMP_121 v) in (let TMP_123 \def (lift h TMP_120 TMP_122) in (let TMP_124 \def
 128 (CHead e2 TMP_117 TMP_123) in (getl TMP_116 c2 TMP_124))))))))))) in (let
 129 TMP_129 \def (\lambda (e2: C).(let TMP_126 \def (trans hds0 i) in (let
 130 TMP_127 \def (S TMP_126) in (let TMP_128 \def (minus d TMP_127) in (drop h
 131 TMP_128 e2 x0))))) in (let TMP_135 \def (\lambda (e2: C).(let TMP_130 \def
 132 (trans hds0 i) in (let TMP_131 \def (S TMP_130) in (let TMP_132 \def (minus d
 133 TMP_131) in (let TMP_133 \def (ptrans hds0 i) in (let TMP_134 \def (PCons h
 134 TMP_132 TMP_133) in (drop1 TMP_134 e2 e1))))))) in (let TMP_145 \def (\lambda
 135 (e2: C).(let TMP_136 \def (trans hds0 i) in (let TMP_137 \def (Bind b) in
 136 (let TMP_138 \def (trans hds0 i) in (let TMP_139 \def (S TMP_138) in (let
 137 TMP_140 \def (minus d TMP_139) in (let TMP_141 \def (ptrans hds0 i) in (let
 138 TMP_142 \def (PCons h TMP_140 TMP_141) in (let TMP_143 \def (lift1 TMP_142 v)
 139 in (let TMP_144 \def (CHead e2 TMP_137 TMP_143) in (getl TMP_136 c2
 140 TMP_144))))))))))) in (let TMP_146 \def (ex2 C TMP_135 TMP_145) in (let
 141 TMP_168 \def (\lambda (x1: C).(\lambda (H10: (getl (trans hds0 i) c2 (CHead
 142 x1 (Bind b) (lift h (minus d (S (trans hds0 i))) (lift1 (ptrans hds0 i)
 143 v))))).(\lambda (H11: (drop h (minus d (S (trans hds0 i))) x1 x0)).(let
 144 TMP_152 \def (\lambda (e2: C).(let TMP_147 \def (trans hds0 i) in (let
 145 TMP_148 \def (S TMP_147) in (let TMP_149 \def (minus d TMP_148) in (let
 146 TMP_150 \def (ptrans hds0 i) in (let TMP_151 \def (PCons h TMP_149 TMP_150)
 147 in (drop1 TMP_151 e2 e1))))))) in (let TMP_162 \def (\lambda (e2: C).(let
 148 TMP_153 \def (trans hds0 i) in (let TMP_154 \def (Bind b) in (let TMP_155
 149 \def (trans hds0 i) in (let TMP_156 \def (S TMP_155) in (let TMP_157 \def
 150 (minus d TMP_156) in (let TMP_158 \def (ptrans hds0 i) in (let TMP_159 \def
 151 (PCons h TMP_157 TMP_158) in (let TMP_160 \def (lift1 TMP_159 v) in (let
 152 TMP_161 \def (CHead e2 TMP_154 TMP_160) in (getl TMP_153 c2
 153 TMP_161))))))))))) in (let TMP_163 \def (trans hds0 i) in (let TMP_164 \def
 154 (S TMP_163) in (let TMP_165 \def (minus d TMP_164) in (let TMP_166 \def
 155 (ptrans hds0 i) in (let TMP_167 \def (drop1_cons x1 x0 h TMP_165 H11 e1
 156 TMP_166 H7) in (ex_intro2 C TMP_152 TMP_162 x1 TMP_167 H10))))))))))) in
 157 (ex2_ind C TMP_125 TMP_129 TMP_146 TMP_168 H9))))))))))))))))) in (ex2_ind C
 158 TMP_87 TMP_93 TMP_110 TMP_169 H6)))))))))) in (let TMP_207 \def (\lambda (H5:
 159 (eq bool (blt (trans hds0 i) d) false)).(let H_x0 \def (H c1 x H4 b e1 v i
 160 H1) in (let H6 \def H_x0 in (let TMP_172 \def (\lambda (e2: C).(let TMP_171
 161 \def (ptrans hds0 i) in (drop1 TMP_171 e2 e1))) in (let TMP_178 \def (\lambda
 162 (e2: C).(let TMP_173 \def (trans hds0 i) in (let TMP_174 \def (Bind b) in
 163 (let TMP_175 \def (ptrans hds0 i) in (let TMP_176 \def (lift1 TMP_175 v) in
 164 (let TMP_177 \def (CHead e2 TMP_174 TMP_176) in (getl TMP_173 x
 165 TMP_177))))))) in (let TMP_180 \def (\lambda (e2: C).(let TMP_179 \def
 166 (ptrans hds0 i) in (drop1 TMP_179 e2 e1))) in (let TMP_187 \def (\lambda (e2:
 167 C).(let TMP_181 \def (trans hds0 i) in (let TMP_182 \def (plus TMP_181 h) in
 168 (let TMP_183 \def (Bind b) in (let TMP_184 \def (ptrans hds0 i) in (let
 169 TMP_185 \def (lift1 TMP_184 v) in (let TMP_186 \def (CHead e2 TMP_183
 170 TMP_185) in (getl TMP_182 c2 TMP_186)))))))) in (let TMP_188 \def (ex2 C
 171 TMP_180 TMP_187) in (let TMP_206 \def (\lambda (x0: C).(\lambda (H7: (drop1
 172 (ptrans hds0 i) x0 e1)).(\lambda (H8: (getl (trans hds0 i) x (CHead x0 (Bind
 173 b) (lift1 (ptrans hds0 i) v)))).(let TMP_189 \def (trans hds0 i) in (let
 174 TMP_190 \def (Bind b) in (let TMP_191 \def (ptrans hds0 i) in (let TMP_192
 175 \def (lift1 TMP_191 v) in (let TMP_193 \def (CHead x0 TMP_190 TMP_192) in
 176 (let H9 \def (drop_getl_trans_ge TMP_189 c2 x d h H3 TMP_193 H8) in (let
 177 TMP_195 \def (\lambda (e2: C).(let TMP_194 \def (ptrans hds0 i) in (drop1
 178 TMP_194 e2 e1))) in (let TMP_202 \def (\lambda (e2: C).(let TMP_196 \def
 179 (trans hds0 i) in (let TMP_197 \def (plus TMP_196 h) in (let TMP_198 \def
 180 (Bind b) in (let TMP_199 \def (ptrans hds0 i) in (let TMP_200 \def (lift1
 181 TMP_199 v) in (let TMP_201 \def (CHead e2 TMP_198 TMP_200) in (getl TMP_197
 182 c2 TMP_201)))))))) in (let TMP_203 \def (trans hds0 i) in (let TMP_204 \def
 183 (bge_le d TMP_203 H5) in (let TMP_205 \def (H9 TMP_204) in (ex_intro2 C
 184 TMP_195 TMP_202 x0 H7 TMP_205))))))))))))))) in (ex2_ind C TMP_172 TMP_178
 185 TMP_188 TMP_206 H6)))))))))) in (bool_ind TMP_85 TMP_170 TMP_207 x_x))))) in
 186 (xinduction bool TMP_49 TMP_67 TMP_208)))))))) in (ex2_ind C TMP_22 TMP_23
 187 TMP_47 TMP_209 H2))))))))))))))))))))) in (PList_ind TMP_9 TMP_21 TMP_210
 188 hds)))).
 189