Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cpco (cmpt (λ x0 . ctop) (λ x0 . cmpt2 (λ x1 x2 . co cii (cv x0) ccn) (λ x1 x2 . co cii (cv x0) ccn) (λ x1 x2 . cmpt (λ x3 . co cc0 c1 cicc) (λ x3 . cif (wbr (cv x3) (co c1 c2 cdiv) cle) (cfv (co c2 (cv x3) cmul) (cv x1)) (cfv (co (co c2 (cv x3) cmul) c1 cmin) (cv x2))))))
as obj
-
as prop
527d9..
theory
SetMM
stx
bc3a6..
address
TMb2K..