Proofgold Term Root Disambiguation

∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 : ο . (∀ x3 . x3 ∈ DirGraphOutNeighbors u18 x0 x1 ⟶ ∀ x4 . x4 ⊆ u18 ⟶ ∀ x5 . x5 ⊆ u18 ⟶ ∀ x6 . x6 ⊆ u18 ⟶ ∀ x7 . x7 ⊆ u18 ⟶ x4 = setminus (DirGraphOutNeighbors u18 x0 x1) (Sing x3) ⟶ x6 = setminus (DirGraphOutNeighbors u18 x0 x3) (Sing x1) ⟶ x5 = {x9 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x9) (DirGraphOutNeighbors u18 x0 x1)) u1} ⟶ x7 = setminus {x9 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x9) (DirGraphOutNeighbors u18 x0 x1)) u2} x6 ⟶ (∀ x8 . x8 ∈ u18 ⟶ ∀ x9 : ο . (x8 = x1 ⟶ x9) ⟶ (x8 = x3 ⟶ x9) ⟶ (x8 ∈ x4 ⟶ x9) ⟶ (x8 ∈ x6 ⟶ x9) ⟶ (x8 ∈ x5 ⟶ x9) ⟶ (x8 ∈ x7 ⟶ x9) ⟶ x9) ⟶ (∀ x8 . x8 ∈ x5 ⟶ not (x0 x3 x8)) ⟶ equip x4 u4 ⟶ equip x5 u4 ⟶ equip x6 u4 ⟶ equip x7 u4 ⟶ (∀ x8 . x8 ∈ x6 ⟶ nIn x8 x7) ⟶ (∀ x8 . x8 ∈ x5 ⟶ ∀ x9 : ο . (∀ x10 . and (x10 ∈ x6) (x0 x8 x10) ⟶ x9) ⟶ x9) ⟶ (∀ x8 . x8 ∈ x6 ⟶ not (x0 x1 x8)) ⟶ (∀ x8 . x8 ∈ x6 ⟶ equip (binintersect (DirGraphOutNeighbors u18 x0 x8) (DirGraphOutNeighbors u18 x0 x1)) u2) ⟶ f1360.. x0 u3 x5 ⟶ x2) ⟶ x2

as obj
-

as prop
52c6f..

theory
HotG

stx
493fb..

address
TMEmT..