Search for blocks/addresses/...
Proofgold Asset
asset id
7289622630a9053c443a9b825c6396890afca4fdb1db1f4ee8b5e982bb37d70d
asset hash
90f8965b23490aa126871d0cc77872bbd9a6c1f255e38065ff13953757268d20
bday / block
27306
tx
d4357..
preasset
doc published by
Pr5Zc..
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
f79f2..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x4
(
x1
x8
(
x1
x6
x9
)
)
)
)
)
)
Theorem
edb11..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x9
(
x1
x5
(
x1
x8
x3
)
)
)
)
)
)
(proof)
Theorem
abbd0..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x9
(
x1
x5
(
x1
x8
x3
)
)
)
)
)
)
(proof)
Known
53c1d..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x8
(
x1
x5
(
x1
x3
x9
)
)
)
)
)
)
Theorem
921bf..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x9
(
x1
x5
(
x1
x3
x8
)
)
)
)
)
)
(proof)
Theorem
fdd66..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x9
(
x1
x5
(
x1
x3
x8
)
)
)
)
)
)
(proof)
Known
034ed..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x2
(
x1
x4
(
x1
x7
(
x1
x6
x9
)
)
)
)
)
)
Theorem
00a63..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x9
(
x1
x8
(
x1
x5
x3
)
)
)
)
)
)
(proof)
Theorem
fc06a..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x9
(
x1
x8
(
x1
x5
x3
)
)
)
)
)
)
(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
)
)
)
Known
28829..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x6
(
x1
x2
(
x1
x8
(
x1
x7
(
x1
x3
x9
)
)
)
)
)
)
Theorem
dc9fe..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x9
(
x1
x8
(
x1
x3
x5
)
)
)
)
)
)
(proof)
Theorem
c153f..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x9
(
x1
x8
(
x1
x3
x5
)
)
)
)
)
)
(proof)
Known
a2bec..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x6
(
x1
x2
(
x1
x7
(
x1
x3
x8
)
)
)
)
)
Theorem
93a55..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x8
(
x1
x3
(
x1
x9
x5
)
)
)
)
)
)
(proof)
Theorem
b0224..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x8
(
x1
x3
(
x1
x9
x5
)
)
)
)
)
)
(proof)
Known
dbcc8..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x4
(
x1
x6
x8
)
)
)
)
)
Theorem
2b325..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x8
(
x1
x5
(
x1
x9
x3
)
)
)
)
)
)
(proof)
Theorem
1113e..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x8
(
x1
x5
(
x1
x9
x3
)
)
)
)
)
)
(proof)
Known
70e23..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x2
(
x1
x4
(
x1
x6
(
x1
x7
x9
)
)
)
)
)
)
Theorem
de55e..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x8
(
x1
x9
(
x1
x5
x3
)
)
)
)
)
)
(proof)
Theorem
12315..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x8
(
x1
x9
(
x1
x5
x3
)
)
)
)
)
)
(proof)
Known
782a0..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x6
(
x1
x2
(
x1
x7
(
x1
x8
(
x1
x3
x9
)
)
)
)
)
)
Theorem
bfd20..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x8
(
x1
x9
(
x1
x3
x5
)
)
)
)
)
)
(proof)
Theorem
50a2b..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x8
(
x1
x9
(
x1
x3
x5
)
)
)
)
)
)
(proof)
Known
caca7..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x5
(
x1
x3
x8
)
)
)
)
)
Theorem
3f116..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x5
(
x1
x3
(
x1
x9
x8
)
)
)
)
)
)
(proof)
Theorem
615cc..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x5
(
x1
x3
(
x1
x9
x8
)
)
)
)
)
)
(proof)
Known
c52bb..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x3
(
x1
x6
(
x1
x2
(
x1
x4
x7
)
)
)
)
Theorem
b3f94..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x5
(
x1
x8
(
x1
x9
x3
)
)
)
)
)
)
(proof)
Theorem
dd36e..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x5
(
x1
x8
(
x1
x9
x3
)
)
)
)
)
)
(proof)
Known
d244c..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x6
(
x1
x2
(
x1
x4
(
x1
x8
(
x1
x7
x9
)
)
)
)
)
)
Theorem
5eef0..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x5
(
x1
x9
(
x1
x8
x3
)
)
)
)
)
)
(proof)
Theorem
235c8..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x5
(
x1
x9
(
x1
x8
x3
)
)
)
)
)
)
(proof)
Known
88ebd..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x5
(
x1
x8
(
x1
x3
x9
)
)
)
)
)
)
Theorem
c1240..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x5
(
x1
x9
(
x1
x3
x8
)
)
)
)
)
)
(proof)
Theorem
60fa4..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x5
(
x1
x9
(
x1
x3
x8
)
)
)
)
)
)
(proof)
Known
f285b..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x3
(
x1
x5
x8
)
)
)
)
)
Theorem
5416c..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x3
(
x1
x5
(
x1
x9
x8
)
)
)
)
)
)
(proof)
Theorem
f4bf1..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x3
(
x1
x5
(
x1
x9
x8
)
)
)
)
)
)
(proof)
Known
7108a..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x4
(
x1
x6
(
x1
x2
(
x1
x3
x7
)
)
)
)
Theorem
03adc..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x3
(
x1
x8
(
x1
x9
x5
)
)
)
)
)
)
(proof)
Theorem
4b56f..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x3
(
x1
x8
(
x1
x9
x5
)
)
)
)
)
)
(proof)
Known
f498f..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x6
(
x1
x2
(
x1
x3
(
x1
x8
(
x1
x7
x9
)
)
)
)
)
)
Theorem
c92d7..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x3
(
x1
x9
(
x1
x8
x5
)
)
)
)
)
)
(proof)
Theorem
536d9..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x3
(
x1
x9
(
x1
x8
x5
)
)
)
)
)
)
(proof)
Known
f70fa..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x3
(
x1
x8
(
x1
x5
x9
)
)
)
)
)
)
Theorem
1f472..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x3
(
x1
x9
(
x1
x5
x8
)
)
)
)
)
)
(proof)
Theorem
e662d..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x2
(
x1
x3
(
x1
x9
(
x1
x5
x8
)
)
)
)
)
)
(proof)
Known
128f2..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x3
(
x1
x2
(
x1
x5
x8
)
)
)
)
)
Theorem
e7415..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x3
(
x1
x2
(
x1
x5
(
x1
x9
x8
)
)
)
)
)
)
(proof)
Theorem
7bc50..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x3
(
x1
x2
(
x1
x5
(
x1
x9
x8
)
)
)
)
)
)
(proof)
Known
8c4b6..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x6
(
x1
x5
(
x1
x3
(
x1
x2
(
x1
x4
x7
)
)
)
)
Theorem
51252..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x3
(
x1
x2
(
x1
x8
(
x1
x9
x5
)
)
)
)
)
)
(proof)
Theorem
53cd7..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x3
(
x1
x2
(
x1
x8
(
x1
x9
x5
)
)
)
)
)
)
(proof)
Known
56ff1..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x3
(
x1
x2
(
x1
x4
(
x1
x8
(
x1
x7
x9
)
)
)
)
)
)
Theorem
df9c2..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x3
(
x1
x2
(
x1
x9
(
x1
x8
x5
)
)
)
)
)
)
(proof)
Theorem
130b6..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x3
(
x1
x2
(
x1
x9
(
x1
x8
x5
)
)
)
)
)
)
(proof)
Known
0a7c2..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x3
(
x1
x2
(
x1
x8
(
x1
x5
x9
)
)
)
)
)
)
Theorem
94ec7..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x3
(
x1
x2
(
x1
x9
(
x1
x5
x8
)
)
)
)
)
)
(proof)
Theorem
81616..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x3
(
x1
x2
(
x1
x9
(
x1
x5
x8
)
)
)
)
)
)
(proof)
Known
dff63..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x5
(
x1
x2
(
x1
x3
x8
)
)
)
)
)
Theorem
0de4b..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x5
(
x1
x2
(
x1
x3
(
x1
x9
x8
)
)
)
)
)
)
(proof)
Theorem
b7fa4..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x5
(
x1
x2
(
x1
x3
(
x1
x9
x8
)
)
)
)
)
)
(proof)
Known
bd148..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x6
(
x1
x3
(
x1
x5
(
x1
x2
(
x1
x4
x7
)
)
)
)
Theorem
1b75a..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x5
(
x1
x2
(
x1
x8
(
x1
x9
x3
)
)
)
)
)
)
(proof)
Theorem
d68b0..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x5
(
x1
x2
(
x1
x8
(
x1
x9
x3
)
)
)
)
)
)
(proof)
Known
8c30c..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x3
(
x1
x5
(
x1
x2
(
x1
x4
(
x1
x8
(
x1
x7
x9
)
)
)
)
)
)
Theorem
98d9c..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x5
(
x1
x2
(
x1
x9
(
x1
x8
x3
)
)
)
)
)
)
(proof)
Theorem
97a9f..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x5
(
x1
x2
(
x1
x9
(
x1
x8
x3
)
)
)
)
)
)
(proof)
Known
d3b84..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x5
(
x1
x2
(
x1
x8
(
x1
x3
x9
)
)
)
)
)
)
Theorem
788b8..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x5
(
x1
x2
(
x1
x9
(
x1
x3
x8
)
)
)
)
)
)
(proof)
Theorem
c1bce..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x5
(
x1
x2
(
x1
x9
(
x1
x3
x8
)
)
)
)
)
)
(proof)
Known
ba174..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x3
(
x1
x2
(
x1
x4
(
x1
x5
x8
)
)
)
)
)
Theorem
5c1c2..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x8
(
x1
x2
(
x1
x3
(
x1
x9
x5
)
)
)
)
)
)
(proof)
Theorem
3c31f..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x8
(
x1
x2
(
x1
x3
(
x1
x9
x5
)
)
)
)
)
)
(proof)
Known
f3668..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x3
(
x1
x7
(
x1
x2
(
x1
x4
(
x1
x5
x8
)
)
)
)
)
Theorem
a2c58..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x8
(
x1
x2
(
x1
x5
(
x1
x9
x3
)
)
)
)
)
)
(proof)
Theorem
617cf..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x8
(
x1
x2
(
x1
x5
(
x1
x9
x3
)
)
)
)
)
)
(proof)
Known
11b51..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x3
(
x1
x8
(
x1
x2
(
x1
x4
(
x1
x5
(
x1
x7
x9
)
)
)
)
)
)
Theorem
2ea84..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x8
(
x1
x2
(
x1
x9
(
x1
x5
x3
)
)
)
)
)
)
(proof)
Theorem
4b326..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x8
(
x1
x2
(
x1
x9
(
x1
x5
x3
)
)
)
)
)
)
(proof)
Known
252ac..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x3
(
x1
x2
(
x1
x4
(
x1
x5
(
x1
x7
x9
)
)
)
)
)
)
Theorem
e45a4..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x8
(
x1
x2
(
x1
x9
(
x1
x3
x5
)
)
)
)
)
)
(proof)
Theorem
db100..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x8
(
x1
x2
(
x1
x9
(
x1
x3
x5
)
)
)
)
)
)
(proof)
Known
f1ca6..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x3
(
x1
x2
(
x1
x4
(
x1
x8
(
x1
x5
x9
)
)
)
)
)
)
Theorem
31c22..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x9
(
x1
x2
(
x1
x3
(
x1
x8
x5
)
)
)
)
)
)
(proof)
Theorem
53251..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x9
(
x1
x2
(
x1
x3
(
x1
x8
x5
)
)
)
)
)
)
(proof)
Known
63d4c..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x8
(
x1
x2
(
x1
x3
(
x1
x5
x9
)
)
)
)
)
)
Theorem
bf14b..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x9
(
x1
x2
(
x1
x3
(
x1
x5
x8
)
)
)
)
)
)
(proof)
Theorem
cc291..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x9
(
x1
x2
(
x1
x3
(
x1
x5
x8
)
)
)
)
)
)
(proof)
Known
2b8ca..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x3
(
x1
x7
(
x1
x2
(
x1
x4
(
x1
x8
(
x1
x5
x9
)
)
)
)
)
)
Theorem
1a24a..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x9
(
x1
x2
(
x1
x5
(
x1
x8
x3
)
)
)
)
)
)
(proof)
Theorem
84cd5..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x9
(
x1
x2
(
x1
x5
(
x1
x8
x3
)
)
)
)
)
)
(proof)
Known
f687d..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x8
(
x1
x2
(
x1
x5
(
x1
x3
x9
)
)
)
)
)
)
Theorem
0b12b..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x9
(
x1
x2
(
x1
x5
(
x1
x3
x8
)
)
)
)
)
)
(proof)
Theorem
ba5e5..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x9
(
x1
x2
(
x1
x5
(
x1
x3
x8
)
)
)
)
)
)
(proof)
Known
edb41..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x3
(
x1
x8
(
x1
x2
(
x1
x4
(
x1
x7
(
x1
x5
x9
)
)
)
)
)
)
Theorem
85eae..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x9
(
x1
x2
(
x1
x8
(
x1
x5
x3
)
)
)
)
)
)
(proof)
Theorem
36189..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x9
(
x1
x2
(
x1
x8
(
x1
x5
x3
)
)
)
)
)
)
(proof)
Known
a97f0..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x8
(
x1
x3
(
x1
x2
(
x1
x4
(
x1
x7
(
x1
x5
x9
)
)
)
)
)
)
Theorem
26cbb..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x9
(
x1
x2
(
x1
x8
(
x1
x3
x5
)
)
)
)
)
)
(proof)
Theorem
d0500..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x7
(
x1
x9
(
x1
x2
(
x1
x8
(
x1
x3
x5
)
)
)
)
)
)
(proof)
Known
a508b..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x8
(
x1
x3
(
x1
x7
x9
)
)
)
)
)
)
Theorem
37638..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x9
(
x1
x3
(
x1
x8
x7
)
)
)
)
)
)
(proof)
Theorem
39fa5..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x9
(
x1
x3
(
x1
x8
x7
)
)
)
)
)
)
(proof)
Theorem
17fd5..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x9
(
x1
x3
(
x1
x7
x8
)
)
)
)
)
)
(proof)
Theorem
2c2c2..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x9
(
x1
x3
(
x1
x7
x8
)
)
)
)
)
)
(proof)
Known
793d0..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x4
(
x1
x2
(
x1
x8
(
x1
x6
(
x1
x7
x9
)
)
)
)
)
)
Theorem
8c78a..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x9
(
x1
x7
(
x1
x8
x3
)
)
)
)
)
)
(proof)
Theorem
a41d9..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x9
(
x1
x7
(
x1
x8
x3
)
)
)
)
)
)
(proof)
Known
20873..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x8
(
x1
x7
(
x1
x3
x9
)
)
)
)
)
)
Theorem
ea5e9..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x9
(
x1
x7
(
x1
x3
x8
)
)
)
)
)
)
(proof)
Theorem
98e8e..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x9
(
x1
x7
(
x1
x3
x8
)
)
)
)
)
)
(proof)
Known
1a1cd..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x4
(
x1
x2
(
x1
x8
(
x1
x7
(
x1
x6
x9
)
)
)
)
)
)
Theorem
4afed..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x9
(
x1
x8
(
x1
x7
x3
)
)
)
)
)
)
(proof)
Theorem
af600..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x9
(
x1
x8
(
x1
x7
x3
)
)
)
)
)
)
(proof)
Theorem
b5a7e..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x9
(
x1
x8
(
x1
x3
x7
)
)
)
)
)
)
(proof)
Theorem
e21d1..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x9
(
x1
x8
(
x1
x3
x7
)
)
)
)
)
)
(proof)
Known
b35e9..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x7
(
x1
x3
x8
)
)
)
)
)
Theorem
88285..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x8
(
x1
x3
(
x1
x9
x7
)
)
)
)
)
)
(proof)
Theorem
f5dd7..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x8
(
x1
x3
(
x1
x9
x7
)
)
)
)
)
)
(proof)
Known
e3d8e..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x4
(
x1
x2
(
x1
x7
(
x1
x6
x8
)
)
)
)
)
Theorem
731dd..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x8
(
x1
x7
(
x1
x9
x3
)
)
)
)
)
)
(proof)
Theorem
37010..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x8
(
x1
x7
(
x1
x9
x3
)
)
)
)
)
)
(proof)
Theorem
05e13..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x8
(
x1
x9
(
x1
x7
x3
)
)
)
)
)
)
(proof)
Theorem
b7ebc..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x8
(
x1
x9
(
x1
x7
x3
)
)
)
)
)
)
(proof)
Known
51e9c..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x7
(
x1
x8
(
x1
x3
x9
)
)
)
)
)
)
Theorem
9fde3..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x8
(
x1
x9
(
x1
x3
x7
)
)
)
)
)
)
(proof)
Theorem
8b0ad..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x8
(
x1
x9
(
x1
x3
x7
)
)
)
)
)
)
(proof)
Theorem
e622d..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x7
(
x1
x3
(
x1
x9
x8
)
)
)
)
)
)
(proof)
Theorem
87f69..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x7
(
x1
x3
(
x1
x9
x8
)
)
)
)
)
)
(proof)
Known
ac781..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x3
(
x1
x4
(
x1
x2
x6
)
)
)
Theorem
788f3..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x7
(
x1
x8
(
x1
x9
x3
)
)
)
)
)
)
(proof)
Theorem
64260..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x7
(
x1
x8
(
x1
x9
x3
)
)
)
)
)
)
(proof)
Known
c6aae..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x4
(
x1
x2
(
x1
x6
(
x1
x8
(
x1
x7
x9
)
)
)
)
)
)
Theorem
5f7fd..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x7
(
x1
x9
(
x1
x8
x3
)
)
)
)
)
)
(proof)
Theorem
f7692..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x7
(
x1
x9
(
x1
x8
x3
)
)
)
)
)
)
(proof)
Theorem
17751..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x7
(
x1
x9
(
x1
x3
x8
)
)
)
)
)
)
(proof)
Theorem
1fd08..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x7
(
x1
x9
(
x1
x3
x8
)
)
)
)
)
)
(proof)
Known
0f4fc..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x6
(
x1
x4
(
x1
x5
(
x1
x2
(
x1
x3
x7
)
)
)
)
Theorem
8bf49..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x3
(
x1
x7
(
x1
x9
x8
)
)
)
)
)
)
(proof)
Theorem
21001..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x3
(
x1
x7
(
x1
x9
x8
)
)
)
)
)
)
(proof)
Theorem
11c9e..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x3
(
x1
x8
(
x1
x9
x7
)
)
)
)
)
)
(proof)
Theorem
c02b9..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x3
(
x1
x8
(
x1
x9
x7
)
)
)
)
)
)
(proof)
Known
843b0..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x3
(
x1
x8
(
x1
x7
x9
)
)
)
)
)
)
Theorem
5748c..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x3
(
x1
x9
(
x1
x8
x7
)
)
)
)
)
)
(proof)
Theorem
75c03..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x3
(
x1
x9
(
x1
x8
x7
)
)
)
)
)
)
(proof)
Theorem
e1e2e..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x3
(
x1
x9
(
x1
x7
x8
)
)
)
)
)
)
(proof)
Theorem
bf91f..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x2
(
x1
x3
(
x1
x9
(
x1
x7
x8
)
)
)
)
)
)
(proof)
Known
5b962..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x6
(
x1
x4
(
x1
x5
(
x1
x3
(
x1
x2
x7
)
)
)
)
Theorem
b6d0f..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x3
(
x1
x2
(
x1
x7
(
x1
x9
x8
)
)
)
)
)
)
(proof)
Theorem
017cf..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 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
x5
(
x1
x3
(
x1
x2
(
x1
x7
(
x1
x9
x8
)
)
)
)
)
)
(proof)