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/tlt/defs.ma".
20 \forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n:
21 nat).(le (f n) (g n)))) \to (\forall (v: nat).(\forall (w: nat).((le v w) \to
22 (\forall (n: nat).(le (wadd f v n) (wadd g w n))))))))
24 \lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H:
25 ((\forall (n: nat).(le (f n) (g n))))).(\lambda (v: nat).(\lambda (w:
26 nat).(\lambda (H0: (le v w)).(\lambda (n: nat).(nat_ind (\lambda (n0:
27 nat).(le (wadd f v n0) (wadd g w n0))) H0 (\lambda (n0: nat).(\lambda (_: (le
28 (wadd f v n0) (wadd g w n0))).(H n0))) n))))))).
34 \forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n:
35 nat).(le (f n) (g n)))) \to (\forall (v: nat).(\forall (w: nat).((lt v w) \to
36 (\forall (n: nat).(le (wadd f v n) (wadd g w n))))))))
38 \lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H:
39 ((\forall (n: nat).(le (f n) (g n))))).(\lambda (v: nat).(\lambda (w:
40 nat).(\lambda (H0: (lt v w)).(\lambda (n: nat).(nat_ind (\lambda (n0:
41 nat).(le (wadd f v n0) (wadd g w n0))) (le_S_n v w (le_S (S v) w H0))
42 (\lambda (n0: nat).(\lambda (_: (le (wadd f v n0) (wadd g w n0))).(H n0)))
49 \forall (n: nat).(eq nat (wadd (\lambda (_: nat).O) O n) O)
51 \lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat (wadd (\lambda (_:
52 nat).O) O n0) O)) (refl_equal nat O) (\lambda (n0: nat).(\lambda (_: (eq nat
53 (wadd (\lambda (_: nat).O) O n0) O)).(refl_equal nat O))) n).
59 \forall (t: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
60 nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f t)
63 \lambda (t: T).(T_ind (\lambda (t0: T).(\forall (f: ((nat \to
64 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n))))
65 \to (le (weight_map f t0) (weight_map g t0)))))) (\lambda (n: nat).(\lambda
66 (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (_: ((\forall
67 (n0: nat).(le (f n0) (g n0))))).(le_n (weight_map g (TSort n))))))) (\lambda
68 (n: nat).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda
69 (H: ((\forall (n0: nat).(le (f n0) (g n0))))).(H n))))) (\lambda (k:
70 K).(K_ind (\lambda (k0: K).(\forall (t0: T).(((\forall (f: ((nat \to
71 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n))))
72 \to (le (weight_map f t0) (weight_map g t0)))))) \to (\forall (t1:
73 T).(((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
74 (n: nat).(le (f n) (g n)))) \to (le (weight_map f t1) (weight_map g t1))))))
75 \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
76 (n: nat).(le (f n) (g n)))) \to (le (weight_map f (THead k0 t0 t1))
77 (weight_map g (THead k0 t0 t1))))))))))) (\lambda (b: B).(B_ind (\lambda (b0:
78 B).(\forall (t0: T).(((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
79 nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f t0)
80 (weight_map g t0)))))) \to (\forall (t1: T).(((\forall (f: ((nat \to
81 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n))))
82 \to (le (weight_map f t1) (weight_map g t1)))))) \to (\forall (f: ((nat \to
83 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n))))
84 \to (le (match b0 with [Abbr \Rightarrow (S (plus (weight_map f t0)
85 (weight_map (wadd f (S (weight_map f t0))) t1))) | Abst \Rightarrow (S (plus
86 (weight_map f t0) (weight_map (wadd f O) t1))) | Void \Rightarrow (S (plus
87 (weight_map f t0) (weight_map (wadd f O) t1)))]) (match b0 with [Abbr
88 \Rightarrow (S (plus (weight_map g t0) (weight_map (wadd g (S (weight_map g
89 t0))) t1))) | Abst \Rightarrow (S (plus (weight_map g t0) (weight_map (wadd g
90 O) t1))) | Void \Rightarrow (S (plus (weight_map g t0) (weight_map (wadd g O)
91 t1)))])))))))))) (\lambda (t0: T).(\lambda (H: ((\forall (f: ((nat \to
92 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n))))
93 \to (le (weight_map f t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda
94 (H0: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
95 (n: nat).(le (f n) (g n)))) \to (le (weight_map f t1) (weight_map g
96 t1))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
97 nat))).(\lambda (H1: ((\forall (n: nat).(le (f n) (g n))))).(le_n_S (plus
98 (weight_map f t0) (weight_map (wadd f (S (weight_map f t0))) t1)) (plus
99 (weight_map g t0) (weight_map (wadd g (S (weight_map g t0))) t1))
100 (le_plus_plus (weight_map f t0) (weight_map g t0) (weight_map (wadd f (S
101 (weight_map f t0))) t1) (weight_map (wadd g (S (weight_map g t0))) t1) (H f g
102 H1) (H0 (wadd f (S (weight_map f t0))) (wadd g (S (weight_map g t0)))
103 (\lambda (n: nat).(wadd_le f g H1 (S (weight_map f t0)) (S (weight_map g t0))
104 (le_n_S (weight_map f t0) (weight_map g t0) (H f g H1)) n))))))))))))
105 (\lambda (t0: T).(\lambda (H: ((\forall (f: ((nat \to nat))).(\forall (g:
106 ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f
107 t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (f:
108 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n)
109 (g n)))) \to (le (weight_map f t1) (weight_map g t1))))))).(\lambda (f: ((nat
110 \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H1: ((\forall (n: nat).(le
111 (f n) (g n))))).(le_n_S (plus (weight_map f t0) (weight_map (wadd f O) t1))
112 (plus (weight_map g t0) (weight_map (wadd g O) t1)) (le_plus_plus (weight_map
113 f t0) (weight_map g t0) (weight_map (wadd f O) t1) (weight_map (wadd g O) t1)
114 (H f g H1) (H0 (wadd f O) (wadd g O) (\lambda (n: nat).(wadd_le f g H1 O O
115 (le_n O) n)))))))))))) (\lambda (t0: T).(\lambda (H: ((\forall (f: ((nat \to
116 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n))))
117 \to (le (weight_map f t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda
118 (H0: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
119 (n: nat).(le (f n) (g n)))) \to (le (weight_map f t1) (weight_map g
120 t1))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
121 nat))).(\lambda (H1: ((\forall (n: nat).(le (f n) (g n))))).(le_n_S (plus
122 (weight_map f t0) (weight_map (wadd f O) t1)) (plus (weight_map g t0)
123 (weight_map (wadd g O) t1)) (le_plus_plus (weight_map f t0) (weight_map g t0)
124 (weight_map (wadd f O) t1) (weight_map (wadd g O) t1) (H f g H1) (H0 (wadd f
125 O) (wadd g O) (\lambda (n: nat).(wadd_le f g H1 O O (le_n O) n))))))))))))
126 b)) (\lambda (_: F).(\lambda (t0: T).(\lambda (H: ((\forall (f0: ((nat \to
127 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f0 n) (g n))))
128 \to (le (weight_map f0 t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda
129 (H0: ((\forall (f0: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
130 (n: nat).(le (f0 n) (g n)))) \to (le (weight_map f0 t1) (weight_map g
131 t1))))))).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat \to
132 nat))).(\lambda (H1: ((\forall (n: nat).(le (f0 n) (g n))))).(le_n_S (plus
133 (weight_map f0 t0) (weight_map f0 t1)) (plus (weight_map g t0) (weight_map g
134 t1)) (le_plus_plus (weight_map f0 t0) (weight_map g t0) (weight_map f0 t1)
135 (weight_map g t1) (H f0 g H1) (H0 f0 g H1))))))))))) k)) t).
141 \forall (t: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
142 nat))).(((\forall (n: nat).(eq nat (f n) (g n)))) \to (eq nat (weight_map f
143 t) (weight_map g t)))))
145 \lambda (t: T).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
146 nat))).(\lambda (H: ((\forall (n: nat).(eq nat (f n) (g n))))).(le_antisym
147 (weight_map f t) (weight_map g t) (weight_le t f g (\lambda (n:
148 nat).(eq_ind_r nat (g n) (\lambda (n0: nat).(le n0 (g n))) (le_n (g n)) (f n)
149 (H n)))) (weight_le t g f (\lambda (n: nat).(eq_ind_r nat (g n) (\lambda (n0:
150 nat).(le (g n) n0)) (le_n (g n)) (f n) (H n)))))))).
155 theorem weight_add_O:
156 \forall (t: T).(eq nat (weight_map (wadd (\lambda (_: nat).O) O) t)
157 (weight_map (\lambda (_: nat).O) t))
159 \lambda (t: T).(weight_eq t (wadd (\lambda (_: nat).O) O) (\lambda (_:
160 nat).O) (\lambda (n: nat).(wadd_O n))).
165 theorem weight_add_S:
166 \forall (t: T).(\forall (m: nat).(le (weight_map (wadd (\lambda (_: nat).O)
167 O) t) (weight_map (wadd (\lambda (_: nat).O) (S m)) t)))
169 \lambda (t: T).(\lambda (m: nat).(weight_le t (wadd (\lambda (_: nat).O) O)
170 (wadd (\lambda (_: nat).O) (S m)) (\lambda (n: nat).(wadd_le (\lambda (_:
171 nat).O) (\lambda (_: nat).O) (\lambda (_: nat).(le_n O)) O (S m) (le_S O m
178 \forall (v: T).(\forall (u: T).(\forall (t: T).((tlt u v) \to ((tlt v t) \to
181 \lambda (v: T).(\lambda (u: T).(\lambda (t: T).(\lambda (H: (lt (weight u)
182 (weight v))).(\lambda (H0: (lt (weight v) (weight t))).(lt_trans (weight u)
183 (weight v) (weight t) H H0))))).
189 \forall (k: K).(\forall (u: T).(\forall (t: T).(tlt u (THead k u t))))
191 \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (u: T).(\forall (t: T).(lt
192 (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) (THead
193 k0 u t)))))) (\lambda (b: B).(B_ind (\lambda (b0: B).(\forall (u: T).(\forall
194 (t: T).(lt (weight_map (\lambda (_: nat).O) u) (match b0 with [Abbr
195 \Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
196 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))) | Abst
197 \Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
198 (\lambda (_: nat).O) O) t))) | Void \Rightarrow (S (plus (weight_map (\lambda
199 (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t)))]))))) (\lambda
200 (u: T).(\lambda (t: T).(le_n_S (weight_map (\lambda (_: nat).O) u) (plus
201 (weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S
202 (weight_map (\lambda (_: nat).O) u))) t)) (le_plus_l (weight_map (\lambda (_:
203 nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_:
204 nat).O) u))) t))))) (\lambda (u: T).(\lambda (t: T).(le_n_S (weight_map
205 (\lambda (_: nat).O) u) (plus (weight_map (\lambda (_: nat).O) u) (weight_map
206 (wadd (\lambda (_: nat).O) O) t)) (le_plus_l (weight_map (\lambda (_: nat).O)
207 u) (weight_map (wadd (\lambda (_: nat).O) O) t))))) (\lambda (u: T).(\lambda
208 (t: T).(le_n_S (weight_map (\lambda (_: nat).O) u) (plus (weight_map (\lambda
209 (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t)) (le_plus_l
210 (weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O)
211 t))))) b)) (\lambda (_: F).(\lambda (u: T).(\lambda (t: T).(le_n_S
212 (weight_map (\lambda (_: nat).O) u) (plus (weight_map (\lambda (_: nat).O) u)
213 (weight_map (\lambda (_: nat).O) t)) (le_plus_l (weight_map (\lambda (_:
214 nat).O) u) (weight_map (\lambda (_: nat).O) t)))))) k).
220 \forall (k: K).(\forall (u: T).(\forall (t: T).(tlt t (THead k u t))))
222 \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (u: T).(\forall (t: T).(lt
223 (weight_map (\lambda (_: nat).O) t) (weight_map (\lambda (_: nat).O) (THead
224 k0 u t)))))) (\lambda (b: B).(B_ind (\lambda (b0: B).(\forall (u: T).(\forall
225 (t: T).(lt (weight_map (\lambda (_: nat).O) t) (match b0 with [Abbr
226 \Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
227 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))) | Abst
228 \Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
229 (\lambda (_: nat).O) O) t))) | Void \Rightarrow (S (plus (weight_map (\lambda
230 (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t)))]))))) (\lambda
231 (u: T).(\lambda (t: T).(lt_le_trans (weight_map (\lambda (_: nat).O) t) (S
232 (weight_map (\lambda (_: nat).O) t)) (S (plus (weight_map (\lambda (_:
233 nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_:
234 nat).O) u))) t))) (lt_n_Sn (weight_map (\lambda (_: nat).O) t)) (le_n_S
235 (weight_map (\lambda (_: nat).O) t) (plus (weight_map (\lambda (_: nat).O) u)
236 (weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O)
237 u))) t)) (le_trans (weight_map (\lambda (_: nat).O) t) (weight_map (wadd
238 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t) (plus
239 (weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S
240 (weight_map (\lambda (_: nat).O) u))) t)) (eq_ind nat (weight_map (wadd
241 (\lambda (_: nat).O) O) t) (\lambda (n: nat).(le n (weight_map (wadd (\lambda
242 (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))) (weight_add_S t
243 (weight_map (\lambda (_: nat).O) u)) (weight_map (\lambda (_: nat).O) t)
244 (weight_add_O t)) (le_plus_r (weight_map (\lambda (_: nat).O) u) (weight_map
245 (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t)))))))
246 (\lambda (u: T).(\lambda (t: T).(eq_ind_r nat (weight_map (\lambda (_:
247 nat).O) t) (\lambda (n: nat).(lt (weight_map (\lambda (_: nat).O) t) (S (plus
248 (weight_map (\lambda (_: nat).O) u) n)))) (le_n_S (weight_map (\lambda (_:
249 nat).O) t) (plus (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_:
250 nat).O) t)) (le_plus_r (weight_map (\lambda (_: nat).O) u) (weight_map
251 (\lambda (_: nat).O) t))) (weight_map (wadd (\lambda (_: nat).O) O) t)
252 (weight_add_O t)))) (\lambda (u: T).(\lambda (t: T).(eq_ind_r nat (weight_map
253 (\lambda (_: nat).O) t) (\lambda (n: nat).(lt (weight_map (\lambda (_:
254 nat).O) t) (S (plus (weight_map (\lambda (_: nat).O) u) n)))) (le_n_S
255 (weight_map (\lambda (_: nat).O) t) (plus (weight_map (\lambda (_: nat).O) u)
256 (weight_map (\lambda (_: nat).O) t)) (le_plus_r (weight_map (\lambda (_:
257 nat).O) u) (weight_map (\lambda (_: nat).O) t))) (weight_map (wadd (\lambda
258 (_: nat).O) O) t) (weight_add_O t)))) b)) (\lambda (_: F).(\lambda (u:
259 T).(\lambda (t: T).(le_n_S (weight_map (\lambda (_: nat).O) t) (plus
260 (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) t))
261 (le_plus_r (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_:
267 theorem tlt_wf__q_ind:
268 \forall (P: ((T \to Prop))).(((\forall (n: nat).((\lambda (P0: ((T \to
269 Prop))).(\lambda (n0: nat).(\forall (t: T).((eq nat (weight t) n0) \to (P0
270 t))))) P n))) \to (\forall (t: T).(P t)))
272 let Q \def (\lambda (P: ((T \to Prop))).(\lambda (n: nat).(\forall (t:
273 T).((eq nat (weight t) n) \to (P t))))) in (\lambda (P: ((T \to
274 Prop))).(\lambda (H: ((\forall (n: nat).(\forall (t: T).((eq nat (weight t)
275 n) \to (P t)))))).(\lambda (t: T).(H (weight t) t (refl_equal nat (weight
282 \forall (P: ((T \to Prop))).(((\forall (t: T).(((\forall (v: T).((tlt v t)
283 \to (P v)))) \to (P t)))) \to (\forall (t: T).(P t)))
285 let Q \def (\lambda (P: ((T \to Prop))).(\lambda (n: nat).(\forall (t:
286 T).((eq nat (weight t) n) \to (P t))))) in (\lambda (P: ((T \to
287 Prop))).(\lambda (H: ((\forall (t: T).(((\forall (v: T).((lt (weight v)
288 (weight t)) \to (P v)))) \to (P t))))).(\lambda (t: T).(tlt_wf__q_ind
289 (\lambda (t0: T).(P t0)) (\lambda (n: nat).(lt_wf_ind n (Q (\lambda (t0:
290 T).(P t0))) (\lambda (n0: nat).(\lambda (H0: ((\forall (m: nat).((lt m n0)
291 \to (Q (\lambda (t0: T).(P t0)) m))))).(\lambda (t0: T).(\lambda (H1: (eq nat
292 (weight t0) n0)).(let H2 \def (eq_ind_r nat n0 (\lambda (n1: nat).(\forall
293 (m: nat).((lt m n1) \to (\forall (t1: T).((eq nat (weight t1) m) \to (P
294 t1)))))) H0 (weight t0) H1) in (H t0 (\lambda (v: T).(\lambda (H3: (lt
295 (weight v) (weight t0))).(H2 (weight v) H3 v (refl_equal nat (weight
296 v))))))))))))) t)))).