Search for blocks/addresses/...

Proofgold Term Root Disambiguation

(∀ x0 . prime_nat x0odd_nat x0∀ x1 : ο . (∀ x2 . and (x2setminus x0 (Sing 0)) (∀ x3 : ο . (∀ x4 . and (x4omega) (∀ x5 : ο . (∀ x6 . and (x6omega) (∀ x7 : ο . (∀ x8 . and (x8omega) (∀ x9 : ο . (∀ x10 . and (x10omega) (mul_SNo x2 x0 = add_SNo (mul_SNo x4 x4) (add_SNo (mul_SNo x6 x6) (add_SNo (mul_SNo x8 x8) (mul_SNo x10 x10))))x9)x9)x7)x7)x5)x5)x3)x3)x1)x1)(∀ x0 . nat_p x0∀ x1 . x1omega∀ x2 . x2omega∀ x3 . x3omega∀ x4 . x4omegamul_SNo 2 x0 = add_SNo (mul_SNo x1 x1) (add_SNo (mul_SNo x2 x2) (add_SNo (mul_SNo x3 x3) (mul_SNo x4 x4)))∀ x5 : ο . (∀ x6 . x6omega∀ x7 . x7omega∀ x8 . x8omega∀ x9 . x9omegax0 = add_SNo (mul_SNo x6 x6) (add_SNo (mul_SNo x7 x7) (add_SNo (mul_SNo x8 x8) (mul_SNo x9 x9)))x5)x5)∀ x0 . prime_nat x0odd_nat x0∀ x1 : ο . (∀ x2 . and (x2omega) (∀ x3 : ο . (∀ x4 . and (x4omega) (∀ x5 : ο . (∀ x6 . and (x6omega) (∀ x7 : ο . (∀ x8 . and (x8omega) (x0 = add_SNo (mul_SNo x2 x2) (add_SNo (mul_SNo x4 x4) (add_SNo (mul_SNo x6 x6) (mul_SNo x8 x8))))x7)x7)x5)x5)x3)x3)x1)x1
as obj
-
as prop
69709..
theory
HotG
stx
f6ee3..
address
TMKHp..