Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 : ι → ι → ι → ι . ∀ x1 : ι → ο . ∀ x2 . ∀ x3 : ι → ι . ∀ x4 x5 x6 x7 . ∀ x8 x9 : ι → ο . ∀ x10 x11 : ι → ι . ∀ x12 . ∀ x13 : ι → ι . ∀ x14 : ι → ο . ∀ x15 : ι → ι . ∀ x16 : ι → ι → ο . ∀ x17 : ι → ι → ι → ι → ι . ∀ x18 : ι → ι → ι → ι . ∀ x19 : ι → ι → ι → ο . ∀ x20 x21 : ι → ο . (∀ x22 x23 x24 x25 . x21 x25x14 x25x20 x25x16 x22 (x15 x25)x16 x24 (x15 x25)x16 x23 (x15 x25)x19 x25 x23 x22x19 x25 x23 x24x19 x25 (x17 x23 x24 x22 x25) x23(x23 = x18 x25 x22 x24False)False)(∀ x22 x23 x24 x25 . x21 x25x14 x25x20 x25x16 x22 (x15 x25)x16 x24 (x15 x25)x16 x23 (x15 x25)x19 x25 x23 x22x19 x25 x23 x24(x19 x25 (x17 x23 x24 x22 x25) x24False)(x23 = x18 x25 x22 x24False)False)(∀ x22 x23 x24 x25 . x21 x25x14 x25x20 x25x16 x22 (x15 x25)x16 x24 (x15 x25)x16 x23 (x15 x25)x19 x25 x23 x22x19 x25 x23 x24(x19 x25 (x17 x23 x24 x22 x25) x22False)(x23 = x18 x25 x22 x24False)False)(∀ x22 x23 x24 x25 . x21 x25x14 x25x20 x25x16 x22 (x15 x25)x16 x24 (x15 x25)x16 x23 (x15 x25)x19 x25 x23 x22x19 x25 x23 x24(x16 (x17 x23 x24 x22 x25) (x15 x25)False)(x23 = x18 x25 x22 x24False)False)(∀ x22 x23 x24 x25 x26 . x21 x26x14 x26x20 x26x16 x22 (x15 x26)x16 x25 (x15 x26)x16 x23 (x15 x26)x23 = x18 x26 x22 x25x16 x24 (x15 x26)x19 x26 x24 x22x19 x26 x24 x25(x19 x26 x24 x23False)False)(∀ x22 x23 x24 x25 . x21 x25x14 x25x20 x25x16 x22 (x15 x25)x16 x24 (x15 x25)x16 x23 (x15 x25)x23 = x18 x25 x22 x24(x19 x25 x23 x24False)False)(∀ x22 x23 x24 x25 . x21 x25x14 x25x20 x25x16 x22 (x15 x25)x16 x24 (x15 x25)x16 x23 (x15 x25)x23 = x18 x25 x22 x24(x19 x25 x23 x22False)False)(∀ x22 x23 x24 . x21 x24x14 x24x20 x24x16 x22 (x15 x24)x16 x23 (x15 x24)(x18 x24 x22 x23 = x0 x24 x22 x23False)False)(∀ x22 . (x16 (x13 x22) x22False)False)((x1 x2False)False)((x20 x12False)False)(∀ x22 . x20 x22(x1 x22False)False)(∀ x22 x23 x24 . x21 x24x14 x24x20 x24x16 x22 (x15 x24)x16 x23 (x15 x24)(x16 (x18 x24 x22 x23) (x15 x24)False)False)(∀ x22 x23 x24 . x20 x24x16 x22 (x15 x24)x16 x23 (x15 x24)(x16 (x0 x24 x22 x23) (x15 x24)False)False)(∀ x22 . x20 x22x19 x22 (x10 x22) (x11 x22)(x9 x22False)False)(∀ x22 . x20 x22(x19 x22 (x3 x22) (x11 x22)False)(x9 x22False)False)(∀ x22 . x20 x22(x19 x22 (x10 x22) (x3 x22)False)(x9 x22False)False)(∀ x22 . x20 x22(x16 (x11 x22) (x15 x22)False)(x9 x22False)False)(∀ x22 . x20 x22(x16 (x3 x22) (x15 x22)False)(x9 x22False)False)(∀ x22 . x20 x22(x16 (x10 x22) (x15 x22)False)(x9 x22False)False)(∀ x22 x23 x24 x25 . x20 x25x9 x25x16 x24 (x15 x25)x16 x22 (x15 x25)x16 x23 (x15 x25)x19 x25 x24 x22x19 x25 x22 x23(x19 x25 x24 x23False)False)(∀ x22 x23 x24 . x21 x24x14 x24x20 x24x16 x22 (x15 x24)x16 x23 (x15 x24)(x18 x24 x22 x23 = x18 x24 x23 x22False)False)(∀ x22 . x20 x22x14 x22x8 x22False)(x19 x4 x5 x6False)((x19 x4 x5 (x18 x4 x6 x7)False)False)((x16 x5 (x15 x4)False)False)((x16 x7 (x15 x4)False)False)((x16 x6 (x15 x4)False)False)((x20 x4False)False)((x14 x4False)False)((x21 x4False)False)((x9 x4False)False)False
as obj
-
as prop
2ea5a..
theory
HotG
stx
02354..
address
TMZ7f..