0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 AND
↳5 QDP
↳6 MNOCProof (⇔)
↳7 QDP
↳8 UsableRulesProof (⇔)
↳9 QDP
↳10 QReductionProof (⇔)
↳11 QDP
↳12 MRRProof (⇔)
↳13 QDP
↳14 QDPSizeChangeProof (⇔)
↳15 TRUE
↳16 QDP
↳17 MNOCProof (⇔)
↳18 QDP
↳19 UsableRulesProof (⇔)
↳20 QDP
↳21 QReductionProof (⇔)
↳22 QDP
↳23 QDPSizeChangeProof (⇔)
↳24 TRUE
↳25 QDP
↳26 MNOCProof (⇔)
↳27 QDP
↳28 UsableRulesProof (⇔)
↳29 QDP
↳30 QReductionProof (⇔)
↳31 QDP
↳32 Narrowing (⇔)
↳33 QDP
↳34 DependencyGraphProof (⇔)
↳35 QDP
↳36 UsableRulesProof (⇔)
↳37 QDP
↳38 QReductionProof (⇔)
↳39 QDP
↳40 Instantiation (⇔)
↳41 QDP
↳42 UsableRulesProof (⇔)
↳43 QDP
↳44 Rewriting (⇔)
↳45 QDP
↳46 UsableRulesProof (⇔)
↳47 QDP
↳48 QReductionProof (⇔)
↳49 QDP
↳50 Narrowing (⇔)
↳51 QDP
↳52 ForwardInstantiation (⇔)
↳53 QDP
↳54 QDPSizeChangeProof (⇔)
↳55 TRUE
double(x) → permute(x, x, a)
permute(x, y, a) → permute(isZero(x), x, b)
permute(false, x, b) → permute(ack(x, x), p(x), c)
permute(true, x, b) → 0
permute(y, x, c) → s(s(permute(x, y, a)))
p(0) → 0
p(s(x)) → x
ack(0, x) → plus(x, s(0))
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, ack(s(x), y))
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
plus(x, s(s(y))) → s(plus(s(x), y))
plus(x, s(0)) → s(x)
plus(x, 0) → x
isZero(0) → true
isZero(s(x)) → false
DOUBLE(x) → PERMUTE(x, x, a)
PERMUTE(x, y, a) → PERMUTE(isZero(x), x, b)
PERMUTE(x, y, a) → ISZERO(x)
PERMUTE(false, x, b) → PERMUTE(ack(x, x), p(x), c)
PERMUTE(false, x, b) → ACK(x, x)
PERMUTE(false, x, b) → P(x)
PERMUTE(y, x, c) → PERMUTE(x, y, a)
ACK(0, x) → PLUS(x, s(0))
ACK(s(x), 0) → ACK(x, s(0))
ACK(s(x), s(y)) → ACK(x, ack(s(x), y))
ACK(s(x), s(y)) → ACK(s(x), y)
PLUS(s(x), y) → PLUS(x, s(y))
PLUS(x, s(s(y))) → PLUS(s(x), y)
double(x) → permute(x, x, a)
permute(x, y, a) → permute(isZero(x), x, b)
permute(false, x, b) → permute(ack(x, x), p(x), c)
permute(true, x, b) → 0
permute(y, x, c) → s(s(permute(x, y, a)))
p(0) → 0
p(s(x)) → x
ack(0, x) → plus(x, s(0))
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, ack(s(x), y))
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
plus(x, s(s(y))) → s(plus(s(x), y))
plus(x, s(0)) → s(x)
plus(x, 0) → x
isZero(0) → true
isZero(s(x)) → false
PLUS(x, s(s(y))) → PLUS(s(x), y)
PLUS(s(x), y) → PLUS(x, s(y))
double(x) → permute(x, x, a)
permute(x, y, a) → permute(isZero(x), x, b)
permute(false, x, b) → permute(ack(x, x), p(x), c)
permute(true, x, b) → 0
permute(y, x, c) → s(s(permute(x, y, a)))
p(0) → 0
p(s(x)) → x
ack(0, x) → plus(x, s(0))
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, ack(s(x), y))
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
plus(x, s(s(y))) → s(plus(s(x), y))
plus(x, s(0)) → s(x)
plus(x, 0) → x
isZero(0) → true
isZero(s(x)) → false
PLUS(x, s(s(y))) → PLUS(s(x), y)
PLUS(s(x), y) → PLUS(x, s(y))
double(x) → permute(x, x, a)
permute(x, y, a) → permute(isZero(x), x, b)
permute(false, x, b) → permute(ack(x, x), p(x), c)
permute(true, x, b) → 0
permute(y, x, c) → s(s(permute(x, y, a)))
p(0) → 0
p(s(x)) → x
ack(0, x) → plus(x, s(0))
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, ack(s(x), y))
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
plus(x, s(s(y))) → s(plus(s(x), y))
plus(x, s(0)) → s(x)
plus(x, 0) → x
isZero(0) → true
isZero(s(x)) → false
double(x0)
permute(x0, x1, a)
permute(false, x0, b)
permute(true, x0, b)
permute(x0, x1, c)
p(0)
p(s(x0))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
plus(x0, s(s(x1)))
plus(x0, s(0))
plus(x0, 0)
isZero(0)
isZero(s(x0))
PLUS(x, s(s(y))) → PLUS(s(x), y)
PLUS(s(x), y) → PLUS(x, s(y))
double(x0)
permute(x0, x1, a)
permute(false, x0, b)
permute(true, x0, b)
permute(x0, x1, c)
p(0)
p(s(x0))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
plus(x0, s(s(x1)))
plus(x0, s(0))
plus(x0, 0)
isZero(0)
isZero(s(x0))
double(x0)
permute(x0, x1, a)
permute(false, x0, b)
permute(true, x0, b)
permute(x0, x1, c)
p(0)
p(s(x0))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
plus(x0, s(s(x1)))
plus(x0, s(0))
plus(x0, 0)
isZero(0)
isZero(s(x0))
PLUS(x, s(s(y))) → PLUS(s(x), y)
PLUS(s(x), y) → PLUS(x, s(y))
PLUS(x, s(s(y))) → PLUS(s(x), y)
POL(PLUS(x1, x2)) = x1 + x2
POL(s(x1)) = 1 + x1
PLUS(s(x), y) → PLUS(x, s(y))
From the DPs we obtained the following set of size-change graphs:
ACK(s(x), s(y)) → ACK(x, ack(s(x), y))
ACK(s(x), 0) → ACK(x, s(0))
ACK(s(x), s(y)) → ACK(s(x), y)
double(x) → permute(x, x, a)
permute(x, y, a) → permute(isZero(x), x, b)
permute(false, x, b) → permute(ack(x, x), p(x), c)
permute(true, x, b) → 0
permute(y, x, c) → s(s(permute(x, y, a)))
p(0) → 0
p(s(x)) → x
ack(0, x) → plus(x, s(0))
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, ack(s(x), y))
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
plus(x, s(s(y))) → s(plus(s(x), y))
plus(x, s(0)) → s(x)
plus(x, 0) → x
isZero(0) → true
isZero(s(x)) → false
ACK(s(x), s(y)) → ACK(x, ack(s(x), y))
ACK(s(x), 0) → ACK(x, s(0))
ACK(s(x), s(y)) → ACK(s(x), y)
double(x) → permute(x, x, a)
permute(x, y, a) → permute(isZero(x), x, b)
permute(false, x, b) → permute(ack(x, x), p(x), c)
permute(true, x, b) → 0
permute(y, x, c) → s(s(permute(x, y, a)))
p(0) → 0
p(s(x)) → x
ack(0, x) → plus(x, s(0))
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, ack(s(x), y))
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
plus(x, s(s(y))) → s(plus(s(x), y))
plus(x, s(0)) → s(x)
plus(x, 0) → x
isZero(0) → true
isZero(s(x)) → false
double(x0)
permute(x0, x1, a)
permute(false, x0, b)
permute(true, x0, b)
permute(x0, x1, c)
p(0)
p(s(x0))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
plus(x0, s(s(x1)))
plus(x0, s(0))
plus(x0, 0)
isZero(0)
isZero(s(x0))
ACK(s(x), s(y)) → ACK(x, ack(s(x), y))
ACK(s(x), 0) → ACK(x, s(0))
ACK(s(x), s(y)) → ACK(s(x), y)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
ack(0, x) → plus(x, s(0))
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
plus(x, s(0)) → s(x)
plus(x, s(s(y))) → s(plus(s(x), y))
plus(x, 0) → x
double(x0)
permute(x0, x1, a)
permute(false, x0, b)
permute(true, x0, b)
permute(x0, x1, c)
p(0)
p(s(x0))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
plus(x0, s(s(x1)))
plus(x0, s(0))
plus(x0, 0)
isZero(0)
isZero(s(x0))
double(x0)
permute(x0, x1, a)
permute(false, x0, b)
permute(true, x0, b)
permute(x0, x1, c)
p(0)
p(s(x0))
isZero(0)
isZero(s(x0))
ACK(s(x), s(y)) → ACK(x, ack(s(x), y))
ACK(s(x), 0) → ACK(x, s(0))
ACK(s(x), s(y)) → ACK(s(x), y)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
ack(0, x) → plus(x, s(0))
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
plus(x, s(0)) → s(x)
plus(x, s(s(y))) → s(plus(s(x), y))
plus(x, 0) → x
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
plus(x0, s(s(x1)))
plus(x0, s(0))
plus(x0, 0)
From the DPs we obtained the following set of size-change graphs:
PERMUTE(false, x, b) → PERMUTE(ack(x, x), p(x), c)
PERMUTE(y, x, c) → PERMUTE(x, y, a)
PERMUTE(x, y, a) → PERMUTE(isZero(x), x, b)
double(x) → permute(x, x, a)
permute(x, y, a) → permute(isZero(x), x, b)
permute(false, x, b) → permute(ack(x, x), p(x), c)
permute(true, x, b) → 0
permute(y, x, c) → s(s(permute(x, y, a)))
p(0) → 0
p(s(x)) → x
ack(0, x) → plus(x, s(0))
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, ack(s(x), y))
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
plus(x, s(s(y))) → s(plus(s(x), y))
plus(x, s(0)) → s(x)
plus(x, 0) → x
isZero(0) → true
isZero(s(x)) → false
PERMUTE(false, x, b) → PERMUTE(ack(x, x), p(x), c)
PERMUTE(y, x, c) → PERMUTE(x, y, a)
PERMUTE(x, y, a) → PERMUTE(isZero(x), x, b)
double(x) → permute(x, x, a)
permute(x, y, a) → permute(isZero(x), x, b)
permute(false, x, b) → permute(ack(x, x), p(x), c)
permute(true, x, b) → 0
permute(y, x, c) → s(s(permute(x, y, a)))
p(0) → 0
p(s(x)) → x
ack(0, x) → plus(x, s(0))
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, ack(s(x), y))
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
plus(x, s(s(y))) → s(plus(s(x), y))
plus(x, s(0)) → s(x)
plus(x, 0) → x
isZero(0) → true
isZero(s(x)) → false
double(x0)
permute(x0, x1, a)
permute(false, x0, b)
permute(true, x0, b)
permute(x0, x1, c)
p(0)
p(s(x0))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
plus(x0, s(s(x1)))
plus(x0, s(0))
plus(x0, 0)
isZero(0)
isZero(s(x0))
PERMUTE(false, x, b) → PERMUTE(ack(x, x), p(x), c)
PERMUTE(y, x, c) → PERMUTE(x, y, a)
PERMUTE(x, y, a) → PERMUTE(isZero(x), x, b)
isZero(0) → true
isZero(s(x)) → false
ack(0, x) → plus(x, s(0))
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
p(0) → 0
p(s(x)) → x
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
plus(x, s(0)) → s(x)
plus(x, s(s(y))) → s(plus(s(x), y))
plus(x, 0) → x
double(x0)
permute(x0, x1, a)
permute(false, x0, b)
permute(true, x0, b)
permute(x0, x1, c)
p(0)
p(s(x0))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
plus(x0, s(s(x1)))
plus(x0, s(0))
plus(x0, 0)
isZero(0)
isZero(s(x0))
double(x0)
permute(x0, x1, a)
permute(false, x0, b)
permute(true, x0, b)
permute(x0, x1, c)
PERMUTE(false, x, b) → PERMUTE(ack(x, x), p(x), c)
PERMUTE(y, x, c) → PERMUTE(x, y, a)
PERMUTE(x, y, a) → PERMUTE(isZero(x), x, b)
isZero(0) → true
isZero(s(x)) → false
ack(0, x) → plus(x, s(0))
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
p(0) → 0
p(s(x)) → x
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
plus(x, s(0)) → s(x)
plus(x, s(s(y))) → s(plus(s(x), y))
plus(x, 0) → x
p(0)
p(s(x0))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
plus(x0, s(s(x1)))
plus(x0, s(0))
plus(x0, 0)
isZero(0)
isZero(s(x0))
PERMUTE(0, y1, a) → PERMUTE(true, 0, b)
PERMUTE(s(x0), y1, a) → PERMUTE(false, s(x0), b)
PERMUTE(false, x, b) → PERMUTE(ack(x, x), p(x), c)
PERMUTE(y, x, c) → PERMUTE(x, y, a)
PERMUTE(0, y1, a) → PERMUTE(true, 0, b)
PERMUTE(s(x0), y1, a) → PERMUTE(false, s(x0), b)
isZero(0) → true
isZero(s(x)) → false
ack(0, x) → plus(x, s(0))
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
p(0) → 0
p(s(x)) → x
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
plus(x, s(0)) → s(x)
plus(x, s(s(y))) → s(plus(s(x), y))
plus(x, 0) → x
p(0)
p(s(x0))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
plus(x0, s(s(x1)))
plus(x0, s(0))
plus(x0, 0)
isZero(0)
isZero(s(x0))
PERMUTE(y, x, c) → PERMUTE(x, y, a)
PERMUTE(s(x0), y1, a) → PERMUTE(false, s(x0), b)
PERMUTE(false, x, b) → PERMUTE(ack(x, x), p(x), c)
isZero(0) → true
isZero(s(x)) → false
ack(0, x) → plus(x, s(0))
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
p(0) → 0
p(s(x)) → x
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
plus(x, s(0)) → s(x)
plus(x, s(s(y))) → s(plus(s(x), y))
plus(x, 0) → x
p(0)
p(s(x0))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
plus(x0, s(s(x1)))
plus(x0, s(0))
plus(x0, 0)
isZero(0)
isZero(s(x0))
PERMUTE(y, x, c) → PERMUTE(x, y, a)
PERMUTE(s(x0), y1, a) → PERMUTE(false, s(x0), b)
PERMUTE(false, x, b) → PERMUTE(ack(x, x), p(x), c)
ack(0, x) → plus(x, s(0))
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
p(0) → 0
p(s(x)) → x
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
plus(x, s(0)) → s(x)
plus(x, s(s(y))) → s(plus(s(x), y))
plus(x, 0) → x
p(0)
p(s(x0))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
plus(x0, s(s(x1)))
plus(x0, s(0))
plus(x0, 0)
isZero(0)
isZero(s(x0))
isZero(0)
isZero(s(x0))
PERMUTE(y, x, c) → PERMUTE(x, y, a)
PERMUTE(s(x0), y1, a) → PERMUTE(false, s(x0), b)
PERMUTE(false, x, b) → PERMUTE(ack(x, x), p(x), c)
ack(0, x) → plus(x, s(0))
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
p(0) → 0
p(s(x)) → x
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
plus(x, s(0)) → s(x)
plus(x, s(s(y))) → s(plus(s(x), y))
plus(x, 0) → x
p(0)
p(s(x0))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
plus(x0, s(s(x1)))
plus(x0, s(0))
plus(x0, 0)
PERMUTE(false, s(z0), b) → PERMUTE(ack(s(z0), s(z0)), p(s(z0)), c)
PERMUTE(y, x, c) → PERMUTE(x, y, a)
PERMUTE(s(x0), y1, a) → PERMUTE(false, s(x0), b)
PERMUTE(false, s(z0), b) → PERMUTE(ack(s(z0), s(z0)), p(s(z0)), c)
ack(0, x) → plus(x, s(0))
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
p(0) → 0
p(s(x)) → x
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
plus(x, s(0)) → s(x)
plus(x, s(s(y))) → s(plus(s(x), y))
plus(x, 0) → x
p(0)
p(s(x0))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
plus(x0, s(s(x1)))
plus(x0, s(0))
plus(x0, 0)
PERMUTE(y, x, c) → PERMUTE(x, y, a)
PERMUTE(s(x0), y1, a) → PERMUTE(false, s(x0), b)
PERMUTE(false, s(z0), b) → PERMUTE(ack(s(z0), s(z0)), p(s(z0)), c)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
p(s(x)) → x
ack(0, x) → plus(x, s(0))
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
plus(x, s(0)) → s(x)
plus(x, s(s(y))) → s(plus(s(x), y))
plus(x, 0) → x
p(0)
p(s(x0))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
plus(x0, s(s(x1)))
plus(x0, s(0))
plus(x0, 0)
PERMUTE(false, s(z0), b) → PERMUTE(ack(s(z0), s(z0)), z0, c)
PERMUTE(y, x, c) → PERMUTE(x, y, a)
PERMUTE(s(x0), y1, a) → PERMUTE(false, s(x0), b)
PERMUTE(false, s(z0), b) → PERMUTE(ack(s(z0), s(z0)), z0, c)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
p(s(x)) → x
ack(0, x) → plus(x, s(0))
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
plus(x, s(0)) → s(x)
plus(x, s(s(y))) → s(plus(s(x), y))
plus(x, 0) → x
p(0)
p(s(x0))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
plus(x0, s(s(x1)))
plus(x0, s(0))
plus(x0, 0)
PERMUTE(y, x, c) → PERMUTE(x, y, a)
PERMUTE(s(x0), y1, a) → PERMUTE(false, s(x0), b)
PERMUTE(false, s(z0), b) → PERMUTE(ack(s(z0), s(z0)), z0, c)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
ack(0, x) → plus(x, s(0))
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
plus(x, s(0)) → s(x)
plus(x, s(s(y))) → s(plus(s(x), y))
plus(x, 0) → x
p(0)
p(s(x0))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
plus(x0, s(s(x1)))
plus(x0, s(0))
plus(x0, 0)
p(0)
p(s(x0))
PERMUTE(y, x, c) → PERMUTE(x, y, a)
PERMUTE(s(x0), y1, a) → PERMUTE(false, s(x0), b)
PERMUTE(false, s(z0), b) → PERMUTE(ack(s(z0), s(z0)), z0, c)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
ack(0, x) → plus(x, s(0))
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
plus(x, s(0)) → s(x)
plus(x, s(s(y))) → s(plus(s(x), y))
plus(x, 0) → x
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
plus(x0, s(s(x1)))
plus(x0, s(0))
plus(x0, 0)
PERMUTE(false, s(x0), b) → PERMUTE(ack(x0, ack(s(x0), x0)), x0, c)
PERMUTE(y, x, c) → PERMUTE(x, y, a)
PERMUTE(s(x0), y1, a) → PERMUTE(false, s(x0), b)
PERMUTE(false, s(x0), b) → PERMUTE(ack(x0, ack(s(x0), x0)), x0, c)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
ack(0, x) → plus(x, s(0))
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
plus(x, s(0)) → s(x)
plus(x, s(s(y))) → s(plus(s(x), y))
plus(x, 0) → x
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
plus(x0, s(s(x1)))
plus(x0, s(0))
plus(x0, 0)
PERMUTE(x0, s(y_0), c) → PERMUTE(s(y_0), x0, a)
PERMUTE(s(x0), y1, a) → PERMUTE(false, s(x0), b)
PERMUTE(false, s(x0), b) → PERMUTE(ack(x0, ack(s(x0), x0)), x0, c)
PERMUTE(x0, s(y_0), c) → PERMUTE(s(y_0), x0, a)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
ack(0, x) → plus(x, s(0))
plus(0, y) → y
plus(s(x), y) → plus(x, s(y))
plus(x, s(0)) → s(x)
plus(x, s(s(y))) → s(plus(s(x), y))
plus(x, 0) → x
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
plus(x0, s(s(x1)))
plus(x0, s(0))
plus(x0, 0)
From the DPs we obtained the following set of size-change graphs: