人間が考えると

昨日の最後の結果は，例えば
0≦a≦1のときm=a^2-2a，1＜aのときm=-1
となりますが
f1:=rlqe( ex(x,0<=x<=a and f(x)=m) and all(x,0<=x<=a impl f(x)>=m) );
と入力すると，RedLogは
f1 := m + 1 >= 0 and (a**2 - 2*a - m >= 0 and a - 1 >= 0 and (m + 1 = 0 or a**2 - 2*a - m > 0 and a - 1 = 0) or m <= 0 and (a**2 - 2*a - m <= 0 or a - 1 >= 0) and (m + 1 = 0 or (a**2 - 2*a - m <= 0 or a - 1 <= 0) and (a**2 - 2*a - m <> 0 or a - 1 < 0))) and (a**2 - 2*a - m >= 0 and a - 1 >= 0 or m <= 0 and (a**2 - 2*a - m <= 0 or a - 1 >= 0) and (a**2 - 2*a - m >= 0 or a < 0)) and (a**2 - 2*a - m >= 0 and a - 1 >= 0 or m <= 0 and (a**2 - 2*a - m <= 0 or a - 1 >= 0))
と答えます．
　申し遅れましたが，１階述語論理を扱うCASでは
・Quantifier Elimination（QE，量化子の消去）
・Simplification（簡約）
が２大テーマであり，現時点で後者について満足のいくレベルに達しているのは，Mathematicaと専用システムのQEPCAD（http://www.usna.edu/Users/cs/qepcad/B/QEPCAD.html）だけです．RedLogはこの２者に比べ，QE(rlqe)では高速なこともありますが，簡約についてはご覧の通りです．
　よって，ここでは上の結果を吟味するため，まず最初に書いた人間の結果を
f2:=(0<=a<=1 and m=a^2-2*a) or (1<a and m=-1);
と式に直し，f1，f2の同値性をRedLog自身に
rlqe( all({a,m},f1 equiv f2) );
のように判定させると，RedLogは
true
と答えます．なお，変数が多いときには，all({a,m}の代わりに全称閉包をとって，rlall(とするのが便利です．