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 set "baseuri" "cic:/matita/SK/".
17 include "legacy/coq.ma".
19 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
20 alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
21 alias id "eq_ind" = "cic:/Coq/Init/Logic/eq_ind.con".
22 alias id "eq_ind_r" = "cic:/Coq/Init/Logic/eq_ind_r.con".
23 alias id "sym_eq" = "cic:/Coq/Init/Logic/sym_eq.con".
27 \forall app: A \to A \to A.
30 \forall H1: (\forall x,y:A.(app (app K x) y) = x).
31 \forall H2: (\forall x,y,z:A.
32 (app (app (app S x) y) z) = (app (app x z) (app y z))).
34 (app (app (app S K) K) x) = x.
35 intros.auto paramodulation.
42 \forall add: A \to A \to A.
43 \forall mult: A \to A \to A.
45 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
46 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
47 \forall d1: (\forall x,y,z:A.
48 (add x (mult y z)) = (mult (add x y) (add x z))).
49 \forall d2: (\forall x,y,z:A.
50 (mult x (add y z)) = (add (mult x y) (mult x z))).
51 \forall i1: (\forall x:A. (add x zero) = x).
52 \forall i2: (\forall x:A. (mult x one) = x).
53 \forall inv1: (\forall x:A. (add x (inv x)) = one).
54 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
56 intros.auto paramodulation.
63 \forall add: A \to A \to A.
64 \forall mult: A \to A \to A.
66 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
67 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
68 \forall d1: (\forall x,y,z:A.
69 (add x (mult y z)) = (mult (add x y) (add x z))).
70 \forall d2: (\forall x,y,z:A.
71 (mult x (add y z)) = (add (mult x y) (mult x z))).
72 \forall i1: (\forall x:A. (add x zero) = x).
73 \forall i2: (\forall x:A. (mult x one) = x).
74 \forall inv1: (\forall x:A. (add x (inv x)) = one).
75 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
76 \forall x:A. (mult x zero) = zero.
77 intros.auto paramodulation.
84 \forall add: A \to A \to A.
85 \forall mult: A \to A \to A.
87 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
88 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
89 \forall d1: (\forall x,y,z:A.
90 (add x (mult y z)) = (mult (add x y) (add x z))).
91 \forall d2: (\forall x,y,z:A.
92 (mult x (add y z)) = (add (mult x y) (mult x z))).
93 \forall i1: (\forall x:A. (add x zero) = x).
94 \forall i2: (\forall x:A. (mult x one) = x).
95 \forall inv1: (\forall x:A. (add x (inv x)) = one).
96 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
97 \forall x:A. (inv (inv x)) = x.
98 intros.auto paramodulation.
105 \forall add: A \to A \to A.
106 \forall mult: A \to A \to A.
107 \forall inv: A \to A.
108 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
109 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
110 \forall d1: (\forall x,y,z:A.
111 (add x (mult y z)) = (mult (add x y) (add x z))).
112 \forall d2: (\forall x,y,z:A.
113 (mult x (add y z)) = (add (mult x y) (mult x z))).
114 \forall i1: (\forall x:A. (add x zero) = x).
115 \forall i2: (\forall x:A. (mult x one) = x).
116 \forall inv1: (\forall x:A. (add x (inv x)) = one).
117 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
119 (add x y) = (add (add x (mult y z)) y).
122 ((eq_ind A (add y (add x (mult y z)))
123 (\lambda x_DemodGoal_193:A.(eq A (add x y) x_DemodGoal_193))
125 (\lambda x_DemodGoal_893:A.(eq A x_DemodGoal_893 (add y (add x (mult y z)))))
126 (eq_ind A y (\lambda x_DemodGoal_894:A.(eq A x x_DemodGoal_894))
127 (eq_ind A (add y zero) (\lambda x_Demod_554:A.(eq A x x_Demod_554))
128 (eq_ind_r A (add zero x) (\lambda x_SupR_809:A.(eq A x_SupR_809 (add y zero)))
129 (eq_ind_r A (add y (mult (add zero y) zero))
130 (\lambda x_Demod_553:A.(eq A (add zero x) x_Demod_553))
131 (eq_ind A (add (add zero x) zero)
132 (\lambda x_Demod_540:A.(eq A x_Demod_540 (add x (mult (add zero x) zero))))
133 (eq_ind_r A (mult zero x))
134 (\lambda x_Demod_526:A.(eq A (add (add zero x) x_Demod_526) (add x (mult (add zero x) zero))))
135 (eq_ind_r A (mult (add zero x) (add (add zero x) x))
136 (\lambda x_SupR_606:A.(eq A (add (add zero x) (mult zero x)) x_SupR_606))
137 (eq_ind A (add (add zero x) zero)
138 (\lambda x_SupR_296:A.(eq A (add (add zero x) (mult zero x)) (mult x_SupR_296 (add (add zero x) x))))
139 (H2 (add zero x) zero x) (add zero x) (H4 (add zero x))) (add x (mult (add zero x) zero))
140 (eq_ind A (add x zero)
141 (\lambda x_SupR_357:A.(eq A (add x (mult (add zero x) zero)) (mult x_SupR_357 (add (add zero x) x))))
142 (eq_ind A (mult (add (add zero x) x) (add x zero))
143 (\lambda x_SupR_310:A.(eq A (add x (mult (add zero x) zero)) x_SupR_310))
144 (eq_ind A (add x (add zero x))
145 (\lambda x_SupR_302:A.(eq A (add x (mult (add zero x) zero)) (mult x_SupR_302 (add x zero))))
146 (H2 x (add zero x) zero) (add (add zero x) x) (H x (add zero x))) (mult (add x zero) (add (add zero x) x)) (H1 (add (add zero x) x) (add x zero))) (add zero x) (H x zero))) zero
147 (eq_ind A (mult zero one)
148 (\lambda x_Demod_507:A.(eq A x_Demod_507 (mult zero x)))
149 (eq_ind_r A (add x one)
150 (\lambda x_Demod_506:A.(eq A (mult zero x_Demod_506) (mult zero x)))
151 (eq_ind_r A (inv zero)
152 (\lambda x_SupR_785:A.(eq A (mult zero (add x x_SupR_785)) (mult zero x)))
153 (eq_ind A (add (mult zero x) zero)
154 (\lambda x_Demod_223:A.(eq A (mult zero (add x (inv zero))) x_Demod_223))
155 (eq_ind A (mult zero (inv zero))
156 (\lambda x_SupR_337:A.(eq A (mult zero (add x (inv zero))) (add (mult zero x) x_SupR_337)))
157 (H3 zero x (inv zero)) zero (H7 zero)) (mult zero x) (H4 (mult zero x))) one
158 (eq_ind A (add (inv zero) zero)
159 (\lambda x_SupR_463:A.(eq A one x_SupR_463))
160 (eq_ind A (add zero (inv zero))
161 (\lambda x_SupR_298:A.(eq A x_SupR_298 (add (inv zero) zero))) (H zero (inv zero)) one (H6 zero)) (inv zero) (H4 (inv zero)))) one
162 (eq_ind A (add x (inv x))
163 (\lambda x_Demod_268:A.(eq A x_Demod_268 (add x one)))
164 (eq_ind A (mult (inv x) one)
165 (\lambda x_SupR_396:A.(eq A (add x x_SupR_396) (add x one)))
166 (eq_ind_r A (mult one (add x one))
167 (\lambda x_Demod_199:A.(eq A (add x (mult (inv x) one)) x_Demod_199))
168 (eq_ind A (add x (inv x))
169 (\lambda x_SupR_268:A.(eq A (add x (mult (inv x) one)) (mult x_SupR_268 (add x one)))) (H2 x (inv x) one) one (H6 x)) (add x one)
170 (eq_ind A (mult (add x one) one)
171 (\lambda x_SupR_271:A.(eq A x_SupR_271 (mult one (add x one))))
172 (H1 (add x one) one) (add x one) (H5 (add x one)))) (inv x) (H5 (inv x))) one (H6 x))) zero (H5 zero))) (add zero x) (H4 (add zero x))) (add y zero)
173 (eq_ind A (add zero zero)
174 (\lambda x_Demod_543:A.(eq A (add y x_Demod_543) (add y (mult (add zero y) zero))))
175 (eq_ind_r A (mult zero y)
176 (\lambda x_Demod_524:A.(eq A (add y (add zero x_Demod_524)) (add y (mult (add zero y) zero))))
177 (eq_ind_r A (mult zero (add zero y))
178 (\lambda x_SupR_628:A.(eq A (add y x_SupR_628) (add y (mult (add zero y) zero))))
179 (eq_ind_r A (mult (add y (add zero y)) (add y zero))
180 (\lambda x_Demod_195:A.(eq A (add y (mult zero (add zero y))) x_Demod_195))
181 (eq_ind_r A (mult (add y zero) (add y (add zero y)))
182 (\lambda x_SupR_272:A.(eq A x_SupR_272 (mult (add y (add zero y)) (add y zero)))) (H1 (add y zero) (add y (add zero y))) (add y (mult zero (add zero y))) (H2 y zero (add zero y))) (add y (mult (add zero y) zero)) (H2 y (add zero y) zero)) (add zero (mult zero y))
183 (eq_ind A (add zero zero)
184 (\lambda x_SupR_296:A.(eq A (add zero (mult zero y)) (mult x_SupR_296 (add zero y)))) (H2 zero zero y) zero (H4 zero))) zero
185 (eq_ind A (mult zero one)
186 (\lambda x_Demod_507:A.(eq A x_Demod_507 (mult zero y)))
187 (eq_ind_r A (add y one)
188 (\lambda x_Demod_506:A.(eq A (mult zero x_Demod_506) (mult zero y)))
189 (eq_ind_r A (inv zero)
190 (\lambda x_SupR_785:A.(eq A (mult zero (add y x_SupR_785)) (mult zero y)))
191 (eq_ind A (add (mult zero y) zero)
192 (\lambda x_Demod_223:A.(eq A (mult zero (add y (inv zero))) x_Demod_223))
193 (eq_ind A (mult zero (inv zero))
194 (\lambda x_SupR_337:A.(eq A (mult zero (add y (inv zero))) (add (mult zero y) x_SupR_337))) (H3 zero y (inv zero)) zero (H7 zero)) (mult zero y) (H4 (mult zero y))) one
195 (eq_ind A (add (inv zero) zero)
196 (\lambda x_SupR_463:A.(eq A one x_SupR_463)) (eq_ind A (add zero (inv zero))
197 (\lambda x_SupR_298:A.(eq A x_SupR_298 (add (inv zero) zero))) (H zero (inv zero)) one (H6 zero)) (inv zero) (H4 (inv zero)))) one
198 (eq_ind A (add y (inv y))
199 (\lambda x_Demod_268:A.(eq A x_Demod_268 (add y one)))
200 (eq_ind A (mult (inv y) one)
201 (\lambda x_SupR_396:A.(eq A (add y x_SupR_396) (add y one)))
202 (eq_ind_r A (mult one (add y one))
203 (\lambda x_Demod_199:A.(eq A (add y (mult (inv y) one)) x_Demod_199))
204 (eq_ind A (add y (inv y))
205 (\lambda x_SupR_268:A.(eq A (add y (mult (inv y) one)) (mult x_SupR_268 (add y one)))) (H2 y (inv y) one) one (H6 y)) (add y one)
206 (eq_ind A (mult (add y one) one)
207 (\lambda x_SupR_271:A.(eq A x_SupR_271 (mult one (add y one)))) (H1 (add y one) one) (add y one) (H5 (add y one)))) (inv y) (H5 (inv y))) one (H6 y))) zero (H5 zero))) zero (H4 zero))) x
208 (eq_ind A (add x zero)
209 (\lambda x_SupR_299:A.(eq A x_SupR_299 (add zero x))) (H x zero) x (H4 x))) y (H4 y)) (add y (add x (mult y z)))
210 (sym_eq\subst[A \Assign A ; x \Assign (add y (add x (mult y z))) ; y \Assign y]
211 (eq_ind_r A (add zero y)
212 (\lambda x_SupR_826:A.(eq A (add y (add x (mult y z))) x_SupR_826))
213 (eq_ind_r A (add zero (mult (add y zero) y))
214 (\lambda x_Demod_553:A.(eq A (add y (add x (mult y z))) x_Demod_553))
215 (eq_ind A (add (add y (add x (mult y z))) zero)
216 (\lambda x_Demod_540:A.(eq A x_Demod_540 (add (add x (mult y z)) (mult (add y (add x (mult y z))) y))))
217 (eq_ind_r A (mult zero (add x (mult y z)))
218 (\lambda x_Demod_526:A.(eq A (add (add y (add x (mult y z))) x_Demod_526) (add (add x (mult y z)) (mult (add y (add x (mult y z))) y))))
219 (eq_ind_r A (mult (add y (add x (mult y z))) (add (add y (add x (mult y z))) (add x (mult y z))))
220 (\lambda x_SupR_606:A.(eq A (add (add y (add x (mult y z))) (mult zero (add x (mult y z)))) x_SupR_606))
221 (eq_ind A (add (add y (add x (mult y z))) zero)
222 (\lambda x_SupR_296:A.(eq A (add (add y (add x (mult y z))) (mult zero (add x (mult y z)))) (mult x_SupR_296 (add (add y (add x (mult y z))) (add x (mult y z))))))
223 (H2 (add y (add x (mult y z))) zero (add x (mult y z))) (add y (add x (mult y z))) (H4 (add y (add x (mult y z))))) (add (add x (mult y z)) (mult (add y (add x (mult y z))) y))
224 (eq_ind A (add (add x (mult y z)) y)
225 (\lambda x_SupR_357:A.(eq A (add (add x (mult y z)) (mult (add y (add x (mult y z))) y)) (mult x_SupR_357 (add (add y (add x (mult y z))) (add x (mult y z)))))) (eq_ind A (mult (add (add y (add x (mult y z))) (add x (mult y z))) (add (add x (mult y z)) y))
226 (\lambda x_SupR_310:A.(eq A (add (add x (mult y z)) (mult (add y (add x (mult y z))) y)) x_SupR_310)) (eq_ind A (add (add x (mult y z)) (add y (add x (mult y z))))
227 (\lambda x_SupR_302:A.(eq A (add (add x (mult y z)) (mult (add y (add x (mult y z))) y)) (mult x_SupR_302 (add (add x (mult y z)) y)))) (H2 (add x (mult y z)) (add y (add x (mult y z))) y) (add (add y (add x (mult y z))) (add x (mult y z))) (H (add x (mult y z)) (add y (add x (mult y z))))) (mult (add (add x (mult y z)) y) (add (add y (add x (mult y z))) (add x (mult y z)))) (H1 (add (add y (add x (mult y z))) (add x (mult y z))) (add (add x (mult y z)) y))) (add y (add x (mult y z))) (H (add x (mult y z)) y))) zero (eq_ind A (mult zero one)
228 (\lambda x_Demod_507:A.(eq A x_Demod_507 (mult zero (add x (mult y z)))))
229 (eq_ind_r A (add (add x (mult y z)) one)
230 (\lambda x_Demod_506:A.(eq A (mult zero x_Demod_506) (mult zero (add x (mult y z)))))
231 (eq_ind_r A (inv zero)
232 (\lambda x_SupR_785:A.(eq A (mult zero (add (add x (mult y z)) x_SupR_785)) (mult zero (add x (mult y z)))))
233 (eq_ind A (add (mult zero (add x (mult y z))) zero)
234 (\lambda x_Demod_223:A.(eq A (mult zero (add (add x (mult y z)) (inv zero))) x_Demod_223))
235 (eq_ind A (mult zero (inv zero))
236 (\lambda x_SupR_337:A.(eq A (mult zero (add (add x (mult y z)) (inv zero))) (add (mult zero (add x (mult y z))) x_SupR_337))) (H3 zero (add x (mult y z)) (inv zero)) zero (H7 zero)) (mult zero (add x (mult y z))) (H4 (mult zero (add x (mult y z))))) one
237 (eq_ind A (add (inv zero) zero)
238 (\lambda x_SupR_463:A.(eq A one x_SupR_463))
239 (eq_ind A (add zero (inv zero))
240 (\lambda x_SupR_298:A.(eq A x_SupR_298 (add (inv zero) zero))) (H zero (inv zero)) one (H6 zero)) (inv zero) (H4 (inv zero)))) one
241 (eq_ind A (add (add x (mult y z)) (inv (add x (mult y z))))
242 (\lambda x_Demod_268:A.(eq A x_Demod_268 (add (add x (mult y z)) one)))
243 (eq_ind A (mult (inv (add x (mult y z))) one)
244 (\lambda x_SupR_396:A.(eq A (add (add x (mult y z)) x_SupR_396) (add (add x (mult y z)) one)))
245 (eq_ind_r A (mult one (add (add x (mult y z)) one))
246 (\lambda x_Demod_199:A.(eq A (add (add x (mult y z)) (mult (inv (add x (mult y z))) one)) x_Demod_199))
247 (eq_ind A (add (add x (mult y z)) (inv (add x (mult y z))))
248 (\lambda x_SupR_268:A.(eq A (add (add x (mult y z)) (mult (inv (add x (mult y z))) one)) (mult x_SupR_268 (add (add x (mult y z)) one)))) (H2 (add x (mult y z)) (inv (add x (mult y z))) one) one (H6 (add x (mult y z)))) (add (add x (mult y z)) one) (eq_ind A (mult (add (add x (mult y z)) one) one)
249 (\lambda x_SupR_271:A.(eq A x_SupR_271 (mult one (add (add x (mult y z)) one)))) (H1 (add (add x (mult y z)) one) one) (add (add x (mult y z)) one) (H5 (add (add x (mult y z)) one)))) (inv (add x (mult y z))) (H5 (inv (add x (mult y z))))) one (H6 (add x (mult y z))))) zero (H5 zero))) (add y (add x (mult y z))) (H4 (add y (add x (mult y z))))) (add zero y)
250 (eq_ind A (add y zero)
251 (\lambda x_Demod_543:A.(eq A (add zero x_Demod_543) (add zero (mult (add y zero) y))))
252 (eq_ind_r A (mult zero zero)
253 (\lambda x_Demod_524:A.(eq A (add zero (add y x_Demod_524)) (add zero (mult (add y zero) y))))
254 (eq_ind_r A (mult y (add y zero))
255 (\lambda x_SupR_628:A.(eq A (add zero x_SupR_628) (add zero (mult (add y zero) y))))
256 (eq_ind_r A (mult (add zero (add y zero)) (add zero y))
257 (\lambda x_Demod_195:A.(eq A (add zero (mult y (add y zero))) x_Demod_195))
258 (eq_ind_r A (mult (add zero y) (add zero (add y zero)))
259 (\lambda x_SupR_272:A.(eq A x_SupR_272 (mult (add zero (add y zero)) (add zero y)))) (H1 (add zero y) (add zero (add y zero))) (add zero (mult y (add y zero))) (H2 zero y (add y zero))) (add zero (mult (add y zero) y)) (H2 zero (add y zero) y)) (add y (mult zero zero))
260 (eq_ind A (add y zero)
261 (\lambda x_SupR_296:A.(eq A (add y (mult zero zero)) (mult x_SupR_296 (add y zero)))) (H2 y zero zero) y (H4 y))) zero
262 (eq_ind A (mult zero one)
263 (\lambda x_Demod_507:A.(eq A x_Demod_507 (mult zero zero)))
264 (eq_ind_r A (add zero one)
265 (\lambda x_Demod_506:A.(eq A (mult zero x_Demod_506) (mult zero zero)))
266 (eq_ind_r A (inv zero)
267 (\lambda x_SupR_785:A.(eq A (mult zero (add zero x_SupR_785)) (mult zero zero)))
268 (eq_ind A (add (mult zero zero) zero)
269 (\lambda x_Demod_223:A.(eq A (mult zero (add zero (inv zero))) x_Demod_223))
270 (eq_ind A (mult zero (inv zero))
271 (\lambda x_SupR_337:A.(eq A (mult zero (add zero (inv zero))) (add (mult zero zero) x_SupR_337))) (H3 zero zero (inv zero)) zero (H7 zero)) (mult zero zero) (H4 (mult zero zero))) one
272 (eq_ind A (add (inv zero) zero)
273 (\lambda x_SupR_463:A.(eq A one x_SupR_463))
274 (eq_ind A (add zero (inv zero))
275 (\lambda x_SupR_298:A.(eq A x_SupR_298 (add (inv zero) zero))) (H zero (inv zero)) one (H6 zero)) (inv zero) (H4 (inv zero)))) one
276 (eq_ind A (add zero (inv zero))
277 (\lambda x_Demod_268:A.(eq A x_Demod_268 (add zero one)))
278 (eq_ind A (mult (inv zero) one) (\lambda x_SupR_396:A.(eq A (add zero x_SupR_396) (add zero one)))
279 (eq_ind_r A (mult one (add zero one))
280 (\lambda x_Demod_199:A.(eq A (add zero (mult (inv zero) one)) x_Demod_199))
281 (eq_ind A (add zero (inv zero))
282 (\lambda x_SupR_268:A.(eq A (add zero (mult (inv zero) one)) (mult x_SupR_268 (add zero one)))) (H2 zero (inv zero) one) one (H6 zero)) (add zero one)
283 (eq_ind A (mult (add zero one) one)
284 (\lambda x_SupR_271:A.(eq A x_SupR_271 (mult one (add zero one)))) (H1 (add zero one) one) (add zero one) (H5 (add zero one)))) (inv zero) (H5 (inv zero))) one (H6 zero))) zero (H5 zero))) y (H4 y))) y
285 (eq_ind A (add y zero)
286 (\lambda x_SupR_299:A.(eq A x_SupR_299 (add zero y))) (H y zero) y (H4 y))))) (add x y)
287 (sym_eq\subst[A \Assign A ; x \Assign (add x y) ; y \Assign x]
288 (eq_ind_r A (add zero x)
289 (\lambda x_SupR_826:A.(eq A (add x y) x_SupR_826))
290 (eq_ind_r A (add zero (mult (add x zero) x))
291 (\lambda x_Demod_553:A.(eq A (add x y) x_Demod_553))
292 (eq_ind A (add (add x y) zero)
293 (\lambda x_Demod_540:A.(eq A x_Demod_540 (add y (mult (add x y) x))))
294 (eq_ind_r A (mult zero y)
295 (\lambda x_Demod_526:A.(eq A (add (add x y) x_Demod_526) (add y (mult (add x y) x))))
296 (eq_ind_r A (mult (add x y) (add (add x y) y))
297 (\lambda x_SupR_606:A.(eq A (add (add x y) (mult zero y)) x_SupR_606))
298 (eq_ind A (add (add x y) zero)
299 (\lambda x_SupR_296:A.(eq A (add (add x y) (mult zero y)) (mult x_SupR_296 (add (add x y) y)))) (H2 (add x y) zero y) (add x y) (H4 (add x y))) (add y (mult (add x y) x))
301 (\lambda x_SupR_357:A.(eq A (add y (mult (add x y) x)) (mult x_SupR_357 (add (add x y) y))))
302 (eq_ind A (mult (add (add x y) y) (add y x))
303 (\lambda x_SupR_310:A.(eq A (add y (mult (add x y) x)) x_SupR_310))
304 (eq_ind A (add y (add x y))
305 (\lambda x_SupR_302:A.(eq A (add y (mult (add x y) x)) (mult x_SupR_302 (add y x)))) (H2 y (add x y) x) (add (add x y) y) (H y (add x y))) (mult (add y x) (add (add x y) y)) (H1 (add (add x y) y) (add y x))) (add x y) (H y x))) zero
306 (eq_ind A (mult zero one)
307 (\lambda x_Demod_507:A.(eq A x_Demod_507 (mult zero y)))
308 (eq_ind_r A (add y one)
309 (\lambda x_Demod_506:A.(eq A (mult zero x_Demod_506) (mult zero y)))
310 (eq_ind_r A (inv zero)
311 (\lambda x_SupR_785:A.(eq A (mult zero (add y x_SupR_785)) (mult zero y)))
312 (eq_ind A (add (mult zero y) zero)
313 (\lambda x_Demod_223:A.(eq A (mult zero (add y (inv zero))) x_Demod_223))
314 (eq_ind A (mult zero (inv zero))
315 (\lambda x_SupR_337:A.(eq A (mult zero (add y (inv zero))) (add (mult zero y) x_SupR_337))) (H3 zero y (inv zero)) zero (H7 zero)) (mult zero y) (H4 (mult zero y))) one
316 (eq_ind A (add (inv zero) zero)
317 (\lambda x_SupR_463:A.(eq A one x_SupR_463))
318 (eq_ind A (add zero (inv zero))
319 (\lambda x_SupR_298:A.(eq A x_SupR_298 (add (inv zero) zero))) (H zero (inv zero)) one (H6 zero)) (inv zero) (H4 (inv zero)))) one
320 (eq_ind A (add y (inv y))
321 (\lambda x_Demod_268:A.(eq A x_Demod_268 (add y one)))
322 (eq_ind A (mult (inv y) one)
323 (\lambda x_SupR_396:A.(eq A (add y x_SupR_396) (add y one)))
324 (eq_ind_r A (mult one (add y one))
325 (\lambda x_Demod_199:A.(eq A (add y (mult (inv y) one)) x_Demod_199))
326 (eq_ind A (add y (inv y))
327 (\lambda x_SupR_268:A.(eq A (add y (mult (inv y) one)) (mult x_SupR_268 (add y one)))) (H2 y (inv y) one) one (H6 y)) (add y one)
328 (eq_ind A (mult (add y one) one)
329 (\lambda x_SupR_271:A.(eq A x_SupR_271 (mult one (add y one)))) (H1 (add y one) one) (add y one) (H5 (add y one)))) (inv y) (H5 (inv y))) one (H6 y))) zero (H5 zero))) (add x y) (H4 (add x y))) (add zero x)
330 (eq_ind A (add x zero)
331 (\lambda x_Demod_543:A.(eq A (add zero x_Demod_543) (add zero (mult (add x zero) x))))
332 (eq_ind_r A (mult zero zero)
333 (\lambda x_Demod_524:A.(eq A (add zero (add x x_Demod_524)) (add zero (mult (add x zero) x))))
334 (eq_ind_r A (mult x (add x zero))
335 (\lambda x_SupR_628:A.(eq A (add zero x_SupR_628) (add zero (mult (add x zero) x))))
336 (eq_ind_r A (mult (add zero (add x zero)) (add zero x))
337 (\lambda x_Demod_195:A.(eq A (add zero (mult x (add x zero))) x_Demod_195))
338 (eq_ind_r A (mult (add zero x) (add zero (add x zero)))
339 (\lambda x_SupR_272:A.(eq A x_SupR_272 (mult (add zero (add x zero)) (add zero x)))) (H1 (add zero x) (add zero (add x zero))) (add zero (mult x (add x zero))) (H2 zero x (add x zero))) (add zero (mult (add x zero) x)) (H2 zero (add x zero) x)) (add x (mult zero zero))
340 (eq_ind A (add x zero)
341 (\lambda x_SupR_296:A.(eq A (add x (mult zero zero)) (mult x_SupR_296 (add x zero)))) (H2 x zero zero) x (H4 x))) zero
342 (eq_ind A (mult zero one)
343 (\lambda x_Demod_507:A.(eq A x_Demod_507 (mult zero zero)))
344 (eq_ind_r A (add zero one)
345 (\lambda x_Demod_506:A.(eq A (mult zero x_Demod_506) (mult zero zero)))
346 (eq_ind_r A (inv zero)
347 (\lambda x_SupR_785:A.(eq A (mult zero (add zero x_SupR_785)) (mult zero zero)))
348 (eq_ind A (add (mult zero zero) zero)
349 (\lambda x_Demod_223:A.(eq A (mult zero (add zero (inv zero))) x_Demod_223))
350 (eq_ind A (mult zero (inv zero))
351 (\lambda x_SupR_337:A.(eq A (mult zero (add zero (inv zero))) (add (mult zero zero) x_SupR_337))) (H3 zero zero (inv zero)) zero (H7 zero)) (mult zero zero) (H4 (mult zero zero))) one
352 (eq_ind A (add (inv zero) zero)
353 (\lambda x_SupR_463:A.(eq A one x_SupR_463))
354 (eq_ind A (add zero (inv zero))
355 (\lambda x_SupR_298:A.(eq A x_SupR_298 (add (inv zero) zero))) (H zero (inv zero)) one (H6 zero)) (inv zero) (H4 (inv zero)))) one
356 (eq_ind A (add zero (inv zero))
357 (\lambda x_Demod_268:A.(eq A x_Demod_268 (add zero one)))
358 (eq_ind A (mult (inv zero) one)
359 (\lambda x_SupR_396:A.(eq A (add zero x_SupR_396) (add zero one)))
360 (eq_ind_r A (mult one (add zero one))
361 (\lambda x_Demod_199:A.(eq A (add zero (mult (inv zero) one)) x_Demod_199))
362 (eq_ind A (add zero (inv zero))
363 (\lambda x_SupR_268:A.(eq A (add zero (mult (inv zero) one)) (mult x_SupR_268 (add zero one)))) (H2 zero (inv zero) one) one (H6 zero)) (add zero one)
364 (eq_ind A (mult (add zero one) one)
365 (\lambda x_SupR_271:A.(eq A x_SupR_271 (mult one (add zero one)))) (H1 (add zero one) one) (add zero one) (H5 (add zero one)))) (inv zero) (H5 (inv zero))) one (H6 zero))) zero (H5 zero))) x (H4 x))) x
366 (eq_ind A (add x zero)
367 (\lambda x_SupR_299:A.(eq A x_SupR_299 (add zero x))) (H x zero) x (H4 x))))) (add (add x (mult y z)) y)
368 (sym_eq\subst[A \Assign A ; x \Assign (add (add x (mult y z)) y) ; y \Assign (add y (add x (mult y z)))] (H (add x (mult y z)) y)))
381 \forall add: A \to A \to A.
382 \forall mult: A \to A \to A.
383 \forall inv: A \to A.
384 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
385 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
386 \forall d1: (\forall x,y,z:A.
387 (add x (mult y z)) = (mult (add x y) (add x z))).
388 \forall d2: (\forall x,y,z:A.
389 (mult x (add y z)) = (add (mult x y) (mult x z))).
390 \forall i1: (\forall x:A. (add x zero) = x).
391 \forall i2: (\forall x:A. (mult x one) = x).
392 \forall inv1: (\forall x:A. (add x (inv x)) = one).
393 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
395 (add x y) = (add (add x (mult y z)) y).
398 ((eq_ind A (add y (add x (mult y z)))
399 (\lambda x_DemodGoal_193:A.(eq A (add x y) x_DemodGoal_193))
401 (\lambda x_DemodGoal_893:A.(eq A x_DemodGoal_893 (add y (add x (mult y z)))))
402 (eq_ind A y (\lambda x_DemodGoal_894:A.(eq A x x_DemodGoal_894))
403 (eq_ind A (add y zero) (\lambda x_Demod_554:A.(eq A x x_Demod_554))
404 (eq_ind_r A (add zero x) (\lambda x_SupR_809:A.(eq A x_SupR_809 (add y zero)))
405 (eq_ind_r A (add y (mult (add zero y) zero))
406 (\lambda x_Demod_553:A.(eq A (add zero x) x_Demod_553))
407 (eq_ind A (add (add zero x) zero)
408 (\lambda x_Demod_540:A.(eq A x_Demod_540 (add x (mult (add zero x) zero))))
409 (eq_ind_r A (mult zero x)
410 (\lambda x_Demod_526:A.(eq A (add (add zero x) x_Demod_526) (add x (mult (add zero x) zero))))
411 (eq_ind_r A (mult (add zero x) (add (add zero x) x))
412 (\lambda x_SupR_606:A.(eq A (add (add zero x) (mult zero x)) x_SupR_606))
413 (eq_ind A (add (add zero x) zero)
414 (\lambda x_SupR_296:A.(eq A (add (add zero x) (mult zero x)) (mult x_SupR_296 (add (add zero x) x))))
415 (H2 (add zero x) zero x) (add zero x) (H4 (add zero x))) (add x (mult (add zero x) zero))
416 (eq_ind A (add x zero)
417 (\lambda x_SupR_357:A.(eq A (add x (mult (add zero x) zero)) (mult x_SupR_357 (add (add zero x) x))))
418 (eq_ind A (mult (add (add zero x) x) (add x zero))
419 (\lambda x_SupR_310:A.(eq A (add x (mult (add zero x) zero)) x_SupR_310))
420 (eq_ind A (add x (add zero x))
421 (\lambda x_SupR_302:A.(eq A (add x (mult (add zero x) zero)) (mult x_SupR_302 (add x zero))))
422 (H2 x (add zero x) zero) (add (add zero x) x) (H x (add zero x))) (mult (add x zero) (add (add zero x) x)) (H1 (add (add zero x) x) (add x zero))) (add zero x) (H x zero))) zero
423 (eq_ind A (mult zero one)
424 (\lambda x_Demod_507:A.(eq A x_Demod_507 (mult zero x)))
425 (eq_ind_r A (add x one)
426 (\lambda x_Demod_506:A.(eq A (mult zero x_Demod_506) (mult zero x)))
427 (eq_ind_r A (inv zero)
428 (\lambda x_SupR_785:A.(eq A (mult zero (add x x_SupR_785)) (mult zero x)))
429 (eq_ind A (add (mult zero x) zero)
430 (\lambda x_Demod_223:A.(eq A (mult zero (add x (inv zero))) x_Demod_223))
431 (eq_ind A (mult zero (inv zero))
432 (\lambda x_SupR_337:A.(eq A (mult zero (add x (inv zero))) (add (mult zero x) x_SupR_337)))
433 (H3 zero x (inv zero)) zero (H7 zero)) (mult zero x) (H4 (mult zero x))) one
434 (eq_ind A (add (inv zero) zero)
435 (\lambda x_SupR_463:A.(eq A one x_SupR_463))
436 (eq_ind A (add zero (inv zero))
437 (\lambda x_SupR_298:A.(eq A x_SupR_298 (add (inv zero) zero))) (H zero (inv zero)) one (H6 zero)) (inv zero) (H4 (inv zero)))) one
438 (eq_ind A (add x (inv x))
439 (\lambda x_Demod_268:A.(eq A x_Demod_268 (add x one)))
440 (eq_ind A (mult (inv x) one)
441 (\lambda x_SupR_396:A.(eq A (add x x_SupR_396) (add x one)))
442 (eq_ind_r A (mult one (add x one))
443 (\lambda x_Demod_199:A.(eq A (add x (mult (inv x) one)) x_Demod_199))
444 (eq_ind A (add x (inv x))
445 (\lambda x_SupR_268:A.(eq A (add x (mult (inv x) one)) (mult x_SupR_268 (add x one)))) (H2 x (inv x) one) one (H6 x)) (add x one)
446 (eq_ind A (mult (add x one) one)
447 (\lambda x_SupR_271:A.(eq A x_SupR_271 (mult one (add x one))))
448 (H1 (add x one) one) (add x one) (H5 (add x one)))) (inv x) (H5 (inv x))) one (H6 x))) zero (H5 zero))) (add zero x) (H4 (add zero x))) (add y zero)
449 (eq_ind A (add zero zero)
450 (\lambda x_Demod_543:A.(eq A (add y x_Demod_543) (add y (mult (add zero y) zero))))
451 (eq_ind_r A (mult zero y)
452 (\lambda x_Demod_524:A.(eq A (add y (add zero x_Demod_524)) (add y (mult (add zero y) zero))))
453 (eq_ind_r A (mult zero (add zero y))
454 (\lambda x_SupR_628:A.(eq A (add y x_SupR_628) (add y (mult (add zero y) zero))))
455 (eq_ind_r A (mult (add y (add zero y)) (add y zero))
456 (\lambda x_Demod_195:A.(eq A (add y (mult zero (add zero y))) x_Demod_195))
457 (eq_ind_r A (mult (add y zero) (add y (add zero y)))
458 (\lambda x_SupR_272:A.(eq A x_SupR_272 (mult (add y (add zero y)) (add y zero)))) (H1 (add y zero) (add y (add zero y))) (add y (mult zero (add zero y))) (H2 y zero (add zero y))) (add y (mult (add zero y) zero)) (H2 y (add zero y) zero)) (add zero (mult zero y))
459 (eq_ind A (add zero zero)
460 (\lambda x_SupR_296:A.(eq A (add zero (mult zero y)) (mult x_SupR_296 (add zero y)))) (H2 zero zero y) zero (H4 zero))) zero
461 (eq_ind A (mult zero one)
462 (\lambda x_Demod_507:A.(eq A x_Demod_507 (mult zero y)))
463 (eq_ind_r A (add y one)
464 (\lambda x_Demod_506:A.(eq A (mult zero x_Demod_506) (mult zero y)))
465 (eq_ind_r A (inv zero)
466 (\lambda x_SupR_785:A.(eq A (mult zero (add y x_SupR_785)) (mult zero y)))
467 (eq_ind A (add (mult zero y) zero)
468 (\lambda x_Demod_223:A.(eq A (mult zero (add y (inv zero))) x_Demod_223))
469 (eq_ind A (mult zero (inv zero))
470 (\lambda x_SupR_337:A.(eq A (mult zero (add y (inv zero))) (add (mult zero y) x_SupR_337))) (H3 zero y (inv zero)) zero (H7 zero)) (mult zero y) (H4 (mult zero y))) one
471 (eq_ind A (add (inv zero) zero)
472 (\lambda x_SupR_463:A.(eq A one x_SupR_463)) (eq_ind A (add zero (inv zero))
473 (\lambda x_SupR_298:A.(eq A x_SupR_298 (add (inv zero) zero))) (H zero (inv zero)) one (H6 zero)) (inv zero) (H4 (inv zero)))) one
474 (eq_ind A (add y (inv y))
475 (\lambda x_Demod_268:A.(eq A x_Demod_268 (add y one)))
476 (eq_ind A (mult (inv y) one)
477 (\lambda x_SupR_396:A.(eq A (add y x_SupR_396) (add y one)))
478 (eq_ind_r A (mult one (add y one))
479 (\lambda x_Demod_199:A.(eq A (add y (mult (inv y) one)) x_Demod_199))
480 (eq_ind A (add y (inv y))
481 (\lambda x_SupR_268:A.(eq A (add y (mult (inv y) one)) (mult x_SupR_268 (add y one)))) (H2 y (inv y) one) one (H6 y)) (add y one)
482 (eq_ind A (mult (add y one) one)
483 (\lambda x_SupR_271:A.(eq A x_SupR_271 (mult one (add y one)))) (H1 (add y one) one) (add y one) (H5 (add y one)))) (inv y) (H5 (inv y))) one (H6 y))) zero (H5 zero))) zero (H4 zero))) x
484 (eq_ind A (add x zero)
485 (\lambda x_SupR_299:A.(eq A x_SupR_299 (add zero x))) (H x zero) x (H4 x))) y (H4 y)) (add y (add x (mult y z)))
486 (sym_eq\subst[A \Assign A ; x \Assign (add y (add x (mult y z))) ; y \Assign y]
487 (eq_ind_r A (add zero y)
488 (\lambda x_SupR_826:A.(eq A (add y (add x (mult y z))) x_SupR_826))
489 (eq_ind_r A (add zero (mult (add y zero) y))
490 (\lambda x_Demod_553:A.(eq A (add y (add x (mult y z))) x_Demod_553))
491 (eq_ind A (add (add y (add x (mult y z))) zero)
492 (\lambda x_Demod_540:A.(eq A x_Demod_540 (add (add x (mult y z)) (mult (add y (add x (mult y z))) y))))
493 (eq_ind_r A (mult zero (add x (mult y z)))
494 (\lambda x_Demod_526:A.(eq A (add (add y (add x (mult y z))) x_Demod_526) (add (add x (mult y z)) (mult (add y (add x (mult y z))) y))))
495 (eq_ind_r A (mult (add y (add x (mult y z))) (add (add y (add x (mult y z))) (add x (mult y z))))
496 (\lambda x_SupR_606:A.(eq A (add (add y (add x (mult y z))) (mult zero (add x (mult y z)))) x_SupR_606))
497 (eq_ind A (add (add y (add x (mult y z))) zero)
498 (\lambda x_SupR_296:A.(eq A (add (add y (add x (mult y z))) (mult zero (add x (mult y z)))) (mult x_SupR_296 (add (add y (add x (mult y z))) (add x (mult y z))))))
499 (H2 (add y (add x (mult y z))) zero (add x (mult y z))) (add y (add x (mult y z))) (H4 (add y (add x (mult y z))))) (add (add x (mult y z)) (mult (add y (add x (mult y z))) y))
500 (eq_ind A (add (add x (mult y z)) y)
501 (\lambda x_SupR_357:A.(eq A (add (add x (mult y z)) (mult (add y (add x (mult y z))) y)) (mult x_SupR_357 (add (add y (add x (mult y z))) (add x (mult y z)))))) (eq_ind A (mult (add (add y (add x (mult y z))) (add x (mult y z))) (add (add x (mult y z)) y))
502 (\lambda x_SupR_310:A.(eq A (add (add x (mult y z)) (mult (add y (add x (mult y z))) y)) x_SupR_310)) (eq_ind A (add (add x (mult y z)) (add y (add x (mult y z))))
503 (\lambda x_SupR_302:A.(eq A (add (add x (mult y z)) (mult (add y (add x (mult y z))) y)) (mult x_SupR_302 (add (add x (mult y z)) y)))) (H2 (add x (mult y z)) (add y (add x (mult y z))) y) (add (add y (add x (mult y z))) (add x (mult y z))) (H (add x (mult y z)) (add y (add x (mult y z))))) (mult (add (add x (mult y z)) y) (add (add y (add x (mult y z))) (add x (mult y z)))) (H1 (add (add y (add x (mult y z))) (add x (mult y z))) (add (add x (mult y z)) y))) (add y (add x (mult y z))) (H (add x (mult y z)) y))) zero (eq_ind A (mult zero one)
504 (\lambda x_Demod_507:A.(eq A x_Demod_507 (mult zero (add x (mult y z)))))
505 (eq_ind_r A (add (add x (mult y z)) one)
506 (\lambda x_Demod_506:A.(eq A (mult zero x_Demod_506) (mult zero (add x (mult y z)))))
507 (eq_ind_r A (inv zero)
508 (\lambda x_SupR_785:A.(eq A (mult zero (add (add x (mult y z)) x_SupR_785)) (mult zero (add x (mult y z)))))
509 (eq_ind A (add (mult zero (add x (mult y z))) zero)
510 (\lambda x_Demod_223:A.(eq A (mult zero (add (add x (mult y z)) (inv zero))) x_Demod_223))
511 (eq_ind A (mult zero (inv zero))
512 (\lambda x_SupR_337:A.(eq A (mult zero (add (add x (mult y z)) (inv zero))) (add (mult zero (add x (mult y z))) x_SupR_337))) (H3 zero (add x (mult y z)) (inv zero)) zero (H7 zero)) (mult zero (add x (mult y z))) (H4 (mult zero (add x (mult y z))))) one
513 (eq_ind A (add (inv zero) zero)
514 (\lambda x_SupR_463:A.(eq A one x_SupR_463))
515 (eq_ind A (add zero (inv zero))
516 (\lambda x_SupR_298:A.(eq A x_SupR_298 (add (inv zero) zero))) (H zero (inv zero)) one (H6 zero)) (inv zero) (H4 (inv zero)))) one
517 (eq_ind A (add (add x (mult y z)) (inv (add x (mult y z))))
518 (\lambda x_Demod_268:A.(eq A x_Demod_268 (add (add x (mult y z)) one)))
519 (eq_ind A (mult (inv (add x (mult y z))) one)
520 (\lambda x_SupR_396:A.(eq A (add (add x (mult y z)) x_SupR_396) (add (add x (mult y z)) one)))
521 (eq_ind_r A (mult one (add (add x (mult y z)) one))
522 (\lambda x_Demod_199:A.(eq A (add (add x (mult y z)) (mult (inv (add x (mult y z))) one)) x_Demod_199))
523 (eq_ind A (add (add x (mult y z)) (inv (add x (mult y z))))
524 (\lambda x_SupR_268:A.(eq A (add (add x (mult y z)) (mult (inv (add x (mult y z))) one)) (mult x_SupR_268 (add (add x (mult y z)) one)))) (H2 (add x (mult y z)) (inv (add x (mult y z))) one) one (H6 (add x (mult y z)))) (add (add x (mult y z)) one) (eq_ind A (mult (add (add x (mult y z)) one) one)
525 (\lambda x_SupR_271:A.(eq A x_SupR_271 (mult one (add (add x (mult y z)) one)))) (H1 (add (add x (mult y z)) one) one) (add (add x (mult y z)) one) (H5 (add (add x (mult y z)) one)))) (inv (add x (mult y z))) (H5 (inv (add x (mult y z))))) one (H6 (add x (mult y z))))) zero (H5 zero))) (add y (add x (mult y z))) (H4 (add y (add x (mult y z))))) (add zero y)
526 (eq_ind A (add y zero)
527 (\lambda x_Demod_543:A.(eq A (add zero x_Demod_543) (add zero (mult (add y zero) y))))
528 (eq_ind_r A (mult zero zero)
529 (\lambda x_Demod_524:A.(eq A (add zero (add y x_Demod_524)) (add zero (mult (add y zero) y))))
530 (eq_ind_r A (mult y (add y zero))
531 (\lambda x_SupR_628:A.(eq A (add zero x_SupR_628) (add zero (mult (add y zero) y))))
532 (eq_ind_r A (mult (add zero (add y zero)) (add zero y))
533 (\lambda x_Demod_195:A.(eq A (add zero (mult y (add y zero))) x_Demod_195))
534 (eq_ind_r A (mult (add zero y) (add zero (add y zero)))
535 (\lambda x_SupR_272:A.(eq A x_SupR_272 (mult (add zero (add y zero)) (add zero y)))) (H1 (add zero y) (add zero (add y zero))) (add zero (mult y (add y zero))) (H2 zero y (add y zero))) (add zero (mult (add y zero) y)) (H2 zero (add y zero) y)) (add y (mult zero zero))
536 (eq_ind A (add y zero)
537 (\lambda x_SupR_296:A.(eq A (add y (mult zero zero)) (mult x_SupR_296 (add y zero)))) (H2 y zero zero) y (H4 y))) zero
538 (eq_ind A (mult zero one)
539 (\lambda x_Demod_507:A.(eq A x_Demod_507 (mult zero zero)))
540 (eq_ind_r A (add zero one)
541 (\lambda x_Demod_506:A.(eq A (mult zero x_Demod_506) (mult zero zero)))
542 (eq_ind_r A (inv zero)
543 (\lambda x_SupR_785:A.(eq A (mult zero (add zero x_SupR_785)) (mult zero zero)))
544 (eq_ind A (add (mult zero zero) zero)
545 (\lambda x_Demod_223:A.(eq A (mult zero (add zero (inv zero))) x_Demod_223))
546 (eq_ind A (mult zero (inv zero))
547 (\lambda x_SupR_337:A.(eq A (mult zero (add zero (inv zero))) (add (mult zero zero) x_SupR_337))) (H3 zero zero (inv zero)) zero (H7 zero)) (mult zero zero) (H4 (mult zero zero))) one
548 (eq_ind A (add (inv zero) zero)
549 (\lambda x_SupR_463:A.(eq A one x_SupR_463))
550 (eq_ind A (add zero (inv zero))
551 (\lambda x_SupR_298:A.(eq A x_SupR_298 (add (inv zero) zero))) (H zero (inv zero)) one (H6 zero)) (inv zero) (H4 (inv zero)))) one
552 (eq_ind A (add zero (inv zero))
553 (\lambda x_Demod_268:A.(eq A x_Demod_268 (add zero one)))
554 (eq_ind A (mult (inv zero) one) (\lambda x_SupR_396:A.(eq A (add zero x_SupR_396) (add zero one)))
555 (eq_ind_r A (mult one (add zero one))
556 (\lambda x_Demod_199:A.(eq A (add zero (mult (inv zero) one)) x_Demod_199))
557 (eq_ind A (add zero (inv zero))
558 (\lambda x_SupR_268:A.(eq A (add zero (mult (inv zero) one)) (mult x_SupR_268 (add zero one)))) (H2 zero (inv zero) one) one (H6 zero)) (add zero one)
559 (eq_ind A (mult (add zero one) one)
560 (\lambda x_SupR_271:A.(eq A x_SupR_271 (mult one (add zero one)))) (H1 (add zero one) one) (add zero one) (H5 (add zero one)))) (inv zero) (H5 (inv zero))) one (H6 zero))) zero (H5 zero))) y (H4 y))) y
561 (eq_ind A (add y zero)
562 (\lambda x_SupR_299:A.(eq A x_SupR_299 (add zero y))) (H y zero) y (H4 y))))) (add x y)
563 (sym_eq\subst[A \Assign A ; x \Assign (add x y) ; y \Assign x]
564 (eq_ind_r A (add zero x)
565 (\lambda x_SupR_826:A.(eq A (add x y) x_SupR_826))
566 (eq_ind_r A (add zero (mult (add x zero) x))
567 (\lambda x_Demod_553:A.(eq A (add x y) x_Demod_553))
568 (eq_ind A (add (add x y) zero)
569 (\lambda x_Demod_540:A.(eq A x_Demod_540 (add y (mult (add x y) x))))
570 (eq_ind_r A (mult zero y)
571 (\lambda x_Demod_526:A.(eq A (add (add x y) x_Demod_526) (add y (mult (add x y) x))))
572 (eq_ind_r A (mult (add x y) (add (add x y) y))
573 (\lambda x_SupR_606:A.(eq A (add (add x y) (mult zero y)) x_SupR_606))
574 (eq_ind A (add (add x y) zero)
575 (\lambda x_SupR_296:A.(eq A (add (add x y) (mult zero y)) (mult x_SupR_296 (add (add x y) y)))) (H2 (add x y) zero y) (add x y) (H4 (add x y))) (add y (mult (add x y) x))
577 (\lambda x_SupR_357:A.(eq A (add y (mult (add x y) x)) (mult x_SupR_357 (add (add x y) y))))
578 (eq_ind A (mult (add (add x y) y) (add y x))
579 (\lambda x_SupR_310:A.(eq A (add y (mult (add x y) x)) x_SupR_310))
580 (eq_ind A (add y (add x y))
581 (\lambda x_SupR_302:A.(eq A (add y (mult (add x y) x)) (mult x_SupR_302 (add y x)))) (H2 y (add x y) x) (add (add x y) y) (H y (add x y))) (mult (add y x) (add (add x y) y)) (H1 (add (add x y) y) (add y x))) (add x y) (H y x))) zero
582 (eq_ind A (mult zero one)
583 (\lambda x_Demod_507:A.(eq A x_Demod_507 (mult zero y)))
584 (eq_ind_r A (add y one)
585 (\lambda x_Demod_506:A.(eq A (mult zero x_Demod_506) (mult zero y)))
586 (eq_ind_r A (inv zero)
587 (\lambda x_SupR_785:A.(eq A (mult zero (add y x_SupR_785)) (mult zero y)))
588 (eq_ind A (add (mult zero y) zero)
589 (\lambda x_Demod_223:A.(eq A (mult zero (add y (inv zero))) x_Demod_223))
590 (eq_ind A (mult zero (inv zero))
591 (\lambda x_SupR_337:A.(eq A (mult zero (add y (inv zero))) (add (mult zero y) x_SupR_337))) (H3 zero y (inv zero)) zero (H7 zero)) (mult zero y) (H4 (mult zero y))) one
592 (eq_ind A (add (inv zero) zero)
593 (\lambda x_SupR_463:A.(eq A one x_SupR_463))
594 (eq_ind A (add zero (inv zero))
595 (\lambda x_SupR_298:A.(eq A x_SupR_298 (add (inv zero) zero))) (H zero (inv zero)) one (H6 zero)) (inv zero) (H4 (inv zero)))) one
596 (eq_ind A (add y (inv y))
597 (\lambda x_Demod_268:A.(eq A x_Demod_268 (add y one)))
598 (eq_ind A (mult (inv y) one)
599 (\lambda x_SupR_396:A.(eq A (add y x_SupR_396) (add y one)))
600 (eq_ind_r A (mult one (add y one))
601 (\lambda x_Demod_199:A.(eq A (add y (mult (inv y) one)) x_Demod_199))
602 (eq_ind A (add y (inv y))
603 (\lambda x_SupR_268:A.(eq A (add y (mult (inv y) one)) (mult x_SupR_268 (add y one)))) (H2 y (inv y) one) one (H6 y)) (add y one)
604 (eq_ind A (mult (add y one) one)
605 (\lambda x_SupR_271:A.(eq A x_SupR_271 (mult one (add y one)))) (H1 (add y one) one) (add y one) (H5 (add y one)))) (inv y) (H5 (inv y))) one (H6 y))) zero (H5 zero))) (add x y) (H4 (add x y))) (add zero x)
606 (eq_ind A (add x zero)
607 (\lambda x_Demod_543:A.(eq A (add zero x_Demod_543) (add zero (mult (add x zero) x))))
608 (eq_ind_r A (mult zero zero)
609 (\lambda x_Demod_524:A.(eq A (add zero (add x x_Demod_524)) (add zero (mult (add x zero) x))))
610 (eq_ind_r A (mult x (add x zero))
611 (\lambda x_SupR_628:A.(eq A (add zero x_SupR_628) (add zero (mult (add x zero) x))))
612 (eq_ind_r A (mult (add zero (add x zero)) (add zero x))
613 (\lambda x_Demod_195:A.(eq A (add zero (mult x (add x zero))) x_Demod_195))
614 (eq_ind_r A (mult (add zero x) (add zero (add x zero)))
615 (\lambda x_SupR_272:A.(eq A x_SupR_272 (mult (add zero (add x zero)) (add zero x)))) (H1 (add zero x) (add zero (add x zero))) (add zero (mult x (add x zero))) (H2 zero x (add x zero))) (add zero (mult (add x zero) x)) (H2 zero (add x zero) x)) (add x (mult zero zero))
616 (eq_ind A (add x zero)
617 (\lambda x_SupR_296:A.(eq A (add x (mult zero zero)) (mult x_SupR_296 (add x zero)))) (H2 x zero zero) x (H4 x))) zero
618 (eq_ind A (mult zero one)
619 (\lambda x_Demod_507:A.(eq A x_Demod_507 (mult zero zero)))
620 (eq_ind_r A (add zero one)
621 (\lambda x_Demod_506:A.(eq A (mult zero x_Demod_506) (mult zero zero)))
622 (eq_ind_r A (inv zero)
623 (\lambda x_SupR_785:A.(eq A (mult zero (add zero x_SupR_785)) (mult zero zero)))
624 (eq_ind A (add (mult zero zero) zero)
625 (\lambda x_Demod_223:A.(eq A (mult zero (add zero (inv zero))) x_Demod_223))
626 (eq_ind A (mult zero (inv zero))
627 (\lambda x_SupR_337:A.(eq A (mult zero (add zero (inv zero))) (add (mult zero zero) x_SupR_337))) (H3 zero zero (inv zero)) zero (H7 zero)) (mult zero zero) (H4 (mult zero zero))) one
628 (eq_ind A (add (inv zero) zero)
629 (\lambda x_SupR_463:A.(eq A one x_SupR_463))
630 (eq_ind A (add zero (inv zero))
631 (\lambda x_SupR_298:A.(eq A x_SupR_298 (add (inv zero) zero))) (H zero (inv zero)) one (H6 zero)) (inv zero) (H4 (inv zero)))) one
632 (eq_ind A (add zero (inv zero))
633 (\lambda x_Demod_268:A.(eq A x_Demod_268 (add zero one)))
634 (eq_ind A (mult (inv zero) one)
635 (\lambda x_SupR_396:A.(eq A (add zero x_SupR_396) (add zero one)))
636 (eq_ind_r A (mult one (add zero one))
637 (\lambda x_Demod_199:A.(eq A (add zero (mult (inv zero) one)) x_Demod_199))
638 (eq_ind A (add zero (inv zero))
639 (\lambda x_SupR_268:A.(eq A (add zero (mult (inv zero) one)) (mult x_SupR_268 (add zero one)))) (H2 zero (inv zero) one) one (H6 zero)) (add zero one)
640 (eq_ind A (mult (add zero one) one)
641 (\lambda x_SupR_271:A.(eq A x_SupR_271 (mult one (add zero one)))) (H1 (add zero one) one) (add zero one) (H5 (add zero one)))) (inv zero) (H5 (inv zero))) one (H6 zero))) zero (H5 zero))) x (H4 x))) x
642 (eq_ind A (add x zero)
643 (\lambda x_SupR_299:A.(eq A x_SupR_299 (add zero x))) (H x zero) x (H4 x))))) (add (add x (mult y z)) y)
644 (sym_eq\subst[A \Assign A ; x \Assign (add (add x (mult y z)) y) ; y \Assign (add y (add x (mult y z)))] (H (add x (mult y z)) y)))
653 \forall add: A \to A \to A.
654 \forall mult: A \to A \to A.
655 \forall inv: A \to A.
656 \forall c1:(\forall x,y:A.(add x y) = (add y x)).
657 \forall c2:(\forall x,y:A.(mult x y) = (mult y x)).
658 \forall d1: (\forall x,y,z:A.
659 (add x (mult y z)) = (mult (add x y) (add x z))).
660 \forall d2: (\forall x,y,z:A.
661 (mult x (add y z)) = (add (mult x y) (mult x z))).
662 \forall i1: (\forall x:A. (add x zero) = x).
663 \forall i2: (\forall x:A. (mult x one) = x).
664 \forall inv1: (\forall x:A. (add x (inv x)) = one).
665 \forall inv2: (\forall x:A. (mult x (inv x)) = zero).
667 (inv (mult x y)) = (add (inv x) (inv y)).
668 intros.auto paramodulation.