Search for blocks/addresses/...
Proofgold Asset
asset id
2d9c3ddbb1c43ff4fb6b041a8c4afe61971b1ca49cef857cedf75a0d51a2bb37
asset hash
f3c864e26199e3200bf46441d14e5a6a116aae0bf847f94c844d5f130f51767e
bday / block
24253
tx
e6996..
preasset
doc published by
Pr5Zc..
Theorem
0c348..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
∀ x2 x3 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
∀ x4 .
x0
x4
⟶
x0
(
x3
(
x2
x4
)
)
(proof)
Theorem
b56a1..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
∀ x2 x3 x4 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
x1
x4
⟶
∀ x5 .
x0
x5
⟶
x0
(
x4
(
x3
(
x2
x5
)
)
)
(proof)
Theorem
7d951..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
∀ x2 x3 x4 x5 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
x1
x4
⟶
x1
x5
⟶
∀ x6 .
x0
x6
⟶
x0
(
x5
(
x4
(
x3
(
x2
x6
)
)
)
)
(proof)
Theorem
31050..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
∀ x2 x3 x4 x5 x6 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
x1
x4
⟶
x1
x5
⟶
x1
x6
⟶
∀ x7 .
x0
x7
⟶
x0
(
x6
(
x5
(
x4
(
x3
(
x2
x7
)
)
)
)
)
(proof)
Theorem
2948f..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
x1
x4
⟶
x1
x5
⟶
x1
x6
⟶
x1
x7
⟶
∀ x8 .
x0
x8
⟶
x0
(
x7
(
x6
(
x5
(
x4
(
x3
(
x2
x8
)
)
)
)
)
)
(proof)
Theorem
10d52..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
x1
x4
⟶
x1
x5
⟶
x1
x6
⟶
x1
x7
⟶
x1
x8
⟶
∀ x9 .
x0
x9
⟶
x0
(
x8
(
x7
(
x6
(
x5
(
x4
(
x3
(
x2
x9
)
)
)
)
)
)
)
(proof)
Theorem
b99b8..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
x1
x4
⟶
x1
x5
⟶
x1
x6
⟶
x1
x7
⟶
x1
x8
⟶
x1
x9
⟶
∀ x10 .
x0
x10
⟶
x0
(
x9
(
x8
(
x7
(
x6
(
x5
(
x4
(
x3
(
x2
x10
)
)
)
)
)
)
)
)
(proof)
Theorem
0e17d..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
x1
x4
⟶
x1
x5
⟶
x1
x6
⟶
x1
x7
⟶
x1
x8
⟶
x1
x9
⟶
x1
x10
⟶
∀ x11 .
x0
x11
⟶
x0
(
x10
(
x9
(
x8
(
x7
(
x6
(
x5
(
x4
(
x3
(
x2
x11
)
)
)
)
)
)
)
)
)
(proof)
Theorem
f2d8f..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
x1
x4
⟶
x1
x5
⟶
x1
x6
⟶
x1
x7
⟶
x1
x8
⟶
x1
x9
⟶
x1
x10
⟶
x1
x11
⟶
∀ x12 .
x0
x12
⟶
x0
(
x11
(
x10
(
x9
(
x8
(
x7
(
x6
(
x5
(
x4
(
x3
(
x2
x12
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
554db..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
x1
x4
⟶
x1
x5
⟶
x1
x6
⟶
x1
x7
⟶
x1
x8
⟶
x1
x9
⟶
x1
x10
⟶
x1
x11
⟶
x1
x12
⟶
∀ x13 .
x0
x13
⟶
x0
(
x12
(
x11
(
x10
(
x9
(
x8
(
x7
(
x6
(
x5
(
x4
(
x3
(
x2
x13
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
69433..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 :
ι → ι
.
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 .
x0
x14
⟶
x0
(
x13
(
x12
(
x11
(
x10
(
x9
(
x8
(
x7
(
x6
(
x5
(
x4
(
x3
(
x2
x14
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
ef9bb..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 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
⟶
x1
x14
⟶
∀ x15 .
x0
x15
⟶
x0
(
x14
(
x13
(
x12
(
x11
(
x10
(
x9
(
x8
(
x7
(
x6
(
x5
(
x4
(
x3
(
x2
x15
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
573cc..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 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
⟶
x1
x15
⟶
∀ x16 .
x0
x16
⟶
x0
(
x15
(
x14
(
x13
(
x12
(
x11
(
x10
(
x9
(
x8
(
x7
(
x6
(
x5
(
x4
(
x3
(
x2
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
92d58..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 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
⟶
x1
x16
⟶
∀ x17 .
x0
x17
⟶
x0
(
x16
(
x15
(
x14
(
x13
(
x12
(
x11
(
x10
(
x9
(
x8
(
x7
(
x6
(
x5
(
x4
(
x3
(
x2
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
b4c6e..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 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
⟶
x1
x17
⟶
∀ x18 .
x0
x18
⟶
x0
(
x17
(
x16
(
x15
(
x14
(
x13
(
x12
(
x11
(
x10
(
x9
(
x8
(
x7
(
x6
(
x5
(
x4
(
x3
(
x2
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
45c54..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
(
∀ x2 x3 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
∀ x4 .
x0
x4
⟶
x2
(
x3
x4
)
=
x3
(
x2
x4
)
)
⟶
∀ x2 x3 x4 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
x1
x4
⟶
∀ x5 .
x0
x5
⟶
x2
(
x3
(
x4
x5
)
)
=
x3
(
x2
(
x4
x5
)
)
(proof)
Theorem
a1479..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
(
∀ x2 x3 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
∀ x4 .
x0
x4
⟶
x2
(
x3
x4
)
=
x3
(
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
x1
x4
⟶
x1
x5
⟶
∀ x6 .
x0
x6
⟶
x2
(
x3
(
x4
(
x5
x6
)
)
)
=
x3
(
x2
(
x4
(
x5
x6
)
)
)
(proof)
Theorem
36187..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
(
∀ x2 x3 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
∀ x4 .
x0
x4
⟶
x2
(
x3
x4
)
=
x3
(
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
x1
x4
⟶
x1
x5
⟶
x1
x6
⟶
∀ x7 .
x0
x7
⟶
x2
(
x3
(
x4
(
x5
(
x6
x7
)
)
)
)
=
x3
(
x2
(
x4
(
x5
(
x6
x7
)
)
)
)
(proof)
Theorem
114a2..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
(
∀ x2 x3 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
∀ x4 .
x0
x4
⟶
x2
(
x3
x4
)
=
x3
(
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
x1
x4
⟶
x1
x5
⟶
x1
x6
⟶
x1
x7
⟶
∀ x8 .
x0
x8
⟶
x2
(
x3
(
x4
(
x5
(
x6
(
x7
x8
)
)
)
)
)
=
x3
(
x2
(
x4
(
x5
(
x6
(
x7
x8
)
)
)
)
)
(proof)
Theorem
843a6..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
(
∀ x2 x3 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
∀ x4 .
x0
x4
⟶
x2
(
x3
x4
)
=
x3
(
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
x1
x4
⟶
x1
x5
⟶
x1
x6
⟶
x1
x7
⟶
x1
x8
⟶
∀ x9 .
x0
x9
⟶
x2
(
x3
(
x4
(
x5
(
x6
(
x7
(
x8
x9
)
)
)
)
)
)
=
x3
(
x2
(
x4
(
x5
(
x6
(
x7
(
x8
x9
)
)
)
)
)
)
(proof)
Theorem
8811b..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
(
∀ x2 x3 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
∀ x4 .
x0
x4
⟶
x2
(
x3
x4
)
=
x3
(
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
x1
x4
⟶
x1
x5
⟶
x1
x6
⟶
x1
x7
⟶
x1
x8
⟶
x1
x9
⟶
∀ x10 .
x0
x10
⟶
x2
(
x3
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
x10
)
)
)
)
)
)
)
=
x3
(
x2
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
x10
)
)
)
)
)
)
)
(proof)
Theorem
6deab..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
(
∀ x2 x3 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
∀ x4 .
x0
x4
⟶
x2
(
x3
x4
)
=
x3
(
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
x1
x4
⟶
x1
x5
⟶
x1
x6
⟶
x1
x7
⟶
x1
x8
⟶
x1
x9
⟶
x1
x10
⟶
∀ x11 .
x0
x11
⟶
x2
(
x3
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
(
x10
x11
)
)
)
)
)
)
)
)
=
x3
(
x2
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
(
x10
x11
)
)
)
)
)
)
)
)
(proof)
Theorem
4723f..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
(
∀ x2 x3 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
∀ x4 .
x0
x4
⟶
x2
(
x3
x4
)
=
x3
(
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
x1
x4
⟶
x1
x5
⟶
x1
x6
⟶
x1
x7
⟶
x1
x8
⟶
x1
x9
⟶
x1
x10
⟶
x1
x11
⟶
∀ x12 .
x0
x12
⟶
x2
(
x3
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
(
x10
(
x11
x12
)
)
)
)
)
)
)
)
)
=
x3
(
x2
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
(
x10
(
x11
x12
)
)
)
)
)
)
)
)
)
(proof)
Theorem
b6264..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
(
∀ x2 x3 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
∀ x4 .
x0
x4
⟶
x2
(
x3
x4
)
=
x3
(
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
x1
x4
⟶
x1
x5
⟶
x1
x6
⟶
x1
x7
⟶
x1
x8
⟶
x1
x9
⟶
x1
x10
⟶
x1
x11
⟶
x1
x12
⟶
∀ x13 .
x0
x13
⟶
x2
(
x3
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
(
x10
(
x11
(
x12
x13
)
)
)
)
)
)
)
)
)
)
=
x3
(
x2
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
(
x10
(
x11
(
x12
x13
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
f7a78..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
(
∀ x2 x3 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
∀ x4 .
x0
x4
⟶
x2
(
x3
x4
)
=
x3
(
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 :
ι → ι
.
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 .
x0
x14
⟶
x2
(
x3
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
(
x10
(
x11
(
x12
(
x13
x14
)
)
)
)
)
)
)
)
)
)
)
=
x3
(
x2
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
(
x10
(
x11
(
x12
(
x13
x14
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
596bd..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
(
∀ x2 x3 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
∀ x4 .
x0
x4
⟶
x2
(
x3
x4
)
=
x3
(
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 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
⟶
x1
x14
⟶
∀ x15 .
x0
x15
⟶
x2
(
x3
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
(
x10
(
x11
(
x12
(
x13
(
x14
x15
)
)
)
)
)
)
)
)
)
)
)
)
=
x3
(
x2
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
(
x10
(
x11
(
x12
(
x13
(
x14
x15
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
da964..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
(
∀ x2 x3 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
∀ x4 .
x0
x4
⟶
x2
(
x3
x4
)
=
x3
(
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 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
⟶
x1
x15
⟶
∀ x16 .
x0
x16
⟶
x2
(
x3
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
(
x10
(
x11
(
x12
(
x13
(
x14
(
x15
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x3
(
x2
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
(
x10
(
x11
(
x12
(
x13
(
x14
(
x15
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
3b9d7..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
(
∀ x2 x3 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
∀ x4 .
x0
x4
⟶
x2
(
x3
x4
)
=
x3
(
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 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
⟶
x1
x16
⟶
∀ x17 .
x0
x17
⟶
x2
(
x3
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
(
x10
(
x11
(
x12
(
x13
(
x14
(
x15
(
x16
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x3
(
x2
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
(
x10
(
x11
(
x12
(
x13
(
x14
(
x15
(
x16
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
2e61c..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
(
∀ x2 x3 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
∀ x4 .
x0
x4
⟶
x2
(
x3
x4
)
=
x3
(
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 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
⟶
x1
x17
⟶
∀ x18 .
x0
x18
⟶
x2
(
x3
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
(
x10
(
x11
(
x12
(
x13
(
x14
(
x15
(
x16
(
x17
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x3
(
x2
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
(
x10
(
x11
(
x12
(
x13
(
x14
(
x15
(
x16
(
x17
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
16021..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
(
∀ x2 x3 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
∀ x4 .
x0
x4
⟶
x2
(
x3
x4
)
=
x3
(
x2
x4
)
)
⟶
∀ x2 x3 x4 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
x1
x4
⟶
∀ x5 .
x0
x5
⟶
x2
(
x3
(
x4
x5
)
)
=
x4
(
x2
(
x3
x5
)
)
(proof)
Theorem
7d7de..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
(
∀ x2 x3 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
∀ x4 .
x0
x4
⟶
x2
(
x3
x4
)
=
x3
(
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
x1
x4
⟶
x1
x5
⟶
∀ x6 .
x0
x6
⟶
x2
(
x3
(
x4
(
x5
x6
)
)
)
=
x5
(
x2
(
x3
(
x4
x6
)
)
)
(proof)
Theorem
53a15..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
(
∀ x2 x3 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
∀ x4 .
x0
x4
⟶
x2
(
x3
x4
)
=
x3
(
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
x1
x4
⟶
x1
x5
⟶
x1
x6
⟶
∀ x7 .
x0
x7
⟶
x2
(
x3
(
x4
(
x5
(
x6
x7
)
)
)
)
=
x6
(
x2
(
x3
(
x4
(
x5
x7
)
)
)
)
(proof)
Theorem
8e732..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
(
∀ x2 x3 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
∀ x4 .
x0
x4
⟶
x2
(
x3
x4
)
=
x3
(
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
x1
x4
⟶
x1
x5
⟶
x1
x6
⟶
x1
x7
⟶
∀ x8 .
x0
x8
⟶
x2
(
x3
(
x4
(
x5
(
x6
(
x7
x8
)
)
)
)
)
=
x7
(
x2
(
x3
(
x4
(
x5
(
x6
x8
)
)
)
)
)
(proof)
Theorem
b1aaf..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
(
∀ x2 x3 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
∀ x4 .
x0
x4
⟶
x2
(
x3
x4
)
=
x3
(
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
x1
x4
⟶
x1
x5
⟶
x1
x6
⟶
x1
x7
⟶
x1
x8
⟶
∀ x9 .
x0
x9
⟶
x2
(
x3
(
x4
(
x5
(
x6
(
x7
(
x8
x9
)
)
)
)
)
)
=
x8
(
x2
(
x3
(
x4
(
x5
(
x6
(
x7
x9
)
)
)
)
)
)
(proof)
Theorem
a2d04..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
(
∀ x2 x3 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
∀ x4 .
x0
x4
⟶
x2
(
x3
x4
)
=
x3
(
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
x1
x4
⟶
x1
x5
⟶
x1
x6
⟶
x1
x7
⟶
x1
x8
⟶
x1
x9
⟶
∀ x10 .
x0
x10
⟶
x2
(
x3
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
x10
)
)
)
)
)
)
)
=
x9
(
x2
(
x3
(
x4
(
x5
(
x6
(
x7
(
x8
x10
)
)
)
)
)
)
)
(proof)
Theorem
9b301..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
(
∀ x2 x3 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
∀ x4 .
x0
x4
⟶
x2
(
x3
x4
)
=
x3
(
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
x1
x4
⟶
x1
x5
⟶
x1
x6
⟶
x1
x7
⟶
x1
x8
⟶
x1
x9
⟶
x1
x10
⟶
∀ x11 .
x0
x11
⟶
x2
(
x3
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
(
x10
x11
)
)
)
)
)
)
)
)
=
x10
(
x2
(
x3
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
x11
)
)
)
)
)
)
)
)
(proof)
Theorem
3c98f..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
(
∀ x2 x3 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
∀ x4 .
x0
x4
⟶
x2
(
x3
x4
)
=
x3
(
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
x1
x4
⟶
x1
x5
⟶
x1
x6
⟶
x1
x7
⟶
x1
x8
⟶
x1
x9
⟶
x1
x10
⟶
x1
x11
⟶
∀ x12 .
x0
x12
⟶
x2
(
x3
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
(
x10
(
x11
x12
)
)
)
)
)
)
)
)
)
=
x11
(
x2
(
x3
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
(
x10
x12
)
)
)
)
)
)
)
)
)
(proof)
Theorem
41b33..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
(
∀ x2 x3 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
∀ x4 .
x0
x4
⟶
x2
(
x3
x4
)
=
x3
(
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
x1
x4
⟶
x1
x5
⟶
x1
x6
⟶
x1
x7
⟶
x1
x8
⟶
x1
x9
⟶
x1
x10
⟶
x1
x11
⟶
x1
x12
⟶
∀ x13 .
x0
x13
⟶
x2
(
x3
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
(
x10
(
x11
(
x12
x13
)
)
)
)
)
)
)
)
)
)
=
x12
(
x2
(
x3
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
(
x10
(
x11
x13
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
11d87..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
(
∀ x2 x3 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
∀ x4 .
x0
x4
⟶
x2
(
x3
x4
)
=
x3
(
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 :
ι → ι
.
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 .
x0
x14
⟶
x2
(
x3
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
(
x10
(
x11
(
x12
(
x13
x14
)
)
)
)
)
)
)
)
)
)
)
=
x13
(
x2
(
x3
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
(
x10
(
x11
(
x12
x14
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
97776..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
(
∀ x2 x3 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
∀ x4 .
x0
x4
⟶
x2
(
x3
x4
)
=
x3
(
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 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
⟶
x1
x14
⟶
∀ x15 .
x0
x15
⟶
x2
(
x3
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
(
x10
(
x11
(
x12
(
x13
(
x14
x15
)
)
)
)
)
)
)
)
)
)
)
)
=
x14
(
x2
(
x3
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
(
x10
(
x11
(
x12
(
x13
x15
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
27d68..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
(
∀ x2 x3 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
∀ x4 .
x0
x4
⟶
x2
(
x3
x4
)
=
x3
(
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 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
⟶
x1
x15
⟶
∀ x16 .
x0
x16
⟶
x2
(
x3
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
(
x10
(
x11
(
x12
(
x13
(
x14
(
x15
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x15
(
x2
(
x3
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
(
x10
(
x11
(
x12
(
x13
(
x14
x16
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
9a7a2..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
(
∀ x2 x3 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
∀ x4 .
x0
x4
⟶
x2
(
x3
x4
)
=
x3
(
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 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
⟶
x1
x16
⟶
∀ x17 .
x0
x17
⟶
x2
(
x3
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
(
x10
(
x11
(
x12
(
x13
(
x14
(
x15
(
x16
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x16
(
x2
(
x3
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
(
x10
(
x11
(
x12
(
x13
(
x14
(
x15
x17
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)
Theorem
76a14..
:
∀ x0 :
ι → ο
.
∀ x1 :
(
ι → ι
)
→ ο
.
(
∀ x2 :
ι → ι
.
x1
x2
⟶
∀ x3 .
x0
x3
⟶
x0
(
x2
x3
)
)
⟶
(
∀ x2 x3 :
ι → ι
.
x1
x2
⟶
x1
x3
⟶
∀ x4 .
x0
x4
⟶
x2
(
x3
x4
)
=
x3
(
x2
x4
)
)
⟶
∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 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
⟶
x1
x17
⟶
∀ x18 .
x0
x18
⟶
x2
(
x3
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
(
x10
(
x11
(
x12
(
x13
(
x14
(
x15
(
x16
(
x17
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
=
x17
(
x2
(
x3
(
x4
(
x5
(
x6
(
x7
(
x8
(
x9
(
x10
(
x11
(
x12
(
x13
(
x14
(
x15
(
x16
x18
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
(proof)