Search for blocks/addresses/...
Proofgold Asset
asset id
52e41077f4bff31c4ef9937a96cedfb969a8e0e30afc0e0ef4b99d43abd33dbe
asset hash
80ad6728a5d625f1b66982289ab4d0a3cb003eed4a82310e46a8907eb1e1ad8e
bday / block
24271
tx
6b678..
preasset
doc published by
Pr5Zc..
Theorem
547c4..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x2
(
x1
x3
(
x1
x4
x5
)
)
x6
=
x1
(
x2
x3
x6
)
(
x1
(
x2
x4
x6
)
(
x2
x5
x6
)
)
(proof)
Known
e11b7..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x2
(
x1
x3
x4
)
)
Theorem
81c99..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
x6
)
)
)
x7
=
x1
(
x2
x3
x7
)
(
x1
(
x2
x4
x7
)
(
x1
(
x2
x5
x7
)
(
x2
x6
x7
)
)
)
(proof)
Known
25618..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
∀ x2 x3 x4 x5 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
(
x1
x2
(
x1
x3
(
x1
x4
x5
)
)
)
Theorem
bc000..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x7
)
)
)
)
x8
=
x1
(
x2
x3
x8
)
(
x1
(
x2
x4
x8
)
(
x1
(
x2
x5
x8
)
(
x1
(
x2
x6
x8
)
(
x2
x7
x8
)
)
)
)
(proof)
Known
b9f0e..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
∀ x2 x3 x4 x5 x6 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x6
)
)
)
)
Theorem
a4026..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
x8
)
)
)
)
)
x9
=
x1
(
x2
x3
x9
)
(
x1
(
x2
x4
x9
)
(
x1
(
x2
x5
x9
)
(
x1
(
x2
x6
x9
)
(
x1
(
x2
x7
x9
)
(
x2
x8
x9
)
)
)
)
)
(proof)
Known
2a50e..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x7
)
)
)
)
)
Theorem
6ee59..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
x9
)
)
)
)
)
)
x10
=
x1
(
x2
x3
x10
)
(
x1
(
x2
x4
x10
)
(
x1
(
x2
x5
x10
)
(
x1
(
x2
x6
x10
)
(
x1
(
x2
x7
x10
)
(
x1
(
x2
x8
x10
)
(
x2
x9
x10
)
)
)
)
)
)
(proof)
Known
948ae..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
x8
)
)
)
)
)
)
Theorem
2fffd..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
x10
)
)
)
)
)
)
)
x11
=
x1
(
x2
x3
x11
)
(
x1
(
x2
x4
x11
)
(
x1
(
x2
x5
x11
)
(
x1
(
x2
x6
x11
)
(
x1
(
x2
x7
x11
)
(
x1
(
x2
x8
x11
)
(
x1
(
x2
x9
x11
)
(
x2
x10
x11
)
)
)
)
)
)
)
(proof)
Known
18faf..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
x9
)
)
)
)
)
)
)
Theorem
de9e9..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
x11
)
)
)
)
)
)
)
)
x12
=
x1
(
x2
x3
x12
)
(
x1
(
x2
x4
x12
)
(
x1
(
x2
x5
x12
)
(
x1
(
x2
x6
x12
)
(
x1
(
x2
x7
x12
)
(
x1
(
x2
x8
x12
)
(
x1
(
x2
x9
x12
)
(
x1
(
x2
x10
x12
)
(
x2
x11
x12
)
)
)
)
)
)
)
)
(proof)
Known
880a1..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
x10
)
)
)
)
)
)
)
)
Theorem
6c866..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
x12
)
)
)
)
)
)
)
)
)
x13
=
x1
(
x2
x3
x13
)
(
x1
(
x2
x4
x13
)
(
x1
(
x2
x5
x13
)
(
x1
(
x2
x6
x13
)
(
x1
(
x2
x7
x13
)
(
x1
(
x2
x8
x13
)
(
x1
(
x2
x9
x13
)
(
x1
(
x2
x10
x13
)
(
x1
(
x2
x11
x13
)
(
x2
x12
x13
)
)
)
)
)
)
)
)
)
(proof)
Known
737fb..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
x11
)
)
)
)
)
)
)
)
)
Theorem
1fe00..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
)
)
)
)
)
)
)
x14
=
x1
(
x2
x3
x14
)
(
x1
(
x2
x4
x14
)
(
x1
(
x2
x5
x14
)
(
x1
(
x2
x6
x14
)
(
x1
(
x2
x7
x14
)
(
x1
(
x2
x8
x14
)
(
x1
(
x2
x9
x14
)
(
x1
(
x2
x10
x14
)
(
x1
(
x2
x11
x14
)
(
x1
(
x2
x12
x14
)
(
x2
x13
x14
)
)
)
)
)
)
)
)
)
)
(proof)
Known
f7821..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
x12
)
)
)
)
)
)
)
)
)
)
Theorem
2555f..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
x14
)
)
)
)
)
)
)
)
)
)
)
x15
=
x1
(
x2
x3
x15
)
(
x1
(
x2
x4
x15
)
(
x1
(
x2
x5
x15
)
(
x1
(
x2
x6
x15
)
(
x1
(
x2
x7
x15
)
(
x1
(
x2
x8
x15
)
(
x1
(
x2
x9
x15
)
(
x1
(
x2
x10
x15
)
(
x1
(
x2
x11
x15
)
(
x1
(
x2
x12
x15
)
(
x1
(
x2
x13
x15
)
(
x2
x14
x15
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
2c5ad..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
)
)
)
)
)
)
)
)
Theorem
3841c..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
x15
)
)
)
)
)
)
)
)
)
)
)
)
x16
=
x1
(
x2
x3
x16
)
(
x1
(
x2
x4
x16
)
(
x1
(
x2
x5
x16
)
(
x1
(
x2
x6
x16
)
(
x1
(
x2
x7
x16
)
(
x1
(
x2
x8
x16
)
(
x1
(
x2
x9
x16
)
(
x1
(
x2
x10
x16
)
(
x1
(
x2
x11
x16
)
(
x1
(
x2
x12
x16
)
(
x1
(
x2
x13
x16
)
(
x1
(
x2
x14
x16
)
(
x2
x15
x16
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
ea7b1..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
x14
)
)
)
)
)
)
)
)
)
)
)
)
Theorem
8454f..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
x17
=
x1
(
x2
x3
x17
)
(
x1
(
x2
x4
x17
)
(
x1
(
x2
x5
x17
)
(
x1
(
x2
x6
x17
)
(
x1
(
x2
x7
x17
)
(
x1
(
x2
x8
x17
)
(
x1
(
x2
x9
x17
)
(
x1
(
x2
x10
x17
)
(
x1
(
x2
x11
x17
)
(
x1
(
x2
x12
x17
)
(
x1
(
x2
x13
x17
)
(
x1
(
x2
x14
x17
)
(
x1
(
x2
x15
x17
)
(
x2
x16
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
6cd80..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
x15
)
)
)
)
)
)
)
)
)
)
)
)
)
Theorem
1d55a..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x0
x18
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
x18
=
x1
(
x2
x3
x18
)
(
x1
(
x2
x4
x18
)
(
x1
(
x2
x5
x18
)
(
x1
(
x2
x6
x18
)
(
x1
(
x2
x7
x18
)
(
x1
(
x2
x8
x18
)
(
x1
(
x2
x9
x18
)
(
x1
(
x2
x10
x18
)
(
x1
(
x2
x11
x18
)
(
x1
(
x2
x12
x18
)
(
x1
(
x2
x13
x18
)
(
x1
(
x2
x14
x18
)
(
x1
(
x2
x15
x18
)
(
x1
(
x2
x16
x18
)
(
x2
x17
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
855a7..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
)
Theorem
d1d81..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x0
x18
⟶
x0
x19
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
x19
=
x1
(
x2
x3
x19
)
(
x1
(
x2
x4
x19
)
(
x1
(
x2
x5
x19
)
(
x1
(
x2
x6
x19
)
(
x1
(
x2
x7
x19
)
(
x1
(
x2
x8
x19
)
(
x1
(
x2
x9
x19
)
(
x1
(
x2
x10
x19
)
(
x1
(
x2
x11
x19
)
(
x1
(
x2
x12
x19
)
(
x1
(
x2
x13
x19
)
(
x1
(
x2
x14
x19
)
(
x1
(
x2
x15
x19
)
(
x1
(
x2
x16
x19
)
(
x1
(
x2
x17
x19
)
(
x2
x18
x19
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
cebfe..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
∀ x3 x4 x5 x6 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x2
x6
(
x1
x3
(
x1
x4
x5
)
)
=
x1
(
x2
x6
x3
)
(
x1
(
x2
x6
x4
)
(
x2
x6
x5
)
)
(proof)
Theorem
bbdc7..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x2
x7
(
x1
x3
(
x1
x4
(
x1
x5
x6
)
)
)
=
x1
(
x2
x7
x3
)
(
x1
(
x2
x7
x4
)
(
x1
(
x2
x7
x5
)
(
x2
x7
x6
)
)
)
(proof)
Theorem
6831b..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x2
x8
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x7
)
)
)
)
=
x1
(
x2
x8
x3
)
(
x1
(
x2
x8
x4
)
(
x1
(
x2
x8
x5
)
(
x1
(
x2
x8
x6
)
(
x2
x8
x7
)
)
)
)
(proof)
Theorem
67024..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x2
x9
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
x8
)
)
)
)
)
=
x1
(
x2
x9
x3
)
(
x1
(
x2
x9
x4
)
(
x1
(
x2
x9
x5
)
(
x1
(
x2
x9
x6
)
(
x1
(
x2
x9
x7
)
(
x2
x9
x8
)
)
)
)
)
(proof)
Theorem
fc0c5..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x2
x10
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
x9
)
)
)
)
)
)
=
x1
(
x2
x10
x3
)
(
x1
(
x2
x10
x4
)
(
x1
(
x2
x10
x5
)
(
x1
(
x2
x10
x6
)
(
x1
(
x2
x10
x7
)
(
x1
(
x2
x10
x8
)
(
x2
x10
x9
)
)
)
)
)
)
(proof)
Theorem
128a5..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x2
x11
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
x10
)
)
)
)
)
)
)
=
x1
(
x2
x11
x3
)
(
x1
(
x2
x11
x4
)
(
x1
(
x2
x11
x5
)
(
x1
(
x2
x11
x6
)
(
x1
(
x2
x11
x7
)
(
x1
(
x2
x11
x8
)
(
x1
(
x2
x11
x9
)
(
x2
x11
x10
)
)
)
)
)
)
)
(proof)
Theorem
3eed7..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x2
x12
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
x11
)
)
)
)
)
)
)
)
=
x1
(
x2
x12
x3
)
(
x1
(
x2
x12
x4
)
(
x1
(
x2
x12
x5
)
(
x1
(
x2
x12
x6
)
(
x1
(
x2
x12
x7
)
(
x1
(
x2
x12
x8
)
(
x1
(
x2
x12
x9
)
(
x1
(
x2
x12
x10
)
(
x2
x12
x11
)
)
)
)
)
)
)
)
(proof)
Theorem
83656..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x2
x13
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
x12
)
)
)
)
)
)
)
)
)
=
x1
(
x2
x13
x3
)
(
x1
(
x2
x13
x4
)
(
x1
(
x2
x13
x5
)
(
x1
(
x2
x13
x6
)
(
x1
(
x2
x13
x7
)
(
x1
(
x2
x13
x8
)
(
x1
(
x2
x13
x9
)
(
x1
(
x2
x13
x10
)
(
x1
(
x2
x13
x11
)
(
x2
x13
x12
)
)
)
)
)
)
)
)
)
(proof)
Theorem
e214f..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x2
x14
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
)
)
)
)
)
)
)
=
x1
(
x2
x14
x3
)
(
x1
(
x2
x14
x4
)
(
x1
(
x2
x14
x5
)
(
x1
(
x2
x14
x6
)
(
x1
(
x2
x14
x7
)
(
x1
(
x2
x14
x8
)
(
x1
(
x2
x14
x9
)
(
x1
(
x2
x14
x10
)
(
x1
(
x2
x14
x11
)
(
x1
(
x2
x14
x12
)
(
x2
x14
x13
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
3d6c4..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x2
x15
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
x14
)
)
)
)
)
)
)
)
)
)
)
=
x1
(
x2
x15
x3
)
(
x1
(
x2
x15
x4
)
(
x1
(
x2
x15
x5
)
(
x1
(
x2
x15
x6
)
(
x1
(
x2
x15
x7
)
(
x1
(
x2
x15
x8
)
(
x1
(
x2
x15
x9
)
(
x1
(
x2
x15
x10
)
(
x1
(
x2
x15
x11
)
(
x1
(
x2
x15
x12
)
(
x1
(
x2
x15
x13
)
(
x2
x15
x14
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
22e9e..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x2
x16
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
x15
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
(
x2
x16
x3
)
(
x1
(
x2
x16
x4
)
(
x1
(
x2
x16
x5
)
(
x1
(
x2
x16
x6
)
(
x1
(
x2
x16
x7
)
(
x1
(
x2
x16
x8
)
(
x1
(
x2
x16
x9
)
(
x1
(
x2
x16
x10
)
(
x1
(
x2
x16
x11
)
(
x1
(
x2
x16
x12
)
(
x1
(
x2
x16
x13
)
(
x1
(
x2
x16
x14
)
(
x2
x16
x15
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
068aa..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x2
x17
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
(
x2
x17
x3
)
(
x1
(
x2
x17
x4
)
(
x1
(
x2
x17
x5
)
(
x1
(
x2
x17
x6
)
(
x1
(
x2
x17
x7
)
(
x1
(
x2
x17
x8
)
(
x1
(
x2
x17
x9
)
(
x1
(
x2
x17
x10
)
(
x1
(
x2
x17
x11
)
(
x1
(
x2
x17
x12
)
(
x1
(
x2
x17
x13
)
(
x1
(
x2
x17
x14
)
(
x1
(
x2
x17
x15
)
(
x2
x17
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
20ea2..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x0
x18
⟶
x2
x18
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
(
x2
x18
x3
)
(
x1
(
x2
x18
x4
)
(
x1
(
x2
x18
x5
)
(
x1
(
x2
x18
x6
)
(
x1
(
x2
x18
x7
)
(
x1
(
x2
x18
x8
)
(
x1
(
x2
x18
x9
)
(
x1
(
x2
x18
x10
)
(
x1
(
x2
x18
x11
)
(
x1
(
x2
x18
x12
)
(
x1
(
x2
x18
x13
)
(
x1
(
x2
x18
x14
)
(
x1
(
x2
x18
x15
)
(
x1
(
x2
x18
x16
)
(
x2
x18
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
44d11..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x0
x18
⟶
x0
x19
⟶
x2
x19
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
(
x2
x19
x3
)
(
x1
(
x2
x19
x4
)
(
x1
(
x2
x19
x5
)
(
x1
(
x2
x19
x6
)
(
x1
(
x2
x19
x7
)
(
x1
(
x2
x19
x8
)
(
x1
(
x2
x19
x9
)
(
x1
(
x2
x19
x10
)
(
x1
(
x2
x19
x11
)
(
x1
(
x2
x19
x12
)
(
x1
(
x2
x19
x13
)
(
x1
(
x2
x19
x14
)
(
x1
(
x2
x19
x15
)
(
x1
(
x2
x19
x16
)
(
x1
(
x2
x19
x17
)
(
x2
x19
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
c50dc..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x2
(
x1
x3
x4
)
(
x1
x5
x6
)
=
x1
(
x1
(
x2
x3
x5
)
(
x2
x3
x6
)
)
(
x1
(
x2
x4
x5
)
(
x2
x4
x6
)
)
(proof)
Theorem
f7342..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x2
(
x1
x3
x4
)
(
x1
x5
(
x1
x6
x7
)
)
=
x1
(
x1
(
x2
x3
x5
)
(
x1
(
x2
x3
x6
)
(
x2
x3
x7
)
)
)
(
x1
(
x2
x4
x5
)
(
x1
(
x2
x4
x6
)
(
x2
x4
x7
)
)
)
(proof)
Theorem
385a8..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x2
(
x1
x3
x4
)
(
x1
x5
(
x1
x6
(
x1
x7
x8
)
)
)
=
x1
(
x1
(
x2
x3
x5
)
(
x1
(
x2
x3
x6
)
(
x1
(
x2
x3
x7
)
(
x2
x3
x8
)
)
)
)
(
x1
(
x2
x4
x5
)
(
x1
(
x2
x4
x6
)
(
x1
(
x2
x4
x7
)
(
x2
x4
x8
)
)
)
)
(proof)
Theorem
99370..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x2
(
x1
x3
x4
)
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
x9
)
)
)
)
=
x1
(
x1
(
x2
x3
x5
)
(
x1
(
x2
x3
x6
)
(
x1
(
x2
x3
x7
)
(
x1
(
x2
x3
x8
)
(
x2
x3
x9
)
)
)
)
)
(
x1
(
x2
x4
x5
)
(
x1
(
x2
x4
x6
)
(
x1
(
x2
x4
x7
)
(
x1
(
x2
x4
x8
)
(
x2
x4
x9
)
)
)
)
)
(proof)
Theorem
7e8a0..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x2
(
x1
x3
x4
)
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
x10
)
)
)
)
)
=
x1
(
x1
(
x2
x3
x5
)
(
x1
(
x2
x3
x6
)
(
x1
(
x2
x3
x7
)
(
x1
(
x2
x3
x8
)
(
x1
(
x2
x3
x9
)
(
x2
x3
x10
)
)
)
)
)
)
(
x1
(
x2
x4
x5
)
(
x1
(
x2
x4
x6
)
(
x1
(
x2
x4
x7
)
(
x1
(
x2
x4
x8
)
(
x1
(
x2
x4
x9
)
(
x2
x4
x10
)
)
)
)
)
)
(proof)
Theorem
2987b..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x2
(
x1
x3
x4
)
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
x11
)
)
)
)
)
)
=
x1
(
x1
(
x2
x3
x5
)
(
x1
(
x2
x3
x6
)
(
x1
(
x2
x3
x7
)
(
x1
(
x2
x3
x8
)
(
x1
(
x2
x3
x9
)
(
x1
(
x2
x3
x10
)
(
x2
x3
x11
)
)
)
)
)
)
)
(
x1
(
x2
x4
x5
)
(
x1
(
x2
x4
x6
)
(
x1
(
x2
x4
x7
)
(
x1
(
x2
x4
x8
)
(
x1
(
x2
x4
x9
)
(
x1
(
x2
x4
x10
)
(
x2
x4
x11
)
)
)
)
)
)
)
(proof)
Theorem
65828..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x2
(
x1
x3
x4
)
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
x12
)
)
)
)
)
)
)
=
x1
(
x1
(
x2
x3
x5
)
(
x1
(
x2
x3
x6
)
(
x1
(
x2
x3
x7
)
(
x1
(
x2
x3
x8
)
(
x1
(
x2
x3
x9
)
(
x1
(
x2
x3
x10
)
(
x1
(
x2
x3
x11
)
(
x2
x3
x12
)
)
)
)
)
)
)
)
(
x1
(
x2
x4
x5
)
(
x1
(
x2
x4
x6
)
(
x1
(
x2
x4
x7
)
(
x1
(
x2
x4
x8
)
(
x1
(
x2
x4
x9
)
(
x1
(
x2
x4
x10
)
(
x1
(
x2
x4
x11
)
(
x2
x4
x12
)
)
)
)
)
)
)
)
(proof)
Theorem
7f9d6..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x2
(
x1
x3
(
x1
x4
x5
)
)
(
x1
x6
x7
)
=
x1
(
x1
(
x2
x3
x6
)
(
x2
x3
x7
)
)
(
x1
(
x1
(
x2
x4
x6
)
(
x2
x4
x7
)
)
(
x1
(
x2
x5
x6
)
(
x2
x5
x7
)
)
)
(proof)
Theorem
ef027..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x2
(
x1
x3
(
x1
x4
x5
)
)
(
x1
x6
(
x1
x7
x8
)
)
=
x1
(
x1
(
x2
x3
x6
)
(
x1
(
x2
x3
x7
)
(
x2
x3
x8
)
)
)
(
x1
(
x1
(
x2
x4
x6
)
(
x1
(
x2
x4
x7
)
(
x2
x4
x8
)
)
)
(
x1
(
x2
x5
x6
)
(
x1
(
x2
x5
x7
)
(
x2
x5
x8
)
)
)
)
(proof)
Theorem
06c4f..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x2
(
x1
x3
(
x1
x4
x5
)
)
(
x1
x6
(
x1
x7
(
x1
x8
x9
)
)
)
=
x1
(
x1
(
x2
x3
x6
)
(
x1
(
x2
x3
x7
)
(
x1
(
x2
x3
x8
)
(
x2
x3
x9
)
)
)
)
(
x1
(
x1
(
x2
x4
x6
)
(
x1
(
x2
x4
x7
)
(
x1
(
x2
x4
x8
)
(
x2
x4
x9
)
)
)
)
(
x1
(
x2
x5
x6
)
(
x1
(
x2
x5
x7
)
(
x1
(
x2
x5
x8
)
(
x2
x5
x9
)
)
)
)
)
(proof)
Theorem
ef15c..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x2
(
x1
x3
(
x1
x4
x5
)
)
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
x10
)
)
)
)
=
x1
(
x1
(
x2
x3
x6
)
(
x1
(
x2
x3
x7
)
(
x1
(
x2
x3
x8
)
(
x1
(
x2
x3
x9
)
(
x2
x3
x10
)
)
)
)
)
(
x1
(
x1
(
x2
x4
x6
)
(
x1
(
x2
x4
x7
)
(
x1
(
x2
x4
x8
)
(
x1
(
x2
x4
x9
)
(
x2
x4
x10
)
)
)
)
)
(
x1
(
x2
x5
x6
)
(
x1
(
x2
x5
x7
)
(
x1
(
x2
x5
x8
)
(
x1
(
x2
x5
x9
)
(
x2
x5
x10
)
)
)
)
)
)
(proof)
Theorem
24435..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x2
(
x1
x3
(
x1
x4
x5
)
)
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
x11
)
)
)
)
)
=
x1
(
x1
(
x2
x3
x6
)
(
x1
(
x2
x3
x7
)
(
x1
(
x2
x3
x8
)
(
x1
(
x2
x3
x9
)
(
x1
(
x2
x3
x10
)
(
x2
x3
x11
)
)
)
)
)
)
(
x1
(
x1
(
x2
x4
x6
)
(
x1
(
x2
x4
x7
)
(
x1
(
x2
x4
x8
)
(
x1
(
x2
x4
x9
)
(
x1
(
x2
x4
x10
)
(
x2
x4
x11
)
)
)
)
)
)
(
x1
(
x2
x5
x6
)
(
x1
(
x2
x5
x7
)
(
x1
(
x2
x5
x8
)
(
x1
(
x2
x5
x9
)
(
x1
(
x2
x5
x10
)
(
x2
x5
x11
)
)
)
)
)
)
)
(proof)
Theorem
6b961..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x2
(
x1
x3
(
x1
x4
x5
)
)
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
x12
)
)
)
)
)
)
=
x1
(
x1
(
x2
x3
x6
)
(
x1
(
x2
x3
x7
)
(
x1
(
x2
x3
x8
)
(
x1
(
x2
x3
x9
)
(
x1
(
x2
x3
x10
)
(
x1
(
x2
x3
x11
)
(
x2
x3
x12
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x4
x6
)
(
x1
(
x2
x4
x7
)
(
x1
(
x2
x4
x8
)
(
x1
(
x2
x4
x9
)
(
x1
(
x2
x4
x10
)
(
x1
(
x2
x4
x11
)
(
x2
x4
x12
)
)
)
)
)
)
)
(
x1
(
x2
x5
x6
)
(
x1
(
x2
x5
x7
)
(
x1
(
x2
x5
x8
)
(
x1
(
x2
x5
x9
)
(
x1
(
x2
x5
x10
)
(
x1
(
x2
x5
x11
)
(
x2
x5
x12
)
)
)
)
)
)
)
)
(proof)
Theorem
3ba1a..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x2
(
x1
x3
(
x1
x4
x5
)
)
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
)
)
)
)
=
x1
(
x1
(
x2
x3
x6
)
(
x1
(
x2
x3
x7
)
(
x1
(
x2
x3
x8
)
(
x1
(
x2
x3
x9
)
(
x1
(
x2
x3
x10
)
(
x1
(
x2
x3
x11
)
(
x1
(
x2
x3
x12
)
(
x2
x3
x13
)
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x4
x6
)
(
x1
(
x2
x4
x7
)
(
x1
(
x2
x4
x8
)
(
x1
(
x2
x4
x9
)
(
x1
(
x2
x4
x10
)
(
x1
(
x2
x4
x11
)
(
x1
(
x2
x4
x12
)
(
x2
x4
x13
)
)
)
)
)
)
)
)
(
x1
(
x2
x5
x6
)
(
x1
(
x2
x5
x7
)
(
x1
(
x2
x5
x8
)
(
x1
(
x2
x5
x9
)
(
x1
(
x2
x5
x10
)
(
x1
(
x2
x5
x11
)
(
x1
(
x2
x5
x12
)
(
x2
x5
x13
)
)
)
)
)
)
)
)
)
(proof)
Theorem
bdad1..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
x6
)
)
)
(
x1
x7
x8
)
=
x1
(
x1
(
x2
x3
x7
)
(
x2
x3
x8
)
)
(
x1
(
x1
(
x2
x4
x7
)
(
x2
x4
x8
)
)
(
x1
(
x1
(
x2
x5
x7
)
(
x2
x5
x8
)
)
(
x1
(
x2
x6
x7
)
(
x2
x6
x8
)
)
)
)
(proof)
Theorem
037b6..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
x6
)
)
)
(
x1
x7
(
x1
x8
x9
)
)
=
x1
(
x1
(
x2
x3
x7
)
(
x1
(
x2
x3
x8
)
(
x2
x3
x9
)
)
)
(
x1
(
x1
(
x2
x4
x7
)
(
x1
(
x2
x4
x8
)
(
x2
x4
x9
)
)
)
(
x1
(
x1
(
x2
x5
x7
)
(
x1
(
x2
x5
x8
)
(
x2
x5
x9
)
)
)
(
x1
(
x2
x6
x7
)
(
x1
(
x2
x6
x8
)
(
x2
x6
x9
)
)
)
)
)
(proof)
Theorem
70471..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
x6
)
)
)
(
x1
x7
(
x1
x8
(
x1
x9
x10
)
)
)
=
x1
(
x1
(
x2
x3
x7
)
(
x1
(
x2
x3
x8
)
(
x1
(
x2
x3
x9
)
(
x2
x3
x10
)
)
)
)
(
x1
(
x1
(
x2
x4
x7
)
(
x1
(
x2
x4
x8
)
(
x1
(
x2
x4
x9
)
(
x2
x4
x10
)
)
)
)
(
x1
(
x1
(
x2
x5
x7
)
(
x1
(
x2
x5
x8
)
(
x1
(
x2
x5
x9
)
(
x2
x5
x10
)
)
)
)
(
x1
(
x2
x6
x7
)
(
x1
(
x2
x6
x8
)
(
x1
(
x2
x6
x9
)
(
x2
x6
x10
)
)
)
)
)
)
(proof)
Theorem
34a9f..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
x6
)
)
)
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
x11
)
)
)
)
=
x1
(
x1
(
x2
x3
x7
)
(
x1
(
x2
x3
x8
)
(
x1
(
x2
x3
x9
)
(
x1
(
x2
x3
x10
)
(
x2
x3
x11
)
)
)
)
)
(
x1
(
x1
(
x2
x4
x7
)
(
x1
(
x2
x4
x8
)
(
x1
(
x2
x4
x9
)
(
x1
(
x2
x4
x10
)
(
x2
x4
x11
)
)
)
)
)
(
x1
(
x1
(
x2
x5
x7
)
(
x1
(
x2
x5
x8
)
(
x1
(
x2
x5
x9
)
(
x1
(
x2
x5
x10
)
(
x2
x5
x11
)
)
)
)
)
(
x1
(
x2
x6
x7
)
(
x1
(
x2
x6
x8
)
(
x1
(
x2
x6
x9
)
(
x1
(
x2
x6
x10
)
(
x2
x6
x11
)
)
)
)
)
)
)
(proof)
Theorem
c5a67..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
x6
)
)
)
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
x12
)
)
)
)
)
=
x1
(
x1
(
x2
x3
x7
)
(
x1
(
x2
x3
x8
)
(
x1
(
x2
x3
x9
)
(
x1
(
x2
x3
x10
)
(
x1
(
x2
x3
x11
)
(
x2
x3
x12
)
)
)
)
)
)
(
x1
(
x1
(
x2
x4
x7
)
(
x1
(
x2
x4
x8
)
(
x1
(
x2
x4
x9
)
(
x1
(
x2
x4
x10
)
(
x1
(
x2
x4
x11
)
(
x2
x4
x12
)
)
)
)
)
)
(
x1
(
x1
(
x2
x5
x7
)
(
x1
(
x2
x5
x8
)
(
x1
(
x2
x5
x9
)
(
x1
(
x2
x5
x10
)
(
x1
(
x2
x5
x11
)
(
x2
x5
x12
)
)
)
)
)
)
(
x1
(
x2
x6
x7
)
(
x1
(
x2
x6
x8
)
(
x1
(
x2
x6
x9
)
(
x1
(
x2
x6
x10
)
(
x1
(
x2
x6
x11
)
(
x2
x6
x12
)
)
)
)
)
)
)
)
(proof)
Theorem
a4275..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
x6
)
)
)
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
)
)
)
=
x1
(
x1
(
x2
x3
x7
)
(
x1
(
x2
x3
x8
)
(
x1
(
x2
x3
x9
)
(
x1
(
x2
x3
x10
)
(
x1
(
x2
x3
x11
)
(
x1
(
x2
x3
x12
)
(
x2
x3
x13
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x4
x7
)
(
x1
(
x2
x4
x8
)
(
x1
(
x2
x4
x9
)
(
x1
(
x2
x4
x10
)
(
x1
(
x2
x4
x11
)
(
x1
(
x2
x4
x12
)
(
x2
x4
x13
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x5
x7
)
(
x1
(
x2
x5
x8
)
(
x1
(
x2
x5
x9
)
(
x1
(
x2
x5
x10
)
(
x1
(
x2
x5
x11
)
(
x1
(
x2
x5
x12
)
(
x2
x5
x13
)
)
)
)
)
)
)
(
x1
(
x2
x6
x7
)
(
x1
(
x2
x6
x8
)
(
x1
(
x2
x6
x9
)
(
x1
(
x2
x6
x10
)
(
x1
(
x2
x6
x11
)
(
x1
(
x2
x6
x12
)
(
x2
x6
x13
)
)
)
)
)
)
)
)
)
(proof)
Theorem
acdf7..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
x6
)
)
)
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
x14
)
)
)
)
)
)
)
=
x1
(
x1
(
x2
x3
x7
)
(
x1
(
x2
x3
x8
)
(
x1
(
x2
x3
x9
)
(
x1
(
x2
x3
x10
)
(
x1
(
x2
x3
x11
)
(
x1
(
x2
x3
x12
)
(
x1
(
x2
x3
x13
)
(
x2
x3
x14
)
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x4
x7
)
(
x1
(
x2
x4
x8
)
(
x1
(
x2
x4
x9
)
(
x1
(
x2
x4
x10
)
(
x1
(
x2
x4
x11
)
(
x1
(
x2
x4
x12
)
(
x1
(
x2
x4
x13
)
(
x2
x4
x14
)
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x5
x7
)
(
x1
(
x2
x5
x8
)
(
x1
(
x2
x5
x9
)
(
x1
(
x2
x5
x10
)
(
x1
(
x2
x5
x11
)
(
x1
(
x2
x5
x12
)
(
x1
(
x2
x5
x13
)
(
x2
x5
x14
)
)
)
)
)
)
)
)
(
x1
(
x2
x6
x7
)
(
x1
(
x2
x6
x8
)
(
x1
(
x2
x6
x9
)
(
x1
(
x2
x6
x10
)
(
x1
(
x2
x6
x11
)
(
x1
(
x2
x6
x12
)
(
x1
(
x2
x6
x13
)
(
x2
x6
x14
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
1634a..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x7
)
)
)
)
(
x1
x8
x9
)
=
x1
(
x1
(
x2
x3
x8
)
(
x2
x3
x9
)
)
(
x1
(
x1
(
x2
x4
x8
)
(
x2
x4
x9
)
)
(
x1
(
x1
(
x2
x5
x8
)
(
x2
x5
x9
)
)
(
x1
(
x1
(
x2
x6
x8
)
(
x2
x6
x9
)
)
(
x1
(
x2
x7
x8
)
(
x2
x7
x9
)
)
)
)
)
(proof)
Theorem
9d4e1..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x7
)
)
)
)
(
x1
x8
(
x1
x9
x10
)
)
=
x1
(
x1
(
x2
x3
x8
)
(
x1
(
x2
x3
x9
)
(
x2
x3
x10
)
)
)
(
x1
(
x1
(
x2
x4
x8
)
(
x1
(
x2
x4
x9
)
(
x2
x4
x10
)
)
)
(
x1
(
x1
(
x2
x5
x8
)
(
x1
(
x2
x5
x9
)
(
x2
x5
x10
)
)
)
(
x1
(
x1
(
x2
x6
x8
)
(
x1
(
x2
x6
x9
)
(
x2
x6
x10
)
)
)
(
x1
(
x2
x7
x8
)
(
x1
(
x2
x7
x9
)
(
x2
x7
x10
)
)
)
)
)
)
(proof)
Theorem
96e70..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x7
)
)
)
)
(
x1
x8
(
x1
x9
(
x1
x10
x11
)
)
)
=
x1
(
x1
(
x2
x3
x8
)
(
x1
(
x2
x3
x9
)
(
x1
(
x2
x3
x10
)
(
x2
x3
x11
)
)
)
)
(
x1
(
x1
(
x2
x4
x8
)
(
x1
(
x2
x4
x9
)
(
x1
(
x2
x4
x10
)
(
x2
x4
x11
)
)
)
)
(
x1
(
x1
(
x2
x5
x8
)
(
x1
(
x2
x5
x9
)
(
x1
(
x2
x5
x10
)
(
x2
x5
x11
)
)
)
)
(
x1
(
x1
(
x2
x6
x8
)
(
x1
(
x2
x6
x9
)
(
x1
(
x2
x6
x10
)
(
x2
x6
x11
)
)
)
)
(
x1
(
x2
x7
x8
)
(
x1
(
x2
x7
x9
)
(
x1
(
x2
x7
x10
)
(
x2
x7
x11
)
)
)
)
)
)
)
(proof)
Theorem
8b8a9..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x7
)
)
)
)
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
x12
)
)
)
)
=
x1
(
x1
(
x2
x3
x8
)
(
x1
(
x2
x3
x9
)
(
x1
(
x2
x3
x10
)
(
x1
(
x2
x3
x11
)
(
x2
x3
x12
)
)
)
)
)
(
x1
(
x1
(
x2
x4
x8
)
(
x1
(
x2
x4
x9
)
(
x1
(
x2
x4
x10
)
(
x1
(
x2
x4
x11
)
(
x2
x4
x12
)
)
)
)
)
(
x1
(
x1
(
x2
x5
x8
)
(
x1
(
x2
x5
x9
)
(
x1
(
x2
x5
x10
)
(
x1
(
x2
x5
x11
)
(
x2
x5
x12
)
)
)
)
)
(
x1
(
x1
(
x2
x6
x8
)
(
x1
(
x2
x6
x9
)
(
x1
(
x2
x6
x10
)
(
x1
(
x2
x6
x11
)
(
x2
x6
x12
)
)
)
)
)
(
x1
(
x2
x7
x8
)
(
x1
(
x2
x7
x9
)
(
x1
(
x2
x7
x10
)
(
x1
(
x2
x7
x11
)
(
x2
x7
x12
)
)
)
)
)
)
)
)
(proof)
Theorem
a33b6..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x7
)
)
)
)
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
)
)
=
x1
(
x1
(
x2
x3
x8
)
(
x1
(
x2
x3
x9
)
(
x1
(
x2
x3
x10
)
(
x1
(
x2
x3
x11
)
(
x1
(
x2
x3
x12
)
(
x2
x3
x13
)
)
)
)
)
)
(
x1
(
x1
(
x2
x4
x8
)
(
x1
(
x2
x4
x9
)
(
x1
(
x2
x4
x10
)
(
x1
(
x2
x4
x11
)
(
x1
(
x2
x4
x12
)
(
x2
x4
x13
)
)
)
)
)
)
(
x1
(
x1
(
x2
x5
x8
)
(
x1
(
x2
x5
x9
)
(
x1
(
x2
x5
x10
)
(
x1
(
x2
x5
x11
)
(
x1
(
x2
x5
x12
)
(
x2
x5
x13
)
)
)
)
)
)
(
x1
(
x1
(
x2
x6
x8
)
(
x1
(
x2
x6
x9
)
(
x1
(
x2
x6
x10
)
(
x1
(
x2
x6
x11
)
(
x1
(
x2
x6
x12
)
(
x2
x6
x13
)
)
)
)
)
)
(
x1
(
x2
x7
x8
)
(
x1
(
x2
x7
x9
)
(
x1
(
x2
x7
x10
)
(
x1
(
x2
x7
x11
)
(
x1
(
x2
x7
x12
)
(
x2
x7
x13
)
)
)
)
)
)
)
)
)
(proof)
Theorem
6c6f7..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x7
)
)
)
)
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
x14
)
)
)
)
)
)
=
x1
(
x1
(
x2
x3
x8
)
(
x1
(
x2
x3
x9
)
(
x1
(
x2
x3
x10
)
(
x1
(
x2
x3
x11
)
(
x1
(
x2
x3
x12
)
(
x1
(
x2
x3
x13
)
(
x2
x3
x14
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x4
x8
)
(
x1
(
x2
x4
x9
)
(
x1
(
x2
x4
x10
)
(
x1
(
x2
x4
x11
)
(
x1
(
x2
x4
x12
)
(
x1
(
x2
x4
x13
)
(
x2
x4
x14
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x5
x8
)
(
x1
(
x2
x5
x9
)
(
x1
(
x2
x5
x10
)
(
x1
(
x2
x5
x11
)
(
x1
(
x2
x5
x12
)
(
x1
(
x2
x5
x13
)
(
x2
x5
x14
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x6
x8
)
(
x1
(
x2
x6
x9
)
(
x1
(
x2
x6
x10
)
(
x1
(
x2
x6
x11
)
(
x1
(
x2
x6
x12
)
(
x1
(
x2
x6
x13
)
(
x2
x6
x14
)
)
)
)
)
)
)
(
x1
(
x2
x7
x8
)
(
x1
(
x2
x7
x9
)
(
x1
(
x2
x7
x10
)
(
x1
(
x2
x7
x11
)
(
x1
(
x2
x7
x12
)
(
x1
(
x2
x7
x13
)
(
x2
x7
x14
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
a8c31..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x7
)
)
)
)
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
x15
)
)
)
)
)
)
)
=
x1
(
x1
(
x2
x3
x8
)
(
x1
(
x2
x3
x9
)
(
x1
(
x2
x3
x10
)
(
x1
(
x2
x3
x11
)
(
x1
(
x2
x3
x12
)
(
x1
(
x2
x3
x13
)
(
x1
(
x2
x3
x14
)
(
x2
x3
x15
)
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x4
x8
)
(
x1
(
x2
x4
x9
)
(
x1
(
x2
x4
x10
)
(
x1
(
x2
x4
x11
)
(
x1
(
x2
x4
x12
)
(
x1
(
x2
x4
x13
)
(
x1
(
x2
x4
x14
)
(
x2
x4
x15
)
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x5
x8
)
(
x1
(
x2
x5
x9
)
(
x1
(
x2
x5
x10
)
(
x1
(
x2
x5
x11
)
(
x1
(
x2
x5
x12
)
(
x1
(
x2
x5
x13
)
(
x1
(
x2
x5
x14
)
(
x2
x5
x15
)
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x6
x8
)
(
x1
(
x2
x6
x9
)
(
x1
(
x2
x6
x10
)
(
x1
(
x2
x6
x11
)
(
x1
(
x2
x6
x12
)
(
x1
(
x2
x6
x13
)
(
x1
(
x2
x6
x14
)
(
x2
x6
x15
)
)
)
)
)
)
)
)
(
x1
(
x2
x7
x8
)
(
x1
(
x2
x7
x9
)
(
x1
(
x2
x7
x10
)
(
x1
(
x2
x7
x11
)
(
x1
(
x2
x7
x12
)
(
x1
(
x2
x7
x13
)
(
x1
(
x2
x7
x14
)
(
x2
x7
x15
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
c240f..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
x8
)
)
)
)
)
(
x1
x9
x10
)
=
x1
(
x1
(
x2
x3
x9
)
(
x2
x3
x10
)
)
(
x1
(
x1
(
x2
x4
x9
)
(
x2
x4
x10
)
)
(
x1
(
x1
(
x2
x5
x9
)
(
x2
x5
x10
)
)
(
x1
(
x1
(
x2
x6
x9
)
(
x2
x6
x10
)
)
(
x1
(
x1
(
x2
x7
x9
)
(
x2
x7
x10
)
)
(
x1
(
x2
x8
x9
)
(
x2
x8
x10
)
)
)
)
)
)
(proof)
Theorem
ab0f3..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
x8
)
)
)
)
)
(
x1
x9
(
x1
x10
x11
)
)
=
x1
(
x1
(
x2
x3
x9
)
(
x1
(
x2
x3
x10
)
(
x2
x3
x11
)
)
)
(
x1
(
x1
(
x2
x4
x9
)
(
x1
(
x2
x4
x10
)
(
x2
x4
x11
)
)
)
(
x1
(
x1
(
x2
x5
x9
)
(
x1
(
x2
x5
x10
)
(
x2
x5
x11
)
)
)
(
x1
(
x1
(
x2
x6
x9
)
(
x1
(
x2
x6
x10
)
(
x2
x6
x11
)
)
)
(
x1
(
x1
(
x2
x7
x9
)
(
x1
(
x2
x7
x10
)
(
x2
x7
x11
)
)
)
(
x1
(
x2
x8
x9
)
(
x1
(
x2
x8
x10
)
(
x2
x8
x11
)
)
)
)
)
)
)
(proof)
Theorem
1b2e4..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
x8
)
)
)
)
)
(
x1
x9
(
x1
x10
(
x1
x11
x12
)
)
)
=
x1
(
x1
(
x2
x3
x9
)
(
x1
(
x2
x3
x10
)
(
x1
(
x2
x3
x11
)
(
x2
x3
x12
)
)
)
)
(
x1
(
x1
(
x2
x4
x9
)
(
x1
(
x2
x4
x10
)
(
x1
(
x2
x4
x11
)
(
x2
x4
x12
)
)
)
)
(
x1
(
x1
(
x2
x5
x9
)
(
x1
(
x2
x5
x10
)
(
x1
(
x2
x5
x11
)
(
x2
x5
x12
)
)
)
)
(
x1
(
x1
(
x2
x6
x9
)
(
x1
(
x2
x6
x10
)
(
x1
(
x2
x6
x11
)
(
x2
x6
x12
)
)
)
)
(
x1
(
x1
(
x2
x7
x9
)
(
x1
(
x2
x7
x10
)
(
x1
(
x2
x7
x11
)
(
x2
x7
x12
)
)
)
)
(
x1
(
x2
x8
x9
)
(
x1
(
x2
x8
x10
)
(
x1
(
x2
x8
x11
)
(
x2
x8
x12
)
)
)
)
)
)
)
)
(proof)
Theorem
afa83..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
x8
)
)
)
)
)
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
)
=
x1
(
x1
(
x2
x3
x9
)
(
x1
(
x2
x3
x10
)
(
x1
(
x2
x3
x11
)
(
x1
(
x2
x3
x12
)
(
x2
x3
x13
)
)
)
)
)
(
x1
(
x1
(
x2
x4
x9
)
(
x1
(
x2
x4
x10
)
(
x1
(
x2
x4
x11
)
(
x1
(
x2
x4
x12
)
(
x2
x4
x13
)
)
)
)
)
(
x1
(
x1
(
x2
x5
x9
)
(
x1
(
x2
x5
x10
)
(
x1
(
x2
x5
x11
)
(
x1
(
x2
x5
x12
)
(
x2
x5
x13
)
)
)
)
)
(
x1
(
x1
(
x2
x6
x9
)
(
x1
(
x2
x6
x10
)
(
x1
(
x2
x6
x11
)
(
x1
(
x2
x6
x12
)
(
x2
x6
x13
)
)
)
)
)
(
x1
(
x1
(
x2
x7
x9
)
(
x1
(
x2
x7
x10
)
(
x1
(
x2
x7
x11
)
(
x1
(
x2
x7
x12
)
(
x2
x7
x13
)
)
)
)
)
(
x1
(
x2
x8
x9
)
(
x1
(
x2
x8
x10
)
(
x1
(
x2
x8
x11
)
(
x1
(
x2
x8
x12
)
(
x2
x8
x13
)
)
)
)
)
)
)
)
)
(proof)
Theorem
30e88..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
x8
)
)
)
)
)
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
x14
)
)
)
)
)
=
x1
(
x1
(
x2
x3
x9
)
(
x1
(
x2
x3
x10
)
(
x1
(
x2
x3
x11
)
(
x1
(
x2
x3
x12
)
(
x1
(
x2
x3
x13
)
(
x2
x3
x14
)
)
)
)
)
)
(
x1
(
x1
(
x2
x4
x9
)
(
x1
(
x2
x4
x10
)
(
x1
(
x2
x4
x11
)
(
x1
(
x2
x4
x12
)
(
x1
(
x2
x4
x13
)
(
x2
x4
x14
)
)
)
)
)
)
(
x1
(
x1
(
x2
x5
x9
)
(
x1
(
x2
x5
x10
)
(
x1
(
x2
x5
x11
)
(
x1
(
x2
x5
x12
)
(
x1
(
x2
x5
x13
)
(
x2
x5
x14
)
)
)
)
)
)
(
x1
(
x1
(
x2
x6
x9
)
(
x1
(
x2
x6
x10
)
(
x1
(
x2
x6
x11
)
(
x1
(
x2
x6
x12
)
(
x1
(
x2
x6
x13
)
(
x2
x6
x14
)
)
)
)
)
)
(
x1
(
x1
(
x2
x7
x9
)
(
x1
(
x2
x7
x10
)
(
x1
(
x2
x7
x11
)
(
x1
(
x2
x7
x12
)
(
x1
(
x2
x7
x13
)
(
x2
x7
x14
)
)
)
)
)
)
(
x1
(
x2
x8
x9
)
(
x1
(
x2
x8
x10
)
(
x1
(
x2
x8
x11
)
(
x1
(
x2
x8
x12
)
(
x1
(
x2
x8
x13
)
(
x2
x8
x14
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
d7b62..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
x8
)
)
)
)
)
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
x15
)
)
)
)
)
)
=
x1
(
x1
(
x2
x3
x9
)
(
x1
(
x2
x3
x10
)
(
x1
(
x2
x3
x11
)
(
x1
(
x2
x3
x12
)
(
x1
(
x2
x3
x13
)
(
x1
(
x2
x3
x14
)
(
x2
x3
x15
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x4
x9
)
(
x1
(
x2
x4
x10
)
(
x1
(
x2
x4
x11
)
(
x1
(
x2
x4
x12
)
(
x1
(
x2
x4
x13
)
(
x1
(
x2
x4
x14
)
(
x2
x4
x15
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x5
x9
)
(
x1
(
x2
x5
x10
)
(
x1
(
x2
x5
x11
)
(
x1
(
x2
x5
x12
)
(
x1
(
x2
x5
x13
)
(
x1
(
x2
x5
x14
)
(
x2
x5
x15
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x6
x9
)
(
x1
(
x2
x6
x10
)
(
x1
(
x2
x6
x11
)
(
x1
(
x2
x6
x12
)
(
x1
(
x2
x6
x13
)
(
x1
(
x2
x6
x14
)
(
x2
x6
x15
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x7
x9
)
(
x1
(
x2
x7
x10
)
(
x1
(
x2
x7
x11
)
(
x1
(
x2
x7
x12
)
(
x1
(
x2
x7
x13
)
(
x1
(
x2
x7
x14
)
(
x2
x7
x15
)
)
)
)
)
)
)
(
x1
(
x2
x8
x9
)
(
x1
(
x2
x8
x10
)
(
x1
(
x2
x8
x11
)
(
x1
(
x2
x8
x12
)
(
x1
(
x2
x8
x13
)
(
x1
(
x2
x8
x14
)
(
x2
x8
x15
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
7be79..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
x8
)
)
)
)
)
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
x16
)
)
)
)
)
)
)
=
x1
(
x1
(
x2
x3
x9
)
(
x1
(
x2
x3
x10
)
(
x1
(
x2
x3
x11
)
(
x1
(
x2
x3
x12
)
(
x1
(
x2
x3
x13
)
(
x1
(
x2
x3
x14
)
(
x1
(
x2
x3
x15
)
(
x2
x3
x16
)
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x4
x9
)
(
x1
(
x2
x4
x10
)
(
x1
(
x2
x4
x11
)
(
x1
(
x2
x4
x12
)
(
x1
(
x2
x4
x13
)
(
x1
(
x2
x4
x14
)
(
x1
(
x2
x4
x15
)
(
x2
x4
x16
)
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x5
x9
)
(
x1
(
x2
x5
x10
)
(
x1
(
x2
x5
x11
)
(
x1
(
x2
x5
x12
)
(
x1
(
x2
x5
x13
)
(
x1
(
x2
x5
x14
)
(
x1
(
x2
x5
x15
)
(
x2
x5
x16
)
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x6
x9
)
(
x1
(
x2
x6
x10
)
(
x1
(
x2
x6
x11
)
(
x1
(
x2
x6
x12
)
(
x1
(
x2
x6
x13
)
(
x1
(
x2
x6
x14
)
(
x1
(
x2
x6
x15
)
(
x2
x6
x16
)
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x7
x9
)
(
x1
(
x2
x7
x10
)
(
x1
(
x2
x7
x11
)
(
x1
(
x2
x7
x12
)
(
x1
(
x2
x7
x13
)
(
x1
(
x2
x7
x14
)
(
x1
(
x2
x7
x15
)
(
x2
x7
x16
)
)
)
)
)
)
)
)
(
x1
(
x2
x8
x9
)
(
x1
(
x2
x8
x10
)
(
x1
(
x2
x8
x11
)
(
x1
(
x2
x8
x12
)
(
x1
(
x2
x8
x13
)
(
x1
(
x2
x8
x14
)
(
x1
(
x2
x8
x15
)
(
x2
x8
x16
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
e6d5e..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
x9
)
)
)
)
)
)
(
x1
x10
x11
)
=
x1
(
x1
(
x2
x3
x10
)
(
x2
x3
x11
)
)
(
x1
(
x1
(
x2
x4
x10
)
(
x2
x4
x11
)
)
(
x1
(
x1
(
x2
x5
x10
)
(
x2
x5
x11
)
)
(
x1
(
x1
(
x2
x6
x10
)
(
x2
x6
x11
)
)
(
x1
(
x1
(
x2
x7
x10
)
(
x2
x7
x11
)
)
(
x1
(
x1
(
x2
x8
x10
)
(
x2
x8
x11
)
)
(
x1
(
x2
x9
x10
)
(
x2
x9
x11
)
)
)
)
)
)
)
(proof)
Theorem
503ac..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
x9
)
)
)
)
)
)
(
x1
x10
(
x1
x11
x12
)
)
=
x1
(
x1
(
x2
x3
x10
)
(
x1
(
x2
x3
x11
)
(
x2
x3
x12
)
)
)
(
x1
(
x1
(
x2
x4
x10
)
(
x1
(
x2
x4
x11
)
(
x2
x4
x12
)
)
)
(
x1
(
x1
(
x2
x5
x10
)
(
x1
(
x2
x5
x11
)
(
x2
x5
x12
)
)
)
(
x1
(
x1
(
x2
x6
x10
)
(
x1
(
x2
x6
x11
)
(
x2
x6
x12
)
)
)
(
x1
(
x1
(
x2
x7
x10
)
(
x1
(
x2
x7
x11
)
(
x2
x7
x12
)
)
)
(
x1
(
x1
(
x2
x8
x10
)
(
x1
(
x2
x8
x11
)
(
x2
x8
x12
)
)
)
(
x1
(
x2
x9
x10
)
(
x1
(
x2
x9
x11
)
(
x2
x9
x12
)
)
)
)
)
)
)
)
(proof)
Theorem
f7ed5..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
x9
)
)
)
)
)
)
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
=
x1
(
x1
(
x2
x3
x10
)
(
x1
(
x2
x3
x11
)
(
x1
(
x2
x3
x12
)
(
x2
x3
x13
)
)
)
)
(
x1
(
x1
(
x2
x4
x10
)
(
x1
(
x2
x4
x11
)
(
x1
(
x2
x4
x12
)
(
x2
x4
x13
)
)
)
)
(
x1
(
x1
(
x2
x5
x10
)
(
x1
(
x2
x5
x11
)
(
x1
(
x2
x5
x12
)
(
x2
x5
x13
)
)
)
)
(
x1
(
x1
(
x2
x6
x10
)
(
x1
(
x2
x6
x11
)
(
x1
(
x2
x6
x12
)
(
x2
x6
x13
)
)
)
)
(
x1
(
x1
(
x2
x7
x10
)
(
x1
(
x2
x7
x11
)
(
x1
(
x2
x7
x12
)
(
x2
x7
x13
)
)
)
)
(
x1
(
x1
(
x2
x8
x10
)
(
x1
(
x2
x8
x11
)
(
x1
(
x2
x8
x12
)
(
x2
x8
x13
)
)
)
)
(
x1
(
x2
x9
x10
)
(
x1
(
x2
x9
x11
)
(
x1
(
x2
x9
x12
)
(
x2
x9
x13
)
)
)
)
)
)
)
)
)
(proof)
Theorem
641ca..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
x9
)
)
)
)
)
)
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
x14
)
)
)
)
=
x1
(
x1
(
x2
x3
x10
)
(
x1
(
x2
x3
x11
)
(
x1
(
x2
x3
x12
)
(
x1
(
x2
x3
x13
)
(
x2
x3
x14
)
)
)
)
)
(
x1
(
x1
(
x2
x4
x10
)
(
x1
(
x2
x4
x11
)
(
x1
(
x2
x4
x12
)
(
x1
(
x2
x4
x13
)
(
x2
x4
x14
)
)
)
)
)
(
x1
(
x1
(
x2
x5
x10
)
(
x1
(
x2
x5
x11
)
(
x1
(
x2
x5
x12
)
(
x1
(
x2
x5
x13
)
(
x2
x5
x14
)
)
)
)
)
(
x1
(
x1
(
x2
x6
x10
)
(
x1
(
x2
x6
x11
)
(
x1
(
x2
x6
x12
)
(
x1
(
x2
x6
x13
)
(
x2
x6
x14
)
)
)
)
)
(
x1
(
x1
(
x2
x7
x10
)
(
x1
(
x2
x7
x11
)
(
x1
(
x2
x7
x12
)
(
x1
(
x2
x7
x13
)
(
x2
x7
x14
)
)
)
)
)
(
x1
(
x1
(
x2
x8
x10
)
(
x1
(
x2
x8
x11
)
(
x1
(
x2
x8
x12
)
(
x1
(
x2
x8
x13
)
(
x2
x8
x14
)
)
)
)
)
(
x1
(
x2
x9
x10
)
(
x1
(
x2
x9
x11
)
(
x1
(
x2
x9
x12
)
(
x1
(
x2
x9
x13
)
(
x2
x9
x14
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
7a734..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
x9
)
)
)
)
)
)
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
x15
)
)
)
)
)
=
x1
(
x1
(
x2
x3
x10
)
(
x1
(
x2
x3
x11
)
(
x1
(
x2
x3
x12
)
(
x1
(
x2
x3
x13
)
(
x1
(
x2
x3
x14
)
(
x2
x3
x15
)
)
)
)
)
)
(
x1
(
x1
(
x2
x4
x10
)
(
x1
(
x2
x4
x11
)
(
x1
(
x2
x4
x12
)
(
x1
(
x2
x4
x13
)
(
x1
(
x2
x4
x14
)
(
x2
x4
x15
)
)
)
)
)
)
(
x1
(
x1
(
x2
x5
x10
)
(
x1
(
x2
x5
x11
)
(
x1
(
x2
x5
x12
)
(
x1
(
x2
x5
x13
)
(
x1
(
x2
x5
x14
)
(
x2
x5
x15
)
)
)
)
)
)
(
x1
(
x1
(
x2
x6
x10
)
(
x1
(
x2
x6
x11
)
(
x1
(
x2
x6
x12
)
(
x1
(
x2
x6
x13
)
(
x1
(
x2
x6
x14
)
(
x2
x6
x15
)
)
)
)
)
)
(
x1
(
x1
(
x2
x7
x10
)
(
x1
(
x2
x7
x11
)
(
x1
(
x2
x7
x12
)
(
x1
(
x2
x7
x13
)
(
x1
(
x2
x7
x14
)
(
x2
x7
x15
)
)
)
)
)
)
(
x1
(
x1
(
x2
x8
x10
)
(
x1
(
x2
x8
x11
)
(
x1
(
x2
x8
x12
)
(
x1
(
x2
x8
x13
)
(
x1
(
x2
x8
x14
)
(
x2
x8
x15
)
)
)
)
)
)
(
x1
(
x2
x9
x10
)
(
x1
(
x2
x9
x11
)
(
x1
(
x2
x9
x12
)
(
x1
(
x2
x9
x13
)
(
x1
(
x2
x9
x14
)
(
x2
x9
x15
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
45365..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
x9
)
)
)
)
)
)
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
x16
)
)
)
)
)
)
=
x1
(
x1
(
x2
x3
x10
)
(
x1
(
x2
x3
x11
)
(
x1
(
x2
x3
x12
)
(
x1
(
x2
x3
x13
)
(
x1
(
x2
x3
x14
)
(
x1
(
x2
x3
x15
)
(
x2
x3
x16
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x4
x10
)
(
x1
(
x2
x4
x11
)
(
x1
(
x2
x4
x12
)
(
x1
(
x2
x4
x13
)
(
x1
(
x2
x4
x14
)
(
x1
(
x2
x4
x15
)
(
x2
x4
x16
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x5
x10
)
(
x1
(
x2
x5
x11
)
(
x1
(
x2
x5
x12
)
(
x1
(
x2
x5
x13
)
(
x1
(
x2
x5
x14
)
(
x1
(
x2
x5
x15
)
(
x2
x5
x16
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x6
x10
)
(
x1
(
x2
x6
x11
)
(
x1
(
x2
x6
x12
)
(
x1
(
x2
x6
x13
)
(
x1
(
x2
x6
x14
)
(
x1
(
x2
x6
x15
)
(
x2
x6
x16
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x7
x10
)
(
x1
(
x2
x7
x11
)
(
x1
(
x2
x7
x12
)
(
x1
(
x2
x7
x13
)
(
x1
(
x2
x7
x14
)
(
x1
(
x2
x7
x15
)
(
x2
x7
x16
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x8
x10
)
(
x1
(
x2
x8
x11
)
(
x1
(
x2
x8
x12
)
(
x1
(
x2
x8
x13
)
(
x1
(
x2
x8
x14
)
(
x1
(
x2
x8
x15
)
(
x2
x8
x16
)
)
)
)
)
)
)
(
x1
(
x2
x9
x10
)
(
x1
(
x2
x9
x11
)
(
x1
(
x2
x9
x12
)
(
x1
(
x2
x9
x13
)
(
x1
(
x2
x9
x14
)
(
x1
(
x2
x9
x15
)
(
x2
x9
x16
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
de0dc..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
x9
)
)
)
)
)
)
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
x17
)
)
)
)
)
)
)
=
x1
(
x1
(
x2
x3
x10
)
(
x1
(
x2
x3
x11
)
(
x1
(
x2
x3
x12
)
(
x1
(
x2
x3
x13
)
(
x1
(
x2
x3
x14
)
(
x1
(
x2
x3
x15
)
(
x1
(
x2
x3
x16
)
(
x2
x3
x17
)
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x4
x10
)
(
x1
(
x2
x4
x11
)
(
x1
(
x2
x4
x12
)
(
x1
(
x2
x4
x13
)
(
x1
(
x2
x4
x14
)
(
x1
(
x2
x4
x15
)
(
x1
(
x2
x4
x16
)
(
x2
x4
x17
)
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x5
x10
)
(
x1
(
x2
x5
x11
)
(
x1
(
x2
x5
x12
)
(
x1
(
x2
x5
x13
)
(
x1
(
x2
x5
x14
)
(
x1
(
x2
x5
x15
)
(
x1
(
x2
x5
x16
)
(
x2
x5
x17
)
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x6
x10
)
(
x1
(
x2
x6
x11
)
(
x1
(
x2
x6
x12
)
(
x1
(
x2
x6
x13
)
(
x1
(
x2
x6
x14
)
(
x1
(
x2
x6
x15
)
(
x1
(
x2
x6
x16
)
(
x2
x6
x17
)
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x7
x10
)
(
x1
(
x2
x7
x11
)
(
x1
(
x2
x7
x12
)
(
x1
(
x2
x7
x13
)
(
x1
(
x2
x7
x14
)
(
x1
(
x2
x7
x15
)
(
x1
(
x2
x7
x16
)
(
x2
x7
x17
)
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x8
x10
)
(
x1
(
x2
x8
x11
)
(
x1
(
x2
x8
x12
)
(
x1
(
x2
x8
x13
)
(
x1
(
x2
x8
x14
)
(
x1
(
x2
x8
x15
)
(
x1
(
x2
x8
x16
)
(
x2
x8
x17
)
)
)
)
)
)
)
)
(
x1
(
x2
x9
x10
)
(
x1
(
x2
x9
x11
)
(
x1
(
x2
x9
x12
)
(
x1
(
x2
x9
x13
)
(
x1
(
x2
x9
x14
)
(
x1
(
x2
x9
x15
)
(
x1
(
x2
x9
x16
)
(
x2
x9
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
74594..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
x10
)
)
)
)
)
)
)
(
x1
x11
x12
)
=
x1
(
x1
(
x2
x3
x11
)
(
x2
x3
x12
)
)
(
x1
(
x1
(
x2
x4
x11
)
(
x2
x4
x12
)
)
(
x1
(
x1
(
x2
x5
x11
)
(
x2
x5
x12
)
)
(
x1
(
x1
(
x2
x6
x11
)
(
x2
x6
x12
)
)
(
x1
(
x1
(
x2
x7
x11
)
(
x2
x7
x12
)
)
(
x1
(
x1
(
x2
x8
x11
)
(
x2
x8
x12
)
)
(
x1
(
x1
(
x2
x9
x11
)
(
x2
x9
x12
)
)
(
x1
(
x2
x10
x11
)
(
x2
x10
x12
)
)
)
)
)
)
)
)
(proof)
Theorem
31403..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
x10
)
)
)
)
)
)
)
(
x1
x11
(
x1
x12
x13
)
)
=
x1
(
x1
(
x2
x3
x11
)
(
x1
(
x2
x3
x12
)
(
x2
x3
x13
)
)
)
(
x1
(
x1
(
x2
x4
x11
)
(
x1
(
x2
x4
x12
)
(
x2
x4
x13
)
)
)
(
x1
(
x1
(
x2
x5
x11
)
(
x1
(
x2
x5
x12
)
(
x2
x5
x13
)
)
)
(
x1
(
x1
(
x2
x6
x11
)
(
x1
(
x2
x6
x12
)
(
x2
x6
x13
)
)
)
(
x1
(
x1
(
x2
x7
x11
)
(
x1
(
x2
x7
x12
)
(
x2
x7
x13
)
)
)
(
x1
(
x1
(
x2
x8
x11
)
(
x1
(
x2
x8
x12
)
(
x2
x8
x13
)
)
)
(
x1
(
x1
(
x2
x9
x11
)
(
x1
(
x2
x9
x12
)
(
x2
x9
x13
)
)
)
(
x1
(
x2
x10
x11
)
(
x1
(
x2
x10
x12
)
(
x2
x10
x13
)
)
)
)
)
)
)
)
)
(proof)
Theorem
24a12..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
x10
)
)
)
)
)
)
)
(
x1
x11
(
x1
x12
(
x1
x13
x14
)
)
)
=
x1
(
x1
(
x2
x3
x11
)
(
x1
(
x2
x3
x12
)
(
x1
(
x2
x3
x13
)
(
x2
x3
x14
)
)
)
)
(
x1
(
x1
(
x2
x4
x11
)
(
x1
(
x2
x4
x12
)
(
x1
(
x2
x4
x13
)
(
x2
x4
x14
)
)
)
)
(
x1
(
x1
(
x2
x5
x11
)
(
x1
(
x2
x5
x12
)
(
x1
(
x2
x5
x13
)
(
x2
x5
x14
)
)
)
)
(
x1
(
x1
(
x2
x6
x11
)
(
x1
(
x2
x6
x12
)
(
x1
(
x2
x6
x13
)
(
x2
x6
x14
)
)
)
)
(
x1
(
x1
(
x2
x7
x11
)
(
x1
(
x2
x7
x12
)
(
x1
(
x2
x7
x13
)
(
x2
x7
x14
)
)
)
)
(
x1
(
x1
(
x2
x8
x11
)
(
x1
(
x2
x8
x12
)
(
x1
(
x2
x8
x13
)
(
x2
x8
x14
)
)
)
)
(
x1
(
x1
(
x2
x9
x11
)
(
x1
(
x2
x9
x12
)
(
x1
(
x2
x9
x13
)
(
x2
x9
x14
)
)
)
)
(
x1
(
x2
x10
x11
)
(
x1
(
x2
x10
x12
)
(
x1
(
x2
x10
x13
)
(
x2
x10
x14
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
ff328..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
x10
)
)
)
)
)
)
)
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
x15
)
)
)
)
=
x1
(
x1
(
x2
x3
x11
)
(
x1
(
x2
x3
x12
)
(
x1
(
x2
x3
x13
)
(
x1
(
x2
x3
x14
)
(
x2
x3
x15
)
)
)
)
)
(
x1
(
x1
(
x2
x4
x11
)
(
x1
(
x2
x4
x12
)
(
x1
(
x2
x4
x13
)
(
x1
(
x2
x4
x14
)
(
x2
x4
x15
)
)
)
)
)
(
x1
(
x1
(
x2
x5
x11
)
(
x1
(
x2
x5
x12
)
(
x1
(
x2
x5
x13
)
(
x1
(
x2
x5
x14
)
(
x2
x5
x15
)
)
)
)
)
(
x1
(
x1
(
x2
x6
x11
)
(
x1
(
x2
x6
x12
)
(
x1
(
x2
x6
x13
)
(
x1
(
x2
x6
x14
)
(
x2
x6
x15
)
)
)
)
)
(
x1
(
x1
(
x2
x7
x11
)
(
x1
(
x2
x7
x12
)
(
x1
(
x2
x7
x13
)
(
x1
(
x2
x7
x14
)
(
x2
x7
x15
)
)
)
)
)
(
x1
(
x1
(
x2
x8
x11
)
(
x1
(
x2
x8
x12
)
(
x1
(
x2
x8
x13
)
(
x1
(
x2
x8
x14
)
(
x2
x8
x15
)
)
)
)
)
(
x1
(
x1
(
x2
x9
x11
)
(
x1
(
x2
x9
x12
)
(
x1
(
x2
x9
x13
)
(
x1
(
x2
x9
x14
)
(
x2
x9
x15
)
)
)
)
)
(
x1
(
x2
x10
x11
)
(
x1
(
x2
x10
x12
)
(
x1
(
x2
x10
x13
)
(
x1
(
x2
x10
x14
)
(
x2
x10
x15
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
075c5..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
x10
)
)
)
)
)
)
)
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
x16
)
)
)
)
)
=
x1
(
x1
(
x2
x3
x11
)
(
x1
(
x2
x3
x12
)
(
x1
(
x2
x3
x13
)
(
x1
(
x2
x3
x14
)
(
x1
(
x2
x3
x15
)
(
x2
x3
x16
)
)
)
)
)
)
(
x1
(
x1
(
x2
x4
x11
)
(
x1
(
x2
x4
x12
)
(
x1
(
x2
x4
x13
)
(
x1
(
x2
x4
x14
)
(
x1
(
x2
x4
x15
)
(
x2
x4
x16
)
)
)
)
)
)
(
x1
(
x1
(
x2
x5
x11
)
(
x1
(
x2
x5
x12
)
(
x1
(
x2
x5
x13
)
(
x1
(
x2
x5
x14
)
(
x1
(
x2
x5
x15
)
(
x2
x5
x16
)
)
)
)
)
)
(
x1
(
x1
(
x2
x6
x11
)
(
x1
(
x2
x6
x12
)
(
x1
(
x2
x6
x13
)
(
x1
(
x2
x6
x14
)
(
x1
(
x2
x6
x15
)
(
x2
x6
x16
)
)
)
)
)
)
(
x1
(
x1
(
x2
x7
x11
)
(
x1
(
x2
x7
x12
)
(
x1
(
x2
x7
x13
)
(
x1
(
x2
x7
x14
)
(
x1
(
x2
x7
x15
)
(
x2
x7
x16
)
)
)
)
)
)
(
x1
(
x1
(
x2
x8
x11
)
(
x1
(
x2
x8
x12
)
(
x1
(
x2
x8
x13
)
(
x1
(
x2
x8
x14
)
(
x1
(
x2
x8
x15
)
(
x2
x8
x16
)
)
)
)
)
)
(
x1
(
x1
(
x2
x9
x11
)
(
x1
(
x2
x9
x12
)
(
x1
(
x2
x9
x13
)
(
x1
(
x2
x9
x14
)
(
x1
(
x2
x9
x15
)
(
x2
x9
x16
)
)
)
)
)
)
(
x1
(
x2
x10
x11
)
(
x1
(
x2
x10
x12
)
(
x1
(
x2
x10
x13
)
(
x1
(
x2
x10
x14
)
(
x1
(
x2
x10
x15
)
(
x2
x10
x16
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
5a91e..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
x10
)
)
)
)
)
)
)
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
x17
)
)
)
)
)
)
=
x1
(
x1
(
x2
x3
x11
)
(
x1
(
x2
x3
x12
)
(
x1
(
x2
x3
x13
)
(
x1
(
x2
x3
x14
)
(
x1
(
x2
x3
x15
)
(
x1
(
x2
x3
x16
)
(
x2
x3
x17
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x4
x11
)
(
x1
(
x2
x4
x12
)
(
x1
(
x2
x4
x13
)
(
x1
(
x2
x4
x14
)
(
x1
(
x2
x4
x15
)
(
x1
(
x2
x4
x16
)
(
x2
x4
x17
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x5
x11
)
(
x1
(
x2
x5
x12
)
(
x1
(
x2
x5
x13
)
(
x1
(
x2
x5
x14
)
(
x1
(
x2
x5
x15
)
(
x1
(
x2
x5
x16
)
(
x2
x5
x17
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x6
x11
)
(
x1
(
x2
x6
x12
)
(
x1
(
x2
x6
x13
)
(
x1
(
x2
x6
x14
)
(
x1
(
x2
x6
x15
)
(
x1
(
x2
x6
x16
)
(
x2
x6
x17
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x7
x11
)
(
x1
(
x2
x7
x12
)
(
x1
(
x2
x7
x13
)
(
x1
(
x2
x7
x14
)
(
x1
(
x2
x7
x15
)
(
x1
(
x2
x7
x16
)
(
x2
x7
x17
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x8
x11
)
(
x1
(
x2
x8
x12
)
(
x1
(
x2
x8
x13
)
(
x1
(
x2
x8
x14
)
(
x1
(
x2
x8
x15
)
(
x1
(
x2
x8
x16
)
(
x2
x8
x17
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x9
x11
)
(
x1
(
x2
x9
x12
)
(
x1
(
x2
x9
x13
)
(
x1
(
x2
x9
x14
)
(
x1
(
x2
x9
x15
)
(
x1
(
x2
x9
x16
)
(
x2
x9
x17
)
)
)
)
)
)
)
(
x1
(
x2
x10
x11
)
(
x1
(
x2
x10
x12
)
(
x1
(
x2
x10
x13
)
(
x1
(
x2
x10
x14
)
(
x1
(
x2
x10
x15
)
(
x1
(
x2
x10
x16
)
(
x2
x10
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
43f21..
:
∀ x0 :
ι → ο
.
∀ x1 x2 :
ι →
ι → ι
.
(
∀ x3 x4 .
x0
x3
⟶
x0
x4
⟶
x0
(
x1
x3
x4
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
x3
(
x1
x4
x5
)
=
x1
(
x2
x3
x4
)
(
x2
x3
x5
)
)
⟶
(
∀ x3 x4 x5 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x2
(
x1
x3
x4
)
x5
=
x1
(
x2
x3
x5
)
(
x2
x4
x5
)
)
⟶
∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x0
x18
⟶
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
x10
)
)
)
)
)
)
)
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
x18
)
)
)
)
)
)
)
=
x1
(
x1
(
x2
x3
x11
)
(
x1
(
x2
x3
x12
)
(
x1
(
x2
x3
x13
)
(
x1
(
x2
x3
x14
)
(
x1
(
x2
x3
x15
)
(
x1
(
x2
x3
x16
)
(
x1
(
x2
x3
x17
)
(
x2
x3
x18
)
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x4
x11
)
(
x1
(
x2
x4
x12
)
(
x1
(
x2
x4
x13
)
(
x1
(
x2
x4
x14
)
(
x1
(
x2
x4
x15
)
(
x1
(
x2
x4
x16
)
(
x1
(
x2
x4
x17
)
(
x2
x4
x18
)
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x5
x11
)
(
x1
(
x2
x5
x12
)
(
x1
(
x2
x5
x13
)
(
x1
(
x2
x5
x14
)
(
x1
(
x2
x5
x15
)
(
x1
(
x2
x5
x16
)
(
x1
(
x2
x5
x17
)
(
x2
x5
x18
)
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x6
x11
)
(
x1
(
x2
x6
x12
)
(
x1
(
x2
x6
x13
)
(
x1
(
x2
x6
x14
)
(
x1
(
x2
x6
x15
)
(
x1
(
x2
x6
x16
)
(
x1
(
x2
x6
x17
)
(
x2
x6
x18
)
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x7
x11
)
(
x1
(
x2
x7
x12
)
(
x1
(
x2
x7
x13
)
(
x1
(
x2
x7
x14
)
(
x1
(
x2
x7
x15
)
(
x1
(
x2
x7
x16
)
(
x1
(
x2
x7
x17
)
(
x2
x7
x18
)
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x8
x11
)
(
x1
(
x2
x8
x12
)
(
x1
(
x2
x8
x13
)
(
x1
(
x2
x8
x14
)
(
x1
(
x2
x8
x15
)
(
x1
(
x2
x8
x16
)
(
x1
(
x2
x8
x17
)
(
x2
x8
x18
)
)
)
)
)
)
)
)
(
x1
(
x1
(
x2
x9
x11
)
(
x1
(
x2
x9
x12
)
(
x1
(
x2
x9
x13
)
(
x1
(
x2
x9
x14
)
(
x1
(
x2
x9
x15
)
(
x1
(
x2
x9
x16
)
(
x1
(
x2
x9
x17
)
(
x2
x9
x18
)
)
)
)
)
)
)
)
(
x1
(
x2
x10
x11
)
(
x1
(
x2
x10
x12
)
(
x1
(
x2
x10
x13
)
(
x1
(
x2
x10
x14
)
(
x1
(
x2
x10
x15
)
(
x1
(
x2
x10
x16
)
(
x1
(
x2
x10
x17
)
(
x2
x10
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)