Proofgold Proposition

∀ x0 x1 x2 . SNo x1 ⟶ (∀ x3 . x3 ∈ SNoS_ (SNoLev x1) ⟶ and (and (and (and (and (SNo (add_SNo x0 x3)) (∀ x4 . x4 ∈ SNoL x0 ⟶ SNoLt (add_SNo x4 x3) (add_SNo x0 x3))) (∀ x4 . x4 ∈ SNoR x0 ⟶ SNoLt (add_SNo x0 x3) (add_SNo x4 x3))) (∀ x4 . x4 ∈ SNoL x3 ⟶ SNoLt (add_SNo x0 x4) (add_SNo x0 x3))) (∀ x4 . x4 ∈ SNoR x3 ⟶ SNoLt (add_SNo x0 x3) (add_SNo x0 x4))) (SNoCutP (binunion {add_SNo x4 x3|x4 ∈ SNoL x0} (prim5 (SNoL x3) (add_SNo x0))) (binunion {add_SNo x4 x3|x4 ∈ SNoR x0} (prim5 (SNoR x3) (add_SNo x0))))) ⟶ SNoLev x2 ∈ SNoLev x1 ⟶ x2 ∈ SNoS_ (SNoLev x1) ⟶ and (and (and (and (and (SNo (add_SNo x0 x2)) (∀ x3 . x3 ∈ SNoL x0 ⟶ SNoLt (add_SNo x3 x2) (add_SNo x0 x2))) (∀ x3 . x3 ∈ SNoR x0 ⟶ SNoLt (add_SNo x0 x2) (add_SNo x3 x2))) (∀ x3 . x3 ∈ SNoL x2 ⟶ SNoLt (add_SNo x0 x3) (add_SNo x0 x2))) (∀ x3 . x3 ∈ SNoR x2 ⟶ SNoLt (add_SNo x0 x2) (add_SNo x0 x3))) (SNoCutP (binunion {add_SNo x3 x2|x3 ∈ SNoL x0} (prim5 (SNoL x2) (add_SNo x0))) (binunion {add_SNo x3 x2|x3 ∈ SNoR x0} (prim5 (SNoR x2) (add_SNo x0))))

type
prop

theory
HotG

name
-

proof
PUTNo..

Megalodon
Conj_add_SNo_prop1__4__2

proofgold address
TMHM1..^{Conj_add_SNo_prop1__4__2}

creator
35053 PrNpY../2633f..

owner
35061 PrNpY../429a5..

term root
9bef0..