Search for blocks/addresses/...
Proofgold Proposition
∀ x0 :
ι →
ι →
ι → ο
.
(
∀ x1 x2 x3 .
SNo
x1
⟶
SNo
x2
⟶
SNo
x3
⟶
(
∀ x4 .
x4
∈
SNoS_
(
SNoLev
x1
)
⟶
x0
x4
x2
x3
)
⟶
(
∀ x4 .
x4
∈
SNoS_
(
SNoLev
x2
)
⟶
x0
x1
x4
x3
)
⟶
(
∀ x4 .
x4
∈
SNoS_
(
SNoLev
x3
)
⟶
x0
x1
x2
x4
)
⟶
(
∀ x4 .
x4
∈
SNoS_
(
SNoLev
x1
)
⟶
∀ x5 .
x5
∈
SNoS_
(
SNoLev
x2
)
⟶
x0
x4
x5
x3
)
⟶
(
∀ x4 .
x4
∈
SNoS_
(
SNoLev
x1
)
⟶
∀ x5 .
x5
∈
SNoS_
(
SNoLev
x3
)
⟶
x0
x4
x2
x5
)
⟶
(
∀ x4 .
x4
∈
SNoS_
(
SNoLev
x2
)
⟶
∀ x5 .
x5
∈
SNoS_
(
SNoLev
x3
)
⟶
x0
x1
x4
x5
)
⟶
(
∀ x4 .
x4
∈
SNoS_
(
SNoLev
x1
)
⟶
∀ x5 .
x5
∈
SNoS_
(
SNoLev
x2
)
⟶
∀ x6 .
x6
∈
SNoS_
(
SNoLev
x3
)
⟶
x0
x4
x5
x6
)
⟶
x0
x1
x2
x3
)
⟶
∀ x1 x2 x3 .
SNo
x1
⟶
SNo
x2
⟶
SNo
x3
⟶
x0
x1
x2
x3
type
prop
theory
HotG
name
SNoLev_ind3
proof
PUK1b..
Megalodon
SNoLev_ind3
proofgold address
TMNAm..
SNoLev_ind3
creator
4949
Pr6Pc..
/
c1a35..
owner
4949
Pr6Pc..
/
c1a35..
term root
f1d77..