Proofgold Proposition

∀ x0 x1 . SNo x0 ⟶ SNo_max_of (SNoL x0) x1 ⟶ ∀ x2 . SNo x2 ⟶ SNoLt x0 x2 ⟶ SNoLt (add_SNo x1 x2) (add_SNo x0 x0) ⟶ ∀ x3 : ο . (∀ x4 . and (x4 ∈ SNoR x2) (add_SNo x1 x4 = add_SNo x0 x0) ⟶ x3) ⟶ x3

type
prop

theory
HotG

name
double_SNo_max_1

proof
PUesu..

Megalodon
double_SNo_max_1

proofgold address
TMGEs..^{double_SNo_max_1}

creator
12391 PrGxv../f4e08..

owner
12391 PrGxv../f4e08..

term root
3155e..