Search for blocks/addresses/...

Proofgold Term Root Disambiguation

wceq cstrkgb (cab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . w3a (wral (λ x3 . wral (λ x4 . wcel (cv x4) (co (cv x3) (cv x3) (cv x2))wceq (cv x3) (cv x4)) (λ x4 . cv x1)) (λ x3 . cv x1)) (wral (λ x3 . wral (λ x4 . wral (λ x5 . wral (λ x6 . wral (λ x7 . wa (wcel (cv x6) (co (cv x3) (cv x5) (cv x2))) (wcel (cv x7) (co (cv x4) (cv x5) (cv x2)))wrex (λ x8 . wa (wcel (cv x8) (co (cv x6) (cv x4) (cv x2))) (wcel (cv x8) (co (cv x7) (cv x3) (cv x2)))) (λ x8 . cv x1)) (λ x7 . cv x1)) (λ x6 . cv x1)) (λ x5 . cv x1)) (λ x4 . cv x1)) (λ x3 . cv x1)) (wral (λ x3 . wral (λ x4 . wrex (λ x5 . wral (λ x6 . wral (λ x7 . wcel (cv x6) (co (cv x5) (cv x7) (cv x2))) (λ x7 . cv x4)) (λ x6 . cv x3)) (λ x5 . cv x1)wrex (λ x5 . wral (λ x6 . wral (λ x7 . wcel (cv x5) (co (cv x6) (cv x7) (cv x2))) (λ x7 . cv x4)) (λ x6 . cv x3)) (λ x5 . cv x1)) (λ x4 . cpw (cv x1))) (λ x3 . cpw (cv x1)))) (cfv (cv x0) citv)) (cfv (cv x0) cbs)))
as obj
-
as prop
11004..
theory
SetMM
stx
cf00c..
address
TMWgB..