Search for blocks/addresses/...
Proofgold Term Root Disambiguation
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 x3 .
x1
x2
x3
⟶
x1
x3
x2
)
⟶
(
∀ x2 .
x2
⊆
x0
⟶
atleastp
u3
x2
⟶
not
(
∀ x3 .
x3
∈
x2
⟶
∀ x4 .
x4
∈
x2
⟶
(
x3
=
x4
⟶
∀ x5 : ο .
x5
)
⟶
x1
x3
x4
)
)
⟶
∀ x2 x3 x4 .
nat_p
x4
⟶
∀ x5 x6 x7 .
x5
⊆
x0
⟶
x6
⊆
x0
⟶
x7
⊆
x0
⟶
x5
=
setminus
(
DirGraphOutNeighbors
x0
x1
x3
)
(
Sing
x2
)
⟶
(
∀ x8 .
x8
∈
x6
⟶
nIn
x8
x5
)
⟶
(
∀ x8 .
x8
∈
x6
⟶
nIn
x8
x7
)
⟶
(
∀ x8 .
x8
∈
x5
⟶
nIn
x8
x7
)
⟶
(
∀ x8 .
x8
∈
x7
⟶
x8
∈
{x9 ∈
setminus
x0
(
binunion
(
DirGraphOutNeighbors
x0
x1
x3
)
(
Sing
x3
)
)
|
equip
(
binintersect
(
DirGraphOutNeighbors
x0
x1
x9
)
(
DirGraphOutNeighbors
x0
x1
x3
)
)
x4
}
)
⟶
∀ x8 x9 .
x8
∈
x6
⟶
x9
∈
x7
⟶
x9
∈
setminus
x0
(
binunion
(
DirGraphOutNeighbors
x0
x1
x2
)
(
Sing
x2
)
)
⟶
x1
x8
x9
⟶
∀ x10 :
ι → ι
.
(
∀ x11 .
x11
∈
x6
⟶
x10
x11
∈
x5
)
⟶
(
∀ x11 .
x11
∈
x6
⟶
x1
x11
(
x10
x11
)
)
⟶
(
∀ x11 .
x11
∈
x5
⟶
∀ x12 : ο .
(
∀ x13 .
and
(
x13
∈
x6
)
(
x10
x13
=
x11
)
⟶
x12
)
⟶
x12
)
⟶
atleastp
x4
{x11 ∈
setminus
x6
(
Sing
x8
)
|
x1
(
x10
x11
)
x9
}
as obj
-
as prop
0bee3..
theory
HotG
stx
e15fa..
address
TMXw7..