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 "LambdaDelta-1/subst0/defs.ma".
19 include "LambdaDelta-1/lift/props.ma".
21 include "LambdaDelta-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 (plus_le_compat (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)) (plus_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd f
65 O) t0) (weight_map (wadd g O) t0) (H1 f g H2 H3) (weight_le t0 (wadd f O)
66 (wadd g O) (\lambda (n: nat).(wadd_le f g H2 O O (le_n O) n))))))))) (\lambda
67 (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall
68 (m: nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O
69 v)) (g 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)) (plus_le_compat (weight_map f
71 u2) (weight_map g u1) (weight_map (wadd f O) t0) (weight_map (wadd g O) t0)
72 (H1 f g H2 H3) (weight_le t0 (wadd f O) (wadd g O) (\lambda (n: nat).(wadd_le
73 f g 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)) (plus_le_compat (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)) (plus_le_compat (weight_map f u0) (weight_map g u0) (weight_map (wadd f
106 (S (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)) (plus_le_compat (weight_map f
122 u0) (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)) (plus_le_compat (weight_map f u0) (weight_map g u0) (weight_map (wadd f
136 O) t2) (weight_map (wadd g O) t1) (weight_le u0 f g H2) (H1 (wadd f O) (wadd
137 g O) (\lambda (m: nat).(wadd_le f g H2 O O (le_n O) m)) (eq_ind nat
138 (weight_map f (lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H3
139 (weight_map (wadd f O) (lift (S (S i)) O v)) (lift_weight_add_O O v (S i)
140 f)))))))))))))))) b)) (\lambda (_: F).(\lambda (v: T).(\lambda (t2:
141 T).(\lambda (t1: T).(\lambda (i: nat).(\lambda (_: (subst0 i v t1
142 t2)).(\lambda (H1: ((\forall (f0: ((nat \to nat))).(\forall (g: ((nat \to
143 nat))).(((\forall (m: nat).(le (f0 m) (g m)))) \to ((lt (weight_map f0 (lift
144 (S i) O v)) (g i)) \to (le (weight_map f0 t2) (weight_map g
145 t1)))))))).(\lambda (u0: T).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat
146 \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f0 m) (g m))))).(\lambda
147 (H3: (lt (weight_map f0 (lift (S i) O v)) (g i))).(le_n_S (plus (weight_map
148 f0 u0) (weight_map f0 t2)) (plus (weight_map g u0) (weight_map g t1))
149 (plus_le_compat (weight_map f0 u0) (weight_map g u0) (weight_map f0 t2)
150 (weight_map g t1) (weight_le u0 f0 g H2) (H1 f0 g H2 H3))))))))))))))) k))
151 (\lambda (v: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (i: nat).(\lambda
152 (_: (subst0 i v u1 u2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall
153 (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt
154 (weight_map f (lift (S i) O v)) (g i)) \to (le (weight_map f u2) (weight_map
155 g u1)))))))).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (t1:
156 T).(\forall (t2: T).((subst0 (s k0 i) v t1 t2) \to (((\forall (f: ((nat \to
157 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
158 \to ((lt (weight_map f (lift (S (s k0 i)) O v)) (g (s k0 i))) \to (le
159 (weight_map f t2) (weight_map g t1))))))) \to (\forall (f: ((nat \to
160 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
161 \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (le (weight_map f (THead
162 k0 u2 t2)) (weight_map g (THead k0 u1 t1)))))))))))) (\lambda (b: B).(B_ind
163 (\lambda (b0: B).(\forall (t1: T).(\forall (t2: T).((subst0 (s (Bind b0) i) v
164 t1 t2) \to (((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
165 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
166 (s (Bind b0) i)) O v)) (g (s (Bind b0) i))) \to (le (weight_map f t2)
167 (weight_map g t1))))))) \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat
168 \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f
169 (lift (S i) O v)) (g i)) \to (le (weight_map f (THead (Bind b0) u2 t2))
170 (weight_map g (THead (Bind b0) u1 t1)))))))))))) (\lambda (t1: T).(\lambda
171 (t2: T).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H3: ((\forall (f:
172 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
173 (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (le
174 (weight_map f t2) (weight_map g t1)))))))).(\lambda (f: ((nat \to
175 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H4: ((\forall (m: nat).(le (f
176 m) (g m))))).(\lambda (H5: (lt (weight_map f (lift (S i) O v)) (g
177 i))).(le_n_S (plus (weight_map f u2) (weight_map (wadd f (S (weight_map f
178 u2))) t2)) (plus (weight_map g u1) (weight_map (wadd g (S (weight_map g u1)))
179 t1)) (plus_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd f
180 (S (weight_map f u2))) t2) (weight_map (wadd g (S (weight_map g u1))) t1) (H1
181 f g H4 H5) (H3 (wadd f (S (weight_map f u2))) (wadd g (S (weight_map g u1)))
182 (\lambda (m: nat).(wadd_le f g H4 (S (weight_map f u2)) (S (weight_map g u1))
183 (le_n_S (weight_map f u2) (weight_map g u1) (H1 f g H4 H5)) m)) (eq_ind nat
184 (weight_map f (lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H5
185 (weight_map (wadd f (S (weight_map f u2))) (lift (S (S i)) O v))
186 (lift_weight_add_O (S (weight_map f u2)) v (S i) f))))))))))))) (\lambda (t1:
187 T).(\lambda (t2: T).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H3:
188 ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
189 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S
190 i))) \to (le (weight_map f t2) (weight_map g t1)))))))).(\lambda (f: ((nat
191 \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H4: ((\forall (m: nat).(le
192 (f m) (g m))))).(\lambda (H5: (lt (weight_map f (lift (S i) O v)) (g
193 i))).(le_n_S (plus (weight_map f u2) (weight_map (wadd f O) t2)) (plus
194 (weight_map g u1) (weight_map (wadd g O) t1)) (plus_le_compat (weight_map f
195 u2) (weight_map g u1) (weight_map (wadd f O) t2) (weight_map (wadd g O) t1)
196 (H1 f g H4 H5) (H3 (wadd f O) (wadd g O) (\lambda (m: nat).(wadd_le f g H4 O
197 O (le_n O) m)) (eq_ind nat (weight_map f (lift (S i) O v)) (\lambda (n:
198 nat).(lt n (g i))) H5 (weight_map (wadd f O) (lift (S (S i)) O v))
199 (lift_weight_add_O O v (S i) f))))))))))))) (\lambda (t1: T).(\lambda (t2:
200 T).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H3: ((\forall (f: ((nat \to
201 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
202 \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (le (weight_map f
203 t2) (weight_map g t1)))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat
204 \to nat))).(\lambda (H4: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H5:
205 (lt (weight_map f (lift (S i) O v)) (g i))).(le_n_S (plus (weight_map f u2)
206 (weight_map (wadd f O) t2)) (plus (weight_map g u1) (weight_map (wadd g O)
207 t1)) (plus_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd f
208 O) t2) (weight_map (wadd g O) t1) (H1 f g H4 H5) (H3 (wadd f O) (wadd g O)
209 (\lambda (m: nat).(wadd_le f g H4 O O (le_n O) m)) (eq_ind nat (weight_map f
210 (lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H5 (weight_map (wadd f O)
211 (lift (S (S i)) O v)) (lift_weight_add_O O v (S i) f))))))))))))) b))
212 (\lambda (_: F).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (subst0 i v t1
213 t2)).(\lambda (H3: ((\forall (f0: ((nat \to nat))).(\forall (g: ((nat \to
214 nat))).(((\forall (m: nat).(le (f0 m) (g m)))) \to ((lt (weight_map f0 (lift
215 (S i) O v)) (g i)) \to (le (weight_map f0 t2) (weight_map g
216 t1)))))))).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat \to
217 nat))).(\lambda (H4: ((\forall (m: nat).(le (f0 m) (g m))))).(\lambda (H5:
218 (lt (weight_map f0 (lift (S i) O v)) (g i))).(le_n_S (plus (weight_map f0 u2)
219 (weight_map f0 t2)) (plus (weight_map g u1) (weight_map g t1))
220 (plus_le_compat (weight_map f0 u2) (weight_map g u1) (weight_map f0 t2)
221 (weight_map g t1) (H1 f0 g H4 H5) (H3 f0 g H4 H5)))))))))))) k)))))))) d u t
224 theorem subst0_weight_lt:
225 \forall (u: T).(\forall (t: T).(\forall (z: T).(\forall (d: nat).((subst0 d
226 u t z) \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
227 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
228 d) O u)) (g d)) \to (lt (weight_map f z) (weight_map g t))))))))))
230 \lambda (u: T).(\lambda (t: T).(\lambda (z: T).(\lambda (d: nat).(\lambda
231 (H: (subst0 d u t z)).(subst0_ind (\lambda (n: nat).(\lambda (t0: T).(\lambda
232 (t1: T).(\lambda (t2: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
233 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
234 n) O t0)) (g n)) \to (lt (weight_map f t2) (weight_map g t1))))))))))
235 (\lambda (v: T).(\lambda (i: nat).(\lambda (f: ((nat \to nat))).(\lambda (g:
236 ((nat \to nat))).(\lambda (_: ((\forall (m: nat).(le (f m) (g m))))).(\lambda
237 (H1: (lt (weight_map f (lift (S i) O v)) (g i))).H1)))))) (\lambda (v:
238 T).(\lambda (u2: T).(\lambda (u1: T).(\lambda (i: nat).(\lambda (_: (subst0 i
239 v u1 u2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
240 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
241 i) O v)) (g i)) \to (lt (weight_map f u2) (weight_map g u1)))))))).(\lambda
242 (t0: T).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (f: ((nat \to
243 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
244 \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (lt (weight_map f (THead
245 k0 u2 t0)) (weight_map g (THead k0 u1 t0)))))))) (\lambda (b: B).(B_ind
246 (\lambda (b0: B).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
247 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
248 i) O v)) (g i)) \to (lt (weight_map f (THead (Bind b0) u2 t0)) (weight_map g
249 (THead (Bind b0) u1 t0)))))))) (\lambda (f: ((nat \to nat))).(\lambda (g:
250 ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f m) (g
251 m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g i))).(lt_n_S
252 (plus (weight_map f u2) (weight_map (wadd f (S (weight_map f u2))) t0)) (plus
253 (weight_map g u1) (weight_map (wadd g (S (weight_map g u1))) t0))
254 (plus_lt_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd f (S
255 (weight_map f u2))) t0) (weight_map (wadd g (S (weight_map g u1))) t0) (H1 f
256 g H2 H3) (weight_le t0 (wadd f (S (weight_map f u2))) (wadd g (S (weight_map
257 g u1))) (\lambda (n: nat).(wadd_lt f g H2 (S (weight_map f u2)) (S
258 (weight_map g u1)) (lt_n_S (weight_map f u2) (weight_map g u1) (H1 f g H2
259 H3)) n))))))))) (\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
260 nat))).(\lambda (H2: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H3: (lt
261 (weight_map f (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map f u2)
262 (weight_map (wadd f O) t0)) (plus (weight_map g u1) (weight_map (wadd g O)
263 t0)) (plus_lt_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd
264 f O) t0) (weight_map (wadd g O) t0) (H1 f g H2 H3) (weight_le t0 (wadd f O)
265 (wadd g O) (\lambda (n: nat).(le_S_n (wadd f O n) (wadd g O n) (le_n_S (wadd
266 f O n) (wadd g O n) (wadd_le f g H2 O O (le_n O) n))))))))))) (\lambda (f:
267 ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m:
268 nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g
269 i))).(lt_n_S (plus (weight_map f u2) (weight_map (wadd f O) t0)) (plus
270 (weight_map g u1) (weight_map (wadd g O) t0)) (plus_lt_le_compat (weight_map
271 f u2) (weight_map g u1) (weight_map (wadd f O) t0) (weight_map (wadd g O) t0)
272 (H1 f g H2 H3) (weight_le t0 (wadd f O) (wadd g O) (\lambda (n: nat).(le_S_n
273 (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
274 O (le_n O) n))))))))))) b)) (\lambda (_: F).(\lambda (f0: ((nat \to
275 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f0
276 m) (g m))))).(\lambda (H3: (lt (weight_map f0 (lift (S i) O v)) (g
277 i))).(lt_n_S (plus (weight_map f0 u2) (weight_map f0 t0)) (plus (weight_map g
278 u1) (weight_map g t0)) (plus_lt_le_compat (weight_map f0 u2) (weight_map g
279 u1) (weight_map f0 t0) (weight_map g t0) (H1 f0 g H2 H3) (weight_le t0 f0 g
280 H2)))))))) k))))))))) (\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (v:
281 T).(\forall (t2: T).(\forall (t1: T).(\forall (i: nat).((subst0 (s k0 i) v t1
282 t2) \to (((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
283 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
284 (s k0 i)) O v)) (g (s k0 i))) \to (lt (weight_map f t2) (weight_map g
285 t1))))))) \to (\forall (u0: T).(\forall (f: ((nat \to nat))).(\forall (g:
286 ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map
287 f (lift (S i) O v)) (g i)) \to (lt (weight_map f (THead k0 u0 t2))
288 (weight_map g (THead k0 u0 t1))))))))))))))) (\lambda (b: B).(B_ind (\lambda
289 (b0: B).(\forall (v: T).(\forall (t2: T).(\forall (t1: T).(\forall (i:
290 nat).((subst0 (s (Bind b0) i) v t1 t2) \to (((\forall (f: ((nat \to
291 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
292 \to ((lt (weight_map f (lift (S (s (Bind b0) i)) O v)) (g (s (Bind b0) i)))
293 \to (lt (weight_map f t2) (weight_map g t1))))))) \to (\forall (u0:
294 T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
295 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to
296 (lt (weight_map f (THead (Bind b0) u0 t2)) (weight_map g (THead (Bind b0) u0
297 t1))))))))))))))) (\lambda (v: T).(\lambda (t2: T).(\lambda (t1: T).(\lambda
298 (i: nat).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H1: ((\forall (f:
299 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
300 (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (lt
301 (weight_map f t2) (weight_map g t1)))))))).(\lambda (u0: T).(\lambda (f:
302 ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m:
303 nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g
304 i))).(lt_n_S (plus (weight_map f u0) (weight_map (wadd f (S (weight_map f
305 u0))) t2)) (plus (weight_map g u0) (weight_map (wadd g (S (weight_map g u0)))
306 t1)) (plus_le_lt_compat (weight_map f u0) (weight_map g u0) (weight_map (wadd
307 f (S (weight_map f u0))) t2) (weight_map (wadd g (S (weight_map g u0))) t1)
308 (weight_le u0 f g H2) (H1 (wadd f (S (weight_map f u0))) (wadd g (S
309 (weight_map g u0))) (\lambda (m: nat).(wadd_le f g H2 (S (weight_map f u0))
310 (S (weight_map g u0)) (le_n_S (weight_map f u0) (weight_map g u0) (weight_le
311 u0 f g H2)) m)) (eq_ind nat (weight_map f (lift (S i) O v)) (\lambda (n:
312 nat).(lt n (g i))) H3 (weight_map (wadd f (S (weight_map f u0))) (lift (S (S
313 i)) O v)) (lift_weight_add_O (S (weight_map f u0)) v (S i) f))))))))))))))))
314 (\lambda (v: T).(\lambda (t2: T).(\lambda (t1: T).(\lambda (i: nat).(\lambda
315 (_: (subst0 (S i) v t1 t2)).(\lambda (H1: ((\forall (f: ((nat \to
316 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
317 \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (lt (weight_map f
318 t2) (weight_map g t1)))))))).(\lambda (u0: T).(\lambda (f: ((nat \to
319 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f
320 m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g
321 i))).(lt_n_S (plus (weight_map f u0) (weight_map (wadd f O) t2)) (plus
322 (weight_map g u0) (weight_map (wadd g O) t1)) (plus_le_lt_compat (weight_map
323 f u0) (weight_map g u0) (weight_map (wadd f O) t2) (weight_map (wadd g O) t1)
324 (weight_le u0 f g H2) (H1 (wadd f O) (wadd g O) (\lambda (m: nat).(wadd_le f
325 g H2 O O (le_n O) m)) (eq_ind nat (weight_map f (lift (S i) O v)) (\lambda
326 (n: nat).(lt n (g i))) H3 (weight_map (wadd f O) (lift (S (S i)) O v))
327 (lift_weight_add_O O v (S i) f)))))))))))))))) (\lambda (v: T).(\lambda (t2:
328 T).(\lambda (t1: T).(\lambda (i: nat).(\lambda (_: (subst0 (S i) v t1
329 t2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
330 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
331 (S i)) O v)) (g (S i))) \to (lt (weight_map f t2) (weight_map g
332 t1)))))))).(\lambda (u0: T).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat
333 \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H3:
334 (lt (weight_map f (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map f u0)
335 (weight_map (wadd f O) t2)) (plus (weight_map g u0) (weight_map (wadd g O)
336 t1)) (plus_le_lt_compat (weight_map f u0) (weight_map g u0) (weight_map (wadd
337 f O) t2) (weight_map (wadd g O) t1) (weight_le u0 f g H2) (H1 (wadd f O)
338 (wadd g O) (\lambda (m: nat).(wadd_le f g H2 O O (le_n O) m)) (eq_ind nat
339 (weight_map f (lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H3
340 (weight_map (wadd f O) (lift (S (S i)) O v)) (lift_weight_add_O O v (S i)
341 f)))))))))))))))) b)) (\lambda (_: F).(\lambda (v: T).(\lambda (t2:
342 T).(\lambda (t1: T).(\lambda (i: nat).(\lambda (_: (subst0 i v t1
343 t2)).(\lambda (H1: ((\forall (f0: ((nat \to nat))).(\forall (g: ((nat \to
344 nat))).(((\forall (m: nat).(le (f0 m) (g m)))) \to ((lt (weight_map f0 (lift
345 (S i) O v)) (g i)) \to (lt (weight_map f0 t2) (weight_map g
346 t1)))))))).(\lambda (u0: T).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat
347 \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f0 m) (g m))))).(\lambda
348 (H3: (lt (weight_map f0 (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map
349 f0 u0) (weight_map f0 t2)) (plus (weight_map g u0) (weight_map g t1))
350 (plus_le_lt_compat (weight_map f0 u0) (weight_map g u0) (weight_map f0 t2)
351 (weight_map g t1) (weight_le u0 f0 g H2) (H1 f0 g H2 H3))))))))))))))) k))
352 (\lambda (v: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (i: nat).(\lambda
353 (_: (subst0 i v u1 u2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall
354 (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt
355 (weight_map f (lift (S i) O v)) (g i)) \to (lt (weight_map f u2) (weight_map
356 g u1)))))))).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (t1:
357 T).(\forall (t2: T).((subst0 (s k0 i) v t1 t2) \to (((\forall (f: ((nat \to
358 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
359 \to ((lt (weight_map f (lift (S (s k0 i)) O v)) (g (s k0 i))) \to (lt
360 (weight_map f t2) (weight_map g t1))))))) \to (\forall (f: ((nat \to
361 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
362 \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (lt (weight_map f (THead
363 k0 u2 t2)) (weight_map g (THead k0 u1 t1)))))))))))) (\lambda (b: B).(B_ind
364 (\lambda (b0: B).(\forall (t1: T).(\forall (t2: T).((subst0 (s (Bind b0) i) v
365 t1 t2) \to (((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
366 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
367 (s (Bind b0) i)) O v)) (g (s (Bind b0) i))) \to (lt (weight_map f t2)
368 (weight_map g t1))))))) \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat
369 \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f
370 (lift (S i) O v)) (g i)) \to (lt (weight_map f (THead (Bind b0) u2 t2))
371 (weight_map g (THead (Bind b0) u1 t1)))))))))))) (\lambda (t1: T).(\lambda
372 (t2: T).(\lambda (H2: (subst0 (S i) v t1 t2)).(\lambda (_: ((\forall (f:
373 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
374 (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (lt
375 (weight_map f t2) (weight_map g t1)))))))).(\lambda (f: ((nat \to
376 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H4: ((\forall (m: nat).(le (f
377 m) (g m))))).(\lambda (H5: (lt (weight_map f (lift (S i) O v)) (g
378 i))).(lt_n_S (plus (weight_map f u2) (weight_map (wadd f (S (weight_map f
379 u2))) t2)) (plus (weight_map g u1) (weight_map (wadd g (S (weight_map g u1)))
380 t1)) (plus_lt_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd
381 f (S (weight_map f u2))) t2) (weight_map (wadd g (S (weight_map g u1))) t1)
382 (H1 f g H4 H5) (subst0_weight_le v t1 t2 (S i) H2 (wadd f (S (weight_map f
383 u2))) (wadd g (S (weight_map g u1))) (\lambda (m: nat).(wadd_lt f g H4 (S
384 (weight_map f u2)) (S (weight_map g u1)) (lt_n_S (weight_map f u2)
385 (weight_map g u1) (H1 f g H4 H5)) m)) (eq_ind nat (weight_map f (lift (S i) O
386 v)) (\lambda (n: nat).(lt n (g i))) H5 (weight_map (wadd f (S (weight_map f
387 u2))) (lift (S (S i)) O v)) (lift_weight_add_O (S (weight_map f u2)) v (S i)
388 f))))))))))))) (\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (subst0 (S i) v
389 t1 t2)).(\lambda (H3: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
390 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
391 (S i)) O v)) (g (S i))) \to (lt (weight_map f t2) (weight_map g
392 t1)))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
393 nat))).(\lambda (H4: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H5: (lt
394 (weight_map f (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map f u2)
395 (weight_map (wadd f O) t2)) (plus (weight_map g u1) (weight_map (wadd g O)
396 t1)) (plus_lt_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd f
397 O) t2) (weight_map (wadd g O) t1) (H1 f g H4 H5) (H3 (wadd f O) (wadd g O)
398 (\lambda (m: nat).(le_S_n (wadd f O m) (wadd g O m) (le_n_S (wadd f O m)
399 (wadd g O m) (wadd_le f g H4 O O (le_n O) m)))) (eq_ind nat (weight_map f
400 (lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H5 (weight_map (wadd f O)
401 (lift (S (S i)) O v)) (lift_weight_add_O O v (S i) f))))))))))))) (\lambda
402 (t1: T).(\lambda (t2: T).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H3:
403 ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
404 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S
405 i))) \to (lt (weight_map f t2) (weight_map g t1)))))))).(\lambda (f: ((nat
406 \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H4: ((\forall (m: nat).(le
407 (f m) (g m))))).(\lambda (H5: (lt (weight_map f (lift (S i) O v)) (g
408 i))).(lt_n_S (plus (weight_map f u2) (weight_map (wadd f O) t2)) (plus
409 (weight_map g u1) (weight_map (wadd g O) t1)) (plus_lt_compat (weight_map f
410 u2) (weight_map g u1) (weight_map (wadd f O) t2) (weight_map (wadd g O) t1)
411 (H1 f g H4 H5) (H3 (wadd f O) (wadd g O) (\lambda (m: nat).(le_S_n (wadd f O
412 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
413 O) m)))) (eq_ind nat (weight_map f (lift (S i) O v)) (\lambda (n: nat).(lt n
414 (g i))) H5 (weight_map (wadd f O) (lift (S (S i)) O v)) (lift_weight_add_O O
415 v (S i) f))))))))))))) b)) (\lambda (_: F).(\lambda (t1: T).(\lambda (t2:
416 T).(\lambda (_: (subst0 i v t1 t2)).(\lambda (H3: ((\forall (f0: ((nat \to
417 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f0 m) (g m))))
418 \to ((lt (weight_map f0 (lift (S i) O v)) (g i)) \to (lt (weight_map f0 t2)
419 (weight_map g t1)))))))).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat
420 \to nat))).(\lambda (H4: ((\forall (m: nat).(le (f0 m) (g m))))).(\lambda
421 (H5: (lt (weight_map f0 (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map
422 f0 u2) (weight_map f0 t2)) (plus (weight_map g u1) (weight_map g t1))
423 (plus_lt_compat (weight_map f0 u2) (weight_map g u1) (weight_map f0 t2)
424 (weight_map g t1) (H1 f0 g H4 H5) (H3 f0 g H4 H5)))))))))))) k)))))))) d u t
427 theorem subst0_tlt_head:
428 \forall (u: T).(\forall (t: T).(\forall (z: T).((subst0 O u t z) \to (tlt
429 (THead (Bind Abbr) u z) (THead (Bind Abbr) u t)))))
431 \lambda (u: T).(\lambda (t: T).(\lambda (z: T).(\lambda (H: (subst0 O u t
432 z)).(lt_n_S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
433 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) z)) (plus
434 (weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S
435 (weight_map (\lambda (_: nat).O) u))) t)) (plus_le_lt_compat (weight_map
436 (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
437 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) z) (weight_map
438 (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t) (le_n
439 (weight_map (\lambda (_: nat).O) u)) (subst0_weight_lt u t z O H (wadd
440 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) (wadd (\lambda
441 (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) (\lambda (m: nat).(le_n
442 (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u)) m)))
443 (eq_ind nat (weight_map (\lambda (_: nat).O) (lift O O u)) (\lambda (n:
444 nat).(lt n (S (weight_map (\lambda (_: nat).O) u)))) (eq_ind_r T u (\lambda
445 (t0: T).(lt (weight_map (\lambda (_: nat).O) t0) (S (weight_map (\lambda (_:
446 nat).O) u)))) (le_n (S (weight_map (\lambda (_: nat).O) u))) (lift O O u)
447 (lift_r u O)) (weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda
448 (_: nat).O) u))) (lift (S O) O u)) (lift_weight_add_O (S (weight_map (\lambda
449 (_: nat).O) u)) u O (\lambda (_: nat).O))))))))).
452 \forall (u: T).(\forall (t: T).(\forall (z: T).((subst0 O u t z) \to (tlt z
453 (THead (Bind Abbr) u t)))))
455 \lambda (u: T).(\lambda (t: T).(\lambda (z: T).(\lambda (H: (subst0 O u t
456 z)).(tlt_trans (THead (Bind Abbr) u z) z (THead (Bind Abbr) u t) (tlt_head_dx
457 (Bind Abbr) u z) (subst0_tlt_head u t z H))))).