Search for blocks/addresses/...
Proofgold Asset
asset id
03523b553b52adc8c24d954a6ff5491d389601a3519a0d3ecb9d5b20fe6626e6
asset hash
104785e124ba7b15637330b7c19645410516a1a1fc39200ad14a90c5b4e59a21
bday / block
24469
tx
00508..
preasset
doc published by
Pr5Zc..
Theorem
45f87..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x1
x2
(
x1
x3
(
x1
x4
x5
)
)
=
x1
x3
(
x1
x4
(
x1
x2
x5
)
)
(proof)
Theorem
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
)
)
)
(proof)
Theorem
75b00..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x7
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x2
x7
)
)
)
)
(proof)
Theorem
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
)
)
)
)
)
(proof)
Theorem
cbdc2..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
x9
)
)
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x2
x9
)
)
)
)
)
)
(proof)
Theorem
d3eb2..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
x10
)
)
)
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x2
x10
)
)
)
)
)
)
)
(proof)
Theorem
2a73e..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
x11
)
)
)
)
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x2
x11
)
)
)
)
)
)
)
)
(proof)
Theorem
4c672..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
x12
)
)
)
)
)
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x2
x12
)
)
)
)
)
)
)
)
)
(proof)
Theorem
000b3..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
)
)
)
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x2
x13
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
495ba..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
x14
)
)
)
)
)
)
)
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x2
x14
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
a1ee1..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
x15
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x2
x15
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
0c618..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x2
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
92560..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x2
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
30837..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x0
x18
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
(
x1
x2
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
0d20b..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x6
)
)
)
=
x1
x4
(
x1
x5
(
x1
x2
(
x1
x3
x6
)
)
)
(proof)
Theorem
f87dc..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x7
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x2
(
x1
x3
x7
)
)
)
)
(proof)
Theorem
3a13f..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
x8
)
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x2
(
x1
x3
x8
)
)
)
)
)
(proof)
Theorem
209c8..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
x8
)
)
)
)
)
=
x1
x5
(
x1
x6
(
x1
x7
(
x1
x2
(
x1
x3
(
x1
x4
x8
)
)
)
)
)
(proof)
Theorem
df7cd..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
x9
)
)
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x2
(
x1
x3
x9
)
)
)
)
)
)
(proof)
Theorem
9fbf6..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
x9
)
)
)
)
)
)
=
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x2
(
x1
x3
(
x1
x4
x9
)
)
)
)
)
)
(proof)
Theorem
9ba1d..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
x10
)
)
)
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x2
(
x1
x3
x10
)
)
)
)
)
)
)
(proof)
Theorem
d3b5b..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
x10
)
)
)
)
)
)
)
=
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x2
(
x1
x3
(
x1
x4
x10
)
)
)
)
)
)
)
(proof)
Theorem
d63ce..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
x10
)
)
)
)
)
)
)
=
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x10
)
)
)
)
)
)
)
(proof)
Theorem
696da..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
x11
)
)
)
)
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x2
(
x1
x3
x11
)
)
)
)
)
)
)
)
(proof)
Theorem
387d2..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
x11
)
)
)
)
)
)
)
)
=
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x2
(
x1
x3
(
x1
x4
x11
)
)
)
)
)
)
)
)
(proof)
Theorem
17b5e..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
x11
)
)
)
)
)
)
)
)
=
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x11
)
)
)
)
)
)
)
)
(proof)
Theorem
0d9d2..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
x12
)
)
)
)
)
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x2
(
x1
x3
x12
)
)
)
)
)
)
)
)
)
(proof)
Theorem
30284..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
x12
)
)
)
)
)
)
)
)
)
=
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x2
(
x1
x3
(
x1
x4
x12
)
)
)
)
)
)
)
)
)
(proof)
Theorem
5a706..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
x12
)
)
)
)
)
)
)
)
)
=
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x12
)
)
)
)
)
)
)
)
)
(proof)
Theorem
a8fd7..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
x12
)
)
)
)
)
)
)
)
)
=
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x12
)
)
)
)
)
)
)
)
)
(proof)
Theorem
6f341..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
)
)
)
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x2
(
x1
x3
x13
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
fb74d..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
)
)
)
)
)
)
)
=
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x2
(
x1
x3
(
x1
x4
x13
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
72568..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
)
)
)
)
)
)
)
=
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x13
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
9bb69..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
)
)
)
)
)
)
)
=
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x13
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
8e1b0..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
x14
)
)
)
)
)
)
)
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x2
(
x1
x3
x14
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
521cb..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
x14
)
)
)
)
)
)
)
)
)
)
)
=
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x2
(
x1
x3
(
x1
x4
x14
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
9b328..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
x14
)
)
)
)
)
)
)
)
)
)
)
=
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x14
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
09a8d..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
x14
)
)
)
)
)
)
)
)
)
)
)
=
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x14
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
b4182..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
x14
)
)
)
)
)
)
)
)
)
)
)
=
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
x14
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
f1d76..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
x15
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x2
(
x1
x3
x15
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
005bf..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
x15
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x2
(
x1
x3
(
x1
x4
x15
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
15bb0..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
x15
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x15
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
25f70..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
x15
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x15
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
47a47..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
x15
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
x15
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
92fce..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x2
(
x1
x3
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
f7ca7..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x2
(
x1
x3
(
x1
x4
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
65a4d..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
8a1ac..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
14bac..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
56712..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
d4a91..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x2
(
x1
x3
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
cdec3..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x2
(
x1
x3
(
x1
x4
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
55afc..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
78083..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
82de4..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
e6374..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
ad9b7..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x0
x18
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
(
x1
x2
(
x1
x3
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
366f2..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x0
x18
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
(
x1
x2
(
x1
x3
(
x1
x4
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
7b7b5..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x0
x18
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
2fa40..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x0
x18
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
11aa7..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x0
x18
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
58df9..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x0
x18
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
80a23..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
x0
x7
⟶
x0
x8
⟶
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x0
x13
⟶
x0
x14
⟶
x0
x15
⟶
x0
x16
⟶
x0
x17
⟶
x0
x18
⟶
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
(
x1
x17
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
8c2ea..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
x2
(
x1
x3
x4
)
=
x1
x3
(
x1
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x1
x2
(
x1
x3
(
x1
x4
x5
)
)
=
x1
x4
(
x1
x3
(
x1
x2
x5
)
)
(proof)