Search for blocks/addresses/...
Proofgold Asset
asset id
00d40abe9d6b41f409690e110a318f0045f0504be2720c10a145c0185854354d
asset hash
b1241a7b1dbd87eb9a443dbdb2a6a21b51bf6208494310f7b5b804cd350c18e5
bday / block
24253
tx
c2f26..
preasset
doc published by
Pr5Zc..
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
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
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
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
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
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
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
20d59..
:
∀ 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 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
⟶
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
(
x1
x16
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
98924..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
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
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
x14
)
)
)
)
)
)
)
)
)
)
)
Theorem
6c527..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
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
)
)
)
)
)
)
)
)
)
)
)
)
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
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
ce587..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
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
)
)
)
)
)
)
)
)
)
)
)
)
)
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
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
58626..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
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
)
)
)
)
)
)
)
)
)
)
)
)
)
)
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
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
5e801..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
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
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
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
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
6d3cf..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
x3
)
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
x11
)
)
)
)
)
)
)
=
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
x11
)
)
)
)
)
)
)
)
Theorem
b1a4d..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
x3
)
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
x12
)
)
)
)
)
)
)
)
=
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
x12
)
)
)
)
)
)
)
)
)
(proof)
Theorem
d42d0..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
x3
)
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
)
)
)
)
)
)
=
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
1de7f..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
x3
)
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
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
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
8c174..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
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
(
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
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
07c5e..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
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
(
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
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
f6743..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
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
(
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
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
d3054..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
(
x1
x3
x4
)
)
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
x12
)
)
)
)
)
)
)
=
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
x12
)
)
)
)
)
)
)
)
)
Theorem
51365..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
(
x1
x3
x4
)
)
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
)
)
)
)
)
=
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
cdcaf..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
(
x1
x3
x4
)
)
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
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
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
2dce9..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
(
x1
x3
x4
)
)
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
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
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
216d3..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
(
x1
x3
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
(
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
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
7ff40..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
(
x1
x3
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
(
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
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
443d0..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
(
x1
x3
(
x1
x4
x5
)
)
)
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
)
)
)
)
=
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
)
)
)
)
)
)
)
Theorem
bd67e..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
(
x1
x3
(
x1
x4
x5
)
)
)
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
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
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
31d91..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
(
x1
x3
(
x1
x4
x5
)
)
)
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
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
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
c3115..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
(
x1
x3
(
x1
x4
x5
)
)
)
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
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
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
91b03..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
(
x1
x3
(
x1
x4
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
(
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
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
65945..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x6
)
)
)
)
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
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
)
)
)
)
)
)
)
)
)
)
)
Theorem
f3234..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x6
)
)
)
)
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
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
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
c5f8f..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x6
)
)
)
)
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
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
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
09f1f..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
x6
)
)
)
)
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
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
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
3e472..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
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
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
03232..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x7
)
)
)
)
)
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
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
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
99928..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
x7
)
)
)
)
)
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
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
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
e06ed..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
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
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
6b05b..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
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
(
x1
x16
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
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Known
a871b..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
x9
)
)
)
)
)
)
)
(
x1
x10
x11
)
=
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
x11
)
)
)
)
)
)
)
)
Known
3e03a..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
x4
)
)
⟶
∀ x2 x3 x4 x5 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x1
(
x1
x2
x3
)
(
x1
x4
x5
)
=
x1
x2
(
x1
x3
(
x1
x4
x5
)
)
Theorem
693ec..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
x10
)
)
)
)
)
)
)
)
(
x1
x11
x12
)
=
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
x12
)
)
)
)
)
)
)
)
)
(proof)
Theorem
02361..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
x10
)
)
)
)
)
)
)
)
(
x1
x11
(
x1
x12
x13
)
)
=
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
cbdd8..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
x10
)
)
)
)
)
)
)
)
(
x1
x11
(
x1
x12
(
x1
x13
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
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
d2cdc..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
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
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
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
fbfe3..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
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
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
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
00001..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
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
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
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
f3ec9..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
x11
)
)
)
)
)
)
)
)
)
(
x1
x12
x13
)
=
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
2e619..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
x11
)
)
)
)
)
)
)
)
)
(
x1
x12
(
x1
x13
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
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
841f4..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
x11
)
)
)
)
)
)
)
)
)
(
x1
x12
(
x1
x13
(
x1
x14
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
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
b3115..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
x11
)
)
)
)
)
)
)
)
)
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
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
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
e54de..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
x11
)
)
)
)
)
)
)
)
)
(
x1
x12
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
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
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
cd854..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
x12
)
)
)
)
)
)
)
)
)
)
(
x1
x13
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
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
84b1f..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
x12
)
)
)
)
)
)
)
)
)
)
(
x1
x13
(
x1
x14
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
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
4b6df..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
x12
)
)
)
)
)
)
)
)
)
)
(
x1
x13
(
x1
x14
(
x1
x15
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
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
11a48..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
x12
)
)
)
)
)
)
)
)
)
)
(
x1
x13
(
x1
x14
(
x1
x15
(
x1
x16
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
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
8c836..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
)
)
)
)
)
)
)
)
(
x1
x14
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
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
17484..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
)
)
)
)
)
)
)
)
(
x1
x14
(
x1
x15
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
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
5b69c..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
x1
x2
(
x1
x3
(
x1
x4
(
x1
x5
(
x1
x6
(
x1
x7
(
x1
x8
(
x1
x9
(
x1
x10
(
x1
x11
(
x1
x12
x13
)
)
)
)
)
)
)
)
)
)
)
(
x1
x14
(
x1
x15
(
x1
x16
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
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
2052e..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
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
x15
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
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
73cc8..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
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
x15
(
x1
x16
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
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
9a64e..
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ι
.
(
∀ x2 x3 .
x0
x2
⟶
x0
x3
⟶
x0
(
x1
x2
x3
)
)
⟶
(
∀ x2 x3 x4 .
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x1
(
x1
x2
x3
)
x4
=
x1
x2
(
x1
x3
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
(
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
x16
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
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)