Proofgold Proposition

∀ x0 . nat_p x0 ⟶ add_SNo (eps_ (ordsucc x0)) (eps_ (ordsucc x0)) = eps_ x0

type
prop

theory
HotG

name
eps_ordsucc_half_add

proof
PUfRQ..

Megalodon
eps_ordsucc_half_add

proofgold address
TMUSP..^{eps_ordsucc_half_add}

creator
6761 Pr6Pc../188a8..

owner
6761 Pr6Pc../188a8..

term root
6f06c..