Lemma IL-2. Inverse loop schema gives inverse loop basis.

{β = α} ⇒

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

As for Thm. IL-1, 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 1.28 seconds).

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

7,6  x · ((((x · y′) · y)′ · z) · ((α · u)′ · (α · u))) = z  [copy,5 :4]
10,9  x · ((((x · y′) · y)′ · z) · (u′ · u)) = z  [6 → 6 :7]
12  x · (y · (z′ · z)) = (((((x · u′) · u)′ · v′) · v)′ · y) · (w′ · w)  [9 → 9]
13  (((((x · y′) · y)′ · z′) · z)′ · u) · (v′ · v) = x · (u · (w′ · w))  [flip 12]
35  x · (y · (z′ · z)) = x · (y · (u′ · u))  [13 → 13]
141  x · (y′ · y) = x · (z′ · z)  [35 → 9 :10]
174  x′ · x = y′ · y  [141 → 9 :10]
175  □  [174,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 → □ 4,3 β = α 6,5 x′ · x = 1 7 x · ((((x · y′) · y)′ · z) · ((α · u)′ · (β · u))) = z

8  x · ((((x · y′) · y)′ · z) · 1) = z  [copy,7 :4,6]
10  A′ · (A · B) = B, (A · B) · B′ = A → □  [2 :6,6 :1]
11  x′′ · (((1 · x)′ · y) · 1) = y  [5 → 8]
13  (((((x · y′) · y)′ · z′) · z)′ · u) · 1 = x · (u · 1)  [8 → 8, flip]
16,15  (x · y′) · y = x · (1 · 1)  [5 → 8, flip]
18,17  (((x · (1 · 1))′ · (1 · 1))′ · y) · 1 = x · (y · 1)  [13 :16,16]
19  x · (((x · (1 · 1))′ · y) · 1) = y  [8 :16]
24,23  x′′ · (1 · 1) = 1 · x  [5 → 15, flip]
25  x′′ · ((1 · x)′ · (1 · 1)) = 1′  [15 → 11]
29  (1 · 1)′ · ((1′ · x) · 1) = x  [5 → 19]
37  ((1′ · (1 · 1))′ · x) · 1 = (1 · 1)′ · (x · 1)  [19 → 29, flip]
40,39  (1 · 1)′ · (1′ · (1 · 1)) = 1′  [15 → 29]
41  1′′ · (x · 1) = (1′ · x) · 1  [29 → 11]

43  1′′ · 1 = 1′ · (1 · 1)  [39 → 11 :6]
45  (x · (1 · 1)′) · (y · 1) = x · (y · 1)  [15 → 17 :18, flip]
49  (x · (1 · 1))′ · (x · (y · 1)) = y  [17 → 19]
56  (1′ · ((1 · 1)′ · x)) · 1 = x  [19 → 41 :24, flip]
73  1′ · ((1 · 1)′ · (x · 1)) = x  [5 → 49]
76,75  (x · (1 · 1))′ · (x · y) = 1′ · ((1 · 1)′ · y)  [56 → 49]
78,77  1′′ = 1′ · 1′  [43 → 49 :76,40, flip]
82  1′ · ((1 · 1)′ · (x · (1 · 1))) = x · 1′  [15 → 49 :76]
89  ((x · 1)′ · (1 · 1))′ · 1 = x  [5 → 49]
104  x · 1′ = 1′ · ((1 · 1)′ · (x · (1 · 1)))  [flip 82]
107  (1′ · 1′) · (1 · 1) = 1 · 1  [77 → 23]
117  (1′ · 1′)′ · (((1 · 1′)′ · x) · 1) = x  [77 → 11]
124,123 1′ · (1 · 1) = 1′  [77 → 25 :6,16]
127  (1 · 1)′ · 1′ = 1′  [39 :124]
129  ((1′ · 1′) · x) · 1 = (1 · 1)′ · (x · 1)  [37 :124,78]
130  (1 · 1)′ · (x · 1) = ((1′ · 1′) · x) · 1  [flip 129]
131  (1 · 1)′ · 1 = 1 · 1  [123 → 29 :6]
142,141 (1 · 1)′ = 1  [131 → 73 :6,6, flip]
149,148 ((1′ · 1′) · x) · 1 = 1 · (x · 1)  [130 :142, flip]
151,150 1 · 1′ = 1′  [127 :142]
152  x · 1′ = 1′ · (1 · (x · (1 · 1)))  [104 :142]
156  (x · (1 · 1))′ · (x · y) = 1′ · (1 · y)  [75 :142]
163,162 (x · 1) · (y · 1) = x · (y · 1)  [45 :142]
171 (1′ · 1′)′ · (1 · (x · 1)) = x [117 :151,78,149]
192,191 1′ = 1 · (1 · 1)  [141 → 23 :124]
196,195 1 · (1 · 1) = 1  [141 → 5]
200,199 1 · 1 = 1  [107 :192,196,192,196,163,196, flip]
204,203 1 · (1 · (x · 1)) = x [171 :192,200,200,192,200,200,200,192,200,200]
219 (x · 1)′ · (x · y) = 1 · (1 · y) [156 :200,192,200,200]
223,222 x · 1 = x  [152 :192,200,200,192,200,200,200,204]
237,236 x′′ = x  [89 :223,223,223,223]
247,246 1 · x = x  [23 :237,223,223, flip]
250 (x · y′) · y = x [15 :223,223]
253,252 x′ · (x · y) = y  [219 :223,247,247]
254  (A · B) · B′ = A → □  [10 :253 :1]
255  (x · y) · y′ = x  [236 → 250]
257  □  [255,254]

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

2 A · ((((A · B′) · B)′ · C) · ((α · D)′ · (β · D))) = C → □ 4,3 β = α 5 x′ · x = y′ · y 7,6 x′ · (x · y) = y 8 (x · y) · y′ = x

10  A · ((((A · B′) · B)′ · C) · ((α · D)′ · (α · D))) = C → □  [2 :4]

12,11  x′′ · y = x · y  [6 → 6]^{15  x · (y · x)′ = y′  [6 → 8]}^{22,21  x · (y′ · y) = x  [5 → 6 :12]}^{23  A · (((A · B′) · B)′ · C) = C → □  [10 :22]}^{27,26  x′′ = x  [6 → 21, flip]}^{31,30  (x · y)′ = y′ · x′  [8 → 15, flip]}^{32  A · (A′ · C) = C → □  [23 :31,31,27,7]}^{41  x · (x′ · y) = y  [26 → 6]}^{43  □  [41,32]}

3