Search for blocks/addresses/...

Proofgold Term Root Disambiguation

λ x0 x1 . prim0 (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x3 x3) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x2) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x3) (prim0 x2 x3))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x3 x2) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x3 x2)) (prim0 (prim0 x2 x2) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x3) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x3) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x2) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x3) (prim0 x3 x3))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x2) (prim0 x3 x3))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x3) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x3 x3) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x3) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x2) (prim0 x3 x3))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x2 x3) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x3 x2)) (prim0 (prim0 x2 x2) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x3 x3) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x2) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x2) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x3) (prim0 x3 x3))))) (prim1 (λ x2 . x2)))))))))))))))))))))) (prim0 x0 x1)
as obj
6b90c..
as prop
-
theory
HOAS
stx
cbccf..
address
TMZCc..