Search for blocks/addresses/...

Proofgold Proposition

wceq csmu (cmpt2 (λ x0 x1 . cpw cn0) (λ x0 x1 . cpw cn0) (λ x0 x1 . crab (λ x2 . wcel (cv x2) (cfv (co (cv x2) c1 caddc) (cseq (cmpt2 (λ x3 x4 . cpw cn0) (λ x3 x4 . cn0) (λ x3 x4 . co (cv x3) (crab (λ x5 . wa (wcel (cv x4) (cv x0)) (wcel (co (cv x5) (cv x4) cmin) (cv x1))) (λ x5 . cn0)) csad)) (cmpt (λ x3 . cn0) (λ x3 . cif (wceq (cv x3) cc0) c0 (co (cv x3) c1 cmin))) cc0))) (λ x2 . cn0)))
type
prop
theory
SetMM
name
df_smu
proof
PUQy1..
Megalodon
-
proofgold address
TMZTU..
creator
36378 PrCmT../73a90..
owner
36378 PrCmT../73a90..
term root
29a19..