The Runtime Complexity (full) of the given

0 CpxTRS

↳1 NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID), 19 ms)

↳2 CpxTRS

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

↳4 CpxTRS

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

↳6 CdtProblem

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

↳8 CdtProblem

↳9 CdtUsableRulesProof (⇔, 0 ms)

↳10 CdtProblem

↳11 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 60 ms)

↳12 CdtProblem

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

↳14 BOUNDS(1, 1)

The TRS R consists of the following rules:

:(:(x, y), z) → :(x, :(y, z))

:(+(x, y), z) → +(:(x, z), :(y, z))

:(z, +(x, f(y))) → :(g(z, y), +(x, a))

Rewrite Strategy: FULL

Hence, the left-hand sides of the following rules are not basic-reachable and can be removed:

:(:(x, y), z) → :(x, :(y, z))

The TRS R consists of the following rules:

:(+(x, y), z) → +(:(x, z), :(y, z))

:(z, +(x, f(y))) → :(g(z, y), +(x, a))

Rewrite Strategy: FULL

As the TRS does not nest defined symbols, we have rc = irc.

The TRS R consists of the following rules:

:(+(x, y), z) → +(:(x, z), :(y, z))

:(z, +(x, f(y))) → :(g(z, y), +(x, a))

Rewrite Strategy: INNERMOST

Rules:

Tuples:

:(+(z0, z1), z2) → +(:(z0, z2), :(z1, z2))

:(z0, +(z1, f(z2))) → :(g(z0, z2), +(z1, a))

S tuples:

:'(+(z0, z1), z2) → c(:'(z0, z2), :'(z1, z2))

:'(z0, +(z1, f(z2))) → c1(:'(g(z0, z2), +(z1, a)))

K tuples:none

:'(+(z0, z1), z2) → c(:'(z0, z2), :'(z1, z2))

:'(z0, +(z1, f(z2))) → c1(:'(g(z0, z2), +(z1, a)))

Defined Rule Symbols:

:

Defined Pair Symbols:

:'

Compound Symbols:

c, c1

:'(z0, +(z1, f(z2))) → c1(:'(g(z0, z2), +(z1, a)))

Rules:

Tuples:

:(+(z0, z1), z2) → +(:(z0, z2), :(z1, z2))

:(z0, +(z1, f(z2))) → :(g(z0, z2), +(z1, a))

S tuples:

:'(+(z0, z1), z2) → c(:'(z0, z2), :'(z1, z2))

K tuples:none

:'(+(z0, z1), z2) → c(:'(z0, z2), :'(z1, z2))

Defined Rule Symbols:

:

Defined Pair Symbols:

:'

Compound Symbols:

c

:(+(z0, z1), z2) → +(:(z0, z2), :(z1, z2))

:(z0, +(z1, f(z2))) → :(g(z0, z2), +(z1, a))

Rules:none

Tuples:

S tuples:

:'(+(z0, z1), z2) → c(:'(z0, z2), :'(z1, z2))

K tuples:none

:'(+(z0, z1), z2) → c(:'(z0, z2), :'(z1, z2))

Defined Rule Symbols:none

Defined Pair Symbols:

:'

Compound Symbols:

c

We considered the (Usable) Rules:none

:'(+(z0, z1), z2) → c(:'(z0, z2), :'(z1, z2))

And the Tuples:

The order we found is given by the following interpretation:

:'(+(z0, z1), z2) → c(:'(z0, z2), :'(z1, z2))

Polynomial interpretation :

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

POL(:'(x) = [2] + [2]x_{1}, x_{2})_{1}^{ }_{ }

POL(c(x) = x_{1}, x_{2})_{1}+ x_{2}^{ }_{ }

Rules:none

Tuples:

S tuples:none

:'(+(z0, z1), z2) → c(:'(z0, z2), :'(z1, z2))

K tuples:

Defined Rule Symbols:none

:'(+(z0, z1), z2) → c(:'(z0, z2), :'(z1, z2))

Defined Pair Symbols:

:'

Compound Symbols:

c