Search for blocks/addresses/...
Proofgold Asset
asset id
a7c9c70ab38576e589cbfafafe661551d9063cef81f57251362a01ab27ef62ad
asset hash
40dbace5f0198df3ad3fbdb3ec1e0cbb857324ec30c2b266aa18c00e37f7e0ad
bday / block
39559
tx
2c719..
preasset
doc published by
Pr4zB..
Param
atleastp
atleastp
:
ι
→
ι
→
ο
Param
u11
:
ι
Param
4402e..
:
ι
→
(
ι
→
ι
→
ο
) →
ο
Param
cf2df..
:
ι
→
(
ι
→
ι
→
ο
) →
ο
Param
40920..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
d17b7..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
ed6d2..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
59d98..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
0dd76..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
f7297..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
940a6..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
580d8..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
04c7a..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
8e334..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
7c6aa..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
38607..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
077c6..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
6a2c7..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
01042..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
6d769..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
0c718..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
25ef3..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
fa706..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
e5296..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
36e22..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
b8ed0..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
44299..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
e9a2b..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
7e591..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
aa284..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
ba6f3..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
dafd9..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
546aa..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
1f676..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
0a50a..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
380c0..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
9e687..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
4cf61..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
6c968..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
6fe5f..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
fd9fb..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
7aa0e..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
0e688..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
c1824..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
df3c6..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
c7c61..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
e5b9c..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
ea5d0..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
7f80f..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
f1399..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
0a04b..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
aec6c..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
b50f9..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
cc1e8..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
ade95..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
5ed8e..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
efc7e..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
8fef1..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
418c9..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
f3a4c..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
8dc75..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
36e27..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
8dbd3..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
0ed40..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
76168..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
df932..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
8aed1..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
9f9d1..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
be6eb..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
913ca..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
e1ecf..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
c6073..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
d10a3..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
e1502..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
cb091..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
e4d18..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
e9c3a..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
c34cb..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
805ab..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
4d434..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
42ad9..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
fe1c4..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
61a95..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
5f61d..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
b5d0d..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
01336..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
d6df6..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
92541..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
672d9..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
7fb8b..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
92a6c..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
54502..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
ce66c..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
28caf..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
5a896..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
27efe..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
6e10f..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
244e1..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
10c44..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
cac90..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
f45e1..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
9a447..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
d09d5..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
6c310..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
59ef4..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
6157c..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
6a2f1..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
d246f..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Param
a81fb..
:
(
ι
→
ι
→
ο
) →
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ι
→
ο
Definition
a0244..
:=
λ x0 .
λ x1 :
ι →
ι → ο
.
∀ x2 : ο .
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
40920..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
d17b7..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
ed6d2..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
59d98..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
0dd76..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
f7297..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
940a6..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
580d8..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
04c7a..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
8e334..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
7c6aa..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
38607..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
077c6..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
6a2c7..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
01042..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
6d769..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
0c718..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
25ef3..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
fa706..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
e5296..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
36e22..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
b8ed0..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
44299..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
e9a2b..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
7e591..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
aa284..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
ba6f3..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
dafd9..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
546aa..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
1f676..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
0a50a..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
380c0..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
9e687..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
4cf61..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
6c968..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
6fe5f..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
fd9fb..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
7aa0e..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
0e688..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
c1824..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
df3c6..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
c7c61..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
e5b9c..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
ea5d0..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
7f80f..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
f1399..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
0a04b..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
aec6c..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
b50f9..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
cc1e8..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
ade95..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
5ed8e..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
efc7e..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
8fef1..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
418c9..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
f3a4c..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
8dc75..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
36e27..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
8dbd3..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
0ed40..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
76168..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
df932..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
8aed1..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
9f9d1..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
be6eb..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
913ca..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
e1ecf..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
c6073..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
d10a3..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
e1502..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
cb091..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
e4d18..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
e9c3a..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
c34cb..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
805ab..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
4d434..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
42ad9..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
fe1c4..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
61a95..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
5f61d..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
b5d0d..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
01336..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
d6df6..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
92541..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
672d9..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
7fb8b..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
92a6c..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
54502..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
ce66c..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
28caf..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
5a896..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
27efe..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
6e10f..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
244e1..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
10c44..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
cac90..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
f45e1..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
9a447..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
d09d5..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
6c310..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
59ef4..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
6157c..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
6a2f1..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
d246f..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
∀ x6 .
x6
∈
x0
⟶
∀ x7 .
x7
∈
x0
⟶
∀ x8 .
x8
∈
x0
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
a81fb..
x1
x3
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
⟶
x2
)
⟶
x2
Known
6336e..
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
x1
x2
x3
⟶
x1
x3
x2
)
⟶
atleastp
u11
x0
⟶
4402e..
x0
x1
⟶
cf2df..
x0
x1
⟶
a0244..
x0
x1
Param
ordsucc
ordsucc
:
ι
→
ι
Definition
u12
:=
ordsucc
u11
Param
50e24..
:
ι
→
(
ι
→
ι
→
ο
) →
ο
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
Param
Subq
Subq
:
ι
→
ι
→
ο
Known
19a77..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
40920..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
53fcb..
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
x1
x2
x3
⟶
x1
x3
x2
)
⟶
4402e..
x0
x1
⟶
cf2df..
x0
x1
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
⊆
setminus
x0
(
Sing
x2
)
⟶
∀ x4 .
x4
∈
x3
⟶
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
d17b7..
x1
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
50e24..
x0
x1
Known
5168b..
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
x1
x2
x3
⟶
x1
x3
x2
)
⟶
4402e..
x0
x1
⟶
cf2df..
x0
x1
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
⊆
setminus
x0
(
Sing
x2
)
⟶
∀ x4 .
x4
∈
x3
⟶
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
ed6d2..
x1
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
50e24..
x0
x1
Known
5a97c..
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
x1
x2
x3
⟶
x1
x3
x2
)
⟶
4402e..
x0
x1
⟶
cf2df..
x0
x1
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
⊆
setminus
x0
(
Sing
x2
)
⟶
∀ x4 .
x4
∈
x3
⟶
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
59d98..
x1
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
50e24..
x0
x1
Known
c70d8..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
0dd76..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
c4f3a..
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
x1
x2
x3
⟶
x1
x3
x2
)
⟶
4402e..
x0
x1
⟶
cf2df..
x0
x1
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
⊆
setminus
x0
(
Sing
x2
)
⟶
∀ x4 .
x4
∈
x3
⟶
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
f7297..
x1
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
50e24..
x0
x1
Known
c1faa..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
940a6..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
18ea6..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
580d8..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
8699d..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
04c7a..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
3cc44..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
8e334..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
a1fe2..
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
x1
x2
x3
⟶
x1
x3
x2
)
⟶
4402e..
x0
x1
⟶
cf2df..
x0
x1
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
⊆
setminus
x0
(
Sing
x2
)
⟶
∀ x4 .
x4
∈
x3
⟶
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
7c6aa..
x1
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
50e24..
x0
x1
Known
9c3c7..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
38607..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
3f61d..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
077c6..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
7ee26..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
6a2c7..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
7b9c3..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
01042..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
a6556..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
6d769..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
1f8bb..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
0c718..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
6288f..
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
x1
x2
x3
⟶
x1
x3
x2
)
⟶
4402e..
x0
x1
⟶
cf2df..
x0
x1
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
⊆
setminus
x0
(
Sing
x2
)
⟶
∀ x4 .
x4
∈
x3
⟶
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
25ef3..
x1
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
50e24..
x0
x1
Known
a4757..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
fa706..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
0f024..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
e5296..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
a6b69..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
36e22..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
ebe5a..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
b8ed0..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
bf46b..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
44299..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
ab30f..
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
x1
x2
x3
⟶
x1
x3
x2
)
⟶
4402e..
x0
x1
⟶
cf2df..
x0
x1
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
⊆
setminus
x0
(
Sing
x2
)
⟶
∀ x4 .
x4
∈
x3
⟶
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
e9a2b..
x1
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
50e24..
x0
x1
Known
e10eb..
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
x1
x2
x3
⟶
x1
x3
x2
)
⟶
4402e..
x0
x1
⟶
cf2df..
x0
x1
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
⊆
setminus
x0
(
Sing
x2
)
⟶
∀ x4 .
x4
∈
x3
⟶
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
7e591..
x1
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
50e24..
x0
x1
Known
7d435..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
aa284..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
f863a..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
ba6f3..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
11263..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
dafd9..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
14442..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
546aa..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
ea688..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
1f676..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
75ae0..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
0a50a..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
05f01..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
380c0..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
9eda7..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
9e687..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
1fc12..
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
x1
x2
x3
⟶
x1
x3
x2
)
⟶
4402e..
x0
x1
⟶
cf2df..
x0
x1
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
⊆
setminus
x0
(
Sing
x2
)
⟶
∀ x4 .
x4
∈
x3
⟶
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
4cf61..
x1
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
50e24..
x0
x1
Known
a6c13..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
6c968..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
a0570..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
6fe5f..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
e3243..
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
x1
x2
x3
⟶
x1
x3
x2
)
⟶
4402e..
x0
x1
⟶
cf2df..
x0
x1
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
⊆
setminus
x0
(
Sing
x2
)
⟶
∀ x4 .
x4
∈
x3
⟶
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
fd9fb..
x1
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
50e24..
x0
x1
Known
2654b..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
7aa0e..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
e70f1..
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
x1
x2
x3
⟶
x1
x3
x2
)
⟶
4402e..
x0
x1
⟶
cf2df..
x0
x1
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
⊆
setminus
x0
(
Sing
x2
)
⟶
∀ x4 .
x4
∈
x3
⟶
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
0e688..
x1
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
50e24..
x0
x1
Known
f6f4f..
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
x1
x2
x3
⟶
x1
x3
x2
)
⟶
4402e..
x0
x1
⟶
cf2df..
x0
x1
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
⊆
setminus
x0
(
Sing
x2
)
⟶
∀ x4 .
x4
∈
x3
⟶
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
c1824..
x1
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
50e24..
x0
x1
Known
9387d..
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
x1
x2
x3
⟶
x1
x3
x2
)
⟶
4402e..
x0
x1
⟶
cf2df..
x0
x1
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
⊆
setminus
x0
(
Sing
x2
)
⟶
∀ x4 .
x4
∈
x3
⟶
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
df3c6..
x1
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
50e24..
x0
x1
Known
1d443..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
c7c61..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
b9e45..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
e5b9c..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
cc073..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
ea5d0..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
ad362..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
7f80f..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
a5e03..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
f1399..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
6ff40..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
0a04b..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
e19e2..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
aec6c..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
2124e..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
b50f9..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
f6dbd..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
cc1e8..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
1aa55..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
ade95..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
6c685..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
5ed8e..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
6b1f3..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
efc7e..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
d3ced..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
8fef1..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
c33fc..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
418c9..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
9e666..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
f3a4c..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
78934..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
8dc75..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
7fef1..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
36e27..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
a4186..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
8dbd3..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
16479..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
0ed40..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
1c98a..
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
x1
x2
x3
⟶
x1
x3
x2
)
⟶
4402e..
x0
x1
⟶
cf2df..
x0
x1
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
⊆
setminus
x0
(
Sing
x2
)
⟶
∀ x4 .
x4
∈
x3
⟶
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
76168..
x1
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
50e24..
x0
x1
Known
4832f..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
df932..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
80cc3..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
8aed1..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
4423a..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
9f9d1..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
fefad..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
be6eb..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
7cdbc..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
913ca..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
2026d..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
e1ecf..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
0b630..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
c6073..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
c8662..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
d10a3..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
47fff..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
e1502..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
38ec9..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
cb091..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
a30ee..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
e4d18..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
07951..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
e9c3a..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
3dace..
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
x1
x2
x3
⟶
x1
x3
x2
)
⟶
4402e..
x0
x1
⟶
cf2df..
x0
x1
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
⊆
setminus
x0
(
Sing
x2
)
⟶
∀ x4 .
x4
∈
x3
⟶
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
c34cb..
x1
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
50e24..
x0
x1
Known
19d08..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
805ab..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
30e2b..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
4d434..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
db024..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
42ad9..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
d2ddc..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
fe1c4..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
b7c43..
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
x1
x2
x3
⟶
x1
x3
x2
)
⟶
4402e..
x0
x1
⟶
cf2df..
x0
x1
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
⊆
setminus
x0
(
Sing
x2
)
⟶
∀ x4 .
x4
∈
x3
⟶
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
61a95..
x1
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
50e24..
x0
x1
Known
d9c12..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
5f61d..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
e587e..
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
x1
x2
x3
⟶
x1
x3
x2
)
⟶
4402e..
x0
x1
⟶
cf2df..
x0
x1
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
⊆
setminus
x0
(
Sing
x2
)
⟶
∀ x4 .
x4
∈
x3
⟶
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
b5d0d..
x1
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
50e24..
x0
x1
Known
6eefc..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
01336..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
a0fac..
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
x1
x2
x3
⟶
x1
x3
x2
)
⟶
4402e..
x0
x1
⟶
cf2df..
x0
x1
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
⊆
setminus
x0
(
Sing
x2
)
⟶
∀ x4 .
x4
∈
x3
⟶
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
d6df6..
x1
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
50e24..
x0
x1
Known
e1516..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
92541..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
68485..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
672d9..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
c934e..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
7fb8b..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
996d2..
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
x1
x2
x3
⟶
x1
x3
x2
)
⟶
4402e..
x0
x1
⟶
cf2df..
x0
x1
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
⊆
setminus
x0
(
Sing
x2
)
⟶
∀ x4 .
x4
∈
x3
⟶
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
92a6c..
x1
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
50e24..
x0
x1
Known
8b3ab..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
54502..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
3d003..
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
x1
x2
x3
⟶
x1
x3
x2
)
⟶
4402e..
x0
x1
⟶
cf2df..
x0
x1
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
⊆
setminus
x0
(
Sing
x2
)
⟶
∀ x4 .
x4
∈
x3
⟶
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
ce66c..
x1
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
50e24..
x0
x1
Known
23738..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
28caf..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
bbbd5..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
5a896..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
e3fcd..
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
x1
x2
x3
⟶
x1
x3
x2
)
⟶
4402e..
x0
x1
⟶
cf2df..
x0
x1
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
⊆
setminus
x0
(
Sing
x2
)
⟶
∀ x4 .
x4
∈
x3
⟶
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
27efe..
x1
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
50e24..
x0
x1
Known
869b5..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
6e10f..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
0b470..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
244e1..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
90ff8..
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
x1
x2
x3
⟶
x1
x3
x2
)
⟶
4402e..
x0
x1
⟶
cf2df..
x0
x1
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
⊆
setminus
x0
(
Sing
x2
)
⟶
∀ x4 .
x4
∈
x3
⟶
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
10c44..
x1
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
50e24..
x0
x1
Known
23ba8..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
cac90..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
8244d..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
f45e1..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
1c709..
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
x1
x2
x3
⟶
x1
x3
x2
)
⟶
4402e..
x0
x1
⟶
cf2df..
x0
x1
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
⊆
setminus
x0
(
Sing
x2
)
⟶
∀ x4 .
x4
∈
x3
⟶
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
9a447..
x1
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
50e24..
x0
x1
Known
47e3c..
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
x1
x2
x3
⟶
x1
x3
x2
)
⟶
4402e..
x0
x1
⟶
cf2df..
x0
x1
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
⊆
setminus
x0
(
Sing
x2
)
⟶
∀ x4 .
x4
∈
x3
⟶
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
d09d5..
x1
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
50e24..
x0
x1
Known
7b4eb..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
6c310..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
13cef..
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
x1
x2
x3
⟶
x1
x3
x2
)
⟶
4402e..
x0
x1
⟶
cf2df..
x0
x1
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
⊆
setminus
x0
(
Sing
x2
)
⟶
∀ x4 .
x4
∈
x3
⟶
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
59ef4..
x1
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
50e24..
x0
x1
Known
75381..
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
x1
x2
x3
⟶
x1
x3
x2
)
⟶
4402e..
x0
x1
⟶
cf2df..
x0
x1
⟶
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
⊆
setminus
x0
(
Sing
x2
)
⟶
∀ x4 .
x4
∈
x3
⟶
∀ x5 .
x5
∈
x3
⟶
∀ x6 .
x6
∈
x3
⟶
∀ x7 .
x7
∈
x3
⟶
∀ x8 .
x8
∈
x3
⟶
∀ x9 .
x9
∈
x3
⟶
∀ x10 .
x10
∈
x3
⟶
∀ x11 .
x11
∈
x3
⟶
∀ x12 .
x12
∈
x3
⟶
∀ x13 .
x13
∈
x3
⟶
∀ x14 .
x14
∈
x3
⟶
6157c..
x1
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
50e24..
x0
x1
Known
86fe6..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
6a2f1..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
01521..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
d246f..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
Known
b88c3..
:
∀ 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
⟶
∀ x9 .
x9
∈
x0
⟶
∀ x10 .
x10
∈
x0
⟶
∀ x11 .
x11
∈
x0
⟶
∀ x12 .
x12
∈
x0
⟶
∀ x13 .
x13
∈
x0
⟶
∀ x14 .
x14
∈
x0
⟶
a81fb..
x2
x4
x5
x6
x7
x8
x9
x10
x11
x12
x13
x14
⟶
∀ x15 : ο .
x15
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
f2636..
:
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x0
⟶
x1
x2
x3
⟶
x1
x3
x2
)
⟶
atleastp
u12
x0
⟶
4402e..
x0
x1
⟶
cf2df..
x0
x1
⟶
50e24..
x0
x1
(proof)