Proofgold Term Root Disambiguation

∀ x0 x1 x2 x3 x4 x5 x6 . SNo x0 ⟶ SNo x1 ⟶ SNo (mul_SNo x0 x1) ⟶ SNo (minus_SNo (mul_SNo x0 x1)) ⟶ SNo x2 ⟶ SNoLt (mul_SNo x0 x1) x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNoLe (add_SNo (mul_SNo x3 x1) (mul_SNo x0 x4)) (add_SNo x2 (mul_SNo x3 x4)) ⟶ SNo (mul_SNo x0 x4) ⟶ SNo (mul_SNo x3 x4) ⟶ SNo (minus_SNo (mul_SNo x3 x4)) ⟶ SNo (add_SNo x0 (minus_SNo x3)) ⟶ SNo (add_SNo x4 (minus_SNo x1)) ⟶ x5 ∈ omega ⟶ SNoLe (eps_ x5) (add_SNo x0 (minus_SNo x3)) ⟶ x6 ∈ omega ⟶ SNoLe (eps_ x6) (add_SNo x4 (minus_SNo x1)) ⟶ SNo (eps_ x5) ⟶ SNo (eps_ x6) ⟶ SNo (eps_ (add_SNo x5 x6)) ⟶ SNo (mul_SNo (eps_ x5) (eps_ x6)) ⟶ SNoLt (abs_SNo (add_SNo x2 (minus_SNo (mul_SNo x0 x1)))) (eps_ (add_SNo x5 x6)) ⟶ not (SNoLe (eps_ (add_SNo x5 x6)) (abs_SNo (add_SNo x2 (minus_SNo (mul_SNo x0 x1)))))

as obj
-

as prop
09057..^{Conj_real_mul_SNo_pos__14__9}

theory
HotG

stx
b740c..

address
TMa9o..^{Conj_real_mul_SNo_pos__14__9}