R
↳Dependency Pair Analysis
ACKIN(s(X), 0) -> U11(ackin(X, s(0)))
ACKIN(s(X), 0) -> ACKIN(X, s(0))
ACKIN(s(X), s(Y)) -> U21(ackin(s(X), Y), X)
ACKIN(s(X), s(Y)) -> ACKIN(s(X), Y)
U21(ackout(X), Y) -> U22(ackin(Y, X))
U21(ackout(X), Y) -> ACKIN(Y, X)
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
ACKIN(s(X), s(Y)) -> ACKIN(s(X), Y)
U21(ackout(X), Y) -> ACKIN(Y, X)
ACKIN(s(X), s(Y)) -> U21(ackin(s(X), Y), X)
ACKIN(s(X), 0) -> ACKIN(X, s(0))
ackin(0, X) -> ackout(s(X))
ackin(s(X), 0) -> u11(ackin(X, s(0)))
ackin(s(X), s(Y)) -> u21(ackin(s(X), Y), X)
u11(ackout(X)) -> ackout(X)
u21(ackout(X), Y) -> u22(ackin(Y, X))
u22(ackout(X)) -> ackout(X)
ACKIN(s(X), s(Y)) -> U21(ackin(s(X), Y), X)
ACKIN(s(X), 0) -> ACKIN(X, s(0))
ackin(0, X) -> ackout(s(X))
ackin(s(X), 0) -> u11(ackin(X, s(0)))
ackin(s(X), s(Y)) -> u21(ackin(s(X), Y), X)
u11(ackout(X)) -> ackout(X)
u21(ackout(X), Y) -> u22(ackin(Y, X))
u22(ackout(X)) -> ackout(X)
POL(u11(x1)) = x1 POL(u22(x1)) = x1 POL(U21(x1, x2)) = x1 + x2 POL(ackin) = 0 POL(s(x1)) = 1 + x1 POL(ackout) = 0
ACKIN(x1, x2) -> x1
s(x1) -> s(x1)
U21(x1, x2) -> U21(x1, x2)
ackin(x1, x2) -> ackin
ackout(x1) -> ackout
u11(x1) -> u11(x1)
u21(x1, x2) -> x1
u22(x1) -> u22(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Dependency Graph
ACKIN(s(X), s(Y)) -> ACKIN(s(X), Y)
U21(ackout(X), Y) -> ACKIN(Y, X)
ackin(0, X) -> ackout(s(X))
ackin(s(X), 0) -> u11(ackin(X, s(0)))
ackin(s(X), s(Y)) -> u21(ackin(s(X), Y), X)
u11(ackout(X)) -> ackout(X)
u21(ackout(X), Y) -> u22(ackin(Y, X))
u22(ackout(X)) -> ackout(X)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳DGraph
...
→DP Problem 3
↳Argument Filtering and Ordering
ACKIN(s(X), s(Y)) -> ACKIN(s(X), Y)
ackin(0, X) -> ackout(s(X))
ackin(s(X), 0) -> u11(ackin(X, s(0)))
ackin(s(X), s(Y)) -> u21(ackin(s(X), Y), X)
u11(ackout(X)) -> ackout(X)
u21(ackout(X), Y) -> u22(ackin(Y, X))
u22(ackout(X)) -> ackout(X)
ACKIN(s(X), s(Y)) -> ACKIN(s(X), Y)
ackin(0, X) -> ackout(s(X))
ackin(s(X), 0) -> u11(ackin(X, s(0)))
ackin(s(X), s(Y)) -> u21(ackin(s(X), Y), X)
u11(ackout(X)) -> ackout(X)
u21(ackout(X), Y) -> u22(ackin(Y, X))
u22(ackout(X)) -> ackout(X)
POL(0) = 0 POL(u11(x1)) = x1 POL(u22) = 0 POL(ackin(x1, x2)) = x1 + x2 POL(s(x1)) = 1 + x1 POL(ACKIN(x1, x2)) = 1 + x1 + x2 POL(ackout) = 0
ACKIN(x1, x2) -> ACKIN(x1, x2)
s(x1) -> s(x1)
ackin(x1, x2) -> ackin(x1, x2)
ackout(x1) -> ackout
u11(x1) -> u11(x1)
u21(x1, x2) -> x1
u22(x1) -> u22
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳DGraph
...
→DP Problem 4
↳Dependency Graph
ackin(0, X) -> ackout(s(X))
ackin(s(X), 0) -> u11(ackin(X, s(0)))
ackin(s(X), s(Y)) -> u21(ackin(s(X), Y), X)
u11(ackout(X)) -> ackout(X)
u21(ackout(X), Y) -> u22(ackin(Y, X))
u22(ackout(X)) -> ackout(X)