0 QTRS
↳1 Overlay + Local Confluence (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔)
↳9 QDP
↳10 QReductionProof (⇔)
↳11 QDP
↳12 QDPSizeChangeProof (⇔)
↳13 TRUE
↳14 QDP
↳15 UsableRulesProof (⇔)
↳16 QDP
↳17 QReductionProof (⇔)
↳18 QDP
↳19 QDPSizeChangeProof (⇔)
↳20 TRUE
↳21 QDP
↳22 UsableRulesProof (⇔)
↳23 QDP
↳24 QReductionProof (⇔)
↳25 QDP
↳26 Instantiation (⇔)
↳27 QDP
↳28 Rewriting (⇔)
↳29 QDP
↳30 UsableRulesProof (⇔)
↳31 QDP
↳32 QReductionProof (⇔)
↳33 QDP
↳34 Rewriting (⇔)
↳35 QDP
↳36 Rewriting (⇔)
↳37 QDP
↳38 Rewriting (⇔)
↳39 QDP
↳40 Rewriting (⇔)
↳41 QDP
↳42 Rewriting (⇔)
↳43 QDP
↳44 Rewriting (⇔)
↳45 QDP
↳46 Rewriting (⇔)
↳47 QDP
↳48 Rewriting (⇔)
↳49 QDP
↳50 Rewriting (⇔)
↳51 QDP
↳52 Rewriting (⇔)
↳53 QDP
↳54 Rewriting (⇔)
↳55 QDP
↳56 Rewriting (⇔)
↳57 QDP
↳58 Rewriting (⇔)
↳59 QDP
↳60 Rewriting (⇔)
↳61 QDP
↳62 Rewriting (⇔)
↳63 QDP
↳64 Rewriting (⇔)
↳65 QDP
↳66 Rewriting (⇔)
↳67 QDP
↳68 Rewriting (⇔)
↳69 QDP
↳70 Rewriting (⇔)
↳71 QDP
↳72 Rewriting (⇔)
↳73 QDP
↳74 Rewriting (⇔)
↳75 QDP
↳76 Rewriting (⇔)
↳77 QDP
↳78 Rewriting (⇔)
↳79 QDP
↳80 Rewriting (⇔)
↳81 QDP
↳82 Rewriting (⇔)
↳83 QDP
↳84 Rewriting (⇔)
↳85 QDP
↳86 Rewriting (⇔)
↳87 QDP
↳88 Rewriting (⇔)
↳89 QDP
↳90 Rewriting (⇔)
↳91 QDP
↳92 Rewriting (⇔)
↳93 QDP
↳94 Rewriting (⇔)
↳95 QDP
↳96 Rewriting (⇔)
↳97 QDP
↳98 Rewriting (⇔)
↳99 QDP
↳100 Rewriting (⇔)
↳101 QDP
↳102 Rewriting (⇔)
↳103 QDP
↳104 Rewriting (⇔)
↳105 QDP
↳106 Rewriting (⇔)
↳107 QDP
↳108 Rewriting (⇔)
↳109 QDP
↳110 Rewriting (⇔)
↳111 QDP
↳112 Rewriting (⇔)
↳113 QDP
↳114 Rewriting (⇔)
↳115 QDP
↳116 Rewriting (⇔)
↳117 QDP
↳118 Rewriting (⇔)
↳119 QDP
↳120 Rewriting (⇔)
↳121 QDP
↳122 Rewriting (⇔)
↳123 QDP
↳124 Rewriting (⇔)
↳125 QDP
↳126 Rewriting (⇔)
↳127 QDP
↳128 Rewriting (⇔)
↳129 QDP
↳130 Rewriting (⇔)
↳131 QDP
↳132 Instantiation (⇔)
↳133 QDP
↳134 RemovalProof (⇐)
↳135 QDP
↳136 NonInfProof (⇔)
↳137 QDP
↳138 DependencyGraphProof (⇔)
↳139 TRUE
numbers → d(0)
d(x) → if(le(x, nr), x)
if(true, x) → cons(x, d(s(x)))
if(false, x) → nil
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
nr → ack(s(s(s(s(s(s(0)))))), 0)
ack(0, x) → s(x)
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, ack(s(x), y))
numbers → d(0)
d(x) → if(le(x, nr), x)
if(true, x) → cons(x, d(s(x)))
if(false, x) → nil
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
nr → ack(s(s(s(s(s(s(0)))))), 0)
ack(0, x) → s(x)
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, ack(s(x), y))
numbers
d(x0)
if(true, x0)
if(false, x0)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
nr
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
NUMBERS → D(0)
D(x) → IF(le(x, nr), x)
D(x) → LE(x, nr)
D(x) → NR
IF(true, x) → D(s(x))
LE(s(x), s(y)) → LE(x, y)
NR → ACK(s(s(s(s(s(s(0)))))), 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)
numbers → d(0)
d(x) → if(le(x, nr), x)
if(true, x) → cons(x, d(s(x)))
if(false, x) → nil
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
nr → ack(s(s(s(s(s(s(0)))))), 0)
ack(0, x) → s(x)
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, ack(s(x), y))
numbers
d(x0)
if(true, x0)
if(false, x0)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
nr
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
ACK(s(x), s(y)) → ACK(x, ack(s(x), y))
ACK(s(x), s(y)) → ACK(s(x), y)
ACK(s(x), 0) → ACK(x, s(0))
numbers → d(0)
d(x) → if(le(x, nr), x)
if(true, x) → cons(x, d(s(x)))
if(false, x) → nil
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
nr → ack(s(s(s(s(s(s(0)))))), 0)
ack(0, x) → s(x)
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, ack(s(x), y))
numbers
d(x0)
if(true, x0)
if(false, x0)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
nr
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
ACK(s(x), s(y)) → ACK(x, ack(s(x), y))
ACK(s(x), s(y)) → ACK(s(x), y)
ACK(s(x), 0) → ACK(x, s(0))
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
ack(0, x) → s(x)
numbers
d(x0)
if(true, x0)
if(false, x0)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
nr
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
numbers
d(x0)
if(true, x0)
if(false, x0)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
nr
ACK(s(x), s(y)) → ACK(x, ack(s(x), y))
ACK(s(x), s(y)) → ACK(s(x), y)
ACK(s(x), 0) → ACK(x, s(0))
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
ack(0, x) → s(x)
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
From the DPs we obtained the following set of size-change graphs:
LE(s(x), s(y)) → LE(x, y)
numbers → d(0)
d(x) → if(le(x, nr), x)
if(true, x) → cons(x, d(s(x)))
if(false, x) → nil
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
nr → ack(s(s(s(s(s(s(0)))))), 0)
ack(0, x) → s(x)
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, ack(s(x), y))
numbers
d(x0)
if(true, x0)
if(false, x0)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
nr
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
LE(s(x), s(y)) → LE(x, y)
numbers
d(x0)
if(true, x0)
if(false, x0)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
nr
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
numbers
d(x0)
if(true, x0)
if(false, x0)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
nr
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
LE(s(x), s(y)) → LE(x, y)
From the DPs we obtained the following set of size-change graphs:
IF(true, x) → D(s(x))
D(x) → IF(le(x, nr), x)
numbers → d(0)
d(x) → if(le(x, nr), x)
if(true, x) → cons(x, d(s(x)))
if(false, x) → nil
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
nr → ack(s(s(s(s(s(s(0)))))), 0)
ack(0, x) → s(x)
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, ack(s(x), y))
numbers
d(x0)
if(true, x0)
if(false, x0)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
nr
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
IF(true, x) → D(s(x))
D(x) → IF(le(x, nr), x)
nr → ack(s(s(s(s(s(s(0)))))), 0)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
ack(0, x) → s(x)
numbers
d(x0)
if(true, x0)
if(false, x0)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
nr
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
numbers
d(x0)
if(true, x0)
if(false, x0)
IF(true, x) → D(s(x))
D(x) → IF(le(x, nr), x)
nr → ack(s(s(s(s(s(s(0)))))), 0)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
nr
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(s(z0)) → IF(le(s(z0), nr), s(z0))
IF(true, x) → D(s(x))
D(s(z0)) → IF(le(s(z0), nr), s(z0))
nr → ack(s(s(s(s(s(s(0)))))), 0)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
nr
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(s(s(0)))))), 0)), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(s(s(0)))))), 0)), x)
nr → ack(s(s(s(s(s(s(0)))))), 0)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
nr
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(s(s(0)))))), 0)), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
nr
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
nr
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(s(s(0)))))), 0)), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(s(0))))), s(0))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(s(0))))), s(0))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(s(s(0))))), 0))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(s(s(0))))), 0))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(s(0)))), s(0)))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(s(0)))), s(0)))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(s(s(s(0)))), 0)))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(s(s(s(0)))), 0)))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(s(s(0))), s(0))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(s(s(0))), s(0))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(s(0)), ack(s(s(s(0))), 0))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(s(0)), ack(s(s(s(0))), 0))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(s(0)), ack(s(s(0)), s(0)))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(s(0)), ack(s(s(0)), s(0)))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(s(0)), ack(s(0), ack(s(s(0)), 0)))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(s(0)), ack(s(0), ack(s(s(0)), 0)))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(s(0)), ack(s(0), ack(s(0), s(0))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(s(0)), ack(s(0), ack(s(0), s(0))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(s(0)), ack(s(0), ack(0, ack(s(0), 0))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(s(0)), ack(s(0), ack(0, ack(s(0), 0))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(s(0)), ack(s(0), s(ack(s(0), 0))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(s(0)), ack(s(0), s(ack(s(0), 0))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(s(0)), ack(0, ack(s(0), ack(s(0), 0))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(s(0)), ack(0, ack(s(0), ack(s(0), 0))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(s(0)), s(ack(s(0), ack(s(0), 0))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(s(0)), s(ack(s(0), ack(s(0), 0))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(s(0)), ack(s(0), ack(s(0), 0))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(s(0)), ack(s(0), ack(s(0), 0))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(s(0)), ack(s(0), ack(0, s(0)))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(s(0)), ack(s(0), ack(0, s(0)))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(s(0)), ack(s(0), s(s(0)))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(s(0)), ack(s(0), s(s(0)))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(s(0)), ack(0, ack(s(0), s(0)))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(s(0)), ack(0, ack(s(0), s(0)))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(s(0)), s(ack(s(0), s(0)))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(s(0)), s(ack(s(0), s(0)))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(s(0)), ack(s(0), s(0)))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(s(0)), ack(s(0), s(0)))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(s(0)), ack(0, ack(s(0), 0)))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(s(0)), ack(0, ack(s(0), 0)))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(s(0)), s(ack(s(0), 0)))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(s(0)), s(ack(s(0), 0)))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(s(s(0)), ack(s(0), 0)))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(s(s(0)), ack(s(0), 0)))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(s(s(0)), ack(0, s(0))))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(s(s(0)), ack(0, s(0))))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(s(s(0)), s(s(0))))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(s(s(0)), s(s(0))))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(s(0)), s(0))))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(s(0)), s(0))))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(s(0)), 0))))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(s(0)), 0))))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(0), s(0)))))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(0), s(0)))))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(0, ack(s(0), 0)))))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(0, ack(s(0), 0)))))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(0), s(ack(s(0), 0)))))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(0), s(ack(s(0), 0)))))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(0, ack(s(0), ack(s(0), 0)))))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(0, ack(s(0), ack(s(0), 0)))))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(s(0), s(ack(s(0), ack(s(0), 0)))))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(s(0), s(ack(s(0), ack(s(0), 0)))))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(0, ack(s(0), ack(s(0), ack(s(0), 0)))))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(0, ack(s(0), ack(s(0), ack(s(0), 0)))))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), s(ack(s(0), ack(s(0), ack(s(0), 0)))))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), s(ack(s(0), ack(s(0), ack(s(0), 0)))))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(0, ack(s(0), ack(s(0), ack(s(0), ack(s(0), 0)))))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(0, ack(s(0), ack(s(0), ack(s(0), ack(s(0), 0)))))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), s(ack(s(0), ack(s(0), ack(s(0), ack(s(0), 0)))))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(s(0), s(ack(s(0), ack(s(0), ack(s(0), ack(s(0), 0)))))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(0, ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(0), 0)))))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), ack(0, ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(0), 0)))))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), s(ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(0), 0)))))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(s(0), s(ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(0), 0)))))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(0, ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(0), 0)))))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), ack(0, ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(0), 0)))))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), s(ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(0), 0)))))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(s(0))), s(ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(0), 0)))))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(0)), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(0), 0)))))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(0)), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(0), 0)))))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(0)), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(0, s(0))))))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(0)), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(0, s(0))))))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(0)), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(0), s(s(0))))))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(0)), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(s(0), s(s(0))))))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(0)), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(0, ack(s(0), s(0))))))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(0)), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(s(0), ack(0, ack(s(0), s(0))))))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(0)), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(s(0), s(ack(s(0), s(0))))))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(0)), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(s(0), s(ack(s(0), s(0))))))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(0)), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(0, ack(s(0), ack(s(0), s(0))))))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(0)), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), ack(0, ack(s(0), ack(s(0), s(0))))))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(0)), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), s(ack(s(0), ack(s(0), s(0))))))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(0)), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(s(0), s(ack(s(0), ack(s(0), s(0))))))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(0)), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(0, ack(s(0), ack(s(0), ack(s(0), s(0))))))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(0)), ack(s(s(s(0))), ack(s(0), ack(s(0), ack(0, ack(s(0), ack(s(0), ack(s(0), s(0))))))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(0)), ack(s(s(s(0))), ack(s(0), ack(s(0), s(ack(s(0), ack(s(0), ack(s(0), s(0))))))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(0)), ack(s(s(s(0))), ack(s(0), ack(s(0), s(ack(s(0), ack(s(0), ack(s(0), s(0))))))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(0)), ack(s(s(s(0))), ack(s(0), ack(0, ack(s(0), ack(s(0), ack(s(0), ack(s(0), s(0))))))))))), x)
IF(true, x) → D(s(x))
D(x) → IF(le(x, ack(s(s(s(s(0)))), ack(s(s(0)), ack(s(s(s(0))), ack(s(0), ack(0, ack(s(0), ack(s(0), ack(s(0), ack(s(0), s(0))))))))))), x)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
D(s(z0)) → IF(le(s(z0), ack(s(s(s(s(0)))), ack(s(s(0)), ack(s(s(s(0))), ack(s(0), ack(0, ack(s(0), ack(s(0), ack(s(0), ack(s(0), s(0))))))))))), s(z0))
IF(true, x) → D(s(x))
D(s(z0)) → IF(le(s(z0), ack(s(s(s(s(0)))), ack(s(s(0)), ack(s(s(s(0))), ack(s(0), ack(0, ack(s(0), ack(s(0), ack(s(0), ack(s(0), s(0))))))))))), s(z0))
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
The new variable was added to all pairs as a new argument[CONREM].
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
ack(0, x) → s(x)
IF(true, x, x_removed) → D(s(x), x_removed)
D(x, x_removed) → IF(le(x, x_removed), x, x_removed)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))
(1) (IF(le(x2, x3), x2, x3)=IF(true, x4, x5) ⇒ IF(true, x4, x5)≥D(s(x4), x5))
(2) (le(x2, x3)=true ⇒ IF(true, x2, x3)≥D(s(x2), x3))
(3) (true=true ⇒ IF(true, 0, x12)≥D(s(0), x12))
(4) (le(x15, x14)=true∧(le(x15, x14)=true ⇒ IF(true, x15, x14)≥D(s(x15), x14)) ⇒ IF(true, s(x15), s(x14))≥D(s(s(x15)), s(x14)))
(5) (IF(true, 0, x12)≥D(s(0), x12))
(6) (IF(true, x15, x14)≥D(s(x15), x14) ⇒ IF(true, s(x15), s(x14))≥D(s(s(x15)), s(x14)))
(7) (D(s(x6), x7)=D(x8, x9) ⇒ D(x8, x9)≥IF(le(x8, x9), x8, x9))
(8) (D(s(x6), x7)≥IF(le(s(x6), x7), s(x6), x7))
POL(0) = 0
POL(D(x1, x2)) = -1 - x1 + x2
POL(IF(x1, x2, x3)) = -1 - x1 - x2 + x3
POL(c) = -2
POL(false) = 0
POL(le(x1, x2)) = 0
POL(s(x1)) = 1 + x1
POL(true) = 0
The following pairs are in Pbound:
IF(true, x, x_removed) → D(s(x), x_removed)
The following rules are usable:
IF(true, x, x_removed) → D(s(x), x_removed)
true → le(0, y)
false → le(s(x), 0)
le(x, y) → le(s(x), s(y))
D(x, x_removed) → IF(le(x, x_removed), x, x_removed)
ack(s(x), s(y)) → ack(x, ack(s(x), y))
ack(s(x), 0) → ack(x, s(0))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
ack(0, x) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
ack(0, x0)
ack(s(x0), 0)
ack(s(x0), s(x1))