YES
0 QTRS
↳1 AAECC Innermost (⇔, 0 ms)
↳2 QTRS
↳3 DependencyPairsProof (⇔, 0 ms)
↳4 QDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 QDP
↳10 QReductionProof (⇔, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 QDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 QDP
↳17 QReductionProof (⇔, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 QDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 QDP
↳24 QReductionProof (⇔, 0 ms)
↳25 QDP
↳26 QDPSizeChangeProof (⇔, 0 ms)
↳27 YES
↳28 QDP
↳29 UsableRulesProof (⇔, 0 ms)
↳30 QDP
↳31 QReductionProof (⇔, 0 ms)
↳32 QDP
↳33 TransformationProof (⇔, 0 ms)
↳34 QDP
↳35 DependencyGraphProof (⇔, 0 ms)
↳36 QDP
↳37 UsableRulesProof (⇔, 0 ms)
↳38 QDP
↳39 QReductionProof (⇔, 0 ms)
↳40 QDP
↳41 TransformationProof (⇔, 0 ms)
↳42 QDP
↳43 QDPQMonotonicMRRProof (⇔, 0 ms)
↳44 QDP
↳45 UsableRulesProof (⇔, 0 ms)
↳46 QDP
↳47 TransformationProof (⇒, 0 ms)
↳48 QDP
↳49 UsableRulesProof (⇔, 0 ms)
↳50 QDP
↳51 QReductionProof (⇔, 0 ms)
↳52 QDP
↳53 TransformationProof (⇔, 0 ms)
↳54 QDP
↳55 UsableRulesProof (⇔, 0 ms)
↳56 QDP
↳57 QReductionProof (⇔, 0 ms)
↳58 QDP
↳59 TransformationProof (⇔, 0 ms)
↳60 QDP
↳61 DependencyGraphProof (⇔, 0 ms)
↳62 TRUE
↳63 QDP
↳64 UsableRulesProof (⇔, 0 ms)
↳65 QDP
↳66 QReductionProof (⇔, 0 ms)
↳67 QDP
↳68 TransformationProof (⇔, 0 ms)
↳69 QDP
↳70 DependencyGraphProof (⇔, 0 ms)
↳71 QDP
↳72 TransformationProof (⇔, 0 ms)
↳73 QDP
↳74 TransformationProof (⇔, 0 ms)
↳75 QDP
↳76 TransformationProof (⇔, 0 ms)
↳77 QDP
↳78 TransformationProof (⇔, 0 ms)
↳79 QDP
↳80 TransformationProof (⇔, 0 ms)
↳81 QDP
↳82 DependencyGraphProof (⇔, 0 ms)
↳83 QDP
↳84 QDPSizeChangeProof (⇔, 0 ms)
↳85 YES
inc(s(x)) → s(inc(x))
inc(0) → s(0)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
ifPlus(false, x, y, z) → plus(x, z)
ifPlus(true, x, y, z) → y
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, 0) → x
minus(x, x) → 0
eq(s(x), s(y)) → eq(x, y)
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
times(x, y) → timesIter(x, y, 0)
timesIter(x, y, z) → ifTimes(eq(x, 0), minus(x, s(0)), y, z, plus(y, z))
ifTimes(true, x, y, z, u) → z
ifTimes(false, x, y, z, u) → timesIter(x, y, u)
f → g
f → h
inc(0) → s(0)
ifPlus(true, x, y, z) → y
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, 0) → x
minus(x, x) → 0
eq(s(x), s(y)) → eq(x, y)
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
ifTimes(true, x, y, z, u) → z
ifTimes(false, x, y, z, u) → timesIter(x, y, u)
inc(s(x)) → s(inc(x))
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
ifPlus(false, x, y, z) → plus(x, z)
times(x, y) → timesIter(x, y, 0)
timesIter(x, y, z) → ifTimes(eq(x, 0), minus(x, s(0)), y, z, plus(y, z))
f → g
f → h
inc(s(x)) → s(inc(x))
inc(0) → s(0)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
ifPlus(false, x, y, z) → plus(x, z)
ifPlus(true, x, y, z) → y
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, 0) → x
minus(x, x) → 0
eq(s(x), s(y)) → eq(x, y)
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
times(x, y) → timesIter(x, y, 0)
timesIter(x, y, z) → ifTimes(eq(x, 0), minus(x, s(0)), y, z, plus(y, z))
ifTimes(true, x, y, z, u) → z
ifTimes(false, x, y, z, u) → timesIter(x, y, u)
f → g
f → h
inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f
INC(s(x)) → INC(x)
PLUS(x, y) → IFPLUS(eq(x, 0), minus(x, s(0)), x, inc(x))
PLUS(x, y) → EQ(x, 0)
PLUS(x, y) → MINUS(x, s(0))
PLUS(x, y) → INC(x)
IFPLUS(false, x, y, z) → PLUS(x, z)
MINUS(s(x), s(y)) → MINUS(x, y)
EQ(s(x), s(y)) → EQ(x, y)
TIMES(x, y) → TIMESITER(x, y, 0)
TIMESITER(x, y, z) → IFTIMES(eq(x, 0), minus(x, s(0)), y, z, plus(y, z))
TIMESITER(x, y, z) → EQ(x, 0)
TIMESITER(x, y, z) → MINUS(x, s(0))
TIMESITER(x, y, z) → PLUS(y, z)
IFTIMES(false, x, y, z, u) → TIMESITER(x, y, u)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
ifPlus(false, x, y, z) → plus(x, z)
ifPlus(true, x, y, z) → y
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, 0) → x
minus(x, x) → 0
eq(s(x), s(y)) → eq(x, y)
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
times(x, y) → timesIter(x, y, 0)
timesIter(x, y, z) → ifTimes(eq(x, 0), minus(x, s(0)), y, z, plus(y, z))
ifTimes(true, x, y, z, u) → z
ifTimes(false, x, y, z, u) → timesIter(x, y, u)
f → g
f → h
inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f
EQ(s(x), s(y)) → EQ(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
ifPlus(false, x, y, z) → plus(x, z)
ifPlus(true, x, y, z) → y
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, 0) → x
minus(x, x) → 0
eq(s(x), s(y)) → eq(x, y)
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
times(x, y) → timesIter(x, y, 0)
timesIter(x, y, z) → ifTimes(eq(x, 0), minus(x, s(0)), y, z, plus(y, z))
ifTimes(true, x, y, z, u) → z
ifTimes(false, x, y, z, u) → timesIter(x, y, u)
f → g
f → h
inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f
EQ(s(x), s(y)) → EQ(x, y)
inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f
inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f
EQ(s(x), s(y)) → EQ(x, y)
From the DPs we obtained the following set of size-change graphs:
MINUS(s(x), s(y)) → MINUS(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
ifPlus(false, x, y, z) → plus(x, z)
ifPlus(true, x, y, z) → y
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, 0) → x
minus(x, x) → 0
eq(s(x), s(y)) → eq(x, y)
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
times(x, y) → timesIter(x, y, 0)
timesIter(x, y, z) → ifTimes(eq(x, 0), minus(x, s(0)), y, z, plus(y, z))
ifTimes(true, x, y, z, u) → z
ifTimes(false, x, y, z, u) → timesIter(x, y, u)
f → g
f → h
inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f
MINUS(s(x), s(y)) → MINUS(x, y)
inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f
inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f
MINUS(s(x), s(y)) → MINUS(x, y)
From the DPs we obtained the following set of size-change graphs:
INC(s(x)) → INC(x)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
ifPlus(false, x, y, z) → plus(x, z)
ifPlus(true, x, y, z) → y
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, 0) → x
minus(x, x) → 0
eq(s(x), s(y)) → eq(x, y)
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
times(x, y) → timesIter(x, y, 0)
timesIter(x, y, z) → ifTimes(eq(x, 0), minus(x, s(0)), y, z, plus(y, z))
ifTimes(true, x, y, z, u) → z
ifTimes(false, x, y, z, u) → timesIter(x, y, u)
f → g
f → h
inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f
INC(s(x)) → INC(x)
inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f
inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f
INC(s(x)) → INC(x)
From the DPs we obtained the following set of size-change graphs:
PLUS(x, y) → IFPLUS(eq(x, 0), minus(x, s(0)), x, inc(x))
IFPLUS(false, x, y, z) → PLUS(x, z)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
ifPlus(false, x, y, z) → plus(x, z)
ifPlus(true, x, y, z) → y
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, 0) → x
minus(x, x) → 0
eq(s(x), s(y)) → eq(x, y)
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
times(x, y) → timesIter(x, y, 0)
timesIter(x, y, z) → ifTimes(eq(x, 0), minus(x, s(0)), y, z, plus(y, z))
ifTimes(true, x, y, z, u) → z
ifTimes(false, x, y, z, u) → timesIter(x, y, u)
f → g
f → h
inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f
PLUS(x, y) → IFPLUS(eq(x, 0), minus(x, s(0)), x, inc(x))
IFPLUS(false, x, y, z) → PLUS(x, z)
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, x) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x
inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f
PLUS(x, y) → IFPLUS(eq(x, 0), minus(x, s(0)), x, inc(x))
IFPLUS(false, x, y, z) → PLUS(x, z)
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, x) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x
inc(s(x0))
inc(0)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
PLUS(s(x0), y1) → IFPLUS(false, minus(s(x0), s(0)), s(x0), inc(s(x0))) → PLUS(s(x0), y1) → IFPLUS(false, minus(s(x0), s(0)), s(x0), inc(s(x0)))
PLUS(0, y1) → IFPLUS(true, minus(0, s(0)), 0, inc(0)) → PLUS(0, y1) → IFPLUS(true, minus(0, s(0)), 0, inc(0))
IFPLUS(false, x, y, z) → PLUS(x, z)
PLUS(s(x0), y1) → IFPLUS(false, minus(s(x0), s(0)), s(x0), inc(s(x0)))
PLUS(0, y1) → IFPLUS(true, minus(0, s(0)), 0, inc(0))
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, x) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x
inc(s(x0))
inc(0)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
PLUS(s(x0), y1) → IFPLUS(false, minus(s(x0), s(0)), s(x0), inc(s(x0)))
IFPLUS(false, x, y, z) → PLUS(x, z)
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, x) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x
inc(s(x0))
inc(0)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
PLUS(s(x0), y1) → IFPLUS(false, minus(s(x0), s(0)), s(x0), inc(s(x0)))
IFPLUS(false, x, y, z) → PLUS(x, z)
minus(s(x), s(y)) → minus(x, y)
minus(x, x) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(0, x) → 0
minus(x, 0) → x
inc(s(x0))
inc(0)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
PLUS(s(x0), y1) → IFPLUS(false, minus(s(x0), s(0)), s(x0), inc(s(x0)))
IFPLUS(false, x, y, z) → PLUS(x, z)
minus(s(x), s(y)) → minus(x, y)
minus(x, x) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(0, x) → 0
minus(x, 0) → x
inc(s(x0))
inc(0)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
PLUS(s(x0), y1) → IFPLUS(false, minus(s(x0), s(0)), s(x0), s(inc(x0))) → PLUS(s(x0), y1) → IFPLUS(false, minus(s(x0), s(0)), s(x0), s(inc(x0)))
IFPLUS(false, x, y, z) → PLUS(x, z)
PLUS(s(x0), y1) → IFPLUS(false, minus(s(x0), s(0)), s(x0), s(inc(x0)))
minus(s(x), s(y)) → minus(x, y)
minus(x, x) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(0, x) → 0
minus(x, 0) → x
inc(s(x0))
inc(0)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
minus(s(x), s(y)) → minus(x, y)
POL(0) = 0
POL(IFPLUS(x1, x2, x3, x4)) = 1 + x1 + 2·x2
POL(PLUS(x1, x2)) = 1 + 2·x1
POL(false) = 0
POL(inc(x1)) = 2 + 2·x1
POL(minus(x1, x2)) = x1
POL(s(x1)) = 1 + x1
IFPLUS(false, x, y, z) → PLUS(x, z)
PLUS(s(x0), y1) → IFPLUS(false, minus(s(x0), s(0)), s(x0), s(inc(x0)))
minus(x, x) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(0, x) → 0
minus(x, 0) → x
inc(s(x0))
inc(0)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
IFPLUS(false, x, y, z) → PLUS(x, z)
PLUS(s(x0), y1) → IFPLUS(false, minus(s(x0), s(0)), s(x0), s(inc(x0)))
minus(x, x) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
inc(s(x0))
inc(0)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
PLUS(s(0), y1) → IFPLUS(false, 0, s(0), s(inc(0))) → PLUS(s(0), y1) → IFPLUS(false, 0, s(0), s(inc(0)))
IFPLUS(false, x, y, z) → PLUS(x, z)
PLUS(s(0), y1) → IFPLUS(false, 0, s(0), s(inc(0)))
minus(x, x) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
inc(s(x0))
inc(0)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
IFPLUS(false, x, y, z) → PLUS(x, z)
PLUS(s(0), y1) → IFPLUS(false, 0, s(0), s(inc(0)))
inc(0) → s(0)
inc(s(x0))
inc(0)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
IFPLUS(false, x, y, z) → PLUS(x, z)
PLUS(s(0), y1) → IFPLUS(false, 0, s(0), s(inc(0)))
inc(0) → s(0)
inc(s(x0))
inc(0)
PLUS(s(0), y1) → IFPLUS(false, 0, s(0), s(s(0))) → PLUS(s(0), y1) → IFPLUS(false, 0, s(0), s(s(0)))
IFPLUS(false, x, y, z) → PLUS(x, z)
PLUS(s(0), y1) → IFPLUS(false, 0, s(0), s(s(0)))
inc(0) → s(0)
inc(s(x0))
inc(0)
IFPLUS(false, x, y, z) → PLUS(x, z)
PLUS(s(0), y1) → IFPLUS(false, 0, s(0), s(s(0)))
inc(s(x0))
inc(0)
inc(s(x0))
inc(0)
IFPLUS(false, x, y, z) → PLUS(x, z)
PLUS(s(0), y1) → IFPLUS(false, 0, s(0), s(s(0)))
IFPLUS(false, 0, s(0), s(s(0))) → PLUS(0, s(s(0))) → IFPLUS(false, 0, s(0), s(s(0))) → PLUS(0, s(s(0)))
PLUS(s(0), y1) → IFPLUS(false, 0, s(0), s(s(0)))
IFPLUS(false, 0, s(0), s(s(0))) → PLUS(0, s(s(0)))
TIMESITER(x, y, z) → IFTIMES(eq(x, 0), minus(x, s(0)), y, z, plus(y, z))
IFTIMES(false, x, y, z, u) → TIMESITER(x, y, u)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
ifPlus(false, x, y, z) → plus(x, z)
ifPlus(true, x, y, z) → y
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, 0) → x
minus(x, x) → 0
eq(s(x), s(y)) → eq(x, y)
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
times(x, y) → timesIter(x, y, 0)
timesIter(x, y, z) → ifTimes(eq(x, 0), minus(x, s(0)), y, z, plus(y, z))
ifTimes(true, x, y, z, u) → z
ifTimes(false, x, y, z, u) → timesIter(x, y, u)
f → g
f → h
inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f
TIMESITER(x, y, z) → IFTIMES(eq(x, 0), minus(x, s(0)), y, z, plus(y, z))
IFTIMES(false, x, y, z, u) → TIMESITER(x, y, u)
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, x) → 0
ifPlus(false, x, y, z) → plus(x, z)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
ifPlus(true, x, y, z) → y
minus(x, 0) → x
inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f
times(x0, x1)
timesIter(x0, x1, x2)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
f
TIMESITER(x, y, z) → IFTIMES(eq(x, 0), minus(x, s(0)), y, z, plus(y, z))
IFTIMES(false, x, y, z, u) → TIMESITER(x, y, u)
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, x) → 0
ifPlus(false, x, y, z) → plus(x, z)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
ifPlus(true, x, y, z) → y
minus(x, 0) → x
inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
TIMESITER(s(x0), y1, y2) → IFTIMES(false, minus(s(x0), s(0)), y1, y2, plus(y1, y2)) → TIMESITER(s(x0), y1, y2) → IFTIMES(false, minus(s(x0), s(0)), y1, y2, plus(y1, y2))
TIMESITER(0, y1, y2) → IFTIMES(true, minus(0, s(0)), y1, y2, plus(y1, y2)) → TIMESITER(0, y1, y2) → IFTIMES(true, minus(0, s(0)), y1, y2, plus(y1, y2))
IFTIMES(false, x, y, z, u) → TIMESITER(x, y, u)
TIMESITER(s(x0), y1, y2) → IFTIMES(false, minus(s(x0), s(0)), y1, y2, plus(y1, y2))
TIMESITER(0, y1, y2) → IFTIMES(true, minus(0, s(0)), y1, y2, plus(y1, y2))
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, x) → 0
ifPlus(false, x, y, z) → plus(x, z)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
ifPlus(true, x, y, z) → y
minus(x, 0) → x
inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
TIMESITER(s(x0), y1, y2) → IFTIMES(false, minus(s(x0), s(0)), y1, y2, plus(y1, y2))
IFTIMES(false, x, y, z, u) → TIMESITER(x, y, u)
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, x) → 0
ifPlus(false, x, y, z) → plus(x, z)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
ifPlus(true, x, y, z) → y
minus(x, 0) → x
inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
TIMESITER(s(x0), y1, y2) → IFTIMES(false, minus(x0, 0), y1, y2, plus(y1, y2)) → TIMESITER(s(x0), y1, y2) → IFTIMES(false, minus(x0, 0), y1, y2, plus(y1, y2))
TIMESITER(s(0), y1, y2) → IFTIMES(false, 0, y1, y2, plus(y1, y2)) → TIMESITER(s(0), y1, y2) → IFTIMES(false, 0, y1, y2, plus(y1, y2))
IFTIMES(false, x, y, z, u) → TIMESITER(x, y, u)
TIMESITER(s(x0), y1, y2) → IFTIMES(false, minus(x0, 0), y1, y2, plus(y1, y2))
TIMESITER(s(0), y1, y2) → IFTIMES(false, 0, y1, y2, plus(y1, y2))
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, x) → 0
ifPlus(false, x, y, z) → plus(x, z)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
ifPlus(true, x, y, z) → y
minus(x, 0) → x
inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
TIMESITER(s(x0), y1, y2) → IFTIMES(false, x0, y1, y2, plus(y1, y2)) → TIMESITER(s(x0), y1, y2) → IFTIMES(false, x0, y1, y2, plus(y1, y2))
IFTIMES(false, x, y, z, u) → TIMESITER(x, y, u)
TIMESITER(s(0), y1, y2) → IFTIMES(false, 0, y1, y2, plus(y1, y2))
TIMESITER(s(x0), y1, y2) → IFTIMES(false, x0, y1, y2, plus(y1, y2))
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, x) → 0
ifPlus(false, x, y, z) → plus(x, z)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
ifPlus(true, x, y, z) → y
minus(x, 0) → x
inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
TIMESITER(s(0), x0, x1) → IFTIMES(false, 0, x0, x1, ifPlus(eq(x0, 0), minus(x0, s(0)), x0, inc(x0))) → TIMESITER(s(0), x0, x1) → IFTIMES(false, 0, x0, x1, ifPlus(eq(x0, 0), minus(x0, s(0)), x0, inc(x0)))
IFTIMES(false, x, y, z, u) → TIMESITER(x, y, u)
TIMESITER(s(x0), y1, y2) → IFTIMES(false, x0, y1, y2, plus(y1, y2))
TIMESITER(s(0), x0, x1) → IFTIMES(false, 0, x0, x1, ifPlus(eq(x0, 0), minus(x0, s(0)), x0, inc(x0)))
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, x) → 0
ifPlus(false, x, y, z) → plus(x, z)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
ifPlus(true, x, y, z) → y
minus(x, 0) → x
inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
TIMESITER(s(y0), x0, x1) → IFTIMES(false, y0, x0, x1, ifPlus(eq(x0, 0), minus(x0, s(0)), x0, inc(x0))) → TIMESITER(s(y0), x0, x1) → IFTIMES(false, y0, x0, x1, ifPlus(eq(x0, 0), minus(x0, s(0)), x0, inc(x0)))
IFTIMES(false, x, y, z, u) → TIMESITER(x, y, u)
TIMESITER(s(0), x0, x1) → IFTIMES(false, 0, x0, x1, ifPlus(eq(x0, 0), minus(x0, s(0)), x0, inc(x0)))
TIMESITER(s(y0), x0, x1) → IFTIMES(false, y0, x0, x1, ifPlus(eq(x0, 0), minus(x0, s(0)), x0, inc(x0)))
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, x) → 0
ifPlus(false, x, y, z) → plus(x, z)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
ifPlus(true, x, y, z) → y
minus(x, 0) → x
inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
IFTIMES(false, s(0), x1, x2, x3) → TIMESITER(s(0), x1, x3) → IFTIMES(false, s(0), x1, x2, x3) → TIMESITER(s(0), x1, x3)
IFTIMES(false, s(y_0), x1, x2, x3) → TIMESITER(s(y_0), x1, x3) → IFTIMES(false, s(y_0), x1, x2, x3) → TIMESITER(s(y_0), x1, x3)
TIMESITER(s(0), x0, x1) → IFTIMES(false, 0, x0, x1, ifPlus(eq(x0, 0), minus(x0, s(0)), x0, inc(x0)))
TIMESITER(s(y0), x0, x1) → IFTIMES(false, y0, x0, x1, ifPlus(eq(x0, 0), minus(x0, s(0)), x0, inc(x0)))
IFTIMES(false, s(0), x1, x2, x3) → TIMESITER(s(0), x1, x3)
IFTIMES(false, s(y_0), x1, x2, x3) → TIMESITER(s(y_0), x1, x3)
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, x) → 0
ifPlus(false, x, y, z) → plus(x, z)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
ifPlus(true, x, y, z) → y
minus(x, 0) → x
inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
TIMESITER(s(y0), x0, x1) → IFTIMES(false, y0, x0, x1, ifPlus(eq(x0, 0), minus(x0, s(0)), x0, inc(x0)))
IFTIMES(false, s(0), x1, x2, x3) → TIMESITER(s(0), x1, x3)
IFTIMES(false, s(y_0), x1, x2, x3) → TIMESITER(s(y_0), x1, x3)
eq(s(x), 0) → false
eq(0, 0) → true
eq(x, x) → true
minus(s(x), s(y)) → minus(x, y)
minus(0, x) → 0
minus(x, x) → 0
ifPlus(false, x, y, z) → plus(x, z)
plus(x, y) → ifPlus(eq(x, 0), minus(x, s(0)), x, inc(x))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
ifPlus(true, x, y, z) → y
minus(x, 0) → x
inc(s(x0))
inc(0)
plus(x0, x1)
ifPlus(false, x0, x1, x2)
ifPlus(true, x0, x1, x2)
minus(s(x0), s(x1))
minus(0, x0)
minus(x0, 0)
minus(x0, x0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
eq(x0, x0)
From the DPs we obtained the following set of size-change graphs: