[1] 0+x0 -> x0 [2] m(x0,1) -> x0 [3] m(1,x0) -> x0 [4] i(x0)+x0 -> 0 [5] i(0) -> 0 [6] i(i(x0)) -> x0 [7] i(i(x0+x)+x) -> x0 [8] i(i(x0)+x)+x -> x0 [9] i(x0+x)+x -> i(x0) [10] i(i(x0)+i(x)) -> x0+x [11] i(i(x)+x0) -> i(x0)+x [12] i(x0+x) -> i(x0)+i(x) [13] m(x,x0+y) -> m(x,x0)+m(x,y) [14] m(x,0)+m(x,x0) -> m(x,x0) [15] m(x0,0)+x0 -> x0 [16] m(0,0) -> 0 [17] m(x0,0) -> 0 [18] m(x,i(x0))+m(x,x0) -> 0 [19] m(x0,i(1))+x0 -> 0 [20] m(0,i(1)) -> 0 [21] i(m(x0,i(1))) -> x0 [22] m(x0,i(1)) -> i(x0) [23] i(m(x0,i(x))) -> m(x0,x) [24] m(x0,i(x)) -> i(m(x0,x)) [25] m(x+y,x0) -> m(x,x0)+m(y,x0) [26] m(0,x)+m(x0,x) -> m(x0,x) [27] m(0,x0)+x0 -> x0 [28] m(0,x0) -> 0 [29] m(i(x0),x)+m(x0,x) -> 0 [30] m(i(1),x0)+x0 -> 0 [31] i(m(i(1),x0)) -> x0 [32] m(i(1),x0) -> i(x0) [33] i(m(i(x),x0)) -> m(x,x0) [34] m(i(x),x0) -> i(m(x,x0)) Completion succeeded. { [-1] 0+x0 = x0 (trace = Original(1,)) [-2] i(x0)+x0 = 0 (trace = Original(2,)) [-3] m(x0,1) = x0 (trace = Original(3,)) [-4] m(1,x0) = x0 (trace = Original(4,)) [-5] m(x+y,x0) = m(x,x0)+m(y,x0) (trace = Original(5,)) [-6] m(x,x0+y) = m(x,x0)+m(x,y) (trace = Original(6,)) [-11] i(0) = 0 (trace = Superposition of [1] 0+x0 -> x0 over [4] i(x0)+x0 -> 0 at /\)) [-30] 0+i(x6) = 0+i(x6+x8)+x8 (trace = Superposition of [-4] i(x0)+x0+x -> 0+x over [-4] i(x0)+x0+x -> 0+x at /\)) [-31] i(x0) = i(x0+x)+x (trace = Rewriting [-30] 0+i(x6) = 0+i(x6+x8)+x8 by ([1] 0+x0 -> x0 at L./\).([1] 0+x0 -> x0 at R./\)) [-65] 0+x7 = 0+i(i(x7)) (trace = Superposition of [-4] i(x0)+x0+x -> 0+x over [-4] i(x0)+x0+x -> 0+x at /\)) [-66] x0 = i(i(x0)) (trace = Rewriting [-65] 0+x7 = 0+i(i(x7)) by ( [1] 0+x0 -> x0 at L./\). ([1] 0+x0 -> x0 at R./\)) [-122] i(0+x6+x8)+i(x5)+x8 = i(x5+x6) (trace = Superposition of [-4] i(x0) +x0 +x -> 0+x over [9] i(x0+x) + x -> i(x0) at 0.0)) [-123] i(x0)+i(x) = i(x0+x) (trace = Rewriting [-122] i(0+x6+x8)+i(x5)+x8 = i(x5+x6) by ( [1] 0+x0 -> x0 at L.0.0). ([-9] i(x0+x)+x+y -> i(x0)+y at L./\)) [-222] m(x,x0) = m(x,0)+m(x,x0) (trace = Superposition of [1] 0+x0 -> x0 over [13] m(x,x0+y) -> m(x,x0)+m(x,y) at 1)) [-225] m(y,0) = m(y,i(x6))+m(y,x6) (trace = Superposition of [4] i(x0)+x0 -> 0 over [13] m(x,x0+y) -> m(x,x0)+m(x,y) at 1)) [-239] m(x,0)+x = m(x,1) (trace = Superposition of [2] m(x0,1) -> x0 over [14] m(x,0)+m(x,x0) -> m(x,x0) at 1)) [-240] m(x0,0)+x0 = x0 (trace = Rewriting [-239] m(x,0)+x = m(x,1) by ([2] m(x0,1) -> x0 at R./\)) [-259] 0+m(x6,0) = i(x6)+x6 (trace = Superposition of [-4] i(x0)+x0+x -> 0+x over [-15] m(x0,0)+x0+x -> x0+x at /\)) [-260] m(x0,0) = 0 (trace = Rewriting [-259] 0+m(x6,0) = i(x6)+x6 by ([1] 0+x0 -> x0 at L./\).([4] i(x0)+x0 -> 0 at R./\)) [-280] 0 = m(x,i(x0))+m(x,x0) (trace = Rewriting [-225] m(y,0) = m(y,i(x6)) + m(y,x6) by ([17] m(x0,0) -> 0 at L./\)) [-342] 0+m(y,i(x0)) = 0+i(m(y,x0)) (trace = Superposition of [-4] i(x0)+x0+x -> 0+x over [-18] m(x,i(x0)) +m(x,x0) +y -> 0+y at /\)) [-343] m(x0,i(x)) = i(m(x0,x)) (trace = Rewriting [-342] 0+m(y,i(x0)) = 0+i(m(y,x0)) by ([1] 0+x0 -> x0 at L./\).([1] 0+x0 -> x0 at R./\)) [-366] m(x0,x) = m(0,x)+m(x0,x) (trace = Superposition of [1] 0+x0 -> x0 over [25] m(x+y,x0) -> m(x,x0)+m(y,x0) at 0)) [-369] m(0,x0) = m(i(x6),x0)+m(x6,x0) (trace = Superposition of [4] i(x0)+x0 -> 0 over [25] m( x+y, x0) -> m(x,x0) +m(y,x0) at 0)) [-387] m(0,x)+x = m(1,x) (trace = Superposition of [3] m(1,x0) -> x0 over [26] m(0,x)+m(x0,x) -> m(x0,x) at 1)) [-388] m(0,x0)+x0 = x0 (trace = Rewriting [-387] m(0,x)+x = m(1,x) by ([3] m(1,x0) -> x0 at R./\)) [-400] 0+m(0,x6) = i(x6)+x6 (trace = Superposition of [-4] i(x0)+x0+x -> 0+x over [-27] m(0,x0)+x0+x -> x0+x at /\)) [-401] m(0,x0) = 0 (trace = Rewriting [-400] 0+m(0,x6) = i(x6)+x6 by ([1] 0+x0 -> x0 at L./\).([4] i(x0)+x0 -> 0 at R./\)) [-415] 0 = m(i(x0),x)+m(x0,x) (trace = Rewriting [-369] m(0,x0) = m(i(x6),x0) +m(x6,x0) by ([28] m(0,x0) -> 0 at L./\)) [-472] 0+m(i(x0),y) = 0+i(m(x0,y)) (trace = Superposition of [-4] i(x0)+x0+x -> 0+x over [-29] m(i(x0),x) +m(x0,x) +y -> 0+y at /\)) [-473] m(i(x),x0) = i(m(x,x0)) (trace = Rewriting [-472] 0+m(i(x0),y) = 0+i(m(x0,y)) by ([1] 0+x0 -> x0 at L./\).([1] 0+x0 -> x0 at R./\)) } (31 equations) { [-29] m(i(x0),x)+m(x0,x)+y -> 0+y (trace = Extension of [29] m(i(x0),x) +m(x0,x) -> 0) [-27] m(0,x0)+x0+x -> x0+x (trace = Extension of [27] m(0,x0)+x0 -> x0) [-18] m(x,i(x0))+m(x,x0)+y -> 0+y (trace = Extension of [18] m(x,i(x0)) +m(x,x0) -> 0) [-15] m(x0,0)+x0+x -> x0+x (trace = Extension of [15] m(x0,0)+x0 -> x0) [-9] i(x0+x)+x+y -> i(x0)+y (trace = Extension of [9] i(x0+x)+x -> i(x0)) [-4] i(x0)+x0+x -> 0+x (trace = Extension of [4] i(x0)+x0 -> 0) [1] 0+x0 -> x0 (trace = Oriented([-1] 0+x0 = x0)) [2] m(x0,1) -> x0 (trace = Oriented([-3] m(x0,1) = x0)) [3] m(1,x0) -> x0 (trace = Oriented([-4] m(1,x0) = x0)) [4] i(x0)+x0 -> 0 (trace = Oriented([-2] i(x0)+x0 = 0)) [9] i(x0+x)+x -> i(x0) (trace = Reverted([-31] i(x0) = i(x0+x)+x)) [13] m(x,x0+y) -> m(x,x0)+m(x,y) (trace = Oriented([-6] m(x,x0+y) = m(x,x0)+m(x,y))) [14] m(x,0)+m(x,x0) -> m(x,x0) (trace = Reverted([-222] m(x,x0) = m(x,0) +m(x,x0))) [15] m(x0,0)+x0 -> x0 (trace = Oriented([-240] m(x0,0)+x0 = x0)) [17] m(x0,0) -> 0 (trace = Oriented([-260] m(x0,0) = 0)) [18] m(x,i(x0))+m(x,x0) -> 0 (trace = Reverted([-280] 0 = m(x,i(x0))+m(x,x0))) [25] m(x+y,x0) -> m(x,x0)+m(y,x0) (trace = Oriented([-5] m(x+y,x0) = m(x,x0)+m(y,x0))) [26] m(0,x)+m(x0,x) -> m(x0,x) (trace = Reverted([-366] m(x0,x) = m(0,x) +m(x0,x))) [27] m(0,x0)+x0 -> x0 (trace = Oriented([-388] m(0,x0)+x0 = x0)) [28] m(0,x0) -> 0 (trace = Oriented([-401] m(0,x0) = 0)) [29] m(i(x0),x)+m(x0,x) -> 0 (trace = Reverted([-415] 0 = m(i(x0),x)+m(x0,x))) } (21 rules) real 0m0.083s user 0m0.080s sys 0m0.004s