YES
0 QTRS
↳1 QTRS Reverse (⇔, 0 ms)
↳2 QTRS
↳3 QTRSRRRProof (⇔, 38 ms)
↳4 QTRS
↳5 DependencyPairsProof (⇔, 0 ms)
↳6 QDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 QDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 QDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 QDP
↳17 QDPSizeChangeProof (⇔, 0 ms)
↳18 YES
↳19 QDP
↳20 QDPOrderProof (⇔, 18 ms)
↳21 QDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 QDP
↳24 MRRProof (⇔, 10 ms)
↳25 QDP
↳26 PisEmptyProof (⇔, 0 ms)
↳27 YES
f(f(X)) → c(n__f(n__g(n__f(X))))
c(X) → d(activate(X))
h(X) → c(n__d(X))
f(X) → n__f(X)
g(X) → n__g(X)
d(X) → n__d(X)
activate(n__f(X)) → f(activate(X))
activate(n__g(X)) → g(X)
activate(n__d(X)) → d(X)
activate(X) → X
f(f(X)) → n__f(n__g(n__f(c(X))))
c(X) → activate(d(X))
h(X) → n__d(c(X))
f(X) → n__f(X)
g(X) → n__g(X)
d(X) → n__d(X)
n__f(activate(X)) → activate(f(X))
n__g(activate(X)) → g(X)
n__d(activate(X)) → d(X)
activate(X) → X
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(activate(x1)) = x1
POL(c(x1)) = x1
POL(d(x1)) = x1
POL(f(x1)) = x1
POL(g(x1)) = x1
POL(h(x1)) = 1 + x1
POL(n__d(x1)) = x1
POL(n__f(x1)) = x1
POL(n__g(x1)) = x1
h(X) → n__d(c(X))
f(f(X)) → n__f(n__g(n__f(c(X))))
c(X) → activate(d(X))
f(X) → n__f(X)
g(X) → n__g(X)
d(X) → n__d(X)
n__f(activate(X)) → activate(f(X))
n__g(activate(X)) → g(X)
n__d(activate(X)) → d(X)
activate(X) → X
F(f(X)) → N__F(n__g(n__f(c(X))))
F(f(X)) → N__G(n__f(c(X)))
F(f(X)) → N__F(c(X))
F(f(X)) → C(X)
C(X) → ACTIVATE(d(X))
C(X) → D(X)
F(X) → N__F(X)
G(X) → N__G(X)
D(X) → N__D(X)
N__F(activate(X)) → ACTIVATE(f(X))
N__F(activate(X)) → F(X)
N__G(activate(X)) → G(X)
N__D(activate(X)) → D(X)
f(f(X)) → n__f(n__g(n__f(c(X))))
c(X) → activate(d(X))
f(X) → n__f(X)
g(X) → n__g(X)
d(X) → n__d(X)
n__f(activate(X)) → activate(f(X))
n__g(activate(X)) → g(X)
n__d(activate(X)) → d(X)
activate(X) → X
N__D(activate(X)) → D(X)
D(X) → N__D(X)
f(f(X)) → n__f(n__g(n__f(c(X))))
c(X) → activate(d(X))
f(X) → n__f(X)
g(X) → n__g(X)
d(X) → n__d(X)
n__f(activate(X)) → activate(f(X))
n__g(activate(X)) → g(X)
n__d(activate(X)) → d(X)
activate(X) → X
N__D(activate(X)) → D(X)
D(X) → N__D(X)
From the DPs we obtained the following set of size-change graphs:
N__G(activate(X)) → G(X)
G(X) → N__G(X)
f(f(X)) → n__f(n__g(n__f(c(X))))
c(X) → activate(d(X))
f(X) → n__f(X)
g(X) → n__g(X)
d(X) → n__d(X)
n__f(activate(X)) → activate(f(X))
n__g(activate(X)) → g(X)
n__d(activate(X)) → d(X)
activate(X) → X
N__G(activate(X)) → G(X)
G(X) → N__G(X)
From the DPs we obtained the following set of size-change graphs:
N__F(activate(X)) → F(X)
F(f(X)) → N__F(n__g(n__f(c(X))))
F(f(X)) → N__F(c(X))
F(X) → N__F(X)
f(f(X)) → n__f(n__g(n__f(c(X))))
c(X) → activate(d(X))
f(X) → n__f(X)
g(X) → n__g(X)
d(X) → n__d(X)
n__f(activate(X)) → activate(f(X))
n__g(activate(X)) → g(X)
n__d(activate(X)) → d(X)
activate(X) → X
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(f(X)) → N__F(n__g(n__f(c(X))))
POL(F(x1)) = 1 + x1
POL(N__F(x1)) = 1 + x1
POL(activate(x1)) = x1
POL(c(x1)) = 1
POL(d(x1)) = 0
POL(f(x1)) = 1
POL(g(x1)) = 0
POL(n__d(x1)) = 0
POL(n__f(x1)) = 1
POL(n__g(x1)) = 0
c(X) → activate(d(X))
n__g(activate(X)) → g(X)
g(X) → n__g(X)
activate(X) → X
n__d(activate(X)) → d(X)
d(X) → n__d(X)
N__F(activate(X)) → F(X)
F(f(X)) → N__F(c(X))
F(X) → N__F(X)
f(f(X)) → n__f(n__g(n__f(c(X))))
c(X) → activate(d(X))
f(X) → n__f(X)
g(X) → n__g(X)
d(X) → n__d(X)
n__f(activate(X)) → activate(f(X))
n__g(activate(X)) → g(X)
n__d(activate(X)) → d(X)
activate(X) → X
N__F(activate(X)) → F(X)
F(f(X)) → N__F(c(X))
F(X) → N__F(X)
c(X) → activate(d(X))
activate(X) → X
n__d(activate(X)) → d(X)
d(X) → n__d(X)
N__F(activate(X)) → F(X)
F(f(X)) → N__F(c(X))
F(X) → N__F(X)
activate(X) → X
n__d(activate(X)) → d(X)
POL(F(x1)) = 2 + 3·x1
POL(N__F(x1)) = 1 + 3·x1
POL(activate(x1)) = 1 + x1
POL(c(x1)) = 1 + 3·x1
POL(d(x1)) = 2·x1
POL(f(x1)) = 3 + 3·x1
POL(n__d(x1)) = 2·x1
c(X) → activate(d(X))
d(X) → n__d(X)