Search for blocks/addresses/...

Proofgold Proposition

∀ x0 . SNo x0 ⟶ SNoLe 0 x0 ⟶ SNoCutP (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 0)) (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 1))
type
prop
theory
HotG
name
SNo_sqrt_SNo_SNoCutP
proof
PUS8F..
Megalodon
SNo_sqrt_SNo_SNoCutP
proofgold address
TMMsG..SNo_sqrt_SNo_SNoCutP
creator
27870 PrQUS../536fb..
owner
27870 PrQUS../536fb..
term root
33c12..