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/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))))))).
31 \forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n:
32 nat).(le (f n) (g n)))) \to (\forall (v: nat).(\forall (w: nat).((lt v w) \to
33 (\forall (n: nat).(le (wadd f v n) (wadd g w n))))))))
35 \lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H:
36 ((\forall (n: nat).(le (f n) (g n))))).(\lambda (v: nat).(\lambda (w:
37 nat).(\lambda (H0: (lt v w)).(\lambda (n: nat).(nat_ind (\lambda (n0:
38 nat).(le (wadd f v n0) (wadd g w n0))) (le_S_n v w (le_S (S v) w H0))
39 (\lambda (n0: nat).(\lambda (_: (le (wadd f v n0) (wadd g w n0))).(H n0)))
43 \forall (n: nat).(eq nat (wadd (\lambda (_: nat).O) O n) O)
45 \lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat (wadd (\lambda (_:
46 nat).O) O n0) O)) (refl_equal nat O) (\lambda (n0: nat).(\lambda (_: (eq nat
47 (wadd (\lambda (_: nat).O) O n0) O)).(refl_equal nat O))) n).
50 \forall (t: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
51 nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f t)
54 \lambda (t: T).(T_ind (\lambda (t0: T).(\forall (f: ((nat \to
55 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n))))
56 \to (le (weight_map f t0) (weight_map g t0)))))) (\lambda (n: nat).(\lambda
57 (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (_: ((\forall
58 (n0: nat).(le (f n0) (g n0))))).(le_n (weight_map g (TSort n))))))) (\lambda
59 (n: nat).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda
60 (H: ((\forall (n0: nat).(le (f n0) (g n0))))).(H n))))) (\lambda (k:
61 K).(K_ind (\lambda (k0: K).(\forall (t0: T).(((\forall (f: ((nat \to
62 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n))))
63 \to (le (weight_map f t0) (weight_map g t0)))))) \to (\forall (t1:
64 T).(((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
65 (n: nat).(le (f n) (g n)))) \to (le (weight_map f t1) (weight_map g t1))))))
66 \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
67 (n: nat).(le (f n) (g n)))) \to (le (weight_map f (THead k0 t0 t1))
68 (weight_map g (THead k0 t0 t1))))))))))) (\lambda (b: B).(B_ind (\lambda (b0:
69 B).(\forall (t0: T).(((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
70 nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f t0)
71 (weight_map g t0)))))) \to (\forall (t1: T).(((\forall (f: ((nat \to
72 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n))))
73 \to (le (weight_map f t1) (weight_map g t1)))))) \to (\forall (f: ((nat \to
74 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n))))
75 \to (le (match b0 with [Abbr \Rightarrow (S (plus (weight_map f t0)
76 (weight_map (wadd f (S (weight_map f t0))) t1))) | Abst \Rightarrow (S (plus
77 (weight_map f t0) (weight_map (wadd f O) t1))) | Void \Rightarrow (S (plus
78 (weight_map f t0) (weight_map (wadd f O) t1)))]) (match b0 with [Abbr
79 \Rightarrow (S (plus (weight_map g t0) (weight_map (wadd g (S (weight_map g
80 t0))) t1))) | Abst \Rightarrow (S (plus (weight_map g t0) (weight_map (wadd g
81 O) t1))) | Void \Rightarrow (S (plus (weight_map g t0) (weight_map (wadd g O)
82 t1)))])))))))))) (\lambda (t0: T).(\lambda (H: ((\forall (f: ((nat \to
83 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n))))
84 \to (le (weight_map f t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda
85 (H0: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
86 (n: nat).(le (f n) (g n)))) \to (le (weight_map f t1) (weight_map g
87 t1))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
88 nat))).(\lambda (H1: ((\forall (n: nat).(le (f n) (g n))))).(le_n_S (plus
89 (weight_map f t0) (weight_map (wadd f (S (weight_map f t0))) t1)) (plus
90 (weight_map g t0) (weight_map (wadd g (S (weight_map g t0))) t1))
91 (plus_le_compat (weight_map f t0) (weight_map g t0) (weight_map (wadd f (S
92 (weight_map f t0))) t1) (weight_map (wadd g (S (weight_map g t0))) t1) (H f g
93 H1) (H0 (wadd f (S (weight_map f t0))) (wadd g (S (weight_map g t0)))
94 (\lambda (n: nat).(wadd_le f g H1 (S (weight_map f t0)) (S (weight_map g t0))
95 (le_n_S (weight_map f t0) (weight_map g t0) (H f g H1)) n))))))))))))
96 (\lambda (t0: T).(\lambda (H: ((\forall (f: ((nat \to nat))).(\forall (g:
97 ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f
98 t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (f:
99 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n)
100 (g n)))) \to (le (weight_map f t1) (weight_map g t1))))))).(\lambda (f: ((nat
101 \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H1: ((\forall (n: nat).(le
102 (f n) (g n))))).(le_n_S (plus (weight_map f t0) (weight_map (wadd f O) t1))
103 (plus (weight_map g t0) (weight_map (wadd g O) t1)) (plus_le_compat
104 (weight_map f t0) (weight_map g t0) (weight_map (wadd f O) t1) (weight_map
105 (wadd g O) t1) (H f g H1) (H0 (wadd f O) (wadd g O) (\lambda (n:
106 nat).(wadd_le f g H1 O O (le_n O) n)))))))))))) (\lambda (t0: T).(\lambda (H:
107 ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n:
108 nat).(le (f n) (g n)))) \to (le (weight_map f t0) (weight_map g
109 t0))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (f: ((nat \to
110 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n))))
111 \to (le (weight_map f t1) (weight_map g t1))))))).(\lambda (f: ((nat \to
112 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H1: ((\forall (n: nat).(le (f
113 n) (g n))))).(le_n_S (plus (weight_map f t0) (weight_map (wadd f O) t1))
114 (plus (weight_map g t0) (weight_map (wadd g O) t1)) (plus_le_compat
115 (weight_map f t0) (weight_map g t0) (weight_map (wadd f O) t1) (weight_map
116 (wadd g O) t1) (H f g H1) (H0 (wadd f O) (wadd g O) (\lambda (n:
117 nat).(wadd_le f g H1 O O (le_n O) n)))))))))))) b)) (\lambda (_: F).(\lambda
118 (t0: T).(\lambda (H: ((\forall (f0: ((nat \to nat))).(\forall (g: ((nat \to
119 nat))).(((\forall (n: nat).(le (f0 n) (g n)))) \to (le (weight_map f0 t0)
120 (weight_map g t0))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (f0: ((nat
121 \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f0 n) (g
122 n)))) \to (le (weight_map f0 t1) (weight_map g t1))))))).(\lambda (f0: ((nat
123 \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H1: ((\forall (n: nat).(le
124 (f0 n) (g n))))).(le_n_S (plus (weight_map f0 t0) (weight_map f0 t1)) (plus
125 (weight_map g t0) (weight_map g t1)) (plus_le_compat (weight_map f0 t0)
126 (weight_map g t0) (weight_map f0 t1) (weight_map g t1) (H f0 g H1) (H0 f0 g
127 H1))))))))))) k)) t).
130 \forall (t: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
131 nat))).(((\forall (n: nat).(eq nat (f n) (g n)))) \to (eq nat (weight_map f
132 t) (weight_map g t)))))
134 \lambda (t: T).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
135 nat))).(\lambda (H: ((\forall (n: nat).(eq nat (f n) (g n))))).(le_antisym
136 (weight_map f t) (weight_map g t) (weight_le t f g (\lambda (n:
137 nat).(eq_ind_r nat (g n) (\lambda (n0: nat).(le n0 (g n))) (le_n (g n)) (f n)
138 (H n)))) (weight_le t g f (\lambda (n: nat).(eq_ind_r nat (g n) (\lambda (n0:
139 nat).(le (g n) n0)) (le_n (g n)) (f n) (H n)))))))).
141 theorem weight_add_O:
142 \forall (t: T).(eq nat (weight_map (wadd (\lambda (_: nat).O) O) t)
143 (weight_map (\lambda (_: nat).O) t))
145 \lambda (t: T).(weight_eq t (wadd (\lambda (_: nat).O) O) (\lambda (_:
146 nat).O) (\lambda (n: nat).(wadd_O n))).
148 theorem weight_add_S:
149 \forall (t: T).(\forall (m: nat).(le (weight_map (wadd (\lambda (_: nat).O)
150 O) t) (weight_map (wadd (\lambda (_: nat).O) (S m)) t)))
152 \lambda (t: T).(\lambda (m: nat).(weight_le t (wadd (\lambda (_: nat).O) O)
153 (wadd (\lambda (_: nat).O) (S m)) (\lambda (n: nat).(wadd_le (\lambda (_:
154 nat).O) (\lambda (_: nat).O) (\lambda (_: nat).(le_n O)) O (S m) (le_S O m
158 \forall (v: T).(\forall (u: T).(\forall (t: T).((tlt u v) \to ((tlt v t) \to
161 \lambda (v: T).(\lambda (u: T).(\lambda (t: T).(\lambda (H: (lt (weight u)
162 (weight v))).(\lambda (H0: (lt (weight v) (weight t))).(lt_trans (weight u)
163 (weight v) (weight t) H H0))))).
166 \forall (k: K).(\forall (u: T).(\forall (t: T).(tlt u (THead k u t))))
168 \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (u: T).(\forall (t: T).(lt
169 (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) (THead
170 k0 u t)))))) (\lambda (b: B).(B_ind (\lambda (b0: B).(\forall (u: T).(\forall
171 (t: T).(lt (weight_map (\lambda (_: nat).O) u) (match b0 with [Abbr
172 \Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
173 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))) | Abst
174 \Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
175 (\lambda (_: nat).O) O) t))) | Void \Rightarrow (S (plus (weight_map (\lambda
176 (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t)))]))))) (\lambda
177 (u: T).(\lambda (t: T).(le_n_S (weight_map (\lambda (_: nat).O) u) (plus
178 (weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S
179 (weight_map (\lambda (_: nat).O) u))) t)) (le_plus_l (weight_map (\lambda (_:
180 nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_:
181 nat).O) u))) t))))) (\lambda (u: T).(\lambda (t: T).(le_n_S (weight_map
182 (\lambda (_: nat).O) u) (plus (weight_map (\lambda (_: nat).O) u) (weight_map
183 (wadd (\lambda (_: nat).O) O) t)) (le_plus_l (weight_map (\lambda (_: nat).O)
184 u) (weight_map (wadd (\lambda (_: nat).O) O) t))))) (\lambda (u: T).(\lambda
185 (t: T).(le_n_S (weight_map (\lambda (_: nat).O) u) (plus (weight_map (\lambda
186 (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t)) (le_plus_l
187 (weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O)
188 t))))) b)) (\lambda (_: F).(\lambda (u: T).(\lambda (t: T).(le_n_S
189 (weight_map (\lambda (_: nat).O) u) (plus (weight_map (\lambda (_: nat).O) u)
190 (weight_map (\lambda (_: nat).O) t)) (le_plus_l (weight_map (\lambda (_:
191 nat).O) u) (weight_map (\lambda (_: nat).O) t)))))) k).
194 \forall (k: K).(\forall (u: T).(\forall (t: T).(tlt t (THead k u t))))
196 \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (u: T).(\forall (t: T).(lt
197 (weight_map (\lambda (_: nat).O) t) (weight_map (\lambda (_: nat).O) (THead
198 k0 u t)))))) (\lambda (b: B).(B_ind (\lambda (b0: B).(\forall (u: T).(\forall
199 (t: T).(lt (weight_map (\lambda (_: nat).O) t) (match b0 with [Abbr
200 \Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
201 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))) | Abst
202 \Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
203 (\lambda (_: nat).O) O) t))) | Void \Rightarrow (S (plus (weight_map (\lambda
204 (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t)))]))))) (\lambda
205 (u: T).(\lambda (t: T).(lt_le_trans (weight_map (\lambda (_: nat).O) t) (S
206 (weight_map (\lambda (_: nat).O) t)) (S (plus (weight_map (\lambda (_:
207 nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_:
208 nat).O) u))) t))) (lt_n_Sn (weight_map (\lambda (_: nat).O) t)) (le_n_S
209 (weight_map (\lambda (_: nat).O) t) (plus (weight_map (\lambda (_: nat).O) u)
210 (weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O)
211 u))) t)) (le_trans (weight_map (\lambda (_: nat).O) t) (weight_map (wadd
212 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t) (plus
213 (weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S
214 (weight_map (\lambda (_: nat).O) u))) t)) (eq_ind nat (weight_map (wadd
215 (\lambda (_: nat).O) O) t) (\lambda (n: nat).(le n (weight_map (wadd (\lambda
216 (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))) (weight_add_S t
217 (weight_map (\lambda (_: nat).O) u)) (weight_map (\lambda (_: nat).O) t)
218 (weight_add_O t)) (le_plus_r (weight_map (\lambda (_: nat).O) u) (weight_map
219 (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t)))))))
220 (\lambda (u: T).(\lambda (t: T).(eq_ind_r nat (weight_map (\lambda (_:
221 nat).O) t) (\lambda (n: nat).(lt (weight_map (\lambda (_: nat).O) t) (S (plus
222 (weight_map (\lambda (_: nat).O) u) n)))) (le_n_S (weight_map (\lambda (_:
223 nat).O) t) (plus (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_:
224 nat).O) t)) (le_plus_r (weight_map (\lambda (_: nat).O) u) (weight_map
225 (\lambda (_: nat).O) t))) (weight_map (wadd (\lambda (_: nat).O) O) t)
226 (weight_add_O t)))) (\lambda (u: T).(\lambda (t: T).(eq_ind_r nat (weight_map
227 (\lambda (_: nat).O) t) (\lambda (n: nat).(lt (weight_map (\lambda (_:
228 nat).O) t) (S (plus (weight_map (\lambda (_: nat).O) u) n)))) (le_n_S
229 (weight_map (\lambda (_: nat).O) t) (plus (weight_map (\lambda (_: nat).O) u)
230 (weight_map (\lambda (_: nat).O) t)) (le_plus_r (weight_map (\lambda (_:
231 nat).O) u) (weight_map (\lambda (_: nat).O) t))) (weight_map (wadd (\lambda
232 (_: nat).O) O) t) (weight_add_O t)))) b)) (\lambda (_: F).(\lambda (u:
233 T).(\lambda (t: T).(le_n_S (weight_map (\lambda (_: nat).O) t) (plus
234 (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) t))
235 (le_plus_r (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_:
238 theorem tlt_wf__q_ind:
239 \forall (P: ((T \to Prop))).(((\forall (n: nat).((\lambda (P0: ((T \to
240 Prop))).(\lambda (n0: nat).(\forall (t: T).((eq nat (weight t) n0) \to (P0
241 t))))) P n))) \to (\forall (t: T).(P t)))
243 let Q \def (\lambda (P: ((T \to Prop))).(\lambda (n: nat).(\forall (t:
244 T).((eq nat (weight t) n) \to (P t))))) in (\lambda (P: ((T \to
245 Prop))).(\lambda (H: ((\forall (n: nat).(\forall (t: T).((eq nat (weight t)
246 n) \to (P t)))))).(\lambda (t: T).(H (weight t) t (refl_equal nat (weight
250 \forall (P: ((T \to Prop))).(((\forall (t: T).(((\forall (v: T).((tlt v t)
251 \to (P v)))) \to (P t)))) \to (\forall (t: T).(P t)))
253 let Q \def (\lambda (P: ((T \to Prop))).(\lambda (n: nat).(\forall (t:
254 T).((eq nat (weight t) n) \to (P t))))) in (\lambda (P: ((T \to
255 Prop))).(\lambda (H: ((\forall (t: T).(((\forall (v: T).((lt (weight v)
256 (weight t)) \to (P v)))) \to (P t))))).(\lambda (t: T).(tlt_wf__q_ind
257 (\lambda (t0: T).(P t0)) (\lambda (n: nat).(lt_wf_ind n (Q (\lambda (t0:
258 T).(P t0))) (\lambda (n0: nat).(\lambda (H0: ((\forall (m: nat).((lt m n0)
259 \to (Q (\lambda (t0: T).(P t0)) m))))).(\lambda (t0: T).(\lambda (H1: (eq nat
260 (weight t0) n0)).(let H2 \def (eq_ind_r nat n0 (\lambda (n1: nat).(\forall
261 (m: nat).((lt m n1) \to (\forall (t1: T).((eq nat (weight t1) m) \to (P
262 t1)))))) H0 (weight t0) H1) in (H t0 (\lambda (v: T).(\lambda (H3: (lt
263 (weight v) (weight t0))).(H2 (weight v) H3 v (refl_equal nat (weight
264 v))))))))))))) t)))).