simplifier

を合成すればより簡単な式が得られるだろうと期待しつつ，rlitab，rlgsn，rldnfの異なる２つ，異なる３つ，それぞれ６通りの合成をgに作用させたところ，２つの合成では，単独の場合と同様あまりぱっとしないrldnfが，３つの合成の一番最後の処理になると僅差ながら最も簡単な式を与え，単独では頑張っていたrlgsn，rlitabはマイペースという結果になりました．

rldnf( rlitab( rlgsn(g) ) )
a - 1 >= 0 and m + 1 = 0 or
a = 0 and m = 0 or
a**2 - 2*a - m = 0 and a - 1 < 0 and a > 0 and m + 1 > 0 and m < 0

rlgsn( rldnf( rlitab(g) ) )
a = 0 and m = 0 or
a**2 - 2*a - m = 0 and a - 1 < 0 and a > 0 and m + 1 > 0 and m < 0 or
a - 1 = 0 and m + 1 = 0 or
a - 1 > 0 and m + 1 = 0

rldnf( rlgsn( rlitab(g) ) )
rlgsn( rlitab( rldnf(g) ) )
a - 1 > 0 and m + 1 = 0 or
a = 0 and m = 0 or
a**2 - 2*a - m = 0 and a - 1 < 0 and a > 0 and m + 1 > 0 and m < 0 or
a - 1 = 0 and m + 1 = 0

rlitab( rldnf( rlgsn(g) ) )
rlitab( rlgsn( rldnf(g) ) )
m + 1 > 0 and (a = 0 and m = 0 or a**2 - 2*a - m = 0 and a - 1 < 0 and a > 0 and m < 0) or
a - 1 >= 0 and m + 1 = 0

rlitab( rlgsn(g) )
m + 1 > 0 and (a**2 - 2*a - m = 0 and a - 1 < 0 and a > 0 and m < 0 or a = 0 and m = 0) or
a - 1 >= 0 and m + 1 = 0

rlgsn( rlitab(g) )
a - 1 > 0 and m + 1 = 0 or
a - 1 = 0 and m + 1 = 0 or
a**2 - 2*a - m = 0 and a - 1 < 0 and a > 0 and m + 1 > 0 and m < 0 or
a = 0 and m = 0

rlitab( rldnf(g) )
a**2 - 2*a - m > 0 and a - 1 > 0 and m + 1 = 0 or
a**2 - 2*a - m = 0 and (a = 0 and m = 0 or a - 1 < 0 and a > 0 and m + 1 > 0 and m < 0 or a - 1 = 0 and m + 1 = 0)

rldnf( rlitab(g) )
a**2 - 2*a - m = 0 and a = 0 and m = 0 or
a**2 - 2*a - m = 0 and a - 1 < 0 and a > 0 and m + 1 > 0 and m < 0 or
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 and m + 1 = 0

rldnf( rlgsn(g) )
rlgsn( rldnf(g) )
a = 0 and m = 0 or
a**2 - 2*a - m = 0 and a - 1 < 0 and a > 0 and m + 1 > 0 and m < 0 or
a - 1 = 0 and m + 1 = 0 or
a - 1 > 0 and a - 2 < 0 and m + 1 = 0 or
a - 2 >= 0 and m + 1 = 0

なお，Mathematicaでは，QEは簡約関数に統合されており，強力な（強力過ぎる？）同値変形を実現しています．その関数の名はReduce（http://reference.wolfram.com/mathematica/ref/Reduce.ja.html）．何とも…な命名ですが，同じ「区間0≦x≦aにおけるx^2-2xの最小値がmである」という条件を
f[x_] := x^2 - 2 x; Reduce[ Exists[x, 0 <= x <= a, f[x] == m] && ForAll[x, 0 <= x <= a, f[x] >= m], Reals]
と入力すると，Mathematicaは
(0 <= a <= 1 && m == -2 a + a^2) || (a > 1 && m == -1)
と答えます．