0 QTRS
↳1 Overlay + Local Confluence (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔)
↳9 QDP
↳10 ATransformationProof (⇔)
↳11 QDP
↳12 QReductionProof (⇔)
↳13 QDP
↳14 QDPSizeChangeProof (⇔)
↳15 TRUE
↳16 QDP
↳17 UsableRulesProof (⇔)
↳18 QDP
↳19 ATransformationProof (⇔)
↳20 QDP
↳21 QReductionProof (⇔)
↳22 QDP
↳23 QDPOrderProof (⇔)
↳24 QDP
↳25 PisEmptyProof (⇔)
↳26 TRUE
↳27 QDP
↳28 UsableRulesProof (⇔)
↳29 QDP
↳30 ATransformationProof (⇔)
↳31 QDP
↳32 QReductionProof (⇔)
↳33 QDP
↳34 QDPOrderProof (⇔)
↳35 QDP
↳36 PisEmptyProof (⇔)
↳37 TRUE
↳38 QDP
↳39 QDPSizeChangeProof (⇔)
↳40 TRUE
app(app(minus, x), 0) → x
app(app(minus, app(s, x)), app(s, y)) → app(app(minus, x), y)
app(app(quot, 0), app(s, y)) → 0
app(app(quot, app(s, x)), app(s, y)) → app(s, app(app(quot, app(app(minus, x), y)), app(s, y)))
app(log, app(s, 0)) → 0
app(log, app(s, app(s, x))) → app(s, app(log, app(s, app(app(quot, x), app(s, app(s, 0))))))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(app(filter, f), nil) → nil
app(app(filter, f), app(app(cons, x), xs)) → app(app(app(app(filter2, app(f, x)), f), x), xs)
app(app(app(app(filter2, true), f), x), xs) → app(app(cons, x), app(app(filter, f), xs))
app(app(app(app(filter2, false), f), x), xs) → app(app(filter, f), xs)
app(app(minus, x), 0) → x
app(app(minus, app(s, x)), app(s, y)) → app(app(minus, x), y)
app(app(quot, 0), app(s, y)) → 0
app(app(quot, app(s, x)), app(s, y)) → app(s, app(app(quot, app(app(minus, x), y)), app(s, y)))
app(log, app(s, 0)) → 0
app(log, app(s, app(s, x))) → app(s, app(log, app(s, app(app(quot, x), app(s, app(s, 0))))))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(app(filter, f), nil) → nil
app(app(filter, f), app(app(cons, x), xs)) → app(app(app(app(filter2, app(f, x)), f), x), xs)
app(app(app(app(filter2, true), f), x), xs) → app(app(cons, x), app(app(filter, f), xs))
app(app(app(app(filter2, false), f), x), xs) → app(app(filter, f), xs)
app(app(minus, x0), 0)
app(app(minus, app(s, x0)), app(s, x1))
app(app(quot, 0), app(s, x0))
app(app(quot, app(s, x0)), app(s, x1))
app(log, app(s, 0))
app(log, app(s, app(s, x0)))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(app(filter2, true), x0), x1), x2)
app(app(app(app(filter2, false), x0), x1), x2)
APP(app(minus, app(s, x)), app(s, y)) → APP(app(minus, x), y)
APP(app(minus, app(s, x)), app(s, y)) → APP(minus, x)
APP(app(quot, app(s, x)), app(s, y)) → APP(s, app(app(quot, app(app(minus, x), y)), app(s, y)))
APP(app(quot, app(s, x)), app(s, y)) → APP(app(quot, app(app(minus, x), y)), app(s, y))
APP(app(quot, app(s, x)), app(s, y)) → APP(quot, app(app(minus, x), y))
APP(app(quot, app(s, x)), app(s, y)) → APP(app(minus, x), y)
APP(app(quot, app(s, x)), app(s, y)) → APP(minus, x)
APP(log, app(s, app(s, x))) → APP(s, app(log, app(s, app(app(quot, x), app(s, app(s, 0))))))
APP(log, app(s, app(s, x))) → APP(log, app(s, app(app(quot, x), app(s, app(s, 0)))))
APP(log, app(s, app(s, x))) → APP(s, app(app(quot, x), app(s, app(s, 0))))
APP(log, app(s, app(s, x))) → APP(app(quot, x), app(s, app(s, 0)))
APP(log, app(s, app(s, x))) → APP(quot, x)
APP(log, app(s, app(s, x))) → APP(s, app(s, 0))
APP(log, app(s, app(s, x))) → APP(s, 0)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(cons, app(f, x)), app(app(map, f), xs))
APP(app(map, f), app(app(cons, x), xs)) → APP(cons, app(f, x))
APP(app(map, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
APP(app(filter, f), app(app(cons, x), xs)) → APP(app(app(app(filter2, app(f, x)), f), x), xs)
APP(app(filter, f), app(app(cons, x), xs)) → APP(app(app(filter2, app(f, x)), f), x)
APP(app(filter, f), app(app(cons, x), xs)) → APP(app(filter2, app(f, x)), f)
APP(app(filter, f), app(app(cons, x), xs)) → APP(filter2, app(f, x))
APP(app(filter, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(app(app(filter2, true), f), x), xs) → APP(app(cons, x), app(app(filter, f), xs))
APP(app(app(app(filter2, true), f), x), xs) → APP(cons, x)
APP(app(app(app(filter2, true), f), x), xs) → APP(app(filter, f), xs)
APP(app(app(app(filter2, true), f), x), xs) → APP(filter, f)
APP(app(app(app(filter2, false), f), x), xs) → APP(app(filter, f), xs)
APP(app(app(app(filter2, false), f), x), xs) → APP(filter, f)
app(app(minus, x), 0) → x
app(app(minus, app(s, x)), app(s, y)) → app(app(minus, x), y)
app(app(quot, 0), app(s, y)) → 0
app(app(quot, app(s, x)), app(s, y)) → app(s, app(app(quot, app(app(minus, x), y)), app(s, y)))
app(log, app(s, 0)) → 0
app(log, app(s, app(s, x))) → app(s, app(log, app(s, app(app(quot, x), app(s, app(s, 0))))))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(app(filter, f), nil) → nil
app(app(filter, f), app(app(cons, x), xs)) → app(app(app(app(filter2, app(f, x)), f), x), xs)
app(app(app(app(filter2, true), f), x), xs) → app(app(cons, x), app(app(filter, f), xs))
app(app(app(app(filter2, false), f), x), xs) → app(app(filter, f), xs)
app(app(minus, x0), 0)
app(app(minus, app(s, x0)), app(s, x1))
app(app(quot, 0), app(s, x0))
app(app(quot, app(s, x0)), app(s, x1))
app(log, app(s, 0))
app(log, app(s, app(s, x0)))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(app(filter2, true), x0), x1), x2)
app(app(app(app(filter2, false), x0), x1), x2)
APP(app(minus, app(s, x)), app(s, y)) → APP(app(minus, x), y)
app(app(minus, x), 0) → x
app(app(minus, app(s, x)), app(s, y)) → app(app(minus, x), y)
app(app(quot, 0), app(s, y)) → 0
app(app(quot, app(s, x)), app(s, y)) → app(s, app(app(quot, app(app(minus, x), y)), app(s, y)))
app(log, app(s, 0)) → 0
app(log, app(s, app(s, x))) → app(s, app(log, app(s, app(app(quot, x), app(s, app(s, 0))))))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(app(filter, f), nil) → nil
app(app(filter, f), app(app(cons, x), xs)) → app(app(app(app(filter2, app(f, x)), f), x), xs)
app(app(app(app(filter2, true), f), x), xs) → app(app(cons, x), app(app(filter, f), xs))
app(app(app(app(filter2, false), f), x), xs) → app(app(filter, f), xs)
app(app(minus, x0), 0)
app(app(minus, app(s, x0)), app(s, x1))
app(app(quot, 0), app(s, x0))
app(app(quot, app(s, x0)), app(s, x1))
app(log, app(s, 0))
app(log, app(s, app(s, x0)))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(app(filter2, true), x0), x1), x2)
app(app(app(app(filter2, false), x0), x1), x2)
APP(app(minus, app(s, x)), app(s, y)) → APP(app(minus, x), y)
app(app(minus, x0), 0)
app(app(minus, app(s, x0)), app(s, x1))
app(app(quot, 0), app(s, x0))
app(app(quot, app(s, x0)), app(s, x1))
app(log, app(s, 0))
app(log, app(s, app(s, x0)))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(app(filter2, true), x0), x1), x2)
app(app(app(app(filter2, false), x0), x1), x2)
minus1(s(x), s(y)) → minus1(x, y)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
log(s(0))
log(s(s(x0)))
map(x0, nil)
map(x0, cons(x1, x2))
filter(x0, nil)
filter(x0, cons(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
log(s(0))
log(s(s(x0)))
map(x0, nil)
map(x0, cons(x1, x2))
filter(x0, nil)
filter(x0, cons(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)
minus1(s(x), s(y)) → minus1(x, y)
From the DPs we obtained the following set of size-change graphs:
APP(app(quot, app(s, x)), app(s, y)) → APP(app(quot, app(app(minus, x), y)), app(s, y))
app(app(minus, x), 0) → x
app(app(minus, app(s, x)), app(s, y)) → app(app(minus, x), y)
app(app(quot, 0), app(s, y)) → 0
app(app(quot, app(s, x)), app(s, y)) → app(s, app(app(quot, app(app(minus, x), y)), app(s, y)))
app(log, app(s, 0)) → 0
app(log, app(s, app(s, x))) → app(s, app(log, app(s, app(app(quot, x), app(s, app(s, 0))))))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(app(filter, f), nil) → nil
app(app(filter, f), app(app(cons, x), xs)) → app(app(app(app(filter2, app(f, x)), f), x), xs)
app(app(app(app(filter2, true), f), x), xs) → app(app(cons, x), app(app(filter, f), xs))
app(app(app(app(filter2, false), f), x), xs) → app(app(filter, f), xs)
app(app(minus, x0), 0)
app(app(minus, app(s, x0)), app(s, x1))
app(app(quot, 0), app(s, x0))
app(app(quot, app(s, x0)), app(s, x1))
app(log, app(s, 0))
app(log, app(s, app(s, x0)))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(app(filter2, true), x0), x1), x2)
app(app(app(app(filter2, false), x0), x1), x2)
APP(app(quot, app(s, x)), app(s, y)) → APP(app(quot, app(app(minus, x), y)), app(s, y))
app(app(minus, x), 0) → x
app(app(minus, app(s, x)), app(s, y)) → app(app(minus, x), y)
app(app(minus, x0), 0)
app(app(minus, app(s, x0)), app(s, x1))
app(app(quot, 0), app(s, x0))
app(app(quot, app(s, x0)), app(s, x1))
app(log, app(s, 0))
app(log, app(s, app(s, x0)))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(app(filter2, true), x0), x1), x2)
app(app(app(app(filter2, false), x0), x1), x2)
quot1(s(x), s(y)) → quot1(minus(x, y), s(y))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
log(s(0))
log(s(s(x0)))
map(x0, nil)
map(x0, cons(x1, x2))
filter(x0, nil)
filter(x0, cons(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)
quot(0, s(x0))
quot(s(x0), s(x1))
log(s(0))
log(s(s(x0)))
map(x0, nil)
map(x0, cons(x1, x2))
filter(x0, nil)
filter(x0, cons(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)
quot1(s(x), s(y)) → quot1(minus(x, y), s(y))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(x0, 0)
minus(s(x0), s(x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
quot1(s(x), s(y)) → quot1(minus(x, y), s(y))
POL(0) = 0
POL(minus(x1, x2)) = x1
POL(quot1(x1, x2)) = x1
POL(s(x1)) = 1 + x1
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(x0, 0)
minus(s(x0), s(x1))
APP(log, app(s, app(s, x))) → APP(log, app(s, app(app(quot, x), app(s, app(s, 0)))))
app(app(minus, x), 0) → x
app(app(minus, app(s, x)), app(s, y)) → app(app(minus, x), y)
app(app(quot, 0), app(s, y)) → 0
app(app(quot, app(s, x)), app(s, y)) → app(s, app(app(quot, app(app(minus, x), y)), app(s, y)))
app(log, app(s, 0)) → 0
app(log, app(s, app(s, x))) → app(s, app(log, app(s, app(app(quot, x), app(s, app(s, 0))))))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(app(filter, f), nil) → nil
app(app(filter, f), app(app(cons, x), xs)) → app(app(app(app(filter2, app(f, x)), f), x), xs)
app(app(app(app(filter2, true), f), x), xs) → app(app(cons, x), app(app(filter, f), xs))
app(app(app(app(filter2, false), f), x), xs) → app(app(filter, f), xs)
app(app(minus, x0), 0)
app(app(minus, app(s, x0)), app(s, x1))
app(app(quot, 0), app(s, x0))
app(app(quot, app(s, x0)), app(s, x1))
app(log, app(s, 0))
app(log, app(s, app(s, x0)))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(app(filter2, true), x0), x1), x2)
app(app(app(app(filter2, false), x0), x1), x2)
APP(log, app(s, app(s, x))) → APP(log, app(s, app(app(quot, x), app(s, app(s, 0)))))
app(app(quot, 0), app(s, y)) → 0
app(app(quot, app(s, x)), app(s, y)) → app(s, app(app(quot, app(app(minus, x), y)), app(s, y)))
app(app(minus, x), 0) → x
app(app(minus, app(s, x)), app(s, y)) → app(app(minus, x), y)
app(app(minus, x0), 0)
app(app(minus, app(s, x0)), app(s, x1))
app(app(quot, 0), app(s, x0))
app(app(quot, app(s, x0)), app(s, x1))
app(log, app(s, 0))
app(log, app(s, app(s, x0)))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(app(filter2, true), x0), x1), x2)
app(app(app(app(filter2, false), x0), x1), x2)
log1(s(s(x))) → log1(s(quot(x, s(s(0)))))
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
log(s(0))
log(s(s(x0)))
map(x0, nil)
map(x0, cons(x1, x2))
filter(x0, nil)
filter(x0, cons(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)
log(s(0))
log(s(s(x0)))
map(x0, nil)
map(x0, cons(x1, x2))
filter(x0, nil)
filter(x0, cons(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)
log1(s(s(x))) → log1(s(quot(x, s(s(0)))))
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
log1(s(s(x))) → log1(s(quot(x, s(s(0)))))
POL(0) = 0
POL(log1(x1)) = x1
POL(minus(x1, x2)) = x1
POL(quot(x1, x2)) = x1
POL(s(x1)) = 1 + x1
quot(0, s(y)) → 0
minus(x, 0) → x
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
APP(app(map, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(filter, f), app(app(cons, x), xs)) → APP(app(app(app(filter2, app(f, x)), f), x), xs)
APP(app(app(app(filter2, true), f), x), xs) → APP(app(filter, f), xs)
APP(app(filter, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(app(app(filter2, false), f), x), xs) → APP(app(filter, f), xs)
app(app(minus, x), 0) → x
app(app(minus, app(s, x)), app(s, y)) → app(app(minus, x), y)
app(app(quot, 0), app(s, y)) → 0
app(app(quot, app(s, x)), app(s, y)) → app(s, app(app(quot, app(app(minus, x), y)), app(s, y)))
app(log, app(s, 0)) → 0
app(log, app(s, app(s, x))) → app(s, app(log, app(s, app(app(quot, x), app(s, app(s, 0))))))
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))
app(app(filter, f), nil) → nil
app(app(filter, f), app(app(cons, x), xs)) → app(app(app(app(filter2, app(f, x)), f), x), xs)
app(app(app(app(filter2, true), f), x), xs) → app(app(cons, x), app(app(filter, f), xs))
app(app(app(app(filter2, false), f), x), xs) → app(app(filter, f), xs)
app(app(minus, x0), 0)
app(app(minus, app(s, x0)), app(s, x1))
app(app(quot, 0), app(s, x0))
app(app(quot, app(s, x0)), app(s, x1))
app(log, app(s, 0))
app(log, app(s, app(s, x0)))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(app(filter2, true), x0), x1), x2)
app(app(app(app(filter2, false), x0), x1), x2)
From the DPs we obtained the following set of size-change graphs: