Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cxad (cmpt2 (λ x0 x1 . cxr) (λ x0 x1 . cxr) (λ x0 x1 . cif (wceq (cv x0) cpnf) (cif (wceq (cv x1) cmnf) cc0 cpnf) (cif (wceq (cv x0) cmnf) (cif (wceq (cv x1) cpnf) cc0 cmnf) (cif (wceq (cv x1) cpnf) cpnf (cif (wceq (cv x1) cmnf) cmnf (co (cv x0) (cv x1) caddc))))))
as obj
-
as prop
b4eef..
theory
SetMM
stx
33c8c..
address
TMcMa..