0 QTRS
↳1 Overlay + Local Confluence (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 QDP
↳8 QDPOrderProof (⇔)
↳9 QDP
↳10 PisEmptyProof (⇔)
↳11 TRUE
↳12 QDP
↳13 QDPOrderProof (⇔)
↳14 QDP
↳15 DependencyGraphProof (⇔)
↳16 TRUE
app(app(neq, 0), 0) → false
app(app(neq, 0), app(s, y)) → true
app(app(neq, app(s, x)), 0) → true
app(app(neq, app(s, x)), app(s, y)) → app(app(neq, x), y)
app(app(filter, f), nil) → nil
app(app(filter, f), app(app(cons, y), ys)) → app(app(app(filtersub, app(f, y)), f), app(app(cons, y), ys))
app(app(app(filtersub, true), f), app(app(cons, y), ys)) → app(app(cons, y), app(app(filter, f), ys))
app(app(app(filtersub, false), f), app(app(cons, y), ys)) → app(app(filter, f), ys)
nonzero → app(filter, app(neq, 0))
app(app(neq, 0), 0) → false
app(app(neq, 0), app(s, y)) → true
app(app(neq, app(s, x)), 0) → true
app(app(neq, app(s, x)), app(s, y)) → app(app(neq, x), y)
app(app(filter, f), nil) → nil
app(app(filter, f), app(app(cons, y), ys)) → app(app(app(filtersub, app(f, y)), f), app(app(cons, y), ys))
app(app(app(filtersub, true), f), app(app(cons, y), ys)) → app(app(cons, y), app(app(filter, f), ys))
app(app(app(filtersub, false), f), app(app(cons, y), ys)) → app(app(filter, f), ys)
nonzero → app(filter, app(neq, 0))
app(app(neq, 0), 0)
app(app(neq, 0), app(s, x0))
app(app(neq, app(s, x0)), 0)
app(app(neq, app(s, x0)), app(s, x1))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(filtersub, true), x0), app(app(cons, x1), x2))
app(app(app(filtersub, false), x0), app(app(cons, x1), x2))
nonzero
APP(app(neq, app(s, x)), app(s, y)) → APP(app(neq, x), y)
APP(app(neq, app(s, x)), app(s, y)) → APP(neq, x)
APP(app(filter, f), app(app(cons, y), ys)) → APP(app(app(filtersub, app(f, y)), f), app(app(cons, y), ys))
APP(app(filter, f), app(app(cons, y), ys)) → APP(app(filtersub, app(f, y)), f)
APP(app(filter, f), app(app(cons, y), ys)) → APP(filtersub, app(f, y))
APP(app(filter, f), app(app(cons, y), ys)) → APP(f, y)
APP(app(app(filtersub, true), f), app(app(cons, y), ys)) → APP(app(cons, y), app(app(filter, f), ys))
APP(app(app(filtersub, true), f), app(app(cons, y), ys)) → APP(app(filter, f), ys)
APP(app(app(filtersub, true), f), app(app(cons, y), ys)) → APP(filter, f)
APP(app(app(filtersub, false), f), app(app(cons, y), ys)) → APP(app(filter, f), ys)
APP(app(app(filtersub, false), f), app(app(cons, y), ys)) → APP(filter, f)
NONZERO → APP(filter, app(neq, 0))
NONZERO → APP(neq, 0)
app(app(neq, 0), 0) → false
app(app(neq, 0), app(s, y)) → true
app(app(neq, app(s, x)), 0) → true
app(app(neq, app(s, x)), app(s, y)) → app(app(neq, x), y)
app(app(filter, f), nil) → nil
app(app(filter, f), app(app(cons, y), ys)) → app(app(app(filtersub, app(f, y)), f), app(app(cons, y), ys))
app(app(app(filtersub, true), f), app(app(cons, y), ys)) → app(app(cons, y), app(app(filter, f), ys))
app(app(app(filtersub, false), f), app(app(cons, y), ys)) → app(app(filter, f), ys)
nonzero → app(filter, app(neq, 0))
app(app(neq, 0), 0)
app(app(neq, 0), app(s, x0))
app(app(neq, app(s, x0)), 0)
app(app(neq, app(s, x0)), app(s, x1))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(filtersub, true), x0), app(app(cons, x1), x2))
app(app(app(filtersub, false), x0), app(app(cons, x1), x2))
nonzero
APP(app(neq, app(s, x)), app(s, y)) → APP(app(neq, x), y)
app(app(neq, 0), 0) → false
app(app(neq, 0), app(s, y)) → true
app(app(neq, app(s, x)), 0) → true
app(app(neq, app(s, x)), app(s, y)) → app(app(neq, x), y)
app(app(filter, f), nil) → nil
app(app(filter, f), app(app(cons, y), ys)) → app(app(app(filtersub, app(f, y)), f), app(app(cons, y), ys))
app(app(app(filtersub, true), f), app(app(cons, y), ys)) → app(app(cons, y), app(app(filter, f), ys))
app(app(app(filtersub, false), f), app(app(cons, y), ys)) → app(app(filter, f), ys)
nonzero → app(filter, app(neq, 0))
app(app(neq, 0), 0)
app(app(neq, 0), app(s, x0))
app(app(neq, app(s, x0)), 0)
app(app(neq, app(s, x0)), app(s, x1))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(filtersub, true), x0), app(app(cons, x1), x2))
app(app(app(filtersub, false), x0), app(app(cons, x1), x2))
nonzero
neq1(s(x), s(y)) → neq1(x, y)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
APP(app(neq, app(s, x)), app(s, y)) → APP(app(neq, x), y)
trivial
neq11: [1]
s1: multiset
app(app(neq, 0), 0) → false
app(app(neq, 0), app(s, y)) → true
app(app(neq, app(s, x)), 0) → true
app(app(neq, app(s, x)), app(s, y)) → app(app(neq, x), y)
app(app(filter, f), nil) → nil
app(app(filter, f), app(app(cons, y), ys)) → app(app(app(filtersub, app(f, y)), f), app(app(cons, y), ys))
app(app(app(filtersub, true), f), app(app(cons, y), ys)) → app(app(cons, y), app(app(filter, f), ys))
app(app(app(filtersub, false), f), app(app(cons, y), ys)) → app(app(filter, f), ys)
nonzero → app(filter, app(neq, 0))
app(app(neq, 0), 0)
app(app(neq, 0), app(s, x0))
app(app(neq, app(s, x0)), 0)
app(app(neq, app(s, x0)), app(s, x1))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(filtersub, true), x0), app(app(cons, x1), x2))
app(app(app(filtersub, false), x0), app(app(cons, x1), x2))
nonzero
APP(app(filter, f), app(app(cons, y), ys)) → APP(app(app(filtersub, app(f, y)), f), app(app(cons, y), ys))
APP(app(app(filtersub, true), f), app(app(cons, y), ys)) → APP(app(filter, f), ys)
APP(app(filter, f), app(app(cons, y), ys)) → APP(f, y)
APP(app(app(filtersub, false), f), app(app(cons, y), ys)) → APP(app(filter, f), ys)
app(app(neq, 0), 0) → false
app(app(neq, 0), app(s, y)) → true
app(app(neq, app(s, x)), 0) → true
app(app(neq, app(s, x)), app(s, y)) → app(app(neq, x), y)
app(app(filter, f), nil) → nil
app(app(filter, f), app(app(cons, y), ys)) → app(app(app(filtersub, app(f, y)), f), app(app(cons, y), ys))
app(app(app(filtersub, true), f), app(app(cons, y), ys)) → app(app(cons, y), app(app(filter, f), ys))
app(app(app(filtersub, false), f), app(app(cons, y), ys)) → app(app(filter, f), ys)
nonzero → app(filter, app(neq, 0))
app(app(neq, 0), 0)
app(app(neq, 0), app(s, x0))
app(app(neq, app(s, x0)), 0)
app(app(neq, app(s, x0)), app(s, x1))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(filtersub, true), x0), app(app(cons, x1), x2))
app(app(app(filtersub, false), x0), app(app(cons, x1), x2))
nonzero
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
APP(app(app(filtersub, true), f), app(app(cons, y), ys)) → APP(app(filter, f), ys)
APP(app(filter, f), app(app(cons, y), ys)) → APP(f, y)
APP(app(app(filtersub, false), f), app(app(cons, y), ys)) → APP(app(filter, f), ys)
APP1 > app2
filter > app2
cons > app2
filtersub > app2
true > app2
neq > false > app2
0 > false > app2
s > app2
nil > app2
APP1: [1]
app2: multiset
filter: multiset
cons: multiset
filtersub: multiset
true: multiset
false: multiset
neq: multiset
0: multiset
s: multiset
nil: multiset
APP(app(filter, f), app(app(cons, y), ys)) → APP(app(app(filtersub, app(f, y)), f), app(app(cons, y), ys))
app(app(neq, 0), 0) → false
app(app(neq, 0), app(s, y)) → true
app(app(neq, app(s, x)), 0) → true
app(app(neq, app(s, x)), app(s, y)) → app(app(neq, x), y)
app(app(filter, f), nil) → nil
app(app(filter, f), app(app(cons, y), ys)) → app(app(app(filtersub, app(f, y)), f), app(app(cons, y), ys))
app(app(app(filtersub, true), f), app(app(cons, y), ys)) → app(app(cons, y), app(app(filter, f), ys))
app(app(app(filtersub, false), f), app(app(cons, y), ys)) → app(app(filter, f), ys)
nonzero → app(filter, app(neq, 0))
app(app(neq, 0), 0)
app(app(neq, 0), app(s, x0))
app(app(neq, app(s, x0)), 0)
app(app(neq, app(s, x0)), app(s, x1))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(filtersub, true), x0), app(app(cons, x1), x2))
app(app(app(filtersub, false), x0), app(app(cons, x1), x2))
nonzero