等価性

nns,nnss と同じく，qex,solvex の入力と出力とは等価，つまり，変数に任意の実数を代入したとき，それらの true,false は一致します．

例えば，sqrt を含む場合，定義：y=sqrt(x)⇔(y^2=x∧y>=0) により，x<0 のとき，y=sqrt(x) は false ですから，前回の最後の例の入力：[ [x^2=a,x>-1] ]，出力：[ [a < 1,x = -sqrt(a)],[x = sqrt(a)] ] の等価性は，a<0 のとき入出力とも false，1<=a のとき出力は [ [false],[x = sqrt(a)] ]，つまり，[ [x = sqrt(a)] ] といった具合に確かめられますし，xa 座標平面における入力，出力が表す図形が一致することからも判るでしょう．

システム自身に等価性をチェックさせるには，solvex の実行直後に

(%i36) thischeck();
Evaluation took 1.9700 seconds (3.1300 elapsed) using 117.474 MB.
(%o36) true

とすればよく，入出力は

(%i37) thisin;
Evaluation took 0.0000 seconds (0.0000 elapsed) using 48 bytes.
(%o37) (x > -1) %and (x^2 = a)
(%i38) thisout;
Evaluation took 0.0000 seconds (0.0000 elapsed) using 48 bytes.
(%o38) [[a < 1,x = -sqrt(a)],[x = sqrt(a)]]

のように参照出来ます．