---

Step * of Lemma qpositive-elim

∀[r:ℚ]. (qpositive(r) ~ if isint(r) then 0 <z r else let p,q = r in (0 <z p ∧b 0 <z q) ∨b(p <z 0 ∧b q <z 0) fi )
BY
{ ((D 0 THENA Auto) THEN RW (AddrC [1] UnfoldTopAbC) 0 THEN (CallByValueReduce 0 THENA Auto) THEN Try (Trivial)) }

---

Latex:

---

Latex:
\mforall{}[r:\mBbbQ{}]
    (qpositive(r)  \msim{}  if  isint(r)
    then  0  <z  r
    else  let  p,q  =  r 
              in  (0  <z  p  \mwedge{}\msubb{}  0  <z  q)  \mvee{}\msubb{}(p  <z  0  \mwedge{}\msubb{}  q  <z  0)
    fi  )


By

---

Latex:
((D  0  THENA  Auto)
  THEN  RW  (AddrC  [1]  UnfoldTopAbC)  0
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  Try  (Trivial))

---

Home Index