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 set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst0/tlt".
19 include "subst0/defs.ma".
21 include "lift/props.ma".
23 include "lift/tlt.ma".
25 theorem subst0_weight_le:
26 \forall (u: T).(\forall (t: T).(\forall (z: T).(\forall (d: nat).((subst0 d
27 u t z) \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
28 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
29 d) O u)) (g d)) \to (le (weight_map f z) (weight_map g t))))))))))
31 \lambda (u: T).(\lambda (t: T).(\lambda (z: T).(\lambda (d: nat).(\lambda
32 (H: (subst0 d u t z)).(subst0_ind (\lambda (n: nat).(\lambda (t0: T).(\lambda
33 (t1: T).(\lambda (t2: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
34 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
35 n) O t0)) (g n)) \to (le (weight_map f t2) (weight_map g t1))))))))))
36 (\lambda (v: T).(\lambda (i: nat).(\lambda (f: ((nat \to nat))).(\lambda (g:
37 ((nat \to nat))).(\lambda (_: ((\forall (m: nat).(le (f m) (g m))))).(\lambda
38 (H1: (lt (weight_map f (lift (S i) O v)) (g i))).(le_S_n (weight_map f (lift
39 (S i) O v)) (weight_map g (TLRef i)) (le_S (S (weight_map f (lift (S i) O
40 v))) (weight_map g (TLRef i)) H1)))))))) (\lambda (v: T).(\lambda (u2:
41 T).(\lambda (u1: T).(\lambda (i: nat).(\lambda (_: (subst0 i v u1
42 u2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
43 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
44 i) O v)) (g i)) \to (le (weight_map f u2) (weight_map g u1)))))))).(\lambda
45 (t0: T).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (f: ((nat \to
46 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
47 \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (le (weight_map f (THead
48 k0 u2 t0)) (weight_map g (THead k0 u1 t0)))))))) (\lambda (b: B).(B_ind
49 (\lambda (b0: B).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
50 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
51 i) O v)) (g i)) \to (le (weight_map f (THead (Bind b0) u2 t0)) (weight_map g
52 (THead (Bind b0) u1 t0)))))))) (\lambda (f: ((nat \to nat))).(\lambda (g:
53 ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f m) (g
54 m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g i))).(le_n_S
55 (plus (weight_map f u2) (weight_map (wadd f (S (weight_map f u2))) t0)) (plus
56 (weight_map g u1) (weight_map (wadd g (S (weight_map g u1))) t0))
57 (plus_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd f (S
58 (weight_map f u2))) t0) (weight_map (wadd g (S (weight_map g u1))) t0) (H1 f
59 g H2 H3) (weight_le t0 (wadd f (S (weight_map f u2))) (wadd g (S (weight_map
60 g u1))) (\lambda (n: nat).(wadd_le f g H2 (S (weight_map f u2)) (S
61 (weight_map g u1)) (le_n_S (weight_map f u2) (weight_map g u1) (H1 f g H2
62 H3)) n))))))))) (\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
63 nat))).(\lambda (H2: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H3: (lt
64 (weight_map f (lift (S i) O v)) (g i))).(le_n_S (plus (weight_map f u2)
65 (weight_map (wadd f O) t0)) (plus (weight_map g u1) (weight_map (wadd g O)
66 t0)) (plus_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd f
67 O) t0) (weight_map (wadd g O) t0) (H1 f g H2 H3) (weight_le t0 (wadd f O)
68 (wadd g O) (\lambda (n: nat).(wadd_le f g H2 O O (le_n O) n))))))))) (\lambda
69 (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall
70 (m: nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O
71 v)) (g i))).(le_n_S (plus (weight_map f u2) (weight_map (wadd f O) t0)) (plus
72 (weight_map g u1) (weight_map (wadd g O) t0)) (plus_le_compat (weight_map f
73 u2) (weight_map g u1) (weight_map (wadd f O) t0) (weight_map (wadd g O) t0)
74 (H1 f g H2 H3) (weight_le t0 (wadd f O) (wadd g O) (\lambda (n: nat).(wadd_le
75 f g H2 O O (le_n O) n))))))))) b)) (\lambda (_: F).(\lambda (f0: ((nat \to
76 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f0
77 m) (g m))))).(\lambda (H3: (lt (weight_map f0 (lift (S i) O v)) (g
78 i))).(lt_le_S (plus (weight_map f0 u2) (weight_map f0 t0)) (S (plus
79 (weight_map g u1) (weight_map g t0))) (le_lt_n_Sm (plus (weight_map f0 u2)
80 (weight_map f0 t0)) (plus (weight_map g u1) (weight_map g t0))
81 (plus_le_compat (weight_map f0 u2) (weight_map g u1) (weight_map f0 t0)
82 (weight_map g t0) (H1 f0 g H2 H3) (weight_le t0 f0 g H2))))))))) k)))))))))
83 (\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (v: T).(\forall (t2:
84 T).(\forall (t1: T).(\forall (i: nat).((subst0 (s k0 i) v t1 t2) \to
85 (((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
86 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S (s k0 i)) O v)) (g (s
87 k0 i))) \to (le (weight_map f t2) (weight_map g t1))))))) \to (\forall (u0:
88 T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
89 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to
90 (le (weight_map f (THead k0 u0 t2)) (weight_map g (THead k0 u0
91 t1))))))))))))))) (\lambda (b: B).(B_ind (\lambda (b0: B).(\forall (v:
92 T).(\forall (t2: T).(\forall (t1: T).(\forall (i: nat).((subst0 (s (Bind b0)
93 i) v t1 t2) \to (((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
94 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
95 (s (Bind b0) i)) O v)) (g (s (Bind b0) i))) \to (le (weight_map f t2)
96 (weight_map g t1))))))) \to (\forall (u0: T).(\forall (f: ((nat \to
97 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
98 \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (le (weight_map f (THead
99 (Bind b0) u0 t2)) (weight_map g (THead (Bind b0) u0 t1)))))))))))))))
100 (\lambda (v: T).(\lambda (t2: T).(\lambda (t1: T).(\lambda (i: nat).(\lambda
101 (_: (subst0 (S i) v t1 t2)).(\lambda (H1: ((\forall (f: ((nat \to
102 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
103 \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (le (weight_map f
104 t2) (weight_map g t1)))))))).(\lambda (u0: T).(\lambda (f: ((nat \to
105 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f
106 m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g
107 i))).(le_n_S (plus (weight_map f u0) (weight_map (wadd f (S (weight_map f
108 u0))) t2)) (plus (weight_map g u0) (weight_map (wadd g (S (weight_map g u0)))
109 t1)) (plus_le_compat (weight_map f u0) (weight_map g u0) (weight_map (wadd f
110 (S (weight_map f u0))) t2) (weight_map (wadd g (S (weight_map g u0))) t1)
111 (weight_le u0 f g H2) (H1 (wadd f (S (weight_map f u0))) (wadd g (S
112 (weight_map g u0))) (\lambda (m: nat).(wadd_le f g H2 (S (weight_map f u0))
113 (S (weight_map g u0)) (le_n_S (weight_map f u0) (weight_map g u0) (weight_le
114 u0 f g H2)) m)) (lt_le_S (weight_map (wadd f (S (weight_map f u0))) (lift (S
115 (S i)) O v)) (wadd g (S (weight_map g u0)) (S i)) (eq_ind nat (weight_map f
116 (lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H3 (weight_map (wadd f (S
117 (weight_map f u0))) (lift (S (S i)) O v)) (lift_weight_add_O (S (weight_map f
118 u0)) v (S i) f))))))))))))))))) (\lambda (v: T).(\lambda (t2: T).(\lambda
119 (t1: T).(\lambda (i: nat).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H1:
120 ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
121 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S
122 i))) \to (le (weight_map f t2) (weight_map g t1)))))))).(\lambda (u0:
123 T).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2:
124 ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift
125 (S i) O v)) (g i))).(le_n_S (plus (weight_map f u0) (weight_map (wadd f O)
126 t2)) (plus (weight_map g u0) (weight_map (wadd g O) t1)) (plus_le_compat
127 (weight_map f u0) (weight_map g u0) (weight_map (wadd f O) t2) (weight_map
128 (wadd g O) t1) (weight_le u0 f g H2) (H1 (wadd f O) (wadd g O) (\lambda (m:
129 nat).(wadd_le f g H2 O O (le_n O) m)) (eq_ind nat (weight_map f (lift (S i) O
130 v)) (\lambda (n: nat).(lt n (g i))) H3 (weight_map (wadd f O) (lift (S (S i))
131 O v)) (lift_weight_add_O O v (S i) f)))))))))))))))) (\lambda (v: T).(\lambda
132 (t2: T).(\lambda (t1: T).(\lambda (i: nat).(\lambda (_: (subst0 (S i) v t1
133 t2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
134 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
135 (S i)) O v)) (g (S i))) \to (le (weight_map f t2) (weight_map g
136 t1)))))))).(\lambda (u0: T).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat
137 \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H3:
138 (lt (weight_map f (lift (S i) O v)) (g i))).(le_n_S (plus (weight_map f u0)
139 (weight_map (wadd f O) t2)) (plus (weight_map g u0) (weight_map (wadd g O)
140 t1)) (plus_le_compat (weight_map f u0) (weight_map g u0) (weight_map (wadd f
141 O) t2) (weight_map (wadd g O) t1) (weight_le u0 f g H2) (H1 (wadd f O) (wadd
142 g O) (\lambda (m: nat).(wadd_le f g H2 O O (le_n O) m)) (eq_ind nat
143 (weight_map f (lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H3
144 (weight_map (wadd f O) (lift (S (S i)) O v)) (lift_weight_add_O O v (S i)
145 f)))))))))))))))) b)) (\lambda (_: F).(\lambda (v: T).(\lambda (t2:
146 T).(\lambda (t1: T).(\lambda (i: nat).(\lambda (_: (subst0 i v t1
147 t2)).(\lambda (H1: ((\forall (f0: ((nat \to nat))).(\forall (g: ((nat \to
148 nat))).(((\forall (m: nat).(le (f0 m) (g m)))) \to ((lt (weight_map f0 (lift
149 (S i) O v)) (g i)) \to (le (weight_map f0 t2) (weight_map g
150 t1)))))))).(\lambda (u0: T).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat
151 \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f0 m) (g m))))).(\lambda
152 (H3: (lt (weight_map f0 (lift (S i) O v)) (g i))).(lt_le_S (plus (weight_map
153 f0 u0) (weight_map f0 t2)) (S (plus (weight_map g u0) (weight_map g t1)))
154 (le_lt_n_Sm (plus (weight_map f0 u0) (weight_map f0 t2)) (plus (weight_map g
155 u0) (weight_map g t1)) (plus_le_compat (weight_map f0 u0) (weight_map g u0)
156 (weight_map f0 t2) (weight_map g t1) (weight_le u0 f0 g H2) (H1 f0 g H2
157 H3)))))))))))))))) k)) (\lambda (v: T).(\lambda (u1: T).(\lambda (u2:
158 T).(\lambda (i: nat).(\lambda (_: (subst0 i v u1 u2)).(\lambda (H1: ((\forall
159 (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f
160 m) (g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (le
161 (weight_map f u2) (weight_map g u1)))))))).(\lambda (k: K).(K_ind (\lambda
162 (k0: K).(\forall (t1: T).(\forall (t2: T).((subst0 (s k0 i) v t1 t2) \to
163 (((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
164 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S (s k0 i)) O v)) (g (s
165 k0 i))) \to (le (weight_map f t2) (weight_map g t1))))))) \to (\forall (f:
166 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
167 (g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (le (weight_map
168 f (THead k0 u2 t2)) (weight_map g (THead k0 u1 t1)))))))))))) (\lambda (b:
169 B).(B_ind (\lambda (b0: B).(\forall (t1: T).(\forall (t2: T).((subst0 (s
170 (Bind b0) i) v t1 t2) \to (((\forall (f: ((nat \to nat))).(\forall (g: ((nat
171 \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f
172 (lift (S (s (Bind b0) i)) O v)) (g (s (Bind b0) i))) \to (le (weight_map f
173 t2) (weight_map g t1))))))) \to (\forall (f: ((nat \to nat))).(\forall (g:
174 ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map
175 f (lift (S i) O v)) (g i)) \to (le (weight_map f (THead (Bind b0) u2 t2))
176 (weight_map g (THead (Bind b0) u1 t1)))))))))))) (\lambda (t1: T).(\lambda
177 (t2: T).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H3: ((\forall (f:
178 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
179 (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (le
180 (weight_map f t2) (weight_map g t1)))))))).(\lambda (f: ((nat \to
181 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H4: ((\forall (m: nat).(le (f
182 m) (g m))))).(\lambda (H5: (lt (weight_map f (lift (S i) O v)) (g
183 i))).(le_n_S (plus (weight_map f u2) (weight_map (wadd f (S (weight_map f
184 u2))) t2)) (plus (weight_map g u1) (weight_map (wadd g (S (weight_map g u1)))
185 t1)) (plus_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd f
186 (S (weight_map f u2))) t2) (weight_map (wadd g (S (weight_map g u1))) t1) (H1
187 f g H4 H5) (H3 (wadd f (S (weight_map f u2))) (wadd g (S (weight_map g u1)))
188 (\lambda (m: nat).(wadd_le f g H4 (S (weight_map f u2)) (S (weight_map g u1))
189 (le_n_S (weight_map f u2) (weight_map g u1) (H1 f g H4 H5)) m)) (lt_le_S
190 (weight_map (wadd f (S (weight_map f u2))) (lift (S (S i)) O v)) (wadd g (S
191 (weight_map g u1)) (S i)) (eq_ind nat (weight_map f (lift (S i) O v))
192 (\lambda (n: nat).(lt n (g i))) H5 (weight_map (wadd f (S (weight_map f u2)))
193 (lift (S (S i)) O v)) (lift_weight_add_O (S (weight_map f u2)) v (S i)
194 f)))))))))))))) (\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (subst0 (S i)
195 v t1 t2)).(\lambda (H3: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
196 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
197 (S i)) O v)) (g (S i))) \to (le (weight_map f t2) (weight_map g
198 t1)))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
199 nat))).(\lambda (H4: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H5: (lt
200 (weight_map f (lift (S i) O v)) (g i))).(le_n_S (plus (weight_map f u2)
201 (weight_map (wadd f O) t2)) (plus (weight_map g u1) (weight_map (wadd g O)
202 t1)) (plus_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd f
203 O) t2) (weight_map (wadd g O) t1) (H1 f g H4 H5) (H3 (wadd f O) (wadd g O)
204 (\lambda (m: nat).(wadd_le f g H4 O O (le_n O) m)) (eq_ind nat (weight_map f
205 (lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H5 (weight_map (wadd f O)
206 (lift (S (S i)) O v)) (lift_weight_add_O O v (S i) f))))))))))))) (\lambda
207 (t1: T).(\lambda (t2: T).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H3:
208 ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
209 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S
210 i))) \to (le (weight_map f t2) (weight_map g t1)))))))).(\lambda (f: ((nat
211 \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H4: ((\forall (m: nat).(le
212 (f m) (g m))))).(\lambda (H5: (lt (weight_map f (lift (S i) O v)) (g
213 i))).(le_n_S (plus (weight_map f u2) (weight_map (wadd f O) t2)) (plus
214 (weight_map g u1) (weight_map (wadd g O) t1)) (plus_le_compat (weight_map f
215 u2) (weight_map g u1) (weight_map (wadd f O) t2) (weight_map (wadd g O) t1)
216 (H1 f g H4 H5) (H3 (wadd f O) (wadd g O) (\lambda (m: nat).(wadd_le f g H4 O
217 O (le_n O) m)) (eq_ind nat (weight_map f (lift (S i) O v)) (\lambda (n:
218 nat).(lt n (g i))) H5 (weight_map (wadd f O) (lift (S (S i)) O v))
219 (lift_weight_add_O O v (S i) f))))))))))))) b)) (\lambda (_: F).(\lambda (t1:
220 T).(\lambda (t2: T).(\lambda (_: (subst0 i v t1 t2)).(\lambda (H3: ((\forall
221 (f0: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le
222 (f0 m) (g m)))) \to ((lt (weight_map f0 (lift (S i) O v)) (g i)) \to (le
223 (weight_map f0 t2) (weight_map g t1)))))))).(\lambda (f0: ((nat \to
224 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H4: ((\forall (m: nat).(le (f0
225 m) (g m))))).(\lambda (H5: (lt (weight_map f0 (lift (S i) O v)) (g
226 i))).(lt_le_S (plus (weight_map f0 u2) (weight_map f0 t2)) (S (plus
227 (weight_map g u1) (weight_map g t1))) (le_lt_n_Sm (plus (weight_map f0 u2)
228 (weight_map f0 t2)) (plus (weight_map g u1) (weight_map g t1))
229 (plus_le_compat (weight_map f0 u2) (weight_map g u1) (weight_map f0 t2)
230 (weight_map g t1) (H1 f0 g H4 H5) (H3 f0 g H4 H5))))))))))))) k)))))))) d u t
233 theorem subst0_weight_lt:
234 \forall (u: T).(\forall (t: T).(\forall (z: T).(\forall (d: nat).((subst0 d
235 u t z) \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
236 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
237 d) O u)) (g d)) \to (lt (weight_map f z) (weight_map g t))))))))))
239 \lambda (u: T).(\lambda (t: T).(\lambda (z: T).(\lambda (d: nat).(\lambda
240 (H: (subst0 d u t z)).(subst0_ind (\lambda (n: nat).(\lambda (t0: T).(\lambda
241 (t1: T).(\lambda (t2: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
242 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
243 n) O t0)) (g n)) \to (lt (weight_map f t2) (weight_map g t1))))))))))
244 (\lambda (v: T).(\lambda (i: nat).(\lambda (f: ((nat \to nat))).(\lambda (g:
245 ((nat \to nat))).(\lambda (_: ((\forall (m: nat).(le (f m) (g m))))).(\lambda
246 (H1: (lt (weight_map f (lift (S i) O v)) (g i))).H1)))))) (\lambda (v:
247 T).(\lambda (u2: T).(\lambda (u1: T).(\lambda (i: nat).(\lambda (_: (subst0 i
248 v u1 u2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
249 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
250 i) O v)) (g i)) \to (lt (weight_map f u2) (weight_map g u1)))))))).(\lambda
251 (t0: T).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (f: ((nat \to
252 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
253 \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (lt (weight_map f (THead
254 k0 u2 t0)) (weight_map g (THead k0 u1 t0)))))))) (\lambda (b: B).(B_ind
255 (\lambda (b0: B).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
256 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
257 i) O v)) (g i)) \to (lt (weight_map f (THead (Bind b0) u2 t0)) (weight_map g
258 (THead (Bind b0) u1 t0)))))))) (\lambda (f: ((nat \to nat))).(\lambda (g:
259 ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f m) (g
260 m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g i))).(lt_n_S
261 (plus (weight_map f u2) (weight_map (wadd f (S (weight_map f u2))) t0)) (plus
262 (weight_map g u1) (weight_map (wadd g (S (weight_map g u1))) t0))
263 (plus_lt_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd f (S
264 (weight_map f u2))) t0) (weight_map (wadd g (S (weight_map g u1))) t0) (H1 f
265 g H2 H3) (weight_le t0 (wadd f (S (weight_map f u2))) (wadd g (S (weight_map
266 g u1))) (\lambda (n: nat).(wadd_le f g H2 (S (weight_map f u2)) (S
267 (weight_map g u1)) (le_S (S (weight_map f u2)) (weight_map g u1) (lt_le_S
268 (weight_map f u2) (weight_map g u1) (H1 f g H2 H3))) n))))))))) (\lambda (f:
269 ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m:
270 nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g
271 i))).(lt_n_S (plus (weight_map f u2) (weight_map (wadd f O) t0)) (plus
272 (weight_map g u1) (weight_map (wadd g O) t0)) (plus_lt_le_compat (weight_map
273 f u2) (weight_map g u1) (weight_map (wadd f O) t0) (weight_map (wadd g O) t0)
274 (H1 f g H2 H3) (weight_le t0 (wadd f O) (wadd g O) (\lambda (n: nat).(le_S_n
275 (wadd f O n) (wadd g O n) (le_n_S (wadd f O n) (wadd g O n) (wadd_le f g H2 O
276 O (le_n O) n))))))))))) (\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
277 nat))).(\lambda (H2: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H3: (lt
278 (weight_map f (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map f u2)
279 (weight_map (wadd f O) t0)) (plus (weight_map g u1) (weight_map (wadd g O)
280 t0)) (plus_lt_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd
281 f O) t0) (weight_map (wadd g O) t0) (H1 f g H2 H3) (weight_le t0 (wadd f O)
282 (wadd g O) (\lambda (n: nat).(le_S_n (wadd f O n) (wadd g O n) (le_n_S (wadd
283 f O n) (wadd g O n) (wadd_le f g H2 O O (le_n O) n))))))))))) b)) (\lambda
284 (_: F).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda
285 (H2: ((\forall (m: nat).(le (f0 m) (g m))))).(\lambda (H3: (lt (weight_map f0
286 (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map f0 u2) (weight_map f0
287 t0)) (plus (weight_map g u1) (weight_map g t0)) (plus_lt_le_compat
288 (weight_map f0 u2) (weight_map g u1) (weight_map f0 t0) (weight_map g t0) (H1
289 f0 g H2 H3) (weight_le t0 f0 g H2)))))))) k))))))))) (\lambda (k: K).(K_ind
290 (\lambda (k0: K).(\forall (v: T).(\forall (t2: T).(\forall (t1: T).(\forall
291 (i: nat).((subst0 (s k0 i) v t1 t2) \to (((\forall (f: ((nat \to
292 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
293 \to ((lt (weight_map f (lift (S (s k0 i)) O v)) (g (s k0 i))) \to (lt
294 (weight_map f t2) (weight_map g t1))))))) \to (\forall (u0: T).(\forall (f:
295 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
296 (g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (lt (weight_map
297 f (THead k0 u0 t2)) (weight_map g (THead k0 u0 t1))))))))))))))) (\lambda (b:
298 B).(B_ind (\lambda (b0: B).(\forall (v: T).(\forall (t2: T).(\forall (t1:
299 T).(\forall (i: nat).((subst0 (s (Bind b0) i) v t1 t2) \to (((\forall (f:
300 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
301 (g m)))) \to ((lt (weight_map f (lift (S (s (Bind b0) i)) O v)) (g (s (Bind
302 b0) i))) \to (lt (weight_map f t2) (weight_map g t1))))))) \to (\forall (u0:
303 T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
304 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to
305 (lt (weight_map f (THead (Bind b0) u0 t2)) (weight_map g (THead (Bind b0) u0
306 t1))))))))))))))) (\lambda (v: T).(\lambda (t2: T).(\lambda (t1: T).(\lambda
307 (i: nat).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H1: ((\forall (f:
308 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
309 (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (lt
310 (weight_map f t2) (weight_map g t1)))))))).(\lambda (u0: T).(\lambda (f:
311 ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m:
312 nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g
313 i))).(lt_n_S (plus (weight_map f u0) (weight_map (wadd f (S (weight_map f
314 u0))) t2)) (plus (weight_map g u0) (weight_map (wadd g (S (weight_map g u0)))
315 t1)) (plus_le_lt_compat (weight_map f u0) (weight_map g u0) (weight_map (wadd
316 f (S (weight_map f u0))) t2) (weight_map (wadd g (S (weight_map g u0))) t1)
317 (weight_le u0 f g H2) (H1 (wadd f (S (weight_map f u0))) (wadd g (S
318 (weight_map g u0))) (\lambda (m: nat).(wadd_le f g H2 (S (weight_map f u0))
319 (S (weight_map g u0)) (lt_le_S (weight_map f u0) (S (weight_map g u0))
320 (le_lt_n_Sm (weight_map f u0) (weight_map g u0) (weight_le u0 f g H2))) m))
321 (lt_le_S (weight_map (wadd f (S (weight_map f u0))) (lift (S (S i)) O v))
322 (wadd g (S (weight_map g u0)) (S i)) (eq_ind nat (weight_map f (lift (S i) O
323 v)) (\lambda (n: nat).(lt n (g i))) H3 (weight_map (wadd f (S (weight_map f
324 u0))) (lift (S (S i)) O v)) (lift_weight_add_O (S (weight_map f u0)) v (S i)
325 f))))))))))))))))) (\lambda (v: T).(\lambda (t2: T).(\lambda (t1: T).(\lambda
326 (i: nat).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H1: ((\forall (f:
327 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
328 (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (lt
329 (weight_map f t2) (weight_map g t1)))))))).(\lambda (u0: T).(\lambda (f:
330 ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m:
331 nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g
332 i))).(lt_n_S (plus (weight_map f u0) (weight_map (wadd f O) t2)) (plus
333 (weight_map g u0) (weight_map (wadd g O) t1)) (plus_le_lt_compat (weight_map
334 f u0) (weight_map g u0) (weight_map (wadd f O) t2) (weight_map (wadd g O) t1)
335 (weight_le u0 f g H2) (H1 (wadd f O) (wadd g O) (\lambda (m: nat).(wadd_le f
336 g H2 O O (le_n O) m)) (eq_ind nat (weight_map f (lift (S i) O v)) (\lambda
337 (n: nat).(lt n (g i))) H3 (weight_map (wadd f O) (lift (S (S i)) O v))
338 (lift_weight_add_O O v (S i) f)))))))))))))))) (\lambda (v: T).(\lambda (t2:
339 T).(\lambda (t1: T).(\lambda (i: nat).(\lambda (_: (subst0 (S i) v t1
340 t2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
341 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
342 (S i)) O v)) (g (S i))) \to (lt (weight_map f t2) (weight_map g
343 t1)))))))).(\lambda (u0: T).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat
344 \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H3:
345 (lt (weight_map f (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map f u0)
346 (weight_map (wadd f O) t2)) (plus (weight_map g u0) (weight_map (wadd g O)
347 t1)) (plus_le_lt_compat (weight_map f u0) (weight_map g u0) (weight_map (wadd
348 f O) t2) (weight_map (wadd g O) t1) (weight_le u0 f g H2) (H1 (wadd f O)
349 (wadd g O) (\lambda (m: nat).(wadd_le f g H2 O O (le_n O) m)) (eq_ind nat
350 (weight_map f (lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H3
351 (weight_map (wadd f O) (lift (S (S i)) O v)) (lift_weight_add_O O v (S i)
352 f)))))))))))))))) b)) (\lambda (_: F).(\lambda (v: T).(\lambda (t2:
353 T).(\lambda (t1: T).(\lambda (i: nat).(\lambda (_: (subst0 i v t1
354 t2)).(\lambda (H1: ((\forall (f0: ((nat \to nat))).(\forall (g: ((nat \to
355 nat))).(((\forall (m: nat).(le (f0 m) (g m)))) \to ((lt (weight_map f0 (lift
356 (S i) O v)) (g i)) \to (lt (weight_map f0 t2) (weight_map g
357 t1)))))))).(\lambda (u0: T).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat
358 \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f0 m) (g m))))).(\lambda
359 (H3: (lt (weight_map f0 (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map
360 f0 u0) (weight_map f0 t2)) (plus (weight_map g u0) (weight_map g t1))
361 (plus_le_lt_compat (weight_map f0 u0) (weight_map g u0) (weight_map f0 t2)
362 (weight_map g t1) (weight_le u0 f0 g H2) (H1 f0 g H2 H3))))))))))))))) k))
363 (\lambda (v: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (i: nat).(\lambda
364 (_: (subst0 i v u1 u2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall
365 (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt
366 (weight_map f (lift (S i) O v)) (g i)) \to (lt (weight_map f u2) (weight_map
367 g u1)))))))).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (t1:
368 T).(\forall (t2: T).((subst0 (s k0 i) v t1 t2) \to (((\forall (f: ((nat \to
369 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
370 \to ((lt (weight_map f (lift (S (s k0 i)) O v)) (g (s k0 i))) \to (lt
371 (weight_map f t2) (weight_map g t1))))))) \to (\forall (f: ((nat \to
372 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
373 \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (lt (weight_map f (THead
374 k0 u2 t2)) (weight_map g (THead k0 u1 t1)))))))))))) (\lambda (b: B).(B_ind
375 (\lambda (b0: B).(\forall (t1: T).(\forall (t2: T).((subst0 (s (Bind b0) i) v
376 t1 t2) \to (((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
377 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
378 (s (Bind b0) i)) O v)) (g (s (Bind b0) i))) \to (lt (weight_map f t2)
379 (weight_map g t1))))))) \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat
380 \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f
381 (lift (S i) O v)) (g i)) \to (lt (weight_map f (THead (Bind b0) u2 t2))
382 (weight_map g (THead (Bind b0) u1 t1)))))))))))) (\lambda (t1: T).(\lambda
383 (t2: T).(\lambda (H2: (subst0 (S i) v t1 t2)).(\lambda (_: ((\forall (f:
384 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
385 (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (lt
386 (weight_map f t2) (weight_map g t1)))))))).(\lambda (f: ((nat \to
387 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H4: ((\forall (m: nat).(le (f
388 m) (g m))))).(\lambda (H5: (lt (weight_map f (lift (S i) O v)) (g
389 i))).(lt_n_S (plus (weight_map f u2) (weight_map (wadd f (S (weight_map f
390 u2))) t2)) (plus (weight_map g u1) (weight_map (wadd g (S (weight_map g u1)))
391 t1)) (plus_lt_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd
392 f (S (weight_map f u2))) t2) (weight_map (wadd g (S (weight_map g u1))) t1)
393 (H1 f g H4 H5) (subst0_weight_le v t1 t2 (S i) H2 (wadd f (S (weight_map f
394 u2))) (wadd g (S (weight_map g u1))) (\lambda (m: nat).(wadd_le f g H4 (S
395 (weight_map f u2)) (S (weight_map g u1)) (le_S (S (weight_map f u2))
396 (weight_map g u1) (lt_le_S (weight_map f u2) (weight_map g u1) (H1 f g H4
397 H5))) m)) (lt_le_S (weight_map (wadd f (S (weight_map f u2))) (lift (S (S i))
398 O v)) (wadd g (S (weight_map g u1)) (S i)) (eq_ind nat (weight_map f (lift (S
399 i) O v)) (\lambda (n: nat).(lt n (g i))) H5 (weight_map (wadd f (S
400 (weight_map f u2))) (lift (S (S i)) O v)) (lift_weight_add_O (S (weight_map f
401 u2)) v (S i) f)))))))))))))) (\lambda (t1: T).(\lambda (t2: T).(\lambda (_:
402 (subst0 (S i) v t1 t2)).(\lambda (H3: ((\forall (f: ((nat \to nat))).(\forall
403 (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt
404 (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (lt (weight_map f t2)
405 (weight_map g t1)))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
406 nat))).(\lambda (H4: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H5: (lt
407 (weight_map f (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map f u2)
408 (weight_map (wadd f O) t2)) (plus (weight_map g u1) (weight_map (wadd g O)
409 t1)) (plus_lt_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd f
410 O) t2) (weight_map (wadd g O) t1) (H1 f g H4 H5) (H3 (wadd f O) (wadd g O)
411 (\lambda (m: nat).(le_S_n (wadd f O m) (wadd g O m) (le_n_S (wadd f O m)
412 (wadd g O m) (wadd_le f g H4 O O (le_n O) m)))) (lt_le_S (weight_map (wadd f
413 O) (lift (S (S i)) O v)) (wadd g O (S i)) (eq_ind nat (weight_map f (lift (S
414 i) O v)) (\lambda (n: nat).(lt n (g i))) H5 (weight_map (wadd f O) (lift (S
415 (S i)) O v)) (lift_weight_add_O O v (S i) f)))))))))))))) (\lambda (t1:
416 T).(\lambda (t2: T).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H3:
417 ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
418 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S
419 i))) \to (lt (weight_map f t2) (weight_map g t1)))))))).(\lambda (f: ((nat
420 \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H4: ((\forall (m: nat).(le
421 (f m) (g m))))).(\lambda (H5: (lt (weight_map f (lift (S i) O v)) (g
422 i))).(lt_n_S (plus (weight_map f u2) (weight_map (wadd f O) t2)) (plus
423 (weight_map g u1) (weight_map (wadd g O) t1)) (plus_lt_compat (weight_map f
424 u2) (weight_map g u1) (weight_map (wadd f O) t2) (weight_map (wadd g O) t1)
425 (H1 f g H4 H5) (H3 (wadd f O) (wadd g O) (\lambda (m: nat).(le_S_n (wadd f O
426 m) (wadd g O m) (le_n_S (wadd f O m) (wadd g O m) (wadd_le f g H4 O O (le_n
427 O) m)))) (lt_le_S (weight_map (wadd f O) (lift (S (S i)) O v)) (wadd g O (S
428 i)) (eq_ind nat (weight_map f (lift (S i) O v)) (\lambda (n: nat).(lt n (g
429 i))) H5 (weight_map (wadd f O) (lift (S (S i)) O v)) (lift_weight_add_O O v
430 (S i) f)))))))))))))) b)) (\lambda (_: F).(\lambda (t1: T).(\lambda (t2:
431 T).(\lambda (_: (subst0 i v t1 t2)).(\lambda (H3: ((\forall (f0: ((nat \to
432 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f0 m) (g m))))
433 \to ((lt (weight_map f0 (lift (S i) O v)) (g i)) \to (lt (weight_map f0 t2)
434 (weight_map g t1)))))))).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat
435 \to nat))).(\lambda (H4: ((\forall (m: nat).(le (f0 m) (g m))))).(\lambda
436 (H5: (lt (weight_map f0 (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map
437 f0 u2) (weight_map f0 t2)) (plus (weight_map g u1) (weight_map g t1))
438 (plus_lt_compat (weight_map f0 u2) (weight_map g u1) (weight_map f0 t2)
439 (weight_map g t1) (H1 f0 g H4 H5) (H3 f0 g H4 H5)))))))))))) k)))))))) d u t
442 theorem subst0_tlt_head:
443 \forall (u: T).(\forall (t: T).(\forall (z: T).((subst0 O u t z) \to (tlt
444 (THead (Bind Abbr) u z) (THead (Bind Abbr) u t)))))
446 \lambda (u: T).(\lambda (t: T).(\lambda (z: T).(\lambda (H: (subst0 O u t
447 z)).(lt_n_S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
448 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) z)) (plus
449 (weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S
450 (weight_map (\lambda (_: nat).O) u))) t)) (plus_le_lt_compat (weight_map
451 (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
452 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) z) (weight_map
453 (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t) (le_n
454 (weight_map (\lambda (_: nat).O) u)) (subst0_weight_lt u t z O H (wadd
455 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) (wadd (\lambda
456 (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) (\lambda (m: nat).(le_n
457 (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u)) m)))
458 (eq_ind nat (weight_map (\lambda (_: nat).O) (lift O O u)) (\lambda (n:
459 nat).(lt n (S (weight_map (\lambda (_: nat).O) u)))) (eq_ind_r T u (\lambda
460 (t0: T).(lt (weight_map (\lambda (_: nat).O) t0) (S (weight_map (\lambda (_:
461 nat).O) u)))) (le_n (S (weight_map (\lambda (_: nat).O) u))) (lift O O u)
462 (lift_r u O)) (weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda
463 (_: nat).O) u))) (lift (S O) O u)) (lift_weight_add_O (S (weight_map (\lambda
464 (_: nat).O) u)) u O (\lambda (_: nat).O))))))))).
467 \forall (u: T).(\forall (t: T).(\forall (z: T).((subst0 O u t z) \to (tlt z
468 (THead (Bind Abbr) u t)))))
470 \lambda (u: T).(\lambda (t: T).(\lambda (z: T).(\lambda (H: (subst0 O u t
471 z)).(tlt_trans (THead (Bind Abbr) u z) z (THead (Bind Abbr) u t) (tlt_head_dx
472 (Bind Abbr) u z) (subst0_tlt_head u t z H))))).