Theorem IL-1. A single axiom for inverse loops.

\{x · ((((x · y′) · y)′ · z) · (u′ · u)) = z\} ⇔ \{ \begin{matrix}x′ · x = y′ · y \\ x′ · (x · y) = y \\ (x · y) · y′ = x \end{matrix} \} .

We prove (⇒) in two steps, first showing that x′ · x is a constant, then including x′ · x = 1 to derive the right-hand side. The third Otter proof is (⇐).

Proof (found by Otter 3.0.4 on gyro at 0.46 seconds).

1 A′ · A = B′ · B → □ 4,3 x · ((((x · y′) · y)′ · z) · (u′ · u)) = z

5  x · (y · (z′ · z)) = (((((x · u′) · u)′ · v′) · v)′ · y) · (w′ · w)  [3 → 3]
6  (((((x · y′) · y)′ · z′) · z)′ · u) · (v′ · v) = x · (u · (w′ · w))  [flip 5]
28  x · (y · (z′ · z)) = x · (y · (u′ · u))  [6 → 6]
64  x · (y′ · y) = x · (z′ · z)  [28 → 3 :4]
84  x′ · x = y′ · y  [64 → 3 :4]
85  □  [84,1]

Proof (⇒) found by Otter 3.0.4 on gyro at 0.66 seconds.

1 x = x 2 B′ · B = A′ · A, A′ · (A · B) = B, (A · B) · B′ = A → □ 3 x · ((((x · y′) · y)′ · z) · (u′ · u)) = z 6,5 x′ · x = 1

7  x · ((((x · y′) · y)′ · z) · 1) = z  [3 :6]
9  A′ · (A · B) = B, (A · B) · B′ = A → □  [2 :6,6 :1]
10  x′′ · (((1 · x)′ · y) · 1) = y  [5 → 7]
12  (((((x · y′) · y)′ · z′) · z)′ · u) · 1 = x · (u · 1)  [7 → 7, flip]
15,14  (x · y′) · y = x · (1 · 1)  [5 → 7, flip]
17,16  (((x · (1 · 1))′ · (1 · 1))′ · y) · 1 = x · (y · 1)  [12 :15,15]
18  x · (((x · (1 · 1))′ · y) · 1) = y  [7 :15]
23,22  x′′ · (1 · 1) = 1 · x  [5 → 14, flip]
24  x′′ · ((1 · x)′ · (1 · 1)) = 1′  [14 → 10]
28  (1 · 1)′ · ((1′ · x) · 1) = x  [5 → 18]
36  ((1′ · (1 · 1))′ · x) · 1 = (1 · 1)′ · (x · 1)  [18 → 28, flip]
39,38  (1 · 1)′ · (1′ · (1 · 1)) = 1′  [14 → 28]
40  1′′ · (x · 1) = (1′ · x) · 1  [28 → 10]
42  1′′ · 1 = 1′ · (1 · 1)  [38 → 10 :6]
44  (x · (1 · 1)′) · (y · 1) = x · (y · 1)  [14 → 16 :17, flip]
48  (x · (1 · 1))′ · (x · (y · 1)) = y  [16 → 18]
55  (1′ · ((1 · 1)′ · x)) · 1 = x  [18 → 40 :23, flip]
66  1′ · ((1 · 1)′ · (x · 1)) = x  [5 → 48]
69,68  (x · (1 · 1))′ · (x · y) = 1′ · ((1 · 1)′ · y)  [55 → 48]
71,70  1′′ = 1′ · 1′  [42 → 48 :69,39, flip]
75  1′ · ((1 · 1)′ · (x · (1 · 1))) = x · 1′  [14 → 48 :69]

82  ((x · 1)′ · (1 · 1))′ · 1 = x  [5 → 48]
104  (1′ · 1′) · (1 · 1) = 1 · 1  [70 → 22]
110  (1′ · 1′)′ · (((1 · 1′)′ · x) · 1) = x  [70 → 10]
121,120 1′ · (1 · 1) = 1′  [70 → 24 :6,15]
124  (1 · 1)′ · 1′ = 1′  [38 :121]
126  ((1′ · 1′) · x) · 1 = (1 · 1)′ · (x · 1)  [36 :121,71]
127  (1 · 1)′ · (x · 1) = ((1′ · 1′) · x) · 1  [flip 126]
128  (1 · 1)′ · 1 = 1 · 1  [120 → 28 :6]
137,136 (1 · 1)′ = 1  [128 → 66 :6,6, flip]
142,141 ((1′ · 1′) · x) · 1 = 1 · (x · 1)  [127 :137, flip]
144,143 1 · 1′ = 1′  [124 :137]
149  1′ · (1 · (x · (1 · 1))) = x · 1′  [75 :137]
151  (x · (1 · 1))′ · (x · y) = 1′ · (1 · y)  [68 :137]
158,157 (x · 1) · (y · 1) = x · (y · 1)  [44 :137]
162 (1′ · 1′)′ · (1 · (x · 1)) = x [110 :144,71,142]
173,172 1′ = 1 · (1 · 1)  [136 → 22 :121]
177,176 1 · (1 · 1) = 1  [136 → 5]
187,186 1 · (1 · (x · 1)) = x  [162 :173,177,173,177,137]
195,194 1 · 1 = 1  [104 :173,177,173,177,158,177, flip]
202 (x · 1)′ · (x · y) = 1 · (1 · y) [151 :195,173,195,195]
206,205 x · 1 = x  [149 :173,195,195,195,187,173,195,195, flip]
226,225 x′′ = x  [82 :206,206,206,206]
232,231 1 · x = x  [22 :226,206,206, flip]
235 (x · y′) · y = x [14 :206,206]
238,237 x′ · (x · y) = y  [202 :206,232,232]
239  (A · B) · B′ = A → □  [9 :238 :1]
244  (x · y) · y′ = x  [225 → 235]
246  □  [244,239]

Proof (⇐) found by Otter 3.0.4 on gyro at 0.08 seconds.

1 x = x 2 A · ((((A · B′) · B)′ · C) · (D′ · D)) = C → □ 3 x′ · x = y′ · y 4 x′ · (x · y) = y 6 (x · y) · y′ = x

8  A · ((((A · B′) · B)′ · C) · (x′ · x)) = C → □  [3 → 2]
10,9  x′′ · y = x · y  [4 → 4]
12,11  x · (y′ · y) = x  [3 → 4 :10]
13  A · (((A · B′) · B)′ · C) = C → □  [8 :12]
24  x′′ = x  [4 → 11, flip]
31,30  (x · y′) · y = x  [24 → 6]
33,32  x · (x′ · y) = y  [24 → 4]
35  C = C → □  [13 :31,33]
36  □  [35,1]