120.68/59.13 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml

120.68/59.13

120.68/59.13
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^2)).

0 CpxTRS

120.68/59.13

↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))

120.68/59.13

↳2 CdtProblem

120.68/59.13

↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))

120.68/59.13

↳4 CdtProblem

120.68/59.13

↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

120.68/59.13

↳6 CdtProblem

120.68/59.13

↳7 CdtNarrowingProof (BOTH BOUNDS(ID, ID))

120.68/59.13

↳8 CdtProblem

120.68/59.13

↳9 CdtNarrowingProof (BOTH BOUNDS(ID, ID))

120.68/59.13

↳10 CdtProblem

120.68/59.13

↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

120.68/59.13

↳12 CdtProblem

120.68/59.13

↳13 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))

120.68/59.13

↳14 CdtProblem

120.68/59.13

↳15 CdtNarrowingProof (BOTH BOUNDS(ID, ID))

120.68/59.13

↳16 CdtProblem

120.68/59.13

↳17 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))

120.68/59.13

↳18 CdtProblem

120.68/59.13

↳19 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))

120.68/59.13

↳20 CdtProblem

120.68/59.13

↳21 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

120.68/59.13

↳22 CdtProblem

120.68/59.13

↳23 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

120.68/59.13

↳24 CdtProblem

120.68/59.13

↳25 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

120.68/59.13

↳26 CdtProblem

120.68/59.13

↳27 CdtNarrowingProof (BOTH BOUNDS(ID, ID))

120.68/59.13

↳28 CdtProblem

120.68/59.13

↳29 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))

120.68/59.13

↳30 CdtProblem

120.68/59.13

↳31 CdtNarrowingProof (BOTH BOUNDS(ID, ID))

120.68/59.13

↳32 CdtProblem

120.68/59.13

↳33 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))

120.68/59.13

↳34 CdtProblem

120.68/59.13

↳35 CdtNarrowingProof (BOTH BOUNDS(ID, ID))

120.68/59.13

↳36 CdtProblem

120.68/59.13

↳37 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))

120.68/59.13

↳38 CdtProblem

120.68/59.13

↳39 CdtNarrowingProof (BOTH BOUNDS(ID, ID))

120.68/59.13

↳40 CdtProblem

120.68/59.13

↳41 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))

120.68/59.13

↳42 CdtProblem

120.68/59.13

↳43 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

120.68/59.13

↳44 CdtProblem

120.68/59.13

↳45 CdtKnowledgeProof (BOTH BOUNDS(ID, ID))

120.68/59.13

↳46 CdtProblem

120.68/59.13

↳47 CdtNarrowingProof (BOTH BOUNDS(ID, ID))

120.68/59.13

↳48 CdtProblem

120.68/59.13

↳49 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))

120.68/59.13

↳50 CdtProblem

120.68/59.13

↳51 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))

120.68/59.13

↳52 CdtProblem

120.68/59.13

↳53 CdtNarrowingProof (BOTH BOUNDS(ID, ID))

120.68/59.13

↳54 CdtProblem

120.68/59.13

↳55 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))

120.68/59.13

↳56 CdtProblem

120.68/59.13

↳57 CdtNarrowingProof (BOTH BOUNDS(ID, ID))

120.68/59.13

↳58 CdtProblem

120.68/59.13

↳59 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))

120.68/59.13

↳60 CdtProblem

120.68/59.13

↳61 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

120.68/59.13

↳62 CdtProblem

120.68/59.13

↳63 CdtKnowledgeProof (⇔)

120.68/59.13

↳64 BOUNDS(O(1), O(1))

120.68/59.13

120.68/59.13 120.68/59.13

120.68/59.13

(0) Obligation:

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

cond1(true, x, y) → cond2(gr(y, 0), x, y) 120.68/59.13
cond2(true, x, y) → cond2(gr(y, 0), x, p(y)) 120.68/59.14
cond2(false, x, y) → cond1(gr(x, 0), p(x), y) 120.68/59.14
gr(0, x) → false 120.68/59.14
gr(s(x), 0) → true 120.68/59.14
gr(s(x), s(y)) → gr(x, y) 120.68/59.14
p(0) → 0 120.68/59.14
p(s(x)) → x

Rewrite Strategy: INNERMOST

120.68/59.14

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

Converted CpxTRS to CDT

120.68/59.14

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

COND1(true, z0, z1) → c(COND2(gr(z1, 0), z0, z1), GR(z1, 0)) 120.68/59.14
COND2(true, z0, z1) → c1(COND2(gr(z1, 0), z0, p(z1)), GR(z1, 0), P(z1)) 120.68/59.14
COND2(false, z0, z1) → c2(COND1(gr(z0, 0), p(z0), z1), GR(z0, 0), P(z0)) 120.68/59.14
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)) 120.68/59.14
COND2(true, z0, z1) → c1(COND2(gr(z1, 0), z0, p(z1)), GR(z1, 0), P(z1)) 120.68/59.14
COND2(false, z0, z1) → c2(COND1(gr(z0, 0), p(z0), z1), GR(z0, 0), P(z0)) 120.68/59.14
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

120.68/59.16

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

Removed 5 trailing tuple parts

120.68/59.16

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 120.68/59.16
COND1(true, z0, z1) → c(COND2(gr(z1, 0), z0, z1)) 120.68/59.16
COND2(true, z0, z1) → c1(COND2(gr(z1, 0), z0, p(z1))) 120.68/59.16
COND2(false, z0, z1) → c2(COND1(gr(z0, 0), p(z0), z1))

S tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 120.68/59.16
COND1(true, z0, z1) → c(COND2(gr(z1, 0), z0, z1)) 120.68/59.16
COND2(true, z0, z1) → c1(COND2(gr(z1, 0), z0, p(z1))) 120.68/59.16
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

120.68/59.16

(5) CdtPolyRedPairProof (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:

gr(0, z0) → false 120.68/59.16
gr(s(z0), 0) → true 120.68/59.16
p(0) → 0 120.68/59.16
p(s(z0)) → z0

And the Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 120.68/59.16
COND1(true, z0, z1) → c(COND2(gr(z1, 0), z0, z1)) 120.68/59.16
COND2(true, z0, z1) → c1(COND2(gr(z1, 0), z0, p(z1))) 120.68/59.16
COND2(false, z0, z1) → c2(COND1(gr(z0, 0), p(z0), z1))

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

POL(0) = [2] 120.68/59.16
POL(COND1(x₁, x₂, x₃)) = 0 120.68/59.16
POL(COND2(x₁, x₂, x₃)) = 0 120.68/59.16
POL(GR(x₁, x₂)) = [2]x₂ 120.68/59.16
POL(c(x₁)) = x₁ 120.68/59.16
POL(c1(x₁)) = x₁ 120.68/59.16
POL(c2(x₁)) = x₁ 120.68/59.16
POL(c5(x₁)) = x₁ 120.68/59.16
POL(false) = [4] 120.68/59.16
POL(gr(x₁, x₂)) = [5]x₁ 120.68/59.16
POL(p(x₁)) = 0 120.68/59.16
POL(s(x₁)) = [2] + x₁ 120.68/59.16
POL(true) = [4]

120.68/59.16

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 120.68/59.16
COND1(true, z0, z1) → c(COND2(gr(z1, 0), z0, z1)) 120.68/59.16
COND2(true, z0, z1) → c1(COND2(gr(z1, 0), z0, p(z1))) 120.68/59.16
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)) 120.68/59.16
COND2(true, z0, z1) → c1(COND2(gr(z1, 0), z0, p(z1))) 120.68/59.16
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:

cond1, cond2, gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c1, c2

120.68/59.16

(7) 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)) 120.68/59.16
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))

120.68/59.16

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 120.68/59.16
COND2(true, z0, z1) → c1(COND2(gr(z1, 0), z0, p(z1))) 120.68/59.16
COND2(false, z0, z1) → c2(COND1(gr(z0, 0), p(z0), z1)) 120.68/59.16
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 120.68/59.16
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))) 120.68/59.16
COND2(false, z0, z1) → c2(COND1(gr(z0, 0), p(z0), z1)) 120.68/59.16
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 120.68/59.16
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:

cond1, cond2, gr, p

Defined Pair Symbols:

GR, COND2, COND1

Compound Symbols:

c5, c1, c2, c

120.68/59.16

(9) 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)) 120.68/59.16
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, p(0))) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0))))

121.02/59.22

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND2(false, z0, z1) → c2(COND1(gr(z0, 0), p(z0), z1)) 121.02/59.22
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, p(0))) 121.02/59.22
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)) 121.02/59.22
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, p(0))) 121.02/59.22
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:

cond1, cond2, gr, p

Defined Pair Symbols:

GR, COND2, COND1

Compound Symbols:

c5, c2, c, c1

121.02/59.22

(11) CdtPolyRedPairProof (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 121.02/59.22
p(0) → 0 121.02/59.22
gr(s(z0), 0) → true 121.02/59.22
gr(0, z0) → false

And the Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND2(false, z0, z1) → c2(COND1(gr(z0, 0), p(z0), z1)) 121.02/59.22
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, p(0))) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0))))

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

POL(0) = 0 121.02/59.22
POL(COND1(x₁, x₂, x₃)) = x₃ 121.02/59.22
POL(COND2(x₁, x₂, x₃)) = x₃ 121.02/59.22
POL(GR(x₁, x₂)) = [5]x₁ + [5]x₂ 121.02/59.22
POL(c(x₁)) = x₁ 121.02/59.22
POL(c1(x₁)) = x₁ 121.02/59.22
POL(c2(x₁)) = x₁ 121.02/59.22
POL(c5(x₁)) = x₁ 121.02/59.22
POL(false) = 0 121.02/59.22
POL(gr(x₁, x₂)) = 0 121.02/59.22
POL(p(x₁)) = x₁ 121.02/59.22
POL(s(x₁)) = [4] + x₁ 121.02/59.22
POL(true) = 0

121.02/59.22

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND2(false, z0, z1) → c2(COND1(gr(z0, 0), p(z0), z1)) 121.02/59.22
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, p(0))) 121.02/59.22
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)) 121.02/59.22
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, p(0))) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0))))

K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0))

Defined Rule Symbols:

cond1, cond2, gr, p

Defined Pair Symbols:

GR, COND2, COND1

Compound Symbols:

c5, c2, c, c1

121.02/59.22

(13) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) 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 121.02/59.22
p(0) → 0 121.02/59.22
gr(s(z0), 0) → true 121.02/59.22
gr(0, z0) → false

And the Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND2(false, z0, z1) → c2(COND1(gr(z0, 0), p(z0), z1)) 121.02/59.22
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, p(0))) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0))))

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

POL(0) = 0 121.02/59.22
POL(COND1(x₁, x₂, x₃)) = [2]x₃ + x₃² 121.02/59.22
POL(COND2(x₁, x₂, x₃)) = x₃ + x₃² + x₁·x₃ 121.02/59.22
POL(GR(x₁, x₂)) = x₁ + x₂ 121.02/59.22
POL(c(x₁)) = x₁ 121.02/59.22
POL(c1(x₁)) = x₁ 121.02/59.22
POL(c2(x₁)) = x₁ 121.02/59.22
POL(c5(x₁)) = x₁ 121.02/59.22
POL(false) = [1] 121.02/59.22
POL(gr(x₁, x₂)) = [2] 121.02/59.22
POL(p(x₁)) = x₁ 121.02/59.22
POL(s(x₁)) = [2] + x₁ 121.02/59.22
POL(true) = 0

121.02/59.22

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND2(false, z0, z1) → c2(COND1(gr(z0, 0), p(z0), z1)) 121.02/59.22
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, p(0))) 121.02/59.22
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)) 121.02/59.22
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, p(0))) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0))))

K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))

Defined Rule Symbols:

cond1, cond2, gr, p

Defined Pair Symbols:

GR, COND2, COND1

Compound Symbols:

c5, c2, c, c1

121.02/59.22

(15) 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)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.22
COND2(false, 0, x1) → c2(COND1(false, p(0), x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))

121.02/59.22

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, p(0))) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0)))) 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.22
COND2(false, 0, x1) → c2(COND1(false, p(0), x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))

S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, p(0))) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0)))) 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.22
COND2(false, 0, x1) → c2(COND1(false, p(0), x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))

K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))

Defined Rule Symbols:

cond1, cond2, gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c1, c2

121.02/59.22

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

Removed 1 trailing tuple parts

121.02/59.22

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, p(0))) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0)))) 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.22
COND2(false, 0, x1) → c2

S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, p(0))) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0)))) 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.22
COND2(false, 0, x1) → c2

K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))

Defined Rule Symbols:

cond1, cond2, gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c1, c2, c2

121.02/59.22

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

Removed 1 trailing nodes:

COND2(false, 0, x1) → c2

121.02/59.22

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, p(0))) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0)))) 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.22
COND2(false, 0, x1) → c2

S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, p(0))) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0)))) 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.22
COND2(false, 0, x1) → c2

K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0)))

Defined Rule Symbols:

cond1, cond2, gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c1, c2, c2

121.02/59.22

(21) CdtPolyRedPairProof (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

We considered the (Usable) Rules:

p(s(z0)) → z0 121.02/59.22
p(0) → 0 121.02/59.22
gr(s(z0), 0) → true 121.02/59.22
gr(0, z0) → false

And the Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, p(0))) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0)))) 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.22
COND2(false, 0, x1) → c2

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

POL(0) = [2] 121.02/59.22
POL(COND1(x₁, x₂, x₃)) = [2] 121.02/59.22
POL(COND2(x₁, x₂, x₃)) = [2] 121.02/59.22
POL(GR(x₁, x₂)) = 0 121.02/59.22
POL(c(x₁)) = x₁ 121.02/59.22
POL(c1(x₁)) = x₁ 121.02/59.22
POL(c2) = 0 121.02/59.22
POL(c2(x₁)) = x₁ 121.02/59.22
POL(c5(x₁)) = x₁ 121.02/59.22
POL(false) = [4] 121.02/59.22
POL(gr(x₁, x₂)) = [4]x₁ + [3]x₂ 121.02/59.22
POL(p(x₁)) = [4] 121.02/59.22
POL(s(x₁)) = 0 121.02/59.22
POL(true) = 0

121.02/59.22

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, p(0))) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0)))) 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.22
COND2(false, 0, x1) → c2

S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, p(0))) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0)))) 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))

K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(false, 0, x1) → c2

Defined Rule Symbols:

cond1, cond2, gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c1, c2, c2

121.02/59.22

(23) CdtPolyRedPairProof (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:

p(s(z0)) → z0 121.02/59.22
p(0) → 0 121.02/59.22
gr(s(z0), 0) → true 121.02/59.22
gr(0, z0) → false

And the Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, p(0))) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0)))) 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.22
COND2(false, 0, x1) → c2

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

POL(0) = 0 121.02/59.22
POL(COND1(x₁, x₂, x₃)) = [2]x₁ 121.02/59.22
POL(COND2(x₁, x₂, x₃)) = [4] 121.02/59.22
POL(GR(x₁, x₂)) = 0 121.02/59.22
POL(c(x₁)) = x₁ 121.02/59.22
POL(c1(x₁)) = x₁ 121.02/59.22
POL(c2) = 0 121.02/59.22
POL(c2(x₁)) = x₁ 121.02/59.22
POL(c5(x₁)) = x₁ 121.02/59.22
POL(false) = 0 121.02/59.22
POL(gr(x₁, x₂)) = [2]x₁ 121.02/59.22
POL(p(x₁)) = 0 121.02/59.22
POL(s(x₁)) = [1] 121.02/59.22
POL(true) = [2]

121.02/59.22

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, p(0))) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0)))) 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.22
COND2(false, 0, x1) → c2

S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, p(0))) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0)))) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))

K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(false, 0, x1) → c2 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1))

Defined Rule Symbols:

cond1, cond2, gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c1, c2, c2

121.02/59.22

(25) CdtPolyRedPairProof (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 121.02/59.22
p(0) → 0 121.02/59.22
gr(s(z0), 0) → true 121.02/59.22
gr(0, z0) → false

And the Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, p(0))) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0)))) 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.22
COND2(false, 0, x1) → c2

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

POL(0) = 0 121.02/59.22
POL(COND1(x₁, x₂, x₃)) = [2]x₂ + [2]x₃ 121.02/59.22
POL(COND2(x₁, x₂, x₃)) = [2]x₂ + [2]x₃ 121.02/59.22
POL(GR(x₁, x₂)) = [3]x₁ + [5]x₂ 121.02/59.22
POL(c(x₁)) = x₁ 121.02/59.22
POL(c1(x₁)) = x₁ 121.02/59.22
POL(c2) = 0 121.02/59.22
POL(c2(x₁)) = x₁ 121.02/59.22
POL(c5(x₁)) = x₁ 121.02/59.22
POL(false) = 0 121.02/59.22
POL(gr(x₁, x₂)) = 0 121.02/59.22
POL(p(x₁)) = x₁ 121.02/59.22
POL(s(x₁)) = [4] + x₁ 121.02/59.22
POL(true) = 0

121.02/59.22

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, p(0))) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0)))) 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.22
COND2(false, 0, x1) → c2

S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(gr(0, 0), x0, 0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, p(0))) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0)))) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))

K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(false, 0, x1) → c2 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))

Defined Rule Symbols:

cond1, cond2, gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c1, c2, c2

121.02/59.22

(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))

121.02/59.22

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, p(0))) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0)))) 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.22
COND2(false, 0, x1) → c2 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, 0))

S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, p(0))) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0)))) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, 0))

K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(false, 0, x1) → c2 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))

Defined Rule Symbols:

cond1, cond2, gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c1, c2, c2

121.02/59.22

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

Removed 1 trailing nodes:

COND2(false, 0, x1) → c2

121.02/59.22

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, p(0))) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0)))) 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.22
COND2(false, 0, x1) → c2 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, 0))

S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, p(0))) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0)))) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, 0))

K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(false, 0, x1) → c2 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))

Defined Rule Symbols:

cond1, cond2, gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c1, c2, c2

121.02/59.22

(31) 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))

121.02/59.22

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, p(0))) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0)))) 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.22
COND2(false, 0, x1) → c2 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, 0)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))

S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, p(0))) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0)))) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, 0))

K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(gr(s(z0), 0), x0, z0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(false, 0, x1) → c2 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))

Defined Rule Symbols:

cond1, cond2, gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c1, c2, c2

121.02/59.22

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

Removed 1 trailing nodes:

COND2(false, 0, x1) → c2

121.02/59.22

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, p(0))) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0)))) 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.22
COND2(false, 0, x1) → c2 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, 0)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))

S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, p(0))) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0)))) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, 0))

K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(false, 0, x1) → c2 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))

Defined Rule Symbols:

cond1, cond2, gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c1, c2, c2

121.02/59.22

(35) 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))

121.02/59.22

(36) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0)))) 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.22
COND2(false, 0, x1) → c2 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, 0)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))

S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0)))) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, 0))

K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(false, 0, x1) → c2 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))

Defined Rule Symbols:

cond1, cond2, gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c1, c2, c2

121.02/59.22

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

Removed 1 trailing nodes:

COND2(false, 0, x1) → c2

121.02/59.22

(38) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0)))) 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.22
COND2(false, 0, x1) → c2 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, 0)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))

S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, p(s(z0)))) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, 0))

K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(false, 0, x1) → c2 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))

Defined Rule Symbols:

cond1, cond2, gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c1, c2, c2

121.02/59.22

(39) 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))

121.02/59.22

(40) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.22
COND2(false, 0, x1) → c2 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, 0)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))

S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, 0)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))

K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(false, 0, x1) → c2 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))

Defined Rule Symbols:

cond1, cond2, gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c2, c2, c1

121.02/59.22

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

Removed 1 trailing nodes:

COND2(false, 0, x1) → c2

121.02/59.22

(42) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.22
COND2(false, 0, x1) → c2 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, 0)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))

S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, 0)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))

K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(false, 0, x1) → c2 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1))

Defined Rule Symbols:

cond1, cond2, gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c2, c2, c1

121.02/59.22

(43) CdtPolyRedPairProof (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:

p(s(z0)) → z0 121.02/59.22
gr(s(z0), 0) → true 121.02/59.22
gr(0, z0) → false

And the Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.22
COND2(false, 0, x1) → c2 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, 0)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))

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

POL(0) = 0 121.02/59.22
POL(COND1(x₁, x₂, x₃)) = x₃ 121.02/59.22
POL(COND2(x₁, x₂, x₃)) = x₃ 121.02/59.22
POL(GR(x₁, x₂)) = [3]x₁ + [5]x₂ 121.02/59.22
POL(c(x₁)) = x₁ 121.02/59.22
POL(c1(x₁)) = x₁ 121.02/59.22
POL(c2) = 0 121.02/59.22
POL(c2(x₁)) = x₁ 121.02/59.22
POL(c5(x₁)) = x₁ 121.02/59.22
POL(false) = 0 121.02/59.22
POL(gr(x₁, x₂)) = 0 121.02/59.22
POL(p(x₁)) = [1] 121.02/59.22
POL(s(x₁)) = [1] + x₁ 121.02/59.22
POL(true) = 0

121.02/59.22

(44) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.22
COND2(false, 0, x1) → c2 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, 0)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))

S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, 0))

K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.22
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.22
COND2(false, 0, x1) → c2 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.22
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))

Defined Rule Symbols:

cond1, cond2, gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c2, c2, c1

121.02/59.22

(45) 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)) 121.02/59.22
COND2(true, x0, 0) → c1(COND2(false, x0, 0)) 121.02/59.22
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.22
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.22
COND2(false, 0, x1) → c2

121.02/59.22

(46) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond1(true, z0, z1) → cond2(gr(z1, 0), z0, z1) 121.02/59.22
cond2(true, z0, z1) → cond2(gr(z1, 0), z0, p(z1)) 121.02/59.22
cond2(false, z0, z1) → cond1(gr(z0, 0), p(z0), z1) 121.02/59.22
gr(0, z0) → false 121.02/59.23
gr(s(z0), 0) → true 121.02/59.23
gr(s(z0), s(z1)) → gr(z0, z1) 121.02/59.23
p(0) → 0 121.02/59.23
p(s(z0)) → z0

Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.23
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.23
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.23
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.23
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.23
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.23
COND2(false, 0, x1) → c2 121.02/59.23
COND2(true, x0, 0) → c1(COND2(false, x0, 0)) 121.02/59.23
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))

S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.23
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))

K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.23
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.23
COND2(false, 0, x1) → c2 121.02/59.23
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.23
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.23
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0)) 121.02/59.23
COND2(true, x0, 0) → c1(COND2(false, x0, 0))

Defined Rule Symbols:

cond1, cond2, gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c2, c2, c1

121.02/59.23

(47) 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))

121.02/59.23

(48) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.23
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.23
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.23
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.23
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.23
COND2(false, 0, x1) → c2 121.02/59.23
COND2(true, x0, 0) → c1(COND2(false, x0, 0)) 121.02/59.23
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0)) 121.02/59.23
COND2(false, 0, x0) → c2(COND1(false, 0, x0))

S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.23
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))

K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.23
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.23
COND2(false, 0, x1) → c2 121.02/59.23
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.23
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.23
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0)) 121.02/59.23
COND2(true, x0, 0) → c1(COND2(false, x0, 0))

Defined Rule Symbols:

cond1, cond2, gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c2, c2, c1

121.02/59.23

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

Removed 1 trailing tuple parts

121.02/59.23

(50) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.23
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.23
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.23
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.23
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.23
COND2(false, 0, x1) → c2 121.02/59.23
COND2(true, x0, 0) → c1(COND2(false, x0, 0)) 121.02/59.23
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))

S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.23
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))

K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.23
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.23
COND2(false, 0, x1) → c2 121.02/59.23
COND2(false, 0, x1) → c2(COND1(gr(0, 0), 0, x1)) 121.02/59.23
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.23
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0)) 121.02/59.23
COND2(true, x0, 0) → c1(COND2(false, x0, 0))

Defined Rule Symbols:

cond1, cond2, gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c2, c2, c1

121.02/59.23

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

Removed 1 trailing nodes:

COND2(false, 0, x0) → c2

121.02/59.23

(52) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.23
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.23
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.23
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.23
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.23
COND2(false, 0, x1) → c2 121.02/59.23
COND2(true, x0, 0) → c1(COND2(false, x0, 0)) 121.02/59.23
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0))

S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.23
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))

K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.23
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.23
COND2(false, 0, x1) → c2 121.02/59.23
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.23
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0)) 121.02/59.23
COND2(true, x0, 0) → c1(COND2(false, x0, 0))

Defined Rule Symbols:

cond1, cond2, gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c2, c2, c1

121.02/59.23

(53) 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))

121.02/59.23

(54) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.23
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.23
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.23
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.23
COND2(false, 0, x1) → c2 121.02/59.23
COND2(true, x0, 0) → c1(COND2(false, x0, 0)) 121.02/59.23
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0)) 121.02/59.23
COND2(false, s(z0), x1) → c2(COND1(true, z0, x1))

S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.23
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))

K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.23
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.23
COND2(false, 0, x1) → c2 121.02/59.23
COND2(false, s(z0), x1) → c2(COND1(gr(s(z0), 0), z0, x1)) 121.02/59.23
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0)) 121.02/59.23
COND2(true, x0, 0) → c1(COND2(false, x0, 0))

Defined Rule Symbols:

cond1, cond2, gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c2, c2, c1

121.02/59.23

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

Removed 1 trailing nodes:

COND2(false, 0, x0) → c2

121.02/59.23

(56) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.23
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.23
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.23
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1)) 121.02/59.23
COND2(false, 0, x1) → c2 121.02/59.23
COND2(true, x0, 0) → c1(COND2(false, x0, 0)) 121.02/59.23
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0)) 121.02/59.23
COND2(false, s(z0), x1) → c2(COND1(true, z0, x1))

S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.23
COND2(false, s(z0), x1) → c2(COND1(true, p(s(z0)), x1))

K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.23
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.23
COND2(false, 0, x1) → c2 121.02/59.23
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0)) 121.02/59.23
COND2(true, x0, 0) → c1(COND2(false, x0, 0))

Defined Rule Symbols:

cond1, cond2, gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c2, c2, c1

121.02/59.23

(57) 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))

121.02/59.23

(58) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.23
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.23
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.23
COND2(false, 0, x1) → c2 121.02/59.23
COND2(true, x0, 0) → c1(COND2(false, x0, 0)) 121.02/59.23
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0)) 121.02/59.23
COND2(false, s(z0), x1) → c2(COND1(true, z0, x1))

S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.23
COND2(false, s(z0), x1) → c2(COND1(true, z0, x1))

K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.23
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.23
COND2(false, 0, x1) → c2 121.02/59.23
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0)) 121.02/59.23
COND2(true, x0, 0) → c1(COND2(false, x0, 0))

Defined Rule Symbols:

cond1, cond2, gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c2, c1, c2

121.02/59.23

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

Removed 1 trailing nodes:

COND2(false, 0, x0) → c2

121.02/59.23

(60) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.23
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.23
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.23
COND2(false, 0, x1) → c2 121.02/59.23
COND2(true, x0, 0) → c1(COND2(false, x0, 0)) 121.02/59.23
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0)) 121.02/59.23
COND2(false, s(z0), x1) → c2(COND1(true, z0, x1))

S tuples:

COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.23
COND2(false, s(z0), x1) → c2(COND1(true, z0, x1))

K tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.23
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.23
COND2(false, 0, x1) → c2 121.02/59.23
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0)) 121.02/59.23
COND2(true, x0, 0) → c1(COND2(false, x0, 0))

Defined Rule Symbols:

cond1, cond2, gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c2, c1, c2

121.02/59.23

(61) CdtPolyRedPairProof (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)) 121.02/59.23
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.23
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.23
COND2(false, 0, x1) → c2 121.02/59.23
COND2(true, x0, 0) → c1(COND2(false, x0, 0)) 121.02/59.23
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0)) 121.02/59.23
COND2(false, s(z0), x1) → c2(COND1(true, z0, x1))

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

POL(0) = 0 121.02/59.23
POL(COND1(x₁, x₂, x₃)) = x₁ + x₂ 121.02/59.23
POL(COND2(x₁, x₂, x₃)) = x₂ 121.02/59.23
POL(GR(x₁, x₂)) = [5]x₁ + [5]x₂ 121.02/59.23
POL(c(x₁)) = x₁ 121.02/59.23
POL(c1(x₁)) = x₁ 121.02/59.23
POL(c2) = 0 121.02/59.23
POL(c2(x₁)) = x₁ 121.02/59.23
POL(c5(x₁)) = x₁ 121.02/59.23
POL(false) = [1] 121.02/59.23
POL(s(x₁)) = [1] + x₁ 121.02/59.23
POL(true) = 0

121.02/59.23

(62) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

GR(s(z0), s(z1)) → c5(GR(z0, z1)) 121.02/59.23
COND1(true, x0, 0) → c(COND2(false, x0, 0)) 121.02/59.23
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.23
COND2(false, 0, x1) → c2 121.02/59.23
COND2(true, x0, 0) → c1(COND2(false, x0, 0)) 121.02/59.23
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0)) 121.02/59.23
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)) 121.02/59.23
COND1(true, x0, s(z0)) → c(COND2(true, x0, s(z0))) 121.02/59.23
COND2(false, 0, x1) → c2 121.02/59.23
COND2(true, x0, s(z0)) → c1(COND2(true, x0, z0)) 121.02/59.23
COND2(true, x0, 0) → c1(COND2(false, x0, 0)) 121.02/59.23
COND2(false, s(z0), x1) → c2(COND1(true, z0, x1))

Defined Rule Symbols:

cond1, cond2, gr, p

Defined Pair Symbols:

GR, COND1, COND2

Compound Symbols:

c5, c, c2, c1, c2

121.02/59.23

(63) 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)) 121.02/59.23
COND2(false, 0, x1) → c2 121.02/59.23
COND2(false, 0, x0) → c2 121.02/59.23
COND2(false, s(z0), x1) → c2(COND1(true, z0, x1)) 121.02/59.23
COND2(false, s(z0), x1) → c2(COND1(true, z0, x1))

Now S is empty

121.02/59.23

(64) BOUNDS(O(1), O(1))

121.02/59.23