計算の例（１）

まず，関数fを
procedure f(x) x^2-2*x
と定義し，「aが関数fの値域に属する」という条件を
rlqe( ex(x,f(x)=a) );
のようにQEすると，RedLogは
a + 1 >= 0
と答えます．また，「点x=aにおいてf(x)が極小となる」という条件を
rlqe( all(p,p>0 impl ex(q,q>0 and all(x,a-q<x<a+q impl f(a)<=f(x)<f(a)+p))) );
のようにQEすると，RedLogは
a - 1 = 0
と答えます．では，「区間0≦x≦aにおけるf(x)の最小値がmである」という条件を
rlqe( ex(x,0<=x<=a and f(x)=m) and all(x,0<=x<=a impl f(x)>=m) );
のようにQEすると，RedLogは何と答えるでしょう？