Proofgold Term Root Disambiguation

∀ x0 . In x0 5 ⟶ ∀ x1 . In x1 5 ⟶ ∀ x2 . In x2 5 ⟶ ∀ x3 . In x3 5 ⟶ ∀ x4 . In x4 5 ⟶ ∀ x5 . In x5 5 ⟶ ∀ x6 . In x6 5 ⟶ ∀ x7 . In x7 5 ⟶ ∀ x8 . In x8 5 ⟶ ∀ x9 . In x9 5 ⟶ ∀ x10 . In x10 5 ⟶ ∀ x11 . In x11 5 ⟶ ∀ x12 . In x12 5 ⟶ ∀ x13 . In x13 5 ⟶ ∀ x14 . In x14 5 ⟶ ∀ x15 . In x15 5 ⟶ ∀ x16 . In x16 5 ⟶ ∀ x17 . In x17 5 ⟶ ∀ x18 . In x18 5 ⟶ ∀ x19 . In x19 5 ⟶ ∀ x20 . In x20 5 ⟶ ∀ x21 . In x21 5 ⟶ ∀ x22 . In x22 5 ⟶ ∀ x23 . In x23 5 ⟶ ∀ x24 . In x24 5 ⟶ binop_on 5 (a80b3.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24)

as obj
-

as prop
25bf5..^{binop_table_on_5}

theory
HF

stx
1efa1..

address
TMVmM..^{binop_table_on_5}