maximaのロジックシステム（６）

　http://d.hatena.ne.jp/ehito/20140506/1399341060 で述べた「分母≠0の付帯」という慣習を実装したCASはあるのでしょうか？　例えば，Mathematicaは

In[1]:= Reduce[ForAll[{x, y, z}, y == z/x, Not[x == 0]], Reals]
Out[1]= True

In[2]:= Reduce[ForAll[{x, y}, y == x/x, Not[x == 0]], Reals]
Out[2]= False

In[3]:= Reduce[ForAll[{x, y}, y == 0/x, Not[x == 0]], Reals]
Out[3]= False

と返し，RedLog/REDUCE(on rlnzden,rladdcond)，Mapleも同様です．原因はロジック以前に，x/x，0/xがそれぞれ1，0に，一般には(k*x)/xがkにsimplifyされるからであり，これを制止するには，Mathematicaの場合，Hold，Unevaluatedとの合成といった手があるわけですが，これでは約分以外の処理も進みません．

　ではどうするか．．．maxima上で実装してみました．

adddm(f):=block([dmX,dmY],
  if atom(f) then return(f),
  if is(op(f)="/") then 
    (part(f,1)+dmX^2-1+(1-dmX)*(1+dmX))
   /(part(f,2)+dmY+dmY/part(f,2)-dmY*(1+1/part(f,2))) else f)$
SF():=simp:false$
nzden(f):=block([g:scanmap(adddm,f,bottomup)],simp:true,qe([],g))$
nzdenqe(l,f):=block([g:scanmap(adddm,f,bottomup)],simp:true,qe(l,g))$

入力例．SF()$nzdenが関数名だと思って下さい．

SF()$nzden(y=x/x);
SF()$nzden(x=x^2/x);
SF()$nzden((1/a+1/b)*(a*b)/(a+b)=((1-x)*(1-x))/(1-x)+(1+x)/((1+x)*(1+x^2))+c);

SF()$nzden(f=1/(x/y));
SF()$nzden(f=1/(x/(y/z)));
SF()$nzden(f=1/(1+x/(y/z)));
SF()$nzden(f=1/(x/(y/(z/w))));
SF()$nzden(f=1/(1+x/(1+y/(1+z/w))));
SF()$nzden(f=(x/y)/(x/y));
SF()$nzden(f=(x/y)/(z/w));

SF()$nzden(y=0/x);
SF()$nzden((0<=x^4/x)%eq(0<x));
SF()$nzden(0/(1-x)<1/x);

qe([[A,x]],(a<=x^2/x) %eq (b<x));
SF()$nzdenqe([[A,x]],(a<=x^2/x) %eq (b<x));

SF()$f:nzden(a<=x^2/x)$
qe([[A,a],[A,b]], qe([[A,x]],(f) %eq (b<x)) %eq ((a=0) %and (b=0)));
kill(f)$