Proofgold Term Root Disambiguation

∀ x0 . x0 ∈ int ⟶ ∀ x1 . x1 ∈ int ⟶ not (and (x0 = 0) (x1 = 0)) ⟶ ∃ x2 . and (and (int_lin_comb x0 x1 x2) (SNoLt 0 x2)) (∀ x4 . int_lin_comb x0 x1 x4 ⟶ SNoLt 0 x4 ⟶ SNoLe x2 x4)

as obj
-

as prop
3821b..^{least_pos_int_lin_comb_ex}

theory
HotG

stx
e9e67..

address
TMcf4..^{least_pos_int_lin_comb_ex}