Runtime Complexity (innermost) proof of /tmp/tmp36t_La/ExProp7_Luc06

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

0 CpxTRS

↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)

↳2 CdtProblem

    ↳3 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳4 CdtProblem

    ↳5 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳6 CdtProblem

    ↳7 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳8 CdtProblem

    ↳9 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳10 CdtProblem

    ↳11 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 6 ms)

    ↳12 CdtProblem

    ↳13 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳14 CdtProblem

    ↳15 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳16 CdtProblem

    ↳17 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳18 CdtProblem

    ↳19 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳20 CdtProblem

    ↳21 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳22 CdtProblem

    ↳23 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳24 CdtProblem

    ↳25 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳26 CdtProblem

    ↳27 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳28 CdtProblem

    ↳29 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳30 CdtProblem

    ↳31 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳32 CdtProblem

    ↳33 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳34 CdtProblem

    ↳35 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳36 CdtProblem

    ↳37 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳38 CdtProblem

    ↳39 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳40 CdtProblem

↳41 CpxTrsMatchBoundsTAProof (⇔, 129 ms)

↳42 BOUNDS(O(1), O(n^1))

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

active(f(0)) → mark(cons(0, f(s(0))))
active(f(s(0))) → mark(f(p(s(0))))
active(p(s(X))) → mark(X)
active(f(X)) → f(active(X))
active(cons(X1, X2)) → cons(active(X1), X2)
active(s(X)) → s(active(X))
active(p(X)) → p(active(X))
f(mark(X)) → mark(f(X))
cons(mark(X1), X2) → mark(cons(X1, X2))
s(mark(X)) → mark(s(X))
p(mark(X)) → mark(p(X))
proper(f(X)) → f(proper(X))
proper(0) → ok(0)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(s(X)) → s(proper(X))
proper(p(X)) → p(proper(X))
f(ok(X)) → ok(f(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
s(ok(X)) → ok(s(X))
p(ok(X)) → ok(p(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(0)) → mark(cons(0, f(s(0))))
active(f(s(0))) → mark(f(p(s(0))))
active(p(s(z0))) → mark(z0)
active(f(z0)) → f(active(z0))
active(cons(z0, z1)) → cons(active(z0), z1)
active(s(z0)) → s(active(z0))
active(p(z0)) → p(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
cons(mark(z0), z1) → mark(cons(z0, z1))
cons(ok(z0), ok(z1)) → ok(cons(z0, z1))
s(mark(z0)) → mark(s(z0))
s(ok(z0)) → ok(s(z0))
p(mark(z0)) → mark(p(z0))
p(ok(z0)) → ok(p(z0))
proper(f(z0)) → f(proper(z0))
proper(0) → ok(0)
proper(cons(z0, z1)) → cons(proper(z0), proper(z1))
proper(s(z0)) → s(proper(z0))
proper(p(z0)) → p(proper(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(f(0)) → c(CONS(0, f(s(0))), F(s(0)), S(0))
ACTIVE(f(s(0))) → c1(F(p(s(0))), P(s(0)), S(0))
ACTIVE(f(z0)) → c3(F(active(z0)), ACTIVE(z0))
ACTIVE(cons(z0, z1)) → c4(CONS(active(z0), z1), ACTIVE(z0))
ACTIVE(s(z0)) → c5(S(active(z0)), ACTIVE(z0))
ACTIVE(p(z0)) → c6(P(active(z0)), ACTIVE(z0))
F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(f(z0)) → c15(F(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))

S tuples:

ACTIVE(f(0)) → c(CONS(0, f(s(0))), F(s(0)), S(0))
ACTIVE(f(s(0))) → c1(F(p(s(0))), P(s(0)), S(0))
ACTIVE(f(z0)) → c3(F(active(z0)), ACTIVE(z0))
ACTIVE(cons(z0, z1)) → c4(CONS(active(z0), z1), ACTIVE(z0))
ACTIVE(s(z0)) → c5(S(active(z0)), ACTIVE(z0))
ACTIVE(p(z0)) → c6(P(active(z0)), ACTIVE(z0))
F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(f(z0)) → c15(F(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))

K tuples:none
Defined Rule Symbols:

active, f, cons, s, p, proper, top

Defined Pair Symbols:

ACTIVE, F, CONS, S, P, PROPER, TOP

Compound Symbols:

c, c1, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c17, c18, c19, c20, c21

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing nodes:

ACTIVE(f(s(0))) → c1(F(p(s(0))), P(s(0)), S(0))
ACTIVE(f(0)) → c(CONS(0, f(s(0))), F(s(0)), S(0))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(0)) → mark(cons(0, f(s(0))))
active(f(s(0))) → mark(f(p(s(0))))
active(p(s(z0))) → mark(z0)
active(f(z0)) → f(active(z0))
active(cons(z0, z1)) → cons(active(z0), z1)
active(s(z0)) → s(active(z0))
active(p(z0)) → p(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
cons(mark(z0), z1) → mark(cons(z0, z1))
cons(ok(z0), ok(z1)) → ok(cons(z0, z1))
s(mark(z0)) → mark(s(z0))
s(ok(z0)) → ok(s(z0))
p(mark(z0)) → mark(p(z0))
p(ok(z0)) → ok(p(z0))
proper(f(z0)) → f(proper(z0))
proper(0) → ok(0)
proper(cons(z0, z1)) → cons(proper(z0), proper(z1))
proper(s(z0)) → s(proper(z0))
proper(p(z0)) → p(proper(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(f(z0)) → c3(F(active(z0)), ACTIVE(z0))
ACTIVE(cons(z0, z1)) → c4(CONS(active(z0), z1), ACTIVE(z0))
ACTIVE(s(z0)) → c5(S(active(z0)), ACTIVE(z0))
ACTIVE(p(z0)) → c6(P(active(z0)), ACTIVE(z0))
F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(f(z0)) → c15(F(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))

S tuples:

ACTIVE(f(z0)) → c3(F(active(z0)), ACTIVE(z0))
ACTIVE(cons(z0, z1)) → c4(CONS(active(z0), z1), ACTIVE(z0))
ACTIVE(s(z0)) → c5(S(active(z0)), ACTIVE(z0))
ACTIVE(p(z0)) → c6(P(active(z0)), ACTIVE(z0))
F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(f(z0)) → c15(F(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))

K tuples:none
Defined Rule Symbols:

active, f, cons, s, p, proper, top

Defined Pair Symbols:

ACTIVE, F, CONS, S, P, PROPER, TOP

Compound Symbols:

c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c17, c18, c19, c20, c21

(5) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace ACTIVE(f(z0)) → c3(F(active(z0)), ACTIVE(z0)) by

ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))), ACTIVE(f(0)))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(x0)) → c3

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(0)) → mark(cons(0, f(s(0))))
active(f(s(0))) → mark(f(p(s(0))))
active(p(s(z0))) → mark(z0)
active(f(z0)) → f(active(z0))
active(cons(z0, z1)) → cons(active(z0), z1)
active(s(z0)) → s(active(z0))
active(p(z0)) → p(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
cons(mark(z0), z1) → mark(cons(z0, z1))
cons(ok(z0), ok(z1)) → ok(cons(z0, z1))
s(mark(z0)) → mark(s(z0))
s(ok(z0)) → ok(s(z0))
p(mark(z0)) → mark(p(z0))
p(ok(z0)) → ok(p(z0))
proper(f(z0)) → f(proper(z0))
proper(0) → ok(0)
proper(cons(z0, z1)) → cons(proper(z0), proper(z1))
proper(s(z0)) → s(proper(z0))
proper(p(z0)) → p(proper(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(cons(z0, z1)) → c4(CONS(active(z0), z1), ACTIVE(z0))
ACTIVE(s(z0)) → c5(S(active(z0)), ACTIVE(z0))
ACTIVE(p(z0)) → c6(P(active(z0)), ACTIVE(z0))
F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(f(z0)) → c15(F(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))), ACTIVE(f(0)))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(x0)) → c3

S tuples:

ACTIVE(cons(z0, z1)) → c4(CONS(active(z0), z1), ACTIVE(z0))
ACTIVE(s(z0)) → c5(S(active(z0)), ACTIVE(z0))
ACTIVE(p(z0)) → c6(P(active(z0)), ACTIVE(z0))
F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(f(z0)) → c15(F(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))), ACTIVE(f(0)))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(x0)) → c3

K tuples:none
Defined Rule Symbols:

active, f, cons, s, p, proper, top

Defined Pair Symbols:

ACTIVE, F, CONS, S, P, PROPER, TOP

Compound Symbols:

c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c17, c18, c19, c20, c21, c3, c3

(7) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

ACTIVE(f(x0)) → c3

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(0)) → mark(cons(0, f(s(0))))
active(f(s(0))) → mark(f(p(s(0))))
active(p(s(z0))) → mark(z0)
active(f(z0)) → f(active(z0))
active(cons(z0, z1)) → cons(active(z0), z1)
active(s(z0)) → s(active(z0))
active(p(z0)) → p(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
cons(mark(z0), z1) → mark(cons(z0, z1))
cons(ok(z0), ok(z1)) → ok(cons(z0, z1))
s(mark(z0)) → mark(s(z0))
s(ok(z0)) → ok(s(z0))
p(mark(z0)) → mark(p(z0))
p(ok(z0)) → ok(p(z0))
proper(f(z0)) → f(proper(z0))
proper(0) → ok(0)
proper(cons(z0, z1)) → cons(proper(z0), proper(z1))
proper(s(z0)) → s(proper(z0))
proper(p(z0)) → p(proper(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(cons(z0, z1)) → c4(CONS(active(z0), z1), ACTIVE(z0))
ACTIVE(s(z0)) → c5(S(active(z0)), ACTIVE(z0))
ACTIVE(p(z0)) → c6(P(active(z0)), ACTIVE(z0))
F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(f(z0)) → c15(F(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))), ACTIVE(f(0)))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))

S tuples:

ACTIVE(cons(z0, z1)) → c4(CONS(active(z0), z1), ACTIVE(z0))
ACTIVE(s(z0)) → c5(S(active(z0)), ACTIVE(z0))
ACTIVE(p(z0)) → c6(P(active(z0)), ACTIVE(z0))
F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(f(z0)) → c15(F(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))), ACTIVE(f(0)))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))

K tuples:none
Defined Rule Symbols:

active, f, cons, s, p, proper, top

Defined Pair Symbols:

ACTIVE, F, CONS, S, P, PROPER, TOP

Compound Symbols:

c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c17, c18, c19, c20, c21, c3

(9) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(0)) → mark(cons(0, f(s(0))))
active(f(s(0))) → mark(f(p(s(0))))
active(p(s(z0))) → mark(z0)
active(f(z0)) → f(active(z0))
active(cons(z0, z1)) → cons(active(z0), z1)
active(s(z0)) → s(active(z0))
active(p(z0)) → p(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
cons(mark(z0), z1) → mark(cons(z0, z1))
cons(ok(z0), ok(z1)) → ok(cons(z0, z1))
s(mark(z0)) → mark(s(z0))
s(ok(z0)) → ok(s(z0))
p(mark(z0)) → mark(p(z0))
p(ok(z0)) → ok(p(z0))
proper(f(z0)) → f(proper(z0))
proper(0) → ok(0)
proper(cons(z0, z1)) → cons(proper(z0), proper(z1))
proper(s(z0)) → s(proper(z0))
proper(p(z0)) → p(proper(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(cons(z0, z1)) → c4(CONS(active(z0), z1), ACTIVE(z0))
ACTIVE(s(z0)) → c5(S(active(z0)), ACTIVE(z0))
ACTIVE(p(z0)) → c6(P(active(z0)), ACTIVE(z0))
F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(f(z0)) → c15(F(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))))

S tuples:

ACTIVE(cons(z0, z1)) → c4(CONS(active(z0), z1), ACTIVE(z0))
ACTIVE(s(z0)) → c5(S(active(z0)), ACTIVE(z0))
ACTIVE(p(z0)) → c6(P(active(z0)), ACTIVE(z0))
F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(f(z0)) → c15(F(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))))

K tuples:none
Defined Rule Symbols:

active, f, cons, s, p, proper, top

Defined Pair Symbols:

ACTIVE, F, CONS, S, P, PROPER, TOP

Compound Symbols:

c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c17, c18, c19, c20, c21, c3, c3

(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace ACTIVE(cons(z0, z1)) → c4(CONS(active(z0), z1), ACTIVE(z0)) by

ACTIVE(cons(f(0), x1)) → c4(CONS(mark(cons(0, f(s(0)))), x1), ACTIVE(f(0)))
ACTIVE(cons(f(s(0)), x1)) → c4(CONS(mark(f(p(s(0)))), x1), ACTIVE(f(s(0))))
ACTIVE(cons(p(s(z0)), x1)) → c4(CONS(mark(z0), x1), ACTIVE(p(s(z0))))
ACTIVE(cons(f(z0), x1)) → c4(CONS(f(active(z0)), x1), ACTIVE(f(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c4(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c4(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(p(z0), x1)) → c4(CONS(p(active(z0)), x1), ACTIVE(p(z0)))
ACTIVE(cons(x0, x1)) → c4

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(0)) → mark(cons(0, f(s(0))))
active(f(s(0))) → mark(f(p(s(0))))
active(p(s(z0))) → mark(z0)
active(f(z0)) → f(active(z0))
active(cons(z0, z1)) → cons(active(z0), z1)
active(s(z0)) → s(active(z0))
active(p(z0)) → p(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
cons(mark(z0), z1) → mark(cons(z0, z1))
cons(ok(z0), ok(z1)) → ok(cons(z0, z1))
s(mark(z0)) → mark(s(z0))
s(ok(z0)) → ok(s(z0))
p(mark(z0)) → mark(p(z0))
p(ok(z0)) → ok(p(z0))
proper(f(z0)) → f(proper(z0))
proper(0) → ok(0)
proper(cons(z0, z1)) → cons(proper(z0), proper(z1))
proper(s(z0)) → s(proper(z0))
proper(p(z0)) → p(proper(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(s(z0)) → c5(S(active(z0)), ACTIVE(z0))
ACTIVE(p(z0)) → c6(P(active(z0)), ACTIVE(z0))
F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(f(z0)) → c15(F(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))))
ACTIVE(cons(f(0), x1)) → c4(CONS(mark(cons(0, f(s(0)))), x1), ACTIVE(f(0)))
ACTIVE(cons(f(s(0)), x1)) → c4(CONS(mark(f(p(s(0)))), x1), ACTIVE(f(s(0))))
ACTIVE(cons(p(s(z0)), x1)) → c4(CONS(mark(z0), x1), ACTIVE(p(s(z0))))
ACTIVE(cons(f(z0), x1)) → c4(CONS(f(active(z0)), x1), ACTIVE(f(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c4(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c4(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(p(z0), x1)) → c4(CONS(p(active(z0)), x1), ACTIVE(p(z0)))
ACTIVE(cons(x0, x1)) → c4

S tuples:

ACTIVE(s(z0)) → c5(S(active(z0)), ACTIVE(z0))
ACTIVE(p(z0)) → c6(P(active(z0)), ACTIVE(z0))
F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(f(z0)) → c15(F(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))))
ACTIVE(cons(f(0), x1)) → c4(CONS(mark(cons(0, f(s(0)))), x1), ACTIVE(f(0)))
ACTIVE(cons(f(s(0)), x1)) → c4(CONS(mark(f(p(s(0)))), x1), ACTIVE(f(s(0))))
ACTIVE(cons(p(s(z0)), x1)) → c4(CONS(mark(z0), x1), ACTIVE(p(s(z0))))
ACTIVE(cons(f(z0), x1)) → c4(CONS(f(active(z0)), x1), ACTIVE(f(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c4(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c4(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(p(z0), x1)) → c4(CONS(p(active(z0)), x1), ACTIVE(p(z0)))
ACTIVE(cons(x0, x1)) → c4

K tuples:none
Defined Rule Symbols:

active, f, cons, s, p, proper, top

Defined Pair Symbols:

ACTIVE, F, CONS, S, P, PROPER, TOP

Compound Symbols:

c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c17, c18, c19, c20, c21, c3, c3, c4, c4

(13) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

ACTIVE(cons(x0, x1)) → c4

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(0)) → mark(cons(0, f(s(0))))
active(f(s(0))) → mark(f(p(s(0))))
active(p(s(z0))) → mark(z0)
active(f(z0)) → f(active(z0))
active(cons(z0, z1)) → cons(active(z0), z1)
active(s(z0)) → s(active(z0))
active(p(z0)) → p(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
cons(mark(z0), z1) → mark(cons(z0, z1))
cons(ok(z0), ok(z1)) → ok(cons(z0, z1))
s(mark(z0)) → mark(s(z0))
s(ok(z0)) → ok(s(z0))
p(mark(z0)) → mark(p(z0))
p(ok(z0)) → ok(p(z0))
proper(f(z0)) → f(proper(z0))
proper(0) → ok(0)
proper(cons(z0, z1)) → cons(proper(z0), proper(z1))
proper(s(z0)) → s(proper(z0))
proper(p(z0)) → p(proper(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(s(z0)) → c5(S(active(z0)), ACTIVE(z0))
ACTIVE(p(z0)) → c6(P(active(z0)), ACTIVE(z0))
F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(f(z0)) → c15(F(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))))
ACTIVE(cons(f(0), x1)) → c4(CONS(mark(cons(0, f(s(0)))), x1), ACTIVE(f(0)))
ACTIVE(cons(f(s(0)), x1)) → c4(CONS(mark(f(p(s(0)))), x1), ACTIVE(f(s(0))))
ACTIVE(cons(p(s(z0)), x1)) → c4(CONS(mark(z0), x1), ACTIVE(p(s(z0))))
ACTIVE(cons(f(z0), x1)) → c4(CONS(f(active(z0)), x1), ACTIVE(f(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c4(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c4(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(p(z0), x1)) → c4(CONS(p(active(z0)), x1), ACTIVE(p(z0)))

S tuples:

ACTIVE(s(z0)) → c5(S(active(z0)), ACTIVE(z0))
ACTIVE(p(z0)) → c6(P(active(z0)), ACTIVE(z0))
F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(f(z0)) → c15(F(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))))
ACTIVE(cons(f(0), x1)) → c4(CONS(mark(cons(0, f(s(0)))), x1), ACTIVE(f(0)))
ACTIVE(cons(f(s(0)), x1)) → c4(CONS(mark(f(p(s(0)))), x1), ACTIVE(f(s(0))))
ACTIVE(cons(p(s(z0)), x1)) → c4(CONS(mark(z0), x1), ACTIVE(p(s(z0))))
ACTIVE(cons(f(z0), x1)) → c4(CONS(f(active(z0)), x1), ACTIVE(f(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c4(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c4(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(p(z0), x1)) → c4(CONS(p(active(z0)), x1), ACTIVE(p(z0)))

K tuples:none
Defined Rule Symbols:

active, f, cons, s, p, proper, top

Defined Pair Symbols:

ACTIVE, F, CONS, S, P, PROPER, TOP

Compound Symbols:

c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c17, c18, c19, c20, c21, c3, c3, c4

(15) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(0)) → mark(cons(0, f(s(0))))
active(f(s(0))) → mark(f(p(s(0))))
active(p(s(z0))) → mark(z0)
active(f(z0)) → f(active(z0))
active(cons(z0, z1)) → cons(active(z0), z1)
active(s(z0)) → s(active(z0))
active(p(z0)) → p(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
cons(mark(z0), z1) → mark(cons(z0, z1))
cons(ok(z0), ok(z1)) → ok(cons(z0, z1))
s(mark(z0)) → mark(s(z0))
s(ok(z0)) → ok(s(z0))
p(mark(z0)) → mark(p(z0))
p(ok(z0)) → ok(p(z0))
proper(f(z0)) → f(proper(z0))
proper(0) → ok(0)
proper(cons(z0, z1)) → cons(proper(z0), proper(z1))
proper(s(z0)) → s(proper(z0))
proper(p(z0)) → p(proper(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(s(z0)) → c5(S(active(z0)), ACTIVE(z0))
ACTIVE(p(z0)) → c6(P(active(z0)), ACTIVE(z0))
F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(f(z0)) → c15(F(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))))
ACTIVE(cons(f(s(0)), x1)) → c4(CONS(mark(f(p(s(0)))), x1), ACTIVE(f(s(0))))
ACTIVE(cons(p(s(z0)), x1)) → c4(CONS(mark(z0), x1), ACTIVE(p(s(z0))))
ACTIVE(cons(f(z0), x1)) → c4(CONS(f(active(z0)), x1), ACTIVE(f(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c4(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c4(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(p(z0), x1)) → c4(CONS(p(active(z0)), x1), ACTIVE(p(z0)))
ACTIVE(cons(f(0), x1)) → c4(CONS(mark(cons(0, f(s(0)))), x1))

S tuples:

ACTIVE(s(z0)) → c5(S(active(z0)), ACTIVE(z0))
ACTIVE(p(z0)) → c6(P(active(z0)), ACTIVE(z0))
F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(f(z0)) → c15(F(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))))
ACTIVE(cons(f(s(0)), x1)) → c4(CONS(mark(f(p(s(0)))), x1), ACTIVE(f(s(0))))
ACTIVE(cons(p(s(z0)), x1)) → c4(CONS(mark(z0), x1), ACTIVE(p(s(z0))))
ACTIVE(cons(f(z0), x1)) → c4(CONS(f(active(z0)), x1), ACTIVE(f(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c4(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c4(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(p(z0), x1)) → c4(CONS(p(active(z0)), x1), ACTIVE(p(z0)))
ACTIVE(cons(f(0), x1)) → c4(CONS(mark(cons(0, f(s(0)))), x1))

K tuples:none
Defined Rule Symbols:

active, f, cons, s, p, proper, top

Defined Pair Symbols:

ACTIVE, F, CONS, S, P, PROPER, TOP

Compound Symbols:

c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c17, c18, c19, c20, c21, c3, c3, c4, c4

(17) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace ACTIVE(s(z0)) → c5(S(active(z0)), ACTIVE(z0)) by

ACTIVE(s(f(0))) → c5(S(mark(cons(0, f(s(0))))), ACTIVE(f(0)))
ACTIVE(s(f(s(0)))) → c5(S(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(s(p(s(z0)))) → c5(S(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(s(f(z0))) → c5(S(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(s(cons(z0, z1))) → c5(S(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(s(s(z0))) → c5(S(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(s(p(z0))) → c5(S(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(s(x0)) → c5

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(0)) → mark(cons(0, f(s(0))))
active(f(s(0))) → mark(f(p(s(0))))
active(p(s(z0))) → mark(z0)
active(f(z0)) → f(active(z0))
active(cons(z0, z1)) → cons(active(z0), z1)
active(s(z0)) → s(active(z0))
active(p(z0)) → p(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
cons(mark(z0), z1) → mark(cons(z0, z1))
cons(ok(z0), ok(z1)) → ok(cons(z0, z1))
s(mark(z0)) → mark(s(z0))
s(ok(z0)) → ok(s(z0))
p(mark(z0)) → mark(p(z0))
p(ok(z0)) → ok(p(z0))
proper(f(z0)) → f(proper(z0))
proper(0) → ok(0)
proper(cons(z0, z1)) → cons(proper(z0), proper(z1))
proper(s(z0)) → s(proper(z0))
proper(p(z0)) → p(proper(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(p(z0)) → c6(P(active(z0)), ACTIVE(z0))
F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(f(z0)) → c15(F(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))))
ACTIVE(cons(f(s(0)), x1)) → c4(CONS(mark(f(p(s(0)))), x1), ACTIVE(f(s(0))))
ACTIVE(cons(p(s(z0)), x1)) → c4(CONS(mark(z0), x1), ACTIVE(p(s(z0))))
ACTIVE(cons(f(z0), x1)) → c4(CONS(f(active(z0)), x1), ACTIVE(f(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c4(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c4(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(p(z0), x1)) → c4(CONS(p(active(z0)), x1), ACTIVE(p(z0)))
ACTIVE(cons(f(0), x1)) → c4(CONS(mark(cons(0, f(s(0)))), x1))
ACTIVE(s(f(0))) → c5(S(mark(cons(0, f(s(0))))), ACTIVE(f(0)))
ACTIVE(s(f(s(0)))) → c5(S(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(s(p(s(z0)))) → c5(S(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(s(f(z0))) → c5(S(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(s(cons(z0, z1))) → c5(S(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(s(s(z0))) → c5(S(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(s(p(z0))) → c5(S(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(s(x0)) → c5

S tuples:

ACTIVE(p(z0)) → c6(P(active(z0)), ACTIVE(z0))
F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(f(z0)) → c15(F(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))))
ACTIVE(cons(f(s(0)), x1)) → c4(CONS(mark(f(p(s(0)))), x1), ACTIVE(f(s(0))))
ACTIVE(cons(p(s(z0)), x1)) → c4(CONS(mark(z0), x1), ACTIVE(p(s(z0))))
ACTIVE(cons(f(z0), x1)) → c4(CONS(f(active(z0)), x1), ACTIVE(f(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c4(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c4(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(p(z0), x1)) → c4(CONS(p(active(z0)), x1), ACTIVE(p(z0)))
ACTIVE(cons(f(0), x1)) → c4(CONS(mark(cons(0, f(s(0)))), x1))
ACTIVE(s(f(0))) → c5(S(mark(cons(0, f(s(0))))), ACTIVE(f(0)))
ACTIVE(s(f(s(0)))) → c5(S(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(s(p(s(z0)))) → c5(S(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(s(f(z0))) → c5(S(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(s(cons(z0, z1))) → c5(S(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(s(s(z0))) → c5(S(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(s(p(z0))) → c5(S(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(s(x0)) → c5

K tuples:none
Defined Rule Symbols:

active, f, cons, s, p, proper, top

Defined Pair Symbols:

ACTIVE, F, CONS, S, P, PROPER, TOP

Compound Symbols:

c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c17, c18, c19, c20, c21, c3, c3, c4, c4, c5, c5

(19) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

ACTIVE(s(x0)) → c5

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(0)) → mark(cons(0, f(s(0))))
active(f(s(0))) → mark(f(p(s(0))))
active(p(s(z0))) → mark(z0)
active(f(z0)) → f(active(z0))
active(cons(z0, z1)) → cons(active(z0), z1)
active(s(z0)) → s(active(z0))
active(p(z0)) → p(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
cons(mark(z0), z1) → mark(cons(z0, z1))
cons(ok(z0), ok(z1)) → ok(cons(z0, z1))
s(mark(z0)) → mark(s(z0))
s(ok(z0)) → ok(s(z0))
p(mark(z0)) → mark(p(z0))
p(ok(z0)) → ok(p(z0))
proper(f(z0)) → f(proper(z0))
proper(0) → ok(0)
proper(cons(z0, z1)) → cons(proper(z0), proper(z1))
proper(s(z0)) → s(proper(z0))
proper(p(z0)) → p(proper(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(p(z0)) → c6(P(active(z0)), ACTIVE(z0))
F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(f(z0)) → c15(F(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))))
ACTIVE(cons(f(s(0)), x1)) → c4(CONS(mark(f(p(s(0)))), x1), ACTIVE(f(s(0))))
ACTIVE(cons(p(s(z0)), x1)) → c4(CONS(mark(z0), x1), ACTIVE(p(s(z0))))
ACTIVE(cons(f(z0), x1)) → c4(CONS(f(active(z0)), x1), ACTIVE(f(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c4(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c4(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(p(z0), x1)) → c4(CONS(p(active(z0)), x1), ACTIVE(p(z0)))
ACTIVE(cons(f(0), x1)) → c4(CONS(mark(cons(0, f(s(0)))), x1))
ACTIVE(s(f(0))) → c5(S(mark(cons(0, f(s(0))))), ACTIVE(f(0)))
ACTIVE(s(f(s(0)))) → c5(S(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(s(p(s(z0)))) → c5(S(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(s(f(z0))) → c5(S(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(s(cons(z0, z1))) → c5(S(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(s(s(z0))) → c5(S(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(s(p(z0))) → c5(S(p(active(z0))), ACTIVE(p(z0)))

S tuples:

ACTIVE(p(z0)) → c6(P(active(z0)), ACTIVE(z0))
F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(f(z0)) → c15(F(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))))
ACTIVE(cons(f(s(0)), x1)) → c4(CONS(mark(f(p(s(0)))), x1), ACTIVE(f(s(0))))
ACTIVE(cons(p(s(z0)), x1)) → c4(CONS(mark(z0), x1), ACTIVE(p(s(z0))))
ACTIVE(cons(f(z0), x1)) → c4(CONS(f(active(z0)), x1), ACTIVE(f(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c4(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c4(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(p(z0), x1)) → c4(CONS(p(active(z0)), x1), ACTIVE(p(z0)))
ACTIVE(cons(f(0), x1)) → c4(CONS(mark(cons(0, f(s(0)))), x1))
ACTIVE(s(f(0))) → c5(S(mark(cons(0, f(s(0))))), ACTIVE(f(0)))
ACTIVE(s(f(s(0)))) → c5(S(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(s(p(s(z0)))) → c5(S(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(s(f(z0))) → c5(S(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(s(cons(z0, z1))) → c5(S(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(s(s(z0))) → c5(S(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(s(p(z0))) → c5(S(p(active(z0))), ACTIVE(p(z0)))

K tuples:none
Defined Rule Symbols:

active, f, cons, s, p, proper, top

Defined Pair Symbols:

ACTIVE, F, CONS, S, P, PROPER, TOP

Compound Symbols:

c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c17, c18, c19, c20, c21, c3, c3, c4, c4, c5

(21) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(0)) → mark(cons(0, f(s(0))))
active(f(s(0))) → mark(f(p(s(0))))
active(p(s(z0))) → mark(z0)
active(f(z0)) → f(active(z0))
active(cons(z0, z1)) → cons(active(z0), z1)
active(s(z0)) → s(active(z0))
active(p(z0)) → p(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
cons(mark(z0), z1) → mark(cons(z0, z1))
cons(ok(z0), ok(z1)) → ok(cons(z0, z1))
s(mark(z0)) → mark(s(z0))
s(ok(z0)) → ok(s(z0))
p(mark(z0)) → mark(p(z0))
p(ok(z0)) → ok(p(z0))
proper(f(z0)) → f(proper(z0))
proper(0) → ok(0)
proper(cons(z0, z1)) → cons(proper(z0), proper(z1))
proper(s(z0)) → s(proper(z0))
proper(p(z0)) → p(proper(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(p(z0)) → c6(P(active(z0)), ACTIVE(z0))
F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(f(z0)) → c15(F(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))))
ACTIVE(cons(f(s(0)), x1)) → c4(CONS(mark(f(p(s(0)))), x1), ACTIVE(f(s(0))))
ACTIVE(cons(p(s(z0)), x1)) → c4(CONS(mark(z0), x1), ACTIVE(p(s(z0))))
ACTIVE(cons(f(z0), x1)) → c4(CONS(f(active(z0)), x1), ACTIVE(f(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c4(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c4(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(p(z0), x1)) → c4(CONS(p(active(z0)), x1), ACTIVE(p(z0)))
ACTIVE(cons(f(0), x1)) → c4(CONS(mark(cons(0, f(s(0)))), x1))
ACTIVE(s(f(s(0)))) → c5(S(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(s(p(s(z0)))) → c5(S(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(s(f(z0))) → c5(S(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(s(cons(z0, z1))) → c5(S(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(s(s(z0))) → c5(S(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(s(p(z0))) → c5(S(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(s(f(0))) → c5(S(mark(cons(0, f(s(0))))))

S tuples:

ACTIVE(p(z0)) → c6(P(active(z0)), ACTIVE(z0))
F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(f(z0)) → c15(F(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))))
ACTIVE(cons(f(s(0)), x1)) → c4(CONS(mark(f(p(s(0)))), x1), ACTIVE(f(s(0))))
ACTIVE(cons(p(s(z0)), x1)) → c4(CONS(mark(z0), x1), ACTIVE(p(s(z0))))
ACTIVE(cons(f(z0), x1)) → c4(CONS(f(active(z0)), x1), ACTIVE(f(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c4(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c4(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(p(z0), x1)) → c4(CONS(p(active(z0)), x1), ACTIVE(p(z0)))
ACTIVE(cons(f(0), x1)) → c4(CONS(mark(cons(0, f(s(0)))), x1))
ACTIVE(s(f(s(0)))) → c5(S(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(s(p(s(z0)))) → c5(S(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(s(f(z0))) → c5(S(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(s(cons(z0, z1))) → c5(S(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(s(s(z0))) → c5(S(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(s(p(z0))) → c5(S(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(s(f(0))) → c5(S(mark(cons(0, f(s(0))))))

K tuples:none
Defined Rule Symbols:

active, f, cons, s, p, proper, top

Defined Pair Symbols:

ACTIVE, F, CONS, S, P, PROPER, TOP

Compound Symbols:

c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c17, c18, c19, c20, c21, c3, c3, c4, c4, c5, c5

(23) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace ACTIVE(p(z0)) → c6(P(active(z0)), ACTIVE(z0)) by

ACTIVE(p(f(0))) → c6(P(mark(cons(0, f(s(0))))), ACTIVE(f(0)))
ACTIVE(p(f(s(0)))) → c6(P(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(p(p(s(z0)))) → c6(P(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(p(f(z0))) → c6(P(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(p(cons(z0, z1))) → c6(P(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(p(s(z0))) → c6(P(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(p(p(z0))) → c6(P(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(p(x0)) → c6

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(0)) → mark(cons(0, f(s(0))))
active(f(s(0))) → mark(f(p(s(0))))
active(p(s(z0))) → mark(z0)
active(f(z0)) → f(active(z0))
active(cons(z0, z1)) → cons(active(z0), z1)
active(s(z0)) → s(active(z0))
active(p(z0)) → p(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
cons(mark(z0), z1) → mark(cons(z0, z1))
cons(ok(z0), ok(z1)) → ok(cons(z0, z1))
s(mark(z0)) → mark(s(z0))
s(ok(z0)) → ok(s(z0))
p(mark(z0)) → mark(p(z0))
p(ok(z0)) → ok(p(z0))
proper(f(z0)) → f(proper(z0))
proper(0) → ok(0)
proper(cons(z0, z1)) → cons(proper(z0), proper(z1))
proper(s(z0)) → s(proper(z0))
proper(p(z0)) → p(proper(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(f(z0)) → c15(F(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))))
ACTIVE(cons(f(s(0)), x1)) → c4(CONS(mark(f(p(s(0)))), x1), ACTIVE(f(s(0))))
ACTIVE(cons(p(s(z0)), x1)) → c4(CONS(mark(z0), x1), ACTIVE(p(s(z0))))
ACTIVE(cons(f(z0), x1)) → c4(CONS(f(active(z0)), x1), ACTIVE(f(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c4(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c4(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(p(z0), x1)) → c4(CONS(p(active(z0)), x1), ACTIVE(p(z0)))
ACTIVE(cons(f(0), x1)) → c4(CONS(mark(cons(0, f(s(0)))), x1))
ACTIVE(s(f(s(0)))) → c5(S(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(s(p(s(z0)))) → c5(S(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(s(f(z0))) → c5(S(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(s(cons(z0, z1))) → c5(S(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(s(s(z0))) → c5(S(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(s(p(z0))) → c5(S(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(s(f(0))) → c5(S(mark(cons(0, f(s(0))))))
ACTIVE(p(f(0))) → c6(P(mark(cons(0, f(s(0))))), ACTIVE(f(0)))
ACTIVE(p(f(s(0)))) → c6(P(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(p(p(s(z0)))) → c6(P(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(p(f(z0))) → c6(P(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(p(cons(z0, z1))) → c6(P(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(p(s(z0))) → c6(P(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(p(p(z0))) → c6(P(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(p(x0)) → c6

S tuples:

F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(f(z0)) → c15(F(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))))
ACTIVE(cons(f(s(0)), x1)) → c4(CONS(mark(f(p(s(0)))), x1), ACTIVE(f(s(0))))
ACTIVE(cons(p(s(z0)), x1)) → c4(CONS(mark(z0), x1), ACTIVE(p(s(z0))))
ACTIVE(cons(f(z0), x1)) → c4(CONS(f(active(z0)), x1), ACTIVE(f(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c4(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c4(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(p(z0), x1)) → c4(CONS(p(active(z0)), x1), ACTIVE(p(z0)))
ACTIVE(cons(f(0), x1)) → c4(CONS(mark(cons(0, f(s(0)))), x1))
ACTIVE(s(f(s(0)))) → c5(S(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(s(p(s(z0)))) → c5(S(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(s(f(z0))) → c5(S(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(s(cons(z0, z1))) → c5(S(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(s(s(z0))) → c5(S(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(s(p(z0))) → c5(S(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(s(f(0))) → c5(S(mark(cons(0, f(s(0))))))
ACTIVE(p(f(0))) → c6(P(mark(cons(0, f(s(0))))), ACTIVE(f(0)))
ACTIVE(p(f(s(0)))) → c6(P(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(p(p(s(z0)))) → c6(P(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(p(f(z0))) → c6(P(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(p(cons(z0, z1))) → c6(P(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(p(s(z0))) → c6(P(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(p(p(z0))) → c6(P(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(p(x0)) → c6

K tuples:none
Defined Rule Symbols:

active, f, cons, s, p, proper, top

Defined Pair Symbols:

F, CONS, S, P, PROPER, TOP, ACTIVE

Compound Symbols:

c7, c8, c9, c10, c11, c12, c13, c14, c15, c17, c18, c19, c20, c21, c3, c3, c4, c4, c5, c5, c6, c6

(25) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

ACTIVE(p(x0)) → c6

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(0)) → mark(cons(0, f(s(0))))
active(f(s(0))) → mark(f(p(s(0))))
active(p(s(z0))) → mark(z0)
active(f(z0)) → f(active(z0))
active(cons(z0, z1)) → cons(active(z0), z1)
active(s(z0)) → s(active(z0))
active(p(z0)) → p(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
cons(mark(z0), z1) → mark(cons(z0, z1))
cons(ok(z0), ok(z1)) → ok(cons(z0, z1))
s(mark(z0)) → mark(s(z0))
s(ok(z0)) → ok(s(z0))
p(mark(z0)) → mark(p(z0))
p(ok(z0)) → ok(p(z0))
proper(f(z0)) → f(proper(z0))
proper(0) → ok(0)
proper(cons(z0, z1)) → cons(proper(z0), proper(z1))
proper(s(z0)) → s(proper(z0))
proper(p(z0)) → p(proper(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(f(z0)) → c15(F(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))))
ACTIVE(cons(f(s(0)), x1)) → c4(CONS(mark(f(p(s(0)))), x1), ACTIVE(f(s(0))))
ACTIVE(cons(p(s(z0)), x1)) → c4(CONS(mark(z0), x1), ACTIVE(p(s(z0))))
ACTIVE(cons(f(z0), x1)) → c4(CONS(f(active(z0)), x1), ACTIVE(f(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c4(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c4(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(p(z0), x1)) → c4(CONS(p(active(z0)), x1), ACTIVE(p(z0)))
ACTIVE(cons(f(0), x1)) → c4(CONS(mark(cons(0, f(s(0)))), x1))
ACTIVE(s(f(s(0)))) → c5(S(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(s(p(s(z0)))) → c5(S(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(s(f(z0))) → c5(S(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(s(cons(z0, z1))) → c5(S(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(s(s(z0))) → c5(S(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(s(p(z0))) → c5(S(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(s(f(0))) → c5(S(mark(cons(0, f(s(0))))))
ACTIVE(p(f(0))) → c6(P(mark(cons(0, f(s(0))))), ACTIVE(f(0)))
ACTIVE(p(f(s(0)))) → c6(P(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(p(p(s(z0)))) → c6(P(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(p(f(z0))) → c6(P(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(p(cons(z0, z1))) → c6(P(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(p(s(z0))) → c6(P(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(p(p(z0))) → c6(P(p(active(z0))), ACTIVE(p(z0)))

S tuples:

F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(f(z0)) → c15(F(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))))
ACTIVE(cons(f(s(0)), x1)) → c4(CONS(mark(f(p(s(0)))), x1), ACTIVE(f(s(0))))
ACTIVE(cons(p(s(z0)), x1)) → c4(CONS(mark(z0), x1), ACTIVE(p(s(z0))))
ACTIVE(cons(f(z0), x1)) → c4(CONS(f(active(z0)), x1), ACTIVE(f(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c4(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c4(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(p(z0), x1)) → c4(CONS(p(active(z0)), x1), ACTIVE(p(z0)))
ACTIVE(cons(f(0), x1)) → c4(CONS(mark(cons(0, f(s(0)))), x1))
ACTIVE(s(f(s(0)))) → c5(S(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(s(p(s(z0)))) → c5(S(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(s(f(z0))) → c5(S(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(s(cons(z0, z1))) → c5(S(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(s(s(z0))) → c5(S(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(s(p(z0))) → c5(S(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(s(f(0))) → c5(S(mark(cons(0, f(s(0))))))
ACTIVE(p(f(0))) → c6(P(mark(cons(0, f(s(0))))), ACTIVE(f(0)))
ACTIVE(p(f(s(0)))) → c6(P(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(p(p(s(z0)))) → c6(P(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(p(f(z0))) → c6(P(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(p(cons(z0, z1))) → c6(P(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(p(s(z0))) → c6(P(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(p(p(z0))) → c6(P(p(active(z0))), ACTIVE(p(z0)))

K tuples:none
Defined Rule Symbols:

active, f, cons, s, p, proper, top

Defined Pair Symbols:

F, CONS, S, P, PROPER, TOP, ACTIVE

Compound Symbols:

c7, c8, c9, c10, c11, c12, c13, c14, c15, c17, c18, c19, c20, c21, c3, c3, c4, c4, c5, c5, c6

(27) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(0)) → mark(cons(0, f(s(0))))
active(f(s(0))) → mark(f(p(s(0))))
active(p(s(z0))) → mark(z0)
active(f(z0)) → f(active(z0))
active(cons(z0, z1)) → cons(active(z0), z1)
active(s(z0)) → s(active(z0))
active(p(z0)) → p(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
cons(mark(z0), z1) → mark(cons(z0, z1))
cons(ok(z0), ok(z1)) → ok(cons(z0, z1))
s(mark(z0)) → mark(s(z0))
s(ok(z0)) → ok(s(z0))
p(mark(z0)) → mark(p(z0))
p(ok(z0)) → ok(p(z0))
proper(f(z0)) → f(proper(z0))
proper(0) → ok(0)
proper(cons(z0, z1)) → cons(proper(z0), proper(z1))
proper(s(z0)) → s(proper(z0))
proper(p(z0)) → p(proper(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(f(z0)) → c15(F(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))))
ACTIVE(cons(f(s(0)), x1)) → c4(CONS(mark(f(p(s(0)))), x1), ACTIVE(f(s(0))))
ACTIVE(cons(p(s(z0)), x1)) → c4(CONS(mark(z0), x1), ACTIVE(p(s(z0))))
ACTIVE(cons(f(z0), x1)) → c4(CONS(f(active(z0)), x1), ACTIVE(f(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c4(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c4(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(p(z0), x1)) → c4(CONS(p(active(z0)), x1), ACTIVE(p(z0)))
ACTIVE(cons(f(0), x1)) → c4(CONS(mark(cons(0, f(s(0)))), x1))
ACTIVE(s(f(s(0)))) → c5(S(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(s(p(s(z0)))) → c5(S(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(s(f(z0))) → c5(S(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(s(cons(z0, z1))) → c5(S(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(s(s(z0))) → c5(S(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(s(p(z0))) → c5(S(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(s(f(0))) → c5(S(mark(cons(0, f(s(0))))))
ACTIVE(p(f(s(0)))) → c6(P(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(p(p(s(z0)))) → c6(P(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(p(f(z0))) → c6(P(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(p(cons(z0, z1))) → c6(P(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(p(s(z0))) → c6(P(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(p(p(z0))) → c6(P(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(p(f(0))) → c6(P(mark(cons(0, f(s(0))))))

S tuples:

F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(f(z0)) → c15(F(proper(z0)), PROPER(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))))
ACTIVE(cons(f(s(0)), x1)) → c4(CONS(mark(f(p(s(0)))), x1), ACTIVE(f(s(0))))
ACTIVE(cons(p(s(z0)), x1)) → c4(CONS(mark(z0), x1), ACTIVE(p(s(z0))))
ACTIVE(cons(f(z0), x1)) → c4(CONS(f(active(z0)), x1), ACTIVE(f(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c4(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c4(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(p(z0), x1)) → c4(CONS(p(active(z0)), x1), ACTIVE(p(z0)))
ACTIVE(cons(f(0), x1)) → c4(CONS(mark(cons(0, f(s(0)))), x1))
ACTIVE(s(f(s(0)))) → c5(S(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(s(p(s(z0)))) → c5(S(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(s(f(z0))) → c5(S(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(s(cons(z0, z1))) → c5(S(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(s(s(z0))) → c5(S(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(s(p(z0))) → c5(S(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(s(f(0))) → c5(S(mark(cons(0, f(s(0))))))
ACTIVE(p(f(s(0)))) → c6(P(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(p(p(s(z0)))) → c6(P(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(p(f(z0))) → c6(P(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(p(cons(z0, z1))) → c6(P(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(p(s(z0))) → c6(P(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(p(p(z0))) → c6(P(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(p(f(0))) → c6(P(mark(cons(0, f(s(0))))))

K tuples:none
Defined Rule Symbols:

active, f, cons, s, p, proper, top

Defined Pair Symbols:

F, CONS, S, P, PROPER, TOP, ACTIVE

Compound Symbols:

c7, c8, c9, c10, c11, c12, c13, c14, c15, c17, c18, c19, c20, c21, c3, c3, c4, c4, c5, c5, c6, c6

(29) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace PROPER(f(z0)) → c15(F(proper(z0)), PROPER(z0)) by

PROPER(f(f(z0))) → c15(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(0)) → c15(F(ok(0)), PROPER(0))
PROPER(f(cons(z0, z1))) → c15(F(cons(proper(z0), proper(z1))), PROPER(cons(z0, z1)))
PROPER(f(s(z0))) → c15(F(s(proper(z0))), PROPER(s(z0)))
PROPER(f(p(z0))) → c15(F(p(proper(z0))), PROPER(p(z0)))
PROPER(f(x0)) → c15

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(0)) → mark(cons(0, f(s(0))))
active(f(s(0))) → mark(f(p(s(0))))
active(p(s(z0))) → mark(z0)
active(f(z0)) → f(active(z0))
active(cons(z0, z1)) → cons(active(z0), z1)
active(s(z0)) → s(active(z0))
active(p(z0)) → p(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
cons(mark(z0), z1) → mark(cons(z0, z1))
cons(ok(z0), ok(z1)) → ok(cons(z0, z1))
s(mark(z0)) → mark(s(z0))
s(ok(z0)) → ok(s(z0))
p(mark(z0)) → mark(p(z0))
p(ok(z0)) → ok(p(z0))
proper(f(z0)) → f(proper(z0))
proper(0) → ok(0)
proper(cons(z0, z1)) → cons(proper(z0), proper(z1))
proper(s(z0)) → s(proper(z0))
proper(p(z0)) → p(proper(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))))
ACTIVE(cons(f(s(0)), x1)) → c4(CONS(mark(f(p(s(0)))), x1), ACTIVE(f(s(0))))
ACTIVE(cons(p(s(z0)), x1)) → c4(CONS(mark(z0), x1), ACTIVE(p(s(z0))))
ACTIVE(cons(f(z0), x1)) → c4(CONS(f(active(z0)), x1), ACTIVE(f(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c4(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c4(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(p(z0), x1)) → c4(CONS(p(active(z0)), x1), ACTIVE(p(z0)))
ACTIVE(cons(f(0), x1)) → c4(CONS(mark(cons(0, f(s(0)))), x1))
ACTIVE(s(f(s(0)))) → c5(S(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(s(p(s(z0)))) → c5(S(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(s(f(z0))) → c5(S(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(s(cons(z0, z1))) → c5(S(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(s(s(z0))) → c5(S(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(s(p(z0))) → c5(S(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(s(f(0))) → c5(S(mark(cons(0, f(s(0))))))
ACTIVE(p(f(s(0)))) → c6(P(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(p(p(s(z0)))) → c6(P(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(p(f(z0))) → c6(P(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(p(cons(z0, z1))) → c6(P(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(p(s(z0))) → c6(P(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(p(p(z0))) → c6(P(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(p(f(0))) → c6(P(mark(cons(0, f(s(0))))))
PROPER(f(f(z0))) → c15(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(0)) → c15(F(ok(0)), PROPER(0))
PROPER(f(cons(z0, z1))) → c15(F(cons(proper(z0), proper(z1))), PROPER(cons(z0, z1)))
PROPER(f(s(z0))) → c15(F(s(proper(z0))), PROPER(s(z0)))
PROPER(f(p(z0))) → c15(F(p(proper(z0))), PROPER(p(z0)))
PROPER(f(x0)) → c15

S tuples:

F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))))
ACTIVE(cons(f(s(0)), x1)) → c4(CONS(mark(f(p(s(0)))), x1), ACTIVE(f(s(0))))
ACTIVE(cons(p(s(z0)), x1)) → c4(CONS(mark(z0), x1), ACTIVE(p(s(z0))))
ACTIVE(cons(f(z0), x1)) → c4(CONS(f(active(z0)), x1), ACTIVE(f(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c4(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c4(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(p(z0), x1)) → c4(CONS(p(active(z0)), x1), ACTIVE(p(z0)))
ACTIVE(cons(f(0), x1)) → c4(CONS(mark(cons(0, f(s(0)))), x1))
ACTIVE(s(f(s(0)))) → c5(S(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(s(p(s(z0)))) → c5(S(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(s(f(z0))) → c5(S(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(s(cons(z0, z1))) → c5(S(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(s(s(z0))) → c5(S(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(s(p(z0))) → c5(S(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(s(f(0))) → c5(S(mark(cons(0, f(s(0))))))
ACTIVE(p(f(s(0)))) → c6(P(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(p(p(s(z0)))) → c6(P(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(p(f(z0))) → c6(P(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(p(cons(z0, z1))) → c6(P(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(p(s(z0))) → c6(P(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(p(p(z0))) → c6(P(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(p(f(0))) → c6(P(mark(cons(0, f(s(0))))))
PROPER(f(f(z0))) → c15(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(0)) → c15(F(ok(0)), PROPER(0))
PROPER(f(cons(z0, z1))) → c15(F(cons(proper(z0), proper(z1))), PROPER(cons(z0, z1)))
PROPER(f(s(z0))) → c15(F(s(proper(z0))), PROPER(s(z0)))
PROPER(f(p(z0))) → c15(F(p(proper(z0))), PROPER(p(z0)))
PROPER(f(x0)) → c15

K tuples:none
Defined Rule Symbols:

active, f, cons, s, p, proper, top

Defined Pair Symbols:

F, CONS, S, P, PROPER, TOP, ACTIVE

Compound Symbols:

c7, c8, c9, c10, c11, c12, c13, c14, c17, c18, c19, c20, c21, c3, c3, c4, c4, c5, c5, c6, c6, c15, c15

(31) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

PROPER(f(x0)) → c15

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(0)) → mark(cons(0, f(s(0))))
active(f(s(0))) → mark(f(p(s(0))))
active(p(s(z0))) → mark(z0)
active(f(z0)) → f(active(z0))
active(cons(z0, z1)) → cons(active(z0), z1)
active(s(z0)) → s(active(z0))
active(p(z0)) → p(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
cons(mark(z0), z1) → mark(cons(z0, z1))
cons(ok(z0), ok(z1)) → ok(cons(z0, z1))
s(mark(z0)) → mark(s(z0))
s(ok(z0)) → ok(s(z0))
p(mark(z0)) → mark(p(z0))
p(ok(z0)) → ok(p(z0))
proper(f(z0)) → f(proper(z0))
proper(0) → ok(0)
proper(cons(z0, z1)) → cons(proper(z0), proper(z1))
proper(s(z0)) → s(proper(z0))
proper(p(z0)) → p(proper(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))))
ACTIVE(cons(f(s(0)), x1)) → c4(CONS(mark(f(p(s(0)))), x1), ACTIVE(f(s(0))))
ACTIVE(cons(p(s(z0)), x1)) → c4(CONS(mark(z0), x1), ACTIVE(p(s(z0))))
ACTIVE(cons(f(z0), x1)) → c4(CONS(f(active(z0)), x1), ACTIVE(f(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c4(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c4(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(p(z0), x1)) → c4(CONS(p(active(z0)), x1), ACTIVE(p(z0)))
ACTIVE(cons(f(0), x1)) → c4(CONS(mark(cons(0, f(s(0)))), x1))
ACTIVE(s(f(s(0)))) → c5(S(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(s(p(s(z0)))) → c5(S(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(s(f(z0))) → c5(S(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(s(cons(z0, z1))) → c5(S(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(s(s(z0))) → c5(S(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(s(p(z0))) → c5(S(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(s(f(0))) → c5(S(mark(cons(0, f(s(0))))))
ACTIVE(p(f(s(0)))) → c6(P(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(p(p(s(z0)))) → c6(P(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(p(f(z0))) → c6(P(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(p(cons(z0, z1))) → c6(P(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(p(s(z0))) → c6(P(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(p(p(z0))) → c6(P(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(p(f(0))) → c6(P(mark(cons(0, f(s(0))))))
PROPER(f(f(z0))) → c15(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(0)) → c15(F(ok(0)), PROPER(0))
PROPER(f(cons(z0, z1))) → c15(F(cons(proper(z0), proper(z1))), PROPER(cons(z0, z1)))
PROPER(f(s(z0))) → c15(F(s(proper(z0))), PROPER(s(z0)))
PROPER(f(p(z0))) → c15(F(p(proper(z0))), PROPER(p(z0)))

S tuples:

F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))))
ACTIVE(cons(f(s(0)), x1)) → c4(CONS(mark(f(p(s(0)))), x1), ACTIVE(f(s(0))))
ACTIVE(cons(p(s(z0)), x1)) → c4(CONS(mark(z0), x1), ACTIVE(p(s(z0))))
ACTIVE(cons(f(z0), x1)) → c4(CONS(f(active(z0)), x1), ACTIVE(f(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c4(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c4(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(p(z0), x1)) → c4(CONS(p(active(z0)), x1), ACTIVE(p(z0)))
ACTIVE(cons(f(0), x1)) → c4(CONS(mark(cons(0, f(s(0)))), x1))
ACTIVE(s(f(s(0)))) → c5(S(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(s(p(s(z0)))) → c5(S(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(s(f(z0))) → c5(S(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(s(cons(z0, z1))) → c5(S(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(s(s(z0))) → c5(S(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(s(p(z0))) → c5(S(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(s(f(0))) → c5(S(mark(cons(0, f(s(0))))))
ACTIVE(p(f(s(0)))) → c6(P(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(p(p(s(z0)))) → c6(P(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(p(f(z0))) → c6(P(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(p(cons(z0, z1))) → c6(P(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(p(s(z0))) → c6(P(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(p(p(z0))) → c6(P(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(p(f(0))) → c6(P(mark(cons(0, f(s(0))))))
PROPER(f(f(z0))) → c15(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(0)) → c15(F(ok(0)), PROPER(0))
PROPER(f(cons(z0, z1))) → c15(F(cons(proper(z0), proper(z1))), PROPER(cons(z0, z1)))
PROPER(f(s(z0))) → c15(F(s(proper(z0))), PROPER(s(z0)))
PROPER(f(p(z0))) → c15(F(p(proper(z0))), PROPER(p(z0)))

K tuples:none
Defined Rule Symbols:

active, f, cons, s, p, proper, top

Defined Pair Symbols:

F, CONS, S, P, PROPER, TOP, ACTIVE

Compound Symbols:

c7, c8, c9, c10, c11, c12, c13, c14, c17, c18, c19, c20, c21, c3, c3, c4, c4, c5, c5, c6, c6, c15

(33) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(0)) → mark(cons(0, f(s(0))))
active(f(s(0))) → mark(f(p(s(0))))
active(p(s(z0))) → mark(z0)
active(f(z0)) → f(active(z0))
active(cons(z0, z1)) → cons(active(z0), z1)
active(s(z0)) → s(active(z0))
active(p(z0)) → p(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
cons(mark(z0), z1) → mark(cons(z0, z1))
cons(ok(z0), ok(z1)) → ok(cons(z0, z1))
s(mark(z0)) → mark(s(z0))
s(ok(z0)) → ok(s(z0))
p(mark(z0)) → mark(p(z0))
p(ok(z0)) → ok(p(z0))
proper(f(z0)) → f(proper(z0))
proper(0) → ok(0)
proper(cons(z0, z1)) → cons(proper(z0), proper(z1))
proper(s(z0)) → s(proper(z0))
proper(p(z0)) → p(proper(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))))
ACTIVE(cons(f(s(0)), x1)) → c4(CONS(mark(f(p(s(0)))), x1), ACTIVE(f(s(0))))
ACTIVE(cons(p(s(z0)), x1)) → c4(CONS(mark(z0), x1), ACTIVE(p(s(z0))))
ACTIVE(cons(f(z0), x1)) → c4(CONS(f(active(z0)), x1), ACTIVE(f(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c4(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c4(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(p(z0), x1)) → c4(CONS(p(active(z0)), x1), ACTIVE(p(z0)))
ACTIVE(cons(f(0), x1)) → c4(CONS(mark(cons(0, f(s(0)))), x1))
ACTIVE(s(f(s(0)))) → c5(S(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(s(p(s(z0)))) → c5(S(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(s(f(z0))) → c5(S(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(s(cons(z0, z1))) → c5(S(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(s(s(z0))) → c5(S(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(s(p(z0))) → c5(S(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(s(f(0))) → c5(S(mark(cons(0, f(s(0))))))
ACTIVE(p(f(s(0)))) → c6(P(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(p(p(s(z0)))) → c6(P(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(p(f(z0))) → c6(P(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(p(cons(z0, z1))) → c6(P(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(p(s(z0))) → c6(P(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(p(p(z0))) → c6(P(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(p(f(0))) → c6(P(mark(cons(0, f(s(0))))))
PROPER(f(f(z0))) → c15(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(cons(z0, z1))) → c15(F(cons(proper(z0), proper(z1))), PROPER(cons(z0, z1)))
PROPER(f(s(z0))) → c15(F(s(proper(z0))), PROPER(s(z0)))
PROPER(f(p(z0))) → c15(F(p(proper(z0))), PROPER(p(z0)))
PROPER(f(0)) → c15(F(ok(0)))

S tuples:

F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))))
ACTIVE(cons(f(s(0)), x1)) → c4(CONS(mark(f(p(s(0)))), x1), ACTIVE(f(s(0))))
ACTIVE(cons(p(s(z0)), x1)) → c4(CONS(mark(z0), x1), ACTIVE(p(s(z0))))
ACTIVE(cons(f(z0), x1)) → c4(CONS(f(active(z0)), x1), ACTIVE(f(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c4(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c4(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(p(z0), x1)) → c4(CONS(p(active(z0)), x1), ACTIVE(p(z0)))
ACTIVE(cons(f(0), x1)) → c4(CONS(mark(cons(0, f(s(0)))), x1))
ACTIVE(s(f(s(0)))) → c5(S(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(s(p(s(z0)))) → c5(S(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(s(f(z0))) → c5(S(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(s(cons(z0, z1))) → c5(S(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(s(s(z0))) → c5(S(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(s(p(z0))) → c5(S(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(s(f(0))) → c5(S(mark(cons(0, f(s(0))))))
ACTIVE(p(f(s(0)))) → c6(P(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(p(p(s(z0)))) → c6(P(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(p(f(z0))) → c6(P(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(p(cons(z0, z1))) → c6(P(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(p(s(z0))) → c6(P(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(p(p(z0))) → c6(P(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(p(f(0))) → c6(P(mark(cons(0, f(s(0))))))
PROPER(f(f(z0))) → c15(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(cons(z0, z1))) → c15(F(cons(proper(z0), proper(z1))), PROPER(cons(z0, z1)))
PROPER(f(s(z0))) → c15(F(s(proper(z0))), PROPER(s(z0)))
PROPER(f(p(z0))) → c15(F(p(proper(z0))), PROPER(p(z0)))
PROPER(f(0)) → c15(F(ok(0)))

K tuples:none
Defined Rule Symbols:

active, f, cons, s, p, proper, top

Defined Pair Symbols:

F, CONS, S, P, PROPER, TOP, ACTIVE

Compound Symbols:

c7, c8, c9, c10, c11, c12, c13, c14, c17, c18, c19, c20, c21, c3, c3, c4, c4, c5, c5, c6, c6, c15, c15

(35) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace PROPER(cons(z0, z1)) → c17(CONS(proper(z0), proper(z1)), PROPER(z0), PROPER(z1)) by

PROPER(cons(x0, f(z0))) → c17(CONS(proper(x0), f(proper(z0))), PROPER(x0), PROPER(f(z0)))
PROPER(cons(x0, 0)) → c17(CONS(proper(x0), ok(0)), PROPER(x0), PROPER(0))
PROPER(cons(x0, cons(z0, z1))) → c17(CONS(proper(x0), cons(proper(z0), proper(z1))), PROPER(x0), PROPER(cons(z0, z1)))
PROPER(cons(x0, s(z0))) → c17(CONS(proper(x0), s(proper(z0))), PROPER(x0), PROPER(s(z0)))
PROPER(cons(x0, p(z0))) → c17(CONS(proper(x0), p(proper(z0))), PROPER(x0), PROPER(p(z0)))
PROPER(cons(f(z0), x1)) → c17(CONS(f(proper(z0)), proper(x1)), PROPER(f(z0)), PROPER(x1))
PROPER(cons(0, x1)) → c17(CONS(ok(0), proper(x1)), PROPER(0), PROPER(x1))
PROPER(cons(cons(z0, z1), x1)) → c17(CONS(cons(proper(z0), proper(z1)), proper(x1)), PROPER(cons(z0, z1)), PROPER(x1))
PROPER(cons(s(z0), x1)) → c17(CONS(s(proper(z0)), proper(x1)), PROPER(s(z0)), PROPER(x1))
PROPER(cons(p(z0), x1)) → c17(CONS(p(proper(z0)), proper(x1)), PROPER(p(z0)), PROPER(x1))
PROPER(cons(x0, x1)) → c17

(36) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(0)) → mark(cons(0, f(s(0))))
active(f(s(0))) → mark(f(p(s(0))))
active(p(s(z0))) → mark(z0)
active(f(z0)) → f(active(z0))
active(cons(z0, z1)) → cons(active(z0), z1)
active(s(z0)) → s(active(z0))
active(p(z0)) → p(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
cons(mark(z0), z1) → mark(cons(z0, z1))
cons(ok(z0), ok(z1)) → ok(cons(z0, z1))
s(mark(z0)) → mark(s(z0))
s(ok(z0)) → ok(s(z0))
p(mark(z0)) → mark(p(z0))
p(ok(z0)) → ok(p(z0))
proper(f(z0)) → f(proper(z0))
proper(0) → ok(0)
proper(cons(z0, z1)) → cons(proper(z0), proper(z1))
proper(s(z0)) → s(proper(z0))
proper(p(z0)) → p(proper(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))))
ACTIVE(cons(f(s(0)), x1)) → c4(CONS(mark(f(p(s(0)))), x1), ACTIVE(f(s(0))))
ACTIVE(cons(p(s(z0)), x1)) → c4(CONS(mark(z0), x1), ACTIVE(p(s(z0))))
ACTIVE(cons(f(z0), x1)) → c4(CONS(f(active(z0)), x1), ACTIVE(f(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c4(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c4(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(p(z0), x1)) → c4(CONS(p(active(z0)), x1), ACTIVE(p(z0)))
ACTIVE(cons(f(0), x1)) → c4(CONS(mark(cons(0, f(s(0)))), x1))
ACTIVE(s(f(s(0)))) → c5(S(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(s(p(s(z0)))) → c5(S(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(s(f(z0))) → c5(S(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(s(cons(z0, z1))) → c5(S(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(s(s(z0))) → c5(S(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(s(p(z0))) → c5(S(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(s(f(0))) → c5(S(mark(cons(0, f(s(0))))))
ACTIVE(p(f(s(0)))) → c6(P(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(p(p(s(z0)))) → c6(P(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(p(f(z0))) → c6(P(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(p(cons(z0, z1))) → c6(P(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(p(s(z0))) → c6(P(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(p(p(z0))) → c6(P(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(p(f(0))) → c6(P(mark(cons(0, f(s(0))))))
PROPER(f(f(z0))) → c15(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(cons(z0, z1))) → c15(F(cons(proper(z0), proper(z1))), PROPER(cons(z0, z1)))
PROPER(f(s(z0))) → c15(F(s(proper(z0))), PROPER(s(z0)))
PROPER(f(p(z0))) → c15(F(p(proper(z0))), PROPER(p(z0)))
PROPER(f(0)) → c15(F(ok(0)))
PROPER(cons(x0, f(z0))) → c17(CONS(proper(x0), f(proper(z0))), PROPER(x0), PROPER(f(z0)))
PROPER(cons(x0, 0)) → c17(CONS(proper(x0), ok(0)), PROPER(x0), PROPER(0))
PROPER(cons(x0, cons(z0, z1))) → c17(CONS(proper(x0), cons(proper(z0), proper(z1))), PROPER(x0), PROPER(cons(z0, z1)))
PROPER(cons(x0, s(z0))) → c17(CONS(proper(x0), s(proper(z0))), PROPER(x0), PROPER(s(z0)))
PROPER(cons(x0, p(z0))) → c17(CONS(proper(x0), p(proper(z0))), PROPER(x0), PROPER(p(z0)))
PROPER(cons(f(z0), x1)) → c17(CONS(f(proper(z0)), proper(x1)), PROPER(f(z0)), PROPER(x1))
PROPER(cons(0, x1)) → c17(CONS(ok(0), proper(x1)), PROPER(0), PROPER(x1))
PROPER(cons(cons(z0, z1), x1)) → c17(CONS(cons(proper(z0), proper(z1)), proper(x1)), PROPER(cons(z0, z1)), PROPER(x1))
PROPER(cons(s(z0), x1)) → c17(CONS(s(proper(z0)), proper(x1)), PROPER(s(z0)), PROPER(x1))
PROPER(cons(p(z0), x1)) → c17(CONS(p(proper(z0)), proper(x1)), PROPER(p(z0)), PROPER(x1))
PROPER(cons(x0, x1)) → c17

S tuples:

F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))))
ACTIVE(cons(f(s(0)), x1)) → c4(CONS(mark(f(p(s(0)))), x1), ACTIVE(f(s(0))))
ACTIVE(cons(p(s(z0)), x1)) → c4(CONS(mark(z0), x1), ACTIVE(p(s(z0))))
ACTIVE(cons(f(z0), x1)) → c4(CONS(f(active(z0)), x1), ACTIVE(f(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c4(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c4(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(p(z0), x1)) → c4(CONS(p(active(z0)), x1), ACTIVE(p(z0)))
ACTIVE(cons(f(0), x1)) → c4(CONS(mark(cons(0, f(s(0)))), x1))
ACTIVE(s(f(s(0)))) → c5(S(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(s(p(s(z0)))) → c5(S(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(s(f(z0))) → c5(S(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(s(cons(z0, z1))) → c5(S(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(s(s(z0))) → c5(S(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(s(p(z0))) → c5(S(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(s(f(0))) → c5(S(mark(cons(0, f(s(0))))))
ACTIVE(p(f(s(0)))) → c6(P(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(p(p(s(z0)))) → c6(P(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(p(f(z0))) → c6(P(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(p(cons(z0, z1))) → c6(P(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(p(s(z0))) → c6(P(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(p(p(z0))) → c6(P(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(p(f(0))) → c6(P(mark(cons(0, f(s(0))))))
PROPER(f(f(z0))) → c15(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(cons(z0, z1))) → c15(F(cons(proper(z0), proper(z1))), PROPER(cons(z0, z1)))
PROPER(f(s(z0))) → c15(F(s(proper(z0))), PROPER(s(z0)))
PROPER(f(p(z0))) → c15(F(p(proper(z0))), PROPER(p(z0)))
PROPER(f(0)) → c15(F(ok(0)))
PROPER(cons(x0, f(z0))) → c17(CONS(proper(x0), f(proper(z0))), PROPER(x0), PROPER(f(z0)))
PROPER(cons(x0, 0)) → c17(CONS(proper(x0), ok(0)), PROPER(x0), PROPER(0))
PROPER(cons(x0, cons(z0, z1))) → c17(CONS(proper(x0), cons(proper(z0), proper(z1))), PROPER(x0), PROPER(cons(z0, z1)))
PROPER(cons(x0, s(z0))) → c17(CONS(proper(x0), s(proper(z0))), PROPER(x0), PROPER(s(z0)))
PROPER(cons(x0, p(z0))) → c17(CONS(proper(x0), p(proper(z0))), PROPER(x0), PROPER(p(z0)))
PROPER(cons(f(z0), x1)) → c17(CONS(f(proper(z0)), proper(x1)), PROPER(f(z0)), PROPER(x1))
PROPER(cons(0, x1)) → c17(CONS(ok(0), proper(x1)), PROPER(0), PROPER(x1))
PROPER(cons(cons(z0, z1), x1)) → c17(CONS(cons(proper(z0), proper(z1)), proper(x1)), PROPER(cons(z0, z1)), PROPER(x1))
PROPER(cons(s(z0), x1)) → c17(CONS(s(proper(z0)), proper(x1)), PROPER(s(z0)), PROPER(x1))
PROPER(cons(p(z0), x1)) → c17(CONS(p(proper(z0)), proper(x1)), PROPER(p(z0)), PROPER(x1))
PROPER(cons(x0, x1)) → c17

K tuples:none
Defined Rule Symbols:

active, f, cons, s, p, proper, top

Defined Pair Symbols:

F, CONS, S, P, PROPER, TOP, ACTIVE

Compound Symbols:

c7, c8, c9, c10, c11, c12, c13, c14, c18, c19, c20, c21, c3, c3, c4, c4, c5, c5, c6, c6, c15, c15, c17, c17

(37) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

PROPER(cons(x0, x1)) → c17

(38) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(0)) → mark(cons(0, f(s(0))))
active(f(s(0))) → mark(f(p(s(0))))
active(p(s(z0))) → mark(z0)
active(f(z0)) → f(active(z0))
active(cons(z0, z1)) → cons(active(z0), z1)
active(s(z0)) → s(active(z0))
active(p(z0)) → p(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
cons(mark(z0), z1) → mark(cons(z0, z1))
cons(ok(z0), ok(z1)) → ok(cons(z0, z1))
s(mark(z0)) → mark(s(z0))
s(ok(z0)) → ok(s(z0))
p(mark(z0)) → mark(p(z0))
p(ok(z0)) → ok(p(z0))
proper(f(z0)) → f(proper(z0))
proper(0) → ok(0)
proper(cons(z0, z1)) → cons(proper(z0), proper(z1))
proper(s(z0)) → s(proper(z0))
proper(p(z0)) → p(proper(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))))
ACTIVE(cons(f(s(0)), x1)) → c4(CONS(mark(f(p(s(0)))), x1), ACTIVE(f(s(0))))
ACTIVE(cons(p(s(z0)), x1)) → c4(CONS(mark(z0), x1), ACTIVE(p(s(z0))))
ACTIVE(cons(f(z0), x1)) → c4(CONS(f(active(z0)), x1), ACTIVE(f(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c4(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c4(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(p(z0), x1)) → c4(CONS(p(active(z0)), x1), ACTIVE(p(z0)))
ACTIVE(cons(f(0), x1)) → c4(CONS(mark(cons(0, f(s(0)))), x1))
ACTIVE(s(f(s(0)))) → c5(S(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(s(p(s(z0)))) → c5(S(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(s(f(z0))) → c5(S(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(s(cons(z0, z1))) → c5(S(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(s(s(z0))) → c5(S(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(s(p(z0))) → c5(S(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(s(f(0))) → c5(S(mark(cons(0, f(s(0))))))
ACTIVE(p(f(s(0)))) → c6(P(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(p(p(s(z0)))) → c6(P(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(p(f(z0))) → c6(P(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(p(cons(z0, z1))) → c6(P(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(p(s(z0))) → c6(P(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(p(p(z0))) → c6(P(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(p(f(0))) → c6(P(mark(cons(0, f(s(0))))))
PROPER(f(f(z0))) → c15(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(cons(z0, z1))) → c15(F(cons(proper(z0), proper(z1))), PROPER(cons(z0, z1)))
PROPER(f(s(z0))) → c15(F(s(proper(z0))), PROPER(s(z0)))
PROPER(f(p(z0))) → c15(F(p(proper(z0))), PROPER(p(z0)))
PROPER(f(0)) → c15(F(ok(0)))
PROPER(cons(x0, f(z0))) → c17(CONS(proper(x0), f(proper(z0))), PROPER(x0), PROPER(f(z0)))
PROPER(cons(x0, 0)) → c17(CONS(proper(x0), ok(0)), PROPER(x0), PROPER(0))
PROPER(cons(x0, cons(z0, z1))) → c17(CONS(proper(x0), cons(proper(z0), proper(z1))), PROPER(x0), PROPER(cons(z0, z1)))
PROPER(cons(x0, s(z0))) → c17(CONS(proper(x0), s(proper(z0))), PROPER(x0), PROPER(s(z0)))
PROPER(cons(x0, p(z0))) → c17(CONS(proper(x0), p(proper(z0))), PROPER(x0), PROPER(p(z0)))
PROPER(cons(f(z0), x1)) → c17(CONS(f(proper(z0)), proper(x1)), PROPER(f(z0)), PROPER(x1))
PROPER(cons(0, x1)) → c17(CONS(ok(0), proper(x1)), PROPER(0), PROPER(x1))
PROPER(cons(cons(z0, z1), x1)) → c17(CONS(cons(proper(z0), proper(z1)), proper(x1)), PROPER(cons(z0, z1)), PROPER(x1))
PROPER(cons(s(z0), x1)) → c17(CONS(s(proper(z0)), proper(x1)), PROPER(s(z0)), PROPER(x1))
PROPER(cons(p(z0), x1)) → c17(CONS(p(proper(z0)), proper(x1)), PROPER(p(z0)), PROPER(x1))

S tuples:

F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))))
ACTIVE(cons(f(s(0)), x1)) → c4(CONS(mark(f(p(s(0)))), x1), ACTIVE(f(s(0))))
ACTIVE(cons(p(s(z0)), x1)) → c4(CONS(mark(z0), x1), ACTIVE(p(s(z0))))
ACTIVE(cons(f(z0), x1)) → c4(CONS(f(active(z0)), x1), ACTIVE(f(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c4(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c4(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(p(z0), x1)) → c4(CONS(p(active(z0)), x1), ACTIVE(p(z0)))
ACTIVE(cons(f(0), x1)) → c4(CONS(mark(cons(0, f(s(0)))), x1))
ACTIVE(s(f(s(0)))) → c5(S(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(s(p(s(z0)))) → c5(S(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(s(f(z0))) → c5(S(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(s(cons(z0, z1))) → c5(S(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(s(s(z0))) → c5(S(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(s(p(z0))) → c5(S(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(s(f(0))) → c5(S(mark(cons(0, f(s(0))))))
ACTIVE(p(f(s(0)))) → c6(P(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(p(p(s(z0)))) → c6(P(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(p(f(z0))) → c6(P(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(p(cons(z0, z1))) → c6(P(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(p(s(z0))) → c6(P(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(p(p(z0))) → c6(P(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(p(f(0))) → c6(P(mark(cons(0, f(s(0))))))
PROPER(f(f(z0))) → c15(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(cons(z0, z1))) → c15(F(cons(proper(z0), proper(z1))), PROPER(cons(z0, z1)))
PROPER(f(s(z0))) → c15(F(s(proper(z0))), PROPER(s(z0)))
PROPER(f(p(z0))) → c15(F(p(proper(z0))), PROPER(p(z0)))
PROPER(f(0)) → c15(F(ok(0)))
PROPER(cons(x0, f(z0))) → c17(CONS(proper(x0), f(proper(z0))), PROPER(x0), PROPER(f(z0)))
PROPER(cons(x0, 0)) → c17(CONS(proper(x0), ok(0)), PROPER(x0), PROPER(0))
PROPER(cons(x0, cons(z0, z1))) → c17(CONS(proper(x0), cons(proper(z0), proper(z1))), PROPER(x0), PROPER(cons(z0, z1)))
PROPER(cons(x0, s(z0))) → c17(CONS(proper(x0), s(proper(z0))), PROPER(x0), PROPER(s(z0)))
PROPER(cons(x0, p(z0))) → c17(CONS(proper(x0), p(proper(z0))), PROPER(x0), PROPER(p(z0)))
PROPER(cons(f(z0), x1)) → c17(CONS(f(proper(z0)), proper(x1)), PROPER(f(z0)), PROPER(x1))
PROPER(cons(0, x1)) → c17(CONS(ok(0), proper(x1)), PROPER(0), PROPER(x1))
PROPER(cons(cons(z0, z1), x1)) → c17(CONS(cons(proper(z0), proper(z1)), proper(x1)), PROPER(cons(z0, z1)), PROPER(x1))
PROPER(cons(s(z0), x1)) → c17(CONS(s(proper(z0)), proper(x1)), PROPER(s(z0)), PROPER(x1))
PROPER(cons(p(z0), x1)) → c17(CONS(p(proper(z0)), proper(x1)), PROPER(p(z0)), PROPER(x1))

K tuples:none
Defined Rule Symbols:

active, f, cons, s, p, proper, top

Defined Pair Symbols:

F, CONS, S, P, PROPER, TOP, ACTIVE

Compound Symbols:

c7, c8, c9, c10, c11, c12, c13, c14, c18, c19, c20, c21, c3, c3, c4, c4, c5, c5, c6, c6, c15, c15, c17

(39) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing tuple parts

(40) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(0)) → mark(cons(0, f(s(0))))
active(f(s(0))) → mark(f(p(s(0))))
active(p(s(z0))) → mark(z0)
active(f(z0)) → f(active(z0))
active(cons(z0, z1)) → cons(active(z0), z1)
active(s(z0)) → s(active(z0))
active(p(z0)) → p(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
cons(mark(z0), z1) → mark(cons(z0, z1))
cons(ok(z0), ok(z1)) → ok(cons(z0, z1))
s(mark(z0)) → mark(s(z0))
s(ok(z0)) → ok(s(z0))
p(mark(z0)) → mark(p(z0))
p(ok(z0)) → ok(p(z0))
proper(f(z0)) → f(proper(z0))
proper(0) → ok(0)
proper(cons(z0, z1)) → cons(proper(z0), proper(z1))
proper(s(z0)) → s(proper(z0))
proper(p(z0)) → p(proper(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))))
ACTIVE(cons(f(s(0)), x1)) → c4(CONS(mark(f(p(s(0)))), x1), ACTIVE(f(s(0))))
ACTIVE(cons(p(s(z0)), x1)) → c4(CONS(mark(z0), x1), ACTIVE(p(s(z0))))
ACTIVE(cons(f(z0), x1)) → c4(CONS(f(active(z0)), x1), ACTIVE(f(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c4(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c4(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(p(z0), x1)) → c4(CONS(p(active(z0)), x1), ACTIVE(p(z0)))
ACTIVE(cons(f(0), x1)) → c4(CONS(mark(cons(0, f(s(0)))), x1))
ACTIVE(s(f(s(0)))) → c5(S(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(s(p(s(z0)))) → c5(S(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(s(f(z0))) → c5(S(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(s(cons(z0, z1))) → c5(S(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(s(s(z0))) → c5(S(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(s(p(z0))) → c5(S(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(s(f(0))) → c5(S(mark(cons(0, f(s(0))))))
ACTIVE(p(f(s(0)))) → c6(P(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(p(p(s(z0)))) → c6(P(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(p(f(z0))) → c6(P(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(p(cons(z0, z1))) → c6(P(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(p(s(z0))) → c6(P(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(p(p(z0))) → c6(P(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(p(f(0))) → c6(P(mark(cons(0, f(s(0))))))
PROPER(f(f(z0))) → c15(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(cons(z0, z1))) → c15(F(cons(proper(z0), proper(z1))), PROPER(cons(z0, z1)))
PROPER(f(s(z0))) → c15(F(s(proper(z0))), PROPER(s(z0)))
PROPER(f(p(z0))) → c15(F(p(proper(z0))), PROPER(p(z0)))
PROPER(f(0)) → c15(F(ok(0)))
PROPER(cons(x0, f(z0))) → c17(CONS(proper(x0), f(proper(z0))), PROPER(x0), PROPER(f(z0)))
PROPER(cons(x0, cons(z0, z1))) → c17(CONS(proper(x0), cons(proper(z0), proper(z1))), PROPER(x0), PROPER(cons(z0, z1)))
PROPER(cons(x0, s(z0))) → c17(CONS(proper(x0), s(proper(z0))), PROPER(x0), PROPER(s(z0)))
PROPER(cons(x0, p(z0))) → c17(CONS(proper(x0), p(proper(z0))), PROPER(x0), PROPER(p(z0)))
PROPER(cons(f(z0), x1)) → c17(CONS(f(proper(z0)), proper(x1)), PROPER(f(z0)), PROPER(x1))
PROPER(cons(cons(z0, z1), x1)) → c17(CONS(cons(proper(z0), proper(z1)), proper(x1)), PROPER(cons(z0, z1)), PROPER(x1))
PROPER(cons(s(z0), x1)) → c17(CONS(s(proper(z0)), proper(x1)), PROPER(s(z0)), PROPER(x1))
PROPER(cons(p(z0), x1)) → c17(CONS(p(proper(z0)), proper(x1)), PROPER(p(z0)), PROPER(x1))
PROPER(cons(x0, 0)) → c17(CONS(proper(x0), ok(0)), PROPER(x0))
PROPER(cons(0, x1)) → c17(CONS(ok(0), proper(x1)), PROPER(x1))

S tuples:

F(mark(z0)) → c7(F(z0))
F(ok(z0)) → c8(F(z0))
CONS(mark(z0), z1) → c9(CONS(z0, z1))
CONS(ok(z0), ok(z1)) → c10(CONS(z0, z1))
S(mark(z0)) → c11(S(z0))
S(ok(z0)) → c12(S(z0))
P(mark(z0)) → c13(P(z0))
P(ok(z0)) → c14(P(z0))
PROPER(s(z0)) → c18(S(proper(z0)), PROPER(z0))
PROPER(p(z0)) → c19(P(proper(z0)), PROPER(z0))
TOP(mark(z0)) → c20(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c21(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(s(0)))) → c3(F(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(f(p(s(z0)))) → c3(F(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(f(f(z0))) → c3(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(cons(z0, z1))) → c3(F(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(f(s(z0))) → c3(F(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(f(p(z0))) → c3(F(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(f(f(0))) → c3(F(mark(cons(0, f(s(0))))))
ACTIVE(cons(f(s(0)), x1)) → c4(CONS(mark(f(p(s(0)))), x1), ACTIVE(f(s(0))))
ACTIVE(cons(p(s(z0)), x1)) → c4(CONS(mark(z0), x1), ACTIVE(p(s(z0))))
ACTIVE(cons(f(z0), x1)) → c4(CONS(f(active(z0)), x1), ACTIVE(f(z0)))
ACTIVE(cons(cons(z0, z1), x1)) → c4(CONS(cons(active(z0), z1), x1), ACTIVE(cons(z0, z1)))
ACTIVE(cons(s(z0), x1)) → c4(CONS(s(active(z0)), x1), ACTIVE(s(z0)))
ACTIVE(cons(p(z0), x1)) → c4(CONS(p(active(z0)), x1), ACTIVE(p(z0)))
ACTIVE(cons(f(0), x1)) → c4(CONS(mark(cons(0, f(s(0)))), x1))
ACTIVE(s(f(s(0)))) → c5(S(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(s(p(s(z0)))) → c5(S(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(s(f(z0))) → c5(S(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(s(cons(z0, z1))) → c5(S(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(s(s(z0))) → c5(S(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(s(p(z0))) → c5(S(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(s(f(0))) → c5(S(mark(cons(0, f(s(0))))))
ACTIVE(p(f(s(0)))) → c6(P(mark(f(p(s(0))))), ACTIVE(f(s(0))))
ACTIVE(p(p(s(z0)))) → c6(P(mark(z0)), ACTIVE(p(s(z0))))
ACTIVE(p(f(z0))) → c6(P(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(p(cons(z0, z1))) → c6(P(cons(active(z0), z1)), ACTIVE(cons(z0, z1)))
ACTIVE(p(s(z0))) → c6(P(s(active(z0))), ACTIVE(s(z0)))
ACTIVE(p(p(z0))) → c6(P(p(active(z0))), ACTIVE(p(z0)))
ACTIVE(p(f(0))) → c6(P(mark(cons(0, f(s(0))))))
PROPER(f(f(z0))) → c15(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(cons(z0, z1))) → c15(F(cons(proper(z0), proper(z1))), PROPER(cons(z0, z1)))
PROPER(f(s(z0))) → c15(F(s(proper(z0))), PROPER(s(z0)))
PROPER(f(p(z0))) → c15(F(p(proper(z0))), PROPER(p(z0)))
PROPER(f(0)) → c15(F(ok(0)))
PROPER(cons(x0, f(z0))) → c17(CONS(proper(x0), f(proper(z0))), PROPER(x0), PROPER(f(z0)))
PROPER(cons(x0, cons(z0, z1))) → c17(CONS(proper(x0), cons(proper(z0), proper(z1))), PROPER(x0), PROPER(cons(z0, z1)))
PROPER(cons(x0, s(z0))) → c17(CONS(proper(x0), s(proper(z0))), PROPER(x0), PROPER(s(z0)))
PROPER(cons(x0, p(z0))) → c17(CONS(proper(x0), p(proper(z0))), PROPER(x0), PROPER(p(z0)))
PROPER(cons(f(z0), x1)) → c17(CONS(f(proper(z0)), proper(x1)), PROPER(f(z0)), PROPER(x1))
PROPER(cons(cons(z0, z1), x1)) → c17(CONS(cons(proper(z0), proper(z1)), proper(x1)), PROPER(cons(z0, z1)), PROPER(x1))
PROPER(cons(s(z0), x1)) → c17(CONS(s(proper(z0)), proper(x1)), PROPER(s(z0)), PROPER(x1))
PROPER(cons(p(z0), x1)) → c17(CONS(p(proper(z0)), proper(x1)), PROPER(p(z0)), PROPER(x1))
PROPER(cons(x0, 0)) → c17(CONS(proper(x0), ok(0)), PROPER(x0))
PROPER(cons(0, x1)) → c17(CONS(ok(0), proper(x1)), PROPER(x1))

K tuples:none
Defined Rule Symbols:

active, f, cons, s, p, proper, top

Defined Pair Symbols:

F, CONS, S, P, PROPER, TOP, ACTIVE

Compound Symbols:

c7, c8, c9, c10, c11, c12, c13, c14, c18, c19, c20, c21, c3, c3, c4, c4, c5, c5, c6, c6, c15, c15, c17, c17

(41) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 2.

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2, 3, 4, 5, 6, 7]
transitions:
00() → 0
mark0(0) → 0
ok0(0) → 0
active0(0) → 1
f0(0) → 2
cons0(0, 0) → 3
s0(0) → 4
p0(0) → 5
proper0(0) → 6
top0(0) → 7
f1(0) → 8
mark1(8) → 2
cons1(0, 0) → 9
mark1(9) → 3
s1(0) → 10
mark1(10) → 4
p1(0) → 11
mark1(11) → 5
01() → 12
ok1(12) → 6
f1(0) → 13
ok1(13) → 2
cons1(0, 0) → 14
ok1(14) → 3
s1(0) → 15
ok1(15) → 4
p1(0) → 16
ok1(16) → 5
proper1(0) → 17
top1(17) → 7
active1(0) → 18
top1(18) → 7
mark1(8) → 8
mark1(8) → 13
mark1(9) → 9
mark1(9) → 14
mark1(10) → 10
mark1(10) → 15
mark1(11) → 11
mark1(11) → 16
ok1(12) → 17
ok1(13) → 8
ok1(13) → 13
ok1(14) → 9
ok1(14) → 14
ok1(15) → 10
ok1(15) → 15
ok1(16) → 11
ok1(16) → 16
active2(12) → 19
top2(19) → 7

(0) Obligation:

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

(2) Obligation:

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

(4) Obligation:

(5) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(6) Obligation:

(7) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

(8) Obligation:

(9) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

(10) Obligation:

(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(12) Obligation:

(13) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

(14) Obligation:

(15) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

(16) Obligation:

(17) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(18) Obligation:

(19) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

(20) Obligation:

(21) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

(22) Obligation:

(23) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(24) Obligation:

(25) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

(26) Obligation:

(27) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

(28) Obligation:

(29) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(30) Obligation:

(31) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

(32) Obligation:

(33) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

(34) Obligation:

(35) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(36) Obligation:

(37) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

(38) Obligation:

(39) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

(40) Obligation:

(41) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

(42) BOUNDS(O(1), O(n^1))