Proofgold Term Root Disambiguation

∀ x0 . x0 ∈ setexp real omega ⟶ ∀ x1 . x1 ∈ setexp real omega ⟶ (∀ x2 . x2 ∈ omega ⟶ and (and (SNoLe (ap x0 x2) (ap x1 x2)) (SNoLe (ap x0 x2) (ap x0 (ordsucc x2)))) (SNoLe (ap x1 (ordsucc x2)) (ap x1 x2))) ⟶ ∃ x2 . and (x2 ∈ real) (∀ x4 . x4 ∈ omega ⟶ and (SNoLe (ap x0 x4) x2) (SNoLe x2 (ap x1 x4)))

as obj
-

as prop
96392..^{real_complete1}

theory
HotG

stx
c59bb..

address
TMPoi..^{real_complete1}