Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cq1p (cmpt (λ x0 . cvv) (λ x0 . csb (cfv (cv x0) cpl1) (λ x1 . csb (cfv (cv x1) cbs) (λ x2 . cmpt2 (λ x3 x4 . cv x2) (λ x3 x4 . cv x2) (λ x3 x4 . crio (λ x5 . wbr (cfv (co (cv x3) (co (cv x5) (cv x4) (cfv (cv x1) cmulr)) (cfv (cv x1) csg)) (cfv (cv x0) cdg1)) (cfv (cv x4) (cfv (cv x0) cdg1)) clt) (λ x5 . cv x2))))))
as obj
-
as prop
21a2d..
theory
SetMM
stx
fc037..
address
TMHo2..