YES(O(1), O(n^3)) 217.99/81.97 YES(O(1), O(n^3)) 217.99/81.98 217.99/81.98 217.99/81.98 217.99/81.98 217.99/81.98 217.99/81.98 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 217.99/81.98 217.99/81.98 217.99/81.98
217.99/81.98
217.99/81.98
217.99/81.98
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^3)).

0 CpxTRS
217.99/81.98 
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳2 CdtProblem
217.99/81.98 
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳4 CdtProblem
217.99/81.98 
↳5 CdtLeafRemovalProof (ComplexityIfPolyImplication)
217.99/81.98 
↳6 CdtProblem
217.99/81.98 
↳7 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳8 CdtProblem
217.99/81.98 
↳9 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳10 CdtProblem
217.99/81.98 
↳11 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳12 CdtProblem
217.99/81.98 
↳13 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
217.99/81.98 
↳14 CdtProblem
217.99/81.98 
↳15 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳16 CdtProblem
217.99/81.98 
↳17 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳18 CdtProblem
217.99/81.98 
↳19 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳20 CdtProblem
217.99/81.98 
↳21 CdtKnowledgeProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳22 CdtProblem
217.99/81.98 
↳23 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
217.99/81.98 
↳24 CdtProblem
217.99/81.98 
↳25 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
217.99/81.98 
↳26 CdtProblem
217.99/81.98 
↳27 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳28 CdtProblem
217.99/81.98 
↳29 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳30 CdtProblem
217.99/81.98 
↳31 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
217.99/81.98 
↳32 CdtProblem
217.99/81.98 
↳33 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳34 CdtProblem
217.99/81.98 
↳35 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳36 CdtProblem
217.99/81.98 
↳37 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳38 CdtProblem
217.99/81.98 
↳39 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳40 CdtProblem
217.99/81.98 
↳41 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳42 CdtProblem
217.99/81.98 
↳43 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳44 CdtProblem
217.99/81.98 
↳45 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
217.99/81.98 
↳46 CdtProblem
217.99/81.98 
↳47 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳48 CdtProblem
217.99/81.98 
↳49 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳50 CdtProblem
217.99/81.98 
↳51 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳52 CdtProblem
217.99/81.98 
↳53 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳54 CdtProblem
217.99/81.98 
↳55 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳56 CdtProblem
217.99/81.98 
↳57 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳58 CdtProblem
217.99/81.98 
↳59 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳60 CdtProblem
217.99/81.98 
↳61 CdtInstantiationProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳62 CdtProblem
217.99/81.98 
↳63 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳64 CdtProblem
217.99/81.98 
↳65 CdtRewritingProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳66 CdtProblem
217.99/81.98 
↳67 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳68 CdtProblem
217.99/81.98 
↳69 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
217.99/81.98 
↳70 CdtProblem
217.99/81.98 
↳71 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^3))))
217.99/81.98 
↳72 CdtProblem
217.99/81.98 
↳73 CdtRewritingProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳74 CdtProblem
217.99/81.98 
↳75 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳76 CdtProblem
217.99/81.98 
↳77 CdtRewritingProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳78 CdtProblem
217.99/81.98 
↳79 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳80 CdtProblem
217.99/81.98 
↳81 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
217.99/81.98 
↳82 CdtProblem
217.99/81.98 
↳83 CdtRewritingProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳84 CdtProblem
217.99/81.98 
↳85 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳86 CdtProblem
217.99/81.98 
↳87 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
217.99/81.98 
↳88 CdtProblem
217.99/81.98 
↳89 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
217.99/81.98 
↳90 CdtProblem
217.99/81.98 
↳91 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
217.99/81.98 
↳92 CdtProblem
217.99/81.98 
↳93 SIsEmptyProof (BOTH BOUNDS(ID, ID))
217.99/81.98 
↳94 BOUNDS(O(1), O(1))
217.99/81.98
217.99/81.98 217.99/81.98
217.99/81.98
217.99/81.98

(0) Obligation:

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

half(0) → 0 217.99/81.98
half(s(0)) → 0 217.99/81.98
half(s(s(x))) → s(half(x)) 217.99/81.98
lastbit(0) → 0 217.99/81.98
lastbit(s(0)) → s(0) 217.99/81.98
lastbit(s(s(x))) → lastbit(x) 217.99/81.98
zero(0) → true 217.99/81.98
zero(s(x)) → false 217.99/81.98
conv(x) → conviter(x, cons(0, nil)) 217.99/81.98
conviter(x, l) → if(zero(x), x, l) 217.99/81.98
if(true, x, l) → l 217.99/81.98
if(false, x, l) → conviter(half(x), cons(lastbit(x), l))

Rewrite Strategy: INNERMOST
217.99/81.98
217.99/81.98

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

Converted CpxTRS to CDT
217.99/81.98
217.99/81.98

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 217.99/81.98
half(s(0)) → 0 217.99/81.98
half(s(s(z0))) → s(half(z0)) 217.99/81.98
lastbit(0) → 0 217.99/81.98
lastbit(s(0)) → s(0) 217.99/81.98
lastbit(s(s(z0))) → lastbit(z0) 217.99/81.98
zero(0) → true 217.99/81.98
zero(s(z0)) → false 217.99/81.98
conv(z0) → conviter(z0, cons(0, nil)) 217.99/81.98
conviter(z0, z1) → if(zero(z0), z0, z1) 217.99/81.98
if(true, z0, z1) → z1 217.99/81.98
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 217.99/81.98
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 217.99/81.98
CONV(z0) → c8(CONVITER(z0, cons(0, nil))) 217.99/81.98
CONVITER(z0, z1) → c9(IF(zero(z0), z0, z1), ZERO(z0)) 217.99/82.00
IF(false, z0, z1) → c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0), LASTBIT(z0))
S tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 217.99/82.00
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 217.99/82.00
CONV(z0) → c8(CONVITER(z0, cons(0, nil))) 217.99/82.00
CONVITER(z0, z1) → c9(IF(zero(z0), z0, z1), ZERO(z0)) 217.99/82.00
IF(false, z0, z1) → c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0), LASTBIT(z0))
K tuples:none
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

HALF, LASTBIT, CONV, CONVITER, IF

Compound Symbols:

c2, c5, c8, c9, c11

217.99/82.00
217.99/82.00

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

Removed 1 trailing tuple parts
217.99/82.00
217.99/82.00

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 217.99/82.00
half(s(0)) → 0 217.99/82.00
half(s(s(z0))) → s(half(z0)) 217.99/82.00
lastbit(0) → 0 217.99/82.00
lastbit(s(0)) → s(0) 217.99/82.00
lastbit(s(s(z0))) → lastbit(z0) 217.99/82.00
zero(0) → true 217.99/82.00
zero(s(z0)) → false 217.99/82.00
conv(z0) → conviter(z0, cons(0, nil)) 217.99/82.00
conviter(z0, z1) → if(zero(z0), z0, z1) 217.99/82.00
if(true, z0, z1) → z1 217.99/82.00
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 217.99/82.00
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 217.99/82.00
CONV(z0) → c8(CONVITER(z0, cons(0, nil))) 217.99/82.00
IF(false, z0, z1) → c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0), LASTBIT(z0)) 217.99/82.00
CONVITER(z0, z1) → c9(IF(zero(z0), z0, z1))
S tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 217.99/82.00
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 217.99/82.00
CONV(z0) → c8(CONVITER(z0, cons(0, nil))) 217.99/82.00
IF(false, z0, z1) → c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0), LASTBIT(z0)) 217.99/82.00
CONVITER(z0, z1) → c9(IF(zero(z0), z0, z1))
K tuples:none
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

HALF, LASTBIT, CONV, IF, CONVITER

Compound Symbols:

c2, c5, c8, c11, c9

217.99/82.00
217.99/82.00

(5) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

CONV(z0) → c8(CONVITER(z0, cons(0, nil)))
217.99/82.00
217.99/82.00

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 217.99/82.00
half(s(0)) → 0 217.99/82.00
half(s(s(z0))) → s(half(z0)) 217.99/82.00
lastbit(0) → 0 217.99/82.00
lastbit(s(0)) → s(0) 217.99/82.00
lastbit(s(s(z0))) → lastbit(z0) 217.99/82.00
zero(0) → true 217.99/82.00
zero(s(z0)) → false 217.99/82.00
conv(z0) → conviter(z0, cons(0, nil)) 217.99/82.00
conviter(z0, z1) → if(zero(z0), z0, z1) 217.99/82.00
if(true, z0, z1) → z1 217.99/82.00
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 217.99/82.00
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 217.99/82.00
IF(false, z0, z1) → c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0), LASTBIT(z0)) 217.99/82.00
CONVITER(z0, z1) → c9(IF(zero(z0), z0, z1))
S tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 217.99/82.00
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 217.99/82.00
IF(false, z0, z1) → c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0), LASTBIT(z0)) 217.99/82.00
CONVITER(z0, z1) → c9(IF(zero(z0), z0, z1))
K tuples:none
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

HALF, LASTBIT, IF, CONVITER

Compound Symbols:

c2, c5, c11, c9

218.52/82.03
218.52/82.03

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

Use narrowing to replace CONVITER(z0, z1) → c9(IF(zero(z0), z0, z1)) by

CONVITER(0, x1) → c9(IF(true, 0, x1)) 218.52/82.03
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1))
218.52/82.03
218.52/82.03

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.52/82.03
half(s(0)) → 0 218.52/82.03
half(s(s(z0))) → s(half(z0)) 218.52/82.03
lastbit(0) → 0 218.52/82.03
lastbit(s(0)) → s(0) 218.52/82.03
lastbit(s(s(z0))) → lastbit(z0) 218.52/82.03
zero(0) → true 218.52/82.03
zero(s(z0)) → false 218.52/82.03
conv(z0) → conviter(z0, cons(0, nil)) 218.52/82.03
conviter(z0, z1) → if(zero(z0), z0, z1) 218.52/82.03
if(true, z0, z1) → z1 218.52/82.03
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.03
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.03
IF(false, z0, z1) → c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0), LASTBIT(z0)) 218.52/82.03
CONVITER(0, x1) → c9(IF(true, 0, x1)) 218.52/82.03
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1))
S tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.03
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.03
IF(false, z0, z1) → c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0), LASTBIT(z0)) 218.52/82.03
CONVITER(0, x1) → c9(IF(true, 0, x1)) 218.52/82.03
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1))
K tuples:none
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

HALF, LASTBIT, IF, CONVITER

Compound Symbols:

c2, c5, c11, c9

218.52/82.03
218.52/82.03

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

Removed 1 trailing tuple parts
218.52/82.03
218.52/82.03

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.52/82.03
half(s(0)) → 0 218.52/82.03
half(s(s(z0))) → s(half(z0)) 218.52/82.03
lastbit(0) → 0 218.52/82.03
lastbit(s(0)) → s(0) 218.52/82.03
lastbit(s(s(z0))) → lastbit(z0) 218.52/82.03
zero(0) → true 218.52/82.03
zero(s(z0)) → false 218.52/82.03
conv(z0) → conviter(z0, cons(0, nil)) 218.52/82.03
conviter(z0, z1) → if(zero(z0), z0, z1) 218.52/82.03
if(true, z0, z1) → z1 218.52/82.03
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.03
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.03
IF(false, z0, z1) → c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0), LASTBIT(z0)) 218.52/82.03
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.03
CONVITER(0, x1) → c9
S tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.03
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.03
IF(false, z0, z1) → c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0), LASTBIT(z0)) 218.52/82.03
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.03
CONVITER(0, x1) → c9
K tuples:none
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

HALF, LASTBIT, IF, CONVITER

Compound Symbols:

c2, c5, c11, c9, c9

218.52/82.03
218.52/82.03

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

Removed 1 trailing nodes:

CONVITER(0, x1) → c9
218.52/82.03
218.52/82.03

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.52/82.03
half(s(0)) → 0 218.52/82.03
half(s(s(z0))) → s(half(z0)) 218.52/82.03
lastbit(0) → 0 218.52/82.03
lastbit(s(0)) → s(0) 218.52/82.03
lastbit(s(s(z0))) → lastbit(z0) 218.52/82.03
zero(0) → true 218.52/82.03
zero(s(z0)) → false 218.52/82.03
conv(z0) → conviter(z0, cons(0, nil)) 218.52/82.03
conviter(z0, z1) → if(zero(z0), z0, z1) 218.52/82.03
if(true, z0, z1) → z1 218.52/82.03
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.03
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.03
IF(false, z0, z1) → c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0), LASTBIT(z0)) 218.52/82.03
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.03
CONVITER(0, x1) → c9
S tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.03
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.03
IF(false, z0, z1) → c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0), LASTBIT(z0)) 218.52/82.03
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.03
CONVITER(0, x1) → c9
K tuples:none
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

HALF, LASTBIT, IF, CONVITER

Compound Symbols:

c2, c5, c11, c9, c9

218.52/82.03
218.52/82.03

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

CONVITER(0, x1) → c9
We considered the (Usable) Rules:

half(0) → 0 218.52/82.03
half(s(0)) → 0 218.52/82.03
half(s(s(z0))) → s(half(z0)) 218.52/82.03
lastbit(0) → 0 218.52/82.03
lastbit(s(0)) → s(0) 218.52/82.03
lastbit(s(s(z0))) → lastbit(z0)
And the Tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.03
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.03
IF(false, z0, z1) → c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0), LASTBIT(z0)) 218.52/82.03
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.03
CONVITER(0, x1) → c9
The order we found is given by the following interpretation:
Polynomial interpretation : 218.52/82.03

POL(0) = 0    218.52/82.03
POL(CONVITER(x1, x2)) = [1] + x2    218.52/82.03
POL(HALF(x1)) = 0    218.52/82.03
POL(IF(x1, x2, x3)) = x1 + x3    218.52/82.03
POL(LASTBIT(x1)) = 0    218.52/82.03
POL(c11(x1, x2, x3)) = x1 + x2 + x3    218.52/82.03
POL(c2(x1)) = x1    218.52/82.03
POL(c5(x1)) = x1    218.52/82.03
POL(c9) = 0    218.52/82.03
POL(c9(x1)) = x1    218.52/82.03
POL(cons(x1, x2)) = 0    218.52/82.03
POL(false) = [1]    218.52/82.03
POL(half(x1)) = [2]    218.52/82.03
POL(lastbit(x1)) = 0    218.52/82.03
POL(s(x1)) = 0   
218.52/82.03
218.52/82.03

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.52/82.03
half(s(0)) → 0 218.52/82.03
half(s(s(z0))) → s(half(z0)) 218.52/82.03
lastbit(0) → 0 218.52/82.03
lastbit(s(0)) → s(0) 218.52/82.03
lastbit(s(s(z0))) → lastbit(z0) 218.52/82.03
zero(0) → true 218.52/82.03
zero(s(z0)) → false 218.52/82.03
conv(z0) → conviter(z0, cons(0, nil)) 218.52/82.03
conviter(z0, z1) → if(zero(z0), z0, z1) 218.52/82.03
if(true, z0, z1) → z1 218.52/82.03
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.03
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.03
IF(false, z0, z1) → c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0), LASTBIT(z0)) 218.52/82.03
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.03
CONVITER(0, x1) → c9
S tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.03
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.03
IF(false, z0, z1) → c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0), LASTBIT(z0)) 218.52/82.03
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1))
K tuples:

CONVITER(0, x1) → c9
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

HALF, LASTBIT, IF, CONVITER

Compound Symbols:

c2, c5, c11, c9, c9

218.52/82.03
218.52/82.03

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

Use narrowing to replace IF(false, z0, z1) → c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0), LASTBIT(z0)) by

IF(false, 0, x1) → c11(CONVITER(half(0), cons(0, x1)), HALF(0), LASTBIT(0)) 218.52/82.03
IF(false, s(0), x1) → c11(CONVITER(half(s(0)), cons(s(0), x1)), HALF(s(0)), LASTBIT(s(0))) 218.52/82.03
IF(false, s(s(z0)), x1) → c11(CONVITER(half(s(s(z0))), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.03
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1)), HALF(0), LASTBIT(0)) 218.52/82.03
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1)), HALF(s(0)), LASTBIT(s(0))) 218.52/82.03
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(s(s(z0))), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0))))
218.52/82.03
218.52/82.03

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.52/82.03
half(s(0)) → 0 218.52/82.03
half(s(s(z0))) → s(half(z0)) 218.52/82.03
lastbit(0) → 0 218.52/82.03
lastbit(s(0)) → s(0) 218.52/82.03
lastbit(s(s(z0))) → lastbit(z0) 218.52/82.03
zero(0) → true 218.52/82.03
zero(s(z0)) → false 218.52/82.03
conv(z0) → conviter(z0, cons(0, nil)) 218.52/82.03
conviter(z0, z1) → if(zero(z0), z0, z1) 218.52/82.03
if(true, z0, z1) → z1 218.52/82.03
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.03
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.03
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.03
CONVITER(0, x1) → c9 218.52/82.03
IF(false, 0, x1) → c11(CONVITER(half(0), cons(0, x1)), HALF(0), LASTBIT(0)) 218.52/82.03
IF(false, s(0), x1) → c11(CONVITER(half(s(0)), cons(s(0), x1)), HALF(s(0)), LASTBIT(s(0))) 218.52/82.03
IF(false, s(s(z0)), x1) → c11(CONVITER(half(s(s(z0))), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.03
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1)), HALF(0), LASTBIT(0)) 218.52/82.03
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1)), HALF(s(0)), LASTBIT(s(0))) 218.52/82.03
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(s(s(z0))), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0))))
S tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.03
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.03
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.03
IF(false, 0, x1) → c11(CONVITER(half(0), cons(0, x1)), HALF(0), LASTBIT(0)) 218.52/82.03
IF(false, s(0), x1) → c11(CONVITER(half(s(0)), cons(s(0), x1)), HALF(s(0)), LASTBIT(s(0))) 218.52/82.03
IF(false, s(s(z0)), x1) → c11(CONVITER(half(s(s(z0))), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.03
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1)), HALF(0), LASTBIT(0)) 218.52/82.03
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1)), HALF(s(0)), LASTBIT(s(0))) 218.52/82.03
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(s(s(z0))), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0))))
K tuples:

CONVITER(0, x1) → c9
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

HALF, LASTBIT, CONVITER, IF

Compound Symbols:

c2, c5, c9, c9, c11

218.52/82.05
218.52/82.05

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

Removed 8 trailing tuple parts
218.52/82.05
218.52/82.05

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.52/82.05
half(s(0)) → 0 218.52/82.05
half(s(s(z0))) → s(half(z0)) 218.52/82.05
lastbit(0) → 0 218.52/82.05
lastbit(s(0)) → s(0) 218.52/82.05
lastbit(s(s(z0))) → lastbit(z0) 218.52/82.05
zero(0) → true 218.52/82.05
zero(s(z0)) → false 218.52/82.05
conv(z0) → conviter(z0, cons(0, nil)) 218.52/82.05
conviter(z0, z1) → if(zero(z0), z0, z1) 218.52/82.05
if(true, z0, z1) → z1 218.52/82.05
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.05
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.05
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.05
CONVITER(0, x1) → c9 218.52/82.05
IF(false, s(s(z0)), x1) → c11(CONVITER(half(s(s(z0))), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.05
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(s(s(z0))), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.05
IF(false, 0, x1) → c11(CONVITER(half(0), cons(0, x1))) 218.52/82.05
IF(false, s(0), x1) → c11(CONVITER(half(s(0)), cons(s(0), x1))) 218.52/82.05
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.05
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1)))
S tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.05
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.05
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.05
IF(false, s(s(z0)), x1) → c11(CONVITER(half(s(s(z0))), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.05
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(s(s(z0))), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.05
IF(false, 0, x1) → c11(CONVITER(half(0), cons(0, x1))) 218.52/82.05
IF(false, s(0), x1) → c11(CONVITER(half(s(0)), cons(s(0), x1))) 218.52/82.05
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.05
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1)))
K tuples:

CONVITER(0, x1) → c9
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

HALF, LASTBIT, CONVITER, IF

Compound Symbols:

c2, c5, c9, c9, c11, c11

218.52/82.05
218.52/82.05

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

Removed 3 trailing nodes:

IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.05
CONVITER(0, x1) → c9 218.52/82.05
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1)))
218.52/82.05
218.52/82.05

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.52/82.05
half(s(0)) → 0 218.52/82.05
half(s(s(z0))) → s(half(z0)) 218.52/82.05
lastbit(0) → 0 218.52/82.05
lastbit(s(0)) → s(0) 218.52/82.05
lastbit(s(s(z0))) → lastbit(z0) 218.52/82.05
zero(0) → true 218.52/82.05
zero(s(z0)) → false 218.52/82.05
conv(z0) → conviter(z0, cons(0, nil)) 218.52/82.05
conviter(z0, z1) → if(zero(z0), z0, z1) 218.52/82.05
if(true, z0, z1) → z1 218.52/82.05
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.05
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.05
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.05
CONVITER(0, x1) → c9 218.52/82.05
IF(false, s(s(z0)), x1) → c11(CONVITER(half(s(s(z0))), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.05
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(s(s(z0))), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.05
IF(false, 0, x1) → c11(CONVITER(half(0), cons(0, x1))) 218.52/82.05
IF(false, s(0), x1) → c11(CONVITER(half(s(0)), cons(s(0), x1))) 218.52/82.05
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.05
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1)))
S tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.05
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.05
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.05
IF(false, s(s(z0)), x1) → c11(CONVITER(half(s(s(z0))), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.05
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(s(s(z0))), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.05
IF(false, 0, x1) → c11(CONVITER(half(0), cons(0, x1))) 218.52/82.05
IF(false, s(0), x1) → c11(CONVITER(half(s(0)), cons(s(0), x1))) 218.52/82.05
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.05
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1)))
K tuples:

CONVITER(0, x1) → c9
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

HALF, LASTBIT, CONVITER, IF

Compound Symbols:

c2, c5, c9, c9, c11, c11

218.52/82.05
218.52/82.05

(21) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

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

IF(false, 0, x1) → c11(CONVITER(half(0), cons(0, x1))) 218.52/82.05
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.05
CONVITER(0, x1) → c9 218.52/82.05
CONVITER(0, x1) → c9
218.52/82.05
218.52/82.05

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.52/82.05
half(s(0)) → 0 218.52/82.05
half(s(s(z0))) → s(half(z0)) 218.52/82.05
lastbit(0) → 0 218.52/82.05
lastbit(s(0)) → s(0) 218.52/82.05
lastbit(s(s(z0))) → lastbit(z0) 218.52/82.05
zero(0) → true 218.52/82.05
zero(s(z0)) → false 218.52/82.05
conv(z0) → conviter(z0, cons(0, nil)) 218.52/82.05
conviter(z0, z1) → if(zero(z0), z0, z1) 218.52/82.05
if(true, z0, z1) → z1 218.52/82.05
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.05
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.05
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.05
CONVITER(0, x1) → c9 218.52/82.05
IF(false, s(s(z0)), x1) → c11(CONVITER(half(s(s(z0))), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.05
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(s(s(z0))), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.07
IF(false, 0, x1) → c11(CONVITER(half(0), cons(0, x1))) 218.52/82.07
IF(false, s(0), x1) → c11(CONVITER(half(s(0)), cons(s(0), x1))) 218.52/82.07
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.07
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1)))
S tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.07
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.07
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.07
IF(false, s(s(z0)), x1) → c11(CONVITER(half(s(s(z0))), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.07
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(s(s(z0))), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.07
IF(false, s(0), x1) → c11(CONVITER(half(s(0)), cons(s(0), x1))) 218.52/82.07
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1)))
K tuples:

CONVITER(0, x1) → c9 218.52/82.07
IF(false, 0, x1) → c11(CONVITER(half(0), cons(0, x1))) 218.52/82.07
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1)))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

HALF, LASTBIT, CONVITER, IF

Compound Symbols:

c2, c5, c9, c9, c11, c11

218.52/82.07
218.52/82.07

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

IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1)))
We considered the (Usable) Rules:

lastbit(s(0)) → s(0) 218.52/82.07
lastbit(0) → 0 218.52/82.07
lastbit(s(s(z0))) → lastbit(z0) 218.52/82.07
half(s(0)) → 0 218.52/82.07
half(0) → 0 218.52/82.07
half(s(s(z0))) → s(half(z0))
And the Tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.07
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.07
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.07
CONVITER(0, x1) → c9 218.52/82.07
IF(false, s(s(z0)), x1) → c11(CONVITER(half(s(s(z0))), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.07
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(s(s(z0))), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.07
IF(false, 0, x1) → c11(CONVITER(half(0), cons(0, x1))) 218.52/82.07
IF(false, s(0), x1) → c11(CONVITER(half(s(0)), cons(s(0), x1))) 218.52/82.07
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.07
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1)))
The order we found is given by the following interpretation:
Polynomial interpretation : 218.52/82.07

POL(0) = 0    218.52/82.07
POL(CONVITER(x1, x2)) = [4]x1    218.52/82.07
POL(HALF(x1)) = 0    218.52/82.07
POL(IF(x1, x2, x3)) = x1    218.52/82.07
POL(LASTBIT(x1)) = 0    218.52/82.07
POL(c11(x1)) = x1    218.52/82.07
POL(c11(x1, x2, x3)) = x1 + x2 + x3    218.52/82.07
POL(c2(x1)) = x1    218.52/82.07
POL(c5(x1)) = x1    218.52/82.07
POL(c9) = 0    218.52/82.07
POL(c9(x1)) = x1    218.52/82.07
POL(cons(x1, x2)) = [1] + x2    218.52/82.07
POL(false) = [4]    218.52/82.07
POL(half(x1)) = x1    218.52/82.07
POL(lastbit(x1)) = 0    218.52/82.07
POL(s(x1)) = [1]   
218.52/82.07
218.52/82.07

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.52/82.07
half(s(0)) → 0 218.52/82.07
half(s(s(z0))) → s(half(z0)) 218.52/82.07
lastbit(0) → 0 218.52/82.07
lastbit(s(0)) → s(0) 218.52/82.07
lastbit(s(s(z0))) → lastbit(z0) 218.52/82.07
zero(0) → true 218.52/82.07
zero(s(z0)) → false 218.52/82.07
conv(z0) → conviter(z0, cons(0, nil)) 218.52/82.07
conviter(z0, z1) → if(zero(z0), z0, z1) 218.52/82.07
if(true, z0, z1) → z1 218.52/82.07
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.07
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.07
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.07
CONVITER(0, x1) → c9 218.52/82.07
IF(false, s(s(z0)), x1) → c11(CONVITER(half(s(s(z0))), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.07
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(s(s(z0))), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.07
IF(false, 0, x1) → c11(CONVITER(half(0), cons(0, x1))) 218.52/82.07
IF(false, s(0), x1) → c11(CONVITER(half(s(0)), cons(s(0), x1))) 218.52/82.07
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.07
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1)))
S tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.07
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.07
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.07
IF(false, s(s(z0)), x1) → c11(CONVITER(half(s(s(z0))), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.07
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(s(s(z0))), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.07
IF(false, s(0), x1) → c11(CONVITER(half(s(0)), cons(s(0), x1)))
K tuples:

CONVITER(0, x1) → c9 218.52/82.07
IF(false, 0, x1) → c11(CONVITER(half(0), cons(0, x1))) 218.52/82.07
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.07
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1)))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

HALF, LASTBIT, CONVITER, IF

Compound Symbols:

c2, c5, c9, c9, c11, c11

218.52/82.07
218.52/82.07

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

IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(s(s(z0))), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0))))
We considered the (Usable) Rules:

lastbit(s(0)) → s(0) 218.52/82.07
lastbit(0) → 0 218.52/82.07
lastbit(s(s(z0))) → lastbit(z0) 218.52/82.07
half(s(0)) → 0 218.52/82.07
half(0) → 0 218.52/82.07
half(s(s(z0))) → s(half(z0))
And the Tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.07
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.07
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.07
CONVITER(0, x1) → c9 218.52/82.07
IF(false, s(s(z0)), x1) → c11(CONVITER(half(s(s(z0))), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.07
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(s(s(z0))), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.07
IF(false, 0, x1) → c11(CONVITER(half(0), cons(0, x1))) 218.52/82.07
IF(false, s(0), x1) → c11(CONVITER(half(s(0)), cons(s(0), x1))) 218.52/82.07
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.07
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1)))
The order we found is given by the following interpretation:
Polynomial interpretation : 218.52/82.07

POL(0) = 0    218.52/82.07
POL(CONVITER(x1, x2)) = x1    218.52/82.07
POL(HALF(x1)) = 0    218.52/82.07
POL(IF(x1, x2, x3)) = x1 + x2    218.52/82.07
POL(LASTBIT(x1)) = 0    218.52/82.07
POL(c11(x1)) = x1    218.52/82.07
POL(c11(x1, x2, x3)) = x1 + x2 + x3    218.52/82.07
POL(c2(x1)) = x1    218.52/82.07
POL(c5(x1)) = x1    218.52/82.07
POL(c9) = 0    218.52/82.07
POL(c9(x1)) = x1    218.52/82.07
POL(cons(x1, x2)) = [1] + x2    218.52/82.07
POL(false) = 0    218.52/82.07
POL(half(x1)) = x1    218.52/82.07
POL(lastbit(x1)) = 0    218.52/82.07
POL(s(x1)) = [1] + x1   
218.52/82.07
218.52/82.07

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.52/82.07
half(s(0)) → 0 218.52/82.07
half(s(s(z0))) → s(half(z0)) 218.52/82.07
lastbit(0) → 0 218.52/82.07
lastbit(s(0)) → s(0) 218.52/82.07
lastbit(s(s(z0))) → lastbit(z0) 218.52/82.07
zero(0) → true 218.52/82.07
zero(s(z0)) → false 218.52/82.07
conv(z0) → conviter(z0, cons(0, nil)) 218.52/82.07
conviter(z0, z1) → if(zero(z0), z0, z1) 218.52/82.07
if(true, z0, z1) → z1 218.52/82.07
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.07
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.07
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.07
CONVITER(0, x1) → c9 218.52/82.07
IF(false, s(s(z0)), x1) → c11(CONVITER(half(s(s(z0))), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.07
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(s(s(z0))), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.08
IF(false, 0, x1) → c11(CONVITER(half(0), cons(0, x1))) 218.52/82.08
IF(false, s(0), x1) → c11(CONVITER(half(s(0)), cons(s(0), x1))) 218.52/82.08
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.08
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1)))
S tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.08
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.08
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.08
IF(false, s(s(z0)), x1) → c11(CONVITER(half(s(s(z0))), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.08
IF(false, s(0), x1) → c11(CONVITER(half(s(0)), cons(s(0), x1)))
K tuples:

CONVITER(0, x1) → c9 218.52/82.08
IF(false, 0, x1) → c11(CONVITER(half(0), cons(0, x1))) 218.52/82.08
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.08
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.08
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(s(s(z0))), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0))))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

HALF, LASTBIT, CONVITER, IF

Compound Symbols:

c2, c5, c9, c9, c11, c11

218.52/82.08
218.52/82.08

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

Use narrowing to replace IF(false, s(s(z0)), x1) → c11(CONVITER(half(s(s(z0))), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) by

IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.08
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.08
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.08
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0))))
218.52/82.08
218.52/82.08

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.52/82.08
half(s(0)) → 0 218.52/82.08
half(s(s(z0))) → s(half(z0)) 218.52/82.08
lastbit(0) → 0 218.52/82.08
lastbit(s(0)) → s(0) 218.52/82.08
lastbit(s(s(z0))) → lastbit(z0) 218.52/82.08
zero(0) → true 218.52/82.08
zero(s(z0)) → false 218.52/82.08
conv(z0) → conviter(z0, cons(0, nil)) 218.52/82.08
conviter(z0, z1) → if(zero(z0), z0, z1) 218.52/82.08
if(true, z0, z1) → z1 218.52/82.08
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.08
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.08
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.08
CONVITER(0, x1) → c9 218.52/82.08
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(s(s(z0))), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.08
IF(false, 0, x1) → c11(CONVITER(half(0), cons(0, x1))) 218.52/82.08
IF(false, s(0), x1) → c11(CONVITER(half(s(0)), cons(s(0), x1))) 218.52/82.08
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.08
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.08
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.08
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.08
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.08
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0))))
S tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.08
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.08
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.08
IF(false, s(0), x1) → c11(CONVITER(half(s(0)), cons(s(0), x1))) 218.52/82.08
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.08
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.08
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.08
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0))))
K tuples:

CONVITER(0, x1) → c9 218.52/82.08
IF(false, 0, x1) → c11(CONVITER(half(0), cons(0, x1))) 218.52/82.08
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.08
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.08
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(s(s(z0))), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0))))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

HALF, LASTBIT, CONVITER, IF

Compound Symbols:

c2, c5, c9, c9, c11, c11

218.52/82.08
218.52/82.08

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

Removed 3 trailing nodes:

IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.08
CONVITER(0, x1) → c9 218.52/82.08
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1)))
218.52/82.08
218.52/82.08

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.52/82.08
half(s(0)) → 0 218.52/82.08
half(s(s(z0))) → s(half(z0)) 218.52/82.08
lastbit(0) → 0 218.52/82.08
lastbit(s(0)) → s(0) 218.52/82.08
lastbit(s(s(z0))) → lastbit(z0) 218.52/82.08
zero(0) → true 218.52/82.08
zero(s(z0)) → false 218.52/82.08
conv(z0) → conviter(z0, cons(0, nil)) 218.52/82.08
conviter(z0, z1) → if(zero(z0), z0, z1) 218.52/82.08
if(true, z0, z1) → z1 218.52/82.08
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.08
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.08
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.08
CONVITER(0, x1) → c9 218.52/82.08
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(s(s(z0))), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.08
IF(false, 0, x1) → c11(CONVITER(half(0), cons(0, x1))) 218.52/82.08
IF(false, s(0), x1) → c11(CONVITER(half(s(0)), cons(s(0), x1))) 218.52/82.08
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.08
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.08
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.08
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.08
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.08
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0))))
S tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.08
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.08
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.08
IF(false, s(0), x1) → c11(CONVITER(half(s(0)), cons(s(0), x1))) 218.52/82.08
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.08
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.08
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.08
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0))))
K tuples:

CONVITER(0, x1) → c9 218.52/82.08
IF(false, 0, x1) → c11(CONVITER(half(0), cons(0, x1))) 218.52/82.08
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.08
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.08
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(s(s(z0))), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0))))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

HALF, LASTBIT, CONVITER, IF

Compound Symbols:

c2, c5, c9, c9, c11, c11

218.52/82.08
218.52/82.08

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

IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0))))
We considered the (Usable) Rules:

half(0) → 0 218.52/82.09
half(s(0)) → 0 218.52/82.09
half(s(s(z0))) → s(half(z0)) 218.52/82.09
lastbit(0) → 0 218.52/82.09
lastbit(s(0)) → s(0) 218.52/82.09
lastbit(s(s(z0))) → lastbit(z0)
And the Tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.09
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.09
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.09
CONVITER(0, x1) → c9 218.52/82.09
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(s(s(z0))), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.09
IF(false, 0, x1) → c11(CONVITER(half(0), cons(0, x1))) 218.52/82.09
IF(false, s(0), x1) → c11(CONVITER(half(s(0)), cons(s(0), x1))) 218.52/82.09
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.09
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.09
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.09
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.09
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.09
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0))))
The order we found is given by the following interpretation:
Polynomial interpretation : 218.52/82.09

POL(0) = 0    218.52/82.09
POL(CONVITER(x1, x2)) = x1    218.52/82.09
POL(HALF(x1)) = 0    218.52/82.09
POL(IF(x1, x2, x3)) = x1 + x2    218.52/82.09
POL(LASTBIT(x1)) = 0    218.52/82.09
POL(c11(x1)) = x1    218.52/82.09
POL(c11(x1, x2, x3)) = x1 + x2 + x3    218.52/82.09
POL(c2(x1)) = x1    218.52/82.09
POL(c5(x1)) = x1    218.52/82.09
POL(c9) = 0    218.52/82.09
POL(c9(x1)) = x1    218.52/82.09
POL(cons(x1, x2)) = [1] + x2    218.52/82.09
POL(false) = 0    218.52/82.09
POL(half(x1)) = x1    218.52/82.09
POL(lastbit(x1)) = 0    218.52/82.09
POL(s(x1)) = [1] + x1   
218.52/82.09
218.52/82.09

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.52/82.09
half(s(0)) → 0 218.52/82.09
half(s(s(z0))) → s(half(z0)) 218.52/82.09
lastbit(0) → 0 218.52/82.09
lastbit(s(0)) → s(0) 218.52/82.09
lastbit(s(s(z0))) → lastbit(z0) 218.52/82.09
zero(0) → true 218.52/82.09
zero(s(z0)) → false 218.52/82.09
conv(z0) → conviter(z0, cons(0, nil)) 218.52/82.09
conviter(z0, z1) → if(zero(z0), z0, z1) 218.52/82.09
if(true, z0, z1) → z1 218.52/82.09
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.09
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.09
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.09
CONVITER(0, x1) → c9 218.52/82.09
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(s(s(z0))), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.09
IF(false, 0, x1) → c11(CONVITER(half(0), cons(0, x1))) 218.52/82.09
IF(false, s(0), x1) → c11(CONVITER(half(s(0)), cons(s(0), x1))) 218.52/82.09
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.09
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.09
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.09
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.09
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.09
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0))))
S tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.09
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.09
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.09
IF(false, s(0), x1) → c11(CONVITER(half(s(0)), cons(s(0), x1))) 218.52/82.09
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.09
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.09
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0))))))
K tuples:

CONVITER(0, x1) → c9 218.52/82.09
IF(false, 0, x1) → c11(CONVITER(half(0), cons(0, x1))) 218.52/82.09
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.09
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.09
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(s(s(z0))), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.09
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0))))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

HALF, LASTBIT, CONVITER, IF

Compound Symbols:

c2, c5, c9, c9, c11, c11

218.52/82.09
218.52/82.09

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

Use narrowing to replace IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(s(s(z0))), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) by

IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.09
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.09
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.09
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(s(s(z0))))), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0))))))
218.52/82.09
218.52/82.09

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.52/82.09
half(s(0)) → 0 218.52/82.09
half(s(s(z0))) → s(half(z0)) 218.52/82.09
lastbit(0) → 0 218.52/82.09
lastbit(s(0)) → s(0) 218.52/82.09
lastbit(s(s(z0))) → lastbit(z0) 218.52/82.09
zero(0) → true 218.52/82.09
zero(s(z0)) → false 218.52/82.09
conv(z0) → conviter(z0, cons(0, nil)) 218.52/82.09
conviter(z0, z1) → if(zero(z0), z0, z1) 218.52/82.09
if(true, z0, z1) → z1 218.52/82.09
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.09
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.09
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.09
CONVITER(0, x1) → c9 218.52/82.09
IF(false, 0, x1) → c11(CONVITER(half(0), cons(0, x1))) 218.52/82.09
IF(false, s(0), x1) → c11(CONVITER(half(s(0)), cons(s(0), x1))) 218.52/82.09
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.09
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.09
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.09
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.09
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.09
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.09
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.09
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.09
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(s(s(z0))))), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0))))))
S tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.09
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.09
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.09
IF(false, s(0), x1) → c11(CONVITER(half(s(0)), cons(s(0), x1))) 218.52/82.09
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.09
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.09
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0))))))
K tuples:

CONVITER(0, x1) → c9 218.52/82.09
IF(false, 0, x1) → c11(CONVITER(half(0), cons(0, x1))) 218.52/82.09
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.09
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.09
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(s(s(z0))), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.09
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0))))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

HALF, LASTBIT, CONVITER, IF

Compound Symbols:

c2, c5, c9, c9, c11, c11

218.52/82.09
218.52/82.09

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

Removed 3 trailing nodes:

IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.09
CONVITER(0, x1) → c9 218.52/82.09
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1)))
218.52/82.09
218.52/82.09

(36) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.52/82.09
half(s(0)) → 0 218.52/82.09
half(s(s(z0))) → s(half(z0)) 218.52/82.09
lastbit(0) → 0 218.52/82.09
lastbit(s(0)) → s(0) 218.52/82.09
lastbit(s(s(z0))) → lastbit(z0) 218.52/82.09
zero(0) → true 218.52/82.09
zero(s(z0)) → false 218.52/82.09
conv(z0) → conviter(z0, cons(0, nil)) 218.52/82.09
conviter(z0, z1) → if(zero(z0), z0, z1) 218.52/82.09
if(true, z0, z1) → z1 218.52/82.09
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.09
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.09
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.09
CONVITER(0, x1) → c9 218.52/82.09
IF(false, 0, x1) → c11(CONVITER(half(0), cons(0, x1))) 218.52/82.09
IF(false, s(0), x1) → c11(CONVITER(half(s(0)), cons(s(0), x1))) 218.52/82.09
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.09
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.09
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.09
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.09
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.09
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.09
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.09
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.09
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(s(s(z0))))), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0))))))
S tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.09
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.09
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.09
IF(false, s(0), x1) → c11(CONVITER(half(s(0)), cons(s(0), x1))) 218.52/82.09
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.09
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.09
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0))))))
K tuples:

CONVITER(0, x1) → c9 218.52/82.09
IF(false, 0, x1) → c11(CONVITER(half(0), cons(0, x1))) 218.52/82.09
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.09
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.09
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0))))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

HALF, LASTBIT, CONVITER, IF

Compound Symbols:

c2, c5, c9, c9, c11, c11

218.52/82.09
218.52/82.09

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

Use narrowing to replace IF(false, 0, x1) → c11(CONVITER(half(0), cons(0, x1))) by

IF(false, 0, x0) → c11(CONVITER(0, cons(0, x0)))
218.52/82.09
218.52/82.09

(38) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.52/82.09
half(s(0)) → 0 218.52/82.09
half(s(s(z0))) → s(half(z0)) 218.52/82.09
lastbit(0) → 0 218.52/82.09
lastbit(s(0)) → s(0) 218.52/82.09
lastbit(s(s(z0))) → lastbit(z0) 218.52/82.09
zero(0) → true 218.52/82.09
zero(s(z0)) → false 218.52/82.09
conv(z0) → conviter(z0, cons(0, nil)) 218.52/82.09
conviter(z0, z1) → if(zero(z0), z0, z1) 218.52/82.09
if(true, z0, z1) → z1 218.52/82.09
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.09
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.09
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.09
CONVITER(0, x1) → c9 218.52/82.09
IF(false, s(0), x1) → c11(CONVITER(half(s(0)), cons(s(0), x1))) 218.52/82.09
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.09
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.09
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.09
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.09
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.09
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.09
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.09
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.09
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(s(s(z0))))), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.09
IF(false, 0, x0) → c11(CONVITER(0, cons(0, x0)))
S tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.09
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.09
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.09
IF(false, s(0), x1) → c11(CONVITER(half(s(0)), cons(s(0), x1))) 218.52/82.09
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.09
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0))))))
K tuples:

CONVITER(0, x1) → c9 218.52/82.10
IF(false, 0, x1) → c11(CONVITER(half(0), cons(0, x1))) 218.52/82.10
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.10
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0))))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

HALF, LASTBIT, CONVITER, IF

Compound Symbols:

c2, c5, c9, c9, c11, c11

218.52/82.10
218.52/82.10

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

Removed 4 trailing nodes:

IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.10
IF(false, 0, x0) → c11(CONVITER(0, cons(0, x0))) 218.52/82.10
CONVITER(0, x1) → c9 218.52/82.10
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1)))
218.52/82.10
218.52/82.10

(40) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.52/82.10
half(s(0)) → 0 218.52/82.10
half(s(s(z0))) → s(half(z0)) 218.52/82.10
lastbit(0) → 0 218.52/82.10
lastbit(s(0)) → s(0) 218.52/82.10
lastbit(s(s(z0))) → lastbit(z0) 218.52/82.10
zero(0) → true 218.52/82.10
zero(s(z0)) → false 218.52/82.10
conv(z0) → conviter(z0, cons(0, nil)) 218.52/82.10
conviter(z0, z1) → if(zero(z0), z0, z1) 218.52/82.10
if(true, z0, z1) → z1 218.52/82.10
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.10
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.10
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.10
CONVITER(0, x1) → c9 218.52/82.10
IF(false, s(0), x1) → c11(CONVITER(half(s(0)), cons(s(0), x1))) 218.52/82.10
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.10
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(s(s(z0))))), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0))))))
S tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.10
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.10
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.10
IF(false, s(0), x1) → c11(CONVITER(half(s(0)), cons(s(0), x1))) 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0))))))
K tuples:

CONVITER(0, x1) → c9 218.52/82.10
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.10
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0))))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

HALF, LASTBIT, CONVITER, IF

Compound Symbols:

c2, c5, c9, c9, c11, c11

218.52/82.10
218.52/82.10

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

Use narrowing to replace IF(false, s(0), x1) → c11(CONVITER(half(s(0)), cons(s(0), x1))) by

IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0)))
218.52/82.10
218.52/82.10

(42) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.52/82.10
half(s(0)) → 0 218.52/82.10
half(s(s(z0))) → s(half(z0)) 218.52/82.10
lastbit(0) → 0 218.52/82.10
lastbit(s(0)) → s(0) 218.52/82.10
lastbit(s(s(z0))) → lastbit(z0) 218.52/82.10
zero(0) → true 218.52/82.10
zero(s(z0)) → false 218.52/82.10
conv(z0) → conviter(z0, cons(0, nil)) 218.52/82.10
conviter(z0, z1) → if(zero(z0), z0, z1) 218.52/82.10
if(true, z0, z1) → z1 218.52/82.10
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.10
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.10
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.10
CONVITER(0, x1) → c9 218.52/82.10
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.10
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(s(s(z0))))), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0)))
S tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.10
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.10
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0)))
K tuples:

CONVITER(0, x1) → c9 218.52/82.10
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.10
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0))))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

HALF, LASTBIT, CONVITER, IF

Compound Symbols:

c2, c5, c9, c9, c11, c11

218.52/82.10
218.52/82.10

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

Removed 4 trailing nodes:

IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.10
CONVITER(0, x1) → c9 218.52/82.10
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0)))
218.52/82.10
218.52/82.10

(44) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.52/82.10
half(s(0)) → 0 218.52/82.10
half(s(s(z0))) → s(half(z0)) 218.52/82.10
lastbit(0) → 0 218.52/82.10
lastbit(s(0)) → s(0) 218.52/82.10
lastbit(s(s(z0))) → lastbit(z0) 218.52/82.10
zero(0) → true 218.52/82.10
zero(s(z0)) → false 218.52/82.10
conv(z0) → conviter(z0, cons(0, nil)) 218.52/82.10
conviter(z0, z1) → if(zero(z0), z0, z1) 218.52/82.10
if(true, z0, z1) → z1 218.52/82.10
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.10
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.10
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.10
CONVITER(0, x1) → c9 218.52/82.10
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.10
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(s(s(z0))))), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0)))
S tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.10
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.10
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0)))
K tuples:

CONVITER(0, x1) → c9 218.52/82.10
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.10
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0))))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

HALF, LASTBIT, CONVITER, IF

Compound Symbols:

c2, c5, c9, c9, c11, c11

218.52/82.10
218.52/82.10

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

IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0)))
We considered the (Usable) Rules:

half(0) → 0 218.52/82.10
half(s(0)) → 0 218.52/82.10
half(s(s(z0))) → s(half(z0)) 218.52/82.10
lastbit(s(s(z0))) → lastbit(z0) 218.52/82.10
lastbit(0) → 0 218.52/82.10
lastbit(s(0)) → s(0)
And the Tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.10
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.10
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.10
CONVITER(0, x1) → c9 218.52/82.10
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.10
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(s(s(z0))))), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0)))
The order we found is given by the following interpretation:
Polynomial interpretation : 218.52/82.10

POL(0) = 0    218.52/82.10
POL(CONVITER(x1, x2)) = [4]x1    218.52/82.10
POL(HALF(x1)) = 0    218.52/82.10
POL(IF(x1, x2, x3)) = x1 + [4]x2    218.52/82.10
POL(LASTBIT(x1)) = 0    218.52/82.10
POL(c11(x1)) = x1    218.52/82.10
POL(c11(x1, x2, x3)) = x1 + x2 + x3    218.52/82.10
POL(c2(x1)) = x1    218.52/82.10
POL(c5(x1)) = x1    218.52/82.10
POL(c9) = 0    218.52/82.10
POL(c9(x1)) = x1    218.52/82.10
POL(cons(x1, x2)) = [1] + x2    218.52/82.10
POL(false) = 0    218.52/82.10
POL(half(x1)) = x1    218.52/82.10
POL(lastbit(x1)) = 0    218.52/82.10
POL(s(x1)) = [4]   
218.52/82.10
218.52/82.10

(46) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.52/82.10
half(s(0)) → 0 218.52/82.10
half(s(s(z0))) → s(half(z0)) 218.52/82.10
lastbit(0) → 0 218.52/82.10
lastbit(s(0)) → s(0) 218.52/82.10
lastbit(s(s(z0))) → lastbit(z0) 218.52/82.10
zero(0) → true 218.52/82.10
zero(s(z0)) → false 218.52/82.10
conv(z0) → conviter(z0, cons(0, nil)) 218.52/82.10
conviter(z0, z1) → if(zero(z0), z0, z1) 218.52/82.10
if(true, z0, z1) → z1 218.52/82.10
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.10
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.10
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.10
CONVITER(0, x1) → c9 218.52/82.10
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.10
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(s(s(z0))))), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0)))
S tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.10
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.10
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0))))))
K tuples:

CONVITER(0, x1) → c9 218.52/82.10
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.10
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0)))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

HALF, LASTBIT, CONVITER, IF

Compound Symbols:

c2, c5, c9, c9, c11, c11

218.52/82.10
218.52/82.10

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

Use narrowing to replace IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) by

IF(false, 0, x0) → c11(CONVITER(0, cons(0, x0)))
218.52/82.10
218.52/82.10

(48) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.52/82.10
half(s(0)) → 0 218.52/82.10
half(s(s(z0))) → s(half(z0)) 218.52/82.10
lastbit(0) → 0 218.52/82.10
lastbit(s(0)) → s(0) 218.52/82.10
lastbit(s(s(z0))) → lastbit(z0) 218.52/82.10
zero(0) → true 218.52/82.10
zero(s(z0)) → false 218.52/82.10
conv(z0) → conviter(z0, cons(0, nil)) 218.52/82.10
conviter(z0, z1) → if(zero(z0), z0, z1) 218.52/82.10
if(true, z0, z1) → z1 218.52/82.10
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.10
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.10
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.10
CONVITER(0, x1) → c9 218.52/82.10
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(s(s(z0))))), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.52/82.10
IF(false, 0, x0) → c11(CONVITER(0, cons(0, x0)))
S tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.10
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.10
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0))))))
K tuples:

CONVITER(0, x1) → c9 218.52/82.10
IF(false, 0, x1) → c11(CONVITER(0, cons(lastbit(0), x1))) 218.52/82.10
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0)))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

HALF, LASTBIT, CONVITER, IF

Compound Symbols:

c2, c5, c9, c9, c11, c11

218.52/82.10
218.52/82.10

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

Removed 4 trailing nodes:

IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.10
IF(false, 0, x0) → c11(CONVITER(0, cons(0, x0))) 218.52/82.10
CONVITER(0, x1) → c9 218.52/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0)))
218.52/82.10
218.52/82.10

(50) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.52/82.10
half(s(0)) → 0 218.52/82.10
half(s(s(z0))) → s(half(z0)) 218.52/82.10
lastbit(0) → 0 218.52/82.10
lastbit(s(0)) → s(0) 218.52/82.10
lastbit(s(s(z0))) → lastbit(z0) 218.52/82.10
zero(0) → true 218.52/82.10
zero(s(z0)) → false 218.52/82.10
conv(z0) → conviter(z0, cons(0, nil)) 218.52/82.10
conviter(z0, z1) → if(zero(z0), z0, z1) 218.52/82.10
if(true, z0, z1) → z1 218.52/82.10
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.10
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.10
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.10
CONVITER(0, x1) → c9 218.52/82.10
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(s(s(z0))))), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0)))
S tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.10
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.10
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0))))))
K tuples:

CONVITER(0, x1) → c9 218.52/82.10
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0)))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

HALF, LASTBIT, CONVITER, IF

Compound Symbols:

c2, c5, c9, c9, c11, c11

218.52/82.10
218.52/82.10

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

Use narrowing to replace IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) by

IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0)))
218.52/82.10
218.52/82.10

(52) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.52/82.10
half(s(0)) → 0 218.52/82.10
half(s(s(z0))) → s(half(z0)) 218.52/82.10
lastbit(0) → 0 218.52/82.10
lastbit(s(0)) → s(0) 218.52/82.10
lastbit(s(s(z0))) → lastbit(z0) 218.52/82.10
zero(0) → true 218.52/82.10
zero(s(z0)) → false 218.52/82.10
conv(z0) → conviter(z0, cons(0, nil)) 218.52/82.10
conviter(z0, z1) → if(zero(z0), z0, z1) 218.52/82.10
if(true, z0, z1) → z1 218.52/82.10
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.10
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.10
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.10
CONVITER(0, x1) → c9 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(s(s(z0))))), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0)))
S tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.10
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.10
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0))))))
K tuples:

CONVITER(0, x1) → c9 218.52/82.10
IF(false, s(0), x1) → c11(CONVITER(0, cons(lastbit(s(0)), x1))) 218.52/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0)))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

HALF, LASTBIT, CONVITER, IF

Compound Symbols:

c2, c5, c9, c9, c11, c11

218.52/82.10
218.52/82.10

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

Removed 2 trailing nodes:

CONVITER(0, x1) → c9 218.52/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0)))
218.52/82.10
218.52/82.10

(54) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.52/82.10
half(s(0)) → 0 218.52/82.10
half(s(s(z0))) → s(half(z0)) 218.52/82.10
lastbit(0) → 0 218.52/82.10
lastbit(s(0)) → s(0) 218.52/82.10
lastbit(s(s(z0))) → lastbit(z0) 218.52/82.10
zero(0) → true 218.52/82.10
zero(s(z0)) → false 218.52/82.10
conv(z0) → conviter(z0, cons(0, nil)) 218.52/82.10
conviter(z0, z1) → if(zero(z0), z0, z1) 218.52/82.10
if(true, z0, z1) → z1 218.52/82.10
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.10
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.10
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.10
CONVITER(0, x1) → c9 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(s(s(z0))))), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0)))
S tuples:

HALF(s(s(z0))) → c2(HALF(z0)) 218.52/82.10
LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.10
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0))))))
K tuples:

CONVITER(0, x1) → c9 218.52/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0)))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

HALF, LASTBIT, CONVITER, IF

Compound Symbols:

c2, c5, c9, c9, c11, c11

218.52/82.10
218.52/82.10

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

Use forward instantiation to replace HALF(s(s(z0))) → c2(HALF(z0)) by

HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0))))
218.52/82.10
218.52/82.10

(56) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.52/82.10
half(s(0)) → 0 218.52/82.10
half(s(s(z0))) → s(half(z0)) 218.52/82.10
lastbit(0) → 0 218.52/82.10
lastbit(s(0)) → s(0) 218.52/82.10
lastbit(s(s(z0))) → lastbit(z0) 218.52/82.10
zero(0) → true 218.52/82.10
zero(s(z0)) → false 218.52/82.10
conv(z0) → conviter(z0, cons(0, nil)) 218.52/82.10
conviter(z0, z1) → if(zero(z0), z0, z1) 218.52/82.10
if(true, z0, z1) → z1 218.52/82.10
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.10
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.10
CONVITER(0, x1) → c9 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(s(s(z0))))), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.52/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0))))
S tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.10
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), HALF(s(s(0))), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), HALF(s(s(s(0)))), LASTBIT(s(s(s(0))))) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0))))
K tuples:

CONVITER(0, x1) → c9 218.52/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0)))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

LASTBIT, CONVITER, IF, HALF

Compound Symbols:

c5, c9, c9, c11, c11, c2

218.52/82.10
218.52/82.10

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

Removed 4 trailing tuple parts
218.52/82.10
218.52/82.10

(58) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.52/82.10
half(s(0)) → 0 218.52/82.10
half(s(s(z0))) → s(half(z0)) 218.52/82.10
lastbit(0) → 0 218.52/82.10
lastbit(s(0)) → s(0) 218.52/82.10
lastbit(s(s(z0))) → lastbit(z0) 218.52/82.10
zero(0) → true 218.52/82.10
zero(s(z0)) → false 218.52/82.10
conv(z0) → conviter(z0, cons(0, nil)) 218.52/82.10
conviter(z0, z1) → if(zero(z0), z0, z1) 218.52/82.10
if(true, z0, z1) → z1 218.52/82.10
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.10
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.10
CONVITER(0, x1) → c9 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(s(s(z0))))), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.52/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), LASTBIT(s(s(s(0))))) 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), LASTBIT(s(s(s(0)))))
S tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.10
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), LASTBIT(s(s(s(0)))))
K tuples:

CONVITER(0, x1) → c9 218.52/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0)))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

LASTBIT, CONVITER, IF, HALF

Compound Symbols:

c5, c9, c9, c11, c11, c2, c11

218.52/82.10
218.52/82.10

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

Removed 2 trailing nodes:

CONVITER(0, x1) → c9 218.52/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0)))
218.52/82.10
218.52/82.10

(60) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.52/82.10
half(s(0)) → 0 218.52/82.10
half(s(s(z0))) → s(half(z0)) 218.52/82.10
lastbit(0) → 0 218.52/82.10
lastbit(s(0)) → s(0) 218.52/82.10
lastbit(s(s(z0))) → lastbit(z0) 218.52/82.10
zero(0) → true 218.52/82.10
zero(s(z0)) → false 218.52/82.10
conv(z0) → conviter(z0, cons(0, nil)) 218.52/82.10
conviter(z0, z1) → if(zero(z0), z0, z1) 218.52/82.10
if(true, z0, z1) → z1 218.52/82.10
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.10
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.10
CONVITER(0, x1) → c9 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(s(s(z0))))), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.52/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.52/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), LASTBIT(s(s(s(0))))) 218.52/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), LASTBIT(s(s(0)))) 218.52/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), LASTBIT(s(s(s(0)))))
S tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.52/82.10
CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) 218.52/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), LASTBIT(s(s(s(0)))))
K tuples:

CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0)))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

LASTBIT, CONVITER, IF, HALF

Compound Symbols:

c5, c9, c9, c11, c11, c2, c11

218.88/82.10
218.88/82.10

(61) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use instantiation to replace CONVITER(s(z0), x1) → c9(IF(false, s(z0), x1)) by

CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0)))
218.88/82.10
218.88/82.10

(62) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.88/82.10
half(s(0)) → 0 218.88/82.10
half(s(s(z0))) → s(half(z0)) 218.88/82.10
lastbit(0) → 0 218.88/82.10
lastbit(s(0)) → s(0) 218.88/82.10
lastbit(s(s(z0))) → lastbit(z0) 218.88/82.10
zero(0) → true 218.88/82.10
zero(s(z0)) → false 218.88/82.10
conv(z0) → conviter(z0, cons(0, nil)) 218.88/82.10
conviter(z0, z1) → if(zero(z0), z0, z1) 218.88/82.10
if(true, z0, z1) → z1 218.88/82.10
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(s(s(z0))))), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0)))
S tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0)))
K tuples:

CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0)))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

LASTBIT, CONVITER, IF, HALF

Compound Symbols:

c5, c9, c11, c11, c2, c11, c9

218.88/82.10
218.88/82.10

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

Removed 2 trailing nodes:

CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0)))
218.88/82.10
218.88/82.10

(64) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.88/82.10
half(s(0)) → 0 218.88/82.10
half(s(s(z0))) → s(half(z0)) 218.88/82.10
lastbit(0) → 0 218.88/82.10
lastbit(s(0)) → s(0) 218.88/82.10
lastbit(s(s(z0))) → lastbit(z0) 218.88/82.10
zero(0) → true 218.88/82.10
zero(s(z0)) → false 218.88/82.10
conv(z0) → conviter(z0, cons(0, nil)) 218.88/82.10
conviter(z0, z1) → if(zero(z0), z0, z1) 218.88/82.10
if(true, z0, z1) → z1 218.88/82.10
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(s(s(z0))))), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0)))
S tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0)))
K tuples:

CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0)))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

LASTBIT, CONVITER, IF, HALF

Compound Symbols:

c5, c9, c11, c11, c2, c11, c9

218.88/82.10
218.88/82.10

(65) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)

Used rewriting to replace IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(half(s(s(s(s(z0))))), cons(lastbit(z0), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) by IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0))))))
218.88/82.10
218.88/82.10

(66) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.88/82.10
half(s(0)) → 0 218.88/82.10
half(s(s(z0))) → s(half(z0)) 218.88/82.10
lastbit(0) → 0 218.88/82.10
lastbit(s(0)) → s(0) 218.88/82.10
lastbit(s(s(z0))) → lastbit(z0) 218.88/82.10
zero(0) → true 218.88/82.10
zero(s(z0)) → false 218.88/82.10
conv(z0) → conviter(z0, cons(0, nil)) 218.88/82.10
conviter(z0, z1) → if(zero(z0), z0, z1) 218.88/82.10
if(true, z0, z1) → z1 218.88/82.10
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(s(s(z0))))), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0))))))
S tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0))))))
K tuples:

CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0)))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

LASTBIT, CONVITER, IF, HALF

Compound Symbols:

c5, c9, c11, c11, c2, c11, c9

218.88/82.10
218.88/82.10

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

Removed 2 trailing nodes:

CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0)))
218.88/82.10
218.88/82.10

(68) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.88/82.10
half(s(0)) → 0 218.88/82.10
half(s(s(z0))) → s(half(z0)) 218.88/82.10
lastbit(0) → 0 218.88/82.10
lastbit(s(0)) → s(0) 218.88/82.10
lastbit(s(s(z0))) → lastbit(z0) 218.88/82.10
zero(0) → true 218.88/82.10
zero(s(z0)) → false 218.88/82.10
conv(z0) → conviter(z0, cons(0, nil)) 218.88/82.10
conviter(z0, z1) → if(zero(z0), z0, z1) 218.88/82.10
if(true, z0, z1) → z1 218.88/82.10
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(s(s(z0))))), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0))))))
S tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0))))))
K tuples:

CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0)))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

LASTBIT, CONVITER, IF, HALF

Compound Symbols:

c5, c9, c11, c11, c2, c11, c9

218.88/82.10
218.88/82.10

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

IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0))))))
We considered the (Usable) Rules:

half(s(s(z0))) → s(half(z0)) 218.88/82.10
half(0) → 0 218.88/82.10
half(s(0)) → 0 218.88/82.10
lastbit(0) → 0 218.88/82.10
lastbit(s(0)) → s(0) 218.88/82.10
lastbit(s(s(z0))) → lastbit(z0)
And the Tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(s(s(z0))))), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0))))))
The order we found is given by the following interpretation:
Polynomial interpretation : 218.88/82.10

POL(0) = 0    218.88/82.10
POL(CONVITER(x1, x2)) = [4]x1    218.88/82.10
POL(HALF(x1)) = 0    218.88/82.10
POL(IF(x1, x2, x3)) = [4]x2    218.88/82.10
POL(LASTBIT(x1)) = 0    218.88/82.10
POL(c11(x1)) = x1    218.88/82.10
POL(c11(x1, x2)) = x1 + x2    218.88/82.10
POL(c11(x1, x2, x3)) = x1 + x2 + x3    218.88/82.10
POL(c2(x1)) = x1    218.88/82.10
POL(c5(x1)) = x1    218.88/82.10
POL(c9) = 0    218.88/82.10
POL(c9(x1)) = x1    218.88/82.10
POL(cons(x1, x2)) = x2    218.88/82.10
POL(false) = [1]    218.88/82.10
POL(half(x1)) = x1    218.88/82.10
POL(lastbit(x1)) = [5]    218.88/82.10
POL(s(x1)) = [4] + x1   
218.88/82.10
218.88/82.10

(70) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.88/82.10
half(s(0)) → 0 218.88/82.10
half(s(s(z0))) → s(half(z0)) 218.88/82.10
lastbit(0) → 0 218.88/82.10
lastbit(s(0)) → s(0) 218.88/82.10
lastbit(s(s(z0))) → lastbit(z0) 218.88/82.10
zero(0) → true 218.88/82.10
zero(s(z0)) → false 218.88/82.10
conv(z0) → conviter(z0, cons(0, nil)) 218.88/82.10
conviter(z0, z1) → if(zero(z0), z0, z1) 218.88/82.10
if(true, z0, z1) → z1 218.88/82.10
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(s(s(z0))))), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0))))))
S tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0)))
K tuples:

CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0))))))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

LASTBIT, CONVITER, IF, HALF

Compound Symbols:

c5, c9, c11, c11, c2, c11, c9

218.88/82.10
218.88/82.10

(71) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^3))) transformation)

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

HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0))))
We considered the (Usable) Rules:

half(s(s(z0))) → s(half(z0)) 218.88/82.10
half(0) → 0 218.88/82.10
half(s(0)) → 0 218.88/82.10
lastbit(0) → 0 218.88/82.10
lastbit(s(0)) → s(0) 218.88/82.10
lastbit(s(s(z0))) → lastbit(z0)
And the Tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(s(s(z0))))), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0))))))
The order we found is given by the following interpretation:
Polynomial interpretation : 218.88/82.10

POL(0) = 0    218.88/82.10
POL(CONVITER(x1, x2)) = x12    218.88/82.10
POL(HALF(x1)) = [1] + x1    218.88/82.10
POL(IF(x1, x2, x3)) = x1·x22    218.88/82.10
POL(LASTBIT(x1)) = 0    218.88/82.10
POL(c11(x1)) = x1    218.88/82.10
POL(c11(x1, x2)) = x1 + x2    218.88/82.10
POL(c11(x1, x2, x3)) = x1 + x2 + x3    218.88/82.10
POL(c2(x1)) = x1    218.88/82.10
POL(c5(x1)) = x1    218.88/82.10
POL(c9) = 0    218.88/82.10
POL(c9(x1)) = x1    218.88/82.10
POL(cons(x1, x2)) = 0    218.88/82.10
POL(false) = [1]    218.88/82.10
POL(half(x1)) = x1    218.88/82.10
POL(lastbit(x1)) = 0    218.88/82.10
POL(s(x1)) = [1] + x1   
218.88/82.10
218.88/82.10

(72) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.88/82.10
half(s(0)) → 0 218.88/82.10
half(s(s(z0))) → s(half(z0)) 218.88/82.10
lastbit(0) → 0 218.88/82.10
lastbit(s(0)) → s(0) 218.88/82.10
lastbit(s(s(z0))) → lastbit(z0) 218.88/82.10
zero(0) → true 218.88/82.10
zero(s(z0)) → false 218.88/82.10
conv(z0) → conviter(z0, cons(0, nil)) 218.88/82.10
conviter(z0, z1) → if(zero(z0), z0, z1) 218.88/82.10
if(true, z0, z1) → z1 218.88/82.10
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(s(s(z0))))), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0))))))
S tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0)))
K tuples:

CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0))))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

LASTBIT, CONVITER, IF, HALF

Compound Symbols:

c5, c9, c11, c11, c2, c11, c9

218.88/82.10
218.88/82.10

(73) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)

Used rewriting to replace IF(false, s(s(s(s(z0)))), x1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(s(s(z0))))), x1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) by IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(z0))), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0))))))
218.88/82.10
218.88/82.10

(74) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.88/82.10
half(s(0)) → 0 218.88/82.10
half(s(s(z0))) → s(half(z0)) 218.88/82.10
lastbit(0) → 0 218.88/82.10
lastbit(s(0)) → s(0) 218.88/82.10
lastbit(s(s(z0))) → lastbit(z0) 218.88/82.10
zero(0) → true 218.88/82.10
zero(s(z0)) → false 218.88/82.10
conv(z0) → conviter(z0, cons(0, nil)) 218.88/82.10
conviter(z0, z1) → if(zero(z0), z0, z1) 218.88/82.10
if(true, z0, z1) → z1 218.88/82.10
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(z0))), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0))))))
S tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0)))
K tuples:

CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0))))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

LASTBIT, CONVITER, IF, HALF

Compound Symbols:

c5, c9, c11, c11, c2, c11, c9

218.88/82.10
218.88/82.10

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

Removed 2 trailing nodes:

CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0)))
218.88/82.10
218.88/82.10

(76) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.88/82.10
half(s(0)) → 0 218.88/82.10
half(s(s(z0))) → s(half(z0)) 218.88/82.10
lastbit(0) → 0 218.88/82.10
lastbit(s(0)) → s(0) 218.88/82.10
lastbit(s(s(z0))) → lastbit(z0) 218.88/82.10
zero(0) → true 218.88/82.10
zero(s(z0)) → false 218.88/82.10
conv(z0) → conviter(z0, cons(0, nil)) 218.88/82.10
conviter(z0, z1) → if(zero(z0), z0, z1) 218.88/82.10
if(true, z0, z1) → z1 218.88/82.10
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(z0))), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0))))))
S tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0)))
K tuples:

CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0))))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

LASTBIT, CONVITER, IF, HALF

Compound Symbols:

c5, c9, c11, c11, c2, c11, c9

218.88/82.10
218.88/82.10

(77) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)

Used rewriting to replace IF(false, s(s(0)), x1) → c11(CONVITER(half(s(s(0))), cons(0, x1)), LASTBIT(s(s(0)))) by IF(false, s(s(0)), z0) → c11(CONVITER(s(half(0)), cons(0, z0)), LASTBIT(s(s(0))))
218.88/82.10
218.88/82.10

(78) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.88/82.10
half(s(0)) → 0 218.88/82.10
half(s(s(z0))) → s(half(z0)) 218.88/82.10
lastbit(0) → 0 218.88/82.10
lastbit(s(0)) → s(0) 218.88/82.10
lastbit(s(s(z0))) → lastbit(z0) 218.88/82.10
zero(0) → true 218.88/82.10
zero(s(z0)) → false 218.88/82.10
conv(z0) → conviter(z0, cons(0, nil)) 218.88/82.10
conviter(z0, z1) → if(zero(z0), z0, z1) 218.88/82.10
if(true, z0, z1) → z1 218.88/82.10
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(z0))), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(s(0)), z0) → c11(CONVITER(s(half(0)), cons(0, z0)), LASTBIT(s(s(0))))
S tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0))) 218.88/82.10
IF(false, s(s(0)), z0) → c11(CONVITER(s(half(0)), cons(0, z0)), LASTBIT(s(s(0))))
K tuples:

CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0))))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

LASTBIT, CONVITER, IF, HALF

Compound Symbols:

c5, c9, c11, c11, c2, c11, c9

218.88/82.10
218.88/82.10

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

Removed 2 trailing nodes:

CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0)))
218.88/82.10
218.88/82.10

(80) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.88/82.10
half(s(0)) → 0 218.88/82.10
half(s(s(z0))) → s(half(z0)) 218.88/82.10
lastbit(0) → 0 218.88/82.10
lastbit(s(0)) → s(0) 218.88/82.10
lastbit(s(s(z0))) → lastbit(z0) 218.88/82.10
zero(0) → true 218.88/82.10
zero(s(z0)) → false 218.88/82.10
conv(z0) → conviter(z0, cons(0, nil)) 218.88/82.10
conviter(z0, z1) → if(zero(z0), z0, z1) 218.88/82.10
if(true, z0, z1) → z1 218.88/82.10
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(z0))), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(s(0)), z0) → c11(CONVITER(s(half(0)), cons(0, z0)), LASTBIT(s(s(0))))
S tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0))) 218.88/82.10
IF(false, s(s(0)), z0) → c11(CONVITER(s(half(0)), cons(0, z0)), LASTBIT(s(s(0))))
K tuples:

CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0))))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

LASTBIT, CONVITER, IF, HALF

Compound Symbols:

c5, c9, c11, c11, c2, c11, c9

218.88/82.10
218.88/82.10

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

IF(false, s(s(0)), z0) → c11(CONVITER(s(half(0)), cons(0, z0)), LASTBIT(s(s(0))))
We considered the (Usable) Rules:

half(0) → 0 218.88/82.10
half(s(0)) → 0 218.88/82.10
half(s(s(z0))) → s(half(z0)) 218.88/82.10
lastbit(s(s(z0))) → lastbit(z0) 218.88/82.10
lastbit(0) → 0 218.88/82.10
lastbit(s(0)) → s(0)
And the Tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(z0))), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(s(0)), z0) → c11(CONVITER(s(half(0)), cons(0, z0)), LASTBIT(s(s(0))))
The order we found is given by the following interpretation:
Polynomial interpretation : 218.88/82.10

POL(0) = [2]    218.88/82.10
POL(CONVITER(x1, x2)) = [2] + [2]x1    218.88/82.10
POL(HALF(x1)) = 0    218.88/82.10
POL(IF(x1, x2, x3)) = [2] + [2]x2    218.88/82.10
POL(LASTBIT(x1)) = 0    218.88/82.10
POL(c11(x1)) = x1    218.88/82.10
POL(c11(x1, x2)) = x1 + x2    218.88/82.10
POL(c11(x1, x2, x3)) = x1 + x2 + x3    218.88/82.10
POL(c2(x1)) = x1    218.88/82.10
POL(c5(x1)) = x1    218.88/82.10
POL(c9) = 0    218.88/82.10
POL(c9(x1)) = x1    218.88/82.10
POL(cons(x1, x2)) = x2    218.88/82.10
POL(false) = [1]    218.88/82.10
POL(half(x1)) = x1    218.88/82.10
POL(lastbit(x1)) = [5]    218.88/82.10
POL(s(x1)) = [1] + x1   
218.88/82.10
218.88/82.10

(82) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.88/82.10
half(s(0)) → 0 218.88/82.10
half(s(s(z0))) → s(half(z0)) 218.88/82.10
lastbit(0) → 0 218.88/82.10
lastbit(s(0)) → s(0) 218.88/82.10
lastbit(s(s(z0))) → lastbit(z0) 218.88/82.10
zero(0) → true 218.88/82.10
zero(s(z0)) → false 218.88/82.10
conv(z0) → conviter(z0, cons(0, nil)) 218.88/82.10
conviter(z0, z1) → if(zero(z0), z0, z1) 218.88/82.10
if(true, z0, z1) → z1 218.88/82.10
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(z0))), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(s(0)), z0) → c11(CONVITER(s(half(0)), cons(0, z0)), LASTBIT(s(s(0))))
S tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0)))
K tuples:

CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(0)), z0) → c11(CONVITER(s(half(0)), cons(0, z0)), LASTBIT(s(s(0))))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

LASTBIT, CONVITER, IF, HALF

Compound Symbols:

c5, c9, c11, c11, c2, c11, c9

218.88/82.10
218.88/82.10

(83) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)

Used rewriting to replace IF(false, s(s(s(0))), x1) → c11(CONVITER(half(s(s(s(0)))), cons(s(0), x1)), LASTBIT(s(s(s(0))))) by IF(false, s(s(s(0))), z0) → c11(CONVITER(s(half(s(0))), cons(s(0), z0)), LASTBIT(s(s(s(0)))))
218.88/82.10
218.88/82.10

(84) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.88/82.10
half(s(0)) → 0 218.88/82.10
half(s(s(z0))) → s(half(z0)) 218.88/82.10
lastbit(0) → 0 218.88/82.10
lastbit(s(0)) → s(0) 218.88/82.10
lastbit(s(s(z0))) → lastbit(z0) 218.88/82.10
zero(0) → true 218.88/82.10
zero(s(z0)) → false 218.88/82.10
conv(z0) → conviter(z0, cons(0, nil)) 218.88/82.10
conviter(z0, z1) → if(zero(z0), z0, z1) 218.88/82.10
if(true, z0, z1) → z1 218.88/82.10
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(z0))), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(s(0)), z0) → c11(CONVITER(s(half(0)), cons(0, z0)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), z0) → c11(CONVITER(s(half(s(0))), cons(s(0), z0)), LASTBIT(s(s(s(0)))))
S tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0))) 218.88/82.10
IF(false, s(s(s(0))), z0) → c11(CONVITER(s(half(s(0))), cons(s(0), z0)), LASTBIT(s(s(s(0)))))
K tuples:

CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(0)), z0) → c11(CONVITER(s(half(0)), cons(0, z0)), LASTBIT(s(s(0))))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

LASTBIT, CONVITER, IF, HALF

Compound Symbols:

c5, c9, c11, c11, c2, c11, c9

218.88/82.10
218.88/82.10

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

Removed 2 trailing nodes:

CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0)))
218.88/82.10
218.88/82.10

(86) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.88/82.10
half(s(0)) → 0 218.88/82.10
half(s(s(z0))) → s(half(z0)) 218.88/82.10
lastbit(0) → 0 218.88/82.10
lastbit(s(0)) → s(0) 218.88/82.10
lastbit(s(s(z0))) → lastbit(z0) 218.88/82.10
zero(0) → true 218.88/82.10
zero(s(z0)) → false 218.88/82.10
conv(z0) → conviter(z0, cons(0, nil)) 218.88/82.10
conviter(z0, z1) → if(zero(z0), z0, z1) 218.88/82.10
if(true, z0, z1) → z1 218.88/82.10
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(z0))), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(s(0)), z0) → c11(CONVITER(s(half(0)), cons(0, z0)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), z0) → c11(CONVITER(s(half(s(0))), cons(s(0), z0)), LASTBIT(s(s(s(0)))))
S tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0))) 218.88/82.10
IF(false, s(s(s(0))), z0) → c11(CONVITER(s(half(s(0))), cons(s(0), z0)), LASTBIT(s(s(s(0)))))
K tuples:

CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(0)), z0) → c11(CONVITER(s(half(0)), cons(0, z0)), LASTBIT(s(s(0))))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

LASTBIT, CONVITER, IF, HALF

Compound Symbols:

c5, c9, c11, c11, c2, c11, c9

218.88/82.10
218.88/82.10

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

IF(false, s(s(s(0))), z0) → c11(CONVITER(s(half(s(0))), cons(s(0), z0)), LASTBIT(s(s(s(0)))))
We considered the (Usable) Rules:

half(s(0)) → 0 218.88/82.10
half(0) → 0 218.88/82.10
half(s(s(z0))) → s(half(z0)) 218.88/82.10
lastbit(s(s(z0))) → lastbit(z0) 218.88/82.10
lastbit(0) → 0 218.88/82.10
lastbit(s(0)) → s(0)
And the Tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(z0))), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(s(0)), z0) → c11(CONVITER(s(half(0)), cons(0, z0)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), z0) → c11(CONVITER(s(half(s(0))), cons(s(0), z0)), LASTBIT(s(s(s(0)))))
The order we found is given by the following interpretation:
Polynomial interpretation : 218.88/82.10

POL(0) = [2]    218.88/82.10
POL(CONVITER(x1, x2)) = [2]x1    218.88/82.10
POL(HALF(x1)) = 0    218.88/82.10
POL(IF(x1, x2, x3)) = [2]x2    218.88/82.10
POL(LASTBIT(x1)) = 0    218.88/82.10
POL(c11(x1)) = x1    218.88/82.10
POL(c11(x1, x2)) = x1 + x2    218.88/82.10
POL(c11(x1, x2, x3)) = x1 + x2 + x3    218.88/82.10
POL(c2(x1)) = x1    218.88/82.10
POL(c5(x1)) = x1    218.88/82.10
POL(c9) = 0    218.88/82.10
POL(c9(x1)) = x1    218.88/82.10
POL(cons(x1, x2)) = x2    218.88/82.10
POL(false) = [1]    218.88/82.10
POL(half(x1)) = x1    218.88/82.10
POL(lastbit(x1)) = [5]    218.88/82.10
POL(s(x1)) = [2] + x1   
218.88/82.10
218.88/82.10

(88) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.88/82.10
half(s(0)) → 0 218.88/82.10
half(s(s(z0))) → s(half(z0)) 218.88/82.10
lastbit(0) → 0 218.88/82.10
lastbit(s(0)) → s(0) 218.88/82.10
lastbit(s(s(z0))) → lastbit(z0) 218.88/82.10
zero(0) → true 218.88/82.10
zero(s(z0)) → false 218.88/82.10
conv(z0) → conviter(z0, cons(0, nil)) 218.88/82.10
conviter(z0, z1) → if(zero(z0), z0, z1) 218.88/82.10
if(true, z0, z1) → z1 218.88/82.10
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(z0))), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(s(0)), z0) → c11(CONVITER(s(half(0)), cons(0, z0)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), z0) → c11(CONVITER(s(half(s(0))), cons(s(0), z0)), LASTBIT(s(s(s(0)))))
S tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0)))
K tuples:

CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(0)), z0) → c11(CONVITER(s(half(0)), cons(0, z0)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), z0) → c11(CONVITER(s(half(s(0))), cons(s(0), z0)), LASTBIT(s(s(s(0)))))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

LASTBIT, CONVITER, IF, HALF

Compound Symbols:

c5, c9, c11, c11, c2, c11, c9

218.88/82.10
218.88/82.10

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

CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0)))
We considered the (Usable) Rules:

half(s(0)) → 0 218.88/82.10
half(0) → 0 218.88/82.10
half(s(s(z0))) → s(half(z0)) 218.88/82.10
lastbit(s(s(z0))) → lastbit(z0) 218.88/82.10
lastbit(0) → 0 218.88/82.10
lastbit(s(0)) → s(0)
And the Tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(z0))), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(s(0)), z0) → c11(CONVITER(s(half(0)), cons(0, z0)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), z0) → c11(CONVITER(s(half(s(0))), cons(s(0), z0)), LASTBIT(s(s(s(0)))))
The order we found is given by the following interpretation:
Polynomial interpretation : 218.88/82.10

POL(0) = 0    218.88/82.10
POL(CONVITER(x1, x2)) = x1 + x2    218.88/82.10
POL(HALF(x1)) = 0    218.88/82.10
POL(IF(x1, x2, x3)) = x2    218.88/82.10
POL(LASTBIT(x1)) = 0    218.88/82.10
POL(c11(x1)) = x1    218.88/82.10
POL(c11(x1, x2)) = x1 + x2    218.88/82.10
POL(c11(x1, x2, x3)) = x1 + x2 + x3    218.88/82.10
POL(c2(x1)) = x1    218.88/82.10
POL(c5(x1)) = x1    218.88/82.10
POL(c9) = 0    218.88/82.10
POL(c9(x1)) = x1    218.88/82.10
POL(cons(x1, x2)) = [1]    218.88/82.10
POL(false) = [1]    218.88/82.10
POL(half(x1)) = x1    218.88/82.10
POL(lastbit(x1)) = [5]    218.88/82.10
POL(s(x1)) = [1] + x1   
218.88/82.10
218.88/82.10

(90) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.88/82.10
half(s(0)) → 0 218.88/82.10
half(s(s(z0))) → s(half(z0)) 218.88/82.10
lastbit(0) → 0 218.88/82.10
lastbit(s(0)) → s(0) 218.88/82.10
lastbit(s(s(z0))) → lastbit(z0) 218.88/82.10
zero(0) → true 218.88/82.10
zero(s(z0)) → false 218.88/82.10
conv(z0) → conviter(z0, cons(0, nil)) 218.88/82.10
conviter(z0, z1) → if(zero(z0), z0, z1) 218.88/82.10
if(true, z0, z1) → z1 218.88/82.10
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(z0))), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(s(0)), z0) → c11(CONVITER(s(half(0)), cons(0, z0)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), z0) → c11(CONVITER(s(half(s(0))), cons(s(0), z0)), LASTBIT(s(s(s(0)))))
S tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0))
K tuples:

CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(0)), z0) → c11(CONVITER(s(half(0)), cons(0, z0)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), z0) → c11(CONVITER(s(half(s(0))), cons(s(0), z0)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0)))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

LASTBIT, CONVITER, IF, HALF

Compound Symbols:

c5, c9, c11, c11, c2, c11, c9

218.88/82.10
218.88/82.10

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

LASTBIT(s(s(z0))) → c5(LASTBIT(z0))
We considered the (Usable) Rules:

half(s(0)) → 0 218.88/82.10
half(0) → 0 218.88/82.10
half(s(s(z0))) → s(half(z0)) 218.88/82.10
lastbit(s(s(z0))) → lastbit(z0) 218.88/82.10
lastbit(0) → 0 218.88/82.10
lastbit(s(0)) → s(0)
And the Tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(z0))), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(s(0)), z0) → c11(CONVITER(s(half(0)), cons(0, z0)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), z0) → c11(CONVITER(s(half(s(0))), cons(s(0), z0)), LASTBIT(s(s(s(0)))))
The order we found is given by the following interpretation:
Polynomial interpretation : 218.88/82.10

POL(0) = [3]    218.88/82.10
POL(CONVITER(x1, x2)) = [1] + x12    218.88/82.10
POL(HALF(x1)) = 0    218.88/82.10
POL(IF(x1, x2, x3)) = [3]x1 + [3]x12 + x22    218.88/82.10
POL(LASTBIT(x1)) = x1    218.88/82.10
POL(c11(x1)) = x1    218.88/82.10
POL(c11(x1, x2)) = x1 + x2    218.88/82.10
POL(c11(x1, x2, x3)) = x1 + x2 + x3    218.88/82.10
POL(c2(x1)) = x1    218.88/82.10
POL(c5(x1)) = x1    218.88/82.10
POL(c9) = 0    218.88/82.10
POL(c9(x1)) = x1    218.88/82.10
POL(cons(x1, x2)) = 0    218.88/82.10
POL(false) = 0    218.88/82.10
POL(half(x1)) = x1    218.88/82.10
POL(lastbit(x1)) = 0    218.88/82.10
POL(s(x1)) = [1] + x1   
218.88/82.10
218.88/82.10

(92) Obligation:

Complexity Dependency Tuples Problem
Rules:

half(0) → 0 218.88/82.10
half(s(0)) → 0 218.88/82.10
half(s(s(z0))) → s(half(z0)) 218.88/82.10
lastbit(0) → 0 218.88/82.10
lastbit(s(0)) → s(0) 218.88/82.10
lastbit(s(s(z0))) → lastbit(z0) 218.88/82.10
zero(0) → true 218.88/82.10
zero(s(z0)) → false 218.88/82.10
conv(z0) → conviter(z0, cons(0, nil)) 218.88/82.10
conviter(z0, z1) → if(zero(z0), z0, z1) 218.88/82.10
if(true, z0, z1) → z1 218.88/82.10
if(false, z0, z1) → conviter(half(z0), cons(lastbit(z0), z1))
Tuples:

LASTBIT(s(s(z0))) → c5(LASTBIT(z0)) 218.88/82.10
CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(0)), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(0))), x1)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), x1) → c11(CONVITER(s(0), cons(lastbit(s(s(s(0)))), x1)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(s(half(z0))), cons(lastbit(s(s(z0))), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
IF(false, s(s(0)), z0) → c11(CONVITER(s(half(0)), cons(0, z0)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), z0) → c11(CONVITER(s(half(s(0))), cons(s(0), z0)), LASTBIT(s(s(s(0)))))
S tuples:none
K tuples:

CONVITER(0, x1) → c9 218.88/82.10
IF(false, s(s(z0)), x1) → c11(CONVITER(s(half(z0)), cons(lastbit(z0), x1)), HALF(s(s(z0))), LASTBIT(s(s(z0)))) 218.88/82.10
IF(false, s(0), x0) → c11(CONVITER(0, cons(s(0), x0))) 218.88/82.10
IF(false, s(s(s(s(z0)))), z1) → c11(CONVITER(s(half(s(s(z0)))), cons(lastbit(z0), z1)), HALF(s(s(s(s(z0))))), LASTBIT(s(s(s(s(z0)))))) 218.88/82.10
HALF(s(s(s(s(y0))))) → c2(HALF(s(s(y0)))) 218.88/82.10
IF(false, s(s(0)), z0) → c11(CONVITER(s(half(0)), cons(0, z0)), LASTBIT(s(s(0)))) 218.88/82.10
IF(false, s(s(s(0))), z0) → c11(CONVITER(s(half(s(0))), cons(s(0), z0)), LASTBIT(s(s(s(0))))) 218.88/82.10
CONVITER(s(z0), cons(y1, x1)) → c9(IF(false, s(z0), cons(y1, x1))) 218.88/82.10
CONVITER(s(s(y0)), cons(y1, x1)) → c9(IF(false, s(s(y0)), cons(y1, x1))) 218.88/82.10
CONVITER(s(z0), cons(0, x0)) → c9(IF(false, s(z0), cons(0, x0))) 218.88/82.10
CONVITER(s(z0), cons(s(0), x0)) → c9(IF(false, s(z0), cons(s(0), x0))) 218.88/82.10
CONVITER(s(0), cons(y0, x0)) → c9(IF(false, s(0), cons(y0, x0))) 218.88/82.10
LASTBIT(s(s(z0))) → c5(LASTBIT(z0))
Defined Rule Symbols:

half, lastbit, zero, conv, conviter, if

Defined Pair Symbols:

LASTBIT, CONVITER, IF, HALF

Compound Symbols:

c5, c9, c11, c11, c2, c11, c9

218.88/82.10
218.88/82.10

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

The set S is empty
218.88/82.10
218.88/82.10

(94) BOUNDS(O(1), O(1))

218.88/82.10
218.88/82.10
218.88/82.14 EOF