Search for blocks/addresses/...
Proofgold Proposition
∀ x0 .
∀ x1 :
ι →
ι → ο
.
(
∀ x2 x3 .
x1
x2
x3
⟶
x1
x3
x2
)
⟶
∀ x2 x3 .
x2
∈
x0
⟶
∀ x4 .
nat_p
x4
⟶
(
∀ x5 .
x5
∈
x0
⟶
(
x5
=
x2
⟶
∀ x6 : ο .
x6
)
⟶
not
(
x1
x5
x2
)
⟶
or
(
equip
(
binintersect
(
DirGraphOutNeighbors
x0
x1
x5
)
(
DirGraphOutNeighbors
x0
x1
x2
)
)
x4
)
(
equip
(
binintersect
(
DirGraphOutNeighbors
x0
x1
x5
)
(
DirGraphOutNeighbors
x0
x1
x2
)
)
(
ordsucc
x4
)
)
)
⟶
(
∀ x5 .
x5
∈
{x6 ∈
setminus
x0
(
binunion
(
DirGraphOutNeighbors
x0
x1
x2
)
(
Sing
x2
)
)
|
equip
(
binintersect
(
DirGraphOutNeighbors
x0
x1
x6
)
(
DirGraphOutNeighbors
x0
x1
x2
)
)
x4
}
⟶
not
(
x1
x3
x5
)
)
⟶
(
∀ x5 .
x5
∈
setminus
(
DirGraphOutNeighbors
x0
x1
x3
)
(
Sing
x2
)
⟶
not
(
x1
x2
x5
)
)
⟶
∀ x5 .
x5
∈
setminus
(
DirGraphOutNeighbors
x0
x1
x3
)
(
Sing
x2
)
⟶
equip
(
binintersect
(
DirGraphOutNeighbors
x0
x1
x5
)
(
DirGraphOutNeighbors
x0
x1
x2
)
)
(
ordsucc
x4
)
type
prop
theory
HotG
name
-
proof
PUMia..
Megalodon
-
proofgold address
TMTto..
creator
27176
Pr4zB..
/
547f5..
owner
27176
Pr4zB..
/
547f5..
term root
5f1f3..