Search for blocks/addresses/...

Proofgold Proposition

∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1and (SNo (x0 x1)) (∀ x2 : ο . (∀ x3 . and (SNo x3) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (∀ x14 : ο . (∀ x15 . and (SNo x15) (x1 = bbc71.. (x0 x1) x3 x5 x7 x9 x11 x13 x15)x14)x14)x12)x12)x10)x10)x8)x8)x6)x6)x4)x4)x2)x2))(∀ x1 . 1eb0a.. x1SNo (x0 x1))∀ x1 : ι → ι . (∀ x2 . 1eb0a.. x2and (SNo (x1 x2)) (∀ x3 : ο . (∀ x4 . and (SNo x4) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (∀ x13 : ο . (∀ x14 . and (SNo x14) (x2 = bbc71.. (x0 x2) (x1 x2) x4 x6 x8 x10 x12 x14)x13)x13)x11)x11)x9)x9)x7)x7)x5)x5)x3)x3))(∀ x2 . 1eb0a.. x2SNo (x1 x2))∀ x2 : ι → ι . (∀ x3 . 1eb0a.. x3and (SNo (x2 x3)) (∀ x4 : ο . (∀ x5 . and (SNo x5) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (∀ x12 : ο . (∀ x13 . and (SNo x13) (x3 = bbc71.. (x0 x3) (x1 x3) (x2 x3) x5 x7 x9 x11 x13)x12)x12)x10)x10)x8)x8)x6)x6)x4)x4))(∀ x3 . 1eb0a.. x3SNo (x2 x3))∀ x3 : ι → ι . (∀ x4 . 1eb0a.. x4and (SNo (x3 x4)) (∀ x5 : ο . (∀ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (∀ x11 : ο . (∀ x12 . and (SNo x12) (x4 = bbc71.. (x0 x4) (x1 x4) (x2 x4) (x3 x4) x6 x8 x10 x12)x11)x11)x9)x9)x7)x7)x5)x5))(∀ x4 . 1eb0a.. x4SNo (x3 x4))∀ x4 : ι → ι . (∀ x5 . 1eb0a.. x5and (SNo (x4 x5)) (∀ x6 : ο . (∀ x7 . and (SNo x7) (∀ x8 : ο . (∀ x9 . and (SNo x9) (∀ x10 : ο . (∀ x11 . and (SNo x11) (x5 = bbc71.. (x0 x5) (x1 x5) (x2 x5) (x3 x5) (x4 x5) x7 x9 x11)x10)x10)x8)x8)x6)x6))(∀ x5 . 1eb0a.. x5SNo (x4 x5))∀ x5 : ι → ι . (∀ x6 . 1eb0a.. x6and (SNo (x5 x6)) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (x6 = bbc71.. (x0 x6) (x1 x6) (x2 x6) (x3 x6) (x4 x6) (x5 x6) x8 x10)x9)x9)x7)x7))(∀ x6 . 1eb0a.. x6SNo (x5 x6))∀ x6 : ι → ι . (∀ x7 . 1eb0a.. x7and (SNo (x6 x7)) (∀ x8 : ο . (∀ x9 . and (SNo x9) (x7 = bbc71.. (x0 x7) (x1 x7) (x2 x7) (x3 x7) (x4 x7) (x5 x7) (x6 x7) x9)x8)x8))∀ x7 . 1eb0a.. x7and (SNo (053de.. x0 x1 x2 x3 x4 x5 x6 x7)) (x7 = bbc71.. (x0 x7) (x1 x7) (x2 x7) (x3 x7) (x4 x7) (x5 x7) (x6 x7) (053de.. x0 x1 x2 x3 x4 x5 x6 x7))
type
prop
theory
HotG
name
-
proof
PUY4m..
Megalodon
-
proofgold address
TMRnz..
creator
28250 PrQUS../4b8dd..
owner
28250 PrQUS../4b8dd..
term root
d4d9f..