Proofgold Proposition

∀ 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)

type
prop

theory
HotG

name
-

proof
PUTNo..

Megalodon
Conj_SNoS_omega_diadic_rational_p_lem__10__12

proofgold address
TMUiB..^{Conj_SNoS_omega_diadic_rational_p_lem__10__12}

creator
35053 PrNpY../a32e5..

owner
35061 PrNpY../6aadf..

term root
ce518..