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 Narrowing (⇔)
↳27 QDP
↳28 DependencyGraphProof (⇔)
↳29 QDP
↳30 Instantiation (⇔)
↳31 QDP
↳32 DependencyGraphProof (⇔)
↳33 AND
↳34 QDP
↳35 Instantiation (⇔)
↳36 QDP
↳37 ForwardInstantiation (⇔)
↳38 QDP
↳39 ForwardInstantiation (⇔)
↳40 QDP
↳41 ForwardInstantiation (⇔)
↳42 QDP
↳43 MNOCProof (⇔)
↳44 QDP
↳45 QDP
↳46 UsableRulesProof (⇔)
↳47 QDP
↳48 QReductionProof (⇔)
↳49 QDP
↳50 ForwardInstantiation (⇔)
↳51 QDP
↳52 ForwardInstantiation (⇔)
↳53 QDP
↳54 QDPSizeChangeProof (⇔)
↳55 TRUE
↳56 UsableRulesProof (⇔)
↳57 QDP
↳58 QReductionProof (⇔)
↳59 QDP
↳60 MNOCProof (⇔)
↳61 QDP
↳62 QDP
↳63 UsableRulesProof (⇔)
↳64 QDP
↳65 QReductionProof (⇔)
↳66 QDP
↳67 QDPSizeChangeProof (⇔)
↳68 TRUE
↳69 QDP
↳70 UsableRulesProof (⇔)
↳71 QDP
↳72 QReductionProof (⇔)
↳73 QDP
↳74 QDPSizeChangeProof (⇔)
↳75 TRUE
↳76 QDP
↳77 UsableRulesProof (⇔)
↳78 QDP
↳79 QReductionProof (⇔)
↳80 QDP
↳81 QDPOrderProof (⇔)
↳82 QDP
↳83 UsableRulesProof (⇔)
↳84 QDP
↳85 QReductionProof (⇔)
↳86 QDP
↳87 QDPSizeChangeProof (⇔)
↳88 TRUE
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(nil) → 0
min(add(n, x)) → minIter(add(n, x), add(n, x), 0)
minIter(nil, add(n, y), m) → minIter(add(n, y), add(n, y), s(m))
minIter(add(n, x), y, m) → if_min(le(n, m), x, y, m)
if_min(true, x, y, m) → m
if_min(false, x, y, m) → minIter(x, y, m)
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(nil, nil) → nil
minsort(add(n, x), y) → if_minsort(eq(n, min(add(n, x))), add(n, x), y)
if_minsort(true, add(n, x), y) → add(n, minsort(app(rm(n, x), y), nil))
if_minsort(false, add(n, x), y) → minsort(x, add(n, y))
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(nil) → 0
min(add(n, x)) → minIter(add(n, x), add(n, x), 0)
minIter(nil, add(n, y), m) → minIter(add(n, y), add(n, y), s(m))
minIter(add(n, x), y, m) → if_min(le(n, m), x, y, m)
if_min(true, x, y, m) → m
if_min(false, x, y, m) → minIter(x, y, m)
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(nil, nil) → nil
minsort(add(n, x), y) → if_minsort(eq(n, min(add(n, x))), add(n, x), y)
if_minsort(true, add(n, x), y) → add(n, minsort(app(rm(n, x), y), nil))
if_minsort(false, add(n, x), y) → minsort(x, add(n, y))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(nil)
min(add(x0, x1))
minIter(nil, add(x0, x1), x2)
minIter(add(x0, x1), x2, x3)
if_min(true, x0, x1, x2)
if_min(false, x0, x1, x2)
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
EQ(s(x), s(y)) → EQ(x, y)
LE(s(x), s(y)) → LE(x, y)
APP(add(n, x), y) → APP(x, y)
MIN(add(n, x)) → MINITER(add(n, x), add(n, x), 0)
MINITER(nil, add(n, y), m) → MINITER(add(n, y), add(n, y), s(m))
MINITER(add(n, x), y, m) → IF_MIN(le(n, m), x, y, m)
MINITER(add(n, x), y, m) → LE(n, m)
IF_MIN(false, x, y, m) → MINITER(x, y, m)
RM(n, add(m, x)) → IF_RM(eq(n, m), n, add(m, x))
RM(n, add(m, x)) → EQ(n, m)
IF_RM(true, n, add(m, x)) → RM(n, x)
IF_RM(false, n, add(m, x)) → RM(n, x)
MINSORT(add(n, x), y) → IF_MINSORT(eq(n, min(add(n, x))), add(n, x), y)
MINSORT(add(n, x), y) → EQ(n, min(add(n, x)))
MINSORT(add(n, x), y) → MIN(add(n, x))
IF_MINSORT(true, add(n, x), y) → MINSORT(app(rm(n, x), y), nil)
IF_MINSORT(true, add(n, x), y) → APP(rm(n, x), y)
IF_MINSORT(true, add(n, x), y) → RM(n, x)
IF_MINSORT(false, add(n, x), y) → MINSORT(x, add(n, y))
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(nil) → 0
min(add(n, x)) → minIter(add(n, x), add(n, x), 0)
minIter(nil, add(n, y), m) → minIter(add(n, y), add(n, y), s(m))
minIter(add(n, x), y, m) → if_min(le(n, m), x, y, m)
if_min(true, x, y, m) → m
if_min(false, x, y, m) → minIter(x, y, m)
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(nil, nil) → nil
minsort(add(n, x), y) → if_minsort(eq(n, min(add(n, x))), add(n, x), y)
if_minsort(true, add(n, x), y) → add(n, minsort(app(rm(n, x), y), nil))
if_minsort(false, add(n, x), y) → minsort(x, add(n, y))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(nil)
min(add(x0, x1))
minIter(nil, add(x0, x1), x2)
minIter(add(x0, x1), x2, x3)
if_min(true, x0, x1, x2)
if_min(false, x0, x1, x2)
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
APP(add(n, x), y) → APP(x, y)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(nil) → 0
min(add(n, x)) → minIter(add(n, x), add(n, x), 0)
minIter(nil, add(n, y), m) → minIter(add(n, y), add(n, y), s(m))
minIter(add(n, x), y, m) → if_min(le(n, m), x, y, m)
if_min(true, x, y, m) → m
if_min(false, x, y, m) → minIter(x, y, m)
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(nil, nil) → nil
minsort(add(n, x), y) → if_minsort(eq(n, min(add(n, x))), add(n, x), y)
if_minsort(true, add(n, x), y) → add(n, minsort(app(rm(n, x), y), nil))
if_minsort(false, add(n, x), y) → minsort(x, add(n, y))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(nil)
min(add(x0, x1))
minIter(nil, add(x0, x1), x2)
minIter(add(x0, x1), x2, x3)
if_min(true, x0, x1, x2)
if_min(false, x0, x1, x2)
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
APP(add(n, x), y) → APP(x, y)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(nil)
min(add(x0, x1))
minIter(nil, add(x0, x1), x2)
minIter(add(x0, x1), x2, x3)
if_min(true, x0, x1, x2)
if_min(false, x0, x1, x2)
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(nil)
min(add(x0, x1))
minIter(nil, add(x0, x1), x2)
minIter(add(x0, x1), x2, x3)
if_min(true, x0, x1, x2)
if_min(false, x0, x1, x2)
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
APP(add(n, x), y) → APP(x, y)
From the DPs we obtained the following set of size-change graphs:
LE(s(x), s(y)) → LE(x, y)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(nil) → 0
min(add(n, x)) → minIter(add(n, x), add(n, x), 0)
minIter(nil, add(n, y), m) → minIter(add(n, y), add(n, y), s(m))
minIter(add(n, x), y, m) → if_min(le(n, m), x, y, m)
if_min(true, x, y, m) → m
if_min(false, x, y, m) → minIter(x, y, m)
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(nil, nil) → nil
minsort(add(n, x), y) → if_minsort(eq(n, min(add(n, x))), add(n, x), y)
if_minsort(true, add(n, x), y) → add(n, minsort(app(rm(n, x), y), nil))
if_minsort(false, add(n, x), y) → minsort(x, add(n, y))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(nil)
min(add(x0, x1))
minIter(nil, add(x0, x1), x2)
minIter(add(x0, x1), x2, x3)
if_min(true, x0, x1, x2)
if_min(false, x0, x1, x2)
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
LE(s(x), s(y)) → LE(x, y)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(nil)
min(add(x0, x1))
minIter(nil, add(x0, x1), x2)
minIter(add(x0, x1), x2, x3)
if_min(true, x0, x1, x2)
if_min(false, x0, x1, x2)
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(nil)
min(add(x0, x1))
minIter(nil, add(x0, x1), x2)
minIter(add(x0, x1), x2, x3)
if_min(true, x0, x1, x2)
if_min(false, x0, x1, x2)
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
LE(s(x), s(y)) → LE(x, y)
From the DPs we obtained the following set of size-change graphs:
MINITER(add(n, x), y, m) → IF_MIN(le(n, m), x, y, m)
IF_MIN(false, x, y, m) → MINITER(x, y, m)
MINITER(nil, add(n, y), m) → MINITER(add(n, y), add(n, y), s(m))
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(nil) → 0
min(add(n, x)) → minIter(add(n, x), add(n, x), 0)
minIter(nil, add(n, y), m) → minIter(add(n, y), add(n, y), s(m))
minIter(add(n, x), y, m) → if_min(le(n, m), x, y, m)
if_min(true, x, y, m) → m
if_min(false, x, y, m) → minIter(x, y, m)
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(nil, nil) → nil
minsort(add(n, x), y) → if_minsort(eq(n, min(add(n, x))), add(n, x), y)
if_minsort(true, add(n, x), y) → add(n, minsort(app(rm(n, x), y), nil))
if_minsort(false, add(n, x), y) → minsort(x, add(n, y))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(nil)
min(add(x0, x1))
minIter(nil, add(x0, x1), x2)
minIter(add(x0, x1), x2, x3)
if_min(true, x0, x1, x2)
if_min(false, x0, x1, x2)
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
MINITER(add(n, x), y, m) → IF_MIN(le(n, m), x, y, m)
IF_MIN(false, x, y, m) → MINITER(x, y, m)
MINITER(nil, add(n, y), m) → MINITER(add(n, y), add(n, y), s(m))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(nil)
min(add(x0, x1))
minIter(nil, add(x0, x1), x2)
minIter(add(x0, x1), x2, x3)
if_min(true, x0, x1, x2)
if_min(false, x0, x1, x2)
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(nil)
min(add(x0, x1))
minIter(nil, add(x0, x1), x2)
minIter(add(x0, x1), x2, x3)
if_min(true, x0, x1, x2)
if_min(false, x0, x1, x2)
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
MINITER(add(n, x), y, m) → IF_MIN(le(n, m), x, y, m)
IF_MIN(false, x, y, m) → MINITER(x, y, m)
MINITER(nil, add(n, y), m) → MINITER(add(n, y), add(n, y), s(m))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
MINITER(add(0, y1), y2, x0) → IF_MIN(true, y1, y2, x0)
MINITER(add(s(x0), y1), y2, 0) → IF_MIN(false, y1, y2, 0)
MINITER(add(s(x0), y1), y2, s(x1)) → IF_MIN(le(x0, x1), y1, y2, s(x1))
IF_MIN(false, x, y, m) → MINITER(x, y, m)
MINITER(nil, add(n, y), m) → MINITER(add(n, y), add(n, y), s(m))
MINITER(add(0, y1), y2, x0) → IF_MIN(true, y1, y2, x0)
MINITER(add(s(x0), y1), y2, 0) → IF_MIN(false, y1, y2, 0)
MINITER(add(s(x0), y1), y2, s(x1)) → IF_MIN(le(x0, x1), y1, y2, s(x1))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
MINITER(nil, add(n, y), m) → MINITER(add(n, y), add(n, y), s(m))
MINITER(add(s(x0), y1), y2, s(x1)) → IF_MIN(le(x0, x1), y1, y2, s(x1))
IF_MIN(false, x, y, m) → MINITER(x, y, m)
MINITER(add(s(x0), y1), y2, 0) → IF_MIN(false, y1, y2, 0)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
IF_MIN(false, z1, z2, s(z3)) → MINITER(z1, z2, s(z3))
IF_MIN(false, z1, z2, 0) → MINITER(z1, z2, 0)
MINITER(nil, add(n, y), m) → MINITER(add(n, y), add(n, y), s(m))
MINITER(add(s(x0), y1), y2, s(x1)) → IF_MIN(le(x0, x1), y1, y2, s(x1))
MINITER(add(s(x0), y1), y2, 0) → IF_MIN(false, y1, y2, 0)
IF_MIN(false, z1, z2, s(z3)) → MINITER(z1, z2, s(z3))
IF_MIN(false, z1, z2, 0) → MINITER(z1, z2, 0)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
MINITER(add(s(x0), y1), y2, s(x1)) → IF_MIN(le(x0, x1), y1, y2, s(x1))
IF_MIN(false, z1, z2, s(z3)) → MINITER(z1, z2, s(z3))
MINITER(nil, add(n, y), m) → MINITER(add(n, y), add(n, y), s(m))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
MINITER(nil, add(x0, x1), s(z2)) → MINITER(add(x0, x1), add(x0, x1), s(s(z2)))
MINITER(add(s(x0), y1), y2, s(x1)) → IF_MIN(le(x0, x1), y1, y2, s(x1))
IF_MIN(false, z1, z2, s(z3)) → MINITER(z1, z2, s(z3))
MINITER(nil, add(x0, x1), s(z2)) → MINITER(add(x0, x1), add(x0, x1), s(s(z2)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
IF_MIN(false, add(s(y_0), y_1), x1, s(x2)) → MINITER(add(s(y_0), y_1), x1, s(x2))
IF_MIN(false, nil, add(y_0, y_1), s(x2)) → MINITER(nil, add(y_0, y_1), s(x2))
MINITER(add(s(x0), y1), y2, s(x1)) → IF_MIN(le(x0, x1), y1, y2, s(x1))
MINITER(nil, add(x0, x1), s(z2)) → MINITER(add(x0, x1), add(x0, x1), s(s(z2)))
IF_MIN(false, add(s(y_0), y_1), x1, s(x2)) → MINITER(add(s(y_0), y_1), x1, s(x2))
IF_MIN(false, nil, add(y_0, y_1), s(x2)) → MINITER(nil, add(y_0, y_1), s(x2))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
MINITER(add(s(x0), add(s(y_1), y_2)), x2, s(x3)) → IF_MIN(le(x0, x3), add(s(y_1), y_2), x2, s(x3))
MINITER(add(s(x0), nil), add(y_1, y_2), s(x3)) → IF_MIN(le(x0, x3), nil, add(y_1, y_2), s(x3))
MINITER(nil, add(x0, x1), s(z2)) → MINITER(add(x0, x1), add(x0, x1), s(s(z2)))
IF_MIN(false, add(s(y_0), y_1), x1, s(x2)) → MINITER(add(s(y_0), y_1), x1, s(x2))
IF_MIN(false, nil, add(y_0, y_1), s(x2)) → MINITER(nil, add(y_0, y_1), s(x2))
MINITER(add(s(x0), add(s(y_1), y_2)), x2, s(x3)) → IF_MIN(le(x0, x3), add(s(y_1), y_2), x2, s(x3))
MINITER(add(s(x0), nil), add(y_1, y_2), s(x3)) → IF_MIN(le(x0, x3), nil, add(y_1, y_2), s(x3))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
MINITER(nil, add(s(y_0), add(s(y_1), y_2)), s(x2)) → MINITER(add(s(y_0), add(s(y_1), y_2)), add(s(y_0), add(s(y_1), y_2)), s(s(x2)))
MINITER(nil, add(s(y_0), nil), s(x2)) → MINITER(add(s(y_0), nil), add(s(y_0), nil), s(s(x2)))
IF_MIN(false, add(s(y_0), y_1), x1, s(x2)) → MINITER(add(s(y_0), y_1), x1, s(x2))
IF_MIN(false, nil, add(y_0, y_1), s(x2)) → MINITER(nil, add(y_0, y_1), s(x2))
MINITER(add(s(x0), add(s(y_1), y_2)), x2, s(x3)) → IF_MIN(le(x0, x3), add(s(y_1), y_2), x2, s(x3))
MINITER(add(s(x0), nil), add(y_1, y_2), s(x3)) → IF_MIN(le(x0, x3), nil, add(y_1, y_2), s(x3))
MINITER(nil, add(s(y_0), add(s(y_1), y_2)), s(x2)) → MINITER(add(s(y_0), add(s(y_1), y_2)), add(s(y_0), add(s(y_1), y_2)), s(s(x2)))
MINITER(nil, add(s(y_0), nil), s(x2)) → MINITER(add(s(y_0), nil), add(s(y_0), nil), s(s(x2)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
IF_MIN(false, add(s(y_0), y_1), x1, s(x2)) → MINITER(add(s(y_0), y_1), x1, s(x2))
IF_MIN(false, nil, add(y_0, y_1), s(x2)) → MINITER(nil, add(y_0, y_1), s(x2))
MINITER(add(s(x0), add(s(y_1), y_2)), x2, s(x3)) → IF_MIN(le(x0, x3), add(s(y_1), y_2), x2, s(x3))
MINITER(add(s(x0), nil), add(y_1, y_2), s(x3)) → IF_MIN(le(x0, x3), nil, add(y_1, y_2), s(x3))
MINITER(nil, add(s(y_0), add(s(y_1), y_2)), s(x2)) → MINITER(add(s(y_0), add(s(y_1), y_2)), add(s(y_0), add(s(y_1), y_2)), s(s(x2)))
MINITER(nil, add(s(y_0), nil), s(x2)) → MINITER(add(s(y_0), nil), add(s(y_0), nil), s(s(x2)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
MINITER(add(s(x0), y1), y2, 0) → IF_MIN(false, y1, y2, 0)
IF_MIN(false, z1, z2, 0) → MINITER(z1, z2, 0)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
MINITER(add(s(x0), y1), y2, 0) → IF_MIN(false, y1, y2, 0)
IF_MIN(false, z1, z2, 0) → MINITER(z1, z2, 0)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
MINITER(add(s(x0), y1), y2, 0) → IF_MIN(false, y1, y2, 0)
IF_MIN(false, z1, z2, 0) → MINITER(z1, z2, 0)
IF_MIN(false, add(s(y_0), y_1), x1, 0) → MINITER(add(s(y_0), y_1), x1, 0)
MINITER(add(s(x0), y1), y2, 0) → IF_MIN(false, y1, y2, 0)
IF_MIN(false, add(s(y_0), y_1), x1, 0) → MINITER(add(s(y_0), y_1), x1, 0)
MINITER(add(s(x0), add(s(y_0), y_1)), x2, 0) → IF_MIN(false, add(s(y_0), y_1), x2, 0)
IF_MIN(false, add(s(y_0), y_1), x1, 0) → MINITER(add(s(y_0), y_1), x1, 0)
MINITER(add(s(x0), add(s(y_0), y_1)), x2, 0) → IF_MIN(false, add(s(y_0), y_1), x2, 0)
From the DPs we obtained the following set of size-change graphs:
MINITER(add(n, x), y, m) → IF_MIN(le(n, m), x, y, m)
IF_MIN(false, x, y, m) → MINITER(x, y, m)
MINITER(nil, add(n, y), m) → MINITER(add(n, y), add(n, y), s(m))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(nil)
min(add(x0, x1))
minIter(nil, add(x0, x1), x2)
minIter(add(x0, x1), x2, x3)
if_min(true, x0, x1, x2)
if_min(false, x0, x1, x2)
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(nil)
min(add(x0, x1))
minIter(nil, add(x0, x1), x2)
minIter(add(x0, x1), x2, x3)
if_min(true, x0, x1, x2)
if_min(false, x0, x1, x2)
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
MINITER(add(n, x), y, m) → IF_MIN(le(n, m), x, y, m)
IF_MIN(false, x, y, m) → MINITER(x, y, m)
MINITER(nil, add(n, y), m) → MINITER(add(n, y), add(n, y), s(m))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
MINITER(add(n, x), y, m) → IF_MIN(le(n, m), x, y, m)
IF_MIN(false, x, y, m) → MINITER(x, y, m)
MINITER(nil, add(n, y), m) → MINITER(add(n, y), add(n, y), s(m))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
EQ(s(x), s(y)) → EQ(x, y)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(nil) → 0
min(add(n, x)) → minIter(add(n, x), add(n, x), 0)
minIter(nil, add(n, y), m) → minIter(add(n, y), add(n, y), s(m))
minIter(add(n, x), y, m) → if_min(le(n, m), x, y, m)
if_min(true, x, y, m) → m
if_min(false, x, y, m) → minIter(x, y, m)
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(nil, nil) → nil
minsort(add(n, x), y) → if_minsort(eq(n, min(add(n, x))), add(n, x), y)
if_minsort(true, add(n, x), y) → add(n, minsort(app(rm(n, x), y), nil))
if_minsort(false, add(n, x), y) → minsort(x, add(n, y))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(nil)
min(add(x0, x1))
minIter(nil, add(x0, x1), x2)
minIter(add(x0, x1), x2, x3)
if_min(true, x0, x1, x2)
if_min(false, x0, x1, x2)
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
EQ(s(x), s(y)) → EQ(x, y)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(nil)
min(add(x0, x1))
minIter(nil, add(x0, x1), x2)
minIter(add(x0, x1), x2, x3)
if_min(true, x0, x1, x2)
if_min(false, x0, x1, x2)
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(nil)
min(add(x0, x1))
minIter(nil, add(x0, x1), x2)
minIter(add(x0, x1), x2, x3)
if_min(true, x0, x1, x2)
if_min(false, x0, x1, x2)
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
EQ(s(x), s(y)) → EQ(x, y)
From the DPs we obtained the following set of size-change graphs:
RM(n, add(m, x)) → IF_RM(eq(n, m), n, add(m, x))
IF_RM(true, n, add(m, x)) → RM(n, x)
IF_RM(false, n, add(m, x)) → RM(n, x)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(nil) → 0
min(add(n, x)) → minIter(add(n, x), add(n, x), 0)
minIter(nil, add(n, y), m) → minIter(add(n, y), add(n, y), s(m))
minIter(add(n, x), y, m) → if_min(le(n, m), x, y, m)
if_min(true, x, y, m) → m
if_min(false, x, y, m) → minIter(x, y, m)
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(nil, nil) → nil
minsort(add(n, x), y) → if_minsort(eq(n, min(add(n, x))), add(n, x), y)
if_minsort(true, add(n, x), y) → add(n, minsort(app(rm(n, x), y), nil))
if_minsort(false, add(n, x), y) → minsort(x, add(n, y))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(nil)
min(add(x0, x1))
minIter(nil, add(x0, x1), x2)
minIter(add(x0, x1), x2, x3)
if_min(true, x0, x1, x2)
if_min(false, x0, x1, x2)
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
RM(n, add(m, x)) → IF_RM(eq(n, m), n, add(m, x))
IF_RM(true, n, add(m, x)) → RM(n, x)
IF_RM(false, n, add(m, x)) → RM(n, x)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(nil)
min(add(x0, x1))
minIter(nil, add(x0, x1), x2)
minIter(add(x0, x1), x2, x3)
if_min(true, x0, x1, x2)
if_min(false, x0, x1, x2)
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(nil)
min(add(x0, x1))
minIter(nil, add(x0, x1), x2)
minIter(add(x0, x1), x2, x3)
if_min(true, x0, x1, x2)
if_min(false, x0, x1, x2)
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
RM(n, add(m, x)) → IF_RM(eq(n, m), n, add(m, x))
IF_RM(true, n, add(m, x)) → RM(n, x)
IF_RM(false, n, add(m, x)) → RM(n, x)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
From the DPs we obtained the following set of size-change graphs:
IF_MINSORT(true, add(n, x), y) → MINSORT(app(rm(n, x), y), nil)
MINSORT(add(n, x), y) → IF_MINSORT(eq(n, min(add(n, x))), add(n, x), y)
IF_MINSORT(false, add(n, x), y) → MINSORT(x, add(n, y))
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(nil) → 0
min(add(n, x)) → minIter(add(n, x), add(n, x), 0)
minIter(nil, add(n, y), m) → minIter(add(n, y), add(n, y), s(m))
minIter(add(n, x), y, m) → if_min(le(n, m), x, y, m)
if_min(true, x, y, m) → m
if_min(false, x, y, m) → minIter(x, y, m)
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(nil, nil) → nil
minsort(add(n, x), y) → if_minsort(eq(n, min(add(n, x))), add(n, x), y)
if_minsort(true, add(n, x), y) → add(n, minsort(app(rm(n, x), y), nil))
if_minsort(false, add(n, x), y) → minsort(x, add(n, y))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(nil)
min(add(x0, x1))
minIter(nil, add(x0, x1), x2)
minIter(add(x0, x1), x2, x3)
if_min(true, x0, x1, x2)
if_min(false, x0, x1, x2)
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
IF_MINSORT(true, add(n, x), y) → MINSORT(app(rm(n, x), y), nil)
MINSORT(add(n, x), y) → IF_MINSORT(eq(n, min(add(n, x))), add(n, x), y)
IF_MINSORT(false, add(n, x), y) → MINSORT(x, add(n, y))
min(add(n, x)) → minIter(add(n, x), add(n, x), 0)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if_min(false, x, y, m) → minIter(x, y, m)
minIter(add(n, x), y, m) → if_min(le(n, m), x, y, m)
minIter(nil, add(n, y), m) → minIter(add(n, y), add(n, y), s(m))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
if_min(true, x, y, m) → m
rm(n, nil) → nil
if_rm(true, n, add(m, x)) → rm(n, x)
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(nil)
min(add(x0, x1))
minIter(nil, add(x0, x1), x2)
minIter(add(x0, x1), x2, x3)
if_min(true, x0, x1, x2)
if_min(false, x0, x1, x2)
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
IF_MINSORT(true, add(n, x), y) → MINSORT(app(rm(n, x), y), nil)
MINSORT(add(n, x), y) → IF_MINSORT(eq(n, min(add(n, x))), add(n, x), y)
IF_MINSORT(false, add(n, x), y) → MINSORT(x, add(n, y))
min(add(n, x)) → minIter(add(n, x), add(n, x), 0)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if_min(false, x, y, m) → minIter(x, y, m)
minIter(add(n, x), y, m) → if_min(le(n, m), x, y, m)
minIter(nil, add(n, y), m) → minIter(add(n, y), add(n, y), s(m))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
if_min(true, x, y, m) → m
rm(n, nil) → nil
if_rm(true, n, add(m, x)) → rm(n, x)
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(nil)
min(add(x0, x1))
minIter(nil, add(x0, x1), x2)
minIter(add(x0, x1), x2, x3)
if_min(true, x0, x1, x2)
if_min(false, x0, x1, x2)
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IF_MINSORT(true, add(n, x), y) → MINSORT(app(rm(n, x), y), nil)
POL(0) = 0
POL(IF_MINSORT(x1, x2, x3)) = x2 + x3
POL(MINSORT(x1, x2)) = x1 + x2
POL(add(x1, x2)) = 1 + x2
POL(app(x1, x2)) = x1 + x2
POL(eq(x1, x2)) = 0
POL(false) = 0
POL(if_min(x1, x2, x3, x4)) = 0
POL(if_rm(x1, x2, x3)) = x3
POL(le(x1, x2)) = 1
POL(min(x1)) = 0
POL(minIter(x1, x2, x3)) = 0
POL(nil) = 0
POL(rm(x1, x2)) = x2
POL(s(x1)) = 0
POL(true) = 0
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
app(add(n, x), y) → add(n, app(x, y))
app(nil, y) → y
if_rm(true, n, add(m, x)) → rm(n, x)
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
rm(n, nil) → nil
MINSORT(add(n, x), y) → IF_MINSORT(eq(n, min(add(n, x))), add(n, x), y)
IF_MINSORT(false, add(n, x), y) → MINSORT(x, add(n, y))
min(add(n, x)) → minIter(add(n, x), add(n, x), 0)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if_min(false, x, y, m) → minIter(x, y, m)
minIter(add(n, x), y, m) → if_min(le(n, m), x, y, m)
minIter(nil, add(n, y), m) → minIter(add(n, y), add(n, y), s(m))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
if_min(true, x, y, m) → m
rm(n, nil) → nil
if_rm(true, n, add(m, x)) → rm(n, x)
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(nil)
min(add(x0, x1))
minIter(nil, add(x0, x1), x2)
minIter(add(x0, x1), x2, x3)
if_min(true, x0, x1, x2)
if_min(false, x0, x1, x2)
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
MINSORT(add(n, x), y) → IF_MINSORT(eq(n, min(add(n, x))), add(n, x), y)
IF_MINSORT(false, add(n, x), y) → MINSORT(x, add(n, y))
min(add(n, x)) → minIter(add(n, x), add(n, x), 0)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if_min(false, x, y, m) → minIter(x, y, m)
minIter(add(n, x), y, m) → if_min(le(n, m), x, y, m)
minIter(nil, add(n, y), m) → minIter(add(n, y), add(n, y), s(m))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
if_min(true, x, y, m) → m
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(nil)
min(add(x0, x1))
minIter(nil, add(x0, x1), x2)
minIter(add(x0, x1), x2, x3)
if_min(true, x0, x1, x2)
if_min(false, x0, x1, x2)
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
app(nil, x0)
app(add(x0, x1), x2)
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
MINSORT(add(n, x), y) → IF_MINSORT(eq(n, min(add(n, x))), add(n, x), y)
IF_MINSORT(false, add(n, x), y) → MINSORT(x, add(n, y))
min(add(n, x)) → minIter(add(n, x), add(n, x), 0)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if_min(false, x, y, m) → minIter(x, y, m)
minIter(add(n, x), y, m) → if_min(le(n, m), x, y, m)
minIter(nil, add(n, y), m) → minIter(add(n, y), add(n, y), s(m))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
if_min(true, x, y, m) → m
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(nil)
min(add(x0, x1))
minIter(nil, add(x0, x1), x2)
minIter(add(x0, x1), x2, x3)
if_min(true, x0, x1, x2)
if_min(false, x0, x1, x2)
From the DPs we obtained the following set of size-change graphs: