Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq csymg (cmpt (λ x0 . cvv) (λ x0 . csb (cab (λ x1 . wf1o (cv x0) (cv x0) (cv x1))) (λ x1 . ctp (cop (cfv cnx cbs) (cv x1)) (cop (cfv cnx cplusg) (cmpt2 (λ x2 x3 . cv x1) (λ x2 x3 . cv x1) (λ x2 x3 . ccom (cv x2) (cv x3)))) (cop (cfv cnx cts) (cfv (cxp (cv x0) (csn (cpw (cv x0)))) cpt)))))
as obj
-
as prop
ff2b2..
theory
SetMM
stx
ac091..
address
TML4x..