Proofgold Proposition

∀ x0 x1 . x0 ∈ omega ⟶ SNo (eps_ (ordsucc x0)) ⟶ SNo x1 ⟶ SNoLev x1 ∈ ordsucc (ordsucc x0) ⟶ SNoLt x1 (eps_ (ordsucc x0)) ⟶ SNoLe x1 0 ⟶ and (SNoLt (add_SNo x1 (eps_ (ordsucc x0))) (eps_ x0)) (SNoLt (add_SNo (eps_ (ordsucc x0)) x1) (eps_ x0))

type
prop

theory
HotG

name
-

proof
PUTNo..

Megalodon
Conj_eps_ordsucc_half_add__7__0

proofgold address
TMJb5..^{Conj_eps_ordsucc_half_add__7__0}

creator
35053 PrNpY../78599..

owner
35061 PrNpY../b5c50..

term root
dc63f..