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

(0) Obligation:

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

div2(S(S(x))) → +(S(0), div2(x))
div2(S(0)) → 0
div2(0) → 0

The (relative) TRS S consists of the following rules:

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

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (UPPER BOUND(ID) transformation)

Converted Cpx (relative) TRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(z0, S(0)) → S(z0)
+(S(0), z0) → S(z0)
div2(S(S(z0))) → +(S(0), div2(z0))
div2(S(0)) → 0
div2(0) → 0

Tuples:

+'(z0, S(0)) → c
+'(S(0), z0) → c1
DIV2(S(S(z0))) → c2(+'(S(0), div2(z0)), DIV2(z0))
DIV2(S(0)) → c3
DIV2(0) → c4

S tuples:

DIV2(S(S(z0))) → c2(+'(S(0), div2(z0)), DIV2(z0))
DIV2(S(0)) → c3
DIV2(0) → c4

K tuples:none
Defined Rule Symbols:

div2, +

Defined Pair Symbols:

+', DIV2

Compound Symbols:

c, c1, c2, c3, c4

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

Removed 4 trailing nodes:

+'(S(0), z0) → c1
DIV2(0) → c4
DIV2(S(0)) → c3
+'(z0, S(0)) → c

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(z0, S(0)) → S(z0)
+(S(0), z0) → S(z0)
div2(S(S(z0))) → +(S(0), div2(z0))
div2(S(0)) → 0
div2(0) → 0

Tuples:

DIV2(S(S(z0))) → c2(+'(S(0), div2(z0)), DIV2(z0))

S tuples:

DIV2(S(S(z0))) → c2(+'(S(0), div2(z0)), DIV2(z0))

K tuples:none
Defined Rule Symbols:

div2, +

Defined Pair Symbols:

DIV2

Compound Symbols:

c2

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

Removed 1 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(z0, S(0)) → S(z0)
+(S(0), z0) → S(z0)
div2(S(S(z0))) → +(S(0), div2(z0))
div2(S(0)) → 0
div2(0) → 0

Tuples:

DIV2(S(S(z0))) → c2(DIV2(z0))

S tuples:

DIV2(S(S(z0))) → c2(DIV2(z0))

K tuples:none
Defined Rule Symbols:

div2, +

Defined Pair Symbols:

DIV2

Compound Symbols:

c2

(7) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

+(z0, S(0)) → S(z0)
+(S(0), z0) → S(z0)
div2(S(S(z0))) → +(S(0), div2(z0))
div2(S(0)) → 0
div2(0) → 0

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

DIV2(S(S(z0))) → c2(DIV2(z0))

S tuples:

DIV2(S(S(z0))) → c2(DIV2(z0))

K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:

DIV2

Compound Symbols:

c2

(9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

DIV2(S(S(z0))) → c2(DIV2(z0))

We considered the (Usable) Rules:none
And the Tuples:

DIV2(S(S(z0))) → c2(DIV2(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(DIV2(x₁)) = [4]x₁   
POL(S(x₁)) = [1] + x₁   
POL(c2(x₁)) = x₁   

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

DIV2(S(S(z0))) → c2(DIV2(z0))

S tuples:none
K tuples:

DIV2(S(S(z0))) → c2(DIV2(z0))

Defined Rule Symbols:none

Defined Pair Symbols:

DIV2

Compound Symbols:

c2

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

The set S is empty

(12) BOUNDS(1, 1)