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 x2 ⟶ SNoLev x2 ∈ SNoLev x1 ⟶ SNoLt x2 x1 ⟶ SNo_min_of (SNoR x1) x3 ⟶ SNo x3 ⟶ SNoLev x3 ∈ SNoLev x1 ⟶ SNoLt x1 x3 ⟶ SNo (add_SNo x1 x1) ⟶ SNo (add_SNo x2 x3) ⟶ not (diadic_rational_p x2)

type
prop

theory
HotG

name
-

proof
PUTNo..

Megalodon
Conj_SNoS_omega_diadic_rational_p_lem__11__5

proofgold address
TMYDT..^{Conj_SNoS_omega_diadic_rational_p_lem__11__5}

creator
35053 PrNpY../05b23..

owner
35061 PrNpY../ad7d8..

term root
80868..