---

Step * of Lemma qadd-elim

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