---

Step * of Lemma qeq-elim

∀[r,s:ℚ].
  (qeq(r;s) ~ if isint(r)
  then if isint(s) then (r =z s) else let i,j = s in (r * j =z i) fi 
  else let p,q = r 
       in if isint(s) then (p =z s * q) else let i,j = s in (p * j =z i * q) fi 
  fi )
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN RW (AddrC [1] UnfoldTopAbC) 0
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[r,s:\mBbbQ{}].
    (qeq(r;s)  \msim{}  if  isint(r)
    then  if  isint(s)  then  (r  =\msubz{}  s)  else  let  i,j  =  s  in  (r  *  j  =\msubz{}  i)  fi 
    else  let  p,q  =  r 
              in  if  isint(s)  then  (p  =\msubz{}  s  *  q)  else  let  i,j  =  s  in  (p  *  j  =\msubz{}  i  *  q)  fi 
    fi  )


By

---

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

---

Home Index