Search for blocks/addresses/...
Proofgold Asset
asset id
2aa0fb41572d61696560ac734d9df1e15b0bd7083d8620320da1826a4949c15e
asset hash
0f4d576d92d8ad27bfabe103fe421c08c5b07c7fa5a430cdebad1b22bca2cbf7
bday / block
27876
tx
6353f..
preasset
doc published by
Pr5Zc..
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
a010f..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x8
(
x1
x6
(
x1
x2
(
x1
x3
(
x1
x5
(
x1
x4
x9
)
)
)
)
)
)
Theorem
25b04..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x2
(
x1
x3
(
x1
x6
(
x1
x5
x4
)
)
)
)
)
)
(proof)
Theorem
cb5fc..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x2
(
x1
x3
(
x1
x6
(
x1
x5
x4
)
)
)
)
)
)
(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
70f2d..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x2
(
x1
x3
(
x1
x6
(
x1
x4
x5
)
)
)
)
)
)
(proof)
Theorem
45a55..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x2
(
x1
x3
(
x1
x6
(
x1
x4
x5
)
)
)
)
)
)
(proof)
Known
22b28..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x5
(
x1
x8
(
x1
x6
(
x1
x4
(
x1
x2
(
x1
x3
x9
)
)
)
)
)
)
Theorem
de829..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x3
(
x1
x6
(
x1
x2
(
x1
x5
x4
)
)
)
)
)
)
(proof)
Theorem
9e2e6..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x3
(
x1
x6
(
x1
x2
(
x1
x5
x4
)
)
)
)
)
)
(proof)
Theorem
48893..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x3
(
x1
x6
(
x1
x2
(
x1
x4
x5
)
)
)
)
)
)
(proof)
Theorem
7e855..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x3
(
x1
x6
(
x1
x2
(
x1
x4
x5
)
)
)
)
)
)
(proof)
Known
58c22..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x5
(
x1
x6
(
x1
x8
(
x1
x4
(
x1
x2
(
x1
x3
x9
)
)
)
)
)
)
Theorem
24361..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x3
(
x1
x5
(
x1
x2
(
x1
x6
x4
)
)
)
)
)
)
(proof)
Theorem
7f074..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x3
(
x1
x5
(
x1
x2
(
x1
x6
x4
)
)
)
)
)
)
(proof)
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
be2b0..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x3
(
x1
x5
(
x1
x2
(
x1
x4
x6
)
)
)
)
)
)
(proof)
Theorem
6c2da..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x3
(
x1
x5
(
x1
x2
(
x1
x4
x6
)
)
)
)
)
)
(proof)
Theorem
d2a3d..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x3
(
x1
x4
(
x1
x2
(
x1
x6
x5
)
)
)
)
)
)
(proof)
Theorem
cc4eb..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x3
(
x1
x4
(
x1
x2
(
x1
x6
x5
)
)
)
)
)
)
(proof)
Theorem
fc785..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x3
(
x1
x4
(
x1
x2
(
x1
x5
x6
)
)
)
)
)
)
(proof)
Theorem
dc82e..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x3
(
x1
x4
(
x1
x2
(
x1
x5
x6
)
)
)
)
)
)
(proof)
Known
3373e..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x8
(
x1
x6
(
x1
x3
(
x1
x2
(
x1
x4
(
x1
x5
x9
)
)
)
)
)
)
Theorem
d81db..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x3
(
x1
x2
(
x1
x4
(
x1
x6
x5
)
)
)
)
)
)
(proof)
Theorem
34829..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x3
(
x1
x2
(
x1
x4
(
x1
x6
x5
)
)
)
)
)
)
(proof)
Theorem
e5530..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x3
(
x1
x2
(
x1
x4
(
x1
x5
x6
)
)
)
)
)
)
(proof)
Theorem
98e72..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x3
(
x1
x2
(
x1
x4
(
x1
x5
x6
)
)
)
)
)
)
(proof)
Theorem
30135..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x3
(
x1
x2
(
x1
x5
(
x1
x6
x4
)
)
)
)
)
)
(proof)
Theorem
bd854..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x3
(
x1
x2
(
x1
x5
(
x1
x6
x4
)
)
)
)
)
)
(proof)
Known
73292..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x8
(
x1
x6
(
x1
x3
(
x1
x2
(
x1
x5
(
x1
x4
x9
)
)
)
)
)
)
Theorem
3ea22..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x3
(
x1
x2
(
x1
x5
(
x1
x4
x6
)
)
)
)
)
)
(proof)
Theorem
a51fa..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x3
(
x1
x2
(
x1
x5
(
x1
x4
x6
)
)
)
)
)
)
(proof)
Theorem
71a2c..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x3
(
x1
x2
(
x1
x6
(
x1
x5
x4
)
)
)
)
)
)
(proof)
Theorem
ac91e..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x3
(
x1
x2
(
x1
x6
(
x1
x5
x4
)
)
)
)
)
)
(proof)
Theorem
ddcc3..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x3
(
x1
x2
(
x1
x6
(
x1
x4
x5
)
)
)
)
)
)
(proof)
Theorem
9ccc8..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x3
(
x1
x2
(
x1
x6
(
x1
x4
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
)
)
)
)
)
Theorem
dd0c0..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x4
(
x1
x6
(
x1
x2
(
x1
x5
x3
)
)
)
)
)
)
(proof)
Theorem
83e7d..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x4
(
x1
x6
(
x1
x2
(
x1
x5
x3
)
)
)
)
)
)
(proof)
Known
5192f..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x8
(
x1
x6
(
x1
x4
(
x1
x5
(
x1
x2
(
x1
x3
x9
)
)
)
)
)
)
Theorem
2524e..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x4
(
x1
x6
(
x1
x2
(
x1
x3
x5
)
)
)
)
)
)
(proof)
Theorem
b7014..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x4
(
x1
x6
(
x1
x2
(
x1
x3
x5
)
)
)
)
)
)
(proof)
Known
5c72d..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x5
(
x1
x7
(
x1
x6
(
x1
x4
(
x1
x2
(
x1
x3
x9
)
)
)
)
)
)
Theorem
7cde3..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x4
(
x1
x6
(
x1
x5
(
x1
x2
x3
)
)
)
)
)
)
(proof)
Theorem
91361..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x4
(
x1
x6
(
x1
x5
(
x1
x2
x3
)
)
)
)
)
)
(proof)
Theorem
03511..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x4
(
x1
x5
(
x1
x2
(
x1
x6
x3
)
)
)
)
)
)
(proof)
Theorem
306ed..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x4
(
x1
x5
(
x1
x2
(
x1
x6
x3
)
)
)
)
)
)
(proof)
Theorem
d7240..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x4
(
x1
x5
(
x1
x2
(
x1
x3
x6
)
)
)
)
)
)
(proof)
Theorem
52072..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x4
(
x1
x5
(
x1
x2
(
x1
x3
x6
)
)
)
)
)
)
(proof)
Known
717f5..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x4
(
x1
x2
(
x1
x3
x9
)
)
)
)
)
)
Theorem
204bb..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x2
x3
)
)
)
)
)
)
(proof)
Theorem
bbc1f..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x2
x3
)
)
)
)
)
)
(proof)
Known
5e965..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x6
(
x1
x5
(
x1
x8
(
x1
x4
(
x1
x2
(
x1
x3
x9
)
)
)
)
)
)
Theorem
f4b9a..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x4
(
x1
x3
(
x1
x2
(
x1
x6
x5
)
)
)
)
)
)
(proof)
Theorem
1e5a9..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x4
(
x1
x3
(
x1
x2
(
x1
x6
x5
)
)
)
)
)
)
(proof)
Theorem
7c190..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x4
(
x1
x3
(
x1
x2
(
x1
x5
x6
)
)
)
)
)
)
(proof)
Theorem
6728e..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x4
(
x1
x3
(
x1
x2
(
x1
x5
x6
)
)
)
)
)
)
(proof)
Known
a4c67..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x8
(
x1
x6
(
x1
x4
(
x1
x2
(
x1
x3
(
x1
x5
x9
)
)
)
)
)
)
Theorem
055a4..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x4
(
x1
x2
(
x1
x3
(
x1
x6
x5
)
)
)
)
)
)
(proof)
Theorem
9f389..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x4
(
x1
x2
(
x1
x3
(
x1
x6
x5
)
)
)
)
)
)
(proof)
Theorem
aec37..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x4
(
x1
x2
(
x1
x3
(
x1
x5
x6
)
)
)
)
)
)
(proof)
Theorem
fee46..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x4
(
x1
x2
(
x1
x3
(
x1
x5
x6
)
)
)
)
)
)
(proof)
Theorem
2bd1d..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x4
(
x1
x2
(
x1
x5
(
x1
x6
x3
)
)
)
)
)
)
(proof)
Theorem
0e968..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x4
(
x1
x2
(
x1
x5
(
x1
x6
x3
)
)
)
)
)
)
(proof)
Known
b4b9d..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x8
(
x1
x6
(
x1
x4
(
x1
x2
(
x1
x5
(
x1
x3
x9
)
)
)
)
)
)
Theorem
fbf74..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x4
(
x1
x2
(
x1
x5
(
x1
x3
x6
)
)
)
)
)
)
(proof)
Theorem
67354..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x4
(
x1
x2
(
x1
x5
(
x1
x3
x6
)
)
)
)
)
)
(proof)
Theorem
e6e63..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x4
(
x1
x2
(
x1
x6
(
x1
x5
x3
)
)
)
)
)
)
(proof)
Theorem
5838d..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x4
(
x1
x2
(
x1
x6
(
x1
x5
x3
)
)
)
)
)
)
(proof)
Theorem
57cb2..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x4
(
x1
x2
(
x1
x6
(
x1
x3
x5
)
)
)
)
)
)
(proof)
Theorem
940f1..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x4
(
x1
x2
(
x1
x6
(
x1
x3
x5
)
)
)
)
)
)
(proof)
Theorem
e3da3..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x5
(
x1
x6
(
x1
x2
(
x1
x4
x3
)
)
)
)
)
)
(proof)
Theorem
f0145..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x5
(
x1
x6
(
x1
x2
(
x1
x4
x3
)
)
)
)
)
)
(proof)
Theorem
954ab..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x5
(
x1
x6
(
x1
x2
(
x1
x3
x4
)
)
)
)
)
)
(proof)
Theorem
e6b99..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x5
(
x1
x6
(
x1
x2
(
x1
x3
x4
)
)
)
)
)
)
(proof)
Known
6fc3c..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x7
(
x1
x5
(
x1
x6
(
x1
x4
(
x1
x2
(
x1
x3
x9
)
)
)
)
)
)
Theorem
82154..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x5
(
x1
x6
(
x1
x4
(
x1
x2
x3
)
)
)
)
)
)
(proof)
Theorem
4f034..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x5
(
x1
x6
(
x1
x4
(
x1
x2
x3
)
)
)
)
)
)
(proof)
Theorem
1302d..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x5
(
x1
x4
(
x1
x2
(
x1
x6
x3
)
)
)
)
)
)
(proof)
Theorem
2a7e8..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x5
(
x1
x4
(
x1
x2
(
x1
x6
x3
)
)
)
)
)
)
(proof)
Known
07e2c..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x8
(
x1
x6
(
x1
x5
(
x1
x4
(
x1
x2
(
x1
x3
x9
)
)
)
)
)
)
Theorem
7a8dc..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x5
(
x1
x4
(
x1
x2
(
x1
x3
x6
)
)
)
)
)
)
(proof)
Theorem
10b75..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x5
(
x1
x4
(
x1
x2
(
x1
x3
x6
)
)
)
)
)
)
(proof)
Known
39a98..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x6
(
x1
x5
(
x1
x7
(
x1
x4
(
x1
x2
(
x1
x3
x9
)
)
)
)
)
)
Theorem
f3bd9..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x5
(
x1
x4
(
x1
x6
(
x1
x2
x3
)
)
)
)
)
)
(proof)
Theorem
d94d6..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x5
(
x1
x4
(
x1
x6
(
x1
x2
x3
)
)
)
)
)
)
(proof)
Theorem
d1e5f..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x5
(
x1
x3
(
x1
x2
(
x1
x6
x4
)
)
)
)
)
)
(proof)
Theorem
0d3fc..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x5
(
x1
x3
(
x1
x2
(
x1
x6
x4
)
)
)
)
)
)
(proof)
Known
1827a..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x6
(
x1
x8
(
x1
x5
(
x1
x4
(
x1
x2
(
x1
x3
x9
)
)
)
)
)
)
Theorem
fbe24..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x5
(
x1
x3
(
x1
x2
(
x1
x4
x6
)
)
)
)
)
)
(proof)
Theorem
c8b74..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x5
(
x1
x3
(
x1
x2
(
x1
x4
x6
)
)
)
)
)
)
(proof)
Theorem
92c91..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x5
(
x1
x2
(
x1
x3
(
x1
x6
x4
)
)
)
)
)
)
(proof)
Theorem
1de38..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x5
(
x1
x2
(
x1
x3
(
x1
x6
x4
)
)
)
)
)
)
(proof)
Known
4deb4..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x8
(
x1
x6
(
x1
x5
(
x1
x2
(
x1
x3
(
x1
x4
x9
)
)
)
)
)
)
Theorem
bb4fd..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x5
(
x1
x2
(
x1
x3
(
x1
x4
x6
)
)
)
)
)
)
(proof)
Theorem
874f0..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x5
(
x1
x2
(
x1
x3
(
x1
x4
x6
)
)
)
)
)
)
(proof)
Theorem
0e6f1..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x5
(
x1
x2
(
x1
x4
(
x1
x6
x3
)
)
)
)
)
)
(proof)
Theorem
081c1..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x5
(
x1
x2
(
x1
x4
(
x1
x6
x3
)
)
)
)
)
)
(proof)
Known
805d1..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x8
(
x1
x6
(
x1
x5
(
x1
x2
(
x1
x4
(
x1
x3
x9
)
)
)
)
)
)
Theorem
5642a..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x5
(
x1
x2
(
x1
x4
(
x1
x3
x6
)
)
)
)
)
)
(proof)
Theorem
20f46..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x5
(
x1
x2
(
x1
x4
(
x1
x3
x6
)
)
)
)
)
)
(proof)
Theorem
d9343..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x5
(
x1
x2
(
x1
x6
(
x1
x4
x3
)
)
)
)
)
)
(proof)
Theorem
0009e..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x5
(
x1
x2
(
x1
x6
(
x1
x4
x3
)
)
)
)
)
)
(proof)
Theorem
ff28d..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x5
(
x1
x2
(
x1
x6
(
x1
x3
x4
)
)
)
)
)
)
(proof)
Theorem
4391d..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x5
(
x1
x2
(
x1
x6
(
x1
x3
x4
)
)
)
)
)
)
(proof)
Theorem
1bda0..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x6
(
x1
x5
(
x1
x2
(
x1
x4
x3
)
)
)
)
)
)
(proof)
Theorem
4c3ff..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x6
(
x1
x5
(
x1
x2
(
x1
x4
x3
)
)
)
)
)
)
(proof)
Theorem
235be..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x6
(
x1
x5
(
x1
x2
(
x1
x3
x4
)
)
)
)
)
)
(proof)
Theorem
b5ded..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x6
(
x1
x5
(
x1
x2
(
x1
x3
x4
)
)
)
)
)
)
(proof)
Known
28848..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x7
(
x1
x6
(
x1
x5
(
x1
x4
(
x1
x2
(
x1
x3
x9
)
)
)
)
)
)
Theorem
49953..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x6
(
x1
x5
(
x1
x4
(
x1
x2
x3
)
)
)
)
)
)
(proof)
Theorem
b045d..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x6
(
x1
x5
(
x1
x4
(
x1
x2
x3
)
)
)
)
)
)
(proof)
Theorem
690a0..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x6
(
x1
x4
(
x1
x2
(
x1
x5
x3
)
)
)
)
)
)
(proof)
Theorem
bbd51..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x6
(
x1
x4
(
x1
x2
(
x1
x5
x3
)
)
)
)
)
)
(proof)
Theorem
a6659..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x6
(
x1
x4
(
x1
x2
(
x1
x3
x5
)
)
)
)
)
)
(proof)
Theorem
e11fa..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x6
(
x1
x4
(
x1
x2
(
x1
x3
x5
)
)
)
)
)
)
(proof)
Known
450b1..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x6
(
x1
x7
(
x1
x5
(
x1
x4
(
x1
x2
(
x1
x3
x9
)
)
)
)
)
)
Theorem
d94cc..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x6
(
x1
x4
(
x1
x5
(
x1
x2
x3
)
)
)
)
)
)
(proof)
Theorem
b07bc..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x6
(
x1
x4
(
x1
x5
(
x1
x2
x3
)
)
)
)
)
)
(proof)
Theorem
c3a46..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x6
(
x1
x3
(
x1
x2
(
x1
x5
x4
)
)
)
)
)
)
(proof)
Theorem
0c9a7..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x6
(
x1
x3
(
x1
x2
(
x1
x5
x4
)
)
)
)
)
)
(proof)
Theorem
bdbab..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x6
(
x1
x3
(
x1
x2
(
x1
x4
x5
)
)
)
)
)
)
(proof)
Theorem
dea37..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x6
(
x1
x3
(
x1
x2
(
x1
x4
x5
)
)
)
)
)
)
(proof)
Theorem
f0238..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x6
(
x1
x2
(
x1
x3
(
x1
x5
x4
)
)
)
)
)
)
(proof)
Theorem
b47f4..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x6
(
x1
x2
(
x1
x3
(
x1
x5
x4
)
)
)
)
)
)
(proof)
Theorem
f0197..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x6
(
x1
x2
(
x1
x3
(
x1
x4
x5
)
)
)
)
)
)
(proof)
Theorem
b195e..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x6
(
x1
x2
(
x1
x3
(
x1
x4
x5
)
)
)
)
)
)
(proof)
Theorem
86a7a..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x6
(
x1
x2
(
x1
x4
(
x1
x5
x3
)
)
)
)
)
)
(proof)
Theorem
e7b71..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x9
(
x1
x7
(
x1
x6
(
x1
x2
(
x1
x4
(
x1
x5
x3
)
)
)
)
)
)
(proof)