### (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:

+(0, y) → y

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

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

Rewrite Strategy: FULL

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

Converted rc-obligation to irc-obligation.

As the TRS is a non-duplicating overlay system, 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:

+(0, y) → y

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

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

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 3.

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) → 1

s1(0) → 1

s1(0) → 3

01() → 5

+1(0, 5) → 4

+1(3, 4) → 2

s1(2) → 1

s1(0) → 4

s2(0) → 2

s2(0) → 7

02() → 9

+2(0, 9) → 8

+2(7, 8) → 6

s2(6) → 2

s1(0) → 8

s3(0) → 6

s2(6) → 6

0 → 1

5 → 4

9 → 8

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