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 QDPOrderProof (⇔)
↳14 QDP
↳15 PisEmptyProof (⇔)
↳16 TRUE
f(0) → cons(0, n__f(n__s(n__0)))
f(s(0)) → f(p(s(0)))
p(s(0)) → 0
f(X) → n__f(X)
s(X) → n__s(X)
0 → n__0
activate(n__f(X)) → f(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0
activate(X) → X
F(s(0)) → F(p(s(0)))
F(s(0)) → P(s(0))
ACTIVATE(n__f(X)) → F(activate(X))
ACTIVATE(n__f(X)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → S(activate(X))
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__0) → 01
f(0) → cons(0, n__f(n__s(n__0)))
f(s(0)) → f(p(s(0)))
p(s(0)) → 0
f(X) → n__f(X)
s(X) → n__s(X)
0 → n__0
activate(n__f(X)) → f(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0
activate(X) → X
F(s(0)) → F(p(s(0)))
f(0) → cons(0, n__f(n__s(n__0)))
f(s(0)) → f(p(s(0)))
p(s(0)) → 0
f(X) → n__f(X)
s(X) → n__s(X)
0 → n__0
activate(n__f(X)) → f(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0
activate(X) → X
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(s(0)) → F(p(s(0)))
[f1, cons1, nf1] > [0, p, n0] > [s1, ns1]
cons1: [1]
f1: [1]
p: []
n0: []
nf1: [1]
s1: [1]
ns1: [1]
0: []
f(0) → cons(0, n__f(n__s(n__0)))
f(s(0)) → f(p(s(0)))
p(s(0)) → 0
f(X) → n__f(X)
s(X) → n__s(X)
0 → n__0
activate(n__f(X)) → f(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0
activate(X) → X
f(0) → cons(0, n__f(n__s(n__0)))
f(s(0)) → f(p(s(0)))
p(s(0)) → 0
f(X) → n__f(X)
s(X) → n__s(X)
0 → n__0
activate(n__f(X)) → f(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0
activate(X) → X
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__f(X)) → ACTIVATE(X)
f(0) → cons(0, n__f(n__s(n__0)))
f(s(0)) → f(p(s(0)))
p(s(0)) → 0
f(X) → n__f(X)
s(X) → n__s(X)
0 → n__0
activate(n__f(X)) → f(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0
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)
[nf1, f1, activate1] > [0, p] > n0
f1: [1]
p: []
n0: []
nf1: [1]
activate1: [1]
0: []
f(0) → cons(0, n__f(n__s(n__0)))
f(s(0)) → f(p(s(0)))
p(s(0)) → 0
f(X) → n__f(X)
s(X) → n__s(X)
0 → n__0
activate(n__f(X)) → f(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0
activate(X) → X
ACTIVATE(n__s(X)) → ACTIVATE(X)
f(0) → cons(0, n__f(n__s(n__0)))
f(s(0)) → f(p(s(0)))
p(s(0)) → 0
f(X) → n__f(X)
s(X) → n__s(X)
0 → n__0
activate(n__f(X)) → f(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0
activate(X) → X
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACTIVATE(n__s(X)) → ACTIVATE(X)
activate1 > [f, p1] > [ns1, 0, nf, s1] > cons2
activate1 > [f, p1] > [ns1, 0, nf, s1] > n0
cons2: [2,1]
f: []
nf: []
n0: []
s1: [1]
p1: [1]
activate1: [1]
ns1: [1]
0: []
f(0) → cons(0, n__f(n__s(n__0)))
f(s(0)) → f(p(s(0)))
p(s(0)) → 0
f(X) → n__f(X)
s(X) → n__s(X)
0 → n__0
activate(n__f(X)) → f(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0
activate(X) → X
f(0) → cons(0, n__f(n__s(n__0)))
f(s(0)) → f(p(s(0)))
p(s(0)) → 0
f(X) → n__f(X)
s(X) → n__s(X)
0 → n__0
activate(n__f(X)) → f(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0
activate(X) → X