Search for blocks/addresses/...

Proofgold Proposition

∀ x0 : ι → ο . ∀ x1 : (ι → ο) → ο . ∀ x2 : (ι → ι → ο) → ο . ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x0 x3x0 x4x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x0 x13x0 x14x0 x15x0 x16(∀ x17 : ι → ο . x17 x3x17 x4x17 x5x17 x6x17 x7x17 x8x17 x9x17 x10x17 x11x17 x12x17 x13x17 x14x17 x15x17 x16x1 x17)(∀ x17 : ι → ι → ο . x17 x3 x3x17 x3 x4x17 x3 x5x17 x3 x6x17 x3 x7x17 x3 x8x17 x3 x9x17 x3 x10x17 x3 x11x17 x3 x12x17 x3 x13x17 x3 x14x17 x3 x15x17 x3 x16x17 x4 x3x17 x4 x4x17 x4 x5x17 x4 x6x17 x4 x7x17 x4 x8x17 x4 x9x17 x4 x10x17 x4 x11x17 x4 x12x17 x4 x13x17 x4 x14x17 x4 x15x17 x4 x16x17 x5 x3x17 x5 x4x17 x5 x5x17 x5 x6x17 x5 x7x17 x5 x8x17 x5 x9x17 x5 x10x17 x5 x11x17 x5 x12x17 x5 x13x17 x5 x14x17 x5 x15x17 x5 x16x17 x6 x3x17 x6 x4x17 x6 x5x17 x6 x6x17 x6 x7x17 x6 x8x17 x6 x9x17 x6 x10x17 x6 x11x17 x6 x12x17 x6 x13x17 x6 x14x17 x6 x15x17 x6 x16x17 x7 x3x17 x7 x4x17 x7 x5x17 x7 x6x17 x7 x7x17 x7 x8x17 x7 x9x17 x7 x10x17 x7 x11x17 x7 x12x17 x7 x13x17 x7 x14x17 x7 x15x17 x7 x16x17 x8 x3x17 x8 x4x17 x8 x5x17 x8 x6x17 x8 x7x17 x8 x8x17 x8 x9x17 x8 x10x17 x8 x11x17 x8 x12x17 x8 x13x17 x8 x14x17 x8 x15x17 x8 x16x17 x9 x3x17 x9 x4x17 x9 x5x17 x9 x6x17 x9 x7x17 x9 x8x17 x9 x9x17 x9 x10x17 x9 x11x17 x9 x12x17 x9 x13x17 x9 x14x17 x9 x15x17 x9 x16x17 x10 x3x17 x10 x4x17 x10 x5x17 x10 x6x17 x10 x7x17 x10 x8x17 x10 x9x17 x10 x10x17 x10 x11x17 x10 x12x17 x10 x13x17 x10 x14x17 x10 x15x17 x10 x16x17 x11 x3x17 x11 x4x17 x11 x5x17 x11 x6x17 x11 x7x17 x11 x8x17 x11 x9x17 x11 x10x17 x11 x11x17 x11 x12x17 x11 x13x17 x11 x14x17 x11 x15x17 x11 x16x17 x12 x3x17 x12 x4x17 x12 x5x17 x12 x6x17 x12 x7x17 x12 x8x17 x12 x9x17 x12 x10x17 x12 x11x17 x12 x12x17 x12 x13x17 x12 x14x17 x12 x15x17 x12 x16x17 x13 x3x17 x13 x4x17 x13 x5x17 x13 x6x17 x13 x7x17 x13 x8x17 x13 x9x17 x13 x10x17 x13 x11x17 x13 x12x17 x13 x13x17 x13 x14x17 x13 x15x17 x13 x16x17 x14 x3x17 x14 x4x17 x14 x5x17 x14 x6x17 x14 x7x17 x14 x8x17 x14 x9x17 x14 x10x17 x14 x11x17 x14 x12x17 x14 x13x17 x14 x14x17 x14 x15x17 x14 x16x17 x15 x3x17 x15 x4x17 x15 x5x17 x15 x6x17 x15 x7x17 x15 x8x17 x15 x9x17 x15 x10x17 x15 x11x17 x15 x12x17 x15 x13x17 x15 x14x17 x15 x15x17 x15 x16x17 x16 x3x17 x16 x4x17 x16 x5x17 x16 x6x17 x16 x7x17 x16 x8x17 x16 x9x17 x16 x10x17 x16 x11x17 x16 x12x17 x16 x13x17 x16 x14x17 x16 x15x17 x16 x16x1 (λ x18 . x1 (x17 x18)))(∀ x17 : ι → ι → ο . x17 x3 x4x17 x3 x5x17 x4 x5x17 x3 x6x17 x4 x6x17 x5 x6x17 x3 x7x17 x4 x7x17 x5 x7x17 x6 x7x17 x3 x8x17 x4 x8x17 x5 x8x17 x6 x8x17 x7 x8x17 x3 x9x17 x4 x9x17 x5 x9x17 x6 x9x17 x7 x9x17 x8 x9x17 x3 x10x17 x4 x10x17 x5 x10x17 x6 x10x17 x7 x10x17 x8 x10x17 x9 x10x17 x3 x11x17 x4 x11x17 x5 x11x17 x6 x11x17 x7 x11x17 x8 x11x17 x9 x11x17 x10 x11x17 x3 x12x17 x4 x12x17 x5 x12x17 x6 x12x17 x7 x12x17 x8 x12x17 x9 x12x17 x10 x12x17 x11 x12x17 x3 x13x17 x4 x13x17 x5 x13x17 x6 x13x17 x7 x13x17 x8 x13x17 x9 x13x17 x10 x13x17 x11 x13x17 x12 x13x17 x3 x14x17 x4 x14x17 x5 x14x17 x6 x14x17 x7 x14x17 x8 x14x17 x9 x14x17 x10 x14x17 x11 x14x17 x12 x14x17 x13 x14x17 x3 x15x17 x4 x15x17 x5 x15x17 x6 x15x17 x7 x15x17 x8 x15x17 x9 x15x17 x10 x15x17 x11 x15x17 x12 x15x17 x13 x15x17 x14 x15x17 x3 x16x17 x4 x16x17 x5 x16x17 x6 x16x17 x7 x16x17 x8 x16x17 x9 x16x17 x10 x16x17 x11 x16x17 x12 x16x17 x13 x16x17 x14 x16x17 x15 x16x2 x17)∀ x17 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . ∀ x18 : ι → ι → ι . (∀ x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 . x18 (x17 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32) x3 = x19)(∀ x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 . x18 (x17 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32) x4 = x20)(∀ x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 . x18 (x17 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32) x5 = x21)(∀ x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 . x18 (x17 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32) x6 = x22)(∀ x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 . x18 (x17 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32) x7 = x23)(∀ x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 . x18 (x17 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32) x8 = x24)(∀ x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 . x18 (x17 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32) x9 = x25)(∀ x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 . x18 (x17 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32) x10 = x26)(∀ x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 . x18 (x17 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32) x11 = x27)(∀ x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 . x18 (x17 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32) x12 = x28)(∀ x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 . x18 (x17 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32) x13 = x29)(∀ x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 . x18 (x17 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32) x14 = x30)(∀ x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 . x18 (x17 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32) x15 = x31)(∀ x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 . x18 (x17 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32) x16 = x32)∀ x19 : ο . (∀ x20 : ι → ι → ι . (∀ x21 : ο . (∀ x22 : ι → ι → ι . and (f3993.. x0 x1 x2 x3 x20 x22) (∀ x23 : ο . (∀ x24 . (∀ x25 : ο . (∀ x26 . (∀ x27 : ο . (∀ x28 . (∀ x29 : ο . (∀ x30 . (∀ x31 : ο . (∀ x32 . and (and (and (and (and (and (x0 x24) (x0 x26)) (x0 x28)) (x0 x30)) (x0 x32)) (and (and (and (and (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 (x20 x24 (x22 x3 x28)) (x22 x3 x30) (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 (x22 x3 x32) x28 (x20 x24 (x22 x3 x28))) = 2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 (x22 x3 x32) x28 (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 (x20 x24 (x22 x3 x28)) (x22 x3 x30) (x20 x24 (x22 x3 x28)))) (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 x32 x24 (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 x28 (x22 x3 x32) x28) = 2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 x28 (x22 x3 x32) (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 x32 x24 x28))) (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 (x20 x24 (x22 x3 x28)) (x20 x24 (x22 x3 x28)) (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 (x22 x24 x26) x26 x26) = 2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 (x22 x24 x26) x26 (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 (x20 x24 (x22 x3 x28)) (x20 x24 (x22 x3 x28)) x26))) (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 x24 x32 (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 (x22 x24 x26) (x20 x24 (x22 x3 x28)) (x22 x3 x32)) = 2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 (x22 x24 x26) (x20 x24 (x22 x3 x28)) (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 x24 x32 (x22 x3 x32)))) (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 x32 (x22 x3 x32) (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 x32 (x22 x3 x30) x26) = 2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 x32 (x22 x3 x30) (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 x32 (x22 x3 x32) x26)))) (and (x20 x30 (x20 (x20 (x22 x3 x28) (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 x24 x26 x28)) x32) = x4) (x20 (x20 x30 (x20 (x22 x3 x28) (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 x24 x26 x28))) x32 = x5))x31)x31)x29)x29)x27)x27)x25)x25)x23)x23)x21)x21)x19)x19
type
prop
theory
HotG
name
-
proof
PUV5s..
Megalodon
-
proofgold address
TMLst..
creator
9425 PrGxv../86615..
owner
9435 PrGxv../d193a..
term root
09060..