Xk のリスト対応版

　前回の最後に挙げたような条件の処理に適した「点（リスト）の個数を規定する量化子」いわゆる「Numerical Existential Quantifier」を作ることは比較的容易です．
　例えば，一般に条件 P を満たす異なるリスト X が少なくとも k 個存在するという式を F(k,X,P) とすれば

F(k,X,P) ∧ ¬(F(k+1,X,P))

は条件 P を満たす異なるリスト X が丁度 k 個存在するという式ですから，F(k,X,P) を出力する関数を作れば十分であり，この方法で上記の量化子を RedLog に実装したのが，次の exk です．


　ただし，この関数は原理をそのままコード化したものなので，処理の効率はよくありません．以下のような簡単な処理でも，rlqe の出力は長大なものとなり，SLFQ はその簡約に QEPCAD B を 140万回以上も呼び出しています．