Proofgold Term Root Disambiguation

∀ x0 . In x0 3 ⟶ ∀ x1 . In x1 3 ⟶ ∀ x2 . In x2 3 ⟶ ∀ x3 . In x3 3 ⟶ ∀ x4 . In x4 3 ⟶ ∀ x5 . In x5 3 ⟶ ∀ x6 . In x6 3 ⟶ ∀ x7 . In x7 3 ⟶ ∀ x8 . In x8 3 ⟶ binop_on 3 (17ce0.. x0 x1 x2 x3 x4 x5 x6 x7 x8)

as obj
-

as prop
479d5..^{binop_table_on_3}

theory
HF

stx
1efa1..

address
TMRDe..^{binop_table_on_3}