Search for blocks/addresses/...
Proofgold Asset
asset id
0dc4dacedd4f23e06850a898afada4ee8984cc0675e497fc31cc9417fe8c9f5b
asset hash
d290d12569a8f82fc9ea6e4f11c9cc2aee1a3355eccc54d5b5b83e5bd46e6cd1
bday / block
34306
tx
6b399..
preasset
doc published by
Pr4zB..
Param
atleastp
atleastp
:
ι
→
ι
→
ο
Param
ordsucc
ordsucc
:
ι
→
ι
Param
u5
:
ι
Definition
u6
:=
ordsucc
u5
Param
4402e..
:
ι
→
(
ι
→
ι
→
ο
) →
ο
Param
cf2df..
:
ι
→
(
ι
→
ι
→
ο
) →
ο
Param
00e19..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
51771..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
32227..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
be724..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
3d300..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
8310d..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
4ce91..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
5e84d..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
fba9e..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
39b60..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
38251..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
6648a..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
f6f09..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
39e43..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
2de86..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
ba720..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
4ea7e..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
170ba..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
f8709..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
f831d..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
9ab39..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
1e330..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
af3c4..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
247da..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
0da49..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
02ade..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
a542b..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
659a1..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
500fe..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
f201d..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
455db..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
85e71..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Definition
and
and
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
Param
setminus
setminus
:
ι
→
ι
→
ι
Param
Sing
Sing
:
ι
→
ι
Known
e2ea8..
:
∀ x0 x1 .
atleastp
(
ordsucc
x0
)
x1
⟶
∀ x2 : ο .
(
∀ x3 .
and
(
x3
∈
x1
)
(
atleastp
x0
(
setminus
x1
(
Sing
x3
)
)
)
⟶
x2
)
⟶
x2
Definition
Subq
Subq
:=
λ x0 x1 .
∀ x2 .
x2
∈
x0
⟶
x2
∈
x1
Param
5a3b5..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
6ff44..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
32385..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
0ee5a..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
45422..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
22dda..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
58403..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
62523..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
87c36..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
42d13..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
c5756..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
2b028..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
80df3..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Known
7a154..
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
x1
x2
x3
⟶
x1
x3
x2
)
⟶
atleastp
u5
x0
⟶
4402e..
x0
x1
⟶
cf2df..
x0
x1
⟶
∀ x2 : ο .
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
5a3b5..
x1
x3
x4
x5
x6
x7
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
6ff44..
x1
x3
x4
x5
x6
x7
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
32385..
x1
x3
x4
x5
x6
x7
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
0ee5a..
x1
x3
x4
x5
x6
x7
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
45422..
x1
x3
x4
x5
x6
x7
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
22dda..
x1
x3
x4
x5
x6
x7
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
58403..
x1
x3
x4
x5
x6
x7
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
62523..
x1
x3
x4
x5
x6
x7
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
87c36..
x1
x3
x4
x5
x6
x7
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
42d13..
x1
x3
x4
x5
x6
x7
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
c5756..
x1
x3
x4
x5
x6
x7
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
2b028..
x1
x3
x4
x5
x6
x7
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
80df3..
x1
x3
x4
x5
x6
x7
⟶
x2
)
⟶
x2
Known
30d72..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
∈
x1
⟶
x2
x3
x4
⟶
x2
x4
x3
)
⟶
4402e..
x1
x2
⟶
cf2df..
x1
x2
⟶
∀ x3 .
x3
∈
x1
⟶
x0
⊆
setminus
x1
(
Sing
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
5a3b5..
x2
x4
x5
x6
x7
x8
⟶
∀ x9 : ο .
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
00e19..
x2
x10
x11
x12
x13
x14
x3
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
5e84d..
x2
x10
x3
x11
x12
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
fba9e..
x2
x10
x11
x3
x12
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
2de86..
x2
x10
x11
x12
x3
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
247da..
x2
x10
x11
x12
x13
x14
x3
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
455db..
x2
x10
x11
x12
x13
x14
x3
⟶
x9
)
⟶
x9
Known
566b3..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
∈
x1
⟶
x2
x3
x4
⟶
x2
x4
x3
)
⟶
4402e..
x1
x2
⟶
cf2df..
x1
x2
⟶
∀ x3 .
x3
∈
x1
⟶
x0
⊆
setminus
x1
(
Sing
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
6ff44..
x2
x4
x5
x6
x7
x8
⟶
∀ x9 : ο .
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
51771..
x2
x10
x11
x12
x13
x3
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
4ce91..
x2
x10
x11
x12
x3
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
fba9e..
x2
x3
x10
x11
x12
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
39b60..
x2
x10
x11
x3
x12
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
38251..
x2
x10
x11
x12
x3
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
ba720..
x2
x10
x11
x12
x3
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
247da..
x2
x10
x3
x11
x12
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
0da49..
x2
x10
x11
x12
x13
x3
x14
⟶
x9
)
⟶
x9
Known
f6ffb..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
∈
x1
⟶
x2
x3
x4
⟶
x2
x4
x3
)
⟶
4402e..
x1
x2
⟶
cf2df..
x1
x2
⟶
∀ x3 .
x3
∈
x1
⟶
x0
⊆
setminus
x1
(
Sing
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
32385..
x2
x4
x5
x6
x7
x8
⟶
∀ x9 : ο .
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
6648a..
x2
x3
x10
x11
x12
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
f6f09..
x2
x3
x10
x11
x12
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
39e43..
x2
x10
x3
x11
x12
x13
x14
⟶
x9
)
⟶
x9
Known
98e05..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
∈
x1
⟶
x2
x3
x4
⟶
x2
x4
x3
)
⟶
4402e..
x1
x2
⟶
cf2df..
x1
x2
⟶
∀ x3 .
x3
∈
x1
⟶
x0
⊆
setminus
x1
(
Sing
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
0ee5a..
x2
x4
x5
x6
x7
x8
⟶
∀ x9 : ο .
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
32227..
x2
x10
x11
x12
x13
x14
x3
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
be724..
x2
x10
x11
x12
x13
x14
x3
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
38251..
x2
x10
x3
x11
x12
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
f6f09..
x2
x10
x11
x3
x12
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
2de86..
x2
x3
x10
x11
x12
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
ba720..
x2
x10
x3
x11
x12
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
170ba..
x2
x10
x11
x12
x3
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
0da49..
x2
x10
x11
x3
x12
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
455db..
x2
x3
x10
x11
x12
x13
x14
⟶
x9
)
⟶
x9
Known
5e260..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
∈
x1
⟶
x2
x3
x4
⟶
x2
x4
x3
)
⟶
4402e..
x1
x2
⟶
cf2df..
x1
x2
⟶
∀ x3 .
x3
∈
x1
⟶
x0
⊆
setminus
x1
(
Sing
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
45422..
x2
x4
x5
x6
x7
x8
⟶
∀ x9 : ο .
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
51771..
x2
x10
x11
x12
x13
x14
x3
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
4ea7e..
x2
x10
x3
x11
x12
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
f8709..
x2
x10
x3
x11
x12
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
9ab39..
x2
x10
x11
x12
x3
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
0da49..
x2
x10
x11
x12
x13
x14
x3
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
85e71..
x2
x10
x11
x12
x13
x14
x3
⟶
x9
)
⟶
x9
Known
c845f..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
∈
x1
⟶
x2
x3
x4
⟶
x2
x4
x3
)
⟶
4402e..
x1
x2
⟶
cf2df..
x1
x2
⟶
∀ x3 .
x3
∈
x1
⟶
x0
⊆
setminus
x1
(
Sing
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
22dda..
x2
x4
x5
x6
x7
x8
⟶
∀ x9 : ο .
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
be724..
x2
x10
x11
x12
x13
x3
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
3d300..
x2
x10
x11
x12
x13
x14
x3
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
39e43..
x2
x10
x11
x12
x3
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
170ba..
x2
x10
x3
x11
x12
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
f8709..
x2
x3
x10
x11
x12
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
f831d..
x2
x10
x3
x11
x12
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
1e330..
x2
x10
x11
x12
x3
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
0da49..
x2
x3
x10
x11
x12
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
f201d..
x2
x10
x3
x11
x12
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
85e71..
x2
x10
x11
x3
x12
x13
x14
⟶
x9
)
⟶
x9
Known
f8a13..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
∈
x1
⟶
x2
x3
x4
⟶
x2
x4
x3
)
⟶
4402e..
x1
x2
⟶
cf2df..
x1
x2
⟶
∀ x3 .
x3
∈
x1
⟶
x0
⊆
setminus
x1
(
Sing
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
58403..
x2
x4
x5
x6
x7
x8
⟶
∀ x9 : ο .
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
3d300..
x2
x10
x11
x12
x3
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
8310d..
x2
x10
x11
x12
x13
x14
x3
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
9ab39..
x2
x3
x10
x11
x12
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
1e330..
x2
x3
x10
x11
x12
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
af3c4..
x2
x10
x11
x12
x3
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
85e71..
x2
x3
x10
x11
x12
x13
x14
⟶
x9
)
⟶
x9
Known
fc555..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
∈
x1
⟶
x2
x3
x4
⟶
x2
x4
x3
)
⟶
4402e..
x1
x2
⟶
cf2df..
x1
x2
⟶
∀ x3 .
x3
∈
x1
⟶
x0
⊆
setminus
x1
(
Sing
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
62523..
x2
x4
x5
x6
x7
x8
⟶
∀ x9 : ο .
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
5e84d..
x2
x10
x11
x12
x13
x14
x3
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
fba9e..
x2
x10
x11
x12
x13
x14
x3
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
39b60..
x2
x10
x11
x12
x13
x14
x3
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
a542b..
x2
x10
x11
x12
x13
x14
x3
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
659a1..
x2
x10
x11
x12
x13
x14
x3
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
500fe..
x2
x10
x11
x12
x13
x14
x3
⟶
x9
)
⟶
x9
Known
de7ca..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
∈
x1
⟶
x2
x3
x4
⟶
x2
x4
x3
)
⟶
4402e..
x1
x2
⟶
cf2df..
x1
x2
⟶
∀ x3 .
x3
∈
x1
⟶
x0
⊆
setminus
x1
(
Sing
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
87c36..
x2
x4
x5
x6
x7
x8
⟶
∀ x9 : ο .
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
38251..
x2
x10
x11
x12
x13
x14
x3
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
6648a..
x2
x10
x11
x12
x13
x14
x3
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
f6f09..
x2
x10
x11
x12
x13
x14
x3
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
2de86..
x2
x10
x11
x3
x12
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
f8709..
x2
x10
x11
x12
x3
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
247da..
x2
x10
x11
x12
x3
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
a542b..
x2
x10
x3
x11
x12
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
659a1..
x2
x10
x11
x3
x12
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
f201d..
x2
x10
x11
x12
x13
x14
x3
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
455db..
x2
x10
x11
x12
x13
x3
x14
⟶
x9
)
⟶
x9
Known
b9468..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
∈
x1
⟶
x2
x3
x4
⟶
x2
x4
x3
)
⟶
4402e..
x1
x2
⟶
cf2df..
x1
x2
⟶
∀ x3 .
x3
∈
x1
⟶
x0
⊆
setminus
x1
(
Sing
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
42d13..
x2
x4
x5
x6
x7
x8
⟶
∀ x9 : ο .
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
f6f09..
x2
x10
x11
x12
x13
x3
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
39e43..
x2
x10
x11
x12
x13
x14
x3
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
ba720..
x2
x10
x11
x3
x12
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
f831d..
x2
x10
x11
x12
x3
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
0da49..
x2
x10
x11
x12
x3
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
02ade..
x2
x10
x11
x12
x3
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
659a1..
x2
x3
x10
x11
x12
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
500fe..
x2
x10
x11
x3
x12
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
f201d..
x2
x10
x11
x12
x3
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
455db..
x2
x10
x11
x3
x12
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
85e71..
x2
x10
x11
x12
x13
x3
x14
⟶
x9
)
⟶
x9
Known
3b5e3..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
∈
x1
⟶
x2
x3
x4
⟶
x2
x4
x3
)
⟶
4402e..
x1
x2
⟶
cf2df..
x1
x2
⟶
∀ x3 .
x3
∈
x1
⟶
x0
⊆
setminus
x1
(
Sing
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
c5756..
x2
x4
x5
x6
x7
x8
⟶
∀ x9 : ο .
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
4ce91..
x2
x10
x11
x12
x13
x14
x3
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
fba9e..
x2
x10
x11
x12
x13
x3
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
2de86..
x2
x10
x11
x12
x13
x14
x3
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
ba720..
x2
x10
x11
x12
x13
x14
x3
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
4ea7e..
x2
x10
x11
x12
x13
x14
x3
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
f8709..
x2
x10
x11
x12
x13
x14
x3
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
f831d..
x2
x10
x11
x12
x13
x14
x3
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
02ade..
x2
x10
x11
x12
x13
x14
x3
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
a542b..
x2
x10
x11
x12
x3
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
659a1..
x2
x10
x11
x12
x13
x3
x14
⟶
x9
)
⟶
x9
Known
6e535..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
∈
x1
⟶
x2
x3
x4
⟶
x2
x4
x3
)
⟶
4402e..
x1
x2
⟶
cf2df..
x1
x2
⟶
∀ x3 .
x3
∈
x1
⟶
x0
⊆
setminus
x1
(
Sing
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
2b028..
x2
x4
x5
x6
x7
x8
⟶
∀ x9 : ο .
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
39b60..
x2
x10
x11
x12
x13
x3
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
ba720..
x2
x10
x11
x12
x13
x3
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
170ba..
x2
x10
x11
x12
x13
x14
x3
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
f8709..
x2
x10
x11
x12
x13
x3
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
9ab39..
x2
x10
x11
x12
x13
x14
x3
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
1e330..
x2
x10
x11
x12
x13
x14
x3
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
659a1..
x2
x10
x11
x12
x3
x13
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
500fe..
x2
x10
x11
x12
x13
x3
x14
⟶
x9
)
⟶
x9
Known
97955..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 .
x4
∈
x1
⟶
x2
x3
x4
⟶
x2
x4
x3
)
⟶
4402e..
x1
x2
⟶
cf2df..
x1
x2
⟶
∀ x3 .
x3
∈
x1
⟶
x0
⊆
setminus
x1
(
Sing
x3
)
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
80df3..
x2
x4
x5
x6
x7
x8
⟶
∀ x9 : ο .
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
f831d..
x2
x10
x11
x12
x13
x3
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
1e330..
x2
x10
x11
x12
x13
x3
x14
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
af3c4..
x2
x10
x11
x12
x13
x14
x3
⟶
x9
)
⟶
(
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
500fe..
x2
x10
x11
x12
x3
x13
x14
⟶
x9
)
⟶
x9
Known
setminus_Subq
setminus_Subq
:
∀ x0 x1 .
setminus
x0
x1
⊆
x0
Known
Subq_ref
Subq_ref
:
∀ x0 .
x0
⊆
x0
Known
e7c7c..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
x0
⊆
x1
⟶
cf2df..
x1
x2
⟶
cf2df..
x0
x2
Known
a55d1..
:
∀ x0 x1 .
∀ x2 :
ι →
ι → ο
.
x0
⊆
x1
⟶
4402e..
x1
x2
⟶
4402e..
x0
x2
Known
setminusE1
setminusE1
:
∀ x0 x1 x2 .
x2
∈
setminus
x0
x1
⟶
x2
∈
x0
Theorem
64269..
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
x1
x2
x3
⟶
x1
x3
x2
)
⟶
atleastp
u6
x0
⟶
4402e..
x0
x1
⟶
cf2df..
x0
x1
⟶
∀ x2 : ο .
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
00e19..
x1
x3
x4
x5
x6
x7
x8
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
51771..
x1
x3
x4
x5
x6
x7
x8
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
32227..
x1
x3
x4
x5
x6
x7
x8
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
be724..
x1
x3
x4
x5
x6
x7
x8
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
3d300..
x1
x3
x4
x5
x6
x7
x8
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
8310d..
x1
x3
x4
x5
x6
x7
x8
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
4ce91..
x1
x3
x4
x5
x6
x7
x8
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
5e84d..
x1
x3
x4
x5
x6
x7
x8
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
fba9e..
x1
x3
x4
x5
x6
x7
x8
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
39b60..
x1
x3
x4
x5
x6
x7
x8
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
38251..
x1
x3
x4
x5
x6
x7
x8
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
6648a..
x1
x3
x4
x5
x6
x7
x8
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
f6f09..
x1
x3
x4
x5
x6
x7
x8
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
39e43..
x1
x3
x4
x5
x6
x7
x8
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
2de86..
x1
x3
x4
x5
x6
x7
x8
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
ba720..
x1
x3
x4
x5
x6
x7
x8
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
4ea7e..
x1
x3
x4
x5
x6
x7
x8
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
170ba..
x1
x3
x4
x5
x6
x7
x8
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
f8709..
x1
x3
x4
x5
x6
x7
x8
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
f831d..
x1
x3
x4
x5
x6
x7
x8
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
9ab39..
x1
x3
x4
x5
x6
x7
x8
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
1e330..
x1
x3
x4
x5
x6
x7
x8
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
af3c4..
x1
x3
x4
x5
x6
x7
x8
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
247da..
x1
x3
x4
x5
x6
x7
x8
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
0da49..
x1
x3
x4
x5
x6
x7
x8
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
02ade..
x1
x3
x4
x5
x6
x7
x8
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
a542b..
x1
x3
x4
x5
x6
x7
x8
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
659a1..
x1
x3
x4
x5
x6
x7
x8
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
500fe..
x1
x3
x4
x5
x6
x7
x8
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
f201d..
x1
x3
x4
x5
x6
x7
x8
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
455db..
x1
x3
x4
x5
x6
x7
x8
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
85e71..
x1
x3
x4
x5
x6
x7
x8
⟶
x2
)
⟶
x2
(proof)