0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 QDP
↳5 QDPOrderProof (⇔)
↳6 QDP
↳7 QDPOrderProof (⇔)
↳8 QDP
↳9 PisEmptyProof (⇔)
↳10 TRUE
f(X) → g(n__h(n__f(X)))
h(X) → n__h(X)
f(X) → n__f(X)
activate(n__h(X)) → h(activate(X))
activate(n__f(X)) → f(activate(X))
activate(X) → X
ACTIVATE(n__h(X)) → H(activate(X))
ACTIVATE(n__h(X)) → ACTIVATE(X)
ACTIVATE(n__f(X)) → F(activate(X))
ACTIVATE(n__f(X)) → ACTIVATE(X)
f(X) → g(n__h(n__f(X)))
h(X) → n__h(X)
f(X) → n__f(X)
activate(n__h(X)) → h(activate(X))
activate(n__f(X)) → f(activate(X))
activate(X) → X
ACTIVATE(n__f(X)) → ACTIVATE(X)
ACTIVATE(n__h(X)) → ACTIVATE(X)
f(X) → g(n__h(n__f(X)))
h(X) → n__h(X)
f(X) → n__f(X)
activate(n__h(X)) → h(activate(X))
activate(n__f(X)) → f(activate(X))
activate(X) → X
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACTIVATE(n__h(X)) → ACTIVATE(X)
[ACTIVATE1, nh1, h1] > g
ACTIVATE1: multiset
nh1: [1]
g: multiset
h1: [1]
f(X) → g(n__h(n__f(X)))
h(X) → n__h(X)
f(X) → n__f(X)
activate(n__h(X)) → h(activate(X))
activate(n__f(X)) → f(activate(X))
activate(X) → X
ACTIVATE(n__f(X)) → ACTIVATE(X)
f(X) → g(n__h(n__f(X)))
h(X) → n__h(X)
f(X) → n__f(X)
activate(n__h(X)) → h(activate(X))
activate(n__f(X)) → f(activate(X))
activate(X) → X
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACTIVATE(n__f(X)) → ACTIVATE(X)
[ACTIVATE1, nf1, f1, g]
ACTIVATE1: multiset
nf1: multiset
f1: multiset
g: multiset
f(X) → g(n__h(n__f(X)))
h(X) → n__h(X)
f(X) → n__f(X)
activate(n__h(X)) → h(activate(X))
activate(n__f(X)) → f(activate(X))
activate(X) → X
f(X) → g(n__h(n__f(X)))
h(X) → n__h(X)
f(X) → n__f(X)
activate(n__h(X)) → h(activate(X))
activate(n__f(X)) → f(activate(X))
activate(X) → X