Proofgold Term Root Disambiguation

∀ x0 : ι → ι → ι → ο . (∀ x1 . d7d78.. c4def.. x1 x1 ⟶ x0 c4def.. x1 x1) ⟶ (∀ x1 x2 x3 x4 x5 . d7d78.. x1 x3 x4 ⟶ x0 x1 x3 x4 ⟶ d7d78.. x2 x4 x5 ⟶ x0 x2 x4 x5 ⟶ x0 (6b90c.. x1 x2) x3 x5) ⟶ (∀ x1 . d7d78.. c9248.. x1 236c6.. ⟶ x0 c9248.. x1 236c6..) ⟶ (∀ x1 x2 x3 . d7d78.. x1 x2 x3 ⟶ x0 x1 x2 x3 ⟶ x0 (a6e19.. x1) x2 (0b8ef.. x3)) ⟶ (∀ x1 x2 x3 . d7d78.. x1 x2 x3 ⟶ x0 x1 x2 x3 ⟶ x0 (2fe34.. x1) x2 (6c5f4.. x3)) ⟶ (∀ x1 x2 x3 x4 x5 . e05e6.. x2 ⟶ d7d78.. x1 (cfc98.. x3 x4) x5 ⟶ x0 x1 (cfc98.. x3 x4) x5 ⟶ x0 (3e00e.. x1 x2) (cfc98.. (0b8ef.. x3) x4) x5) ⟶ (∀ x1 x2 x3 x4 x5 . e05e6.. x1 ⟶ d7d78.. x2 (cfc98.. x3 x4) x5 ⟶ x0 x2 (cfc98.. x3 x4) x5 ⟶ x0 (3e00e.. x1 x2) (cfc98.. (6c5f4.. x3) x4) x5) ⟶ (∀ x1 x2 x3 x4 x5 . d7d78.. x1 x3 x4 ⟶ x0 x1 x3 x4 ⟶ d7d78.. x2 x3 x5 ⟶ x0 x2 x3 x5 ⟶ x0 (f9341.. x1 x2) x3 (cfc98.. x4 x5)) ⟶ (∀ x1 x2 x3 x4 . d7d78.. x1 x2 x4 ⟶ x0 x1 x2 x4 ⟶ x0 (1fa6d.. x1) (cfc98.. x2 x3) x4) ⟶ (∀ x1 x2 x3 x4 . d7d78.. x1 x3 x4 ⟶ x0 x1 x3 x4 ⟶ x0 (3a365.. x1) (cfc98.. x2 x3) x4) ⟶ ∀ x1 x2 x3 . d7d78.. x1 x2 x3 ⟶ x0 x1 x2 x3

as obj
-

as prop
4bdfc..

theory
HOAS

stx
8d75a..

address
TMN9s..