Proofgold Term Root Disambiguation

wceq csrg (crab (λ x0 . wa (wcel (cfv (cv x0) cmgp) cmnd) (wsbc (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wsbc (λ x4 . wral (λ x5 . wa (wral (λ x6 . wral (λ x7 . wa (wceq (co (cv x5) (co (cv x6) (cv x7) (cv x2)) (cv x3)) (co (co (cv x5) (cv x6) (cv x3)) (co (cv x5) (cv x7) (cv x3)) (cv x2))) (wceq (co (co (cv x5) (cv x6) (cv x2)) (cv x7) (cv x3)) (co (co (cv x5) (cv x7) (cv x3)) (co (cv x6) (cv x7) (cv x3)) (cv x2)))) (λ x7 . cv x1)) (λ x6 . cv x1)) (wa (wceq (co (cv x4) (cv x5) (cv x3)) (cv x4)) (wceq (co (cv x5) (cv x4) (cv x3)) (cv x4)))) (λ x5 . cv x1)) (cfv (cv x0) c0g)) (cfv (cv x0) cmulr)) (cfv (cv x0) cplusg)) (cfv (cv x0) cbs))) (λ x0 . ccmn))

as obj
-

as prop
fbe9e..

theory
SetMM

stx
9edd3..

address
TMXys..