QE で極限

　今回は極限のお話です．
　よく知られた CAS（計算機代数システム）には極限を求めるコマンドが実装されており，例えば
\lim_{x\to a}\frac{1}{x}
を得るには，Reduce では

limit( 1/x , x , a ) ;

Mathematica では

Limit[ 1/x , x -> a ]

Maple では

limit( 1/x , x = a ) ;

maxima では

limit( 1/x , x , a ) ;

とすればよく，何れも 1/a と出力されます（幾つかのシステムでは分数関数が現れた際にその分母が 0 でないことを仮定に加えるスイッチがデフォルトでオンになっています）．
　これに対して我々は，コーシー流のイプシロンデルタ論法による極限の定義を QE することで直接に結果を得ることにします．すなわち，複素数 a の近くで定義された（ a で定義されていなくてもよい ）複素数値関数 f と複素数 b について
\lim_{x\to a}f(x)=b
とは

∀ p ( p ＞ 0 → ∃ q ( q ＞ 0 ∧ ∀ x ( 0 ＜|x-a|＜ q → |f(x)-b| ＜ p ) ) )

ということでしたから，RedLog で分数関数が扱えるように

on rlnzden,rladdcond;

とした後
\lim_{x\to a}\frac{1}{x}=b
を

rlqepcad(
　all( p, p > 0 impl
　ex( q, q > 0 and all( x, -q < x-a < q impl -p < 1/x-b < p ) )
　)
);

のように QE すれば，QEPCAD B は

a*b - 1 = 0

と答えます．