---

Step * 1 1 of Lemma normal-p-outcome


1. Σ0 ≤ i < 0. ⊥ = 1 ∈ ℚ@i
2. (∀q∈[].0 ≤ q)@i
⊢ 0 < 0
BY
{ (RWO "sum_unroll_base_q" 1 THEN Auto THEN RWO "int-eq-in-rationals" 1 THEN Auto') }

---

Latex:



1.  \mSigma{}0  \mleq{}  i  <  0.  \mbot{}  =  1@i
2.  (\mforall{}q\mmember{}[].0  \mleq{}  q)@i
\mvdash{}  0  <  0


By

(RWO  "sum\_unroll\_base\_q"  1  THEN  Auto  THEN  RWO  "int-eq-in-rationals"  1  THEN  Auto')

---

Home Index