Proofgold Term Root Disambiguation

∀ x0 x1 x2 x3 . nat_p x0 ⟶ (∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . SNo x5 ⟶ SNoLev x5 = x4 ⟶ diadic_rational_p x5) ⟶ SNo x1 ⟶ SNoLev x1 = x0 ⟶ not (diadic_rational_p x1) ⟶ SNo_max_of (SNoL x1) x2 ⟶ SNo x2 ⟶ SNoLev x2 ∈ SNoLev x1 ⟶ SNoLt x2 x1 ⟶ SNo_min_of (SNoR x1) x3 ⟶ SNo x3 ⟶ SNoLev x3 ∈ SNoLev x1 ⟶ SNo (add_SNo x1 x1) ⟶ SNo (add_SNo x2 x3) ⟶ diadic_rational_p x2 ⟶ not (diadic_rational_p x3)

as obj
-

as prop
9e6ca..^{Conj_SNoS_omega_diadic_rational_p_lem__10__12}

theory
HotG

stx
b740c..

address
TMNHE..^{Conj_SNoS_omega_diadic_rational_p_lem__10__12}