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