Proofgold Proposition

∀ x0 x1 x2 . SNo x0 ⟶ (∀ x3 . x3 ∈ SNoS_ (SNoLev x0) ⟶ and (and (and (SNo (minus_SNo x3)) (∀ x4 . x4 ∈ SNoL x3 ⟶ SNoLt (minus_SNo x3) (minus_SNo x4))) (∀ x4 . x4 ∈ SNoR x3 ⟶ SNoLt (minus_SNo x4) (minus_SNo x3))) (SNoCutP (prim5 (SNoR x3) minus_SNo) (prim5 (SNoL x3) minus_SNo))) ⟶ SNo x1 ⟶ SNoLev x1 ∈ SNoLev x0 ⟶ SNoLt x0 x1 ⟶ SNo x2 ⟶ SNoLt x2 x0 ⟶ (∀ x3 . x3 ∈ SNoR x2 ⟶ SNoLt (minus_SNo x3) (minus_SNo x2)) ⟶ SNo (minus_SNo x1) ⟶ (∀ x3 . x3 ∈ SNoL x1 ⟶ SNoLt (minus_SNo x1) (minus_SNo x3)) ⟶ SNoLt x2 x1 ⟶ SNoLt (minus_SNo x1) (minus_SNo x2)

type
prop

theory
HotG

name
-

proof
PUTNo..

Megalodon
Conj_minus_SNo_prop1__5__7

proofgold address
TMRCM..^{Conj_minus_SNo_prop1__5__7}

creator
35053 PrNpY../1f1b7..

owner
35061 PrNpY../9e81e..

term root
62be8..