項書き換え規則を完備化します．

アルゴリズムにはKnuth-Bendixによる方法を用いているため，本来完備化に成功する等式集合であっても実際に成功するかどうかは記述した順序に依存します．

入力は概ね標準的なtrsファイルのフォーマットに準拠します．<>で囲んだ文字列はコメントになります．

完備化中にtermの比較がlpoにて失敗した場合，あるいはlpoでupper limitで指定した回比較して完備化が終了しなかった場合に強制停止し完備化そのものを失敗として扱います．

trsファイルの例などはこちらから参照すると良いです．

このプログラムはC++とemscriptenで書かれています．ソースコードはこちら