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 . x22 x24(x24 = x23False)x22 x23False)(∀ x23 x24 . x0 x23 x24x22 x24False)(∀ x23 . x22 x23(x23 = x21False)False)(∀ x23 x24 x25 . x0 x23 x24x2 x24 (x1 x25)x22 x25False)(∀ x23 x24 x25 . x0 x24 x25x2 x25 (x1 x23)(x2 x24 x23False)False)(∀ x23 x24 . x3 x24 x23(x2 x24 (x1 x23)False)False)(∀ x23 x24 . x2 x24 (x1 x23)(x3 x24 x23False)False)(∀ x23 x24 . x0 x23 x24(x3 (x4 x24) x23False)False)(∀ x23 x24 . x2 x23 x24(x22 x24False)(x0 x23 x24False)False)(∀ x23 x24 . x0 x24 x23(x2 x24 x23False)False)(∀ x23 . (x3 x23 x23False)False)(∀ x23 . (x22 x23False)(x6 (x5 x23) x23False)False)(∀ x23 . (x22 x23False)(x2 (x5 x23) (x1 x23)False)False)(∀ x23 . x6 (x7 x23) x23False)(∀ x23 . (x2 (x7 x23) (x1 x23)False)False)(x22 x8False)(∀ x23 . (x22 (x20 x23)False)False)(∀ x23 . (x2 (x20 x23) (x1 x23)False)False)((x22 x19False)False)(∀ x23 . (x22 x23False)x22 (x9 x23)False)(∀ x23 . (x22 x23False)(x2 (x9 x23) (x1 x23)False)False)(∀ x23 . x22 (x10 x23)False)((x22 x21False)False)(∀ x23 . x22 (x1 x23)False)(∀ x23 . (x2 (x18 x23) x23False)False)((x22 x11False)False)(∀ x23 x24 . x0 (x17 x23 x24) x23(x3 x24 x23False)False)(∀ x23 x24 . (x0 (x17 x23 x24) x24False)(x3 x24 x23False)False)(∀ x23 x24 x25 . x3 x24 x25x0 x23 x24(x0 x23 x25False)False)((x21 = x11False)False)(∀ x23 x24 . (x16 x24 x23 = x23False)(x0 (x16 x24 x23) x24False)(x24 = x10 x23False)False)(∀ x23 x24 . x0 (x16 x24 x23) x24x16 x24 x23 = x23(x24 = x10 x23False)False)(∀ x23 x24 x25 . x24 = x10 x25x23 = x25(x0 x23 x24False)False)(∀ x23 x24 x25 . x24 = x10 x25x0 x23 x24(x23 = x25False)False)(∀ x23 x24 . x24 = x21x23 = x21(x23 = x4 x24False)False)(∀ x23 x24 . x24 = x21x23 = x4 x24(x23 = x21False)False)(∀ x23 x24 x25 . (x25 = x21False)x0 x23 x25(x0 (x15 x24 x25) x23False)(x0 (x15 x24 x25) x24False)(x24 = x4 x25False)False)(∀ x23 x24 . (x24 = x21False)x0 (x15 x23 x24) x23x0 (x15 x23 x24) (x12 x23 x24)(x23 = x4 x24False)False)(∀ x23 x24 . (x24 = x21False)x0 (x15 x23 x24) x23(x0 (x12 x23 x24) x24False)(x23 = x4 x24False)False)(∀ x23 x24 x25 . (x25 = x21False)x23 = x4 x25x0 x24 (x13 x24 x23 x25)(x0 x24 x23False)False)(∀ x23 x24 x25 . (x25 = x21False)x23 = x4 x25(x0 (x13 x24 x23 x25) x25False)(x0 x24 x23False)False)(∀ x23 x24 x25 x26 . (x26 = x21False)x23 = x4 x26x0 x25 x23x0 x24 x26(x0 x25 x24False)False)(∀ x23 x24 . x3 x24 x23x3 x23 x24(x24 = x23False)False)(∀ x23 x24 . x23 = x24(x3 x24 x23False)False)(∀ x23 x24 . x24 = x23(x3 x24 x23False)False)(∀ x23 x24 . x22 x24x2 x23 (x1 x24)x6 x23 x24False)(∀ x23 x24 . (x22 x24False)x2 x23 (x1 x24)x22 x23(x6 x23 x24False)False)(∀ x23 x24 . (x22 x24False)x2 x23 (x1 x24)(x6 x23 x24False)x22 x23False)(∀ x23 x24 . x22 x24x2 x23 (x1 x24)(x22 x23False)False)(∀ x23 x24 . x0 x23 x24x0 x24 x23False)(x4 (x10 x14) = x14False)False
as obj
-
as prop
bf66e..
theory
HotG
stx
e16a9..
address
TMMkh..