YES Term Rewriting System R: [L, E, L'] conc-osb-Listocb-X-ccb-csb-osb-Listocb-X-ccb-csb(nil, L) -> L conc-osb-Listocb-X-ccb-csb-osb-Listocb-X-ccb-csb(cons-osb-X$Elt-csb-osb-Listocb-X-ccb-csb(E, L), L') -> cons-osb-X$Elt-csb-osb-Listocb-X-ccb-csb(E, conc-osb-Listocb-X-ccb-csb-osb-Listocb-X-ccb-csb(L, L')) Termination of R to be shown. R ->Removing Redundant Rules Removing the following rules from R which fullfill a polynomial ordering: conc-osb-Listocb-X-ccb-csb-osb-Listocb-X-ccb-csb(nil, L) -> L where the Polynomial interpretation: POL(nil) = 1 POL(cons-osb-X$Elt-csb-osb-Listocb-X-ccb-csb(xo1, xo2)) = xo1 + xo2 POL(conc-osb-Listocb-X-ccb-csb-osb-Listocb-X-ccb-csb(xo1, xo2)) = xo1 + xo2 was used. Not all Rules of R can be deleted, so we still have to regard a part of R. R ->RRRPolo ->TRS2 ->Removing Redundant Rules Removing the following rules from R which fullfill a polynomial ordering: conc-osb-Listocb-X-ccb-csb-osb-Listocb-X-ccb-csb(cons-osb-X$Elt-csb-osb-Listocb-X-ccb-csb(E, L), L') -> cons-osb-X$Elt-csb-osb-Listocb-X-ccb-csb(E, conc-osb-Listocb-X-ccb-csb-osb-Listocb-X-ccb-csb(L, L')) where the Polynomial interpretation: POL(cons-osb-X$Elt-csb-osb-Listocb-X-ccb-csb(xo1, xo2)) = 1 + xo1 + xo2 POL(conc-osb-Listocb-X-ccb-csb-osb-Listocb-X-ccb-csb(xo1, xo2)) = 2*xo1 + xo2 was used. All Rules of R can be deleted. R ->RRRPolo ->TRS2 ->RRRPolo ->TRS3 ->Non-Overlappingness Check This program has no overlaps, so it is sufficient to show innermost termination. R ->RRRPolo ->TRS2 ->RRRPolo ->TRS3 ->NOC ... ->TRS4 ->Dependency Pair Analysis R contains no Dependency Pairs and therefore no SCCs. Termination of R successfully shown. Duration: 0:00 minutes