(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
plus(s(s(x)), y) → s(plus(x, s(y)))
plus(x, s(s(y))) → s(plus(s(x), y))
plus(s(0), y) → s(y)
plus(0, y) → y
ack(0, y) → s(y)
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, plus(y, ack(s(x), y)))
Q is empty.
(1) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
(2) Obligation:
Q DP problem:
The TRS P consists of the following rules:
PLUS(s(s(x)), y) → PLUS(x, s(y))
PLUS(x, s(s(y))) → PLUS(s(x), y)
ACK(s(x), 0) → ACK(x, s(0))
ACK(s(x), s(y)) → ACK(x, plus(y, ack(s(x), y)))
ACK(s(x), s(y)) → PLUS(y, ack(s(x), y))
ACK(s(x), s(y)) → ACK(s(x), y)
The TRS R consists of the following rules:
plus(s(s(x)), y) → s(plus(x, s(y)))
plus(x, s(s(y))) → s(plus(s(x), y))
plus(s(0), y) → s(y)
plus(0, y) → y
ack(0, y) → s(y)
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, plus(y, ack(s(x), y)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(3) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 1 less node.
(4) Complex Obligation (AND)
(5) Obligation:
Q DP problem:
The TRS P consists of the following rules:
PLUS(x, s(s(y))) → PLUS(s(x), y)
PLUS(s(s(x)), y) → PLUS(x, s(y))
The TRS R consists of the following rules:
plus(s(s(x)), y) → s(plus(x, s(y)))
plus(x, s(s(y))) → s(plus(s(x), y))
plus(s(0), y) → s(y)
plus(0, y) → y
ack(0, y) → s(y)
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, plus(y, ack(s(x), y)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(6) Obligation:
Q DP problem:
The TRS P consists of the following rules:
ACK(s(x), s(y)) → ACK(x, plus(y, ack(s(x), y)))
ACK(s(x), 0) → ACK(x, s(0))
ACK(s(x), s(y)) → ACK(s(x), y)
The TRS R consists of the following rules:
plus(s(s(x)), y) → s(plus(x, s(y)))
plus(x, s(s(y))) → s(plus(s(x), y))
plus(s(0), y) → s(y)
plus(0, y) → y
ack(0, y) → s(y)
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, plus(y, ack(s(x), y)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.