Search for blocks/addresses/...

Proofgold Proposition

∀ 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 . In x3 x0∀ x4 . In x4 x0∀ x5 : ι → ι → ι . (∀ x6 . In x6 x0∀ x7 . In x7 x0In (x5 x6 x7) x0)∀ x6 : ι → ι → ι . (∀ x7 . In x7 x0∀ x8 . In x8 x0In (x6 x7 x8) x0)∀ x7 . In x7 x0∀ x8 : ι → ι → ι . (∀ x9 . In x9 x0∀ x10 . In x10 x0In (x8 x9 x10) x0)(∀ x9 . In x9 x0(x8 x7 x9 = x9False)False)(∀ x9 . In x9 x0(x8 x9 x7 = x9False)False)(∀ x9 . In x9 x0∀ x10 . In x10 x0(x6 x9 (x8 x9 x10) = x10False)False)(∀ x9 . In x9 x0∀ x10 . In x10 x0(x8 x9 (x6 x9 x10) = x10False)False)(∀ x9 . In x9 x0∀ x10 . In x10 x0∀ x11 . In x11 x0x8 x9 x10 = x8 x9 x11(x10 = x11False)False)(∀ x9 . In x9 x0∀ x10 . In x10 x0(x1 x9 x10 = x8 (x6 x9 x10) (x6 (x6 x9 x7) x7)False)False)(∀ x9 . In x9 x0(x6 x7 x9 = x9False)False)(∀ x9 . In x9 x0(x6 x9 x9 = x7False)False)(∀ x9 . In x9 x0(x5 x7 x9 = x9False)False)(∀ x9 . In x9 x0∀ x10 . In x10 x0(x2 x7 x9 x10 = x10False)False)(∀ x9 . In x9 x0∀ x10 . In x10 x0∀ x11 . In x11 x0(x2 x9 x10 (x5 x9 (x1 x10 (x2 x9 x10 (x5 x9 (x1 x10 x11))))) = x11False)False)(∀ x9 . In x9 x0∀ x10 . In x10 x0∀ x11 . In x11 x0∀ x12 . In x12 x0(x2 x9 x11 (x1 x10 (x1 x9 (x2 x11 x10 (x2 x9 x11 (x1 x10 (x1 x9 (x2 x11 x10 (x2 x9 x11 (x1 x10 (x1 x9 (x2 x11 x10 x12))))))))))) = x12False)False)(x8 x3 x4 = x8 x4 x3False)False
type
prop
theory
HF
name
-
proof
PULXW..
Megalodon
-
proofgold address
TMRei..
creator
11752 PrGVS../bab3d..
owner
11752 PrGVS../bab3d..
term root
7bede..