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 (le_plus_plus (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)) (le_plus_plus (weight_map
104 f t0) (weight_map g t0) (weight_map (wadd f O) t1) (weight_map (wadd g O) t1)
105 (H f g H1) (H0 (wadd f O) (wadd g O) (\lambda (n: nat).(wadd_le f g H1 O O
106 (le_n O) n)))))))))))) (\lambda (t0: T).(\lambda (H: ((\forall (f: ((nat \to
107 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n))))
108 \to (le (weight_map f t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda
109 (H0: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
110 (n: nat).(le (f n) (g n)))) \to (le (weight_map f t1) (weight_map g
111 t1))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
112 nat))).(\lambda (H1: ((\forall (n: nat).(le (f n) (g n))))).(le_n_S (plus
113 (weight_map f t0) (weight_map (wadd f O) t1)) (plus (weight_map g t0)
114 (weight_map (wadd g O) t1)) (le_plus_plus (weight_map f t0) (weight_map g t0)
115 (weight_map (wadd f O) t1) (weight_map (wadd g O) t1) (H f g H1) (H0 (wadd f
116 O) (wadd g O) (\lambda (n: nat).(wadd_le f g H1 O O (le_n O) n))))))))))))
117 b)) (\lambda (_: F).(\lambda (t0: T).(\lambda (H: ((\forall (f0: ((nat \to
118 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f0 n) (g n))))
119 \to (le (weight_map f0 t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda
120 (H0: ((\forall (f0: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
121 (n: nat).(le (f0 n) (g n)))) \to (le (weight_map f0 t1) (weight_map g
122 t1))))))).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat \to
123 nat))).(\lambda (H1: ((\forall (n: nat).(le (f0 n) (g n))))).(le_n_S (plus
124 (weight_map f0 t0) (weight_map f0 t1)) (plus (weight_map g t0) (weight_map g
125 t1)) (le_plus_plus (weight_map f0 t0) (weight_map g t0) (weight_map f0 t1)
126 (weight_map g t1) (H f0 g H1) (H0 f0 g H1))))))))))) k)) t).
129 \forall (t: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
130 nat))).(((\forall (n: nat).(eq nat (f n) (g n)))) \to (eq nat (weight_map f
131 t) (weight_map g t)))))
133 \lambda (t: T).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
134 nat))).(\lambda (H: ((\forall (n: nat).(eq nat (f n) (g n))))).(le_antisym
135 (weight_map f t) (weight_map g t) (weight_le t f g (\lambda (n:
136 nat).(eq_ind_r nat (g n) (\lambda (n0: nat).(le n0 (g n))) (le_n (g n)) (f n)
137 (H n)))) (weight_le t g f (\lambda (n: nat).(eq_ind_r nat (g n) (\lambda (n0:
138 nat).(le (g n) n0)) (le_n (g n)) (f n) (H n)))))))).
140 theorem weight_add_O:
141 \forall (t: T).(eq nat (weight_map (wadd (\lambda (_: nat).O) O) t)
142 (weight_map (\lambda (_: nat).O) t))
144 \lambda (t: T).(weight_eq t (wadd (\lambda (_: nat).O) O) (\lambda (_:
145 nat).O) (\lambda (n: nat).(wadd_O n))).
147 theorem weight_add_S:
148 \forall (t: T).(\forall (m: nat).(le (weight_map (wadd (\lambda (_: nat).O)
149 O) t) (weight_map (wadd (\lambda (_: nat).O) (S m)) t)))
151 \lambda (t: T).(\lambda (m: nat).(weight_le t (wadd (\lambda (_: nat).O) O)
152 (wadd (\lambda (_: nat).O) (S m)) (\lambda (n: nat).(wadd_le (\lambda (_:
153 nat).O) (\lambda (_: nat).O) (\lambda (_: nat).(le_n O)) O (S m) (le_S O m
157 \forall (v: T).(\forall (u: T).(\forall (t: T).((tlt u v) \to ((tlt v t) \to
160 \lambda (v: T).(\lambda (u: T).(\lambda (t: T).(\lambda (H: (lt (weight u)
161 (weight v))).(\lambda (H0: (lt (weight v) (weight t))).(lt_trans (weight u)
162 (weight v) (weight t) H H0))))).
165 \forall (k: K).(\forall (u: T).(\forall (t: T).(tlt u (THead k u t))))
167 \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (u: T).(\forall (t: T).(lt
168 (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) (THead
169 k0 u t)))))) (\lambda (b: B).(B_ind (\lambda (b0: B).(\forall (u: T).(\forall
170 (t: T).(lt (weight_map (\lambda (_: nat).O) u) (match b0 with [Abbr
171 \Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
172 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))) | Abst
173 \Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
174 (\lambda (_: nat).O) O) t))) | Void \Rightarrow (S (plus (weight_map (\lambda
175 (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t)))]))))) (\lambda
176 (u: T).(\lambda (t: T).(le_n_S (weight_map (\lambda (_: nat).O) u) (plus
177 (weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S
178 (weight_map (\lambda (_: nat).O) u))) t)) (le_plus_l (weight_map (\lambda (_:
179 nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_:
180 nat).O) u))) t))))) (\lambda (u: T).(\lambda (t: T).(le_n_S (weight_map
181 (\lambda (_: nat).O) u) (plus (weight_map (\lambda (_: nat).O) u) (weight_map
182 (wadd (\lambda (_: nat).O) O) t)) (le_plus_l (weight_map (\lambda (_: nat).O)
183 u) (weight_map (wadd (\lambda (_: nat).O) O) t))))) (\lambda (u: T).(\lambda
184 (t: T).(le_n_S (weight_map (\lambda (_: nat).O) u) (plus (weight_map (\lambda
185 (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t)) (le_plus_l
186 (weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O)
187 t))))) b)) (\lambda (_: F).(\lambda (u: T).(\lambda (t: T).(le_n_S
188 (weight_map (\lambda (_: nat).O) u) (plus (weight_map (\lambda (_: nat).O) u)
189 (weight_map (\lambda (_: nat).O) t)) (le_plus_l (weight_map (\lambda (_:
190 nat).O) u) (weight_map (\lambda (_: nat).O) t)))))) k).
193 \forall (k: K).(\forall (u: T).(\forall (t: T).(tlt t (THead k u t))))
195 \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (u: T).(\forall (t: T).(lt
196 (weight_map (\lambda (_: nat).O) t) (weight_map (\lambda (_: nat).O) (THead
197 k0 u t)))))) (\lambda (b: B).(B_ind (\lambda (b0: B).(\forall (u: T).(\forall
198 (t: T).(lt (weight_map (\lambda (_: nat).O) t) (match b0 with [Abbr
199 \Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
200 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))) | Abst
201 \Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
202 (\lambda (_: nat).O) O) t))) | Void \Rightarrow (S (plus (weight_map (\lambda
203 (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t)))]))))) (\lambda
204 (u: T).(\lambda (t: T).(lt_le_trans (weight_map (\lambda (_: nat).O) t) (S
205 (weight_map (\lambda (_: nat).O) t)) (S (plus (weight_map (\lambda (_:
206 nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_:
207 nat).O) u))) t))) (lt_n_Sn (weight_map (\lambda (_: nat).O) t)) (le_n_S
208 (weight_map (\lambda (_: nat).O) t) (plus (weight_map (\lambda (_: nat).O) u)
209 (weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O)
210 u))) t)) (le_trans (weight_map (\lambda (_: nat).O) t) (weight_map (wadd
211 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t) (plus
212 (weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S
213 (weight_map (\lambda (_: nat).O) u))) t)) (eq_ind nat (weight_map (wadd
214 (\lambda (_: nat).O) O) t) (\lambda (n: nat).(le n (weight_map (wadd (\lambda
215 (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))) (weight_add_S t
216 (weight_map (\lambda (_: nat).O) u)) (weight_map (\lambda (_: nat).O) t)
217 (weight_add_O t)) (le_plus_r (weight_map (\lambda (_: nat).O) u) (weight_map
218 (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t)))))))
219 (\lambda (u: T).(\lambda (t: T).(eq_ind_r nat (weight_map (\lambda (_:
220 nat).O) t) (\lambda (n: nat).(lt (weight_map (\lambda (_: nat).O) t) (S (plus
221 (weight_map (\lambda (_: nat).O) u) n)))) (le_n_S (weight_map (\lambda (_:
222 nat).O) t) (plus (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_:
223 nat).O) t)) (le_plus_r (weight_map (\lambda (_: nat).O) u) (weight_map
224 (\lambda (_: nat).O) t))) (weight_map (wadd (\lambda (_: nat).O) O) t)
225 (weight_add_O t)))) (\lambda (u: T).(\lambda (t: T).(eq_ind_r nat (weight_map
226 (\lambda (_: nat).O) t) (\lambda (n: nat).(lt (weight_map (\lambda (_:
227 nat).O) t) (S (plus (weight_map (\lambda (_: nat).O) u) n)))) (le_n_S
228 (weight_map (\lambda (_: nat).O) t) (plus (weight_map (\lambda (_: nat).O) u)
229 (weight_map (\lambda (_: nat).O) t)) (le_plus_r (weight_map (\lambda (_:
230 nat).O) u) (weight_map (\lambda (_: nat).O) t))) (weight_map (wadd (\lambda
231 (_: nat).O) O) t) (weight_add_O t)))) b)) (\lambda (_: F).(\lambda (u:
232 T).(\lambda (t: T).(le_n_S (weight_map (\lambda (_: nat).O) t) (plus
233 (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) t))
234 (le_plus_r (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_:
237 theorem tlt_wf__q_ind:
238 \forall (P: ((T \to Prop))).(((\forall (n: nat).((\lambda (P0: ((T \to
239 Prop))).(\lambda (n0: nat).(\forall (t: T).((eq nat (weight t) n0) \to (P0
240 t))))) P n))) \to (\forall (t: T).(P t)))
242 let Q \def (\lambda (P: ((T \to Prop))).(\lambda (n: nat).(\forall (t:
243 T).((eq nat (weight t) n) \to (P t))))) in (\lambda (P: ((T \to
244 Prop))).(\lambda (H: ((\forall (n: nat).(\forall (t: T).((eq nat (weight t)
245 n) \to (P t)))))).(\lambda (t: T).(H (weight t) t (refl_equal nat (weight
249 \forall (P: ((T \to Prop))).(((\forall (t: T).(((\forall (v: T).((tlt v t)
250 \to (P v)))) \to (P t)))) \to (\forall (t: T).(P t)))
252 let Q \def (\lambda (P: ((T \to Prop))).(\lambda (n: nat).(\forall (t:
253 T).((eq nat (weight t) n) \to (P t))))) in (\lambda (P: ((T \to
254 Prop))).(\lambda (H: ((\forall (t: T).(((\forall (v: T).((lt (weight v)
255 (weight t)) \to (P v)))) \to (P t))))).(\lambda (t: T).(tlt_wf__q_ind
256 (\lambda (t0: T).(P t0)) (\lambda (n: nat).(lt_wf_ind n (Q (\lambda (t0:
257 T).(P t0))) (\lambda (n0: nat).(\lambda (H0: ((\forall (m: nat).((lt m n0)
258 \to (Q (\lambda (t0: T).(P t0)) m))))).(\lambda (t0: T).(\lambda (H1: (eq nat
259 (weight t0) n0)).(let H2 \def (eq_ind_r nat n0 (\lambda (n1: nat).(\forall
260 (m: nat).((lt m n1) \to (\forall (t1: T).((eq nat (weight t1) m) \to (P
261 t1)))))) H0 (weight t0) H1) in (H t0 (\lambda (v: T).(\lambda (H3: (lt
262 (weight v) (weight t0))).(H2 (weight v) H3 v (refl_equal nat (weight
263 v))))))))))))) t)))).