Search for blocks/addresses/...
Proofgold Asset
asset id
efee52a14da720d9a259900d3d23e32e973f49586cde8182f2eb199c28905d13
asset hash
03d37b2bac0a289c870d529c1a3b93c7697a44cfcb43d2f795017d413f8066f4
bday / block
24822
tx
751c8..
preasset
doc published by
Pr5Zc..
Known
45f87..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x1
x2
(
x1
x3
(
x1
x4
x5
)
)
=
x1
x3
(
x1
x4
(
x1
x2
x5
)
)
Theorem
60e4a..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x1
x2
(
x1
x3
(
x1
x4
x5
)
)
=
x1
x3
(
x1
x4
(
x1
x2
x5
)
)
(proof)
Known
93eac..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x6
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x2
x6
)
)
)
Theorem
6024d..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x6
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x2
x6
)
)
)
(proof)
Known
75b00..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x7
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x2
x7
)
)
)
)
Theorem
b4a61..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x7
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x2
x7
)
)
)
)
(proof)
Known
c0c54..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
x8
)
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x2
x8
)
)
)
)
)
Theorem
9b1f7..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
x8
)
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x2
x8
)
)
)
)
)
(proof)
Known
cbdc2..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
x9
)
)
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x2
x9
)
)
)
)
)
)
Theorem
36b70..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
x9
)
)
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x2
x9
)
)
)
)
)
)
(proof)
Known
d3eb2..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
x10
)
)
)
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x2
x10
)
)
)
)
)
)
)
Theorem
792e4..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
x10
)
)
)
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x2
x10
)
)
)
)
)
)
)
(proof)
Known
2a73e..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
x11
)
)
)
)
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x2
x11
)
)
)
)
)
)
)
)
Theorem
59e4d..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
x11
)
)
)
)
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x2
x11
)
)
)
)
)
)
)
)
(proof)
Known
4c672..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
x12
)
)
)
)
)
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x2
x12
)
)
)
)
)
)
)
)
)
Theorem
32c8a..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
x12
)
)
)
)
)
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x2
x12
)
)
)
)
)
)
)
)
)
(proof)
Known
000b3..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
)
)
)
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x2
x13
)
)
)
)
)
)
)
)
)
)
Theorem
542d7..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
)
)
)
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x2
x13
)
)
)
)
)
)
)
)
)
)
(proof)
Known
495ba..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
x14
)
)
)
)
)
)
)
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x2
x14
)
)
)
)
)
)
)
)
)
)
)
Theorem
54f3e..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
x14
)
)
)
)
)
)
)
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x2
x14
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
a1ee1..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
x15
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x2
x15
)
)
)
)
)
)
)
)
)
)
)
)
Theorem
689e8..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
x15
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x2
x15
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
0c618..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x2
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
Theorem
eb077..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x2
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
92560..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x2
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
Theorem
dee36..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x2
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
30837..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x0
x18
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
(
x1
x2
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
Theorem
dad49..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x0
x18
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
(
x1
x2
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
0d20b..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x6
)
)
)
=
x1
x4
(
x1
x5
(
x1
x2
(
x1
x3
x6
)
)
)
Theorem
28124..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x6
)
)
)
=
x1
x4
(
x1
x5
(
x1
x2
(
x1
x3
x6
)
)
)
(proof)
Known
f87dc..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x7
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x2
(
x1
x3
x7
)
)
)
)
Theorem
c9f83..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x7
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x2
(
x1
x3
x7
)
)
)
)
(proof)
Known
3a13f..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
x8
)
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x2
(
x1
x3
x8
)
)
)
)
)
Theorem
a6071..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
x8
)
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x2
(
x1
x3
x8
)
)
)
)
)
(proof)
Known
209c8..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
x8
)
)
)
)
)
=
x1
x5
(
x1
x6
(
x1
x7
(
x1
x2
(
x1
x3
(
x1
x4
x8
)
)
)
)
)
Theorem
50110..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
x8
)
)
)
)
)
=
x1
x5
(
x1
x6
(
x1
x7
(
x1
x2
(
x1
x3
(
x1
x4
x8
)
)
)
)
)
(proof)
Known
df7cd..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
x9
)
)
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x2
(
x1
x3
x9
)
)
)
)
)
)
Theorem
447df..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
x9
)
)
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x2
(
x1
x3
x9
)
)
)
)
)
)
(proof)
Known
9fbf6..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
x9
)
)
)
)
)
)
=
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x2
(
x1
x3
(
x1
x4
x9
)
)
)
)
)
)
Theorem
62596..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
x9
)
)
)
)
)
)
=
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x2
(
x1
x3
(
x1
x4
x9
)
)
)
)
)
)
(proof)
Known
9ba1d..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
x10
)
)
)
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x2
(
x1
x3
x10
)
)
)
)
)
)
)
Theorem
72787..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
x10
)
)
)
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x2
(
x1
x3
x10
)
)
)
)
)
)
)
(proof)
Known
d3b5b..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
x10
)
)
)
)
)
)
)
=
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x2
(
x1
x3
(
x1
x4
x10
)
)
)
)
)
)
)
Theorem
98831..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
x10
)
)
)
)
)
)
)
=
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x2
(
x1
x3
(
x1
x4
x10
)
)
)
)
)
)
)
(proof)
Known
d63ce..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
x10
)
)
)
)
)
)
)
=
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x10
)
)
)
)
)
)
)
Theorem
5dd73..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
x10
)
)
)
)
)
)
)
=
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x10
)
)
)
)
)
)
)
(proof)
Known
696da..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
x11
)
)
)
)
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x2
(
x1
x3
x11
)
)
)
)
)
)
)
)
Theorem
a0be6..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
x11
)
)
)
)
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x2
(
x1
x3
x11
)
)
)
)
)
)
)
)
(proof)
Known
387d2..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
x11
)
)
)
)
)
)
)
)
=
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x2
(
x1
x3
(
x1
x4
x11
)
)
)
)
)
)
)
)
Theorem
1eb59..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
x11
)
)
)
)
)
)
)
)
=
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x2
(
x1
x3
(
x1
x4
x11
)
)
)
)
)
)
)
)
(proof)
Known
17b5e..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
x11
)
)
)
)
)
)
)
)
=
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x11
)
)
)
)
)
)
)
)
Theorem
b4695..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
x11
)
)
)
)
)
)
)
)
=
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x11
)
)
)
)
)
)
)
)
(proof)
Known
0d9d2..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
x12
)
)
)
)
)
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x2
(
x1
x3
x12
)
)
)
)
)
)
)
)
)
Theorem
f675b..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
x12
)
)
)
)
)
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x2
(
x1
x3
x12
)
)
)
)
)
)
)
)
)
(proof)
Known
30284..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
x12
)
)
)
)
)
)
)
)
)
=
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x2
(
x1
x3
(
x1
x4
x12
)
)
)
)
)
)
)
)
)
Theorem
a40e8..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
x12
)
)
)
)
)
)
)
)
)
=
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x2
(
x1
x3
(
x1
x4
x12
)
)
)
)
)
)
)
)
)
(proof)
Known
5a706..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
x12
)
)
)
)
)
)
)
)
)
=
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x12
)
)
)
)
)
)
)
)
)
Theorem
d2263..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
x12
)
)
)
)
)
)
)
)
)
=
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x12
)
)
)
)
)
)
)
)
)
(proof)
Known
a8fd7..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
x12
)
)
)
)
)
)
)
)
)
=
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x12
)
)
)
)
)
)
)
)
)
Theorem
f009b..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
x12
)
)
)
)
)
)
)
)
)
=
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x12
)
)
)
)
)
)
)
)
)
(proof)
Known
6f341..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
)
)
)
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x2
(
x1
x3
x13
)
)
)
)
)
)
)
)
)
)
Theorem
1d6bf..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
)
)
)
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x2
(
x1
x3
x13
)
)
)
)
)
)
)
)
)
)
(proof)
Known
fb74d..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
)
)
)
)
)
)
)
=
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x2
(
x1
x3
(
x1
x4
x13
)
)
)
)
)
)
)
)
)
)
Theorem
2253a..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
)
)
)
)
)
)
)
=
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x2
(
x1
x3
(
x1
x4
x13
)
)
)
)
)
)
)
)
)
)
(proof)
Known
72568..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
)
)
)
)
)
)
)
=
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x13
)
)
)
)
)
)
)
)
)
)
Theorem
8db74..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
)
)
)
)
)
)
)
=
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x13
)
)
)
)
)
)
)
)
)
)
(proof)
Known
9bb69..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
)
)
)
)
)
)
)
=
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x13
)
)
)
)
)
)
)
)
)
)
Theorem
c92b5..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
)
)
)
)
)
)
)
=
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x13
)
)
)
)
)
)
)
)
)
)
(proof)
Known
8e1b0..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
x14
)
)
)
)
)
)
)
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x2
(
x1
x3
x14
)
)
)
)
)
)
)
)
)
)
)
Theorem
8b875..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
x14
)
)
)
)
)
)
)
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x2
(
x1
x3
x14
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
521cb..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
x14
)
)
)
)
)
)
)
)
)
)
)
=
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x2
(
x1
x3
(
x1
x4
x14
)
)
)
)
)
)
)
)
)
)
)
Theorem
a298a..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
x14
)
)
)
)
)
)
)
)
)
)
)
=
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x2
(
x1
x3
(
x1
x4
x14
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
9b328..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
x14
)
)
)
)
)
)
)
)
)
)
)
=
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x14
)
)
)
)
)
)
)
)
)
)
)
Theorem
2a04c..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
x14
)
)
)
)
)
)
)
)
)
)
)
=
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x14
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
09a8d..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
x14
)
)
)
)
)
)
)
)
)
)
)
=
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x14
)
)
)
)
)
)
)
)
)
)
)
Theorem
343b8..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
x14
)
)
)
)
)
)
)
)
)
)
)
=
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x14
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
b4182..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
x14
)
)
)
)
)
)
)
)
)
)
)
=
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
x14
)
)
)
)
)
)
)
)
)
)
)
Theorem
c6ef2..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
x14
)
)
)
)
)
)
)
)
)
)
)
=
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
x14
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
f1d76..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
x15
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x2
(
x1
x3
x15
)
)
)
)
)
)
)
)
)
)
)
)
Theorem
2dbc6..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
x15
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x2
(
x1
x3
x15
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
005bf..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
x15
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x2
(
x1
x3
(
x1
x4
x15
)
)
)
)
)
)
)
)
)
)
)
)
Theorem
93b0c..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
x15
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x2
(
x1
x3
(
x1
x4
x15
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
15bb0..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
x15
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x15
)
)
)
)
)
)
)
)
)
)
)
)
Theorem
c0afc..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
x15
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x15
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
25f70..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
x15
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x15
)
)
)
)
)
)
)
)
)
)
)
)
Theorem
71cd8..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
x15
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x15
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
47a47..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
x15
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
x15
)
)
)
)
)
)
)
)
)
)
)
)
Theorem
b48c0..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
x15
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
x15
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
92fce..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x2
(
x1
x3
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
Theorem
e7257..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x2
(
x1
x3
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
f7ca7..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x2
(
x1
x3
(
x1
x4
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
Theorem
285b4..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x2
(
x1
x3
(
x1
x4
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
65a4d..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
Theorem
5aea4..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
8a1ac..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
Theorem
4a237..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
14bac..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
Theorem
0057a..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
56712..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
Theorem
74adf..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
d4a91..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x2
(
x1
x3
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
Theorem
09f31..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x2
(
x1
x3
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
cdec3..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x2
(
x1
x3
(
x1
x4
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
Theorem
15cd1..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x2
(
x1
x3
(
x1
x4
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
55afc..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
Theorem
31b2f..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
78083..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
Theorem
e06ab..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
82de4..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
Theorem
e5a90..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
e6374..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
Theorem
c78ef..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
ad9b7..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x0
x18
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
(
x1
x2
(
x1
x3
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
Theorem
957b7..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x0
x18
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
(
x1
x2
(
x1
x3
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
366f2..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x0
x18
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
(
x1
x2
(
x1
x3
(
x1
x4
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
Theorem
af6e2..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x0
x18
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
(
x1
x2
(
x1
x3
(
x1
x4
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
7b7b5..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x0
x18
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
Theorem
2f787..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x0
x18
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
2fa40..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x0
x18
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
Theorem
247df..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x0
x18
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
11aa7..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x0
x18
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
Theorem
cbaa5..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x0
x18
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
58df9..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x0
x18
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
Theorem
0b2cf..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x0
x18
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
80a23..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x0
x18
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
Theorem
082f9..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
(
x1
x2
x3
)
x4
)
⟶
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x1
x2
x3
=
x1
x3
x2
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x0
x18
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)