The Runtime Complexity (innermost) of the given

0 CpxTRS

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

↳2 CdtProblem

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

↳4 CdtProblem

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

↳6 CdtProblem

↳7 CdtUsableRulesProof (⇔, 0 ms)

↳8 CdtProblem

↳9 CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))), 36 ms)

↳10 CdtProblem

↳11 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)

↳12 BOUNDS(O(1), O(1))

The TRS R consists of the following rules:

dbl(S(0), S(0)) → S(S(S(S(0))))

unsafe(S(x)) → dbl(unsafe(x), 0)

unsafe(0) → 0

dbl(0, y) → y

Rewrite Strategy: INNERMOST

Rules:

Tuples:

dbl(S(0), S(0)) → S(S(S(S(0))))

dbl(0, z0) → z0

unsafe(S(z0)) → dbl(unsafe(z0), 0)

unsafe(0) → 0

S tuples:

DBL(S(0), S(0)) → c

DBL(0, z0) → c1

UNSAFE(S(z0)) → c2(DBL(unsafe(z0), 0), UNSAFE(z0))

UNSAFE(0) → c3

K tuples:none

DBL(S(0), S(0)) → c

DBL(0, z0) → c1

UNSAFE(S(z0)) → c2(DBL(unsafe(z0), 0), UNSAFE(z0))

UNSAFE(0) → c3

Defined Rule Symbols:

dbl, unsafe

Defined Pair Symbols:

DBL, UNSAFE

Compound Symbols:

c, c1, c2, c3

UNSAFE(0) → c3

DBL(0, z0) → c1

DBL(S(0), S(0)) → c

Rules:

Tuples:

dbl(S(0), S(0)) → S(S(S(S(0))))

dbl(0, z0) → z0

unsafe(S(z0)) → dbl(unsafe(z0), 0)

unsafe(0) → 0

S tuples:

UNSAFE(S(z0)) → c2(DBL(unsafe(z0), 0), UNSAFE(z0))

K tuples:none

UNSAFE(S(z0)) → c2(DBL(unsafe(z0), 0), UNSAFE(z0))

Defined Rule Symbols:

dbl, unsafe

Defined Pair Symbols:

UNSAFE

Compound Symbols:

c2

Rules:

Tuples:

dbl(S(0), S(0)) → S(S(S(S(0))))

dbl(0, z0) → z0

unsafe(S(z0)) → dbl(unsafe(z0), 0)

unsafe(0) → 0

S tuples:

UNSAFE(S(z0)) → c2(UNSAFE(z0))

K tuples:none

UNSAFE(S(z0)) → c2(UNSAFE(z0))

Defined Rule Symbols:

dbl, unsafe

Defined Pair Symbols:

UNSAFE

Compound Symbols:

c2

dbl(S(0), S(0)) → S(S(S(S(0))))

dbl(0, z0) → z0

unsafe(S(z0)) → dbl(unsafe(z0), 0)

unsafe(0) → 0

Rules:none

Tuples:

S tuples:

UNSAFE(S(z0)) → c2(UNSAFE(z0))

K tuples:none

UNSAFE(S(z0)) → c2(UNSAFE(z0))

Defined Rule Symbols:none

Defined Pair Symbols:

UNSAFE

Compound Symbols:

c2

We considered the (Usable) Rules:none

UNSAFE(S(z0)) → c2(UNSAFE(z0))

And the Tuples:

The order we found is given by the following interpretation:

UNSAFE(S(z0)) → c2(UNSAFE(z0))

Polynomial interpretation :

POL(S(x) = [1] + x_{1})_{1}^{ }_{ }

POL(UNSAFE(x) = [5]x_{1})_{1}^{ }_{ }

POL(c2(x) = x_{1})_{1}^{ }_{ }

Rules:none

Tuples:

S tuples:none

UNSAFE(S(z0)) → c2(UNSAFE(z0))

K tuples:

Defined Rule Symbols:none

UNSAFE(S(z0)) → c2(UNSAFE(z0))

Defined Pair Symbols:

UNSAFE

Compound Symbols:

c2