それでは，

昨日の入力の説明です．まず
load_package redlog;
は文字通り，RedLog（reduce logic system）パッケージをロードするもので，MathematicaやmapleといったCASでも特定の内容を扱う際にはパッケージの明示的なロードが必要ですが，Reduceはその割合が大きいシステムです．次の
rlset r;
はRedLogのコンテキストを指定するもので，r（実数体），c（複素数体），z（有理整数環）などが選べます．ここまでは毎回の決まり事で，最後の
rlqe(ex(x,x^2+a*x+b=0 and x>0));
が個別のコマンドです．一番外のrlqeは
rlqe(式)
の形で用いられ，その式に含まれるすべての量化子∃，∀（というより束縛変数）を消去する（QE，Quantifier Elimination）関数の一つで，virtual substitutionという方法を採用したものです．RedLogには他にも，Cylindrical Algebraic Decompositionを採用したQE関数 rlcad，Hermitian Quantifier Eliminationを採用したQE関数 rlhqe が実装されています．次のexは
ex(束縛変数またはそのリスト,式)
の形で用いられ，その式を満たす束縛変数が存在するという式を返す特称量化の関数，これに対して，allは
all(束縛変数またはそのリスト,式)
の形で用いられ，任意の束縛変数がその式を満たすという式を返す全称量化の関数です．最後のx^2+a*x+b=0 and x>0は見ての通り，2つの式を and で結合した式で，一般には
not 式，または，not(式)
式 and 式 …，または，and(式,式,…)
式 or 式 …，または，or(式,式,…)
式 impl 式，または，impl(式,式)
式 repl 式，または，repl(式,式)
式 equiv 式，または，equiv(式,式)
の組み合わせになります．なお，非等号（≠）は <> です．