Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cpsgn (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . crab (λ x2 . wcel (cdm (cdif (cv x2) cid)) cfn) (λ x2 . cfv (cfv (cv x0) csymg) cbs)) (λ x1 . cio (λ x2 . wrex (λ x3 . wa (wceq (cv x1) (co (cfv (cv x0) csymg) (cv x3) cgsu)) (wceq (cv x2) (co (cneg c1) (cfv (cv x3) chash) cexp))) (λ x3 . cword (crn (cfv (cv x0) cpmtr)))))))
as obj
-
as prop
28633..
theory
SetMM
stx
ac091..
address
TMPow..