YES Term Rewriting System R: [D, KR, M, R, D', R', X] AC [--comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb] -==--osb-X$Elt-csb-osb-X$Elt-csb(D, D) -> true -==--osb-Y$Elt-csb-osb-Y$Elt-csb(KR, KR) -> true -osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(empty, D) -> undefined -osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(--comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R)), D') -> U11(equal-osb-Bool-csb-osb-Bool-csb(not-osb-Bool-csb(-==--osb-X$Elt-csb-osb-X$Elt-csb(D, D')), true), D', M) -osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(--comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R)), D) -> U21(equal-osb-Bool-csb-osb-Bool-csb(-==--osb-Y$Elt-csb-osb-Y$Elt-csb(-osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(M, D), R), true), R) -osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(--comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R)), D) -> U31(equal-osb-Bool-csb-osb-Bool-csb(not-osb-Bool-csb(-==--osb-Y$Elt-csb-osb-Y$Elt-csb(-osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(M, D), R)), true)) U11(tt, D', M) -> -osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(M, D') U21(tt, R) -> R U31(tt) -> undefined U41(tt, D', D, M, R', R) -> --comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(insert-osb-X$Elt-csb-osb-Y$Elt-csb-osb-Mapocb-X-comma-Y-ccb-csb(D, R, M), -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D', R')) equal-osb-Bool-csb-osb-Bool-csb(X, X) -> tt insert-osb-X$Elt-csb-osb-Y$Elt-csb-osb-Mapocb-X-comma-Y-ccb-csb(D, R, empty) -> -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R) insert-osb-X$Elt-csb-osb-Y$Elt-csb-osb-Mapocb-X-comma-Y-ccb-csb(D, R, --comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D', R'))) -> U41(equal-osb-Bool-csb-osb-Bool-csb(not-osb-Bool-csb(-==--osb-X$Elt-csb-osb-X$Elt-csb(D, D')), true), D', D, M, R', R) insert-osb-X$Elt-csb-osb-Y$Elt-csb-osb-Mapocb-X-comma-Y-ccb-csb(D, R, --comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R'))) -> insert-osb-X$Elt-csb-osb-Y$Elt-csb-osb-Mapocb-X-comma-Y-ccb-csb(D, R, M) not-osb-Bool-csb(false) -> true not-osb-Bool-csb(true) -> false Termination of R to be shown. R ->Dependency Pair Analysis R contains the following Dependency Pairs: -OSB---CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB-OSB-X$ELT-CSB(--comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R)), D) -> U31'(equal-osb-Bool-csb-osb-Bool-csb(not-osb-Bool-csb(-==--osb-Y$Elt-csb-osb-Y$Elt-csb(-osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(M, D), R)), true)) -OSB---CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB-OSB-X$ELT-CSB(--comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R)), D) -> EQUAL-OSB-BOOL-CSB-OSB-BOOL-CSB(not-osb-Bool-csb(-==--osb-Y$Elt-csb-osb-Y$Elt-csb(-osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(M, D), R)), true) -OSB---CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB-OSB-X$ELT-CSB(--comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R)), D) -> NOT-OSB-BOOL-CSB(-==--osb-Y$Elt-csb-osb-Y$Elt-csb(-osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(M, D), R)) -OSB---CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB-OSB-X$ELT-CSB(--comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R)), D) -> -==--OSB-Y$ELT-CSB-OSB-Y$ELT-CSB(-osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(M, D), R) -OSB---CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB-OSB-X$ELT-CSB(--comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R)), D) -> -OSB---CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB-OSB-X$ELT-CSB(M, D) -OSB---CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB-OSB-X$ELT-CSB(--comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R)), D') -> U11'(equal-osb-Bool-csb-osb-Bool-csb(not-osb-Bool-csb(-==--osb-X$Elt-csb-osb-X$Elt-csb(D, D')), true), D', M) -OSB---CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB-OSB-X$ELT-CSB(--comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R)), D') -> EQUAL-OSB-BOOL-CSB-OSB-BOOL-CSB(not-osb-Bool-csb(-==--osb-X$Elt-csb-osb-X$Elt-csb(D, D')), true) -OSB---CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB-OSB-X$ELT-CSB(--comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R)), D') -> NOT-OSB-BOOL-CSB(-==--osb-X$Elt-csb-osb-X$Elt-csb(D, D')) -OSB---CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB-OSB-X$ELT-CSB(--comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R)), D') -> -==--OSB-X$ELT-CSB-OSB-X$ELT-CSB(D, D') -OSB---CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB-OSB-X$ELT-CSB(--comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R)), D) -> U21'(equal-osb-Bool-csb-osb-Bool-csb(-==--osb-Y$Elt-csb-osb-Y$Elt-csb(-osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(M, D), R), true), R) -OSB---CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB-OSB-X$ELT-CSB(--comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R)), D) -> EQUAL-OSB-BOOL-CSB-OSB-BOOL-CSB(-==--osb-Y$Elt-csb-osb-Y$Elt-csb(-osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(M, D), R), true) INSERT-OSB-X$ELT-CSB-OSB-Y$ELT-CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB(D, R, --comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R'))) -> INSERT-OSB-X$ELT-CSB-OSB-Y$ELT-CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB(D, R, M) INSERT-OSB-X$ELT-CSB-OSB-Y$ELT-CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB(D, R, --comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D', R'))) -> U41'(equal-osb-Bool-csb-osb-Bool-csb(not-osb-Bool-csb(-==--osb-X$Elt-csb-osb-X$Elt-csb(D, D')), true), D', D, M, R', R) INSERT-OSB-X$ELT-CSB-OSB-Y$ELT-CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB(D, R, --comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D', R'))) -> EQUAL-OSB-BOOL-CSB-OSB-BOOL-CSB(not-osb-Bool-csb(-==--osb-X$Elt-csb-osb-X$Elt-csb(D, D')), true) INSERT-OSB-X$ELT-CSB-OSB-Y$ELT-CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB(D, R, --comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D', R'))) -> NOT-OSB-BOOL-CSB(-==--osb-X$Elt-csb-osb-X$Elt-csb(D, D')) INSERT-OSB-X$ELT-CSB-OSB-Y$ELT-CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB(D, R, --comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D', R'))) -> -==--OSB-X$ELT-CSB-OSB-X$ELT-CSB(D, D') U11'(tt, D', M) -> -OSB---CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB-OSB-X$ELT-CSB(M, D') U41'(tt, D', D, M, R', R) -> INSERT-OSB-X$ELT-CSB-OSB-Y$ELT-CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB(D, R, M) Furthermore, R contains two SCCs. R ->DPs ->DP Problem 1 ->Polynomial Ordering ->DP Problem 2 ->Polo Dependency Pairs: U11'(tt, D', M) -> -OSB---CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB-OSB-X$ELT-CSB(M, D') -OSB---CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB-OSB-X$ELT-CSB(--comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R)), D') -> U11'(equal-osb-Bool-csb-osb-Bool-csb(not-osb-Bool-csb(-==--osb-X$Elt-csb-osb-X$Elt-csb(D, D')), true), D', M) -OSB---CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB-OSB-X$ELT-CSB(--comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R)), D) -> -OSB---CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB-OSB-X$ELT-CSB(M, D) Rules: -==--osb-Y$Elt-csb-osb-Y$Elt-csb(KR, KR) -> true -osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(--comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R)), D) -> U31(equal-osb-Bool-csb-osb-Bool-csb(not-osb-Bool-csb(-==--osb-Y$Elt-csb-osb-Y$Elt-csb(-osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(M, D), R)), true)) -osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(--comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R)), D') -> U11(equal-osb-Bool-csb-osb-Bool-csb(not-osb-Bool-csb(-==--osb-X$Elt-csb-osb-X$Elt-csb(D, D')), true), D', M) -osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(empty, D) -> undefined -osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(--comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R)), D) -> U21(equal-osb-Bool-csb-osb-Bool-csb(-==--osb-Y$Elt-csb-osb-Y$Elt-csb(-osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(M, D), R), true), R) U31(tt) -> undefined equal-osb-Bool-csb-osb-Bool-csb(X, X) -> tt not-osb-Bool-csb(false) -> true not-osb-Bool-csb(true) -> false insert-osb-X$Elt-csb-osb-Y$Elt-csb-osb-Mapocb-X-comma-Y-ccb-csb(D, R, empty) -> -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R) insert-osb-X$Elt-csb-osb-Y$Elt-csb-osb-Mapocb-X-comma-Y-ccb-csb(D, R, --comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R'))) -> insert-osb-X$Elt-csb-osb-Y$Elt-csb-osb-Mapocb-X-comma-Y-ccb-csb(D, R, M) insert-osb-X$Elt-csb-osb-Y$Elt-csb-osb-Mapocb-X-comma-Y-ccb-csb(D, R, --comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D', R'))) -> U41(equal-osb-Bool-csb-osb-Bool-csb(not-osb-Bool-csb(-==--osb-X$Elt-csb-osb-X$Elt-csb(D, D')), true), D', D, M, R', R) U11(tt, D', M) -> -osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(M, D') -==--osb-X$Elt-csb-osb-X$Elt-csb(D, D) -> true U41(tt, D', D, M, R', R) -> --comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(insert-osb-X$Elt-csb-osb-Y$Elt-csb-osb-Mapocb-X-comma-Y-ccb-csb(D, R, M), -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D', R')) U21(tt, R) -> R The following dependency pairs can be strictly oriented: -OSB---CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB-OSB-X$ELT-CSB(--comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R)), D') -> U11'(equal-osb-Bool-csb-osb-Bool-csb(not-osb-Bool-csb(-==--osb-X$Elt-csb-osb-X$Elt-csb(D, D')), true), D', M) -OSB---CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB-OSB-X$ELT-CSB(--comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R)), D) -> -OSB---CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB-OSB-X$ELT-CSB(M, D) Additionally, the following usable rules w.r.t. the implicit AFS can be oriented: -==--osb-X$Elt-csb-osb-X$Elt-csb(D, D) -> true equal-osb-Bool-csb-osb-Bool-csb(X, X) -> tt not-osb-Bool-csb(false) -> true not-osb-Bool-csb(true) -> false Used ordering: Polynomial ordering with Polynomial interpretation: POL(-OSB---CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB-OSB-X$ELT-CSB(xo1, xo2)) = xo1 POL(--comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(xo1, xo2)) = xo1 + xo2 POL(-==--osb-X$Elt-csb-osb-X$Elt-csb(xo1, xo2)) = 0 POL(false) = 0 POL(equal-osb-Bool-csb-osb-Bool-csb(xo1, xo2)) = 0 POL(-|->--osb-X$Elt-csb-osb-Y$Elt-csb(xo1, xo2)) = 1 POL(true) = 0 POL(U11'(xo1, xo2, xo3)) = xo3 POL(not-osb-Bool-csb(xo1)) = 0 POL(tt) = 0 resulting in one new DP problem. R ->DPs ->DP Problem 1 ->Polo ->DP Problem 3 ->Dependency Graph ->DP Problem 2 ->Polo Dependency Pair: U11'(tt, D', M) -> -OSB---CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB-OSB-X$ELT-CSB(M, D') Rules: -==--osb-Y$Elt-csb-osb-Y$Elt-csb(KR, KR) -> true -osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(--comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R)), D) -> U31(equal-osb-Bool-csb-osb-Bool-csb(not-osb-Bool-csb(-==--osb-Y$Elt-csb-osb-Y$Elt-csb(-osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(M, D), R)), true)) -osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(--comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R)), D') -> U11(equal-osb-Bool-csb-osb-Bool-csb(not-osb-Bool-csb(-==--osb-X$Elt-csb-osb-X$Elt-csb(D, D')), true), D', M) -osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(empty, D) -> undefined -osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(--comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R)), D) -> U21(equal-osb-Bool-csb-osb-Bool-csb(-==--osb-Y$Elt-csb-osb-Y$Elt-csb(-osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(M, D), R), true), R) U31(tt) -> undefined equal-osb-Bool-csb-osb-Bool-csb(X, X) -> tt not-osb-Bool-csb(false) -> true not-osb-Bool-csb(true) -> false insert-osb-X$Elt-csb-osb-Y$Elt-csb-osb-Mapocb-X-comma-Y-ccb-csb(D, R, empty) -> -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R) insert-osb-X$Elt-csb-osb-Y$Elt-csb-osb-Mapocb-X-comma-Y-ccb-csb(D, R, --comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R'))) -> insert-osb-X$Elt-csb-osb-Y$Elt-csb-osb-Mapocb-X-comma-Y-ccb-csb(D, R, M) insert-osb-X$Elt-csb-osb-Y$Elt-csb-osb-Mapocb-X-comma-Y-ccb-csb(D, R, --comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D', R'))) -> U41(equal-osb-Bool-csb-osb-Bool-csb(not-osb-Bool-csb(-==--osb-X$Elt-csb-osb-X$Elt-csb(D, D')), true), D', D, M, R', R) U11(tt, D', M) -> -osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(M, D') -==--osb-X$Elt-csb-osb-X$Elt-csb(D, D) -> true U41(tt, D', D, M, R', R) -> --comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(insert-osb-X$Elt-csb-osb-Y$Elt-csb-osb-Mapocb-X-comma-Y-ccb-csb(D, R, M), -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D', R')) U21(tt, R) -> R Using the Dependency Graph resulted in no new DP problems. R ->DPs ->DP Problem 1 ->Polo ->DP Problem 2 ->Polynomial Ordering Dependency Pairs: U41'(tt, D', D, M, R', R) -> INSERT-OSB-X$ELT-CSB-OSB-Y$ELT-CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB(D, R, M) INSERT-OSB-X$ELT-CSB-OSB-Y$ELT-CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB(D, R, --comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D', R'))) -> U41'(equal-osb-Bool-csb-osb-Bool-csb(not-osb-Bool-csb(-==--osb-X$Elt-csb-osb-X$Elt-csb(D, D')), true), D', D, M, R', R) INSERT-OSB-X$ELT-CSB-OSB-Y$ELT-CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB(D, R, --comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R'))) -> INSERT-OSB-X$ELT-CSB-OSB-Y$ELT-CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB(D, R, M) Rules: -==--osb-Y$Elt-csb-osb-Y$Elt-csb(KR, KR) -> true -osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(--comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R)), D) -> U31(equal-osb-Bool-csb-osb-Bool-csb(not-osb-Bool-csb(-==--osb-Y$Elt-csb-osb-Y$Elt-csb(-osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(M, D), R)), true)) -osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(--comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R)), D') -> U11(equal-osb-Bool-csb-osb-Bool-csb(not-osb-Bool-csb(-==--osb-X$Elt-csb-osb-X$Elt-csb(D, D')), true), D', M) -osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(empty, D) -> undefined -osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(--comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R)), D) -> U21(equal-osb-Bool-csb-osb-Bool-csb(-==--osb-Y$Elt-csb-osb-Y$Elt-csb(-osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(M, D), R), true), R) U31(tt) -> undefined equal-osb-Bool-csb-osb-Bool-csb(X, X) -> tt not-osb-Bool-csb(false) -> true not-osb-Bool-csb(true) -> false insert-osb-X$Elt-csb-osb-Y$Elt-csb-osb-Mapocb-X-comma-Y-ccb-csb(D, R, empty) -> -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R) insert-osb-X$Elt-csb-osb-Y$Elt-csb-osb-Mapocb-X-comma-Y-ccb-csb(D, R, --comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R'))) -> insert-osb-X$Elt-csb-osb-Y$Elt-csb-osb-Mapocb-X-comma-Y-ccb-csb(D, R, M) insert-osb-X$Elt-csb-osb-Y$Elt-csb-osb-Mapocb-X-comma-Y-ccb-csb(D, R, --comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D', R'))) -> U41(equal-osb-Bool-csb-osb-Bool-csb(not-osb-Bool-csb(-==--osb-X$Elt-csb-osb-X$Elt-csb(D, D')), true), D', D, M, R', R) U11(tt, D', M) -> -osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(M, D') -==--osb-X$Elt-csb-osb-X$Elt-csb(D, D) -> true U41(tt, D', D, M, R', R) -> --comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(insert-osb-X$Elt-csb-osb-Y$Elt-csb-osb-Mapocb-X-comma-Y-ccb-csb(D, R, M), -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D', R')) U21(tt, R) -> R The following dependency pairs can be strictly oriented: INSERT-OSB-X$ELT-CSB-OSB-Y$ELT-CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB(D, R, --comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D', R'))) -> U41'(equal-osb-Bool-csb-osb-Bool-csb(not-osb-Bool-csb(-==--osb-X$Elt-csb-osb-X$Elt-csb(D, D')), true), D', D, M, R', R) INSERT-OSB-X$ELT-CSB-OSB-Y$ELT-CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB(D, R, --comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R'))) -> INSERT-OSB-X$ELT-CSB-OSB-Y$ELT-CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB(D, R, M) Additionally, the following usable rules w.r.t. the implicit AFS can be oriented: -==--osb-X$Elt-csb-osb-X$Elt-csb(D, D) -> true equal-osb-Bool-csb-osb-Bool-csb(X, X) -> tt not-osb-Bool-csb(false) -> true not-osb-Bool-csb(true) -> false Used ordering: Polynomial ordering with Polynomial interpretation: POL(--comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(xo1, xo2)) = 1 + xo1 POL(-==--osb-X$Elt-csb-osb-X$Elt-csb(xo1, xo2)) = 0 POL(false) = 0 POL(INSERT-OSB-X$ELT-CSB-OSB-Y$ELT-CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB(xo1, xo2, xo3)) = xo3 POL(equal-osb-Bool-csb-osb-Bool-csb(xo1, xo2)) = 0 POL(-|->--osb-X$Elt-csb-osb-Y$Elt-csb(xo1, xo2)) = 0 POL(true) = 0 POL(U41'(xo1, xo2, xo3, xo4, xo5, xo6)) = xo4 POL(not-osb-Bool-csb(xo1)) = 0 POL(tt) = 0 resulting in one new DP problem. R ->DPs ->DP Problem 1 ->Polo ->DP Problem 2 ->Polo ->DP Problem 4 ->Dependency Graph Dependency Pair: U41'(tt, D', D, M, R', R) -> INSERT-OSB-X$ELT-CSB-OSB-Y$ELT-CSB-OSB-MAPOCB-X-COMMA-Y-CCB-CSB(D, R, M) Rules: -==--osb-Y$Elt-csb-osb-Y$Elt-csb(KR, KR) -> true -osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(--comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R)), D) -> U31(equal-osb-Bool-csb-osb-Bool-csb(not-osb-Bool-csb(-==--osb-Y$Elt-csb-osb-Y$Elt-csb(-osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(M, D), R)), true)) -osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(--comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R)), D') -> U11(equal-osb-Bool-csb-osb-Bool-csb(not-osb-Bool-csb(-==--osb-X$Elt-csb-osb-X$Elt-csb(D, D')), true), D', M) -osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(empty, D) -> undefined -osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(--comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R)), D) -> U21(equal-osb-Bool-csb-osb-Bool-csb(-==--osb-Y$Elt-csb-osb-Y$Elt-csb(-osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(M, D), R), true), R) U31(tt) -> undefined equal-osb-Bool-csb-osb-Bool-csb(X, X) -> tt not-osb-Bool-csb(false) -> true not-osb-Bool-csb(true) -> false insert-osb-X$Elt-csb-osb-Y$Elt-csb-osb-Mapocb-X-comma-Y-ccb-csb(D, R, empty) -> -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R) insert-osb-X$Elt-csb-osb-Y$Elt-csb-osb-Mapocb-X-comma-Y-ccb-csb(D, R, --comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D, R'))) -> insert-osb-X$Elt-csb-osb-Y$Elt-csb-osb-Mapocb-X-comma-Y-ccb-csb(D, R, M) insert-osb-X$Elt-csb-osb-Y$Elt-csb-osb-Mapocb-X-comma-Y-ccb-csb(D, R, --comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(M, -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D', R'))) -> U41(equal-osb-Bool-csb-osb-Bool-csb(not-osb-Bool-csb(-==--osb-X$Elt-csb-osb-X$Elt-csb(D, D')), true), D', D, M, R', R) U11(tt, D', M) -> -osb---csb-osb-Mapocb-X-comma-Y-ccb-csb-osb-X$Elt-csb(M, D') -==--osb-X$Elt-csb-osb-X$Elt-csb(D, D) -> true U41(tt, D', D, M, R', R) -> --comma---osb-Mapocb-X-comma-Y-ccb-csb-osb-Mapocb-X-comma-Y-ccb-csb(insert-osb-X$Elt-csb-osb-Y$Elt-csb-osb-Mapocb-X-comma-Y-ccb-csb(D, R, M), -|->--osb-X$Elt-csb-osb-Y$Elt-csb(D', R')) U21(tt, R) -> R Using the Dependency Graph resulted in no new DP problems. Termination of R successfully shown. Duration: 0:00 minutes