Proofgold Proposition

∀ x0 . SNo x0 ⟶ and (and (and (SNo (minus_SNo x0)) (∀ x1 . x1 ∈ SNoL x0 ⟶ SNoLt (minus_SNo x0) (minus_SNo x1))) (∀ x1 . x1 ∈ SNoR x0 ⟶ SNoLt (minus_SNo x1) (minus_SNo x0))) (SNoCutP (prim5 (SNoR x0) minus_SNo) (prim5 (SNoL x0) minus_SNo))

type
prop

theory
HotG

name
minus_SNo_prop1

proof
PUK1b..

Megalodon
minus_SNo_prop1

proofgold address
TMHp3..^{minus_SNo_prop1}

creator
4949 Pr6Pc../379af..

owner
4949 Pr6Pc../379af..

term root
7c0e8..