0 QTRS
↳1 AAECC Innermost (⇔)
↳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 QDPSizeChangeProof (⇔)
↳27 TRUE
↳28 QDP
↳29 UsableRulesProof (⇔)
↳30 QDP
↳31 QReductionProof (⇔)
↳32 QDP
↳33 Narrowing (⇔)
↳34 QDP
↳35 DependencyGraphProof (⇔)
↳36 QDP
↳37 UsableRulesProof (⇔)
↳38 QDP
↳39 QReductionProof (⇔)
↳40 QDP
↳41 Rewriting (⇔)
↳42 QDP
↳43 Narrowing (⇔)
↳44 QDP
↳45 UsableRulesProof (⇔)
↳46 QDP
↳47 Rewriting (⇔)
↳48 QDP
↳49 UsableRulesProof (⇔)
↳50 QDP
↳51 QReductionProof (⇔)
↳52 QDP
↳53 Rewriting (⇔)
↳54 QDP
↳55 Instantiation (⇔)
↳56 QDP
↳57 DependencyGraphProof (⇔)
↳58 QDP
↳59 Instantiation (⇔)
↳60 QDP
↳61 Instantiation (⇔)
↳62 QDP
↳63 ForwardInstantiation (⇔)
↳64 QDP
↳65 DependencyGraphProof (⇔)
↳66 QDP
↳67 Narrowing (⇔)
↳68 QDP
↳69 DependencyGraphProof (⇔)
↳70 QDP
↳71 Instantiation (⇔)
↳72 QDP
↳73 Instantiation (⇔)
↳74 QDP
↳75 QDPSizeChangeProof (⇔)
↳76 TRUE
↳77 QDP
↳78 UsableRulesProof (⇔)
↳79 QDP
↳80 QReductionProof (⇔)
↳81 QDP
↳82 Narrowing (⇔)
↳83 QDP
↳84 DependencyGraphProof (⇔)
↳85 QDP
↳86 Narrowing (⇔)
↳87 QDP
↳88 Rewriting (⇔)
↳89 QDP
↳90 Narrowing (⇔)
↳91 QDP
↳92 Narrowing (⇔)
↳93 QDP
↳94 ForwardInstantiation (⇔)
↳95 QDP
↳96 DependencyGraphProof (⇔)
↳97 QDP
↳98 QDPSizeChangeProof (⇔)
↳99 TRUE
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(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)))
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)
PLUS(s(x0), y1) → IFPLUS(false, minus(x0, 0), s(x0), s(inc(x0)))
PLUS(s(0), y1) → IFPLUS(false, 0, s(0), s(inc(0)))
IFPLUS(false, x, y, z) → PLUS(x, z)
PLUS(s(x0), y1) → IFPLUS(false, minus(x0, 0), s(x0), s(inc(x0)))
PLUS(s(0), y1) → IFPLUS(false, 0, s(0), s(inc(0)))
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)
IFPLUS(false, x, y, z) → PLUS(x, z)
PLUS(s(x0), y1) → IFPLUS(false, minus(x0, 0), s(x0), s(inc(x0)))
PLUS(s(0), y1) → IFPLUS(false, 0, s(0), s(inc(0)))
inc(0) → s(0)
minus(x, x) → 0
minus(0, x) → 0
minus(x, 0) → x
inc(s(x)) → s(inc(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, x0, s(x0), s(inc(x0)))
IFPLUS(false, x, y, z) → PLUS(x, z)
PLUS(s(0), y1) → IFPLUS(false, 0, s(0), s(inc(0)))
PLUS(s(x0), y1) → IFPLUS(false, x0, s(x0), s(inc(x0)))
inc(0) → s(0)
minus(x, x) → 0
minus(0, x) → 0
minus(x, 0) → x
inc(s(x)) → s(inc(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(0), y1) → IFPLUS(false, 0, s(0), s(inc(0)))
PLUS(s(x0), y1) → IFPLUS(false, x0, s(x0), s(inc(x0)))
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)
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)))
PLUS(s(x0), y1) → IFPLUS(false, x0, s(x0), s(inc(x0)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
inc(s(x0))
inc(0)
PLUS(s(0), y1) → IFPLUS(false, 0, s(0), s(s(0)))
IFPLUS(false, x, y, z) → PLUS(x, z)
PLUS(s(x0), y1) → IFPLUS(false, x0, s(x0), s(inc(x0)))
PLUS(s(0), y1) → IFPLUS(false, 0, s(0), s(s(0)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
inc(s(x0))
inc(0)
IFPLUS(false, z0, s(z0), s(y_0)) → PLUS(z0, s(y_0))
IFPLUS(false, 0, s(0), s(s(0))) → PLUS(0, s(s(0)))
PLUS(s(x0), y1) → IFPLUS(false, x0, s(x0), s(inc(x0)))
PLUS(s(0), y1) → IFPLUS(false, 0, s(0), s(s(0)))
IFPLUS(false, z0, s(z0), s(y_0)) → PLUS(z0, s(y_0))
IFPLUS(false, 0, s(0), s(s(0))) → PLUS(0, s(s(0)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
inc(s(x0))
inc(0)
IFPLUS(false, z0, s(z0), s(y_0)) → PLUS(z0, s(y_0))
PLUS(s(x0), y1) → IFPLUS(false, x0, s(x0), s(inc(x0)))
PLUS(s(0), y1) → IFPLUS(false, 0, s(0), s(s(0)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
inc(s(x0))
inc(0)
PLUS(s(x0), s(z1)) → IFPLUS(false, x0, s(x0), s(inc(x0)))
IFPLUS(false, z0, s(z0), s(y_0)) → PLUS(z0, s(y_0))
PLUS(s(0), y1) → IFPLUS(false, 0, s(0), s(s(0)))
PLUS(s(x0), s(z1)) → IFPLUS(false, x0, s(x0), s(inc(x0)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
inc(s(x0))
inc(0)
PLUS(s(0), s(z1)) → IFPLUS(false, 0, s(0), s(s(0)))
IFPLUS(false, z0, s(z0), s(y_0)) → PLUS(z0, s(y_0))
PLUS(s(x0), s(z1)) → IFPLUS(false, x0, s(x0), s(inc(x0)))
PLUS(s(0), s(z1)) → IFPLUS(false, 0, s(0), s(s(0)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
inc(s(x0))
inc(0)
IFPLUS(false, s(y_0), s(s(y_0)), s(x1)) → PLUS(s(y_0), s(x1))
IFPLUS(false, s(0), s(s(0)), s(x1)) → PLUS(s(0), s(x1))
PLUS(s(x0), s(z1)) → IFPLUS(false, x0, s(x0), s(inc(x0)))
PLUS(s(0), s(z1)) → IFPLUS(false, 0, s(0), s(s(0)))
IFPLUS(false, s(y_0), s(s(y_0)), s(x1)) → PLUS(s(y_0), s(x1))
IFPLUS(false, s(0), s(s(0)), s(x1)) → PLUS(s(0), s(x1))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
inc(s(x0))
inc(0)
IFPLUS(false, s(y_0), s(s(y_0)), s(x1)) → PLUS(s(y_0), s(x1))
PLUS(s(x0), s(z1)) → IFPLUS(false, x0, s(x0), s(inc(x0)))
IFPLUS(false, s(0), s(s(0)), s(x1)) → PLUS(s(0), s(x1))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
inc(s(x0))
inc(0)
PLUS(s(s(x0)), s(y1)) → IFPLUS(false, s(x0), s(s(x0)), s(s(inc(x0))))
PLUS(s(0), s(y1)) → IFPLUS(false, 0, s(0), s(s(0)))
IFPLUS(false, s(y_0), s(s(y_0)), s(x1)) → PLUS(s(y_0), s(x1))
IFPLUS(false, s(0), s(s(0)), s(x1)) → PLUS(s(0), s(x1))
PLUS(s(s(x0)), s(y1)) → IFPLUS(false, s(x0), s(s(x0)), s(s(inc(x0))))
PLUS(s(0), s(y1)) → IFPLUS(false, 0, s(0), s(s(0)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
inc(s(x0))
inc(0)
PLUS(s(s(x0)), s(y1)) → IFPLUS(false, s(x0), s(s(x0)), s(s(inc(x0))))
IFPLUS(false, s(y_0), s(s(y_0)), s(x1)) → PLUS(s(y_0), s(x1))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
inc(s(x0))
inc(0)
IFPLUS(false, s(z0), s(s(z0)), s(s(y_0))) → PLUS(s(z0), s(s(y_0)))
PLUS(s(s(x0)), s(y1)) → IFPLUS(false, s(x0), s(s(x0)), s(s(inc(x0))))
IFPLUS(false, s(z0), s(s(z0)), s(s(y_0))) → PLUS(s(z0), s(s(y_0)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
inc(s(x0))
inc(0)
PLUS(s(s(x0)), s(s(z1))) → IFPLUS(false, s(x0), s(s(x0)), s(s(inc(x0))))
IFPLUS(false, s(z0), s(s(z0)), s(s(y_0))) → PLUS(s(z0), s(s(y_0)))
PLUS(s(s(x0)), s(s(z1))) → IFPLUS(false, s(x0), s(s(x0)), s(s(inc(x0))))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
inc(s(x0))
inc(0)
From the DPs we obtained the following set of size-change graphs:
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(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(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))
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)))
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)))
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(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: