Search for blocks/addresses/...
Proofgold Proposition
∀ x0 x1 .
SNoCutP
x0
x1
⟶
(
∀ x2 .
x2
∈
x0
⟶
minus_SNo
(
minus_SNo
x2
)
=
x2
)
⟶
(
∀ x2 .
x2
∈
x1
⟶
minus_SNo
(
minus_SNo
x2
)
=
x2
)
⟶
(
∀ x2 .
x2
∈
x0
⟶
SNo
x2
)
⟶
(
∀ x2 .
x2
∈
x1
⟶
SNo
x2
)
⟶
SNo
(
SNoCut
x0
x1
)
⟶
SNo
(
minus_SNo
(
minus_SNo
(
SNoCut
x0
x1
)
)
)
⟶
and
(
SNoLev
(
SNoCut
x0
x1
)
⊆
SNoLev
(
minus_SNo
(
minus_SNo
(
SNoCut
x0
x1
)
)
)
)
(
SNoEq_
(
SNoLev
(
SNoCut
x0
x1
)
)
(
SNoCut
x0
x1
)
(
minus_SNo
(
minus_SNo
(
SNoCut
x0
x1
)
)
)
)
⟶
minus_SNo
(
minus_SNo
(
SNoCut
x0
x1
)
)
=
SNoCut
x0
x1
type
prop
theory
HotG
name
-
proof
PUTNo..
Megalodon
Conj_minus_SNo_invol__5__6
proofgold address
TMJwh..
Conj_minus_SNo_invol__5__6
creator
35053
PrNpY..
/
ed8ef..
owner
35061
PrNpY..
/
2dcb2..
term root
6ebb6..