Search for blocks/addresses/...

Proofgold Proposition

∀ x0 . x0setexp (SNoS_ omega) omega∀ x1 . x1setexp (SNoS_ omega) omega(∀ x2 . x2omega∀ x3 . x3omegaSNoLt (ap x0 x2) (ap x1 x3))∀ x2 : ο . (SNoCutP (prim5 omega (ap x0)) (prim5 omega (ap x1))SNo (SNoCut (prim5 omega (ap x0)) (prim5 omega (ap x1)))SNoLev (SNoCut (prim5 omega (ap x0)) (prim5 omega (ap x1)))ordsucc omegaSNoCut (prim5 omega (ap x0)) (prim5 omega (ap x1))SNoS_ (ordsucc omega)(∀ x3 . x3omegaSNoLt (ap x0 x3) (SNoCut (prim5 omega (ap x0)) (prim5 omega (ap x1))))(∀ x3 . x3omegaSNoLt (SNoCut (prim5 omega (ap x0)) (prim5 omega (ap x1))) (ap x1 x3))x2)x2
type
prop
theory
HotG
name
SNo_approx_real_lem
proof
PUK9h..
Megalodon
SNo_approx_real_lem
proofgold address
TMbTG..SNo_approx_real_lem
creator
12306 PrGxv../70662..
owner
12306 PrGxv../70662..
term root
d275e..