Term Rewriting System R: [x] rec(rec(x)) -> sent(rec(x)) rec(sent(x)) -> sent(rec(x)) rec(no(x)) -> sent(rec(x)) rec(bot) -> up(sent(bot)) rec(up(x)) -> up(rec(x)) sent(up(x)) -> up(sent(x)) no(up(x)) -> up(no(x)) top(rec(up(x))) -> top(check(rec(x))) top(sent(up(x))) -> top(check(rec(x))) top(no(up(x))) -> top(check(rec(x))) check(up(x)) -> up(check(x)) check(sent(x)) -> sent(check(x)) check(rec(x)) -> rec(check(x)) check(no(x)) -> no(check(x)) check(no(x)) -> no(x) Termination of R to be shown. Removing the following rules from R which fullfill a polynomial ordering: rec(no(x)) -> sent(rec(x)) top(no(up(x))) -> top(check(rec(x))) where the Polynomial interpretation: POL(top(x_1)) = 1 + x_1 POL(no(x_1)) = 1 + x_1 POL(check(x_1)) = x_1 POL(bot) = 0 POL(rec(x_1)) = x_1 POL(sent(x_1)) = x_1 POL(up(x_1)) = x_1 was used. Not all Rules of R can be deleted, so we still have to regard a part of R. Removing the following rules from R which fullfill a polynomial ordering: rec(rec(x)) -> sent(rec(x)) top(rec(up(x))) -> top(check(rec(x))) where the Polynomial interpretation: POL(top(x_1)) = 1 + x_1 POL(no(x_1)) = x_1 POL(check(x_1)) = x_1 POL(bot) = 0 POL(rec(x_1)) = 1 + x_1 POL(sent(x_1)) = x_1 POL(up(x_1)) = 1 + x_1 was used. Not all Rules of R can be deleted, so we still have to regard a part of R. Removing the following rules from R which fullfill a polynomial ordering: check(no(x)) -> no(check(x)) check(no(x)) -> no(x) where the Polynomial interpretation: POL(top(x_1)) = x_1 POL(no(x_1)) = 1 + x_1 POL(check(x_1)) = 2*x_1 POL(bot) = 0 POL(rec(x_1)) = x_1 POL(sent(x_1)) = 2*x_1 POL(up(x_1)) = x_1 was used. Not all Rules of R can be deleted, so we still have to regard a part of R. Removing the following rules from R which fullfill a polynomial ordering: no(up(x)) -> up(no(x)) where the Polynomial interpretation: POL(top(x_1)) = 1 + x_1 POL(no(x_1)) = 2*x_1 POL(check(x_1)) = x_1 POL(bot) = 0 POL(rec(x_1)) = 1 + x_1 POL(sent(x_1)) = x_1 POL(up(x_1)) = 1 + x_1 was used. Not all Rules of R can be deleted, so we still have to regard a part of R. R contains the following Dependency Pairs: SENT(up(x)) -> SENT(x) REC(bot) -> SENT(bot) REC(up(x)) -> REC(x) REC(sent(x)) -> SENT(rec(x)) REC(sent(x)) -> REC(x) CHECK(rec(x)) -> REC(check(x)) CHECK(rec(x)) -> CHECK(x) CHECK(up(x)) -> CHECK(x) CHECK(sent(x)) -> SENT(check(x)) CHECK(sent(x)) -> CHECK(x) TOP(sent(up(x))) -> TOP(check(rec(x))) TOP(sent(up(x))) -> CHECK(rec(x)) TOP(sent(up(x))) -> REC(x) Furthermore, R contains four SCCs. SCC1: SENT(up(x)) -> SENT(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(SENT(x_1)) = 2 + x_1 POL(up(x_1)) = 2 + x_1 The following Dependency Pairs can be deleted: SENT(up(x)) -> SENT(x) This transformation is resulting in no new subcycles. SCC2: REC(sent(x)) -> REC(x) REC(up(x)) -> REC(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(REC(x_1)) = 2 + x_1 POL(sent(x_1)) = 2 + x_1 POL(up(x_1)) = 2 + x_1 The following Dependency Pairs can be deleted: REC(sent(x)) -> REC(x) REC(up(x)) -> REC(x) This transformation is resulting in no new subcycles. SCC3: CHECK(sent(x)) -> CHECK(x) CHECK(up(x)) -> CHECK(x) CHECK(rec(x)) -> CHECK(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(CHECK(x_1)) = 2 + x_1 POL(rec(x_1)) = 2 + x_1 POL(sent(x_1)) = 2 + x_1 POL(up(x_1)) = 2 + x_1 The following Dependency Pairs can be deleted: CHECK(sent(x)) -> CHECK(x) CHECK(up(x)) -> CHECK(x) CHECK(rec(x)) -> CHECK(x) This transformation is resulting in no new subcycles. SCC4: TOP(sent(up(x))) -> TOP(check(rec(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(TOP(x_1)) = 1 + x_1 POL(check(x_1)) = x_1 POL(bot) = 0 POL(rec(x_1)) = x_1 POL(sent(x_1)) = x_1 POL(up(x_1)) = x_1 No Dependency Pairs can be deleted. The following rules of R can be deleted: top(sent(up(x))) -> top(check(rec(x))) This transformation is resulting in one new subcycle: SCC4.MRR1: TOP(sent(up(x))) -> TOP(check(rec(x))) Using Semantic Labelling, the Scc could be transformed. The following model was found: sent(x_0) = x_0 up(x_0) = x_0 rec(x_0) = x_0 bot = 0 check(x_0) = 1 TOP(x_0) = 0 The labeled system could be transformed as follows: 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(sent_1(x_1)) = x_1 POL(TOP_1(x_1)) = 1 + x_1 POL(check_1(x_1)) = x_1 POL(up_1(x_1)) = x_1 POL(rec_1(x_1)) = x_1 No Dependency Pairs can be deleted. The following rules of R can be deleted: check_0(rec_0(x)) -> rec_1(check_0(x)) check_0(up_0(x)) -> up_1(check_0(x)) check_0(sent_0(x)) -> sent_1(check_0(x)) rec_0(bot) -> up_0(sent_0(bot)) rec_0(up_0(x)) -> up_0(rec_0(x)) rec_0(sent_0(x)) -> sent_0(rec_0(x)) sent_0(up_0(x)) -> up_0(sent_0(x)) This transformation is resulting in one new subcycle: 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(sent_1(x_1)) = x_1 POL(TOP_1(x_1)) = 1 + x_1 POL(check_1(x_1)) = x_1 POL(up_1(x_1)) = 1 + x_1 POL(rec_1(x_1)) = x_1 The following Dependency Pairs can be deleted: TOP_1(sent_1(up_1(x))) -> TOP_1(check_1(rec_1(x))) This transformation is resulting in no new subcycles. The new TRS has no more cycles! Termination of R successfully shown. Duration: 24.101 seconds.