t(N) → cs(r(q(N)), nt(ns(N)))
q(0) → 0
q(s(X)) → s(p(q(X), d(X)))
d(0) → 0
d(s(X)) → s(s(d(X)))
p(0, X) → X
p(X, 0) → X
p(s(X), s(Y)) → s(s(p(X, Y)))
f(0, X) → nil
f(s(X), cs(Y, Z)) → cs(Y, nf(X, a(Z)))
t(X) → nt(X)
s(X) → ns(X)
f(X1, X2) → nf(X1, X2)
a(nt(X)) → t(a(X))
a(ns(X)) → s(a(X))
a(nf(X1, X2)) → f(a(X1), a(X2))
a(X) → X
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
t'(N) → cs'(r'(q'(N)), nt'(ns'(N)))
q'(0') → 0'
q'(s'(X)) → s'(p'(q'(X), d'(X)))
d'(0') → 0'
d'(s'(X)) → s'(s'(d'(X)))
p'(0', X) → X
p'(X, 0') → X
p'(s'(X), s'(Y)) → s'(s'(p'(X, Y)))
f'(0', X) → nil'
f'(s'(X), cs'(Y, Z)) → cs'(Y, nf'(X, a'(Z)))
t'(X) → nt'(X)
s'(X) → ns'(X)
f'(X1, X2) → nf'(X1, X2)
a'(nt'(X)) → t'(a'(X))
a'(ns'(X)) → s'(a'(X))
a'(nf'(X1, X2)) → f'(a'(X1), a'(X2))
a'(X) → X
Infered types.
Rules:
t'(N) → cs'(r'(q'(N)), nt'(ns'(N)))
q'(0') → 0'
q'(s'(X)) → s'(p'(q'(X), d'(X)))
d'(0') → 0'
d'(s'(X)) → s'(s'(d'(X)))
p'(0', X) → X
p'(X, 0') → X
p'(s'(X), s'(Y)) → s'(s'(p'(X, Y)))
f'(0', X) → nil'
f'(s'(X), cs'(Y, Z)) → cs'(Y, nf'(X, a'(Z)))
t'(X) → nt'(X)
s'(X) → ns'(X)
f'(X1, X2) → nf'(X1, X2)
a'(nt'(X)) → t'(a'(X))
a'(ns'(X)) → s'(a'(X))
a'(nf'(X1, X2)) → f'(a'(X1), a'(X2))
a'(X) → X
Types:
t' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
cs' :: r' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
r' :: ns':nt':cs':0':nil':nf' → r'
q' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
nt' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
ns' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
0' :: ns':nt':cs':0':nil':nf'
s' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
p' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
d' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
f' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
nil' :: ns':nt':cs':0':nil':nf'
nf' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
a' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
_hole_ns':nt':cs':0':nil':nf'1 :: ns':nt':cs':0':nil':nf'
_hole_r'2 :: r'
_gen_ns':nt':cs':0':nil':nf'3 :: Nat → ns':nt':cs':0':nil':nf'
Heuristically decided to analyse the following defined symbols:
q', p', d', a'
They will be analysed ascendingly in the following order:
p' < q'
d' < q'
Rules:
t'(N) → cs'(r'(q'(N)), nt'(ns'(N)))
q'(0') → 0'
q'(s'(X)) → s'(p'(q'(X), d'(X)))
d'(0') → 0'
d'(s'(X)) → s'(s'(d'(X)))
p'(0', X) → X
p'(X, 0') → X
p'(s'(X), s'(Y)) → s'(s'(p'(X, Y)))
f'(0', X) → nil'
f'(s'(X), cs'(Y, Z)) → cs'(Y, nf'(X, a'(Z)))
t'(X) → nt'(X)
s'(X) → ns'(X)
f'(X1, X2) → nf'(X1, X2)
a'(nt'(X)) → t'(a'(X))
a'(ns'(X)) → s'(a'(X))
a'(nf'(X1, X2)) → f'(a'(X1), a'(X2))
a'(X) → X
Types:
t' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
cs' :: r' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
r' :: ns':nt':cs':0':nil':nf' → r'
q' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
nt' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
ns' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
0' :: ns':nt':cs':0':nil':nf'
s' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
p' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
d' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
f' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
nil' :: ns':nt':cs':0':nil':nf'
nf' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
a' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
_hole_ns':nt':cs':0':nil':nf'1 :: ns':nt':cs':0':nil':nf'
_hole_r'2 :: r'
_gen_ns':nt':cs':0':nil':nf'3 :: Nat → ns':nt':cs':0':nil':nf'
Generator Equations:
_gen_ns':nt':cs':0':nil':nf'3(0) ⇔ 0'
_gen_ns':nt':cs':0':nil':nf'3(+(x, 1)) ⇔ cs'(r'(0'), _gen_ns':nt':cs':0':nil':nf'3(x))
The following defined symbols remain to be analysed:
p', q', d', a'
They will be analysed ascendingly in the following order:
p' < q'
d' < q'
Could not prove a rewrite lemma for the defined symbol p'.
Rules:
t'(N) → cs'(r'(q'(N)), nt'(ns'(N)))
q'(0') → 0'
q'(s'(X)) → s'(p'(q'(X), d'(X)))
d'(0') → 0'
d'(s'(X)) → s'(s'(d'(X)))
p'(0', X) → X
p'(X, 0') → X
p'(s'(X), s'(Y)) → s'(s'(p'(X, Y)))
f'(0', X) → nil'
f'(s'(X), cs'(Y, Z)) → cs'(Y, nf'(X, a'(Z)))
t'(X) → nt'(X)
s'(X) → ns'(X)
f'(X1, X2) → nf'(X1, X2)
a'(nt'(X)) → t'(a'(X))
a'(ns'(X)) → s'(a'(X))
a'(nf'(X1, X2)) → f'(a'(X1), a'(X2))
a'(X) → X
Types:
t' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
cs' :: r' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
r' :: ns':nt':cs':0':nil':nf' → r'
q' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
nt' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
ns' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
0' :: ns':nt':cs':0':nil':nf'
s' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
p' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
d' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
f' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
nil' :: ns':nt':cs':0':nil':nf'
nf' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
a' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
_hole_ns':nt':cs':0':nil':nf'1 :: ns':nt':cs':0':nil':nf'
_hole_r'2 :: r'
_gen_ns':nt':cs':0':nil':nf'3 :: Nat → ns':nt':cs':0':nil':nf'
Generator Equations:
_gen_ns':nt':cs':0':nil':nf'3(0) ⇔ 0'
_gen_ns':nt':cs':0':nil':nf'3(+(x, 1)) ⇔ cs'(r'(0'), _gen_ns':nt':cs':0':nil':nf'3(x))
The following defined symbols remain to be analysed:
d', q', a'
They will be analysed ascendingly in the following order:
d' < q'
Could not prove a rewrite lemma for the defined symbol d'.
Rules:
t'(N) → cs'(r'(q'(N)), nt'(ns'(N)))
q'(0') → 0'
q'(s'(X)) → s'(p'(q'(X), d'(X)))
d'(0') → 0'
d'(s'(X)) → s'(s'(d'(X)))
p'(0', X) → X
p'(X, 0') → X
p'(s'(X), s'(Y)) → s'(s'(p'(X, Y)))
f'(0', X) → nil'
f'(s'(X), cs'(Y, Z)) → cs'(Y, nf'(X, a'(Z)))
t'(X) → nt'(X)
s'(X) → ns'(X)
f'(X1, X2) → nf'(X1, X2)
a'(nt'(X)) → t'(a'(X))
a'(ns'(X)) → s'(a'(X))
a'(nf'(X1, X2)) → f'(a'(X1), a'(X2))
a'(X) → X
Types:
t' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
cs' :: r' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
r' :: ns':nt':cs':0':nil':nf' → r'
q' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
nt' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
ns' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
0' :: ns':nt':cs':0':nil':nf'
s' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
p' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
d' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
f' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
nil' :: ns':nt':cs':0':nil':nf'
nf' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
a' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
_hole_ns':nt':cs':0':nil':nf'1 :: ns':nt':cs':0':nil':nf'
_hole_r'2 :: r'
_gen_ns':nt':cs':0':nil':nf'3 :: Nat → ns':nt':cs':0':nil':nf'
Generator Equations:
_gen_ns':nt':cs':0':nil':nf'3(0) ⇔ 0'
_gen_ns':nt':cs':0':nil':nf'3(+(x, 1)) ⇔ cs'(r'(0'), _gen_ns':nt':cs':0':nil':nf'3(x))
The following defined symbols remain to be analysed:
q', a'
Could not prove a rewrite lemma for the defined symbol q'.
Rules:
t'(N) → cs'(r'(q'(N)), nt'(ns'(N)))
q'(0') → 0'
q'(s'(X)) → s'(p'(q'(X), d'(X)))
d'(0') → 0'
d'(s'(X)) → s'(s'(d'(X)))
p'(0', X) → X
p'(X, 0') → X
p'(s'(X), s'(Y)) → s'(s'(p'(X, Y)))
f'(0', X) → nil'
f'(s'(X), cs'(Y, Z)) → cs'(Y, nf'(X, a'(Z)))
t'(X) → nt'(X)
s'(X) → ns'(X)
f'(X1, X2) → nf'(X1, X2)
a'(nt'(X)) → t'(a'(X))
a'(ns'(X)) → s'(a'(X))
a'(nf'(X1, X2)) → f'(a'(X1), a'(X2))
a'(X) → X
Types:
t' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
cs' :: r' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
r' :: ns':nt':cs':0':nil':nf' → r'
q' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
nt' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
ns' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
0' :: ns':nt':cs':0':nil':nf'
s' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
p' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
d' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
f' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
nil' :: ns':nt':cs':0':nil':nf'
nf' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
a' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
_hole_ns':nt':cs':0':nil':nf'1 :: ns':nt':cs':0':nil':nf'
_hole_r'2 :: r'
_gen_ns':nt':cs':0':nil':nf'3 :: Nat → ns':nt':cs':0':nil':nf'
Generator Equations:
_gen_ns':nt':cs':0':nil':nf'3(0) ⇔ 0'
_gen_ns':nt':cs':0':nil':nf'3(+(x, 1)) ⇔ cs'(r'(0'), _gen_ns':nt':cs':0':nil':nf'3(x))
The following defined symbols remain to be analysed:
a'
Could not prove a rewrite lemma for the defined symbol a'.
Rules:
t'(N) → cs'(r'(q'(N)), nt'(ns'(N)))
q'(0') → 0'
q'(s'(X)) → s'(p'(q'(X), d'(X)))
d'(0') → 0'
d'(s'(X)) → s'(s'(d'(X)))
p'(0', X) → X
p'(X, 0') → X
p'(s'(X), s'(Y)) → s'(s'(p'(X, Y)))
f'(0', X) → nil'
f'(s'(X), cs'(Y, Z)) → cs'(Y, nf'(X, a'(Z)))
t'(X) → nt'(X)
s'(X) → ns'(X)
f'(X1, X2) → nf'(X1, X2)
a'(nt'(X)) → t'(a'(X))
a'(ns'(X)) → s'(a'(X))
a'(nf'(X1, X2)) → f'(a'(X1), a'(X2))
a'(X) → X
Types:
t' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
cs' :: r' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
r' :: ns':nt':cs':0':nil':nf' → r'
q' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
nt' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
ns' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
0' :: ns':nt':cs':0':nil':nf'
s' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
p' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
d' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
f' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
nil' :: ns':nt':cs':0':nil':nf'
nf' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
a' :: ns':nt':cs':0':nil':nf' → ns':nt':cs':0':nil':nf'
_hole_ns':nt':cs':0':nil':nf'1 :: ns':nt':cs':0':nil':nf'
_hole_r'2 :: r'
_gen_ns':nt':cs':0':nil':nf'3 :: Nat → ns':nt':cs':0':nil':nf'
Generator Equations:
_gen_ns':nt':cs':0':nil':nf'3(0) ⇔ 0'
_gen_ns':nt':cs':0':nil':nf'3(+(x, 1)) ⇔ cs'(r'(0'), _gen_ns':nt':cs':0':nil':nf'3(x))
No more defined symbols left to analyse.