Search for blocks/addresses/...

Proofgold Proposition

∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 . ∀ x3 x4 : ι → ι → ο . x4 (3fa3a.. (pack_r x0 x1) (pack_r x2 x3)) (pack_r (setsum x0 x2) (λ x5 x6 . or (and (and (x5 = Inj0 (Unj x5)) (x6 = Inj0 (Unj x6))) (x1 (Unj x5) (Unj x6))) (and (and (x5 = Inj1 (Unj x5)) (x6 = Inj1 (Unj x6))) (x3 (Unj x5) (Unj x6)))))x4 (pack_r (setsum x0 x2) (λ x5 x6 . or (and (and (x5 = Inj0 (Unj x5)) (x6 = Inj0 (Unj x6))) (x1 (Unj x5) (Unj x6))) (and (and (x5 = Inj1 (Unj x5)) (x6 = Inj1 (Unj x6))) (x3 (Unj x5) (Unj x6))))) (3fa3a.. (pack_r x0 x1) (pack_r x2 x3))
type
prop
theory
HotG
name
-
proof
PUVXG..
Megalodon
-
proofgold address
TMXVG..
creator
11733 PrEBh../7ef3c..
owner
11733 PrEBh../7ef3c..
term root
2b21d..