[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(m(x,y),x0) -> m(x,m(y,x0)) [14] m(x,x0+y) -> m(x,x0)+m(x,y) [15] m(x,0)+m(x,x0) -> m(x,x0) [16] m(x0,0)+x0 -> x0 [17] m(0,0) -> 0 [18] m(x0,0) -> 0 [19] m(x,m(0,x0)) -> m(0,x0) [20] m(x,i(x0))+m(x,x0) -> 0 [21] m(x0,i(1))+x0 -> 0 [22] m(0,i(1)) -> 0 [23] i(m(x0,i(1))) -> x0 [24] m(x0,i(1)) -> i(x0) [25] m(x0,i(x)) -> i(m(x0,x)) [26] m(0,m(i(1),x0)) -> m(0,x0) Unorientable equation m(i(x),x0) = m(x,m(i(1),x0)) [29] m(i(x0),m(i(1),x)) -> m(x0,x) [34] m(x+y,x0) -> m(x,x0)+m(y,x0) [35] m(0,x)+m(x0,x) -> m(x0,x) [36] m(0,x0)+x0 -> x0 [37] m(0,x0) -> 0 [38] m(i(x0),x)+m(x0,x) -> 0 [39] m(i(1),x0)+x0 -> 0 [40] i(m(i(1),x0)) -> x0 [41] m(i(1),x0) -> i(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(m(x,y),x0) = m(x,m(y,x0)) (trace = Original(5,)) [-6] m(x+y,x0) = m(x,x0)+m(y,x0) (trace = Original(6,)) [-7] m(x,x0+y) = m(x,x0)+m(x,y) (trace = Original(7,)) [-12] i(0) = 0 (trace = Superposition of [1] 0+x0 -> x0 over [4] i(x0)+x0 -> 0 at /\)) [-31] 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 /\)) [-32] i(x0) = i(x0+x)+x (trace = Rewriting [-31] 0+i(x6) = 0+i(x6+x8)+x8 by ([1] 0+x0 -> x0 at L./\).([1] 0+x0 -> x0 at R./\)) [-66] 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 /\)) [-67] x0 = i(i(x0)) (trace = Rewriting [-66] 0+x7 = 0+i(i(x7)) by ( [1] 0+x0 -> x0 at L./\). ([1] 0+x0 -> x0 at R./\)) [-123] 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)) [-124] i(x0)+i(x) = i(x0+x) (trace = Rewriting [-123] 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./\)) [-228] m(x,x0) = m(x,0)+m(x,x0) (trace = Superposition of [1] 0+x0 -> x0 over [14] m(x,x0+y) -> m(x,x0)+m(x,y) at 1)) [-231] m(y,0) = m(y,i(x6))+m(y,x6) (trace = Superposition of [4] i(x0)+x0 -> 0 over [14] m(x,x0+y) -> m(x,x0)+m(x,y) at 1)) [-245] m(x,0)+x = m(x,1) (trace = Superposition of [2] m(x0,1) -> x0 over [15] m(x,0)+m(x,x0) -> m(x,x0) at 1)) [-246] m(x0,0)+x0 = x0 (trace = Rewriting [-245] m(x,0)+x = m(x,1) by ([2] m(x0,1) -> x0 at R./\)) [-265] 0+m(x6,0) = i(x6)+x6 (trace = Superposition of [-4] i(x0)+x0+x -> 0+x over [-16] m(x0,0)+x0+x -> x0+x at /\)) [-266] m(x0,0) = 0 (trace = Rewriting [-265] 0+m(x6,0) = i(x6)+x6 by ([1] 0+x0 -> x0 at L./\).([4] i(x0)+x0 -> 0 at R./\)) [-298] 0 = m(x,i(x0))+m(x,x0) (trace = Rewriting [-231] m(y,0) = m(y,i(x6)) + m(y,x6) by ([18] m(x0,0) -> 0 at L./\)) [-299] m(x0,i(1))+x0 = 0 (trace = Superposition of [2] m(x0,1) -> x0 over [20] m(x,i(x0))+m(x,x0) -> 0 at 1)) [-331] 0+m(x6,i(1)) = 0+i(x6) (trace = Superposition of [-4] i(x0)+x0+x -> 0+x over [-21] m(x0,i(1)) +x0 +x -> 0+x at /\)) [-332] m(x0,i(1)) = i(x0) (trace = Rewriting [-331] 0+m(x6,i(1)) = 0+i(x6) by ([1] 0+x0 -> x0 at L./\).([1] 0+x0 -> x0 at R./\)) [-357] m(z,m(x5,i(1))) = i(m(z,x5)) (trace = Superposition of [13] m(m(x,y), x0) -> m(x,m(y,x0)) over [24] m(x0, i(1)) -> i(x0) at /\)) [-358] m(x0,i(x)) = i(m(x0,x)) (trace = Rewriting [-357] m(z,m(x5,i(1))) = i(m(z,x5)) by ([24] m(x0,i(1)) -> i(x0) at L.1)) [-359] m(i(x),x0) = m(x,m(i(1),x0)) (trace = Superposition of [13] m(m(x,y), x0) -> m(x,m(y,x0)) over [24] m(x0, i(1)) -> i(x0) at 0)) [-404] m(x0,x) = m(0,x)+m(x0,x) (trace = Superposition of [1] 0+x0 -> x0 over [34] m(x+y,x0) -> m(x,x0)+m(y,x0) at 0)) [-407] m(0,x0) = m(i(x6),x0)+m(x6,x0) (trace = Superposition of [4] i(x0)+x0 -> 0 over [34] m( x+y, x0) -> m(x,x0) +m(y,x0) at 0)) [-427] m(0,x)+x = m(1,x) (trace = Superposition of [3] m(1,x0) -> x0 over [35] m(0,x)+m(x0,x) -> m(x0,x) at 1)) [-428] m(0,x0)+x0 = x0 (trace = Rewriting [-427] m(0,x)+x = m(1,x) by ([3] m(1,x0) -> x0 at R./\)) [-440] 0+m(0,x6) = i(x6)+x6 (trace = Superposition of [-4] i(x0)+x0+x -> 0+x over [-36] m(0,x0)+x0+x -> x0+x at /\)) [-441] m(0,x0) = 0 (trace = Rewriting [-440] 0+m(0,x6) = i(x6)+x6 by ([1] 0+x0 -> x0 at L./\).([4] i(x0)+x0 -> 0 at R./\)) [-459] 0 = m(i(x0),x)+m(x0,x) (trace = Rewriting [-407] m(0,x0) = m(i(x6),x0) +m(x6,x0) by ([37] m(0,x0) -> 0 at L./\)) [-462] m(i(1),x0)+x0 = 0 (trace = Superposition of [3] m(1,x0) -> x0 over [38] m(i(x0),x)+m(x0,x) -> 0 at 1)) [-485] 0+m(i(1),x6) = 0+i(x6) (trace = Superposition of [-4] i(x0)+x0+x -> 0+x over [-39] m(i(1),x0) +x0 +x -> 0+x at /\)) [-486] m(i(1),x0) = i(x0) (trace = Rewriting [-485] 0+m(i(1),x6) = 0+i(x6) by ([1] 0+x0 -> x0 at L./\).([1] 0+x0 -> x0 at R./\)) } (37 equations) { [-39] m(i(1),x0)+x0+x -> 0+x (trace = Extension of [39] m(i(1),x0)+x0 -> 0) [-36] m(0,x0)+x0+x -> x0+x (trace = Extension of [36] m(0,x0)+x0 -> x0) [-21] m(x0,i(1))+x0+x -> 0+x (trace = Extension of [21] m(x0,i(1))+x0 -> 0) [-16] m(x0,0)+x0+x -> x0+x (trace = Extension of [16] 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([-32] i(x0) = i(x0+x)+x)) [13] m(m(x,y),x0) -> m(x,m(y,x0)) (trace = Oriented([-5] m(m(x,y),x0) = m(x,m(y,x0)))) [14] m(x,x0+y) -> m(x,x0)+m(x,y) (trace = Oriented([-7] m(x,x0+y) = m(x,x0)+m(x,y))) [15] m(x,0)+m(x,x0) -> m(x,x0) (trace = Reverted([-228] m(x,x0) = m(x,0) +m(x,x0))) [16] m(x0,0)+x0 -> x0 (trace = Oriented([-246] m(x0,0)+x0 = x0)) [18] m(x0,0) -> 0 (trace = Oriented([-266] m(x0,0) = 0)) [20] m(x,i(x0))+m(x,x0) -> 0 (trace = Reverted([-298] 0 = m(x,i(x0))+m(x,x0))) [21] m(x0,i(1))+x0 -> 0 (trace = Oriented([-299] m(x0,i(1))+x0 = 0)) [24] m(x0,i(1)) -> i(x0) (trace = Oriented([-332] m(x0,i(1)) = i(x0))) [28] m(i(x),x0) -> m(x,m(i(1),x0)) (trace = Oriented([-359] m(i(x),x0) = m(x,m(i(1),x0)))) [34] m(x+y,x0) -> m(x,x0)+m(y,x0) (trace = Oriented([-6] m(x+y,x0) = m(x,x0)+m(y,x0))) [35] m(0,x)+m(x0,x) -> m(x0,x) (trace = Reverted([-404] m(x0,x) = m(0,x) +m(x0,x))) [36] m(0,x0)+x0 -> x0 (trace = Oriented([-428] m(0,x0)+x0 = x0)) [37] m(0,x0) -> 0 (trace = Oriented([-441] m(0,x0) = 0)) [38] m(i(x0),x)+m(x0,x) -> 0 (trace = Reverted([-459] 0 = m(i(x0),x)+m(x0,x))) [39] m(i(1),x0)+x0 -> 0 (trace = Oriented([-462] m(i(1),x0)+x0 = 0)) [41] m(i(1),x0) -> i(x0) (trace = Oriented([-486] m(i(1),x0) = i(x0))) } (27 rules) real 0m0.103s user 0m0.084s sys 0m0.012s