0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 AND
↳5 QDP
↳6 QDPOrderProof (⇔)
↳7 QDP
↳8 PisEmptyProof (⇔)
↳9 TRUE
↳10 QDP
↳11 QDPOrderProof (⇔)
↳12 QDP
↳13 PisEmptyProof (⇔)
↳14 TRUE
↳15 QDP
↳16 QDPOrderProof (⇔)
↳17 QDP
↳18 PisEmptyProof (⇔)
↳19 TRUE
↳20 QDP
↳21 QDPOrderProof (⇔)
↳22 QDP
↳23 QDPOrderProof (⇔)
↳24 QDP
↳25 PisEmptyProof (⇔)
↳26 TRUE
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
ACTIVE(c) → F(g(c))
ACTIVE(c) → G(c)
PROPER(f(X)) → F(proper(X))
PROPER(f(X)) → PROPER(X)
PROPER(g(X)) → G(proper(X))
PROPER(g(X)) → PROPER(X)
F(ok(X)) → F(X)
G(ok(X)) → G(X)
TOP(mark(X)) → TOP(proper(X))
TOP(mark(X)) → PROPER(X)
TOP(ok(X)) → TOP(active(X))
TOP(ok(X)) → ACTIVE(X)
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
G(ok(X)) → G(X)
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
G(ok(X)) → G(X)
active1 > c > ok1
proper1 > c > ok1
top > ok1
ok1: [1]
active1: multiset
c: multiset
proper1: [1]
top: []
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
F(ok(X)) → F(X)
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(ok(X)) → F(X)
active1 > c > ok1
proper1 > c > ok1
top > ok1
ok1: [1]
active1: multiset
c: multiset
proper1: [1]
top: []
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
PROPER(g(X)) → PROPER(X)
PROPER(f(X)) → PROPER(X)
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PROPER(g(X)) → PROPER(X)
PROPER(f(X)) → PROPER(X)
active1 > g1 > f1
c > ok > g1 > f1
top > proper1 > ok > g1 > f1
g1: multiset
f1: multiset
active1: multiset
c: multiset
proper1: multiset
ok: multiset
top: multiset
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
TOP(ok(X)) → TOP(active(X))
TOP(mark(X)) → TOP(proper(X))
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TOP(mark(X)) → TOP(proper(X))
TOP1 > proper1 > top1
c > f > mark1 > proper1 > top1
c > f > g > top1
TOP1: multiset
mark1: multiset
proper1: [1]
c: multiset
f: multiset
g: multiset
top1: [1]
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
TOP(ok(X)) → TOP(active(X))
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TOP(ok(X)) → TOP(active(X))
proper1 > ok > active > mark
proper1 > ok > f1 > mark
proper1 > ok > top > mark
proper1 > c > mark
proper1 > g1 > mark
ok: []
active: multiset
c: multiset
mark: multiset
f1: multiset
g1: multiset
proper1: [1]
top: []
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))