Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι . ∀ x3 : ι → ι → ι → ι . ∀ x4 : ι → ι → ι → ι → ι . ∀ x5 : ι → ι → ι → ι → ι → ι . ∀ x6 : ι → ι → ι → ι → ι → ι → ο . ∀ x7 : ι → ι → ι → ι → ι → ι → ι . ∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 (x1 x8)∀ x10 . prim1 x10 (x2 x8 x9)∀ x11 . prim1 x11 (x3 x8 x9 x10)∀ x12 . prim1 x12 (x4 x8 x9 x10 x11)∀ x13 . prim1 x13 (x5 x8 x9 x10 x11 x12)x6 x8 x9 x10 x11 x12 x13prim1 (x7 x8 x9 x10 x11 x12 x13) (6cd44.. x0 x1 x2 x3 x4 x5 x6 x7)
as obj
-
as prop
803ff..
theory
HoTg
stx
336f4..
address
TMKKZ..