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 . x12 x16 x13x12 x14 x13x12 x15 x13x11 x16 x14x11 x14 x15(x11 x16 x15False)False)(∀ x14 x15 x16 . x12 x16 x13x12 x14 x13x12 x15 x13x16 = x0 x14 x15(x11 x15 x16False)False)(∀ x14 x15 x16 . x12 x16 x13x12 x14 x13x12 x15 x13x11 x16 x14(x0 x15 (x10 x14 x16) = x10 (x0 x15 x14) x16False)False)((x1 = x2False)False)(∀ x14 . (x12 (x9 x14) x14False)False)(∀ x14 x15 . x12 x15 x13x12 x14 x13(x12 (x0 x15 x14) x13False)False)(∀ x14 x15 . x12 x15 x13x12 x14 x13(x12 (x10 x15 x14) x13False)False)((x12 x1 x3False)False)(∀ x14 x15 . x12 x15 x13x12 x14 x13(x11 x14 x15False)(x8 x15 x14 = x7 x1 (x10 x14 x15)False)False)(∀ x14 x15 . x12 x15 x13x12 x14 x13x11 x14 x15(x8 x15 x14 = x10 x15 x14False)False)(∀ x14 x15 . x12 x15 x13x12 x14 x13(x11 x15 x14False)(x11 x14 x15False)False)(∀ x14 x15 . x12 x15 x13x12 x14 x13(x0 x15 x14 = x0 x14 x15False)False)(x0 x4 (x10 x6 x5) = x8 (x0 x4 x6) x5False)((x11 x5 x6False)False)((x12 x4 x13False)False)((x12 x6 x13False)False)((x12 x5 x13False)False)False
as obj
-
as prop
6eafe..
theory
HotG
stx
376db..
address
TMbb4..