0, 0', 0'', 0''', ... という元からなる集合に 演算 + を、a + 0 = a、a + b' = (a + b)'、 演算 * を、a * 0 = 0、a * b' = (a * b) + a と定義します。
a + b' = (a + b)' から a + b'' = (a + b)'', a + b''' = (a + b)''', ... が成り立ちます。 これを a + b^ = (a + b)^ で表します。 これと a + 0 = a から、a + 0^ = (a + 0)^ = a^ ---(1) となります。 また、a + b' = (a + b)' から a + (b + c') = (a + (b + c)') = (a + (b + c))' となるので、a + (b + c^) = (a + (b + c))^ が成り立ちます。 これと a + 0 = a から、a + (b + 0^) = (a + (b + 0))^ = (a + b)^ ---(2) となります。 (1) と (2) から、a + (b + 0^) = (a + b)^ = (a + b) + 0^ となり、 任意の {0, 0', 0'', ... } の元 c に対して、(a + b) + c = a + (b + c) が成り立つことがわかります。 また、
使い方: リストから式を選んで[select]ボタンを押すと、 下のテキストボックスにコピーされます。 このようにして2つの式を選んで、[all]ボタンを押すと、 2つの式を組み合わせた式が、下のリストに出るので、 式を選択して、[add]を押してください。 上のリストに式が追加されます。 [add ^] を押すと、選択した式の ' を ^ に変えることができるとき、 ^ に変えた式が登録されます。 [add 0^] を押すと、選択した式の 0^ を変数に変えることができるとき、 変数に変えた式が登録されます。