1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 include "Basic-1/lift/fwd.ma".
19 include "Basic-1/tlt/props.ma".
21 theorem lift_weight_map:
22 \forall (t: T).(\forall (h: nat).(\forall (d: nat).(\forall (f: ((nat \to
23 nat))).(((\forall (m: nat).((le d m) \to (eq nat (f m) O)))) \to (eq nat
24 (weight_map f (lift h d t)) (weight_map f t))))))
26 \lambda (t: T).(T_ind (\lambda (t0: T).(\forall (h: nat).(\forall (d:
27 nat).(\forall (f: ((nat \to nat))).(((\forall (m: nat).((le d m) \to (eq nat
28 (f m) O)))) \to (eq nat (weight_map f (lift h d t0)) (weight_map f t0)))))))
29 (\lambda (n: nat).(\lambda (_: nat).(\lambda (d: nat).(\lambda (f: ((nat \to
30 nat))).(\lambda (_: ((\forall (m: nat).((le d m) \to (eq nat (f m)
31 O))))).(refl_equal nat (weight_map f (TSort n)))))))) (\lambda (n:
32 nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (f: ((nat \to
33 nat))).(\lambda (H: ((\forall (m: nat).((le d m) \to (eq nat (f m)
34 O))))).(lt_le_e n d (eq nat (weight_map f (lift h d (TLRef n))) (weight_map f
35 (TLRef n))) (\lambda (H0: (lt n d)).(eq_ind_r T (TLRef n) (\lambda (t0:
36 T).(eq nat (weight_map f t0) (weight_map f (TLRef n)))) (refl_equal nat
37 (weight_map f (TLRef n))) (lift h d (TLRef n)) (lift_lref_lt n h d H0)))
38 (\lambda (H0: (le d n)).(eq_ind_r T (TLRef (plus n h)) (\lambda (t0: T).(eq
39 nat (weight_map f t0) (weight_map f (TLRef n)))) (eq_ind_r nat O (\lambda
40 (n0: nat).(eq nat (f (plus n h)) n0)) (H (plus n h) (le_plus_trans d n h H0))
41 (f n) (H n H0)) (lift h d (TLRef n)) (lift_lref_ge n h d H0))))))))) (\lambda
42 (k: K).(\lambda (t0: T).(\lambda (H: ((\forall (h: nat).(\forall (d:
43 nat).(\forall (f: ((nat \to nat))).(((\forall (m: nat).((le d m) \to (eq nat
44 (f m) O)))) \to (eq nat (weight_map f (lift h d t0)) (weight_map f
45 t0)))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (h: nat).(\forall (d:
46 nat).(\forall (f: ((nat \to nat))).(((\forall (m: nat).((le d m) \to (eq nat
47 (f m) O)))) \to (eq nat (weight_map f (lift h d t1)) (weight_map f
48 t1)))))))).(\lambda (h: nat).(\lambda (d: nat).(\lambda (f: ((nat \to
49 nat))).(\lambda (H1: ((\forall (m: nat).((le d m) \to (eq nat (f m)
50 O))))).(K_ind (\lambda (k0: K).(eq nat (weight_map f (lift h d (THead k0 t0
51 t1))) (weight_map f (THead k0 t0 t1)))) (\lambda (b: B).(eq_ind_r T (THead
52 (Bind b) (lift h d t0) (lift h (s (Bind b) d) t1)) (\lambda (t2: T).(eq nat
53 (weight_map f t2) (weight_map f (THead (Bind b) t0 t1)))) (B_ind (\lambda
54 (b0: B).(eq nat (match b0 with [Abbr \Rightarrow (S (plus (weight_map f (lift
55 h d t0)) (weight_map (wadd f (S (weight_map f (lift h d t0)))) (lift h (S d)
56 t1)))) | Abst \Rightarrow (S (plus (weight_map f (lift h d t0)) (weight_map
57 (wadd f O) (lift h (S d) t1)))) | Void \Rightarrow (S (plus (weight_map f
58 (lift h d t0)) (weight_map (wadd f O) (lift h (S d) t1))))]) (match b0 with
59 [Abbr \Rightarrow (S (plus (weight_map f t0) (weight_map (wadd f (S
60 (weight_map f t0))) t1))) | Abst \Rightarrow (S (plus (weight_map f t0)
61 (weight_map (wadd f O) t1))) | Void \Rightarrow (S (plus (weight_map f t0)
62 (weight_map (wadd f O) t1)))]))) (eq_ind_r nat (weight_map f t0) (\lambda (n:
63 nat).(eq nat (S (plus n (weight_map (wadd f (S n)) (lift h (S d) t1)))) (S
64 (plus (weight_map f t0) (weight_map (wadd f (S (weight_map f t0))) t1)))))
65 (eq_ind_r nat (weight_map (wadd f (S (weight_map f t0))) t1) (\lambda (n:
66 nat).(eq nat (S (plus (weight_map f t0) n)) (S (plus (weight_map f t0)
67 (weight_map (wadd f (S (weight_map f t0))) t1))))) (refl_equal nat (S (plus
68 (weight_map f t0) (weight_map (wadd f (S (weight_map f t0))) t1))))
69 (weight_map (wadd f (S (weight_map f t0))) (lift h (S d) t1)) (H0 h (S d)
70 (wadd f (S (weight_map f t0))) (\lambda (m: nat).(\lambda (H2: (le (S d)
71 m)).(ex2_ind nat (\lambda (n: nat).(eq nat m (S n))) (\lambda (n: nat).(le d
72 n)) (eq nat (wadd f (S (weight_map f t0)) m) O) (\lambda (x: nat).(\lambda
73 (H3: (eq nat m (S x))).(\lambda (H4: (le d x)).(eq_ind_r nat (S x) (\lambda
74 (n: nat).(eq nat (wadd f (S (weight_map f t0)) n) O)) (H1 x H4) m H3))))
75 (le_gen_S d m H2)))))) (weight_map f (lift h d t0)) (H h d f H1)) (eq_ind_r
76 nat (weight_map (wadd f O) t1) (\lambda (n: nat).(eq nat (S (plus (weight_map
77 f (lift h d t0)) n)) (S (plus (weight_map f t0) (weight_map (wadd f O)
78 t1))))) (f_equal nat nat S (plus (weight_map f (lift h d t0)) (weight_map
79 (wadd f O) t1)) (plus (weight_map f t0) (weight_map (wadd f O) t1)) (f_equal2
80 nat nat nat plus (weight_map f (lift h d t0)) (weight_map f t0) (weight_map
81 (wadd f O) t1) (weight_map (wadd f O) t1) (H h d f H1) (refl_equal nat
82 (weight_map (wadd f O) t1)))) (weight_map (wadd f O) (lift h (S d) t1)) (H0 h
83 (S d) (wadd f O) (\lambda (m: nat).(\lambda (H2: (le (S d) m)).(ex2_ind nat
84 (\lambda (n: nat).(eq nat m (S n))) (\lambda (n: nat).(le d n)) (eq nat (wadd
85 f O m) O) (\lambda (x: nat).(\lambda (H3: (eq nat m (S x))).(\lambda (H4: (le
86 d x)).(eq_ind_r nat (S x) (\lambda (n: nat).(eq nat (wadd f O n) O)) (H1 x
87 H4) m H3)))) (le_gen_S d m H2)))))) (eq_ind_r nat (weight_map (wadd f O) t1)
88 (\lambda (n: nat).(eq nat (S (plus (weight_map f (lift h d t0)) n)) (S (plus
89 (weight_map f t0) (weight_map (wadd f O) t1))))) (f_equal nat nat S (plus
90 (weight_map f (lift h d t0)) (weight_map (wadd f O) t1)) (plus (weight_map f
91 t0) (weight_map (wadd f O) t1)) (f_equal2 nat nat nat plus (weight_map f
92 (lift h d t0)) (weight_map f t0) (weight_map (wadd f O) t1) (weight_map (wadd
93 f O) t1) (H h d f H1) (refl_equal nat (weight_map (wadd f O) t1))))
94 (weight_map (wadd f O) (lift h (S d) t1)) (H0 h (S d) (wadd f O) (\lambda (m:
95 nat).(\lambda (H2: (le (S d) m)).(ex2_ind nat (\lambda (n: nat).(eq nat m (S
96 n))) (\lambda (n: nat).(le d n)) (eq nat (wadd f O m) O) (\lambda (x:
97 nat).(\lambda (H3: (eq nat m (S x))).(\lambda (H4: (le d x)).(eq_ind_r nat (S
98 x) (\lambda (n: nat).(eq nat (wadd f O n) O)) (H1 x H4) m H3)))) (le_gen_S d
99 m H2)))))) b) (lift h d (THead (Bind b) t0 t1)) (lift_head (Bind b) t0 t1 h
100 d))) (\lambda (f0: F).(eq_ind_r T (THead (Flat f0) (lift h d t0) (lift h (s
101 (Flat f0) d) t1)) (\lambda (t2: T).(eq nat (weight_map f t2) (weight_map f
102 (THead (Flat f0) t0 t1)))) (f_equal nat nat S (plus (weight_map f (lift h d
103 t0)) (weight_map f (lift h d t1))) (plus (weight_map f t0) (weight_map f t1))
104 (f_equal2 nat nat nat plus (weight_map f (lift h d t0)) (weight_map f t0)
105 (weight_map f (lift h d t1)) (weight_map f t1) (H h d f H1) (H0 h d f H1)))
106 (lift h d (THead (Flat f0) t0 t1)) (lift_head (Flat f0) t0 t1 h d)))
113 \forall (t: T).(\forall (h: nat).(\forall (d: nat).(eq nat (weight (lift h d
116 \lambda (t: T).(\lambda (h: nat).(\lambda (d: nat).(lift_weight_map t h d
117 (\lambda (_: nat).O) (\lambda (m: nat).(\lambda (_: (le d m)).(refl_equal nat
123 theorem lift_weight_add:
124 \forall (w: nat).(\forall (t: T).(\forall (h: nat).(\forall (d:
125 nat).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
126 (m: nat).((lt m d) \to (eq nat (g m) (f m))))) \to ((eq nat (g d) w) \to
127 (((\forall (m: nat).((le d m) \to (eq nat (g (S m)) (f m))))) \to (eq nat
128 (weight_map f (lift h d t)) (weight_map g (lift (S h) d t)))))))))))
130 \lambda (w: nat).(\lambda (t: T).(T_ind (\lambda (t0: T).(\forall (h:
131 nat).(\forall (d: nat).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
132 nat))).(((\forall (m: nat).((lt m d) \to (eq nat (g m) (f m))))) \to ((eq nat
133 (g d) w) \to (((\forall (m: nat).((le d m) \to (eq nat (g (S m)) (f m)))))
134 \to (eq nat (weight_map f (lift h d t0)) (weight_map g (lift (S h) d
135 t0))))))))))) (\lambda (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda
136 (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (_: ((\forall (m:
137 nat).((lt m d) \to (eq nat (g m) (f m)))))).(\lambda (_: (eq nat (g d)
138 w)).(\lambda (_: ((\forall (m: nat).((le d m) \to (eq nat (g (S m)) (f
139 m)))))).(refl_equal nat (weight_map g (lift (S h) d (TSort n))))))))))))
140 (\lambda (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (f: ((nat \to
141 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H: ((\forall (m: nat).((lt m
142 d) \to (eq nat (g m) (f m)))))).(\lambda (_: (eq nat (g d) w)).(\lambda (H1:
143 ((\forall (m: nat).((le d m) \to (eq nat (g (S m)) (f m)))))).(lt_le_e n d
144 (eq nat (weight_map f (lift h d (TLRef n))) (weight_map g (lift (S h) d
145 (TLRef n)))) (\lambda (H2: (lt n d)).(eq_ind_r T (TLRef n) (\lambda (t0:
146 T).(eq nat (weight_map f t0) (weight_map g (lift (S h) d (TLRef n)))))
147 (eq_ind_r T (TLRef n) (\lambda (t0: T).(eq nat (weight_map f (TLRef n))
148 (weight_map g t0))) (sym_eq nat (g n) (f n) (H n H2)) (lift (S h) d (TLRef
149 n)) (lift_lref_lt n (S h) d H2)) (lift h d (TLRef n)) (lift_lref_lt n h d
150 H2))) (\lambda (H2: (le d n)).(eq_ind_r T (TLRef (plus n h)) (\lambda (t0:
151 T).(eq nat (weight_map f t0) (weight_map g (lift (S h) d (TLRef n)))))
152 (eq_ind_r T (TLRef (plus n (S h))) (\lambda (t0: T).(eq nat (weight_map f
153 (TLRef (plus n h))) (weight_map g t0))) (eq_ind nat (S (plus n h)) (\lambda
154 (n0: nat).(eq nat (f (plus n h)) (g n0))) (sym_eq nat (g (S (plus n h))) (f
155 (plus n h)) (H1 (plus n h) (le_plus_trans d n h H2))) (plus n (S h))
156 (plus_n_Sm n h)) (lift (S h) d (TLRef n)) (lift_lref_ge n (S h) d H2)) (lift
157 h d (TLRef n)) (lift_lref_ge n h d H2)))))))))))) (\lambda (k: K).(\lambda
158 (t0: T).(\lambda (H: ((\forall (h: nat).(\forall (d: nat).(\forall (f: ((nat
159 \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).((lt m d) \to
160 (eq nat (g m) (f m))))) \to ((eq nat (g d) w) \to (((\forall (m: nat).((le d
161 m) \to (eq nat (g (S m)) (f m))))) \to (eq nat (weight_map f (lift h d t0))
162 (weight_map g (lift (S h) d t0)))))))))))).(\lambda (t1: T).(\lambda (H0:
163 ((\forall (h: nat).(\forall (d: nat).(\forall (f: ((nat \to nat))).(\forall
164 (g: ((nat \to nat))).(((\forall (m: nat).((lt m d) \to (eq nat (g m) (f
165 m))))) \to ((eq nat (g d) w) \to (((\forall (m: nat).((le d m) \to (eq nat (g
166 (S m)) (f m))))) \to (eq nat (weight_map f (lift h d t1)) (weight_map g (lift
167 (S h) d t1)))))))))))).(\lambda (h: nat).(\lambda (d: nat).(\lambda (f: ((nat
168 \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H1: ((\forall (m:
169 nat).((lt m d) \to (eq nat (g m) (f m)))))).(\lambda (H2: (eq nat (g d)
170 w)).(\lambda (H3: ((\forall (m: nat).((le d m) \to (eq nat (g (S m)) (f
171 m)))))).(K_ind (\lambda (k0: K).(eq nat (weight_map f (lift h d (THead k0 t0
172 t1))) (weight_map g (lift (S h) d (THead k0 t0 t1))))) (\lambda (b:
173 B).(eq_ind_r T (THead (Bind b) (lift h d t0) (lift h (s (Bind b) d) t1))
174 (\lambda (t2: T).(eq nat (weight_map f t2) (weight_map g (lift (S h) d (THead
175 (Bind b) t0 t1))))) (eq_ind_r T (THead (Bind b) (lift (S h) d t0) (lift (S h)
176 (s (Bind b) d) t1)) (\lambda (t2: T).(eq nat (weight_map f (THead (Bind b)
177 (lift h d t0) (lift h (s (Bind b) d) t1))) (weight_map g t2))) (B_ind
178 (\lambda (b0: B).(eq nat (match b0 with [Abbr \Rightarrow (S (plus
179 (weight_map f (lift h d t0)) (weight_map (wadd f (S (weight_map f (lift h d
180 t0)))) (lift h (S d) t1)))) | Abst \Rightarrow (S (plus (weight_map f (lift h
181 d t0)) (weight_map (wadd f O) (lift h (S d) t1)))) | Void \Rightarrow (S
182 (plus (weight_map f (lift h d t0)) (weight_map (wadd f O) (lift h (S d)
183 t1))))]) (match b0 with [Abbr \Rightarrow (S (plus (weight_map g (lift (S h)
184 d t0)) (weight_map (wadd g (S (weight_map g (lift (S h) d t0)))) (lift (S h)
185 (S d) t1)))) | Abst \Rightarrow (S (plus (weight_map g (lift (S h) d t0))
186 (weight_map (wadd g O) (lift (S h) (S d) t1)))) | Void \Rightarrow (S (plus
187 (weight_map g (lift (S h) d t0)) (weight_map (wadd g O) (lift (S h) (S d)
188 t1))))]))) (f_equal nat nat S (plus (weight_map f (lift h d t0)) (weight_map
189 (wadd f (S (weight_map f (lift h d t0)))) (lift h (S d) t1))) (plus
190 (weight_map g (lift (S h) d t0)) (weight_map (wadd g (S (weight_map g (lift
191 (S h) d t0)))) (lift (S h) (S d) t1))) (f_equal2 nat nat nat plus (weight_map
192 f (lift h d t0)) (weight_map g (lift (S h) d t0)) (weight_map (wadd f (S
193 (weight_map f (lift h d t0)))) (lift h (S d) t1)) (weight_map (wadd g (S
194 (weight_map g (lift (S h) d t0)))) (lift (S h) (S d) t1)) (H h d f g H1 H2
195 H3) (H0 h (S d) (wadd f (S (weight_map f (lift h d t0)))) (wadd g (S
196 (weight_map g (lift (S h) d t0)))) (\lambda (m: nat).(\lambda (H4: (lt m (S
197 d))).(or_ind (eq nat m O) (ex2 nat (\lambda (m0: nat).(eq nat m (S m0)))
198 (\lambda (m0: nat).(lt m0 d))) (eq nat (wadd g (S (weight_map g (lift (S h) d
199 t0))) m) (wadd f (S (weight_map f (lift h d t0))) m)) (\lambda (H5: (eq nat m
200 O)).(eq_ind_r nat O (\lambda (n: nat).(eq nat (wadd g (S (weight_map g (lift
201 (S h) d t0))) n) (wadd f (S (weight_map f (lift h d t0))) n))) (f_equal nat
202 nat S (weight_map g (lift (S h) d t0)) (weight_map f (lift h d t0)) (sym_eq
203 nat (weight_map f (lift h d t0)) (weight_map g (lift (S h) d t0)) (H h d f g
204 H1 H2 H3))) m H5)) (\lambda (H5: (ex2 nat (\lambda (m0: nat).(eq nat m (S
205 m0))) (\lambda (m0: nat).(lt m0 d)))).(ex2_ind nat (\lambda (m0: nat).(eq nat
206 m (S m0))) (\lambda (m0: nat).(lt m0 d)) (eq nat (wadd g (S (weight_map g
207 (lift (S h) d t0))) m) (wadd f (S (weight_map f (lift h d t0))) m)) (\lambda
208 (x: nat).(\lambda (H6: (eq nat m (S x))).(\lambda (H7: (lt x d)).(eq_ind_r
209 nat (S x) (\lambda (n: nat).(eq nat (wadd g (S (weight_map g (lift (S h) d
210 t0))) n) (wadd f (S (weight_map f (lift h d t0))) n))) (H1 x H7) m H6))))
211 H5)) (lt_gen_xS m d H4)))) H2 (\lambda (m: nat).(\lambda (H4: (le (S d)
212 m)).(ex2_ind nat (\lambda (n: nat).(eq nat m (S n))) (\lambda (n: nat).(le d
213 n)) (eq nat (g m) (wadd f (S (weight_map f (lift h d t0))) m)) (\lambda (x:
214 nat).(\lambda (H5: (eq nat m (S x))).(\lambda (H6: (le d x)).(eq_ind_r nat (S
215 x) (\lambda (n: nat).(eq nat (g n) (wadd f (S (weight_map f (lift h d t0)))
216 n))) (H3 x H6) m H5)))) (le_gen_S d m H4))))))) (f_equal nat nat S (plus
217 (weight_map f (lift h d t0)) (weight_map (wadd f O) (lift h (S d) t1))) (plus
218 (weight_map g (lift (S h) d t0)) (weight_map (wadd g O) (lift (S h) (S d)
219 t1))) (f_equal2 nat nat nat plus (weight_map f (lift h d t0)) (weight_map g
220 (lift (S h) d t0)) (weight_map (wadd f O) (lift h (S d) t1)) (weight_map
221 (wadd g O) (lift (S h) (S d) t1)) (H h d f g H1 H2 H3) (H0 h (S d) (wadd f O)
222 (wadd g O) (\lambda (m: nat).(\lambda (H4: (lt m (S d))).(or_ind (eq nat m O)
223 (ex2 nat (\lambda (m0: nat).(eq nat m (S m0))) (\lambda (m0: nat).(lt m0 d)))
224 (eq nat (wadd g O m) (wadd f O m)) (\lambda (H5: (eq nat m O)).(eq_ind_r nat
225 O (\lambda (n: nat).(eq nat (wadd g O n) (wadd f O n))) (refl_equal nat O) m
226 H5)) (\lambda (H5: (ex2 nat (\lambda (m0: nat).(eq nat m (S m0))) (\lambda
227 (m0: nat).(lt m0 d)))).(ex2_ind nat (\lambda (m0: nat).(eq nat m (S m0)))
228 (\lambda (m0: nat).(lt m0 d)) (eq nat (wadd g O m) (wadd f O m)) (\lambda (x:
229 nat).(\lambda (H6: (eq nat m (S x))).(\lambda (H7: (lt x d)).(eq_ind_r nat (S
230 x) (\lambda (n: nat).(eq nat (wadd g O n) (wadd f O n))) (H1 x H7) m H6))))
231 H5)) (lt_gen_xS m d H4)))) H2 (\lambda (m: nat).(\lambda (H4: (le (S d)
232 m)).(ex2_ind nat (\lambda (n: nat).(eq nat m (S n))) (\lambda (n: nat).(le d
233 n)) (eq nat (g m) (wadd f O m)) (\lambda (x: nat).(\lambda (H5: (eq nat m (S
234 x))).(\lambda (H6: (le d x)).(eq_ind_r nat (S x) (\lambda (n: nat).(eq nat (g
235 n) (wadd f O n))) (H3 x H6) m H5)))) (le_gen_S d m H4))))))) (f_equal nat nat
236 S (plus (weight_map f (lift h d t0)) (weight_map (wadd f O) (lift h (S d)
237 t1))) (plus (weight_map g (lift (S h) d t0)) (weight_map (wadd g O) (lift (S
238 h) (S d) t1))) (f_equal2 nat nat nat plus (weight_map f (lift h d t0))
239 (weight_map g (lift (S h) d t0)) (weight_map (wadd f O) (lift h (S d) t1))
240 (weight_map (wadd g O) (lift (S h) (S d) t1)) (H h d f g H1 H2 H3) (H0 h (S
241 d) (wadd f O) (wadd g O) (\lambda (m: nat).(\lambda (H4: (lt m (S
242 d))).(or_ind (eq nat m O) (ex2 nat (\lambda (m0: nat).(eq nat m (S m0)))
243 (\lambda (m0: nat).(lt m0 d))) (eq nat (wadd g O m) (wadd f O m)) (\lambda
244 (H5: (eq nat m O)).(eq_ind_r nat O (\lambda (n: nat).(eq nat (wadd g O n)
245 (wadd f O n))) (refl_equal nat O) m H5)) (\lambda (H5: (ex2 nat (\lambda (m0:
246 nat).(eq nat m (S m0))) (\lambda (m0: nat).(lt m0 d)))).(ex2_ind nat (\lambda
247 (m0: nat).(eq nat m (S m0))) (\lambda (m0: nat).(lt m0 d)) (eq nat (wadd g O
248 m) (wadd f O m)) (\lambda (x: nat).(\lambda (H6: (eq nat m (S x))).(\lambda
249 (H7: (lt x d)).(eq_ind_r nat (S x) (\lambda (n: nat).(eq nat (wadd g O n)
250 (wadd f O n))) (H1 x H7) m H6)))) H5)) (lt_gen_xS m d H4)))) H2 (\lambda (m:
251 nat).(\lambda (H4: (le (S d) m)).(ex2_ind nat (\lambda (n: nat).(eq nat m (S
252 n))) (\lambda (n: nat).(le d n)) (eq nat (g m) (wadd f O m)) (\lambda (x:
253 nat).(\lambda (H5: (eq nat m (S x))).(\lambda (H6: (le d x)).(eq_ind_r nat (S
254 x) (\lambda (n: nat).(eq nat (g n) (wadd f O n))) (H3 x H6) m H5))))
255 (le_gen_S d m H4))))))) b) (lift (S h) d (THead (Bind b) t0 t1)) (lift_head
256 (Bind b) t0 t1 (S h) d)) (lift h d (THead (Bind b) t0 t1)) (lift_head (Bind
257 b) t0 t1 h d))) (\lambda (f0: F).(eq_ind_r T (THead (Flat f0) (lift h d t0)
258 (lift h (s (Flat f0) d) t1)) (\lambda (t2: T).(eq nat (weight_map f t2)
259 (weight_map g (lift (S h) d (THead (Flat f0) t0 t1))))) (eq_ind_r T (THead
260 (Flat f0) (lift (S h) d t0) (lift (S h) (s (Flat f0) d) t1)) (\lambda (t2:
261 T).(eq nat (weight_map f (THead (Flat f0) (lift h d t0) (lift h (s (Flat f0)
262 d) t1))) (weight_map g t2))) (f_equal nat nat S (plus (weight_map f (lift h d
263 t0)) (weight_map f (lift h d t1))) (plus (weight_map g (lift (S h) d t0))
264 (weight_map g (lift (S h) d t1))) (f_equal2 nat nat nat plus (weight_map f
265 (lift h d t0)) (weight_map g (lift (S h) d t0)) (weight_map f (lift h d t1))
266 (weight_map g (lift (S h) d t1)) (H h d f g H1 H2 H3) (H0 h d f g H1 H2 H3)))
267 (lift (S h) d (THead (Flat f0) t0 t1)) (lift_head (Flat f0) t0 t1 (S h) d))
268 (lift h d (THead (Flat f0) t0 t1)) (lift_head (Flat f0) t0 t1 h d)))
274 theorem lift_weight_add_O:
275 \forall (w: nat).(\forall (t: T).(\forall (h: nat).(\forall (f: ((nat \to
276 nat))).(eq nat (weight_map f (lift h O t)) (weight_map (wadd f w) (lift (S h)
279 \lambda (w: nat).(\lambda (t: T).(\lambda (h: nat).(\lambda (f: ((nat \to
280 nat))).(lift_weight_add (plus (wadd f w O) O) t h O f (wadd f w) (\lambda (m:
281 nat).(\lambda (H: (lt m O)).(lt_x_O m H (eq nat (wadd f w m) (f m)))))
282 (plus_n_O (wadd f w O)) (\lambda (m: nat).(\lambda (_: (le O m)).(refl_equal
289 \forall (k: K).(\forall (u: T).(\forall (t: T).(\forall (h: nat).(\forall
290 (d: nat).(tlt t (THead k u (lift h d t)))))))
292 \lambda (k: K).(\lambda (u: T).(\lambda (t: T).(\lambda (h: nat).(\lambda
293 (d: nat).(eq_ind nat (weight (lift h d t)) (\lambda (n: nat).(lt n (weight
294 (THead k u (lift h d t))))) (tlt_head_dx k u (lift h d t)) (weight t)
295 (lift_weight t h d)))))).