R
↳Dependency Pair Analysis
REC(rec(x)) -> SENT(rec(x))
REC(sent(x)) -> SENT(rec(x))
REC(sent(x)) -> REC(x)
REC(no(x)) -> SENT(rec(x))
REC(no(x)) -> REC(x)
REC(bot) -> SENT(bot)
REC(up(x)) -> REC(x)
SENT(up(x)) -> SENT(x)
NO(up(x)) -> NO(x)
TOP(rec(up(x))) -> TOP(check(rec(x)))
TOP(rec(up(x))) -> CHECK(rec(x))
TOP(rec(up(x))) -> REC(x)
TOP(sent(up(x))) -> TOP(check(rec(x)))
TOP(sent(up(x))) -> CHECK(rec(x))
TOP(sent(up(x))) -> REC(x)
TOP(no(up(x))) -> TOP(check(rec(x)))
TOP(no(up(x))) -> CHECK(rec(x))
TOP(no(up(x))) -> REC(x)
CHECK(up(x)) -> CHECK(x)
CHECK(sent(x)) -> SENT(check(x))
CHECK(sent(x)) -> CHECK(x)
CHECK(rec(x)) -> REC(check(x))
CHECK(rec(x)) -> CHECK(x)
CHECK(no(x)) -> NO(check(x))
CHECK(no(x)) -> CHECK(x)
R
↳DPs
→DP Problem 1
↳Polynomial Ordering
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 4
↳Polo
→DP Problem 5
↳Polo
SENT(up(x)) -> SENT(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)
SENT(up(x)) -> SENT(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)
POL(top(x1)) = 0 POL(rec(x1)) = 1 + x1 POL(no(x1)) = x1 POL(bot) = 0 POL(up(x1)) = 1 + x1 POL(check(x1)) = x1 POL(sent(x1)) = x1 POL(SENT(x1)) = x1
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 6
↳Dependency Graph
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 4
↳Polo
→DP Problem 5
↳Polo
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)
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polynomial Ordering
→DP Problem 3
↳Polo
→DP Problem 4
↳Polo
→DP Problem 5
↳Polo
NO(up(x)) -> NO(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)
NO(up(x)) -> NO(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)
POL(top(x1)) = 0 POL(rec(x1)) = 1 + x1 POL(no(x1)) = x1 POL(bot) = 0 POL(NO(x1)) = x1 POL(up(x1)) = 1 + x1 POL(check(x1)) = x1 POL(sent(x1)) = x1
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 7
↳Dependency Graph
→DP Problem 3
↳Polo
→DP Problem 4
↳Polo
→DP Problem 5
↳Polo
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)
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Polynomial Ordering
→DP Problem 4
↳Polo
→DP Problem 5
↳Polo
REC(up(x)) -> REC(x)
REC(no(x)) -> REC(x)
REC(sent(x)) -> REC(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)
REC(no(x)) -> REC(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)
POL(top(x1)) = 0 POL(rec(x1)) = 0 POL(no(x1)) = 1 + x1 POL(bot) = 0 POL(up(x1)) = x1 POL(check(x1)) = x1 POL(REC(x1)) = x1 POL(sent(x1)) = x1
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 8
↳Polynomial Ordering
→DP Problem 4
↳Polo
→DP Problem 5
↳Polo
REC(up(x)) -> REC(x)
REC(sent(x)) -> REC(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)
REC(sent(x)) -> REC(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)
POL(top(x1)) = 0 POL(rec(x1)) = 1 + x1 POL(no(x1)) = 1 + x1 POL(bot) = 0 POL(up(x1)) = x1 POL(check(x1)) = x1 POL(REC(x1)) = x1 POL(sent(x1)) = 1 + x1
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 8
↳Polo
...
→DP Problem 9
↳Polynomial Ordering
→DP Problem 4
↳Polo
→DP Problem 5
↳Polo
REC(up(x)) -> REC(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)
REC(up(x)) -> REC(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)
POL(top(x1)) = 0 POL(rec(x1)) = 1 + x1 POL(no(x1)) = x1 POL(bot) = 0 POL(up(x1)) = 1 + x1 POL(check(x1)) = x1 POL(REC(x1)) = x1 POL(sent(x1)) = x1
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 8
↳Polo
...
→DP Problem 10
↳Dependency Graph
→DP Problem 4
↳Polo
→DP Problem 5
↳Polo
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)
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 4
↳Polynomial Ordering
→DP Problem 5
↳Polo
CHECK(no(x)) -> CHECK(x)
CHECK(rec(x)) -> CHECK(x)
CHECK(sent(x)) -> CHECK(x)
CHECK(up(x)) -> CHECK(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)
CHECK(no(x)) -> CHECK(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)
POL(top(x1)) = 0 POL(rec(x1)) = x1 POL(no(x1)) = 1 + x1 POL(bot) = 0 POL(up(x1)) = x1 POL(check(x1)) = x1 POL(CHECK(x1)) = x1 POL(sent(x1)) = x1
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 4
↳Polo
→DP Problem 11
↳Polynomial Ordering
→DP Problem 5
↳Polo
CHECK(rec(x)) -> CHECK(x)
CHECK(sent(x)) -> CHECK(x)
CHECK(up(x)) -> CHECK(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)
CHECK(rec(x)) -> CHECK(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)
POL(top(x1)) = 0 POL(rec(x1)) = 1 + x1 POL(no(x1)) = x1 POL(bot) = 0 POL(up(x1)) = x1 POL(check(x1)) = x1 POL(CHECK(x1)) = x1 POL(sent(x1)) = x1
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 4
↳Polo
→DP Problem 11
↳Polo
...
→DP Problem 12
↳Polynomial Ordering
→DP Problem 5
↳Polo
CHECK(sent(x)) -> CHECK(x)
CHECK(up(x)) -> CHECK(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)
CHECK(sent(x)) -> CHECK(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)
POL(top(x1)) = 0 POL(rec(x1)) = 1 + x1 POL(no(x1)) = 1 + x1 POL(bot) = 0 POL(up(x1)) = x1 POL(check(x1)) = x1 POL(CHECK(x1)) = x1 POL(sent(x1)) = 1 + x1
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 4
↳Polo
→DP Problem 11
↳Polo
...
→DP Problem 13
↳Polynomial Ordering
→DP Problem 5
↳Polo
CHECK(up(x)) -> CHECK(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)
CHECK(up(x)) -> CHECK(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)
POL(top(x1)) = 0 POL(rec(x1)) = 1 + x1 POL(no(x1)) = x1 POL(bot) = 0 POL(up(x1)) = 1 + x1 POL(check(x1)) = x1 POL(CHECK(x1)) = x1 POL(sent(x1)) = x1
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 4
↳Polo
→DP Problem 11
↳Polo
...
→DP Problem 14
↳Dependency Graph
→DP Problem 5
↳Polo
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)
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 4
↳Polo
→DP Problem 5
↳Polynomial Ordering
TOP(no(up(x))) -> TOP(check(rec(x)))
TOP(sent(up(x))) -> TOP(check(rec(x)))
TOP(rec(up(x))) -> TOP(check(rec(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)
TOP(no(up(x))) -> TOP(check(rec(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)
POL(top(x1)) = 0 POL(rec(x1)) = 0 POL(no(x1)) = 1 POL(bot) = 0 POL(up(x1)) = 0 POL(check(x1)) = x1 POL(TOP(x1)) = x1 POL(sent(x1)) = 0
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 4
↳Polo
→DP Problem 5
↳Polo
→DP Problem 15
↳Polynomial Ordering
TOP(sent(up(x))) -> TOP(check(rec(x)))
TOP(rec(up(x))) -> TOP(check(rec(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)
TOP(rec(up(x))) -> TOP(check(rec(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)
POL(top(x1)) = 1 POL(rec(x1)) = 1 + x1 POL(no(x1)) = x1 POL(bot) = 0 POL(up(x1)) = 1 + x1 POL(check(x1)) = x1 POL(TOP(x1)) = x1 POL(sent(x1)) = x1
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 4
↳Polo
→DP Problem 5
↳Polo
→DP Problem 15
↳Polo
...
→DP Problem 16
↳Narrowing Transformation
TOP(sent(up(x))) -> TOP(check(rec(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)
six new Dependency Pairs are created:
TOP(sent(up(x))) -> TOP(check(rec(x)))
TOP(sent(up(x''))) -> TOP(rec(check(x'')))
TOP(sent(up(rec(x'')))) -> TOP(check(sent(rec(x''))))
TOP(sent(up(sent(x'')))) -> TOP(check(sent(rec(x''))))
TOP(sent(up(no(x'')))) -> TOP(check(sent(rec(x''))))
TOP(sent(up(bot))) -> TOP(check(up(sent(bot))))
TOP(sent(up(up(x'')))) -> TOP(check(up(rec(x''))))
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 4
↳Polo
→DP Problem 5
↳Polo
→DP Problem 15
↳Polo
...
→DP Problem 17
↳Polynomial Ordering
TOP(sent(up(up(x'')))) -> TOP(check(up(rec(x''))))
TOP(sent(up(bot))) -> TOP(check(up(sent(bot))))
TOP(sent(up(no(x'')))) -> TOP(check(sent(rec(x''))))
TOP(sent(up(sent(x'')))) -> TOP(check(sent(rec(x''))))
TOP(sent(up(rec(x'')))) -> TOP(check(sent(rec(x''))))
TOP(sent(up(x''))) -> TOP(rec(check(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)
TOP(sent(up(up(x'')))) -> TOP(check(up(rec(x''))))
TOP(sent(up(bot))) -> TOP(check(up(sent(bot))))
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)
POL(top(x1)) = 0 POL(rec(x1)) = 1 POL(no(x1)) = 0 POL(bot) = 0 POL(up(x1)) = 0 POL(check(x1)) = x1 POL(TOP(x1)) = x1 POL(sent(x1)) = 1
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 4
↳Polo
→DP Problem 5
↳Polo
→DP Problem 15
↳Polo
...
→DP Problem 18
↳Polynomial Ordering
TOP(sent(up(no(x'')))) -> TOP(check(sent(rec(x''))))
TOP(sent(up(sent(x'')))) -> TOP(check(sent(rec(x''))))
TOP(sent(up(rec(x'')))) -> TOP(check(sent(rec(x''))))
TOP(sent(up(x''))) -> TOP(rec(check(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)
TOP(sent(up(no(x'')))) -> TOP(check(sent(rec(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)
POL(top(x1)) = 1 POL(rec(x1)) = 0 POL(no(x1)) = 1 POL(bot) = 0 POL(up(x1)) = x1 POL(check(x1)) = x1 POL(TOP(x1)) = 1 + x1 POL(sent(x1)) = x1
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 4
↳Polo
→DP Problem 5
↳Polo
→DP Problem 15
↳Polo
...
→DP Problem 19
↳Polynomial Ordering
TOP(sent(up(sent(x'')))) -> TOP(check(sent(rec(x''))))
TOP(sent(up(rec(x'')))) -> TOP(check(sent(rec(x''))))
TOP(sent(up(x''))) -> TOP(rec(check(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)
TOP(sent(up(rec(x'')))) -> TOP(check(sent(rec(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)
POL(top(x1)) = 1 POL(rec(x1)) = 1 + x1 POL(no(x1)) = x1 POL(bot) = 0 POL(up(x1)) = 1 + x1 POL(check(x1)) = x1 POL(TOP(x1)) = 1 + x1 POL(sent(x1)) = x1
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 4
↳Polo
→DP Problem 5
↳Polo
→DP Problem 15
↳Polo
...
→DP Problem 20
↳Remaining Obligation(s)
TOP(sent(up(sent(x'')))) -> TOP(check(sent(rec(x''))))
TOP(sent(up(x''))) -> TOP(rec(check(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)