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 set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst0/tlt".
19 include "subst0/defs.ma".
21 include "lift/props.ma".
23 include "lift/tlt.ma".
25 theorem subst0_weight_le:
26 \forall (u: T).(\forall (t: T).(\forall (z: T).(\forall (d: nat).((subst0 d
27 u t z) \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
28 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
29 d) O u)) (g d)) \to (le (weight_map f z) (weight_map g t))))))))))
31 \lambda (u: T).(\lambda (t: T).(\lambda (z: T).(\lambda (d: nat).(\lambda
32 (H: (subst0 d u t z)).(subst0_ind (\lambda (n: nat).(\lambda (t0: T).(\lambda
33 (t1: T).(\lambda (t2: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
34 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
35 n) O t0)) (g n)) \to (le (weight_map f t2) (weight_map g t1))))))))))
36 (\lambda (v: T).(\lambda (i: nat).(\lambda (f: ((nat \to nat))).(\lambda (g:
37 ((nat \to nat))).(\lambda (_: ((\forall (m: nat).(le (f m) (g m))))).(\lambda
38 (H1: (lt (weight_map f (lift (S i) O v)) (g i))).(le_S_n (weight_map f (lift
39 (S i) O v)) (weight_map g (TLRef i)) (le_S (S (weight_map f (lift (S i) O
40 v))) (weight_map g (TLRef i)) H1)))))))) (\lambda (v: T).(\lambda (u2:
41 T).(\lambda (u1: T).(\lambda (i: nat).(\lambda (_: (subst0 i v u1
42 u2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
43 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
44 i) O v)) (g i)) \to (le (weight_map f u2) (weight_map g u1)))))))).(\lambda
45 (t0: T).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (f: ((nat \to
46 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
47 \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (le (weight_map f (THead
48 k0 u2 t0)) (weight_map g (THead k0 u1 t0)))))))) (\lambda (b: B).(B_ind
49 (\lambda (b0: B).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
50 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
51 i) O v)) (g i)) \to (le (weight_map f (THead (Bind b0) u2 t0)) (weight_map g
52 (THead (Bind b0) u1 t0)))))))) (\lambda (f: ((nat \to nat))).(\lambda (g:
53 ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f m) (g
54 m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g i))).(le_n_S
55 (plus (weight_map f u2) (weight_map (wadd f (S (weight_map f u2))) t0)) (plus
56 (weight_map g u1) (weight_map (wadd g (S (weight_map g u1))) t0))
57 (plus_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd f (S
58 (weight_map f u2))) t0) (weight_map (wadd g (S (weight_map g u1))) t0) (H1 f
59 g H2 H3) (weight_le t0 (wadd f (S (weight_map f u2))) (wadd g (S (weight_map
60 g u1))) (\lambda (n: nat).(wadd_le f g H2 (S (weight_map f u2)) (S
61 (weight_map g u1)) (le_n_S (weight_map f u2) (weight_map g u1) (H1 f g H2
62 H3)) n))))))))) (\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
63 nat))).(\lambda (H2: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H3: (lt
64 (weight_map f (lift (S i) O v)) (g i))).(le_n_S (plus (weight_map f u2)
65 (weight_map (wadd f O) t0)) (plus (weight_map g u1) (weight_map (wadd g O)
66 t0)) (plus_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd f
67 O) t0) (weight_map (wadd g O) t0) (H1 f g H2 H3) (weight_le t0 (wadd f O)
68 (wadd g O) (\lambda (n: nat).(wadd_le f g H2 O O (le_n O) n))))))))) (\lambda
69 (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall
70 (m: nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O
71 v)) (g i))).(le_n_S (plus (weight_map f u2) (weight_map (wadd f O) t0)) (plus
72 (weight_map g u1) (weight_map (wadd g O) t0)) (plus_le_compat (weight_map f
73 u2) (weight_map g u1) (weight_map (wadd f O) t0) (weight_map (wadd g O) t0)
74 (H1 f g H2 H3) (weight_le t0 (wadd f O) (wadd g O) (\lambda (n: nat).(wadd_le
75 f g H2 O O (le_n O) n))))))))) b)) (\lambda (_: F).(\lambda (f0: ((nat \to
76 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f0
77 m) (g m))))).(\lambda (H3: (lt (weight_map f0 (lift (S i) O v)) (g
78 i))).(le_n_S (plus (weight_map f0 u2) (weight_map f0 t0)) (plus (weight_map g
79 u1) (weight_map g t0)) (plus_le_compat (weight_map f0 u2) (weight_map g u1)
80 (weight_map f0 t0) (weight_map g t0) (H1 f0 g H2 H3) (weight_le t0 f0 g
81 H2)))))))) k))))))))) (\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (v:
82 T).(\forall (t2: T).(\forall (t1: T).(\forall (i: nat).((subst0 (s k0 i) v t1
83 t2) \to (((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
84 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
85 (s k0 i)) O v)) (g (s k0 i))) \to (le (weight_map f t2) (weight_map g
86 t1))))))) \to (\forall (u0: T).(\forall (f: ((nat \to nat))).(\forall (g:
87 ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map
88 f (lift (S i) O v)) (g i)) \to (le (weight_map f (THead k0 u0 t2))
89 (weight_map g (THead k0 u0 t1))))))))))))))) (\lambda (b: B).(B_ind (\lambda
90 (b0: B).(\forall (v: T).(\forall (t2: T).(\forall (t1: T).(\forall (i:
91 nat).((subst0 (s (Bind b0) i) v t1 t2) \to (((\forall (f: ((nat \to
92 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
93 \to ((lt (weight_map f (lift (S (s (Bind b0) i)) O v)) (g (s (Bind b0) i)))
94 \to (le (weight_map f t2) (weight_map g t1))))))) \to (\forall (u0:
95 T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
96 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to
97 (le (weight_map f (THead (Bind b0) u0 t2)) (weight_map g (THead (Bind b0) u0
98 t1))))))))))))))) (\lambda (v: T).(\lambda (t2: T).(\lambda (t1: T).(\lambda
99 (i: nat).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H1: ((\forall (f:
100 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
101 (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (le
102 (weight_map f t2) (weight_map g t1)))))))).(\lambda (u0: T).(\lambda (f:
103 ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m:
104 nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g
105 i))).(le_n_S (plus (weight_map f u0) (weight_map (wadd f (S (weight_map f
106 u0))) t2)) (plus (weight_map g u0) (weight_map (wadd g (S (weight_map g u0)))
107 t1)) (plus_le_compat (weight_map f u0) (weight_map g u0) (weight_map (wadd f
108 (S (weight_map f u0))) t2) (weight_map (wadd g (S (weight_map g u0))) t1)
109 (weight_le u0 f g H2) (H1 (wadd f (S (weight_map f u0))) (wadd g (S
110 (weight_map g u0))) (\lambda (m: nat).(wadd_le f g H2 (S (weight_map f u0))
111 (S (weight_map g u0)) (le_n_S (weight_map f u0) (weight_map g u0) (weight_le
112 u0 f g H2)) m)) (eq_ind nat (weight_map f (lift (S i) O v)) (\lambda (n:
113 nat).(lt n (g i))) H3 (weight_map (wadd f (S (weight_map f u0))) (lift (S (S
114 i)) O v)) (lift_weight_add_O (S (weight_map f u0)) v (S i) f))))))))))))))))
115 (\lambda (v: T).(\lambda (t2: T).(\lambda (t1: T).(\lambda (i: nat).(\lambda
116 (_: (subst0 (S i) v t1 t2)).(\lambda (H1: ((\forall (f: ((nat \to
117 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
118 \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (le (weight_map f
119 t2) (weight_map g t1)))))))).(\lambda (u0: T).(\lambda (f: ((nat \to
120 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f
121 m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g
122 i))).(le_n_S (plus (weight_map f u0) (weight_map (wadd f O) t2)) (plus
123 (weight_map g u0) (weight_map (wadd g O) t1)) (plus_le_compat (weight_map f
124 u0) (weight_map g u0) (weight_map (wadd f O) t2) (weight_map (wadd g O) t1)
125 (weight_le u0 f g H2) (H1 (wadd f O) (wadd g O) (\lambda (m: nat).(wadd_le f
126 g H2 O O (le_n O) m)) (eq_ind nat (weight_map f (lift (S i) O v)) (\lambda
127 (n: nat).(lt n (g i))) H3 (weight_map (wadd f O) (lift (S (S i)) O v))
128 (lift_weight_add_O O v (S i) f)))))))))))))))) (\lambda (v: T).(\lambda (t2:
129 T).(\lambda (t1: T).(\lambda (i: nat).(\lambda (_: (subst0 (S i) v t1
130 t2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
131 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
132 (S i)) O v)) (g (S i))) \to (le (weight_map f t2) (weight_map g
133 t1)))))))).(\lambda (u0: T).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat
134 \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H3:
135 (lt (weight_map f (lift (S i) O v)) (g i))).(le_n_S (plus (weight_map f u0)
136 (weight_map (wadd f O) t2)) (plus (weight_map g u0) (weight_map (wadd g O)
137 t1)) (plus_le_compat (weight_map f u0) (weight_map g u0) (weight_map (wadd f
138 O) t2) (weight_map (wadd g O) t1) (weight_le u0 f g H2) (H1 (wadd f O) (wadd
139 g O) (\lambda (m: nat).(wadd_le f g H2 O O (le_n O) m)) (eq_ind nat
140 (weight_map f (lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H3
141 (weight_map (wadd f O) (lift (S (S i)) O v)) (lift_weight_add_O O v (S i)
142 f)))))))))))))))) b)) (\lambda (_: F).(\lambda (v: T).(\lambda (t2:
143 T).(\lambda (t1: T).(\lambda (i: nat).(\lambda (_: (subst0 i v t1
144 t2)).(\lambda (H1: ((\forall (f0: ((nat \to nat))).(\forall (g: ((nat \to
145 nat))).(((\forall (m: nat).(le (f0 m) (g m)))) \to ((lt (weight_map f0 (lift
146 (S i) O v)) (g i)) \to (le (weight_map f0 t2) (weight_map g
147 t1)))))))).(\lambda (u0: T).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat
148 \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f0 m) (g m))))).(\lambda
149 (H3: (lt (weight_map f0 (lift (S i) O v)) (g i))).(le_n_S (plus (weight_map
150 f0 u0) (weight_map f0 t2)) (plus (weight_map g u0) (weight_map g t1))
151 (plus_le_compat (weight_map f0 u0) (weight_map g u0) (weight_map f0 t2)
152 (weight_map g t1) (weight_le u0 f0 g H2) (H1 f0 g H2 H3))))))))))))))) k))
153 (\lambda (v: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (i: nat).(\lambda
154 (_: (subst0 i v u1 u2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall
155 (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt
156 (weight_map f (lift (S i) O v)) (g i)) \to (le (weight_map f u2) (weight_map
157 g u1)))))))).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (t1:
158 T).(\forall (t2: T).((subst0 (s k0 i) v t1 t2) \to (((\forall (f: ((nat \to
159 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
160 \to ((lt (weight_map f (lift (S (s k0 i)) O v)) (g (s k0 i))) \to (le
161 (weight_map f t2) (weight_map g t1))))))) \to (\forall (f: ((nat \to
162 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
163 \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (le (weight_map f (THead
164 k0 u2 t2)) (weight_map g (THead k0 u1 t1)))))))))))) (\lambda (b: B).(B_ind
165 (\lambda (b0: B).(\forall (t1: T).(\forall (t2: T).((subst0 (s (Bind b0) i) v
166 t1 t2) \to (((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
167 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
168 (s (Bind b0) i)) O v)) (g (s (Bind b0) i))) \to (le (weight_map f t2)
169 (weight_map g t1))))))) \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat
170 \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f
171 (lift (S i) O v)) (g i)) \to (le (weight_map f (THead (Bind b0) u2 t2))
172 (weight_map g (THead (Bind b0) u1 t1)))))))))))) (\lambda (t1: T).(\lambda
173 (t2: T).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H3: ((\forall (f:
174 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
175 (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (le
176 (weight_map f t2) (weight_map g t1)))))))).(\lambda (f: ((nat \to
177 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H4: ((\forall (m: nat).(le (f
178 m) (g m))))).(\lambda (H5: (lt (weight_map f (lift (S i) O v)) (g
179 i))).(le_n_S (plus (weight_map f u2) (weight_map (wadd f (S (weight_map f
180 u2))) t2)) (plus (weight_map g u1) (weight_map (wadd g (S (weight_map g u1)))
181 t1)) (plus_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd f
182 (S (weight_map f u2))) t2) (weight_map (wadd g (S (weight_map g u1))) t1) (H1
183 f g H4 H5) (H3 (wadd f (S (weight_map f u2))) (wadd g (S (weight_map g u1)))
184 (\lambda (m: nat).(wadd_le f g H4 (S (weight_map f u2)) (S (weight_map g u1))
185 (le_n_S (weight_map f u2) (weight_map g u1) (H1 f g H4 H5)) m)) (eq_ind nat
186 (weight_map f (lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H5
187 (weight_map (wadd f (S (weight_map f u2))) (lift (S (S i)) O v))
188 (lift_weight_add_O (S (weight_map f u2)) v (S i) f))))))))))))) (\lambda (t1:
189 T).(\lambda (t2: T).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H3:
190 ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
191 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S
192 i))) \to (le (weight_map f t2) (weight_map g t1)))))))).(\lambda (f: ((nat
193 \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H4: ((\forall (m: nat).(le
194 (f m) (g m))))).(\lambda (H5: (lt (weight_map f (lift (S i) O v)) (g
195 i))).(le_n_S (plus (weight_map f u2) (weight_map (wadd f O) t2)) (plus
196 (weight_map g u1) (weight_map (wadd g O) t1)) (plus_le_compat (weight_map f
197 u2) (weight_map g u1) (weight_map (wadd f O) t2) (weight_map (wadd g O) t1)
198 (H1 f g H4 H5) (H3 (wadd f O) (wadd g O) (\lambda (m: nat).(wadd_le f g H4 O
199 O (le_n O) m)) (eq_ind nat (weight_map f (lift (S i) O v)) (\lambda (n:
200 nat).(lt n (g i))) H5 (weight_map (wadd f O) (lift (S (S i)) O v))
201 (lift_weight_add_O O v (S i) f))))))))))))) (\lambda (t1: T).(\lambda (t2:
202 T).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H3: ((\forall (f: ((nat \to
203 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
204 \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (le (weight_map f
205 t2) (weight_map g t1)))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat
206 \to nat))).(\lambda (H4: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H5:
207 (lt (weight_map f (lift (S i) O v)) (g i))).(le_n_S (plus (weight_map f u2)
208 (weight_map (wadd f O) t2)) (plus (weight_map g u1) (weight_map (wadd g O)
209 t1)) (plus_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd f
210 O) t2) (weight_map (wadd g O) t1) (H1 f g H4 H5) (H3 (wadd f O) (wadd g O)
211 (\lambda (m: nat).(wadd_le f g H4 O O (le_n O) m)) (eq_ind nat (weight_map f
212 (lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H5 (weight_map (wadd f O)
213 (lift (S (S i)) O v)) (lift_weight_add_O O v (S i) f))))))))))))) b))
214 (\lambda (_: F).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (subst0 i v t1
215 t2)).(\lambda (H3: ((\forall (f0: ((nat \to nat))).(\forall (g: ((nat \to
216 nat))).(((\forall (m: nat).(le (f0 m) (g m)))) \to ((lt (weight_map f0 (lift
217 (S i) O v)) (g i)) \to (le (weight_map f0 t2) (weight_map g
218 t1)))))))).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat \to
219 nat))).(\lambda (H4: ((\forall (m: nat).(le (f0 m) (g m))))).(\lambda (H5:
220 (lt (weight_map f0 (lift (S i) O v)) (g i))).(le_n_S (plus (weight_map f0 u2)
221 (weight_map f0 t2)) (plus (weight_map g u1) (weight_map g t1))
222 (plus_le_compat (weight_map f0 u2) (weight_map g u1) (weight_map f0 t2)
223 (weight_map g t1) (H1 f0 g H4 H5) (H3 f0 g H4 H5)))))))))))) k)))))))) d u t
226 theorem subst0_weight_lt:
227 \forall (u: T).(\forall (t: T).(\forall (z: T).(\forall (d: nat).((subst0 d
228 u t z) \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
229 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
230 d) O u)) (g d)) \to (lt (weight_map f z) (weight_map g t))))))))))
232 \lambda (u: T).(\lambda (t: T).(\lambda (z: T).(\lambda (d: nat).(\lambda
233 (H: (subst0 d u t z)).(subst0_ind (\lambda (n: nat).(\lambda (t0: T).(\lambda
234 (t1: T).(\lambda (t2: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
235 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
236 n) O t0)) (g n)) \to (lt (weight_map f t2) (weight_map g t1))))))))))
237 (\lambda (v: T).(\lambda (i: nat).(\lambda (f: ((nat \to nat))).(\lambda (g:
238 ((nat \to nat))).(\lambda (_: ((\forall (m: nat).(le (f m) (g m))))).(\lambda
239 (H1: (lt (weight_map f (lift (S i) O v)) (g i))).H1)))))) (\lambda (v:
240 T).(\lambda (u2: T).(\lambda (u1: T).(\lambda (i: nat).(\lambda (_: (subst0 i
241 v u1 u2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
242 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
243 i) O v)) (g i)) \to (lt (weight_map f u2) (weight_map g u1)))))))).(\lambda
244 (t0: T).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (f: ((nat \to
245 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
246 \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (lt (weight_map f (THead
247 k0 u2 t0)) (weight_map g (THead k0 u1 t0)))))))) (\lambda (b: B).(B_ind
248 (\lambda (b0: B).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
249 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
250 i) O v)) (g i)) \to (lt (weight_map f (THead (Bind b0) u2 t0)) (weight_map g
251 (THead (Bind b0) u1 t0)))))))) (\lambda (f: ((nat \to nat))).(\lambda (g:
252 ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f m) (g
253 m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g i))).(lt_n_S
254 (plus (weight_map f u2) (weight_map (wadd f (S (weight_map f u2))) t0)) (plus
255 (weight_map g u1) (weight_map (wadd g (S (weight_map g u1))) t0))
256 (plus_lt_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd f (S
257 (weight_map f u2))) t0) (weight_map (wadd g (S (weight_map g u1))) t0) (H1 f
258 g H2 H3) (weight_le t0 (wadd f (S (weight_map f u2))) (wadd g (S (weight_map
259 g u1))) (\lambda (n: nat).(wadd_lt f g H2 (S (weight_map f u2)) (S
260 (weight_map g u1)) (lt_n_S (weight_map f u2) (weight_map g u1) (H1 f g H2
261 H3)) n))))))))) (\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
262 nat))).(\lambda (H2: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H3: (lt
263 (weight_map f (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map f u2)
264 (weight_map (wadd f O) t0)) (plus (weight_map g u1) (weight_map (wadd g O)
265 t0)) (plus_lt_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd
266 f O) t0) (weight_map (wadd g O) t0) (H1 f g H2 H3) (weight_le t0 (wadd f O)
267 (wadd g O) (\lambda (n: nat).(le_S_n (wadd f O n) (wadd g O n) (le_n_S (wadd
268 f O n) (wadd g O n) (wadd_le f g H2 O O (le_n O) n))))))))))) (\lambda (f:
269 ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m:
270 nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g
271 i))).(lt_n_S (plus (weight_map f u2) (weight_map (wadd f O) t0)) (plus
272 (weight_map g u1) (weight_map (wadd g O) t0)) (plus_lt_le_compat (weight_map
273 f u2) (weight_map g u1) (weight_map (wadd f O) t0) (weight_map (wadd g O) t0)
274 (H1 f g H2 H3) (weight_le t0 (wadd f O) (wadd g O) (\lambda (n: nat).(le_S_n
275 (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
276 O (le_n O) n))))))))))) b)) (\lambda (_: F).(\lambda (f0: ((nat \to
277 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f0
278 m) (g m))))).(\lambda (H3: (lt (weight_map f0 (lift (S i) O v)) (g
279 i))).(lt_n_S (plus (weight_map f0 u2) (weight_map f0 t0)) (plus (weight_map g
280 u1) (weight_map g t0)) (plus_lt_le_compat (weight_map f0 u2) (weight_map g
281 u1) (weight_map f0 t0) (weight_map g t0) (H1 f0 g H2 H3) (weight_le t0 f0 g
282 H2)))))))) k))))))))) (\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (v:
283 T).(\forall (t2: T).(\forall (t1: T).(\forall (i: nat).((subst0 (s k0 i) v t1
284 t2) \to (((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
285 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
286 (s k0 i)) O v)) (g (s k0 i))) \to (lt (weight_map f t2) (weight_map g
287 t1))))))) \to (\forall (u0: T).(\forall (f: ((nat \to nat))).(\forall (g:
288 ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map
289 f (lift (S i) O v)) (g i)) \to (lt (weight_map f (THead k0 u0 t2))
290 (weight_map g (THead k0 u0 t1))))))))))))))) (\lambda (b: B).(B_ind (\lambda
291 (b0: B).(\forall (v: T).(\forall (t2: T).(\forall (t1: T).(\forall (i:
292 nat).((subst0 (s (Bind b0) i) v t1 t2) \to (((\forall (f: ((nat \to
293 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
294 \to ((lt (weight_map f (lift (S (s (Bind b0) i)) O v)) (g (s (Bind b0) i)))
295 \to (lt (weight_map f t2) (weight_map g t1))))))) \to (\forall (u0:
296 T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
297 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to
298 (lt (weight_map f (THead (Bind b0) u0 t2)) (weight_map g (THead (Bind b0) u0
299 t1))))))))))))))) (\lambda (v: T).(\lambda (t2: T).(\lambda (t1: T).(\lambda
300 (i: nat).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H1: ((\forall (f:
301 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
302 (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (lt
303 (weight_map f t2) (weight_map g t1)))))))).(\lambda (u0: T).(\lambda (f:
304 ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m:
305 nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g
306 i))).(lt_n_S (plus (weight_map f u0) (weight_map (wadd f (S (weight_map f
307 u0))) t2)) (plus (weight_map g u0) (weight_map (wadd g (S (weight_map g u0)))
308 t1)) (plus_le_lt_compat (weight_map f u0) (weight_map g u0) (weight_map (wadd
309 f (S (weight_map f u0))) t2) (weight_map (wadd g (S (weight_map g u0))) t1)
310 (weight_le u0 f g H2) (H1 (wadd f (S (weight_map f u0))) (wadd g (S
311 (weight_map g u0))) (\lambda (m: nat).(wadd_le f g H2 (S (weight_map f u0))
312 (S (weight_map g u0)) (le_n_S (weight_map f u0) (weight_map g u0) (weight_le
313 u0 f g H2)) m)) (eq_ind nat (weight_map f (lift (S i) O v)) (\lambda (n:
314 nat).(lt n (g i))) H3 (weight_map (wadd f (S (weight_map f u0))) (lift (S (S
315 i)) O v)) (lift_weight_add_O (S (weight_map f u0)) v (S i) f))))))))))))))))
316 (\lambda (v: T).(\lambda (t2: T).(\lambda (t1: T).(\lambda (i: nat).(\lambda
317 (_: (subst0 (S i) v t1 t2)).(\lambda (H1: ((\forall (f: ((nat \to
318 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
319 \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (lt (weight_map f
320 t2) (weight_map g t1)))))))).(\lambda (u0: T).(\lambda (f: ((nat \to
321 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f
322 m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g
323 i))).(lt_n_S (plus (weight_map f u0) (weight_map (wadd f O) t2)) (plus
324 (weight_map g u0) (weight_map (wadd g O) t1)) (plus_le_lt_compat (weight_map
325 f u0) (weight_map g u0) (weight_map (wadd f O) t2) (weight_map (wadd g O) t1)
326 (weight_le u0 f g H2) (H1 (wadd f O) (wadd g O) (\lambda (m: nat).(wadd_le f
327 g H2 O O (le_n O) m)) (eq_ind nat (weight_map f (lift (S i) O v)) (\lambda
328 (n: nat).(lt n (g i))) H3 (weight_map (wadd f O) (lift (S (S i)) O v))
329 (lift_weight_add_O O v (S i) f)))))))))))))))) (\lambda (v: T).(\lambda (t2:
330 T).(\lambda (t1: T).(\lambda (i: nat).(\lambda (_: (subst0 (S i) v t1
331 t2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
332 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
333 (S i)) O v)) (g (S i))) \to (lt (weight_map f t2) (weight_map g
334 t1)))))))).(\lambda (u0: T).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat
335 \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H3:
336 (lt (weight_map f (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map f u0)
337 (weight_map (wadd f O) t2)) (plus (weight_map g u0) (weight_map (wadd g O)
338 t1)) (plus_le_lt_compat (weight_map f u0) (weight_map g u0) (weight_map (wadd
339 f O) t2) (weight_map (wadd g O) t1) (weight_le u0 f g H2) (H1 (wadd f O)
340 (wadd g O) (\lambda (m: nat).(wadd_le f g H2 O O (le_n O) m)) (eq_ind nat
341 (weight_map f (lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H3
342 (weight_map (wadd f O) (lift (S (S i)) O v)) (lift_weight_add_O O v (S i)
343 f)))))))))))))))) b)) (\lambda (_: F).(\lambda (v: T).(\lambda (t2:
344 T).(\lambda (t1: T).(\lambda (i: nat).(\lambda (_: (subst0 i v t1
345 t2)).(\lambda (H1: ((\forall (f0: ((nat \to nat))).(\forall (g: ((nat \to
346 nat))).(((\forall (m: nat).(le (f0 m) (g m)))) \to ((lt (weight_map f0 (lift
347 (S i) O v)) (g i)) \to (lt (weight_map f0 t2) (weight_map g
348 t1)))))))).(\lambda (u0: T).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat
349 \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f0 m) (g m))))).(\lambda
350 (H3: (lt (weight_map f0 (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map
351 f0 u0) (weight_map f0 t2)) (plus (weight_map g u0) (weight_map g t1))
352 (plus_le_lt_compat (weight_map f0 u0) (weight_map g u0) (weight_map f0 t2)
353 (weight_map g t1) (weight_le u0 f0 g H2) (H1 f0 g H2 H3))))))))))))))) k))
354 (\lambda (v: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (i: nat).(\lambda
355 (_: (subst0 i v u1 u2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall
356 (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt
357 (weight_map f (lift (S i) O v)) (g i)) \to (lt (weight_map f u2) (weight_map
358 g u1)))))))).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (t1:
359 T).(\forall (t2: T).((subst0 (s k0 i) v t1 t2) \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 (s k0 i)) O v)) (g (s k0 i))) \to (lt
362 (weight_map f t2) (weight_map g t1))))))) \to (\forall (f: ((nat \to
363 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
364 \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (lt (weight_map f (THead
365 k0 u2 t2)) (weight_map g (THead k0 u1 t1)))))))))))) (\lambda (b: B).(B_ind
366 (\lambda (b0: B).(\forall (t1: T).(\forall (t2: T).((subst0 (s (Bind b0) i) v
367 t1 t2) \to (((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
368 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
369 (s (Bind b0) i)) O v)) (g (s (Bind b0) i))) \to (lt (weight_map f t2)
370 (weight_map g t1))))))) \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat
371 \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f
372 (lift (S i) O v)) (g i)) \to (lt (weight_map f (THead (Bind b0) u2 t2))
373 (weight_map g (THead (Bind b0) u1 t1)))))))))))) (\lambda (t1: T).(\lambda
374 (t2: T).(\lambda (H2: (subst0 (S i) v t1 t2)).(\lambda (_: ((\forall (f:
375 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
376 (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (lt
377 (weight_map f t2) (weight_map g t1)))))))).(\lambda (f: ((nat \to
378 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H4: ((\forall (m: nat).(le (f
379 m) (g m))))).(\lambda (H5: (lt (weight_map f (lift (S i) O v)) (g
380 i))).(lt_n_S (plus (weight_map f u2) (weight_map (wadd f (S (weight_map f
381 u2))) t2)) (plus (weight_map g u1) (weight_map (wadd g (S (weight_map g u1)))
382 t1)) (plus_lt_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd
383 f (S (weight_map f u2))) t2) (weight_map (wadd g (S (weight_map g u1))) t1)
384 (H1 f g H4 H5) (subst0_weight_le v t1 t2 (S i) H2 (wadd f (S (weight_map f
385 u2))) (wadd g (S (weight_map g u1))) (\lambda (m: nat).(wadd_lt f g H4 (S
386 (weight_map f u2)) (S (weight_map g u1)) (lt_n_S (weight_map f u2)
387 (weight_map g u1) (H1 f g H4 H5)) m)) (eq_ind nat (weight_map f (lift (S i) O
388 v)) (\lambda (n: nat).(lt n (g i))) H5 (weight_map (wadd f (S (weight_map f
389 u2))) (lift (S (S i)) O v)) (lift_weight_add_O (S (weight_map f u2)) v (S i)
390 f))))))))))))) (\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (subst0 (S i) v
391 t1 t2)).(\lambda (H3: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
392 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
393 (S i)) O v)) (g (S i))) \to (lt (weight_map f t2) (weight_map g
394 t1)))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
395 nat))).(\lambda (H4: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H5: (lt
396 (weight_map f (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map f u2)
397 (weight_map (wadd f O) t2)) (plus (weight_map g u1) (weight_map (wadd g O)
398 t1)) (plus_lt_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd f
399 O) t2) (weight_map (wadd g O) t1) (H1 f g H4 H5) (H3 (wadd f O) (wadd g O)
400 (\lambda (m: nat).(le_S_n (wadd f O m) (wadd g O m) (le_n_S (wadd f O m)
401 (wadd g O m) (wadd_le f g H4 O O (le_n O) m)))) (eq_ind nat (weight_map f
402 (lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H5 (weight_map (wadd f O)
403 (lift (S (S i)) O v)) (lift_weight_add_O O v (S i) f))))))))))))) (\lambda
404 (t1: T).(\lambda (t2: T).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H3:
405 ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
406 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S
407 i))) \to (lt (weight_map f t2) (weight_map g t1)))))))).(\lambda (f: ((nat
408 \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H4: ((\forall (m: nat).(le
409 (f m) (g m))))).(\lambda (H5: (lt (weight_map f (lift (S i) O v)) (g
410 i))).(lt_n_S (plus (weight_map f u2) (weight_map (wadd f O) t2)) (plus
411 (weight_map g u1) (weight_map (wadd g O) t1)) (plus_lt_compat (weight_map f
412 u2) (weight_map g u1) (weight_map (wadd f O) t2) (weight_map (wadd g O) t1)
413 (H1 f g H4 H5) (H3 (wadd f O) (wadd g O) (\lambda (m: nat).(le_S_n (wadd f O
414 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
415 O) m)))) (eq_ind nat (weight_map f (lift (S i) O v)) (\lambda (n: nat).(lt n
416 (g i))) H5 (weight_map (wadd f O) (lift (S (S i)) O v)) (lift_weight_add_O O
417 v (S i) f))))))))))))) b)) (\lambda (_: F).(\lambda (t1: T).(\lambda (t2:
418 T).(\lambda (_: (subst0 i v t1 t2)).(\lambda (H3: ((\forall (f0: ((nat \to
419 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f0 m) (g m))))
420 \to ((lt (weight_map f0 (lift (S i) O v)) (g i)) \to (lt (weight_map f0 t2)
421 (weight_map g t1)))))))).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat
422 \to nat))).(\lambda (H4: ((\forall (m: nat).(le (f0 m) (g m))))).(\lambda
423 (H5: (lt (weight_map f0 (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map
424 f0 u2) (weight_map f0 t2)) (plus (weight_map g u1) (weight_map g t1))
425 (plus_lt_compat (weight_map f0 u2) (weight_map g u1) (weight_map f0 t2)
426 (weight_map g t1) (H1 f0 g H4 H5) (H3 f0 g H4 H5)))))))))))) k)))))))) d u t
429 theorem subst0_tlt_head:
430 \forall (u: T).(\forall (t: T).(\forall (z: T).((subst0 O u t z) \to (tlt
431 (THead (Bind Abbr) u z) (THead (Bind Abbr) u t)))))
433 \lambda (u: T).(\lambda (t: T).(\lambda (z: T).(\lambda (H: (subst0 O u t
434 z)).(lt_n_S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
435 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) z)) (plus
436 (weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S
437 (weight_map (\lambda (_: nat).O) u))) t)) (plus_le_lt_compat (weight_map
438 (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
439 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) z) (weight_map
440 (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t) (le_n
441 (weight_map (\lambda (_: nat).O) u)) (subst0_weight_lt u t z O H (wadd
442 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) (wadd (\lambda
443 (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) (\lambda (m: nat).(le_n
444 (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u)) m)))
445 (eq_ind nat (weight_map (\lambda (_: nat).O) (lift O O u)) (\lambda (n:
446 nat).(lt n (S (weight_map (\lambda (_: nat).O) u)))) (eq_ind_r T u (\lambda
447 (t0: T).(lt (weight_map (\lambda (_: nat).O) t0) (S (weight_map (\lambda (_:
448 nat).O) u)))) (le_n (S (weight_map (\lambda (_: nat).O) u))) (lift O O u)
449 (lift_r u O)) (weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda
450 (_: nat).O) u))) (lift (S O) O u)) (lift_weight_add_O (S (weight_map (\lambda
451 (_: nat).O) u)) u O (\lambda (_: nat).O))))))))).
454 \forall (u: T).(\forall (t: T).(\forall (z: T).((subst0 O u t z) \to (tlt z
455 (THead (Bind Abbr) u t)))))
457 \lambda (u: T).(\lambda (t: T).(\lambda (z: T).(\lambda (H: (subst0 O u t
458 z)).(tlt_trans (THead (Bind Abbr) u z) z (THead (Bind Abbr) u t) (tlt_head_dx
459 (Bind Abbr) u z) (subst0_tlt_head u t z H))))).
projects / helm.git / blob