Search for blocks/addresses/...
Proofgold Asset
asset id
639d1a46706610bd1d9202d5ea4830cfc5840c74676b6fc58c7239a5e665946b
asset hash
ff0d3535e2e4e8a247d26cba39f2c2058f7f1ae490ca5d7853054f0dab2e4841
bday / block
27313
tx
f4fa2..
preasset
doc published by
Pr5Zc..
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
)
)
)
Known
a1cab..
:
∀ 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
x4
(
x1
x2
(
x1
x7
(
x1
x8
(
x1
x6
(
x1
x3
x9
)
)
)
)
)
)
Theorem
663f1..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x8
(
x1
x9
(
x1
x7
(
x1
x3
x5
)
)
)
)
)
)
(proof)
Theorem
8963d..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x8
(
x1
x9
(
x1
x7
(
x1
x3
x5
)
)
)
)
)
)
(proof)
Known
d84c5..
:
∀ 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
x4
(
x1
x2
(
x1
x7
(
x1
x6
(
x1
x3
x8
)
)
)
)
)
Theorem
b456a..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x8
(
x1
x7
(
x1
x3
(
x1
x9
x5
)
)
)
)
)
)
(proof)
Theorem
8bc42..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x8
(
x1
x7
(
x1
x3
(
x1
x9
x5
)
)
)
)
)
)
(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
)
)
)
)
)
Known
d1b03..
:
∀ 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
x3
(
x1
x2
(
x1
x7
(
x1
x6
(
x1
x4
x8
)
)
)
)
)
Theorem
fded2..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x8
(
x1
x7
(
x1
x5
(
x1
x9
x3
)
)
)
)
)
)
(proof)
Theorem
2daa8..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x8
(
x1
x7
(
x1
x5
(
x1
x9
x3
)
)
)
)
)
)
(proof)
Known
6e970..
:
∀ 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
x3
(
x1
x2
(
x1
x7
(
x1
x6
(
x1
x8
(
x1
x4
x9
)
)
)
)
)
)
Theorem
8c3ea..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x8
(
x1
x7
(
x1
x9
(
x1
x5
x3
)
)
)
)
)
)
(proof)
Theorem
39f38..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x8
(
x1
x7
(
x1
x9
(
x1
x5
x3
)
)
)
)
)
)
(proof)
Known
a7d17..
:
∀ 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
x4
(
x1
x2
(
x1
x7
(
x1
x6
(
x1
x8
(
x1
x3
x9
)
)
)
)
)
)
Theorem
d3bb9..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x8
(
x1
x7
(
x1
x9
(
x1
x3
x5
)
)
)
)
)
)
(proof)
Theorem
88b2e..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x8
(
x1
x7
(
x1
x9
(
x1
x3
x5
)
)
)
)
)
)
(proof)
Known
bf22a..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x7
(
x1
x5
(
x1
x3
x8
)
)
)
)
)
Theorem
7e6c5..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x8
(
x1
x5
(
x1
x3
(
x1
x9
x7
)
)
)
)
)
)
(proof)
Theorem
e821a..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x8
(
x1
x5
(
x1
x3
(
x1
x9
x7
)
)
)
)
)
)
(proof)
Known
4df0d..
:
∀ 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
x3
(
x1
x2
(
x1
x7
(
x1
x4
(
x1
x6
x8
)
)
)
)
)
Theorem
a47d9..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x8
(
x1
x5
(
x1
x7
(
x1
x9
x3
)
)
)
)
)
)
(proof)
Theorem
e2cff..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x8
(
x1
x5
(
x1
x7
(
x1
x9
x3
)
)
)
)
)
)
(proof)
Known
1c62c..
:
∀ 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
x3
(
x1
x2
(
x1
x7
(
x1
x4
(
x1
x8
(
x1
x6
x9
)
)
)
)
)
)
Theorem
0e3f3..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x8
(
x1
x5
(
x1
x9
(
x1
x7
x3
)
)
)
)
)
)
(proof)
Theorem
df2a8..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x8
(
x1
x5
(
x1
x9
(
x1
x7
x3
)
)
)
)
)
)
(proof)
Known
9ebdf..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x7
(
x1
x5
(
x1
x8
(
x1
x3
x9
)
)
)
)
)
)
Theorem
71b90..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x8
(
x1
x5
(
x1
x9
(
x1
x3
x7
)
)
)
)
)
)
(proof)
Theorem
31845..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x8
(
x1
x5
(
x1
x9
(
x1
x3
x7
)
)
)
)
)
)
(proof)
Known
a283f..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x7
(
x1
x3
(
x1
x5
x8
)
)
)
)
)
Theorem
dc516..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x8
(
x1
x3
(
x1
x5
(
x1
x9
x7
)
)
)
)
)
)
(proof)
Theorem
76688..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x8
(
x1
x3
(
x1
x5
(
x1
x9
x7
)
)
)
)
)
)
(proof)
Known
f9b7d..
:
∀ 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
x4
(
x1
x2
(
x1
x7
(
x1
x3
(
x1
x6
x8
)
)
)
)
)
Theorem
29333..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x8
(
x1
x3
(
x1
x7
(
x1
x9
x5
)
)
)
)
)
)
(proof)
Theorem
0af8e..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x8
(
x1
x3
(
x1
x7
(
x1
x9
x5
)
)
)
)
)
)
(proof)
Known
1b1fb..
:
∀ 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
x4
(
x1
x2
(
x1
x7
(
x1
x3
(
x1
x8
(
x1
x6
x9
)
)
)
)
)
)
Theorem
2a9cb..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x8
(
x1
x3
(
x1
x9
(
x1
x7
x5
)
)
)
)
)
)
(proof)
Theorem
5d66b..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x8
(
x1
x3
(
x1
x9
(
x1
x7
x5
)
)
)
)
)
)
(proof)
Known
504c6..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x7
(
x1
x3
(
x1
x8
(
x1
x5
x9
)
)
)
)
)
)
Theorem
cab33..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x8
(
x1
x3
(
x1
x9
(
x1
x5
x7
)
)
)
)
)
)
(proof)
Theorem
c7be2..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x8
(
x1
x3
(
x1
x9
(
x1
x5
x7
)
)
)
)
)
)
(proof)
Known
c7b41..
:
∀ 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
x4
(
x1
x2
(
x1
x8
(
x1
x7
(
x1
x3
(
x1
x6
x9
)
)
)
)
)
)
Theorem
66d7b..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x8
(
x1
x3
(
x1
x7
x5
)
)
)
)
)
)
(proof)
Theorem
24398..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x8
(
x1
x3
(
x1
x7
x5
)
)
)
)
)
)
(proof)
Known
2ea7b..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x8
(
x1
x7
(
x1
x3
(
x1
x5
x9
)
)
)
)
)
)
Theorem
a956e..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x8
(
x1
x3
(
x1
x5
x7
)
)
)
)
)
)
(proof)
Theorem
7999e..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x8
(
x1
x3
(
x1
x5
x7
)
)
)
)
)
)
(proof)
Known
e3857..
:
∀ 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
x3
(
x1
x2
(
x1
x8
(
x1
x7
(
x1
x4
(
x1
x6
x9
)
)
)
)
)
)
Theorem
f9f0e..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x8
(
x1
x5
(
x1
x7
x3
)
)
)
)
)
)
(proof)
Theorem
10a89..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x8
(
x1
x5
(
x1
x7
x3
)
)
)
)
)
)
(proof)
Known
664e7..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x8
(
x1
x7
(
x1
x5
(
x1
x3
x9
)
)
)
)
)
)
Theorem
11f23..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x8
(
x1
x5
(
x1
x3
x7
)
)
)
)
)
)
(proof)
Theorem
01132..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x8
(
x1
x5
(
x1
x3
x7
)
)
)
)
)
)
(proof)
Known
da54d..
:
∀ 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
x3
(
x1
x2
(
x1
x8
(
x1
x7
(
x1
x6
(
x1
x4
x9
)
)
)
)
)
)
Theorem
512e2..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x8
(
x1
x7
(
x1
x5
x3
)
)
)
)
)
)
(proof)
Theorem
92176..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x8
(
x1
x7
(
x1
x5
x3
)
)
)
)
)
)
(proof)
Known
5dc9d..
:
∀ 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
x4
(
x1
x2
(
x1
x8
(
x1
x7
(
x1
x6
(
x1
x3
x9
)
)
)
)
)
)
Theorem
7e12d..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x8
(
x1
x7
(
x1
x3
x5
)
)
)
)
)
)
(proof)
Theorem
09adb..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x8
(
x1
x7
(
x1
x3
x5
)
)
)
)
)
)
(proof)
Known
47002..
:
∀ 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
x4
(
x1
x2
(
x1
x8
(
x1
x6
(
x1
x3
(
x1
x7
x9
)
)
)
)
)
)
Theorem
e29f6..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x7
(
x1
x3
(
x1
x8
x5
)
)
)
)
)
)
(proof)
Theorem
88178..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x7
(
x1
x3
(
x1
x8
x5
)
)
)
)
)
)
(proof)
Theorem
cd1c6..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x7
(
x1
x3
(
x1
x5
x8
)
)
)
)
)
)
(proof)
Theorem
4db3a..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x7
(
x1
x3
(
x1
x5
x8
)
)
)
)
)
)
(proof)
Known
2b216..
:
∀ 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
x3
(
x1
x2
(
x1
x8
(
x1
x6
(
x1
x4
(
x1
x7
x9
)
)
)
)
)
)
Theorem
03401..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x7
(
x1
x5
(
x1
x8
x3
)
)
)
)
)
)
(proof)
Theorem
fe773..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x7
(
x1
x5
(
x1
x8
x3
)
)
)
)
)
)
(proof)
Theorem
0c58f..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x7
(
x1
x5
(
x1
x3
x8
)
)
)
)
)
)
(proof)
Theorem
22c53..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x7
(
x1
x5
(
x1
x3
x8
)
)
)
)
)
)
(proof)
Known
afa4a..
:
∀ 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
x3
(
x1
x2
(
x1
x8
(
x1
x6
(
x1
x7
(
x1
x4
x9
)
)
)
)
)
)
Theorem
c0c72..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x7
(
x1
x8
(
x1
x5
x3
)
)
)
)
)
)
(proof)
Theorem
5478a..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x7
(
x1
x8
(
x1
x5
x3
)
)
)
)
)
)
(proof)
Known
5fe36..
:
∀ 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
x4
(
x1
x2
(
x1
x8
(
x1
x6
(
x1
x7
(
x1
x3
x9
)
)
)
)
)
)
Theorem
2568e..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x7
(
x1
x8
(
x1
x3
x5
)
)
)
)
)
)
(proof)
Theorem
314a4..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x7
(
x1
x8
(
x1
x3
x5
)
)
)
)
)
)
(proof)
Known
fb196..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x8
(
x1
x5
(
x1
x3
(
x1
x7
x9
)
)
)
)
)
)
Theorem
d4871..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x5
(
x1
x3
(
x1
x8
x7
)
)
)
)
)
)
(proof)
Theorem
ed352..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x5
(
x1
x3
(
x1
x8
x7
)
)
)
)
)
)
(proof)
Theorem
489ed..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x5
(
x1
x3
(
x1
x7
x8
)
)
)
)
)
)
(proof)
Theorem
5f5fa..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x5
(
x1
x3
(
x1
x7
x8
)
)
)
)
)
)
(proof)
Known
7e167..
:
∀ 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
x3
(
x1
x2
(
x1
x8
(
x1
x4
(
x1
x6
(
x1
x7
x9
)
)
)
)
)
)
Theorem
c7d63..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x5
(
x1
x7
(
x1
x8
x3
)
)
)
)
)
)
(proof)
Theorem
1a96e..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x5
(
x1
x7
(
x1
x8
x3
)
)
)
)
)
)
(proof)
Known
77a80..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x8
(
x1
x5
(
x1
x7
(
x1
x3
x9
)
)
)
)
)
)
Theorem
dff88..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x5
(
x1
x7
(
x1
x3
x8
)
)
)
)
)
)
(proof)
Theorem
d659f..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x5
(
x1
x7
(
x1
x3
x8
)
)
)
)
)
)
(proof)
Known
1dacc..
:
∀ 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
x3
(
x1
x2
(
x1
x8
(
x1
x4
(
x1
x7
(
x1
x6
x9
)
)
)
)
)
)
Theorem
b9966..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x5
(
x1
x8
(
x1
x7
x3
)
)
)
)
)
)
(proof)
Theorem
fda1e..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x5
(
x1
x8
(
x1
x7
x3
)
)
)
)
)
)
(proof)
Theorem
c7e08..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x5
(
x1
x8
(
x1
x3
x7
)
)
)
)
)
)
(proof)
Theorem
2a935..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x5
(
x1
x8
(
x1
x3
x7
)
)
)
)
)
)
(proof)
Known
556e6..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x8
(
x1
x3
(
x1
x5
(
x1
x7
x9
)
)
)
)
)
)
Theorem
a4dd7..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x3
(
x1
x5
(
x1
x8
x7
)
)
)
)
)
)
(proof)
Theorem
139e4..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x3
(
x1
x5
(
x1
x8
x7
)
)
)
)
)
)
(proof)
Theorem
f58b1..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x3
(
x1
x5
(
x1
x7
x8
)
)
)
)
)
)
(proof)
Theorem
41076..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x3
(
x1
x5
(
x1
x7
x8
)
)
)
)
)
)
(proof)
Known
60c03..
:
∀ 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
x4
(
x1
x2
(
x1
x8
(
x1
x3
(
x1
x6
(
x1
x7
x9
)
)
)
)
)
)
Theorem
8e83e..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x3
(
x1
x7
(
x1
x8
x5
)
)
)
)
)
)
(proof)
Theorem
90427..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x3
(
x1
x7
(
x1
x8
x5
)
)
)
)
)
)
(proof)
Known
d1751..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x8
(
x1
x3
(
x1
x7
(
x1
x5
x9
)
)
)
)
)
)
Theorem
e7bcb..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x3
(
x1
x7
(
x1
x5
x8
)
)
)
)
)
)
(proof)
Theorem
1fef9..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x3
(
x1
x7
(
x1
x5
x8
)
)
)
)
)
)
(proof)
Known
848d5..
:
∀ 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
x4
(
x1
x2
(
x1
x8
(
x1
x3
(
x1
x7
(
x1
x6
x9
)
)
)
)
)
)
Theorem
8a4dc..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x3
(
x1
x8
(
x1
x7
x5
)
)
)
)
)
)
(proof)
Theorem
fdfa7..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x3
(
x1
x8
(
x1
x7
x5
)
)
)
)
)
)
(proof)
Theorem
0f020..
:
∀ 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 .
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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x3
(
x1
x8
(
x1
x5
x7
)
)
)
)
)
)
(proof)
Theorem
5f884..
:
∀ 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
x6
(
x1
x4
(
x1
x2
(
x1
x9
(
x1
x3
(
x1
x8
(
x1
x5
x7
)
)
)
)
)
)
(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
)
)
)
)
Known
82db6..
:
∀ 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
x4
(
x1
x8
(
x1
x2
(
x1
x7
(
x1
x3
(
x1
x6
x9
)
)
)
)
)
)
Theorem
4cd12..
:
∀ 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 .
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
x6
(
x1
x5
(
x1
x9
(
x1
x2
(
x1
x8
(
x1
x3
(
x1
x7
x4
)
)
)
)
)
)
(proof)
Theorem
c2a99..
:
∀ 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
x6
(
x1
x5
(
x1
x9
(
x1
x2
(
x1
x8
(
x1
x3
(
x1
x7
x4
)
)
)
)
)
)
(proof)
Known
ba695..
:
∀ 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
x6
(
x1
x5
(
x1
x8
(
x1
x2
(
x1
x7
(
x1
x3
(
x1
x4
x9
)
)
)
)
)
)
Theorem
ac37f..
:
∀ 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 .
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
x6
(
x1
x5
(
x1
x9
(
x1
x2
(
x1
x8
(
x1
x3
(
x1
x4
x7
)
)
)
)
)
)
(proof)
Theorem
8d6c8..
:
∀ 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
x6
(
x1
x5
(
x1
x9
(
x1
x2
(
x1
x8
(
x1
x3
(
x1
x4
x7
)
)
)
)
)
)
(proof)
Theorem
9d8d4..
:
∀ 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 .
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
x6
(
x1
x5
(
x1
x9
(
x1
x2
(
x1
x8
(
x1
x4
(
x1
x7
x3
)
)
)
)
)
)
(proof)
Theorem
df715..
:
∀ 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
x6
(
x1
x5
(
x1
x9
(
x1
x2
(
x1
x8
(
x1
x4
(
x1
x7
x3
)
)
)
)
)
)
(proof)
Known
31e40..
:
∀ 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
x6
(
x1
x5
(
x1
x8
(
x1
x2
(
x1
x7
(
x1
x4
(
x1
x3
x9
)
)
)
)
)
)
Theorem
61ca8..
:
∀ 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 .
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
x6
(
x1
x5
(
x1
x9
(
x1
x2
(
x1
x8
(
x1
x4
(
x1
x3
x7
)
)
)
)
)
)
(proof)
Theorem
6775a..
:
∀ 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
x6
(
x1
x5
(
x1
x9
(
x1
x2
(
x1
x8
(
x1
x4
(
x1
x3
x7
)
)
)
)
)
)
(proof)
Known
c9b04..
:
∀ 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
x4
(
x1
x8
(
x1
x2
(
x1
x7
(
x1
x6
(
x1
x3
x9
)
)
)
)
)
)
Theorem
5677e..
:
∀ 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 .
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
x6
(
x1
x5
(
x1
x9
(
x1
x2
(
x1
x8
(
x1
x7
(
x1
x4
x3
)
)
)
)
)
)
(proof)
Theorem
843cf..
:
∀ 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
x6
(
x1
x5
(
x1
x9
(
x1
x2
(
x1
x8
(
x1
x7
(
x1
x4
x3
)
)
)
)
)
)
(proof)
Theorem
ac095..
:
∀ 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 .
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
x6
(
x1
x5
(
x1
x9
(
x1
x2
(
x1
x8
(
x1
x7
(
x1
x3
x4
)
)
)
)
)
)
(proof)
Theorem
3900d..
:
∀ 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
x6
(
x1
x5
(
x1
x9
(
x1
x2
(
x1
x8
(
x1
x7
(
x1
x3
x4
)
)
)
)
)
)
(proof)
Known
22e7a..
:
∀ 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
x4
(
x1
x8
(
x1
x2
(
x1
x6
(
x1
x3
(
x1
x7
x9
)
)
)
)
)
)
Theorem
3ec1f..
:
∀ 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 .
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
x6
(
x1
x5
(
x1
x9
(
x1
x2
(
x1
x7
(
x1
x3
(
x1
x8
x4
)
)
)
)
)
)
(proof)
Theorem
8c7fd..
:
∀ 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
x6
(
x1
x5
(
x1
x9
(
x1
x2
(
x1
x7
(
x1
x3
(
x1
x8
x4
)
)
)
)
)
)
(proof)
Theorem
be558..
:
∀ 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 .
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
x6
(
x1
x5
(
x1
x9
(
x1
x2
(
x1
x7
(
x1
x3
(
x1
x4
x8
)
)
)
)
)
)
(proof)
Theorem
66cad..
:
∀ 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
x6
(
x1
x5
(
x1
x9
(
x1
x2
(
x1
x7
(
x1
x3
(
x1
x4
x8
)
)
)
)
)
)
(proof)
Theorem
7253a..
:
∀ 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 .
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
x6
(
x1
x5
(
x1
x9
(
x1
x2
(
x1
x7
(
x1
x4
(
x1
x8
x3
)
)
)
)
)
)
(proof)
Theorem
9d266..
:
∀ 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
x6
(
x1
x5
(
x1
x9
(
x1
x2
(
x1
x7
(
x1
x4
(
x1
x8
x3
)
)
)
)
)
)
(proof)
Theorem
881a5..
:
∀ 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 .
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
x6
(
x1
x5
(
x1
x9
(
x1
x2
(
x1
x7
(
x1
x4
(
x1
x3
x8
)
)
)
)
)
)
(proof)
Theorem
b74e6..
:
∀ 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
x6
(
x1
x5
(
x1
x9
(
x1
x2
(
x1
x7
(
x1
x4
(
x1
x3
x8
)
)
)
)
)
)
(proof)
Known
43042..
:
∀ 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
x4
(
x1
x8
(
x1
x2
(
x1
x6
(
x1
x7
(
x1
x3
x9
)
)
)
)
)
)
Theorem
fa046..
:
∀ 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 .
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
x6
(
x1
x5
(
x1
x9
(
x1
x2
(
x1
x7
(
x1
x8
(
x1
x4
x3
)
)
)
)
)
)
(proof)
Theorem
069f4..
:
∀ 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
x6
(
x1
x5
(
x1
x9
(
x1
x2
(
x1
x7
(
x1
x8
(
x1
x4
x3
)
)
)
)
)
)
(proof)
Theorem
71948..
:
∀ 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 .
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
x6
(
x1
x5
(
x1
x9
(
x1
x2
(
x1
x7
(
x1
x8
(
x1
x3
x4
)
)
)
)
)
)
(proof)
Theorem
1d918..
:
∀ 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
x6
(
x1
x5
(
x1
x9
(
x1
x2
(
x1
x7
(
x1
x8
(
x1
x3
x4
)
)
)
)
)
)
(proof)
Known
93cc9..
:
∀ 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
x6
(
x1
x5
(
x1
x8
(
x1
x2
(
x1
x4
(
x1
x3
(
x1
x7
x9
)
)
)
)
)
)
Theorem
8afb4..
:
∀ 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 .
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
x6
(
x1
x5
(
x1
x9
(
x1
x2
(
x1
x4
(
x1
x3
(
x1
x8
x7
)
)
)
)
)
)
(proof)
Theorem
d767f..
:
∀ 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
x6
(
x1
x5
(
x1
x9
(
x1
x2
(
x1
x4
(
x1
x3
(
x1
x8
x7
)
)
)
)
)
)
(proof)
Theorem
3af1c..
:
∀ 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 .
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
x6
(
x1
x5
(
x1
x9
(
x1
x2
(
x1
x4
(
x1
x3
(
x1
x7
x8
)
)
)
)
)
)
(proof)
Theorem
1928c..
:
∀ 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
x6
(
x1
x5
(
x1
x9
(
x1
x2
(
x1
x4
(
x1
x3
(
x1
x7
x8
)
)
)
)
)
)
(proof)
Known
ac48d..
:
∀ 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
x4
(
x1
x8
(
x1
x2
(
x1
x3
(
x1
x6
(
x1
x7
x9
)
)
)
)
)
)
Theorem
48b7b..
:
∀ 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 .
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
x6
(
x1
x5
(
x1
x9
(
x1
x2
(
x1
x4
(
x1
x7
(
x1
x8
x3
)
)
)
)
)
)
(proof)
Theorem
2f964..
:
∀ 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
x6
(
x1
x5
(
x1
x9
(
x1
x2
(
x1
x4
(
x1
x7
(
x1
x8
x3
)
)
)
)
)
)
(proof)
Known
1f260..
:
∀ 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
x6
(
x1
x5
(
x1
x8
(
x1
x2
(
x1
x4
(
x1
x7
(
x1
x3
x9
)
)
)
)
)
)
Theorem
eb6e9..
:
∀ 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 .
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
x6
(
x1
x5
(
x1
x9
(
x1
x2
(
x1
x4
(
x1
x7
(
x1
x3
x8
)
)
)
)
)
)
(proof)
Theorem
e56ec..
:
∀ 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
x6
(
x1
x5
(
x1
x9
(
x1
x2
(
x1
x4
(
x1
x7
(
x1
x3
x8
)
)
)
)
)
)
(proof)