---

Step * of Lemma qmul-elim

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