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/subst0/defs.ma".
19 include "LambdaDelta-1/lift/props.ma".
21 include "LambdaDelta-1/lift/tlt.ma".
23 theorem subst0_weight_le:
24 \forall (u: T).(\forall (t: T).(\forall (z: T).(\forall (d: nat).((subst0 d
25 u t z) \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
26 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
27 d) O u)) (g d)) \to (le (weight_map f z) (weight_map g t))))))))))
29 \lambda (u: T).(\lambda (t: T).(\lambda (z: T).(\lambda (d: nat).(\lambda
30 (H: (subst0 d u t z)).(subst0_ind (\lambda (n: nat).(\lambda (t0: T).(\lambda
31 (t1: T).(\lambda (t2: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
32 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
33 n) O t0)) (g n)) \to (le (weight_map f t2) (weight_map g t1))))))))))
34 (\lambda (v: T).(\lambda (i: nat).(\lambda (f: ((nat \to nat))).(\lambda (g:
35 ((nat \to nat))).(\lambda (_: ((\forall (m: nat).(le (f m) (g m))))).(\lambda
36 (H1: (lt (weight_map f (lift (S i) O v)) (g i))).(le_S_n (weight_map f (lift
37 (S i) O v)) (weight_map g (TLRef i)) (le_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_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_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_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_n O) m)) (eq_ind nat (weight_map
138 f (lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H3 (weight_map (wadd f O)
139 (lift (S (S i)) O v)) (lift_weight_add_O O v (S i) f)))))))))))))))) b))
140 (\lambda (_: F).(\lambda (v: T).(\lambda (t2: T).(\lambda (t1: T).(\lambda
141 (i: nat).(\lambda (_: (subst0 i v t1 t2)).(\lambda (H1: ((\forall (f0: ((nat
142 \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f0 m) (g
143 m)))) \to ((lt (weight_map f0 (lift (S i) O v)) (g i)) \to (le (weight_map f0
144 t2) (weight_map g t1)))))))).(\lambda (u0: T).(\lambda (f0: ((nat \to
145 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f0
146 m) (g m))))).(\lambda (H3: (lt (weight_map f0 (lift (S i) O v)) (g
147 i))).(le_n_S (plus (weight_map f0 u0) (weight_map f0 t2)) (plus (weight_map g
148 u0) (weight_map g t1)) (le_plus_plus (weight_map f0 u0) (weight_map g u0)
149 (weight_map f0 t2) (weight_map g t1) (weight_le u0 f0 g H2) (H1 f0 g H2
150 H3))))))))))))))) k)) (\lambda (v: T).(\lambda (u1: T).(\lambda (u2:
151 T).(\lambda (i: nat).(\lambda (_: (subst0 i v u1 u2)).(\lambda (H1: ((\forall
152 (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f
153 m) (g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (le
154 (weight_map f u2) (weight_map g u1)))))))).(\lambda (k: K).(K_ind (\lambda
155 (k0: K).(\forall (t1: T).(\forall (t2: T).((subst0 (s k0 i) v t1 t2) \to
156 (((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
157 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S (s k0 i)) O v)) (g (s
158 k0 i))) \to (le (weight_map f t2) (weight_map g t1))))))) \to (\forall (f:
159 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
160 (g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (le (weight_map
161 f (THead k0 u2 t2)) (weight_map g (THead k0 u1 t1)))))))))))) (\lambda (b:
162 B).(B_ind (\lambda (b0: B).(\forall (t1: T).(\forall (t2: T).((subst0 (s
163 (Bind b0) i) v t1 t2) \to (((\forall (f: ((nat \to nat))).(\forall (g: ((nat
164 \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f
165 (lift (S (s (Bind b0) i)) O v)) (g (s (Bind b0) i))) \to (le (weight_map f
166 t2) (weight_map g t1))))))) \to (\forall (f: ((nat \to nat))).(\forall (g:
167 ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map
168 f (lift (S i) O v)) (g i)) \to (le (weight_map f (THead (Bind b0) u2 t2))
169 (weight_map g (THead (Bind b0) u1 t1)))))))))))) (\lambda (t1: T).(\lambda
170 (t2: T).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H3: ((\forall (f:
171 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
172 (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (le
173 (weight_map f t2) (weight_map g t1)))))))).(\lambda (f: ((nat \to
174 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H4: ((\forall (m: nat).(le (f
175 m) (g m))))).(\lambda (H5: (lt (weight_map f (lift (S i) O v)) (g
176 i))).(le_n_S (plus (weight_map f u2) (weight_map (wadd f (S (weight_map f
177 u2))) t2)) (plus (weight_map g u1) (weight_map (wadd g (S (weight_map g u1)))
178 t1)) (le_plus_plus (weight_map f u2) (weight_map g u1) (weight_map (wadd f (S
179 (weight_map f u2))) t2) (weight_map (wadd g (S (weight_map g u1))) t1) (H1 f
180 g H4 H5) (H3 (wadd f (S (weight_map f u2))) (wadd g (S (weight_map g u1)))
181 (\lambda (m: nat).(wadd_le f g H4 (S (weight_map f u2)) (S (weight_map g u1))
182 (le_n_S (weight_map f u2) (weight_map g u1) (H1 f g H4 H5)) m)) (eq_ind nat
183 (weight_map f (lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H5
184 (weight_map (wadd f (S (weight_map f u2))) (lift (S (S i)) O v))
185 (lift_weight_add_O (S (weight_map f u2)) v (S i) f))))))))))))) (\lambda (t1:
186 T).(\lambda (t2: T).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H3:
187 ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
188 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S
189 i))) \to (le (weight_map f t2) (weight_map g t1)))))))).(\lambda (f: ((nat
190 \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H4: ((\forall (m: nat).(le
191 (f m) (g m))))).(\lambda (H5: (lt (weight_map f (lift (S i) O v)) (g
192 i))).(le_n_S (plus (weight_map f u2) (weight_map (wadd f O) t2)) (plus
193 (weight_map g u1) (weight_map (wadd g O) t1)) (le_plus_plus (weight_map f u2)
194 (weight_map g u1) (weight_map (wadd f O) t2) (weight_map (wadd g O) t1) (H1 f
195 g H4 H5) (H3 (wadd f O) (wadd g O) (\lambda (m: nat).(wadd_le f g H4 O O
196 (le_n O) m)) (eq_ind nat (weight_map f (lift (S i) O v)) (\lambda (n:
197 nat).(lt n (g i))) H5 (weight_map (wadd f O) (lift (S (S i)) O v))
198 (lift_weight_add_O O v (S i) f))))))))))))) (\lambda (t1: T).(\lambda (t2:
199 T).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H3: ((\forall (f: ((nat \to
200 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
201 \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (le (weight_map f
202 t2) (weight_map g t1)))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat
203 \to nat))).(\lambda (H4: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H5:
204 (lt (weight_map f (lift (S i) O v)) (g i))).(le_n_S (plus (weight_map f u2)
205 (weight_map (wadd f O) t2)) (plus (weight_map g u1) (weight_map (wadd g O)
206 t1)) (le_plus_plus (weight_map f u2) (weight_map g u1) (weight_map (wadd f O)
207 t2) (weight_map (wadd g O) t1) (H1 f g H4 H5) (H3 (wadd f O) (wadd g O)
208 (\lambda (m: nat).(wadd_le f g H4 O O (le_n O) m)) (eq_ind nat (weight_map f
209 (lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H5 (weight_map (wadd f O)
210 (lift (S (S i)) O v)) (lift_weight_add_O O v (S i) f))))))))))))) b))
211 (\lambda (_: F).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (subst0 i v t1
212 t2)).(\lambda (H3: ((\forall (f0: ((nat \to nat))).(\forall (g: ((nat \to
213 nat))).(((\forall (m: nat).(le (f0 m) (g m)))) \to ((lt (weight_map f0 (lift
214 (S i) O v)) (g i)) \to (le (weight_map f0 t2) (weight_map g
215 t1)))))))).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat \to
216 nat))).(\lambda (H4: ((\forall (m: nat).(le (f0 m) (g m))))).(\lambda (H5:
217 (lt (weight_map f0 (lift (S i) O v)) (g i))).(le_n_S (plus (weight_map f0 u2)
218 (weight_map f0 t2)) (plus (weight_map g u1) (weight_map g t1)) (le_plus_plus
219 (weight_map f0 u2) (weight_map g u1) (weight_map f0 t2) (weight_map g t1) (H1
220 f0 g H4 H5) (H3 f0 g H4 H5)))))))))))) k)))))))) d u t z H))))).
222 theorem subst0_weight_lt:
223 \forall (u: T).(\forall (t: T).(\forall (z: T).(\forall (d: nat).((subst0 d
224 u t z) \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
225 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
226 d) O u)) (g d)) \to (lt (weight_map f z) (weight_map g t))))))))))
228 \lambda (u: T).(\lambda (t: T).(\lambda (z: T).(\lambda (d: nat).(\lambda
229 (H: (subst0 d u t z)).(subst0_ind (\lambda (n: nat).(\lambda (t0: T).(\lambda
230 (t1: T).(\lambda (t2: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
231 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
232 n) O t0)) (g n)) \to (lt (weight_map f t2) (weight_map g t1))))))))))
233 (\lambda (v: T).(\lambda (i: nat).(\lambda (f: ((nat \to nat))).(\lambda (g:
234 ((nat \to nat))).(\lambda (_: ((\forall (m: nat).(le (f m) (g m))))).(\lambda
235 (H1: (lt (weight_map f (lift (S i) O v)) (g i))).H1)))))) (\lambda (v:
236 T).(\lambda (u2: T).(\lambda (u1: T).(\lambda (i: nat).(\lambda (_: (subst0 i
237 v u1 u2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
238 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
239 i) O v)) (g i)) \to (lt (weight_map f u2) (weight_map g u1)))))))).(\lambda
240 (t0: T).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (f: ((nat \to
241 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
242 \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (lt (weight_map f (THead
243 k0 u2 t0)) (weight_map g (THead k0 u1 t0)))))))) (\lambda (b: B).(B_ind
244 (\lambda (b0: B).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
245 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
246 i) O v)) (g i)) \to (lt (weight_map f (THead (Bind b0) u2 t0)) (weight_map g
247 (THead (Bind b0) u1 t0)))))))) (\lambda (f: ((nat \to nat))).(\lambda (g:
248 ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f m) (g
249 m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g i))).(lt_n_S
250 (plus (weight_map f u2) (weight_map (wadd f (S (weight_map f u2))) t0)) (plus
251 (weight_map g u1) (weight_map (wadd g (S (weight_map g u1))) t0))
252 (lt_le_plus_plus (weight_map f u2) (weight_map g u1) (weight_map (wadd f (S
253 (weight_map f u2))) t0) (weight_map (wadd g (S (weight_map g u1))) t0) (H1 f
254 g H2 H3) (weight_le t0 (wadd f (S (weight_map f u2))) (wadd g (S (weight_map
255 g u1))) (\lambda (n: nat).(wadd_lt f g H2 (S (weight_map f u2)) (S
256 (weight_map g u1)) (lt_n_S (weight_map f u2) (weight_map g u1) (H1 f g H2
257 H3)) n))))))))) (\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
258 nat))).(\lambda (H2: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H3: (lt
259 (weight_map f (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map f u2)
260 (weight_map (wadd f O) t0)) (plus (weight_map g u1) (weight_map (wadd g O)
261 t0)) (lt_le_plus_plus (weight_map f u2) (weight_map g u1) (weight_map (wadd f
262 O) t0) (weight_map (wadd g O) t0) (H1 f g H2 H3) (weight_le t0 (wadd f O)
263 (wadd g O) (\lambda (n: nat).(le_S_n (wadd f O n) (wadd g O n) (le_n_S (wadd
264 f O n) (wadd g O n) (wadd_le f g H2 O O (le_n O) n))))))))))) (\lambda (f:
265 ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m:
266 nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g
267 i))).(lt_n_S (plus (weight_map f u2) (weight_map (wadd f O) t0)) (plus
268 (weight_map g u1) (weight_map (wadd g O) t0)) (lt_le_plus_plus (weight_map f
269 u2) (weight_map g u1) (weight_map (wadd f O) t0) (weight_map (wadd g O) t0)
270 (H1 f g H2 H3) (weight_le t0 (wadd f O) (wadd g O) (\lambda (n: nat).(le_S_n
271 (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
272 O (le_n O) n))))))))))) b)) (\lambda (_: F).(\lambda (f0: ((nat \to
273 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f0
274 m) (g m))))).(\lambda (H3: (lt (weight_map f0 (lift (S i) O v)) (g
275 i))).(lt_n_S (plus (weight_map f0 u2) (weight_map f0 t0)) (plus (weight_map g
276 u1) (weight_map g t0)) (lt_le_plus_plus (weight_map f0 u2) (weight_map g u1)
277 (weight_map f0 t0) (weight_map g t0) (H1 f0 g H2 H3) (weight_le t0 f0 g
278 H2)))))))) k))))))))) (\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (v:
279 T).(\forall (t2: T).(\forall (t1: T).(\forall (i: nat).((subst0 (s k0 i) v t1
280 t2) \to (((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
281 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
282 (s k0 i)) O v)) (g (s k0 i))) \to (lt (weight_map f t2) (weight_map g
283 t1))))))) \to (\forall (u0: T).(\forall (f: ((nat \to nat))).(\forall (g:
284 ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map
285 f (lift (S i) O v)) (g i)) \to (lt (weight_map f (THead k0 u0 t2))
286 (weight_map g (THead k0 u0 t1))))))))))))))) (\lambda (b: B).(B_ind (\lambda
287 (b0: B).(\forall (v: T).(\forall (t2: T).(\forall (t1: T).(\forall (i:
288 nat).((subst0 (s (Bind b0) i) v t1 t2) \to (((\forall (f: ((nat \to
289 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
290 \to ((lt (weight_map f (lift (S (s (Bind b0) i)) O v)) (g (s (Bind b0) i)))
291 \to (lt (weight_map f t2) (weight_map g t1))))))) \to (\forall (u0:
292 T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
293 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to
294 (lt (weight_map f (THead (Bind b0) u0 t2)) (weight_map g (THead (Bind b0) u0
295 t1))))))))))))))) (\lambda (v: T).(\lambda (t2: T).(\lambda (t1: T).(\lambda
296 (i: nat).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H1: ((\forall (f:
297 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
298 (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (lt
299 (weight_map f t2) (weight_map g t1)))))))).(\lambda (u0: T).(\lambda (f:
300 ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m:
301 nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g
302 i))).(lt_n_S (plus (weight_map f u0) (weight_map (wadd f (S (weight_map f
303 u0))) t2)) (plus (weight_map g u0) (weight_map (wadd g (S (weight_map g u0)))
304 t1)) (le_lt_plus_plus (weight_map f u0) (weight_map g u0) (weight_map (wadd f
305 (S (weight_map f u0))) t2) (weight_map (wadd g (S (weight_map g u0))) t1)
306 (weight_le u0 f g H2) (H1 (wadd f (S (weight_map f u0))) (wadd g (S
307 (weight_map g u0))) (\lambda (m: nat).(wadd_le f g H2 (S (weight_map f u0))
308 (S (weight_map g u0)) (le_n_S (weight_map f u0) (weight_map g u0) (weight_le
309 u0 f g H2)) m)) (eq_ind nat (weight_map f (lift (S i) O v)) (\lambda (n:
310 nat).(lt n (g i))) H3 (weight_map (wadd f (S (weight_map f u0))) (lift (S (S
311 i)) O v)) (lift_weight_add_O (S (weight_map f u0)) v (S i) f))))))))))))))))
312 (\lambda (v: T).(\lambda (t2: T).(\lambda (t1: T).(\lambda (i: nat).(\lambda
313 (_: (subst0 (S i) v t1 t2)).(\lambda (H1: ((\forall (f: ((nat \to
314 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
315 \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (lt (weight_map f
316 t2) (weight_map g t1)))))))).(\lambda (u0: T).(\lambda (f: ((nat \to
317 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f
318 m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g
319 i))).(lt_n_S (plus (weight_map f u0) (weight_map (wadd f O) t2)) (plus
320 (weight_map g u0) (weight_map (wadd g O) t1)) (le_lt_plus_plus (weight_map f
321 u0) (weight_map g u0) (weight_map (wadd f O) t2) (weight_map (wadd g O) t1)
322 (weight_le u0 f g H2) (H1 (wadd f O) (wadd g O) (\lambda (m: nat).(wadd_le f
323 g H2 O O (le_n O) m)) (eq_ind nat (weight_map f (lift (S i) O v)) (\lambda
324 (n: nat).(lt n (g i))) H3 (weight_map (wadd f O) (lift (S (S i)) O v))
325 (lift_weight_add_O O v (S i) f)))))))))))))))) (\lambda (v: T).(\lambda (t2:
326 T).(\lambda (t1: T).(\lambda (i: nat).(\lambda (_: (subst0 (S i) v t1
327 t2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
328 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
329 (S i)) O v)) (g (S i))) \to (lt (weight_map f t2) (weight_map g
330 t1)))))))).(\lambda (u0: T).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat
331 \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H3:
332 (lt (weight_map f (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map f u0)
333 (weight_map (wadd f O) t2)) (plus (weight_map g u0) (weight_map (wadd g O)
334 t1)) (le_lt_plus_plus (weight_map f u0) (weight_map g u0) (weight_map (wadd f
335 O) t2) (weight_map (wadd g O) t1) (weight_le u0 f g H2) (H1 (wadd f O) (wadd
336 g O) (\lambda (m: nat).(wadd_le f g H2 O O (le_n O) m)) (eq_ind nat
337 (weight_map f (lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H3
338 (weight_map (wadd f O) (lift (S (S i)) O v)) (lift_weight_add_O O v (S i)
339 f)))))))))))))))) b)) (\lambda (_: F).(\lambda (v: T).(\lambda (t2:
340 T).(\lambda (t1: T).(\lambda (i: nat).(\lambda (_: (subst0 i v t1
341 t2)).(\lambda (H1: ((\forall (f0: ((nat \to nat))).(\forall (g: ((nat \to
342 nat))).(((\forall (m: nat).(le (f0 m) (g m)))) \to ((lt (weight_map f0 (lift
343 (S i) O v)) (g i)) \to (lt (weight_map f0 t2) (weight_map g
344 t1)))))))).(\lambda (u0: T).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat
345 \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f0 m) (g m))))).(\lambda
346 (H3: (lt (weight_map f0 (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map
347 f0 u0) (weight_map f0 t2)) (plus (weight_map g u0) (weight_map g t1))
348 (le_lt_plus_plus (weight_map f0 u0) (weight_map g u0) (weight_map f0 t2)
349 (weight_map g t1) (weight_le u0 f0 g H2) (H1 f0 g H2 H3))))))))))))))) k))
350 (\lambda (v: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (i: nat).(\lambda
351 (_: (subst0 i v u1 u2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall
352 (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt
353 (weight_map f (lift (S i) O v)) (g i)) \to (lt (weight_map f u2) (weight_map
354 g u1)))))))).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (t1:
355 T).(\forall (t2: T).((subst0 (s k0 i) v t1 t2) \to (((\forall (f: ((nat \to
356 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
357 \to ((lt (weight_map f (lift (S (s k0 i)) O v)) (g (s k0 i))) \to (lt
358 (weight_map f t2) (weight_map g t1))))))) \to (\forall (f: ((nat \to
359 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
360 \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (lt (weight_map f (THead
361 k0 u2 t2)) (weight_map g (THead k0 u1 t1)))))))))))) (\lambda (b: B).(B_ind
362 (\lambda (b0: B).(\forall (t1: T).(\forall (t2: T).((subst0 (s (Bind b0) i) v
363 t1 t2) \to (((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
364 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
365 (s (Bind b0) i)) O v)) (g (s (Bind b0) i))) \to (lt (weight_map f t2)
366 (weight_map g t1))))))) \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat
367 \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f
368 (lift (S i) O v)) (g i)) \to (lt (weight_map f (THead (Bind b0) u2 t2))
369 (weight_map g (THead (Bind b0) u1 t1)))))))))))) (\lambda (t1: T).(\lambda
370 (t2: T).(\lambda (H2: (subst0 (S i) v t1 t2)).(\lambda (_: ((\forall (f:
371 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
372 (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (lt
373 (weight_map f t2) (weight_map g t1)))))))).(\lambda (f: ((nat \to
374 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H4: ((\forall (m: nat).(le (f
375 m) (g m))))).(\lambda (H5: (lt (weight_map f (lift (S i) O v)) (g
376 i))).(lt_n_S (plus (weight_map f u2) (weight_map (wadd f (S (weight_map f
377 u2))) t2)) (plus (weight_map g u1) (weight_map (wadd g (S (weight_map g u1)))
378 t1)) (lt_le_plus_plus (weight_map f u2) (weight_map g u1) (weight_map (wadd f
379 (S (weight_map f u2))) t2) (weight_map (wadd g (S (weight_map g u1))) t1) (H1
380 f g H4 H5) (subst0_weight_le v t1 t2 (S i) H2 (wadd f (S (weight_map f u2)))
381 (wadd g (S (weight_map g u1))) (\lambda (m: nat).(wadd_lt f g H4 (S
382 (weight_map f u2)) (S (weight_map g u1)) (lt_n_S (weight_map f u2)
383 (weight_map g u1) (H1 f g H4 H5)) m)) (eq_ind nat (weight_map f (lift (S i) O
384 v)) (\lambda (n: nat).(lt n (g i))) H5 (weight_map (wadd f (S (weight_map f
385 u2))) (lift (S (S i)) O v)) (lift_weight_add_O (S (weight_map f u2)) v (S i)
386 f))))))))))))) (\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (subst0 (S i) v
387 t1 t2)).(\lambda (H3: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
388 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
389 (S i)) O v)) (g (S i))) \to (lt (weight_map f t2) (weight_map g
390 t1)))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
391 nat))).(\lambda (H4: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H5: (lt
392 (weight_map f (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map f u2)
393 (weight_map (wadd f O) t2)) (plus (weight_map g u1) (weight_map (wadd g O)
394 t1)) (lt_plus_plus (weight_map f u2) (weight_map g u1) (weight_map (wadd f O)
395 t2) (weight_map (wadd g O) t1) (H1 f g H4 H5) (H3 (wadd f O) (wadd g O)
396 (\lambda (m: nat).(le_S_n (wadd f O m) (wadd g O m) (le_n_S (wadd f O m)
397 (wadd g O m) (wadd_le f g H4 O O (le_n O) m)))) (eq_ind nat (weight_map f
398 (lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H5 (weight_map (wadd f O)
399 (lift (S (S i)) O v)) (lift_weight_add_O O v (S i) f))))))))))))) (\lambda
400 (t1: T).(\lambda (t2: T).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H3:
401 ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
402 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S
403 i))) \to (lt (weight_map f t2) (weight_map g t1)))))))).(\lambda (f: ((nat
404 \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H4: ((\forall (m: nat).(le
405 (f m) (g m))))).(\lambda (H5: (lt (weight_map f (lift (S i) O v)) (g
406 i))).(lt_n_S (plus (weight_map f u2) (weight_map (wadd f O) t2)) (plus
407 (weight_map g u1) (weight_map (wadd g O) t1)) (lt_plus_plus (weight_map f u2)
408 (weight_map g u1) (weight_map (wadd f O) t2) (weight_map (wadd g O) t1) (H1 f
409 g H4 H5) (H3 (wadd f O) (wadd g O) (\lambda (m: nat).(le_S_n (wadd f O m)
410 (wadd g O m) (le_n_S (wadd f O m) (wadd g O m) (wadd_le f g H4 O O (le_n O)
411 m)))) (eq_ind nat (weight_map f (lift (S i) O v)) (\lambda (n: nat).(lt n (g
412 i))) H5 (weight_map (wadd f O) (lift (S (S i)) O v)) (lift_weight_add_O O v
413 (S i) f))))))))))))) b)) (\lambda (_: F).(\lambda (t1: T).(\lambda (t2:
414 T).(\lambda (_: (subst0 i v t1 t2)).(\lambda (H3: ((\forall (f0: ((nat \to
415 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f0 m) (g m))))
416 \to ((lt (weight_map f0 (lift (S i) O v)) (g i)) \to (lt (weight_map f0 t2)
417 (weight_map g t1)))))))).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat
418 \to nat))).(\lambda (H4: ((\forall (m: nat).(le (f0 m) (g m))))).(\lambda
419 (H5: (lt (weight_map f0 (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map
420 f0 u2) (weight_map f0 t2)) (plus (weight_map g u1) (weight_map g t1))
421 (lt_plus_plus (weight_map f0 u2) (weight_map g u1) (weight_map f0 t2)
422 (weight_map g t1) (H1 f0 g H4 H5) (H3 f0 g H4 H5)))))))))))) k)))))))) d u t
425 theorem subst0_tlt_head:
426 \forall (u: T).(\forall (t: T).(\forall (z: T).((subst0 O u t z) \to (tlt
427 (THead (Bind Abbr) u z) (THead (Bind Abbr) u t)))))
429 \lambda (u: T).(\lambda (t: T).(\lambda (z: T).(\lambda (H: (subst0 O u t
430 z)).(lt_n_S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
431 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) z)) (plus
432 (weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S
433 (weight_map (\lambda (_: nat).O) u))) t)) (le_lt_plus_plus (weight_map
434 (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
435 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) z) (weight_map
436 (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t) (le_n
437 (weight_map (\lambda (_: nat).O) u)) (subst0_weight_lt u t z O H (wadd
438 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) (wadd (\lambda
439 (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) (\lambda (m: nat).(le_n
440 (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u)) m)))
441 (eq_ind nat (weight_map (\lambda (_: nat).O) (lift O O u)) (\lambda (n:
442 nat).(lt n (S (weight_map (\lambda (_: nat).O) u)))) (eq_ind_r T u (\lambda
443 (t0: T).(lt (weight_map (\lambda (_: nat).O) t0) (S (weight_map (\lambda (_:
444 nat).O) u)))) (le_n (S (weight_map (\lambda (_: nat).O) u))) (lift O O u)
445 (lift_r u O)) (weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda
446 (_: nat).O) u))) (lift (S O) O u)) (lift_weight_add_O (S (weight_map (\lambda
447 (_: nat).O) u)) u O (\lambda (_: nat).O))))))))).
450 \forall (u: T).(\forall (t: T).(\forall (z: T).((subst0 O u t z) \to (tlt z
451 (THead (Bind Abbr) u t)))))
453 \lambda (u: T).(\lambda (t: T).(\lambda (z: T).(\lambda (H: (subst0 O u t
454 z)).(tlt_trans (THead (Bind Abbr) u z) z (THead (Bind Abbr) u t) (tlt_head_dx
455 (Bind Abbr) u z) (subst0_tlt_head u t z H))))).
projects / helm.git / blob