Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cclwwlk (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . w3a (wne (cv x1) c0) (wral (λ x2 . wcel (cpr (cfv (cv x2) (cv x1)) (cfv (co (cv x2) c1 caddc) (cv x1))) (cfv (cv x0) cedg)) (λ x2 . co cc0 (co (cfv (cv x1) chash) c1 cmin) cfzo)) (wcel (cpr (cfv (cv x1) clsw) (cfv cc0 (cv x1))) (cfv (cv x0) cedg))) (λ x1 . cword (cfv (cv x0) cvtx))))
as obj
-
as prop
89161..
theory
SetMM
stx
83052..
address
TMbsT..