### (0) Obligation:

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

cond1(true, x, y) → cond2(gr(y, 0), x, y)
cond2(true, x, y) → cond2(gr(y, 0), x, p(y))
cond2(false, x, y) → cond1(gr(x, 0), p(x), y)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
p(0) → 0
p(s(x)) → x

Rewrite Strategy: INNERMOST

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

Converted Cpx (relative) TRS to CDT

### (2) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond1(true, z0, z1) → cond2(gr(z1, 0), z0, z1)
cond2(true, z0, z1) → cond2(gr(z1, 0), z0, p(z1))
cond2(false, z0, z1) → cond1(gr(z0, 0), p(z0), z1)
gr(0, z0) → false
gr(s(z0), 0) → true
gr(s(z0), s(z1)) → gr(z0, z1)
p(0) → 0
p(s(z0)) → z0
Tuples:

COND1(true, z0, z1) → c(COND2(gr(z1, 0), z0, z1), GR(z1, 0))
COND2(true, z0, z1) → c1(COND2(gr(z1, 0), z0, p(z1)), GR(z1, 0), P(z1))
COND2(false, z0, z1) → c2(COND1(gr(z0, 0), p(z0), z1), GR(z0, 0), P(z0))
GR(0, z0) → c3
GR(s(z0), 0) → c4
GR(s(z0), s(z1)) → c5(GR(z0, z1))
P(0) → c6
P(s(z0)) → c7
S tuples:

COND1(true, z0, z1) → c(COND2(gr(z1, 0), z0, z1), GR(z1, 0))
COND2(true, z0, z1) → c1(COND2(gr(z1, 0), z0, p(z1)), GR(z1, 0), P(z1))
COND2(false, z0, z1) → c2(COND1(gr(z0, 0), p(z0), z1), GR(z0, 0), P(z0))
GR(0, z0) → c3
GR(s(z0), 0) → c4
GR(s(z0), s(z1)) → c5(GR(z0, z1))
P(0) → c6
P(s(z0)) → c7
K tuples:none
Defined Rule Symbols:

cond1, cond2, gr, p

Defined Pair Symbols:

COND1, COND2, GR, P

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7

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

Removed 4 trailing nodes:

GR(0, z0) → c3
GR(s(z0), 0) → c4
P(0) → c6
P(s(z0)) → c7

### (4) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond1(true, z0, z1) → cond2(gr(z1, 0), z0, z1)
cond2(true, z0, z1) → cond2(gr(z1, 0), z0, p(z1))
cond2(false, z0, z1) → cond1(gr(z0, 0), p(z0), z1)
gr(0, z0) → false
gr(s(z0), 0) → true
gr(s(z0), s(z1)) → gr(z0, z1)
p(0) → 0
p(s(z0)) → z0
Tuples:

COND1(true, z0, z1) → c(COND2(gr(z1, 0), z0, z1), GR(z1, 0))
COND2(true, z0, z1) → c1(COND2(gr(z1, 0), z0, p(z1)), GR(z1, 0), P(z1))
COND2(false, z0, z1) → c2(COND1(gr(z0, 0), p(z0), z1), GR(z0, 0), P(z0))
GR(s(z0), s(z1)) → c5(GR(z0, z1))
S tuples:

COND1(true, z0, z1) → c(COND2(gr(z1, 0), z0, z1), GR(z1, 0))
COND2(true, z0, z1) → c1(COND2(gr(z1, 0), z0, p(z1)), GR(z1, 0), P(z1))
COND2(false, z0, z1) → c2(COND1(gr(z0, 0), p(z0), z1), GR(z0, 0), P(z0))
GR(s(z0), s(z1)) → c5(GR(z0, z1))
K tuples:none
Defined Rule Symbols:

cond1, cond2, gr, p

Defined Pair Symbols:

COND1, COND2, GR

Compound Symbols:

c, c1, c2, c5

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

Removed 5 trailing tuple parts

### (6) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond1(true, z0, z1) → cond2(gr(z1, 0), z0, z1)
cond2(true, z0, z1) → cond2(gr(z1, 0), z0, p(z1))
cond2(false, z0, z1) → cond1(gr(z0, 0), p(z0), z1)
gr(0, z0) → false
gr(s(z0), 0) → true
gr(s(z0), s(z1)) → gr(z0, z1)
p(0) → 0
p(s(z0)) → z0
Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, z0, z1) → c(COND2(gr(z1, 0), z0, z1))
COND2(true, z0, z1) → c1(COND2(gr(z1, 0), z0, p(z1)))
COND2(false, z0, z1) → c2(COND1(gr(z0, 0), p(z0), z1))
S tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, z0, z1) → c(COND2(gr(z1, 0), z0, z1))
COND2(true, z0, z1) → c1(COND2(gr(z1, 0), z0, p(z1)))
COND2(false, z0, z1) → c2(COND1(gr(z0, 0), p(z0), z1))
K tuples:none
Defined Rule Symbols:

cond1, cond2, gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c1, c2

### (7) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

cond1(true, z0, z1) → cond2(gr(z1, 0), z0, z1)
cond2(true, z0, z1) → cond2(gr(z1, 0), z0, p(z1))
cond2(false, z0, z1) → cond1(gr(z0, 0), p(z0), z1)
gr(s(z0), s(z1)) → gr(z0, z1)

### (8) Obligation:

Complexity Dependency Tuples Problem
Rules:

gr(0, z0) → false
gr(s(z0), 0) → true
p(0) → 0
p(s(z0)) → z0
Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, z0, z1) → c(COND2(gr(z1, 0), z0, z1))
COND2(true, z0, z1) → c1(COND2(gr(z1, 0), z0, p(z1)))
COND2(false, z0, z1) → c2(COND1(gr(z0, 0), p(z0), z1))
S tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, z0, z1) → c(COND2(gr(z1, 0), z0, z1))
COND2(true, z0, z1) → c1(COND2(gr(z1, 0), z0, p(z1)))
COND2(false, z0, z1) → c2(COND1(gr(z0, 0), p(z0), z1))
K tuples:none
Defined Rule Symbols:

gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c1, c2

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

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

GR(s(z0), s(z1)) → c5(GR(z0, z1))
We considered the (Usable) Rules:none
And the Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, z0, z1) → c(COND2(gr(z1, 0), z0, z1))
COND2(true, z0, z1) → c1(COND2(gr(z1, 0), z0, p(z1)))
COND2(false, z0, z1) → c2(COND1(gr(z0, 0), p(z0), z1))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [5]
POL(COND1(x1, x2, x3)) = [2]
POL(COND2(x1, x2, x3)) = [2]
POL(GR(x1, x2)) = [2]x2
POL(c(x1)) = x1
POL(c1(x1)) = x1
POL(c2(x1)) = x1
POL(c5(x1)) = x1
POL(false) = [3]
POL(gr(x1, x2)) = [3] + [4]x1 + [5]x2
POL(p(x1)) = [4] + [4]x1
POL(s(x1)) = [5] + x1
POL(true) = [3]

### (10) Obligation:

Complexity Dependency Tuples Problem
Rules:

gr(0, z0) → false
gr(s(z0), 0) → true
p(0) → 0
p(s(z0)) → z0
Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, z0, z1) → c(COND2(gr(z1, 0), z0, z1))
COND2(true, z0, z1) → c1(COND2(gr(z1, 0), z0, p(z1)))
COND2(false, z0, z1) → c2(COND1(gr(z0, 0), p(z0), z1))
S tuples:

COND1(true, z0, z1) → c(COND2(gr(z1, 0), z0, z1))
COND2(true, z0, z1) → c1(COND2(gr(z1, 0), z0, p(z1)))
COND2(false, z0, z1) → c2(COND1(gr(z0, 0), p(z0), z1))
K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
Defined Rule Symbols:

gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c1, c2

### (11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace COND1(true, z0, z1) → c(COND2(gr(z1, 0), z0, z1)) by

COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))

### (12) Obligation:

Complexity Dependency Tuples Problem
Rules:

gr(0, z0) → false
gr(s(z0), 0) → true
p(0) → 0
p(s(z0)) → z0
Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND2(true, z0, z1) → c1(COND2(gr(z1, 0), z0, p(z1)))
COND2(false, z0, z1) → c2(COND1(gr(z0, 0), p(z0), z1))
COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
S tuples:

COND2(true, z0, z1) → c1(COND2(gr(z1, 0), z0, p(z1)))
COND2(false, z0, z1) → c2(COND1(gr(z0, 0), p(z0), z1))
COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
Defined Rule Symbols:

gr, p

Defined Pair Symbols:

GR, COND2, COND1

Compound Symbols:

c5, c1, c2, c

### (13) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace COND2(true, z0, z1) → c1(COND2(gr(z1, 0), z0, p(z1))) by

COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0))
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0))
COND2(true, x0, 0) → c1(COND2(false, x0, p(0)))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0))))

### (14) Obligation:

Complexity Dependency Tuples Problem
Rules:

gr(0, z0) → false
gr(s(z0), 0) → true
p(0) → 0
p(s(z0)) → z0
Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND2(false, z0, z1) → c2(COND1(gr(z0, 0), p(z0), z1))
COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0))
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0))
COND2(true, x0, 0) → c1(COND2(false, x0, p(0)))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0))))
S tuples:

COND2(false, z0, z1) → c2(COND1(gr(z0, 0), p(z0), z1))
COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0))
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0))
COND2(true, x0, 0) → c1(COND2(false, x0, p(0)))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0))))
K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
Defined Rule Symbols:

gr, p

Defined Pair Symbols:

GR, COND2, COND1

Compound Symbols:

c5, c2, c, c1

### (15) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

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

COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0))
We considered the (Usable) Rules:

p(s(z0)) → z0
p(0) → 0
And the Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND2(false, z0, z1) → c2(COND1(gr(z0, 0), p(z0), z1))
COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0))
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0))
COND2(true, x0, 0) → c1(COND2(false, x0, p(0)))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0))))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(COND1(x1, x2, x3)) = [4]x3
POL(COND2(x1, x2, x3)) = [4]x3
POL(GR(x1, x2)) = [3]x1
POL(c(x1)) = x1
POL(c1(x1)) = x1
POL(c2(x1)) = x1
POL(c5(x1)) = x1
POL(false) = [2]
POL(gr(x1, x2)) = 0
POL(p(x1)) = x1
POL(s(x1)) = [4] + x1
POL(true) = 0

### (16) Obligation:

Complexity Dependency Tuples Problem
Rules:

gr(0, z0) → false
gr(s(z0), 0) → true
p(0) → 0
p(s(z0)) → z0
Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND2(false, z0, z1) → c2(COND1(gr(z0, 0), p(z0), z1))
COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0))
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0))
COND2(true, x0, 0) → c1(COND2(false, x0, p(0)))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0))))
S tuples:

COND2(false, z0, z1) → c2(COND1(gr(z0, 0), p(z0), z1))
COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0))
COND2(true, x0, 0) → c1(COND2(false, x0, p(0)))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0))))
K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0))
Defined Rule Symbols:

gr, p

Defined Pair Symbols:

GR, COND2, COND1

Compound Symbols:

c5, c2, c, c1

### (17) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^3))) transformation)

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

COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
We considered the (Usable) Rules:

p(s(z0)) → z0
gr(s(z0), 0) → true
p(0) → 0
gr(0, z0) → false
And the Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND2(false, z0, z1) → c2(COND1(gr(z0, 0), p(z0), z1))
COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0))
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0))
COND2(true, x0, 0) → c1(COND2(false, x0, p(0)))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0))))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(COND1(x1, x2, x3)) = x3 + x32 + x2·x32
POL(COND2(x1, x2, x3)) = x32 + x1·x3 + x2·x32 + x1·x2·x3
POL(GR(x1, x2)) = x1·x2
POL(c(x1)) = x1
POL(c1(x1)) = x1
POL(c2(x1)) = x1
POL(c5(x1)) = x1
POL(false) = [1]
POL(gr(x1, x2)) = [1]
POL(p(x1)) = x1
POL(s(x1)) = [1] + x1
POL(true) = 0

### (18) Obligation:

Complexity Dependency Tuples Problem
Rules:

gr(0, z0) → false
gr(s(z0), 0) → true
p(0) → 0
p(s(z0)) → z0
Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND2(false, z0, z1) → c2(COND1(gr(z0, 0), p(z0), z1))
COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0))
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0))
COND2(true, x0, 0) → c1(COND2(false, x0, p(0)))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0))))
S tuples:

COND2(false, z0, z1) → c2(COND1(gr(z0, 0), p(z0), z1))
COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0))
COND2(true, x0, 0) → c1(COND2(false, x0, p(0)))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0))))
K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
Defined Rule Symbols:

gr, p

Defined Pair Symbols:

GR, COND2, COND1

Compound Symbols:

c5, c2, c, c1

### (19) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace COND2(false, z0, z1) → c2(COND1(gr(z0, 0), p(z0), z1)) by

COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(false, 0, x1) → c2(COND1(false, p(0), x1))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))

### (20) Obligation:

Complexity Dependency Tuples Problem
Rules:

gr(0, z0) → false
gr(s(z0), 0) → true
p(0) → 0
p(s(z0)) → z0
Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0))
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0))
COND2(true, x0, 0) → c1(COND2(false, x0, p(0)))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0))))
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(false, 0, x1) → c2(COND1(false, p(0), x1))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0))
COND2(true, x0, 0) → c1(COND2(false, x0, p(0)))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0))))
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(false, 0, x1) → c2(COND1(false, p(0), x1))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
Defined Rule Symbols:

gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c1, c2

### (21) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

COND2(false, 0, x1) → c2(COND1(false, p(0), x1))

### (22) Obligation:

Complexity Dependency Tuples Problem
Rules:

gr(0, z0) → false
gr(s(z0), 0) → true
p(0) → 0
p(s(z0)) → z0
Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0))
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0))
COND2(true, x0, 0) → c1(COND2(false, x0, p(0)))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0))))
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0))
COND2(true, x0, 0) → c1(COND2(false, x0, p(0)))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0))))
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
Defined Rule Symbols:

gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c1, c2

### (23) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

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

COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
We considered the (Usable) Rules:

p(s(z0)) → z0
And the Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0))
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0))
COND2(true, x0, 0) → c1(COND2(false, x0, p(0)))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0))))
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(COND1(x1, x2, x3)) = x2
POL(COND2(x1, x2, x3)) = x2
POL(GR(x1, x2)) = [2]x1
POL(c(x1)) = x1
POL(c1(x1)) = x1
POL(c2(x1)) = x1
POL(c5(x1)) = x1
POL(false) = 0
POL(gr(x1, x2)) = 0
POL(p(x1)) = x1
POL(s(x1)) = [4] + x1
POL(true) = 0

### (24) Obligation:

Complexity Dependency Tuples Problem
Rules:

gr(0, z0) → false
gr(s(z0), 0) → true
p(0) → 0
p(s(z0)) → z0
Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0))
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0))
COND2(true, x0, 0) → c1(COND2(false, x0, p(0)))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0))))
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0))
COND2(true, x0, 0) → c1(COND2(false, x0, p(0)))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0))))
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
Defined Rule Symbols:

gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c1, c2

### (25) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

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

COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1))
We considered the (Usable) Rules:

gr(s(z0), 0) → true
gr(0, z0) → false
And the Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0))
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0))
COND2(true, x0, 0) → c1(COND2(false, x0, p(0)))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0))))
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(COND1(x1, x2, x3)) = [2]x1
POL(COND2(x1, x2, x3)) = [4]
POL(GR(x1, x2)) = 0
POL(c(x1)) = x1
POL(c1(x1)) = x1
POL(c2(x1)) = x1
POL(c5(x1)) = x1
POL(false) = 0
POL(gr(x1, x2)) = [2]x1
POL(p(x1)) = 0
POL(s(x1)) = [1]
POL(true) = [2]

### (26) Obligation:

Complexity Dependency Tuples Problem
Rules:

gr(0, z0) → false
gr(s(z0), 0) → true
p(0) → 0
p(s(z0)) → z0
Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0))
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0))
COND2(true, x0, 0) → c1(COND2(false, x0, p(0)))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0))))
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0))
COND2(true, x0, 0) → c1(COND2(false, x0, p(0)))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0))))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1))
Defined Rule Symbols:

gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c1, c2

### (27) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0)) by

COND2(true, x0, 0) → c1(COND2(false, x0, 0))

### (28) Obligation:

Complexity Dependency Tuples Problem
Rules:

gr(0, z0) → false
gr(s(z0), 0) → true
p(0) → 0
p(s(z0)) → z0
Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0))
COND2(true, x0, 0) → c1(COND2(false, x0, p(0)))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0))))
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
COND2(true, x0, 0) → c1(COND2(false, x0, 0))
S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND2(true, x0, 0) → c1(COND2(false, x0, p(0)))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0))))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
COND2(true, x0, 0) → c1(COND2(false, x0, 0))
K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1))
Defined Rule Symbols:

gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c1, c2

### (29) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0)) by

COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))

### (30) Obligation:

Complexity Dependency Tuples Problem
Rules:

gr(0, z0) → false
gr(s(z0), 0) → true
p(0) → 0
p(s(z0)) → z0
Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(true, x0, 0) → c1(COND2(false, x0, p(0)))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0))))
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
COND2(true, x0, 0) → c1(COND2(false, x0, 0))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))
S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND2(true, x0, 0) → c1(COND2(false, x0, p(0)))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0))))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
COND2(true, x0, 0) → c1(COND2(false, x0, 0))
K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1))
Defined Rule Symbols:

gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c1, c2

### (31) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace COND2(true, x0, 0) → c1(COND2(false, x0, p(0))) by

COND2(true, x0, 0) → c1(COND2(false, x0, 0))

### (32) Obligation:

Complexity Dependency Tuples Problem
Rules:

gr(0, z0) → false
gr(s(z0), 0) → true
p(0) → 0
p(s(z0)) → z0
Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0))))
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
COND2(true, x0, 0) → c1(COND2(false, x0, 0))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))
S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0))))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
COND2(true, x0, 0) → c1(COND2(false, x0, 0))
K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1))
Defined Rule Symbols:

gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c1, c2

### (33) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

p(0) → 0

### (34) Obligation:

Complexity Dependency Tuples Problem
Rules:

p(s(z0)) → z0
gr(0, z0) → false
gr(s(z0), 0) → true
Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0))))
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
COND2(true, x0, 0) → c1(COND2(false, x0, 0))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))
S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0))))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
COND2(true, x0, 0) → c1(COND2(false, x0, 0))
K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1))
Defined Rule Symbols:

p, gr

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c1, c2

### (35) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0)))) by

COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))

### (36) Obligation:

Complexity Dependency Tuples Problem
Rules:

p(s(z0)) → z0
gr(0, z0) → false
gr(s(z0), 0) → true
Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
COND2(true, x0, 0) → c1(COND2(false, x0, 0))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))
S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
COND2(true, x0, 0) → c1(COND2(false, x0, 0))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))
K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1))
Defined Rule Symbols:

p, gr

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c2, c1

### (37) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

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

COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))
We considered the (Usable) Rules:none
And the Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
COND2(true, x0, 0) → c1(COND2(false, x0, 0))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(COND1(x1, x2, x3)) = [4]x3
POL(COND2(x1, x2, x3)) = [4]x3
POL(GR(x1, x2)) = [4]x1
POL(c(x1)) = x1
POL(c1(x1)) = x1
POL(c2(x1)) = x1
POL(c5(x1)) = x1
POL(false) = 0
POL(gr(x1, x2)) = 0
POL(p(x1)) = 0
POL(s(x1)) = [2] + x1
POL(true) = 0

### (38) Obligation:

Complexity Dependency Tuples Problem
Rules:

p(s(z0)) → z0
gr(0, z0) → false
gr(s(z0), 0) → true
Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
COND2(true, x0, 0) → c1(COND2(false, x0, 0))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))
S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
COND2(true, x0, 0) → c1(COND2(false, x0, 0))
K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))
Defined Rule Symbols:

p, gr

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c2, c1

### (39) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

The following tuples could be moved from S to K by knowledge propagation:

COND2(true, x0, 0) → c1(COND2(false, x0, 0))
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))

### (40) Obligation:

Complexity Dependency Tuples Problem
Rules:

p(s(z0)) → z0
gr(0, z0) → false
gr(s(z0), 0) → true
Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
COND2(true, x0, 0) → c1(COND2(false, x0, 0))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))
S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))
COND2(true, x0, 0) → c1(COND2(false, x0, 0))
Defined Rule Symbols:

p, gr

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c2, c1

### (41) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) by

COND2(false, 0, x0) → c2(COND1(false, 0, x0))

### (42) Obligation:

Complexity Dependency Tuples Problem
Rules:

p(s(z0)) → z0
gr(0, z0) → false
gr(s(z0), 0) → true
Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
COND2(true, x0, 0) → c1(COND2(false, x0, 0))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))
COND2(false, 0, x0) → c2(COND1(false, 0, x0))
S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))
COND2(true, x0, 0) → c1(COND2(false, x0, 0))
Defined Rule Symbols:

p, gr

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c2, c1

### (43) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

COND2(false, 0, x0) → c2(COND1(false, 0, x0))

### (44) Obligation:

Complexity Dependency Tuples Problem
Rules:

p(s(z0)) → z0
gr(0, z0) → false
gr(s(z0), 0) → true
Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
COND2(true, x0, 0) → c1(COND2(false, x0, 0))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))
S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))
COND2(true, x0, 0) → c1(COND2(false, x0, 0))
Defined Rule Symbols:

p, gr

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c2, c1

### (45) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

gr(0, z0) → false

### (46) Obligation:

Complexity Dependency Tuples Problem
Rules:

gr(s(z0), 0) → true
p(s(z0)) → z0
Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
COND2(true, x0, 0) → c1(COND2(false, x0, 0))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))
S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))
COND2(true, x0, 0) → c1(COND2(false, x0, 0))
Defined Rule Symbols:

gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c2, c1

### (47) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) by

COND2(false, s(z0), x1) → c2(COND1(true, z0, x1))

### (48) Obligation:

Complexity Dependency Tuples Problem
Rules:

gr(s(z0), 0) → true
p(s(z0)) → z0
Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
COND2(true, x0, 0) → c1(COND2(false, x0, 0))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))
COND2(false, s(z0), x1) → c2(COND1(true, z0, x1))
S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))
COND2(true, x0, 0) → c1(COND2(false, x0, 0))
Defined Rule Symbols:

gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c2, c1

### (49) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

gr(s(z0), 0) → true

### (50) Obligation:

Complexity Dependency Tuples Problem
Rules:

p(s(z0)) → z0
Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
COND2(true, x0, 0) → c1(COND2(false, x0, 0))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))
COND2(false, s(z0), x1) → c2(COND1(true, z0, x1))
S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))
K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))
COND2(true, x0, 0) → c1(COND2(false, x0, 0))
Defined Rule Symbols:

p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c2, c1

### (51) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) by

COND2(false, s(z0), x1) → c2(COND1(true, z0, x1))

### (52) Obligation:

Complexity Dependency Tuples Problem
Rules:

p(s(z0)) → z0
Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(true, x0, 0) → c1(COND2(false, x0, 0))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))
COND2(false, s(z0), x1) → c2(COND1(true, z0, x1))
S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND2(false, s(z0), x1) → c2(COND1(true, z0, x1))
K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))
COND2(true, x0, 0) → c1(COND2(false, x0, 0))
Defined Rule Symbols:

p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c1, c2

### (53) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

p(s(z0)) → z0

### (54) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(true, x0, 0) → c1(COND2(false, x0, 0))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))
COND2(false, s(z0), x1) → c2(COND1(true, z0, x1))
S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND2(false, s(z0), x1) → c2(COND1(true, z0, x1))
K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))
COND2(true, x0, 0) → c1(COND2(false, x0, 0))
Defined Rule Symbols:none

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c1, c2

### (55) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

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

COND2(false, s(z0), x1) → c2(COND1(true, z0, x1))
We considered the (Usable) Rules:none
And the Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(true, x0, 0) → c1(COND2(false, x0, 0))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))
COND2(false, s(z0), x1) → c2(COND1(true, z0, x1))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(COND1(x1, x2, x3)) = x2
POL(COND2(x1, x2, x3)) = x2
POL(GR(x1, x2)) = 0
POL(c(x1)) = x1
POL(c1(x1)) = x1
POL(c2(x1)) = x1
POL(c5(x1)) = x1
POL(false) = [3]
POL(s(x1)) = [1] + x1
POL(true) = [4]

### (56) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(true, x0, 0) → c1(COND2(false, x0, 0))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))
COND2(false, s(z0), x1) → c2(COND1(true, z0, x1))
S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0))
K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1))
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))
COND2(true, x0, 0) → c1(COND2(false, x0, 0))
COND2(false, s(z0), x1) → c2(COND1(true, z0, x1))
Defined Rule Symbols:none

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c1, c2

### (57) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

COND1(true, x0, 0) → c(COND2(false, x0, 0))
COND2(false, s(z0), x1) → c2(COND1(true, z0, x1))
Now S is empty