%
Length of proof is 13.
%
Level of proof is 7.
%
Maximum clause weight is 15.
%
Given clauses 11.
1
(A / A) * x = x # label(non_clause) #
label(goal). [goal].
2
A * (A \ x) = x. [assumption].
3
A \ (A * x) = x. [assumption].
4
(x * A) / A = x. [assumption].
5
A * ((x * y) * A) = (A * x) * (y * A).
[assumption].
6
(A * x) * (y * A) = A * ((x * y) * A).
[copy(5),flip(a)].
11
(A / A) * c1 != c1. [deny(1)].
12
A * (((A \ x) * y) * A) = x * (y * A).
[para(2(a,1),6(a,1,1)),flip(a)].
21
A \ (x * (y * A)) = ((A \ x) * y) * A.
[para(12(a,1),3(a,1,2))].
25
((A \ A) * x) * A = x * A. [para(21(a,1),3(a,1))].
26
(A \ A) * x = x. [para(25(a,1),4(a,1,1)),rewrite([4(4)]),flip(a)].
27
A / A = A \ A. [para(26(a,1),4(a,1,1))].
34 $F. [back_rewrite(11),rewrite([27(3),26(5)]),xx(a)].
==============================
end of proof ==========================
%
Length of proof is 41.
%
Level of proof is 17.
%
Maximum clause weight is 19.
%
Given clauses 41.
1
x * (A / A) = x # label(non_clause) #
label(goal). [goal].
2
A * (A \ x) = x. [assumption].
3
A \ (A * x) = x. [assumption].
4
(x * A) / A = x. [assumption].
5
A * ((x * y) * A) = (A * x) * (y * A).
[assumption].
6
(A * x) * (y * A) = A * ((x * y) * A).
[copy(5),flip(a)].
7
x * ((A * y) * x) = (x * A) * (y * x).
[assumption].
8
(x * A) * (y * x) = x * ((A * y) * x).
[copy(7),flip(a)].
9
x * ((y * A) * x) = (x * y) * (A * x).
[assumption].
10
(x * y) * (A * x) = x * ((y * A) * x).
[copy(9),flip(a)].
11
c1 * (A / A) != c1. [deny(1)].
12
A * (((A \ x) * y) * A) = x * (y * A).
[para(2(a,1),6(a,1,1)),flip(a)].
21
A \ (x * (y * A)) = ((A \ x) * y) * A.
[para(12(a,1),3(a,1,2))].
25
((A \ A) * x) * A = x * A. [para(21(a,1),3(a,1))].
26
(A \ A) * x = x. [para(25(a,1),4(a,1,1)),rewrite([4(4)]),flip(a)].
27
A / A = A \ A. [para(26(a,1),4(a,1,1))].
29
(A * x) * (A \ A) = A * (x * (A \ A)).
[para(26(a,1),8(a,1,1)),rewrite([26(16)]=),flip(a)].
31
(x * A) * (A \ A) = x * A. [para(26(a,1),10(a,2)),rewrite([26(4),2(5)]),flip(a)].
32
((A \ x) * (A \ A)) * A = A \ (x * A).
[para(26(a,1),21(a,1,2,2)),flip(a)].
33
((A \ (A \ A)) * x) * A = A \ (x * A).
[para(26(a,1),21(a,1,2)),flip(a)].
34
c1 * (A \ A) != c1. [back_rewrite(11),rewrite([27(4)])].
55
(A * (x * A)) * A = A * ((x * A) * A).
[para(31(a,1),6(a,2,2,1)),rewrite([26(9)])].
87
A * ((A \ x) * (A \ A)) = x * (A \ A).
[para(2(a,1),29(a,1,1)),flip(a)].
90
(x * (y * A)) * (A \ A) = x * (y * A).
[para(12(a,1),29(a,1,1)),rewrite([31(17),12(14)])].
93
(A \ (x * A)) / A = (A \ x) * (A \ A).
[para(32(a,1),4(a,1,1))].
95
(x * (A \ A)) * (A * A) = A * ((A \ (x * A)) * A). [para(32(a,1),6(a,2,2,1)),rewrite([87(8)])].
102
(A \ (x * A)) * (A \ A) = A \ (x * A).
[para(32(a,1),31(a,1,1)),rewrite([32(16)])].
104
(A \ (A \ A)) * x = (A \ x) * (A \ A).
[para(33(a,1),4(a,1,1)),rewrite([93(6)]),flip(a)].
111
(A * ((x * A) * A)) / A = A * (x * A).
[para(55(a,1),4(a,1,1))].
121
A * ((A \ (x * A)) * A) = (x * A) * A.
[para(32(a,1),55(a,1,1,2)),rewrite([2(6),32(13)]),flip(a)].
127
(x * (A \ A)) * (A * A) = (x * A) * A.
[back_rewrite(95),rewrite([121(16)])].
205
(A \ (A \ A)) * A = A \ A. [para(104(a,2),26(a,1))].
211
(x * (A \ A)) * (A \ A) = x * (A \ A).
[para(104(a,1),90(a,1,1,2)),rewrite([26(7),205(15)])].
248
(x * (A * A)) / A = A * ((A \ x) * A).
[para(12(a,1),111(a,1,1))].
307
(A \ (x * A)) * A = ((A \ x) * A) * A.
[para(32(a,1),127(a,2,1)),rewrite([211(10),127(10)]),flip(a)].
334
(x * A) * A = x * (A * A). [back_rewrite(121),rewrite([307(7),12(8)]),flip(a)].
427
A * ((A \ x) * A) = x * A. [para(334(a,1),4(a,1,1)),rewrite([248(6)])].
436
A \ (x * A) = (A \ x) * A. [para(334(a,1),93(a,1,1,2)),rewrite([21(6),334(6),248(8),427(8),102(12)]),flip(a)].
472
(A \ x) * (A \ A) = A \ x. [back_rewrite(93),rewrite([436(4),4(6)]),flip(a)].
524
x * (A \ A) = x. [back_rewrite(87),rewrite([472(7),2(4)]),flip(a)].
525 $F. [resolve(524,a,34,a)].
==============================
end of proof ==========================
% Length of proof is 40.
% Level of proof is 13.
% Maximum clause weight is 19.
% Given clauses 69.
1 (A / A) * x = x # label(non_clause)
# label(goal). [goal].
2 A * (A \ x) = x. [assumption].
3 A \ (A * x) = x. [assumption].
4 (x / A) * A = x. [assumption].
5 A * ((x * y) * A) = (A * x) * (y * A). [assumption].
6 (A * x) * (y * A) = A * ((x * y) * A). [copy(5),flip(a)].
7 x * ((A * y) * x) = (x * A) * (y * x). [assumption].
8 (x * A) * (y * x) = x * ((A * y) * x). [copy(7),flip(a)].
9 x * ((y * A) * x) = (x * y) * (A * x). [assumption].
10 (x * y) * (A * x) = x * ((y * A) * x). [copy(9),flip(a)].
11 (A / A) * c1 !=
c1. [deny(1)].
12 A * (((A \ x) * y) * A) = x * (y * A). [para(2(a,1),6(a,1,1)),flip(a)].
13 A * ((x * (y / A)) * A) = (A * x) * y. [para(4(a,1),6(a,1,2)),flip(a)].
15 (x / A) * ((A * y) * (x / A)) = x * (y * (x
/ A)). [para(4(a,1),8(a,1,1)),flip(a)].
18 (A \ x) * ((y * A) * (A \ x)) = ((A \ x) *
y) * x. [para(2(a,1),10(a,1,2)),flip(a)].
23 A \ (x * (y * A)) = ((A \ x) * y) * A. [para(12(a,1),3(a,1,2))].
27 A \ ((A * x) * y) = (x * (y / A)) * A. [para(13(a,1),3(a,1,2))].
31 ((A \ A) * x) * A = x * A. [para(23(a,1),3(a,1))].
32 ((A \ x) * (y / A)) * A = A \ (x * y). [para(4(a,1),23(a,1,2,2)),flip(a)].
36 (x * ((y * A) / A)) * A = (x * y) * A. [para(6(a,1),27(a,1,2)),rewrite([23(7),31(7)]),flip(a)].
39 (x / A) * (y * (x / A)) = x * ((A \ y) * (x
/ A)). [para(2(a,1),15(a,1,2,1))].
83 ((A \ x) * (y / A)) * x = (A \ x) * (y * (A
\ x)). [para(4(a,1),18(a,1,2,1)),flip(a)].
89 (A \ A) * (x * (A \ A)) = x. [para(32(a,1),18(a,2)),rewrite([4(7),3(12)])].
95 (A \ A) * A = A. [para(2(a,1),89(a,1,2))].
98 A * (x * (A \ A)) = A * x. [para(89(a,1),8(a,2)),rewrite([95(5)])].
99 (x * (A \ A)) * A = x * A. [para(89(a,1),31(a,1,1)),flip(a)].
112 A \ (x * A) = (A \ x) * A. [para(95(a,1),23(a,1,2,2)),rewrite([99(12)])].
113 (x * (A / A)) * A = x * A. [para(95(a,1),36(a,1,1,2,1)),rewrite([99(12)])].
132 x * (A \ A) = x. [para(98(a,1),3(a,1,2)),rewrite([3(4)]),flip(a)].
133 (A \ A) * x = x. [para(98(a,1),32(a,2,2)),rewrite([132(7),83(8),132(7),3(8)])].
155 (x * ((A \ A) / A)) * A = x. [para(132(a,1),27(a,1,2)),rewrite([3(4)]),flip(a)].
287 (A \ (x / A)) * A = A \ x. [para(4(a,1),112(a,1,2)),flip(a)].
290 (A \ (A \ A)) * A = A \ A. [para(133(a,1),112(a,1,2)),flip(a)].
297 (x * (y * (A / A))) * A = (x * y) * A. [para(113(a,1),36(a,1,1,2,1)),rewrite([36(7)]),flip(a)].
383 (x * ((A \ y) / A)) * A = (x * (A \ (y /
A))) * A. [para(287(a,1),36(a,1,1,2,1))].
389 (x * (A \ (A / A))) * A = x. [back_rewrite(155),rewrite([383(8)])].
395 (x * (A \ (A \ A))) * A = x. [para(290(a,1),36(a,1,1,2,1)),rewrite([383(8),389(8)]),flip(a)].
757 ((A / A) * x) * A = x * A. [para(39(a,1),297(a,1,1)),rewrite([297(10),2(4)]),flip(a)].
770 A / A = A \ A. [para(290(a,1),757(a,2)),rewrite([395(11)])].
773 $F. [back_rewrite(11),rewrite([770(3),133(5)]),xx(a)].
============================== end of proof ==========================
% Length of proof is 40.
% Level of proof is 13.
% Maximum clause weight is 19.
% Given clauses 69.
1 x * (A / A) = x # label(non_clause)
# label(goal). [goal].
2 A * (A \ x) = x. [assumption].
3 A \ (A * x) = x. [assumption].
4 (x / A) * A = x. [assumption].
5 A * ((x * y) * A) = (A * x) * (y * A). [assumption].
6 (A * x) * (y * A) = A * ((x * y) * A). [copy(5),flip(a)].
7 x * ((A * y) * x) = (x * A) * (y * x). [assumption].
8 (x * A) * (y * x) = x * ((A * y) * x). [copy(7),flip(a)].
9 x * ((y * A) * x) = (x * y) * (A * x). [assumption].
10 (x * y) * (A * x) = x * ((y * A) * x). [copy(9),flip(a)].
11 c1 * (A / A) !=
c1. [deny(1)].
12 A * (((A \ x) * y) * A) = x * (y * A). [para(2(a,1),6(a,1,1)),flip(a)].
13 A * ((x * (y / A)) * A) = (A * x) * y. [para(4(a,1),6(a,1,2)),flip(a)].
15 (x / A) * ((A * y) * (x / A)) = x * (y * (x
/ A)). [para(4(a,1),8(a,1,1)),flip(a)].
18 (A \ x) * ((y * A) * (A \ x)) = ((A \ x) *
y) * x. [para(2(a,1),10(a,1,2)),flip(a)].
23 A \ (x * (y * A)) = ((A \ x) * y) * A. [para(12(a,1),3(a,1,2))].
27 A \ ((A * x) * y) = (x * (y / A)) * A. [para(13(a,1),3(a,1,2))].
31 ((A \ A) * x) * A = x * A. [para(23(a,1),3(a,1))].
32 ((A \ x) * (y / A)) * A = A \ (x * y). [para(4(a,1),23(a,1,2,2)),flip(a)].
36 (x * ((y * A) / A)) * A = (x * y) * A. [para(6(a,1),27(a,1,2)),rewrite([23(7),31(7)]),flip(a)].
39 (x / A) * (y * (x / A)) = x * ((A \ y) * (x
/ A)). [para(2(a,1),15(a,1,2,1))].
83 ((A \ x) * (y / A)) * x = (A \ x) * (y * (A
\ x)). [para(4(a,1),18(a,1,2,1)),flip(a)].
89 (A \ A) * (x * (A \ A)) = x. [para(32(a,1),18(a,2)),rewrite([4(7),3(12)])].
95 (A \ A) * A = A. [para(2(a,1),89(a,1,2))].
98 A * (x * (A \ A)) = A * x. [para(89(a,1),8(a,2)),rewrite([95(5)])].
99 (x * (A \ A)) * A = x * A. [para(89(a,1),31(a,1,1)),flip(a)].
112 A \ (x * A) = (A \ x) * A. [para(95(a,1),23(a,1,2,2)),rewrite([99(12)])].
113 (x * (A / A)) * A = x * A. [para(95(a,1),36(a,1,1,2,1)),rewrite([99(12)])].
132 x * (A \ A) = x. [para(98(a,1),3(a,1,2)),rewrite([3(4)]),flip(a)].
133 (A \ A) * x = x. [para(98(a,1),32(a,2,2)),rewrite([132(7),83(8),132(7),3(8)])].
155 (x * ((A \ A) / A)) * A = x. [para(132(a,1),27(a,1,2)),rewrite([3(4)]),flip(a)].
287 (A \ (x / A)) * A = A \ x. [para(4(a,1),112(a,1,2)),flip(a)].
290 (A \ (A \ A)) * A = A \ A. [para(133(a,1),112(a,1,2)),flip(a)].
297 (x * (y * (A / A))) * A = (x * y) * A. [para(113(a,1),36(a,1,1,2,1)),rewrite([36(7)]),flip(a)].
383 (x * ((A \ y) / A)) * A = (x * (A \ (y /
A))) * A. [para(287(a,1),36(a,1,1,2,1))].
389 (x * (A \ (A / A))) * A = x. [back_rewrite(155),rewrite([383(8)])].
395 (x * (A \ (A \ A))) * A = x. [para(290(a,1),36(a,1,1,2,1)),rewrite([383(8),389(8)]),flip(a)].
757 ((A / A) * x) * A = x * A. [para(39(a,1),297(a,1,1)),rewrite([297(10),2(4)]),flip(a)].
770 A / A = A \ A. [para(290(a,1),757(a,2)),rewrite([395(11)])].
773 $F. [back_rewrite(11),rewrite([770(4),132(5)]),xx(a)].
============================== end of proof ==========================
% Length of proof is 57.
% Level of proof is 22.
% Maximum clause weight is 23.
% Given clauses 76.
1 x * (A / A) = x # label(non_clause)
# label(goal). [goal].
2 A * (A \ x) = x. [assumption].
3 (x / A) * A = x. [assumption].
4 A * (A * x) = (A * A) * x. [assumption].
5 (A * A) * x = A * (A * x). [copy(4),flip(a)].
6 A * (x * (A * y)) = ((A * x) * A) * y. [assumption].
7 ((A * x) * A) * y = A * (x * (A * y)). [copy(6),flip(a)].
8 x * (A * (x * y)) = ((x * A) * x) * y. [assumption].
9 ((x * A) * x) * y = x * (A * (x * y)). [copy(8),flip(a)].
10 x * (y * (x * A)) = ((x * y) * x) * A. [assumption].
11 ((x * y) * x) * A = x * (y * (x * A)). [copy(10),flip(a)].
12 c1 * (A / A) !=
c1. [deny(1)].
13 A * ((A \ x) * (A * y)) = (x * A) * y. [para(2(a,1),7(a,1,1,1)),flip(a)].
17 (x * (x / A)) * A = (x / A) * (A * x). [para(3(a,1),9(a,2,2,2)),rewrite([3(4)])].
27 (x * A) * (A \ y) = A * ((A \ x) * y). [para(2(a,1),13(a,1,2,2)),flip(a)].
34 ((A / A) * (A * A)) * x = A * ((A / A) * (A
* x)). [para(17(a,1),7(a,1,1))].
39 A * ((A \ (x / A)) * y) = x * (A \ y). [para(3(a,1),27(a,1,1)),flip(a)].
40 A * ((A \ A) * x) = A * x. [para(27(a,1),5(a,1)),rewrite([2(11)])].
56 x * (A \ (A * y)) = x * y. [para(39(a,1),7(a,2)),rewrite([2(6),3(4)]),flip(a)].
62 x * ((A \ A) * y) = x * y. [para(40(a,1),56(a,1,2,2)),rewrite([56(5)]),flip(a)].
63 x * (A \ (A \ (A * y))) = x * (A \ y). [para(56(a,1),39(a,1,2)),rewrite([39(7)]),flip(a)].
80 A \ (A * x) = x. [para(63(a,1),2(a,1)),rewrite([2(4)]),flip(a)].
84 A \ (x * (A \ y)) = (A \ (x / A)) * y. [para(39(a,1),80(a,1,2))].
85 (A \ A) * x = x. [para(62(a,1),80(a,1,2)),rewrite([80(4)]),flip(a)].
86 (x * (A \ A)) * A = x * A. [para(85(a,1),11(a,1,1,1)),rewrite([85(14),85(12)])].
87 A * ((A \ (A \ A)) * x) = x. [para(85(a,1),27(a,1,1)),rewrite([2(4)]),flip(a)].
88 (A * (x * A)) * A = A * (x * (A * A)). [para(7(a,1),86(a,1,1)),rewrite([2(6),11(12)])].
102 (A \ (A \ A)) * x = A \ x. [para(87(a,1),80(a,1,2)),flip(a)].
103 ((A \ x) * (A \ (A \ A))) * A = (A \ (x /
A)) * A. [para(102(a,1),11(a,1,1,1)),rewrite([102(22),102(20),84(16)])].
118 (A \ ((x * A) / A)) * y = (A \ x) * y. [para(27(a,1),84(a,1,2)),rewrite([80(7)]),flip(a)].
137 A * ((x / A) * (A * A)) = (A * x) * A. [para(3(a,1),88(a,1,1,2)),flip(a)].
174 (A \ ((x * (y * (x * A))) / A)) * z = (A \
((x * y) * x)) * z. [para(11(a,1),118(a,1,1,2,1))].
178 ((A \ (x / A)) * A) * y = (A \ x) * y. [para(86(a,1),118(a,1,1,2,1)),rewrite([118(7),84(9)]),flip(a)].
182 (A \ ((A * x) * A)) * y = (x * A) * y. [para(88(a,1),118(a,1,1,2,1)),rewrite([174(11),80(13)])].
192 A \ ((A * x) * A) = (x / A) * (A * A). [para(137(a,1),80(a,1,2))].
196 ((x / A) * (A * A)) * y = (x * A) * y. [back_rewrite(182),rewrite([192(6)])].
197 A * ((A / A) * (A * x)) = A * (A * x). [back_rewrite(34),rewrite([196(8),5(4)]),flip(a)].
259 (A \ (A \ (x / A))) * y = (A \ ((A \ x) /
A)) * y. [para(178(a,1),84(a,1,2)),rewrite([84(7),118(18)]),flip(a)].
261 (A \ (x * A)) * y = ((A \ x) * A) * y. [para(118(a,1),178(a,1,1)),flip(a)].
278 (((x / A) * (A * A)) / A) * (A * A) = x *
(A * A). [para(137(a,1),192(a,1,2,1)),rewrite([11(7),80(8)]),flip(a)].
320 ((x * A) * A) * y = (x * (A * A)) * y. [para(196(a,1),196(a,2,1)),rewrite([278(12)]),flip(a)].
323 A * ((A / A) * x) = A * x. [para(2(a,1),197(a,1,2,2)),rewrite([2(11)])].
328 (A / A) * (A * x) = A * x. [para(197(a,1),80(a,1,2)),rewrite([80(6)]),flip(a)].
338 (A * (A / A)) * x = A * x. [para(323(a,1),9(a,2,2)),rewrite([3(5),328(12)])].
340 (A / A) * x = x. [para(323(a,1),80(a,1,2)),rewrite([80(4)]),flip(a)].
359 (A \ ((A / A) / A)) * x = A \ (A \ x). [para(340(a,1),84(a,1,2)),flip(a)].
363 (A \ ((A * (A / A)) / A)) * x = A \ x. [para(338(a,1),84(a,1,2)),rewrite([2(5)]),flip(a)].
427 (x * (A * A)) * (A \ y) = A * (((A \ x) *
A) * y). [para(320(a,1),27(a,1)),rewrite([261(13)])].
469 ((A \ x) * (A \ ((A * (A / A)) / A))) * A =
(A \ (x / A)) * A. [para(363(a,1),11(a,1,1,1)),rewrite([363(34),363(28),84(20)])].
571 (A * ((A \ x) * (A \ A))) * A = x * A. [para(192(a,1),103(a,1,1,1)),rewrite([427(12),27(11),259(10),39(11),118(20),80(14)])].
623 (x * (A \ (A \ A))) * A = x. [para(3(a,1),571(a,2)),rewrite([39(10)])].
640 A \ A = A / A. [para(359(a,1),571(a,1,1,2)),rewrite([2(9),102(7),3(10)])].
641 A * (A / A) = A. [para(363(a,1),571(a,1,1,2)),rewrite([640(5),2(7),3(5),3(10)]),flip(a)].
664 (x * (A \ (A / A))) * A = x. [back_rewrite(623),rewrite([640(4)])].
688 (A \ (x / A)) * A = A \ x. [back_rewrite(469),rewrite([641(8),664(10)]),flip(a)].
710 x * (A / A) = x. [para(640(a,1),39(a,2,2)),rewrite([688(7),2(4)]),flip(a)].
711 $F. [resolve(710,a,12,a)].
============================== end of proof ==========================
% Length of proof is 36.
% Level of proof is 17.
% Maximum clause weight is
23.
% Given clauses 47.
1 (A / A) * x = x # label(non_clause) # label(goal). [goal].
2 A * (A \ x) = x. [assumption].
3 (x / A) * A = x. [assumption].
4 A * (A * x) = (A * A) *
x. [assumption].
5 (A * A) * x = A * (A *
x). [copy(4),flip(a)].
6 A * (x * (A * y)) = ((A
* x) * A) * y. [assumption].
7 ((A * x) * A) * y = A *
(x * (A * y)). [copy(6),flip(a)].
8 x * (A * (x * y)) = ((x
* A) * x) * y. [assumption].
9 ((x * A) * x) * y = x *
(A * (x * y)). [copy(8),flip(a)].
10 x * (y * (x * A)) = ((x
* y) * x) * A. [assumption].
11 ((x * y) * x) * A = x *
(y * (x * A)). [copy(10),flip(a)].
12 (A / A) * c1 != c1. [deny(1)].
13 A * ((A \ x) * (A * y))
= (x * A) * y. [para(2(a,1),7(a,1,1,1)),flip(a)].
17 (x * (x / A)) * A = (x
/ A) * (A * x). [para(3(a,1),9(a,2,2,2)),rewrite([3(4)])].
27 (x * A) * (A \ y) = A *
((A \ x) * y). [para(2(a,1),13(a,1,2,2)),flip(a)].
34 ((A / A) * (A * A)) * x
= A * ((A / A) * (A * x)). [para(17(a,1),7(a,1,1))].
39 A * ((A \ (x / A)) * y)
= x * (A \ y). [para(3(a,1),27(a,1,1)),flip(a)].
40 A * ((A \ A) * x) = A *
x. [para(27(a,1),5(a,1)),rewrite([2(11)])].
56 x * (A \ (A * y)) = x *
y. [para(39(a,1),7(a,2)),rewrite([2(6),3(4)]),flip(a)].
62 x * ((A \ A) * y) = x *
y. [para(40(a,1),56(a,1,2,2)),rewrite([56(5)]),flip(a)].
63 x * (A \ (A \ (A * y)))
= x * (A \ y). [para(56(a,1),39(a,1,2)),rewrite([39(7)]),flip(a)].
80 A \ (A * x) = x. [para(63(a,1),2(a,1)),rewrite([2(4)]),flip(a)].
84 A \ (x * (A \ y)) = (A
\ (x / A)) * y. [para(39(a,1),80(a,1,2))].
85 (A \ A) * x = x. [para(62(a,1),80(a,1,2)),rewrite([80(4)]),flip(a)].
86 (x * (A \ A)) * A = x *
A. [para(85(a,1),11(a,1,1,1)),rewrite([85(14),85(12)])].
88 (A * (x * A)) * A = A *
(x * (A * A)). [para(7(a,1),86(a,1,1)),rewrite([2(6),11(12)])].
118 (A \ ((x * A) / A)) *
y = (A \ x) * y. [para(27(a,1),84(a,1,2)),rewrite([80(7)]),flip(a)].
137 A * ((x / A) * (A *
A)) = (A * x) * A. [para(3(a,1),88(a,1,1,2)),flip(a)].
174 (A \ ((x * (y * (x *
A))) / A)) * z = (A \ ((x * y) * x)) * z.
[para(11(a,1),118(a,1,1,2,1))].
182 (A \ ((A * x) * A)) *
y = (x * A) * y. [para(88(a,1),118(a,1,1,2,1)),rewrite([174(11),80(13)])].
192 A \ ((A * x) * A) = (x
/ A) * (A * A). [para(137(a,1),80(a,1,2))].
196 ((x / A) * (A * A)) *
y = (x * A) * y. [back_rewrite(182),rewrite([192(6)])].
197 A * ((A / A) * (A *
x)) = A * (A * x). [back_rewrite(34),rewrite([196(8),5(4)]),flip(a)].
323 A * ((A / A) * x) = A
* x. [para(2(a,1),197(a,1,2,2)),rewrite([2(11)])].
340 (A / A) * x = x. [para(323(a,1),80(a,1,2)),rewrite([80(4)]),flip(a)].
341 $F. [resolve(340,a,12,a)].
==============================
end of proof ==========================