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_1A/subst0/fwd.ma".
19 include "basic_1A/lift/tlt.ma".
21 lemma subst0_weight_le:
22 \forall (u: T).(\forall (t: T).(\forall (z: T).(\forall (d: nat).((subst0 d
23 u t z) \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
24 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
25 d) O u)) (g d)) \to (le (weight_map f z) (weight_map g t))))))))))
27 \lambda (u: T).(\lambda (t: T).(\lambda (z: T).(\lambda (d: nat).(\lambda
28 (H: (subst0 d u t z)).(subst0_ind (\lambda (n: nat).(\lambda (t0: T).(\lambda
29 (t1: T).(\lambda (t2: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
30 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
31 n) O t0)) (g n)) \to (le (weight_map f t2) (weight_map g t1))))))))))
32 (\lambda (v: T).(\lambda (i: nat).(\lambda (f: ((nat \to nat))).(\lambda (g:
33 ((nat \to nat))).(\lambda (_: ((\forall (m: nat).(le (f m) (g m))))).(\lambda
34 (H1: (lt (weight_map f (lift (S i) O v)) (g i))).(le_S_n (weight_map f (lift
35 (S i) O v)) (weight_map g (TLRef i)) (le_S_n (S (weight_map f (lift (S i) O
36 v))) (S (weight_map g (TLRef i))) (le_S (S (S (weight_map f (lift (S i) O
37 v)))) (S (weight_map g (TLRef i))) (le_n_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_O_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_O_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_O_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_O_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 (le_plus_plus (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)) (le_plus_plus (weight_map f u2) (weight_map g u1) (weight_map (wadd f (S
180 (weight_map f u2))) t2) (weight_map (wadd g (S (weight_map g u1))) t1) (H1 f
181 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)) (le_plus_plus (weight_map f u2)
195 (weight_map g u1) (weight_map (wadd f O) t2) (weight_map (wadd g O) t1) (H1 f
196 g H4 H5) (H3 (wadd f O) (wadd g O) (\lambda (m: nat).(wadd_le f g H4 O O
197 (le_O_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)) (le_plus_plus (weight_map f u2) (weight_map g u1) (weight_map (wadd f O)
208 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_O_n O) m)) (eq_ind nat (weight_map
210 f (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)) (le_plus_plus
220 (weight_map f0 u2) (weight_map g u1) (weight_map f0 t2) (weight_map g t1) (H1
221 f0 g H4 H5) (H3 f0 g H4 H5)))))))))))) k)))))))) d u t z H))))).
223 lemma subst0_weight_lt:
224 \forall (u: T).(\forall (t: T).(\forall (z: T).(\forall (d: nat).((subst0 d
225 u t z) \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
226 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
227 d) O u)) (g d)) \to (lt (weight_map f z) (weight_map g t))))))))))
229 \lambda (u: T).(\lambda (t: T).(\lambda (z: T).(\lambda (d: nat).(\lambda
230 (H: (subst0 d u t z)).(subst0_ind (\lambda (n: nat).(\lambda (t0: T).(\lambda
231 (t1: T).(\lambda (t2: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
232 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
233 n) O t0)) (g n)) \to (lt (weight_map f t2) (weight_map g t1))))))))))
234 (\lambda (v: T).(\lambda (i: nat).(\lambda (f: ((nat \to nat))).(\lambda (g:
235 ((nat \to nat))).(\lambda (_: ((\forall (m: nat).(le (f m) (g m))))).(\lambda
236 (H1: (lt (weight_map f (lift (S i) O v)) (g i))).H1)))))) (\lambda (v:
237 T).(\lambda (u2: T).(\lambda (u1: T).(\lambda (i: nat).(\lambda (_: (subst0 i
238 v u1 u2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
239 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
240 i) O v)) (g i)) \to (lt (weight_map f u2) (weight_map g u1)))))))).(\lambda
241 (t0: T).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (f: ((nat \to
242 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
243 \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (lt (weight_map f (THead
244 k0 u2 t0)) (weight_map g (THead k0 u1 t0)))))))) (\lambda (b: B).(B_ind
245 (\lambda (b0: B).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
246 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
247 i) O v)) (g i)) \to (lt (weight_map f (THead (Bind b0) u2 t0)) (weight_map g
248 (THead (Bind b0) u1 t0)))))))) (\lambda (f: ((nat \to nat))).(\lambda (g:
249 ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f m) (g
250 m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g i))).(lt_n_S
251 (plus (weight_map f u2) (weight_map (wadd f (S (weight_map f u2))) t0)) (plus
252 (weight_map g u1) (weight_map (wadd g (S (weight_map g u1))) t0))
253 (lt_le_plus_plus (weight_map f u2) (weight_map g u1) (weight_map (wadd f (S
254 (weight_map f u2))) t0) (weight_map (wadd g (S (weight_map g u1))) t0) (H1 f
255 g H2 H3) (weight_le t0 (wadd f (S (weight_map f u2))) (wadd g (S (weight_map
256 g u1))) (\lambda (n: nat).(wadd_lt f g H2 (S (weight_map f u2)) (S
257 (weight_map g u1)) (lt_n_S (weight_map f u2) (weight_map g u1) (H1 f g H2
258 H3)) n))))))))) (\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
259 nat))).(\lambda (H2: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H3: (lt
260 (weight_map f (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map f u2)
261 (weight_map (wadd f O) t0)) (plus (weight_map g u1) (weight_map (wadd g O)
262 t0)) (lt_le_plus_plus (weight_map f u2) (weight_map g u1) (weight_map (wadd f
263 O) t0) (weight_map (wadd g O) t0) (H1 f g H2 H3) (weight_le t0 (wadd f O)
264 (wadd g O) (\lambda (n: nat).(le_S_n (wadd f O n) (wadd g O n) (le_n_S (wadd
265 f O n) (wadd g O n) (wadd_le f g H2 O O (le_O_n O) n))))))))))) (\lambda (f:
266 ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m:
267 nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g
268 i))).(lt_n_S (plus (weight_map f u2) (weight_map (wadd f O) t0)) (plus
269 (weight_map g u1) (weight_map (wadd g O) t0)) (lt_le_plus_plus (weight_map f
270 u2) (weight_map g u1) (weight_map (wadd f O) t0) (weight_map (wadd g O) t0)
271 (H1 f g H2 H3) (weight_le t0 (wadd f O) (wadd g O) (\lambda (n: nat).(le_S_n
272 (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
273 O (le_O_n O) n))))))))))) b)) (\lambda (_: F).(\lambda (f0: ((nat \to
274 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f0
275 m) (g m))))).(\lambda (H3: (lt (weight_map f0 (lift (S i) O v)) (g
276 i))).(lt_n_S (plus (weight_map f0 u2) (weight_map f0 t0)) (plus (weight_map g
277 u1) (weight_map g t0)) (lt_le_plus_plus (weight_map f0 u2) (weight_map g u1)
278 (weight_map f0 t0) (weight_map g t0) (H1 f0 g H2 H3) (weight_le t0 f0 g
279 H2)))))))) k))))))))) (\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (v:
280 T).(\forall (t2: T).(\forall (t1: T).(\forall (i: nat).((subst0 (s k0 i) v t1
281 t2) \to (((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
282 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
283 (s k0 i)) O v)) (g (s k0 i))) \to (lt (weight_map f t2) (weight_map g
284 t1))))))) \to (\forall (u0: T).(\forall (f: ((nat \to nat))).(\forall (g:
285 ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map
286 f (lift (S i) O v)) (g i)) \to (lt (weight_map f (THead k0 u0 t2))
287 (weight_map g (THead k0 u0 t1))))))))))))))) (\lambda (b: B).(B_ind (\lambda
288 (b0: B).(\forall (v: T).(\forall (t2: T).(\forall (t1: T).(\forall (i:
289 nat).((subst0 (s (Bind b0) i) v t1 t2) \to (((\forall (f: ((nat \to
290 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
291 \to ((lt (weight_map f (lift (S (s (Bind b0) i)) O v)) (g (s (Bind b0) i)))
292 \to (lt (weight_map f t2) (weight_map g t1))))))) \to (\forall (u0:
293 T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
294 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to
295 (lt (weight_map f (THead (Bind b0) u0 t2)) (weight_map g (THead (Bind b0) u0
296 t1))))))))))))))) (\lambda (v: T).(\lambda (t2: T).(\lambda (t1: T).(\lambda
297 (i: nat).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H1: ((\forall (f:
298 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
299 (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (lt
300 (weight_map f t2) (weight_map g t1)))))))).(\lambda (u0: T).(\lambda (f:
301 ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m:
302 nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g
303 i))).(lt_n_S (plus (weight_map f u0) (weight_map (wadd f (S (weight_map f
304 u0))) t2)) (plus (weight_map g u0) (weight_map (wadd g (S (weight_map g u0)))
305 t1)) (le_lt_plus_plus (weight_map f u0) (weight_map g u0) (weight_map (wadd f
306 (S (weight_map f u0))) t2) (weight_map (wadd g (S (weight_map g u0))) t1)
307 (weight_le u0 f g H2) (H1 (wadd f (S (weight_map f u0))) (wadd g (S
308 (weight_map g u0))) (\lambda (m: nat).(wadd_le f g H2 (S (weight_map f u0))
309 (S (weight_map g u0)) (le_n_S (weight_map f u0) (weight_map g u0) (weight_le
310 u0 f g H2)) m)) (eq_ind nat (weight_map f (lift (S i) O v)) (\lambda (n:
311 nat).(lt n (g i))) H3 (weight_map (wadd f (S (weight_map f u0))) (lift (S (S
312 i)) O v)) (lift_weight_add_O (S (weight_map f u0)) v (S i) f))))))))))))))))
313 (\lambda (v: T).(\lambda (t2: T).(\lambda (t1: T).(\lambda (i: nat).(\lambda
314 (_: (subst0 (S i) v t1 t2)).(\lambda (H1: ((\forall (f: ((nat \to
315 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
316 \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (lt (weight_map f
317 t2) (weight_map g t1)))))))).(\lambda (u0: T).(\lambda (f: ((nat \to
318 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f
319 m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g
320 i))).(lt_n_S (plus (weight_map f u0) (weight_map (wadd f O) t2)) (plus
321 (weight_map g u0) (weight_map (wadd g O) t1)) (le_lt_plus_plus (weight_map f
322 u0) (weight_map g u0) (weight_map (wadd f O) t2) (weight_map (wadd g O) t1)
323 (weight_le u0 f g H2) (H1 (wadd f O) (wadd g O) (\lambda (m: nat).(wadd_le f
324 g H2 O O (le_O_n O) m)) (eq_ind nat (weight_map f (lift (S i) O v)) (\lambda
325 (n: nat).(lt n (g i))) H3 (weight_map (wadd f O) (lift (S (S i)) O v))
326 (lift_weight_add_O O v (S i) f)))))))))))))))) (\lambda (v: T).(\lambda (t2:
327 T).(\lambda (t1: T).(\lambda (i: nat).(\lambda (_: (subst0 (S i) v t1
328 t2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
329 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
330 (S i)) O v)) (g (S i))) \to (lt (weight_map f t2) (weight_map g
331 t1)))))))).(\lambda (u0: T).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat
332 \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H3:
333 (lt (weight_map f (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map f u0)
334 (weight_map (wadd f O) t2)) (plus (weight_map g u0) (weight_map (wadd g O)
335 t1)) (le_lt_plus_plus (weight_map f u0) (weight_map g u0) (weight_map (wadd f
336 O) t2) (weight_map (wadd g O) t1) (weight_le u0 f g H2) (H1 (wadd f O) (wadd
337 g O) (\lambda (m: nat).(wadd_le f g H2 O O (le_O_n O) m)) (eq_ind nat
338 (weight_map f (lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H3
339 (weight_map (wadd f O) (lift (S (S i)) O v)) (lift_weight_add_O O v (S i)
340 f)))))))))))))))) b)) (\lambda (_: F).(\lambda (v: T).(\lambda (t2:
341 T).(\lambda (t1: T).(\lambda (i: nat).(\lambda (_: (subst0 i v t1
342 t2)).(\lambda (H1: ((\forall (f0: ((nat \to nat))).(\forall (g: ((nat \to
343 nat))).(((\forall (m: nat).(le (f0 m) (g m)))) \to ((lt (weight_map f0 (lift
344 (S i) O v)) (g i)) \to (lt (weight_map f0 t2) (weight_map g
345 t1)))))))).(\lambda (u0: T).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat
346 \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f0 m) (g m))))).(\lambda
347 (H3: (lt (weight_map f0 (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map
348 f0 u0) (weight_map f0 t2)) (plus (weight_map g u0) (weight_map g t1))
349 (le_lt_plus_plus (weight_map f0 u0) (weight_map g u0) (weight_map f0 t2)
350 (weight_map g t1) (weight_le u0 f0 g H2) (H1 f0 g H2 H3))))))))))))))) k))
351 (\lambda (v: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (i: nat).(\lambda
352 (_: (subst0 i v u1 u2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall
353 (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt
354 (weight_map f (lift (S i) O v)) (g i)) \to (lt (weight_map f u2) (weight_map
355 g u1)))))))).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (t1:
356 T).(\forall (t2: T).((subst0 (s k0 i) v t1 t2) \to (((\forall (f: ((nat \to
357 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
358 \to ((lt (weight_map f (lift (S (s k0 i)) O v)) (g (s k0 i))) \to (lt
359 (weight_map f t2) (weight_map g t1))))))) \to (\forall (f: ((nat \to
360 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
361 \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (lt (weight_map f (THead
362 k0 u2 t2)) (weight_map g (THead k0 u1 t1)))))))))))) (\lambda (b: B).(B_ind
363 (\lambda (b0: B).(\forall (t1: T).(\forall (t2: T).((subst0 (s (Bind b0) i) v
364 t1 t2) \to (((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
365 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
366 (s (Bind b0) i)) O v)) (g (s (Bind b0) i))) \to (lt (weight_map f t2)
367 (weight_map g t1))))))) \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat
368 \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f
369 (lift (S i) O v)) (g i)) \to (lt (weight_map f (THead (Bind b0) u2 t2))
370 (weight_map g (THead (Bind b0) u1 t1)))))))))))) (\lambda (t1: T).(\lambda
371 (t2: T).(\lambda (H2: (subst0 (S i) v t1 t2)).(\lambda (_: ((\forall (f:
372 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
373 (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (lt
374 (weight_map f t2) (weight_map g t1)))))))).(\lambda (f: ((nat \to
375 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H4: ((\forall (m: nat).(le (f
376 m) (g m))))).(\lambda (H5: (lt (weight_map f (lift (S i) O v)) (g
377 i))).(lt_n_S (plus (weight_map f u2) (weight_map (wadd f (S (weight_map f
378 u2))) t2)) (plus (weight_map g u1) (weight_map (wadd g (S (weight_map g u1)))
379 t1)) (lt_le_plus_plus (weight_map f u2) (weight_map g u1) (weight_map (wadd f
380 (S (weight_map f u2))) t2) (weight_map (wadd g (S (weight_map g u1))) t1) (H1
381 f g H4 H5) (subst0_weight_le v t1 t2 (S i) H2 (wadd f (S (weight_map f u2)))
382 (wadd g (S (weight_map g u1))) (\lambda (m: nat).(wadd_lt f g H4 (S
383 (weight_map f u2)) (S (weight_map g u1)) (lt_n_S (weight_map f u2)
384 (weight_map g u1) (H1 f g H4 H5)) m)) (eq_ind nat (weight_map f (lift (S i) O
385 v)) (\lambda (n: nat).(lt n (g i))) H5 (weight_map (wadd f (S (weight_map f
386 u2))) (lift (S (S i)) O v)) (lift_weight_add_O (S (weight_map f u2)) v (S i)
387 f))))))))))))) (\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (subst0 (S i) v
388 t1 t2)).(\lambda (H3: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
389 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
390 (S i)) O v)) (g (S i))) \to (lt (weight_map f t2) (weight_map g
391 t1)))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
392 nat))).(\lambda (H4: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H5: (lt
393 (weight_map f (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map f u2)
394 (weight_map (wadd f O) t2)) (plus (weight_map g u1) (weight_map (wadd g O)
395 t1)) (lt_plus_plus (weight_map f u2) (weight_map g u1) (weight_map (wadd f O)
396 t2) (weight_map (wadd g O) t1) (H1 f g H4 H5) (H3 (wadd f O) (wadd g O)
397 (\lambda (m: nat).(le_S_n (wadd f O m) (wadd g O m) (le_n_S (wadd f O m)
398 (wadd g O m) (wadd_le f g H4 O O (le_O_n O) m)))) (eq_ind nat (weight_map f
399 (lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H5 (weight_map (wadd f O)
400 (lift (S (S i)) O v)) (lift_weight_add_O O v (S i) f))))))))))))) (\lambda
401 (t1: T).(\lambda (t2: T).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H3:
402 ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
403 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S
404 i))) \to (lt (weight_map f t2) (weight_map g t1)))))))).(\lambda (f: ((nat
405 \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H4: ((\forall (m: nat).(le
406 (f m) (g m))))).(\lambda (H5: (lt (weight_map f (lift (S i) O v)) (g
407 i))).(lt_n_S (plus (weight_map f u2) (weight_map (wadd f O) t2)) (plus
408 (weight_map g u1) (weight_map (wadd g O) t1)) (lt_plus_plus (weight_map f u2)
409 (weight_map g u1) (weight_map (wadd f O) t2) (weight_map (wadd g O) t1) (H1 f
410 g H4 H5) (H3 (wadd f O) (wadd g O) (\lambda (m: nat).(le_S_n (wadd f O m)
411 (wadd g O m) (le_n_S (wadd f O m) (wadd g O m) (wadd_le f g H4 O O (le_O_n O)
412 m)))) (eq_ind nat (weight_map f (lift (S i) O v)) (\lambda (n: nat).(lt n (g
413 i))) H5 (weight_map (wadd f O) (lift (S (S i)) O v)) (lift_weight_add_O O v
414 (S i) f))))))))))))) b)) (\lambda (_: F).(\lambda (t1: T).(\lambda (t2:
415 T).(\lambda (_: (subst0 i v t1 t2)).(\lambda (H3: ((\forall (f0: ((nat \to
416 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f0 m) (g m))))
417 \to ((lt (weight_map f0 (lift (S i) O v)) (g i)) \to (lt (weight_map f0 t2)
418 (weight_map g t1)))))))).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat
419 \to nat))).(\lambda (H4: ((\forall (m: nat).(le (f0 m) (g m))))).(\lambda
420 (H5: (lt (weight_map f0 (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map
421 f0 u2) (weight_map f0 t2)) (plus (weight_map g u1) (weight_map g t1))
422 (lt_plus_plus (weight_map f0 u2) (weight_map g u1) (weight_map f0 t2)
423 (weight_map g t1) (H1 f0 g H4 H5) (H3 f0 g H4 H5)))))))))))) k)))))))) d u t
426 lemma subst0_tlt_head:
427 \forall (u: T).(\forall (t: T).(\forall (z: T).((subst0 O u t z) \to (tlt
428 (THead (Bind Abbr) u z) (THead (Bind Abbr) u t)))))
430 \lambda (u: T).(\lambda (t: T).(\lambda (z: T).(\lambda (H: (subst0 O u t
431 z)).(lt_n_S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
432 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) z)) (plus
433 (weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S
434 (weight_map (\lambda (_: nat).O) u))) t)) (le_lt_plus_plus (weight_map
435 (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
436 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) z) (weight_map
437 (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t) (le_n
438 (weight_map (\lambda (_: nat).O) u)) (subst0_weight_lt u t z O H (wadd
439 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) (wadd (\lambda
440 (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) (\lambda (m: nat).(le_n
441 (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u)) m)))
442 (eq_ind nat (weight_map (\lambda (_: nat).O) (lift O O u)) (\lambda (n:
443 nat).(lt n (S (weight_map (\lambda (_: nat).O) u)))) (eq_ind_r T u (\lambda
444 (t0: T).(lt (weight_map (\lambda (_: nat).O) t0) (S (weight_map (\lambda (_:
445 nat).O) u)))) (le_n (S (weight_map (\lambda (_: nat).O) u))) (lift O O u)
446 (lift_r u O)) (weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda
447 (_: nat).O) u))) (lift (S O) O u)) (lift_weight_add_O (S (weight_map (\lambda
448 (_: nat).O) u)) u O (\lambda (_: nat).O))))))))).
451 \forall (u: T).(\forall (t: T).(\forall (z: T).((subst0 O u t z) \to (tlt z
452 (THead (Bind Abbr) u t)))))
454 \lambda (u: T).(\lambda (t: T).(\lambda (z: T).(\lambda (H: (subst0 O u t
455 z)).(tlt_trans (THead (Bind Abbr) u z) z (THead (Bind Abbr) u t) (tlt_head_dx
456 (Bind Abbr) u z) (subst0_tlt_head u t z H))))).
projects / helm.git / blob