Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . In x2 x0∀ x3 . In x3 x0In (x1 x2 x3) x0)∀ x2 : ι → ι → ι → ι . (∀ x3 . In x3 x0∀ x4 . In x4 x0∀ x5 . In x5 x0In (x2 x3 x4 x5) x0)∀ x3 : ι → ι → ι . (∀ x4 . In x4 x0∀ x5 . In x5 x0In (x3 x4 x5) x0)∀ x4 : ι → ι → ι . (∀ x5 . In x5 x0∀ x6 . In x6 x0In (x4 x5 x6) x0)∀ x5 . In x5 x0∀ x6 . In x6 x0∀ x7 . In x7 x0∀ x8 : ι → ι → ι → ι . (∀ x9 . In x9 x0∀ x10 . In x10 x0∀ x11 . In x11 x0In (x8 x9 x10 x11) x0)∀ x9 : ι → ι → ι . (∀ x10 . In x10 x0∀ x11 . In x11 x0In (x9 x10 x11) x0)∀ x10 . In x10 x0∀ x11 : ι → ι → ι . (∀ x12 . In x12 x0∀ x13 . In x13 x0In (x11 x12 x13) x0)(∀ x12 . In x12 x0(x11 x10 x12 = x12False)False)(∀ x12 . In x12 x0∀ x13 . In x13 x0(x1 x12 (x11 x12 x13) = x13False)False)(∀ x12 . In x12 x0∀ x13 . In x13 x0(x11 x12 (x1 x12 x13) = x13False)False)(∀ x12 . In x12 x0∀ x13 . In x13 x0∀ x14 . In x14 x0(x2 x12 x13 x14 = x1 (x11 x13 x12) (x11 x13 (x11 x12 x14))False)False)(∀ x12 . In x12 x0(x9 x10 x12 = x12False)False)(∀ x12 . In x12 x0(x3 x10 x12 = x12False)False)(∀ x12 . In x12 x0∀ x13 . In x13 x0(x8 x12 x10 x13 = x13False)False)(∀ x12 . In x12 x0∀ x13 . In x13 x0∀ x14 . In x14 x0∀ x15 . In x15 x0(x2 x12 x14 (x3 x13 (x4 x12 (x8 x14 x13 (x2 x12 x14 (x3 x13 (x4 x12 (x8 x14 x13 (x2 x12 x14 (x3 x13 (x4 x12 (x8 x14 x13 x15))))))))))) = x15False)False)(∀ x12 . In x12 x0∀ x13 . In x13 x0∀ x14 . In x14 x0∀ x15 . In x15 x0(x2 x12 x14 (x9 x13 (x4 x12 (x8 x14 x13 (x2 x12 x14 (x9 x13 (x4 x12 (x8 x14 x13 (x2 x12 x14 (x9 x13 (x4 x12 (x8 x14 x13 (x2 x12 x14 (x9 x13 (x4 x12 (x8 x14 x13 x15))))))))))))))) = x15False)False)(x11 (x11 x5 x6) x7 = x11 x5 (x11 x6 x7)False)False
as obj
-
as prop
65348..
theory
HF
stx
2a83e..
address
TMHAK..