Term Rewriting System R: [x, y] O(0) -> 0 +(0, x) -> x +(x, 0) -> x +(O(x), O(y)) -> O(+(x, y)) +(O(x), I(y)) -> I(+(x, y)) +(I(x), O(y)) -> I(+(x, y)) +(I(x), I(y)) -> O(+(+(x, y), I(0))) *(0, x) -> 0 *(x, 0) -> 0 *(O(x), y) -> O(*(x, y)) *(I(x), y) -> +(O(*(x, y)), y) -(x, 0) -> x -(0, x) -> 0 -(O(x), O(y)) -> O(-(x, y)) -(O(x), I(y)) -> I(-(-(x, y), I(1))) -(I(x), O(y)) -> I(-(x, y)) -(I(x), I(y)) -> O(-(x, y)) Termination of R to be shown. R contains the following Dependency Pairs: +'(I(x), I(y)) -> O'(+(+(x, y), I(0))) +'(I(x), I(y)) -> +'(+(x, y), I(0)) +'(I(x), I(y)) -> +'(x, y) +'(O(x), O(y)) -> O'(+(x, y)) +'(O(x), O(y)) -> +'(x, y) +'(O(x), I(y)) -> +'(x, y) +'(I(x), O(y)) -> +'(x, y) -'(I(x), I(y)) -> O'(-(x, y)) -'(I(x), I(y)) -> -'(x, y) -'(O(x), O(y)) -> O'(-(x, y)) -'(O(x), O(y)) -> -'(x, y) -'(I(x), O(y)) -> -'(x, y) -'(O(x), I(y)) -> -'(-(x, y), I(1)) -'(O(x), I(y)) -> -'(x, y) *'(I(x), y) -> +'(O(*(x, y)), y) *'(I(x), y) -> O'(*(x, y)) *'(I(x), y) -> *'(x, y) *'(O(x), y) -> O'(*(x, y)) *'(O(x), y) -> *'(x, y) Furthermore, R contains three SCCs. SCC1: +'(I(x), O(y)) -> +'(x, y) +'(O(x), I(y)) -> +'(x, y) +'(O(x), O(y)) -> +'(x, y) +'(I(x), I(y)) -> +'(x, y) +'(I(x), I(y)) -> +'(+(x, y), I(0)) Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations. This is possible by using the following (C_E-compatible) Polynomial ordering. Polynomial interpretation: POL(I(x_1)) = x_1 POL(O(x_1)) = x_1 POL(+'(x_1, x_2)) = 1 + x_1 + x_2 POL(+(x_1, x_2)) = x_1 + x_2 POL(0) = 0 No Dependency Pairs can be deleted. The following rules of R can be deleted: -(I(x), I(y)) -> O(-(x, y)) -(x, 0) -> x -(O(x), O(y)) -> O(-(x, y)) -(0, x) -> 0 -(I(x), O(y)) -> I(-(x, y)) -(O(x), I(y)) -> I(-(-(x, y), I(1))) *(0, x) -> 0 *(I(x), y) -> +(O(*(x, y)), y) *(O(x), y) -> O(*(x, y)) *(x, 0) -> 0 This transformation is resulting in one new subcycle: SCC1.MRR1: +'(O(x), I(y)) -> +'(x, y) +'(O(x), O(y)) -> +'(x, y) +'(I(x), I(y)) -> +'(x, y) +'(I(x), I(y)) -> +'(+(x, y), I(0)) +'(I(x), O(y)) -> +'(x, y) Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations. This is possible by using the following (C_E-compatible) Polynomial ordering. Polynomial interpretation: POL(I(x_1)) = 1 + x_1 POL(O(x_1)) = x_1 POL(+'(x_1, x_2)) = 1 + x_1 + x_2 POL(+(x_1, x_2)) = x_1 + x_2 POL(0) = 0 The following Dependency Pairs can be deleted: +'(O(x), I(y)) -> +'(x, y) +'(I(x), I(y)) -> +'(x, y) +'(I(x), I(y)) -> +'(+(x, y), I(0)) +'(I(x), O(y)) -> +'(x, y) The following rules of R can be deleted: +(I(x), I(y)) -> O(+(+(x, y), I(0))) This transformation is resulting in one new subcycle: SCC1.MRR1.MRR1: +'(O(x), O(y)) -> +'(x, y) Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations. This is possible by using the following (C_E-compatible) Polynomial ordering. Polynomial interpretation: POL(O(x_1)) = 1 + x_1 POL(+'(x_1, x_2)) = 1 + x_1 + x_2 The following Dependency Pairs can be deleted: +'(O(x), O(y)) -> +'(x, y) This transformation is resulting in no new subcycles. SCC2: -'(O(x), I(y)) -> -'(x, y) -'(O(x), I(y)) -> -'(-(x, y), I(1)) -'(I(x), O(y)) -> -'(x, y) -'(O(x), O(y)) -> -'(x, y) -'(I(x), I(y)) -> -'(x, y) Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations. This is possible by using the following (C_E-compatible) Polynomial ordering. Polynomial interpretation: POL(1) = 0 POL(-(x_1, x_2)) = x_1 + x_2 POL(-'(x_1, x_2)) = 1 + x_1 + x_2 POL(I(x_1)) = x_1 POL(O(x_1)) = x_1 POL(0) = 0 No Dependency Pairs can be deleted. The following rules of R can be deleted: +(0, x) -> x +(I(x), I(y)) -> O(+(+(x, y), I(0))) +(O(x), O(y)) -> O(+(x, y)) +(O(x), I(y)) -> I(+(x, y)) +(I(x), O(y)) -> I(+(x, y)) +(x, 0) -> x *(0, x) -> 0 *(I(x), y) -> +(O(*(x, y)), y) *(O(x), y) -> O(*(x, y)) *(x, 0) -> 0 This transformation is resulting in one new subcycle: SCC2.MRR1: -'(O(x), I(y)) -> -'(-(x, y), I(1)) -'(I(x), O(y)) -> -'(x, y) -'(O(x), O(y)) -> -'(x, y) -'(I(x), I(y)) -> -'(x, y) -'(O(x), I(y)) -> -'(x, y) Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations. This is possible by using the following (C_E-compatible) Polynomial ordering. Polynomial interpretation: POL(1) = 0 POL(-(x_1, x_2)) = x_1 + x_2 POL(-'(x_1, x_2)) = 1 + x_1 + x_2 POL(I(x_1)) = x_1 POL(O(x_1)) = x_1 POL(0) = 1 No Dependency Pairs can be deleted. The following rules of R can be deleted: -(x, 0) -> x This transformation is resulting in one new subcycle: SCC2.MRR1.MRR1: -'(O(x), I(y)) -> -'(x, y) -'(I(x), O(y)) -> -'(x, y) -'(O(x), O(y)) -> -'(x, y) -'(I(x), I(y)) -> -'(x, y) -'(O(x), I(y)) -> -'(-(x, y), I(1)) Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations. This is possible by using the following (C_E-compatible) Polynomial ordering. Polynomial interpretation: POL(1) = 0 POL(-(x_1, x_2)) = x_1 + x_2 POL(-'(x_1, x_2)) = 1 + x_1 + x_2 POL(I(x_1)) = 1 + x_1 POL(O(x_1)) = 1 + x_1 POL(0) = 0 The following Dependency Pairs can be deleted: -'(O(x), I(y)) -> -'(x, y) -'(I(x), O(y)) -> -'(x, y) -'(O(x), O(y)) -> -'(x, y) -'(I(x), I(y)) -> -'(x, y) -'(O(x), I(y)) -> -'(-(x, y), I(1)) This transformation is resulting in no new subcycles. SCC3: *'(O(x), y) -> *'(x, y) *'(I(x), y) -> *'(x, y) Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations. This is possible by using the following (C_E-compatible) Polynomial ordering. Polynomial interpretation: POL(I(x_1)) = 1 + x_1 POL(O(x_1)) = 1 + x_1 POL(*'(x_1, x_2)) = 1 + x_1 + x_2 The following Dependency Pairs can be deleted: *'(O(x), y) -> *'(x, y) *'(I(x), y) -> *'(x, y) This transformation is resulting in no new subcycles. Termination of R successfully shown. Duration: 1.368 seconds.