Search for blocks/addresses/...

Proofgold Proposition

∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . ∀ x6 : ι → ι → ι . 62ee1.. x0 x1 x2 x3 x4 x5(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0∀ x10 . prim1 x10 x0x6 x7 x8 = x6 x9 x10and (x7 = x9) (x8 = x10))∀ x7 . prim1 x7 (3b429.. x0 (λ x8 . x0) (λ x8 x9 . True) x6)(x7 = x6 x1 x1∀ x8 : ο . x8)∀ x8 : ο . (∀ x9 . and (prim1 x9 (3b429.. x0 (λ x10 . x0) (λ x10 x11 . True) x6)) (x6 (x3 (x4 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x7 = x6 x11 x13)x12)x12))) (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x9 = x6 x11 x13)x12)x12)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x11 . and (prim1 x11 x0) (x7 = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x7 = x6 x13 x15)x14)x14))) x11))) (prim0 (λ x11 . and (prim1 x11 x0) (x9 = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x9 = x6 x13 x15)x14)x14))) x11)))))) (x3 (x4 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x7 = x6 x11 x13)x12)x12))) (prim0 (λ x11 . and (prim1 x11 x0) (x9 = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x9 = x6 x13 x15)x14)x14))) x11)))) (x4 (prim0 (λ x11 . and (prim1 x11 x0) (x7 = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x7 = x6 x13 x15)x14)x14))) x11))) (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x9 = x6 x11 x13)x12)x12))))) = x6 x2 x1)x8)x8
type
prop
theory
HoTg
name
-
proof
PUbuw..
Megalodon
-
proofgold address
TMbDg..
creator
3882 PrGxv../afc18..
owner
3882 PrGxv../afc18..
term root
0895a..