Search for blocks/addresses/...
Proofgold Proposition
∀ x0 .
SNo
x0
⟶
(
∀ x1 .
x1
∈
omega
⟶
∀ x2 : ο .
(
∀ x3 .
and
(
x3
∈
SNoS_
omega
)
(
and
(
SNoLt
x3
x0
)
(
SNoLt
x0
(
add_SNo
x3
(
eps_
x1
)
)
)
)
⟶
x2
)
⟶
x2
)
⟶
∀ x1 .
x1
∈
omega
⟶
∀ x2 : ο .
(
∀ x3 .
and
(
x3
∈
SNoS_
omega
)
(
and
(
SNoLt
x3
(
minus_SNo
x0
)
)
(
SNoLt
(
minus_SNo
x0
)
(
add_SNo
x3
(
eps_
x1
)
)
)
)
⟶
x2
)
⟶
x2
type
prop
theory
HotG
name
minus_SNo_prereal_2
proof
PUgvb..
Megalodon
minus_SNo_prereal_2
proofgold address
TMJ2G..
minus_SNo_prereal_2
creator
12283
PrGxv..
/
db2ff..
owner
12283
PrGxv..
/
db2ff..
term root
68fe9..