Term Rewriting System R: [x, y, z, l, l1, l2, l3] 0(#) -> # +(x, #) -> x +(#, x) -> x +(0(x), 0(y)) -> 0(+(x, y)) +(0(x), 1(y)) -> 1(+(x, y)) +(1(x), 0(y)) -> 1(+(x, y)) +(1(x), 1(y)) -> 0(+(+(x, y), 1(#))) +(+(x, y), z) -> +(x, +(y, z)) -(#, x) -> # -(x, #) -> x -(0(x), 0(y)) -> 0(-(x, y)) -(0(x), 1(y)) -> 1(-(-(x, y), 1(#))) -(1(x), 0(y)) -> 1(-(x, y)) -(1(x), 1(y)) -> 0(-(x, y)) not(true) -> false not(false) -> true if(true, x, y) -> x if(false, x, y) -> y eq(#, #) -> true eq(#, 1(y)) -> false eq(1(x), #) -> false eq(#, 0(y)) -> eq(#, y) eq(0(x), #) -> eq(x, #) eq(1(x), 1(y)) -> eq(x, y) eq(0(x), 1(y)) -> false eq(1(x), 0(y)) -> false eq(0(x), 0(y)) -> eq(x, y) ge(0(x), 0(y)) -> ge(x, y) ge(0(x), 1(y)) -> not(ge(y, x)) ge(1(x), 0(y)) -> ge(x, y) ge(1(x), 1(y)) -> ge(x, y) ge(x, #) -> true ge(#, 0(x)) -> ge(#, x) ge(#, 1(x)) -> false log(x) -> -(log'(x), 1(#)) log'(#) -> # log'(1(x)) -> +(log'(x), 1(#)) log'(0(x)) -> if(ge(x, 1(#)), +(log'(x), 1(#)), #) *(#, x) -> # *(0(x), y) -> 0(*(x, y)) *(1(x), y) -> +(0(*(x, y)), y) *(*(x, y), z) -> *(x, *(y, z)) *(x, +(y, z)) -> +(*(x, y), *(x, z)) app(nil, l) -> l app(cons(x, l1), l2) -> cons(x, app(l1, l2)) sum(nil) -> 0(#) sum(cons(x, l)) -> +(x, sum(l)) sum(app(l1, l2)) -> +(sum(l1), sum(l2)) prod(nil) -> 1(#) prod(cons(x, l)) -> *(x, prod(l)) prod(app(l1, l2)) -> *(prod(l1), prod(l2)) mem(x, nil) -> false mem(x, cons(y, l)) -> if(eq(x, y), true, mem(x, l)) inter(x, nil) -> nil inter(nil, x) -> nil inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)) inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)) inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2) inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1) ifinter(true, x, l1, l2) -> cons(x, inter(l1, l2)) ifinter(false, x, l1, l2) -> inter(l1, l2) Termination of R to be shown. R contains the following Dependency Pairs: GE(0(x), 1(y)) -> NOT(ge(y, x)) GE(0(x), 1(y)) -> GE(y, x) GE(1(x), 0(y)) -> GE(x, y) GE(0(x), 0(y)) -> GE(x, y) GE(1(x), 1(y)) -> GE(x, y) GE(#, 0(x)) -> GE(#, x) -'(0(x), 1(y)) -> -'(-(x, y), 1(#)) -'(0(x), 1(y)) -> -'(x, y) -'(1(x), 1(y)) -> 0'(-(x, y)) -'(1(x), 1(y)) -> -'(x, y) -'(1(x), 0(y)) -> -'(x, y) -'(0(x), 0(y)) -> 0'(-(x, y)) -'(0(x), 0(y)) -> -'(x, y) +'(0(x), 1(y)) -> +'(x, y) +'(1(x), 0(y)) -> +'(x, y) +'(0(x), 0(y)) -> 0'(+(x, y)) +'(0(x), 0(y)) -> +'(x, y) +'(1(x), 1(y)) -> 0'(+(+(x, y), 1(#))) +'(1(x), 1(y)) -> +'(+(x, y), 1(#)) +'(1(x), 1(y)) -> +'(x, y) +'(+(x, y), z) -> +'(x, +(y, z)) +'(+(x, y), z) -> +'(y, z) EQ(0(x), 0(y)) -> EQ(x, y) EQ(1(x), 1(y)) -> EQ(x, y) EQ(#, 0(y)) -> EQ(#, y) EQ(0(x), #) -> EQ(x, #) SUM(nil) -> 0'(#) SUM(cons(x, l)) -> +'(x, sum(l)) SUM(cons(x, l)) -> SUM(l) SUM(app(l1, l2)) -> +'(sum(l1), sum(l2)) SUM(app(l1, l2)) -> SUM(l1) SUM(app(l1, l2)) -> SUM(l2) PROD(app(l1, l2)) -> *'(prod(l1), prod(l2)) PROD(app(l1, l2)) -> PROD(l1) PROD(app(l1, l2)) -> PROD(l2) PROD(cons(x, l)) -> *'(x, prod(l)) PROD(cons(x, l)) -> PROD(l) MEM(x, cons(y, l)) -> IF(eq(x, y), true, mem(x, l)) MEM(x, cons(y, l)) -> EQ(x, y) MEM(x, cons(y, l)) -> MEM(x, l) APP(cons(x, l1), l2) -> APP(l1, l2) *'(x, +(y, z)) -> +'(*(x, y), *(x, z)) *'(x, +(y, z)) -> *'(x, y) *'(x, +(y, z)) -> *'(x, z) *'(*(x, y), z) -> *'(x, *(y, z)) *'(*(x, y), z) -> *'(y, z) *'(0(x), y) -> 0'(*(x, y)) *'(0(x), y) -> *'(x, y) *'(1(x), y) -> +'(0(*(x, y)), y) *'(1(x), y) -> 0'(*(x, y)) *'(1(x), y) -> *'(x, y) INTER(l1, cons(x, l2)) -> IFINTER(mem(x, l1), x, l2, l1) INTER(l1, cons(x, l2)) -> MEM(x, l1) INTER(app(l1, l2), l3) -> APP(inter(l1, l3), inter(l2, l3)) INTER(app(l1, l2), l3) -> INTER(l1, l3) INTER(app(l1, l2), l3) -> INTER(l2, l3) INTER(l1, app(l2, l3)) -> APP(inter(l1, l2), inter(l1, l3)) INTER(l1, app(l2, l3)) -> INTER(l1, l2) INTER(l1, app(l2, l3)) -> INTER(l1, l3) INTER(cons(x, l1), l2) -> IFINTER(mem(x, l2), x, l1, l2) INTER(cons(x, l1), l2) -> MEM(x, l2) IFINTER(false, x, l1, l2) -> INTER(l1, l2) IFINTER(true, x, l1, l2) -> INTER(l1, l2) LOG(x) -> -'(log'(x), 1(#)) LOG(x) -> LOG'(x) LOG'(0(x)) -> IF(ge(x, 1(#)), +(log'(x), 1(#)), #) LOG'(0(x)) -> GE(x, 1(#)) LOG'(0(x)) -> +'(log'(x), 1(#)) LOG'(0(x)) -> LOG'(x) LOG'(1(x)) -> +'(log'(x), 1(#)) LOG'(1(x)) -> LOG'(x) Furthermore, R contains 14 SCCs. SCC1: GE(#, 0(x)) -> GE(#, x) 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(GE(x_1, x_2)) = 1 + x_1 + x_2 POL(0(x_1)) = 1 + x_1 POL(#) = 1 The following Dependency Pairs can be deleted: GE(#, 0(x)) -> GE(#, x) This transformation is resulting in no new subcycles. SCC2: GE(1(x), 1(y)) -> GE(x, y) GE(0(x), 0(y)) -> GE(x, y) GE(1(x), 0(y)) -> GE(x, y) GE(0(x), 1(y)) -> GE(y, x) 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(x_1)) = 1 + x_1 POL(GE(x_1, x_2)) = 1 + x_1 + x_2 POL(0(x_1)) = 1 + x_1 The following Dependency Pairs can be deleted: GE(1(x), 1(y)) -> GE(x, y) GE(0(x), 0(y)) -> GE(x, y) GE(1(x), 0(y)) -> GE(x, y) GE(0(x), 1(y)) -> GE(y, x) This transformation is resulting in no new subcycles. SCC3: -'(0(x), 0(y)) -> -'(x, y) -'(1(x), 0(y)) -> -'(x, y) -'(1(x), 1(y)) -> -'(x, y) -'(0(x), 1(y)) -> -'(x, y) -'(0(x), 1(y)) -> -'(-(x, y), 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(x_1)) = x_1 POL(-(x_1, x_2)) = x_1 + x_2 POL(-'(x_1, x_2)) = 1 + x_1 + x_2 POL(0(x_1)) = x_1 POL(#) = 0 No Dependency Pairs can be deleted. The following rules of R can be deleted: ge(0(x), 1(y)) -> not(ge(y, x)) ge(1(x), 0(y)) -> ge(x, y) ge(0(x), 0(y)) -> ge(x, y) ge(1(x), 1(y)) -> ge(x, y) ge(x, #) -> true ge(#, 0(x)) -> ge(#, x) ge(#, 1(x)) -> false not(true) -> false not(false) -> true +(0(x), 1(y)) -> 1(+(x, y)) +(1(x), 0(y)) -> 1(+(x, y)) +(0(x), 0(y)) -> 0(+(x, y)) +(1(x), 1(y)) -> 0(+(+(x, y), 1(#))) +(+(x, y), z) -> +(x, +(y, z)) +(x, #) -> x +(#, x) -> x eq(#, #) -> true eq(0(x), 0(y)) -> eq(x, y) eq(1(x), 1(y)) -> eq(x, y) eq(#, 1(y)) -> false eq(1(x), 0(y)) -> false eq(0(x), 1(y)) -> false eq(#, 0(y)) -> eq(#, y) eq(1(x), #) -> false eq(0(x), #) -> eq(x, #) sum(nil) -> 0(#) sum(cons(x, l)) -> +(x, sum(l)) sum(app(l1, l2)) -> +(sum(l1), sum(l2)) if(false, x, y) -> y if(true, x, y) -> x prod(nil) -> 1(#) prod(app(l1, l2)) -> *(prod(l1), prod(l2)) prod(cons(x, l)) -> *(x, prod(l)) mem(x, cons(y, l)) -> if(eq(x, y), true, mem(x, l)) mem(x, nil) -> false app(nil, l) -> l app(cons(x, l1), l2) -> cons(x, app(l1, l2)) *(x, +(y, z)) -> +(*(x, y), *(x, z)) *(*(x, y), z) -> *(x, *(y, z)) *(0(x), y) -> 0(*(x, y)) *(#, x) -> # *(1(x), y) -> +(0(*(x, y)), y) inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1) inter(x, nil) -> nil inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)) inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)) inter(nil, x) -> nil inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2) ifinter(false, x, l1, l2) -> inter(l1, l2) ifinter(true, x, l1, l2) -> cons(x, inter(l1, l2)) log(x) -> -(log'(x), 1(#)) log'(0(x)) -> if(ge(x, 1(#)), +(log'(x), 1(#)), #) log'(1(x)) -> +(log'(x), 1(#)) log'(#) -> # This transformation is resulting in one new subcycle: SCC3.MRR1: -'(1(x), 0(y)) -> -'(x, y) -'(1(x), 1(y)) -> -'(x, y) -'(0(x), 1(y)) -> -'(x, y) -'(0(x), 1(y)) -> -'(-(x, y), 1(#)) -'(0(x), 0(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(x_1)) = 1 + x_1 POL(-(x_1, x_2)) = x_1 + x_2 POL(-'(x_1, x_2)) = 1 + x_1 + x_2 POL(0(x_1)) = 1 + x_1 POL(#) = 0 The following Dependency Pairs can be deleted: -'(1(x), 0(y)) -> -'(x, y) -'(1(x), 1(y)) -> -'(x, y) -'(0(x), 1(y)) -> -'(x, y) -'(0(x), 1(y)) -> -'(-(x, y), 1(#)) -'(0(x), 0(y)) -> -'(x, y) This transformation is resulting in no new subcycles. SCC4: +'(+(x, y), z) -> +'(y, z) +'(+(x, y), z) -> +'(x, +(y, z)) +'(1(x), 1(y)) -> +'(x, y) +'(1(x), 1(y)) -> +'(+(x, y), 1(#)) +'(0(x), 0(y)) -> +'(x, y) +'(1(x), 0(y)) -> +'(x, y) +'(0(x), 1(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(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(x_1)) = x_1 POL(#) = 0 No Dependency Pairs can be deleted. The following rules of R can be deleted: ge(0(x), 1(y)) -> not(ge(y, x)) ge(1(x), 0(y)) -> ge(x, y) ge(0(x), 0(y)) -> ge(x, y) ge(1(x), 1(y)) -> ge(x, y) ge(x, #) -> true ge(#, 0(x)) -> ge(#, x) ge(#, 1(x)) -> false not(true) -> false not(false) -> true -(0(x), 1(y)) -> 1(-(-(x, y), 1(#))) -(1(x), 1(y)) -> 0(-(x, y)) -(1(x), 0(y)) -> 1(-(x, y)) -(0(x), 0(y)) -> 0(-(x, y)) -(x, #) -> x -(#, x) -> # eq(#, #) -> true eq(0(x), 0(y)) -> eq(x, y) eq(1(x), 1(y)) -> eq(x, y) eq(#, 1(y)) -> false eq(1(x), 0(y)) -> false eq(0(x), 1(y)) -> false eq(#, 0(y)) -> eq(#, y) eq(1(x), #) -> false eq(0(x), #) -> eq(x, #) sum(nil) -> 0(#) sum(cons(x, l)) -> +(x, sum(l)) sum(app(l1, l2)) -> +(sum(l1), sum(l2)) if(false, x, y) -> y if(true, x, y) -> x prod(nil) -> 1(#) prod(app(l1, l2)) -> *(prod(l1), prod(l2)) prod(cons(x, l)) -> *(x, prod(l)) mem(x, cons(y, l)) -> if(eq(x, y), true, mem(x, l)) mem(x, nil) -> false app(nil, l) -> l app(cons(x, l1), l2) -> cons(x, app(l1, l2)) *(x, +(y, z)) -> +(*(x, y), *(x, z)) *(*(x, y), z) -> *(x, *(y, z)) *(0(x), y) -> 0(*(x, y)) *(#, x) -> # *(1(x), y) -> +(0(*(x, y)), y) inter(l1, cons(x, l2)) -> ifinter(mem(x, l1), x, l2, l1) inter(x, nil) -> nil inter(app(l1, l2), l3) -> app(inter(l1, l3), inter(l2, l3)) inter(l1, app(l2, l3)) -> app(inter(l1, l2), inter(l1, l3)) inter(nil, x) -> nil inter(cons(x, l1), l2) -> ifinter(mem(x, l2), x, l1, l2) ifinter(false, x, l1, l2) -> inter(l1, l2) ifinter(true, x, l1, l2) -> cons(x, inter(l1, l2)) log(x) -> -(log'(x), 1(#)) log'(0(x)) -> if(ge(x, 1(#)), +(log'(x), 1(#)), #) log'(1(x)) -> +(log'(x), 1(#)) log'(#) -> # This transformation is resulting in one new subcycle: SCC4.MRR1: +'(+(x, y), z) -> +'(x, +(y, z)) +'(1(x), 1(y)) -> +'(x, y) +'(1(x), 1(y)) -> +'(+(x, y), 1(#)) +'(0(x), 0(y)) -> +'(x, y) +'(1(x), 0(y)) -> +'(x, y) +'(0(x), 1(y)) -> +'(x, y) +'(+(x, y), z) -> +'(y, z) 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(x_1)) = 1 + x_1 POL(+'(x_1, x_2)) = 1 + x_1 + x_2 POL(+(x_1, x_2)) = x_1 + x_2 POL(0(x_1)) = x_1 POL(#) = 0 The following Dependency Pairs can be deleted: +'(1(x), 1(y)) -> +'(x, y) +'(1(x), 1(y)) -> +'(+(x, y), 1(#)) +'(1(x), 0(y)) -> +'(x, y) +'(0(x), 1(y)) -> +'(x, y) The following rules of R can be deleted: +(1(x), 1(y)) -> 0(+(+(x, y), 1(#))) This transformation is resulting in one new subcycle: SCC4.MRR1.MRR1: +'(+(x, y), z) -> +'(y, z) +'(0(x), 0(y)) -> +'(x, y) +'(+(x, y), z) -> +'(x, +(y, z)) 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(x_1)) = x_1 POL(+'(x_1, x_2)) = x_1 + x_2 POL(+(x_1, x_2)) = x_1 + x_2 POL(0(x_1)) = 1 + x_1 POL(#) = 0 The following Dependency Pairs can be deleted: +'(0(x), 0(y)) -> +'(x, y) The following rules of R can be deleted: +(0(x), 1(y)) -> 1(+(x, y)) +(1(x), 0(y)) -> 1(+(x, y)) +(0(x), 0(y)) -> 0(+(x, y)) 0(#) -> # +(x, #) -> x +(#, x) -> x This transformation is resulting in one new subcycle: SCC4.MRR1.MRR1.MRR1: +'(+(x, y), z) -> +'(x, +(y, z)) +'(+(x, y), z) -> +'(y, z) 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(+'(x_1, x_2)) = 1 + x_1 + x_2 POL(+(x_1, x_2)) = 1 + x_1 + x_2 The following Dependency Pairs can be deleted: +'(+(x, y), z) -> +'(y, z) No rules of R can be deleted. This transformation is resulting in one new subcycle: SCC4.MRR1.MRR1.MRR1.MRR1: +'(+(x, y), z) -> +'(x, +(y, z)) By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented. No rules need to be oriented. Used ordering: Polynomial ordering with Polynomial interpretation: POL(+(x_1, x_2)) = 1 + x_1 POL(+'(x_1, x_2)) = x_1 resulting in no subcycles. SCC5: EQ(#, 0(y)) -> EQ(#, 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(EQ(x_1, x_2)) = 1 + x_1 + x_2 POL(0(x_1)) = 1 + x_1 POL(#) = 1 The following Dependency Pairs can be deleted: EQ(#, 0(y)) -> EQ(#, y) This transformation is resulting in no new subcycles. SCC6: EQ(0(x), #) -> EQ(x, #) 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(EQ(x_1, x_2)) = 1 + x_1 + x_2 POL(0(x_1)) = 1 + x_1 POL(#) = 1 The following Dependency Pairs can be deleted: EQ(0(x), #) -> EQ(x, #) This transformation is resulting in no new subcycles. SCC7: EQ(1(x), 1(y)) -> EQ(x, y) EQ(0(x), 0(y)) -> EQ(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(x_1)) = 1 + x_1 POL(EQ(x_1, x_2)) = 1 + x_1 + x_2 POL(0(x_1)) = 1 + x_1 The following Dependency Pairs can be deleted: EQ(1(x), 1(y)) -> EQ(x, y) EQ(0(x), 0(y)) -> EQ(x, y) This transformation is resulting in no new subcycles. SCC8: APP(cons(x, l1), l2) -> APP(l1, l2) 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(APP(x_1, x_2)) = 1 + x_1 + x_2 POL(cons(x_1, x_2)) = 1 + x_1 + x_2 The following Dependency Pairs can be deleted: APP(cons(x, l1), l2) -> APP(l1, l2) This transformation is resulting in no new subcycles. SCC9: LOG'(1(x)) -> LOG'(x) LOG'(0(x)) -> LOG'(x) 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(x_1)) = 1 + x_1 POL(LOG'(x_1)) = 1 + x_1 POL(0(x_1)) = 1 + x_1 The following Dependency Pairs can be deleted: LOG'(1(x)) -> LOG'(x) LOG'(0(x)) -> LOG'(x) This transformation is resulting in no new subcycles. SCC10: SUM(app(l1, l2)) -> SUM(l2) SUM(app(l1, l2)) -> SUM(l1) SUM(cons(x, l)) -> SUM(l) 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(SUM(x_1)) = 1 + x_1 POL(app(x_1, x_2)) = 1 + x_1 + x_2 POL(cons(x_1, x_2)) = 1 + x_1 + x_2 The following Dependency Pairs can be deleted: SUM(app(l1, l2)) -> SUM(l2) SUM(app(l1, l2)) -> SUM(l1) SUM(cons(x, l)) -> SUM(l) This transformation is resulting in no new subcycles. SCC11: *'(1(x), y) -> *'(x, y) *'(0(x), y) -> *'(x, y) *'(*(x, y), z) -> *'(y, z) *'(*(x, y), z) -> *'(x, *(y, z)) *'(x, +(y, z)) -> *'(x, z) *'(x, +(y, z)) -> *'(x, y) By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented. No rules need to be oriented. Used ordering: Polynomial ordering with Polynomial interpretation: POL(*(x_1, x_2)) = x_1 + x_2 POL(1(x_1)) = 1 + x_1 POL(*'(x_1, x_2)) = x_1 POL(+(x_1, x_2)) = 0 POL(0(x_1)) = x_1 POL(#) = 0 resulting in one subcycle. SCC11.Polo1: *'(*(x, y), z) -> *'(y, z) *'(*(x, y), z) -> *'(x, *(y, z)) *'(x, +(y, z)) -> *'(x, z) *'(x, +(y, z)) -> *'(x, y) *'(0(x), y) -> *'(x, y) By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented. No rules need to be oriented. Used ordering: Polynomial ordering with Polynomial interpretation: POL(*(x_1, x_2)) = 1 + x_1 + x_2 POL(1(x_1)) = 0 POL(*'(x_1, x_2)) = x_1 POL(+(x_1, x_2)) = 0 POL(0(x_1)) = x_1 POL(#) = 0 resulting in one subcycle. SCC11.Polo1.Polo1: *'(0(x), y) -> *'(x, y) *'(x, +(y, z)) -> *'(x, y) *'(x, +(y, z)) -> *'(x, z) 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(*'(x_1, x_2)) = 1 + x_1 + x_2 POL(+(x_1, x_2)) = 1 + x_1 + x_2 POL(0(x_1)) = 1 + x_1 The following Dependency Pairs can be deleted: *'(0(x), y) -> *'(x, y) *'(x, +(y, z)) -> *'(x, y) *'(x, +(y, z)) -> *'(x, z) This transformation is resulting in no new subcycles. SCC12: MEM(x, cons(y, l)) -> MEM(x, l) 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(MEM(x_1, x_2)) = 1 + x_1 + x_2 POL(cons(x_1, x_2)) = 1 + x_1 + x_2 The following Dependency Pairs can be deleted: MEM(x, cons(y, l)) -> MEM(x, l) This transformation is resulting in no new subcycles. SCC13: PROD(cons(x, l)) -> PROD(l) PROD(app(l1, l2)) -> PROD(l2) PROD(app(l1, l2)) -> PROD(l1) 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(PROD(x_1)) = 1 + x_1 POL(app(x_1, x_2)) = 1 + x_1 + x_2 POL(cons(x_1, x_2)) = 1 + x_1 + x_2 The following Dependency Pairs can be deleted: PROD(cons(x, l)) -> PROD(l) PROD(app(l1, l2)) -> PROD(l2) PROD(app(l1, l2)) -> PROD(l1) This transformation is resulting in no new subcycles. SCC14: IFINTER(true, x, l1, l2) -> INTER(l1, l2) INTER(cons(x, l1), l2) -> IFINTER(mem(x, l2), x, l1, l2) INTER(l1, app(l2, l3)) -> INTER(l1, l3) INTER(l1, app(l2, l3)) -> INTER(l1, l2) INTER(app(l1, l2), l3) -> INTER(l2, l3) INTER(app(l1, l2), l3) -> INTER(l1, l3) IFINTER(false, x, l1, l2) -> INTER(l1, l2) INTER(l1, cons(x, l2)) -> IFINTER(mem(x, l1), x, l2, l1) By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented. No rules need to be oriented. Used ordering: Polynomial ordering with Polynomial interpretation: POL(nil) = 0 POL(eq(x_1, x_2)) = 0 POL(mem(x_1, x_2)) = 0 POL(0(x_1)) = 0 POL(#) = 0 POL(cons(x_1, x_2)) = 1 + x_2 POL(1(x_1)) = 0 POL(true) = 0 POL(IFINTER(x_1, x_2, x_3, x_4)) = 1 + x_3 + x_4 POL(if(x_1, x_2, x_3)) = 0 POL(INTER(x_1, x_2)) = x_1 + x_2 POL(app(x_1, x_2)) = x_1 + x_2 POL(false) = 0 resulting in one subcycle. SCC14.Polo1: INTER(l1, app(l2, l3)) -> INTER(l1, l2) INTER(app(l1, l2), l3) -> INTER(l2, l3) INTER(app(l1, l2), l3) -> INTER(l1, l3) INTER(l1, app(l2, l3)) -> INTER(l1, l3) 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(INTER(x_1, x_2)) = 1 + x_1 + x_2 POL(app(x_1, x_2)) = 1 + x_1 + x_2 The following Dependency Pairs can be deleted: INTER(l1, app(l2, l3)) -> INTER(l1, l2) INTER(app(l1, l2), l3) -> INTER(l2, l3) INTER(app(l1, l2), l3) -> INTER(l1, l3) INTER(l1, app(l2, l3)) -> INTER(l1, l3) This transformation is resulting in no new subcycles. Termination of R successfully shown. Duration: 5.808 seconds.