Proofgold Term Root Disambiguation

∀ x0 . In x0 4 ⟶ ∀ x1 . In x1 4 ⟶ ∀ x2 . In x2 4 ⟶ ∀ x3 . In x3 4 ⟶ ∀ x4 . In x4 4 ⟶ ∀ x5 . In x5 4 ⟶ ∀ x6 . In x6 4 ⟶ ∀ x7 . In x7 4 ⟶ ∀ x8 . In x8 4 ⟶ ∀ x9 . In x9 4 ⟶ ∀ x10 . In x10 4 ⟶ ∀ x11 . In x11 4 ⟶ ∀ x12 . In x12 4 ⟶ ∀ x13 . In x13 4 ⟶ ∀ x14 . In x14 4 ⟶ ∀ x15 . In x15 4 ⟶ binop_on 4 (44bc7.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)

as obj
-

as prop
d1a06..^{binop_table_on_4}

theory
HF

stx
1efa1..

address
TMc41..^{binop_table_on_4}