### (0) Obligation:

The Runtime Complexity (full) of the given

*CpxTRS* could be proven to be

BOUNDS(1, n^1).

The TRS R consists of the following rules:

f(0) → s(0)

f(s(0)) → s(s(0))

f(s(0)) → *(s(s(0)), f(0))

f(+(x, s(0))) → +(s(s(0)), f(x))

f(+(x, y)) → *(f(x), f(y))

Rewrite Strategy: FULL

### (1) RcToIrcProof (BOTH BOUNDS(ID, ID) transformation)

Converted rc-obligation to irc-obligation.

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

### (2) Obligation:

The Runtime Complexity (innermost) of the given

*CpxTRS* could be proven to be

BOUNDS(1, n^1).

The TRS R consists of the following rules:

f(0) → s(0)

f(s(0)) → s(s(0))

f(s(0)) → *(s(s(0)), f(0))

f(+(x, s(0))) → +(s(s(0)), f(x))

f(+(x, y)) → *(f(x), f(y))

Rewrite Strategy: INNERMOST

### (3) 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]

transitions:

00() → 0

s0(0) → 0

*0(0, 0) → 0

+0(0, 0) → 0

f0(0) → 1

01() → 2

s1(2) → 1

s1(2) → 3

s1(3) → 1

s1(3) → 4

01() → 6

f1(6) → 5

*1(4, 5) → 1

s1(3) → 7

f1(0) → 8

+1(7, 8) → 1

f1(0) → 9

f1(0) → 10

*1(9, 10) → 1

s1(2) → 8

s1(2) → 9

s1(2) → 10

02() → 11

s2(11) → 5

s1(3) → 8

s1(3) → 9

s1(3) → 10

*1(4, 5) → 8

*1(4, 5) → 9

*1(4, 5) → 10

+1(7, 8) → 8

+1(7, 8) → 9

+1(7, 8) → 10

*1(9, 10) → 8

*1(9, 10) → 9

*1(9, 10) → 10

### (4) BOUNDS(1, n^1)