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 : ι → ι → ι → ι . ∀ x26 . ∀ x27 : ι → ι . ∀ x28 : ι → ο . ∀ x29 x30 : ι → ι . ∀ x31 x32 . ∀ x33 : ι → ο . ∀ x34 x35 x36 . ∀ x37 : ι → ο . ∀ x38 : ι → ι → ι . ∀ x39 : ι → ι → ο . ∀ x40 : ι → ι → ι . ∀ x41 . (∀ x42 x43 . x43 = x41(x40 x42 x43 = x41False)False)(∀ x42 x43 . x43 = x41(x40 x43 x42 = x41False)False)(∀ x42 x43 . x40 x42 x43 = x41(x42 = x41False)(x43 = x41False)False)(∀ x42 x43 . x0 x43(x43 = x42False)x0 x42False)(∀ x42 x43 x44 x45 . x39 x44 x45x39 x43 x42(x39 (x38 x44 x43) (x40 x45 x42)False)False)(∀ x42 x43 x44 x45 . x39 (x38 x43 x45) (x40 x42 x44)(x39 x45 x44False)False)(∀ x42 x43 x44 x45 . x39 (x38 x45 x43) (x40 x44 x42)(x39 x45 x44False)False)(∀ x42 x43 . x39 x42 x43x0 x43False)(∀ x42 . x0 x42(x42 = x41False)False)(∀ x42 x43 . x1 x42 x43(x0 x43False)(x39 x42 x43False)False)(∀ x42 x43 . x39 x43 x42(x1 x43 x42False)False)((x2 x3False)False)(x0 x3False)(x4 x5False)((x37 x5False)False)((x6 x5False)False)((x37 x36False)False)((x7 x36False)False)((x6 x36False)False)(x0 x36False)((x37 x35False)False)((x7 x35False)False)((x6 x35False)False)(x0 x8False)((x7 x34False)False)((x6 x34False)False)((x33 x32False)False)((x37 x32False)False)((x6 x32False)False)((x9 x10False)False)((x0 x31False)False)((x6 x11False)False)(x0 x11False)((x37 x12False)False)((x6 x12False)False)(∀ x42 . (x0 x42False)x6 x42x0 (x13 x42)False)(∀ x42 . (x0 x42False)x6 x42x0 (x30 x42)False)(∀ x42 x43 x44 x45 . (x6 (x14 (x38 x43 x42) (x38 x45 x44))False)False)(∀ x42 x43 . (x6 (x40 x42 x43)False)False)(∀ x42 . x0 x42(x0 (x13 x42)False)False)(∀ x42 x43 . (x6 (x29 (x38 x43 x42))False)False)(∀ x42 . x0 x42(x0 (x30 x42)False)False)(∀ x42 x43 . x0 (x14 x42 x43)False)(∀ x42 . x0 (x29 x42)False)(∀ x42 . x28 x42x6 x42(x28 (x13 x42)False)False)(∀ x42 . x28 x42x6 x42(x28 (x30 x42)False)False)(∀ x42 x43 . (x9 (x38 x42 x43)False)False)((x0 x41False)False)(∀ x42 x43 . (x37 (x29 (x38 x43 x42))False)False)(∀ x42 . (x28 x42False)x6 x42x37 x42x28 (x30 x42)False)(∀ x42 x43 . x6 x43x37 x43x6 x42x37 x42(x2 (x14 x43 x42)False)False)(∀ x42 . x6 x42x37 x42(x2 (x29 x42)False)False)(∀ x42 . x6 x42x37 x42(x4 x42False)x28 (x13 x42)False)(∀ x42 . x6 x42x37 x42x4 x42(x28 (x13 x42)False)False)(∀ x42 . x0 x42(x0 (x13 x42)False)False)(∀ x42 x43 . (x0 x43False)(x0 x42False)x0 (x40 x43 x42)False)(∀ x42 . x0 x42(x0 (x30 x42)False)False)(∀ x42 . x6 x42x7 x42x37 x42(x15 (x13 x42)False)False)(∀ x42 . (x1 (x27 x42) x42False)False)(∀ x42 . (x1 (x16 x42) x42False)False)((x0 x26False)False)(∀ x42 x43 . (x38 x43 x42 = x14 (x14 x43 x42) (x29 x43)False)False)((x41 = x26False)False)(∀ x42 x43 . (x39 (x38 (x18 x43 x42) (x17 x43 x42)) x42False)(x39 (x17 x43 x42) x43False)(x43 = x13 x42False)False)(∀ x42 x43 x44 . x39 (x17 x44 x43) x44x39 (x38 x42 (x17 x44 x43)) x43(x44 = x13 x43False)False)(∀ x42 x43 x44 x45 . x44 = x13 x45x39 (x38 x43 x42) x45(x39 x42 x44False)False)(∀ x42 x43 x44 . x43 = x13 x44x39 x42 x43(x39 (x38 (x25 x42 x43 x44) x42) x44False)False)(∀ x42 x43 . (x39 (x38 (x19 x43 x42) (x20 x43 x42)) x42False)(x39 (x19 x43 x42) x43False)(x43 = x30 x42False)False)(∀ x42 x43 x44 . x39 (x19 x44 x43) x44x39 (x38 (x19 x44 x43) x42) x43(x44 = x30 x43False)False)(∀ x42 x43 x44 x45 . x44 = x30 x45x39 (x38 x42 x43) x45(x39 x42 x44False)False)(∀ x42 x43 x44 . x43 = x30 x44x39 x42 x43(x39 (x38 x42 (x24 x42 x43 x44)) x44False)False)(∀ x42 x43 . (x14 x43 x42 = x14 x42 x43False)False)(∀ x42 x43 . x2 x43x1 x42 x43(x37 x42False)False)(∀ x42 x43 . x2 x43x1 x42 x43(x6 x42False)False)(∀ x42 . x0 x42(x2 x42False)False)(∀ x42 . x28 x42x6 x42x37 x42(x4 x42False)False)(∀ x42 . x28 x42x6 x42x37 x42(x37 x42False)False)(∀ x42 . x28 x42x6 x42x37 x42(x6 x42False)False)(∀ x42 . x6 x42x37 x42(x4 x42False)(x37 x42False)False)(∀ x42 . x6 x42x37 x42(x4 x42False)(x6 x42False)False)(∀ x42 . x6 x42x37 x42(x4 x42False)x28 x42False)(∀ x42 . x0 x42x6 x42(x7 x42False)False)(∀ x42 . x0 x42x6 x42(x6 x42False)False)(∀ x42 . x0 x42x6 x42x37 x42(x4 x42False)False)(∀ x42 . x0 x42x6 x42x37 x42(x37 x42False)False)(∀ x42 . x0 x42x6 x42x37 x42(x6 x42False)False)(∀ x42 . x0 x42x6 x42(x23 x42False)False)(∀ x42 . x0 x42x6 x42(x6 x42False)False)(∀ x42 . x0 x42x6 x42x37 x42(x33 x42False)False)(∀ x42 . x0 x42x6 x42x37 x42(x37 x42False)False)(∀ x42 . x0 x42x6 x42x37 x42(x6 x42False)False)(∀ x42 . x0 x42(x6 x42False)False)(∀ x42 . x0 x42(x37 x42False)False)(∀ x42 x43 . x39 x42 x43x39 x43 x42False)(x30 (x40 x22 x21) = x22x13 (x40 x21 x22) = x22False)(x21 = x41x40 x22 x21 = x41x40 x21 x22 = x41False)False
as obj
-
as prop
2b798..
theory
HotG
stx
c4a0d..
address
TMbfQ..