0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 AND
↳5 QDP
↳6 QDPOrderProof (⇔)
↳7 QDP
↳8 QDPOrderProof (⇔)
↳9 QDP
↳10 PisEmptyProof (⇔)
↳11 TRUE
↳12 QDP
↳13 QDPOrderProof (⇔)
↳14 QDP
↳15 QDPOrderProof (⇔)
↳16 QDP
↳17 PisEmptyProof (⇔)
↳18 TRUE
↳19 QDP
↳20 QDPOrderProof (⇔)
↳21 QDP
↳22 QDPOrderProof (⇔)
↳23 QDP
↳24 PisEmptyProof (⇔)
↳25 TRUE
active(f(f(a))) → mark(f(g(f(a))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
ACTIVE(f(f(a))) → MARK(f(g(f(a))))
ACTIVE(f(f(a))) → F(g(f(a)))
ACTIVE(f(f(a))) → G(f(a))
MARK(f(X)) → ACTIVE(f(mark(X)))
MARK(f(X)) → F(mark(X))
MARK(f(X)) → MARK(X)
MARK(a) → ACTIVE(a)
MARK(g(X)) → ACTIVE(g(X))
F(mark(X)) → F(X)
F(active(X)) → F(X)
G(mark(X)) → G(X)
G(active(X)) → G(X)
active(f(f(a))) → mark(f(g(f(a))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
G(active(X)) → G(X)
G(mark(X)) → G(X)
active(f(f(a))) → mark(f(g(f(a))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
G(active(X)) → G(X)
[G1, active1]
active1: multiset
G1: multiset
G(mark(X)) → G(X)
active(f(f(a))) → mark(f(g(f(a))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
G(mark(X)) → G(X)
mark1 > G1
mark1: multiset
G1: multiset
active(f(f(a))) → mark(f(g(f(a))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
F(active(X)) → F(X)
F(mark(X)) → F(X)
active(f(f(a))) → mark(f(g(f(a))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(active(X)) → F(X)
[F1, active1]
active1: multiset
F1: multiset
F(mark(X)) → F(X)
active(f(f(a))) → mark(f(g(f(a))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(mark(X)) → F(X)
mark1 > F1
mark1: multiset
F1: multiset
active(f(f(a))) → mark(f(g(f(a))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
MARK(f(X)) → ACTIVE(f(mark(X)))
ACTIVE(f(f(a))) → MARK(f(g(f(a))))
MARK(f(X)) → MARK(X)
MARK(g(X)) → ACTIVE(g(X))
active(f(f(a))) → mark(f(g(f(a))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MARK(g(X)) → ACTIVE(g(X))
[MARK, f, a] > [mark1, g]
MARK: multiset
a: multiset
f: multiset
g: multiset
mark1: [1]
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(active(X)) → g(X)
g(mark(X)) → g(X)
MARK(f(X)) → ACTIVE(f(mark(X)))
ACTIVE(f(f(a))) → MARK(f(g(f(a))))
MARK(f(X)) → MARK(X)
active(f(f(a))) → mark(f(g(f(a))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MARK(f(X)) → ACTIVE(f(mark(X)))
ACTIVE(f(f(a))) → MARK(f(g(f(a))))
MARK(f(X)) → MARK(X)
a > MARK1 > f1
a > g > f1
a: multiset
f1: multiset
MARK1: [1]
g: multiset
mark(f(X)) → active(f(mark(X)))
active(f(f(a))) → mark(f(g(f(a))))
mark(a) → active(a)
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(active(X)) → g(X)
g(mark(X)) → g(X)
active(f(f(a))) → mark(f(g(f(a))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)