---

Step * of Lemma runop_wf

∀[op:ℤ]. ∀[p:ℝ].
  (runop(op;p) ∈ ℝ) supposing 
     (((op = 5 ∈ ℤ) ⇒ (r0 < p)) and 
     ((op = 6 ∈ ℤ) ⇒ (p ∈ (r(-1), r1))) and 
     ((op = 9 ∈ ℤ) ⇒ (r1 ≤ p)) and 
     ((op = 11 ∈ ℤ) ⇒ p ≠ r0) and 
     ((op = 12 ∈ ℤ) ⇒ ((-(π/2) < p) ∧ (p < π/2))))
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[op:\mBbbZ{}].  \mforall{}[p:\mBbbR{}].
    (runop(op;p)  \mmember{}  \mBbbR{})  supposing 
          (((op  =  5)  {}\mRightarrow{}  (r0  <  p))  and 
          ((op  =  6)  {}\mRightarrow{}  (p  \mmember{}  (r(-1),  r1)))  and 
          ((op  =  9)  {}\mRightarrow{}  (r1  \mleq{}  p))  and 
          ((op  =  11)  {}\mRightarrow{}  p  \mneq{}  r0)  and 
          ((op  =  12)  {}\mRightarrow{}  ((-(\mpi{}/2)  <  p)  \mwedge{}  (p  <  \mpi{}/2))))


By

---

Latex:
ProveWfLemma

---

Home Index