---

Step * of Lemma qinv-elim

∀[r:ℚ]. (1/r ~ if isint(r) then <1, r> else let p,q = r in <q, p> 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{}].  (1/r  \msim{}  if  isint(r)  then  ə,  r>  else  let  p,q  =  r  in  <q,  p>  fi  )


By

---

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

---

Home Index