Proofgold Term Root Disambiguation

∀ x0 : ι → ι → ο . x0 0 u2 ⟶ x0 u4 u6 ⟶ x0 u1 u12 ⟶ x0 u5 u12 ⟶ x0 u8 u12 ⟶ x0 u9 u12 ⟶ x0 u3 u13 ⟶ x0 u7 u13 ⟶ x0 u10 u13 ⟶ x0 u2 u14 ⟶ x0 u6 u14 ⟶ x0 u11 u14 ⟶ x0 0 u15 ⟶ x0 u4 u15 ⟶ x0 0 u2 ⟶ x0 u4 u6 ⟶ x0 u11 u15 ⟶ ∀ x1 . x1 ⊆ u16 ⟶ atleastp u6 x1 ⟶ u12 ∈ x1 ⟶ u13 ∈ x1 ⟶ (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ not (x0 x2 x3)) ⟶ False

as obj
-

as prop
27d0c..

theory
HotG

stx
fe913..

address
TMaUG..