Search for blocks/addresses/...

Proofgold Proposition

∀ x0 . x0SNoS_ (ordsucc omega)SNoLt 0 x0SNoLt x0 omega∀ x1 : ο . (∀ x2 . and (x2omega) (SNoLt (mul_SNo (eps_ x2) x0) 1)x1)x1
type
prop
theory
HotG
name
SNoS_ordsucc_omega_bdd_eps_pos
proof
PULPi..
Megalodon
SNoS_ordsucc_omega_bdd_eps_pos
proofgold address
TMM2m..SNoS_ordsucc_omega_bdd_eps_pos
creator
12306 PrGxv../ab7ed..
owner
12306 PrGxv../ab7ed..
term root
06495..