WORST_CASE(Omega(n^1),O(n^1))
proof of input_t89NxiWvHU.trs
# AProVE Commit ID: 5b976082cb74a395683ed8cc7acf94bd611ab29f fuhs 20230524 unpublished


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

(0) CpxTRS
(1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(2) CdtProblem
    (3) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms]
    (4) CdtProblem
    (5) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
    (6) CdtProblem
    (7) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CdtProblem
    (9) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (10) CpxRelTRS
    (11) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (12) CpxWeightedTrs
    (13) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (14) CpxTypedWeightedTrs
    (15) CompletionProof [UPPER BOUND(ID), 0 ms]
    (16) CpxTypedWeightedCompleteTrs
    (17) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
    (18) CpxRNTS
    (19) CompleteCoflocoProof [FINISHED, 1268 ms]
    (20) BOUNDS(1, n^1)
(21) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(22) CdtProblem
    (23) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (24) CpxRelTRS
    (25) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (26) CpxRelTRS
    (27) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (28) typed CpxTrs
    (29) OrderProof [LOWER BOUND(ID), 10 ms]
    (30) typed CpxTrs
    (31) RewriteLemmaProof [LOWER BOUND(ID), 343 ms]
    (32) BEST
        (33) proven lower bound
            (34) LowerBoundPropagationProof [FINISHED, 0 ms]
            (35) BOUNDS(n^1, INF)
        (36) typed CpxTrs
            (37) RewriteLemmaProof [LOWER BOUND(ID), 73 ms]
            (38) typed CpxTrs
            (39) RewriteLemmaProof [LOWER BOUND(ID), 30 ms]
            (40) typed CpxTrs
            (41) RewriteLemmaProof [LOWER BOUND(ID), 67 ms]
            (42) typed CpxTrs


----------------------------------------

(0)
Obligation:
The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, n^1).


The TRS R consists of the following rules:

   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   lastbit(0) -> 0
   lastbit(s(0)) -> s(0)
   lastbit(s(s(x))) -> lastbit(x)
   zero(0) -> true
   zero(s(x)) -> false
   conv(x) -> conviter(x, cons(0, nil))
   conviter(x, l) -> if(zero(x), x, l)
   if(true, x, l) -> l
   if(false, x, l) -> conviter(half(x), cons(lastbit(x), l))

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) CpxTrsToCdtProof (UPPER BOUND(ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(z0))) -> s(half(z0))
   lastbit(0) -> 0
   lastbit(s(0)) -> s(0)
   lastbit(s(s(z0))) -> lastbit(z0)
   zero(0) -> true
   zero(s(z0)) -> false
   conv(z0) -> conviter(z0, cons(0, nil))
   conviter(z0, z1) -> if(zero(z0), z0, z1)
   if(true, z0, z1) -> z1
   if(false, z0, z1) -> conviter(half(z0), cons(lastbit(z0), z1))
Tuples:
   HALF(0) -> c
   HALF(s(0)) -> c1
   HALF(s(s(z0))) -> c2(HALF(z0))
   LASTBIT(0) -> c3
   LASTBIT(s(0)) -> c4
   LASTBIT(s(s(z0))) -> c5(LASTBIT(z0))
   ZERO(0) -> c6
   ZERO(s(z0)) -> c7
   CONV(z0) -> c8(CONVITER(z0, cons(0, nil)))
   CONVITER(z0, z1) -> c9(IF(zero(z0), z0, z1), ZERO(z0))
   IF(true, z0, z1) -> c10
   IF(false, z0, z1) -> c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0))
   IF(false, z0, z1) -> c12(CONVITER(half(z0), cons(lastbit(z0), z1)), LASTBIT(z0))
S tuples:
   HALF(0) -> c
   HALF(s(0)) -> c1
   HALF(s(s(z0))) -> c2(HALF(z0))
   LASTBIT(0) -> c3
   LASTBIT(s(0)) -> c4
   LASTBIT(s(s(z0))) -> c5(LASTBIT(z0))
   ZERO(0) -> c6
   ZERO(s(z0)) -> c7
   CONV(z0) -> c8(CONVITER(z0, cons(0, nil)))
   CONVITER(z0, z1) -> c9(IF(zero(z0), z0, z1), ZERO(z0))
   IF(true, z0, z1) -> c10
   IF(false, z0, z1) -> c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0))
   IF(false, z0, z1) -> c12(CONVITER(half(z0), cons(lastbit(z0), z1)), LASTBIT(z0))
K tuples:none
Defined Rule Symbols:   half_1, lastbit_1, zero_1, conv_1, conviter_2, if_3

Defined Pair Symbols:   HALF_1, LASTBIT_1, ZERO_1, CONV_1, CONVITER_2, IF_3

Compound Symbols:   c, c1, c2_1, c3, c4, c5_1, c6, c7, c8_1, c9_2, c10, c11_2, c12_2


----------------------------------------

(3) CdtLeafRemovalProof (ComplexityIfPolyImplication)
Removed 1 leading nodes:
   CONV(z0) -> c8(CONVITER(z0, cons(0, nil)))
Removed 7 trailing nodes:
   ZERO(0) -> c6
   LASTBIT(0) -> c3
   IF(true, z0, z1) -> c10
   HALF(0) -> c
   ZERO(s(z0)) -> c7
   HALF(s(0)) -> c1
   LASTBIT(s(0)) -> c4

----------------------------------------

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(z0))) -> s(half(z0))
   lastbit(0) -> 0
   lastbit(s(0)) -> s(0)
   lastbit(s(s(z0))) -> lastbit(z0)
   zero(0) -> true
   zero(s(z0)) -> false
   conv(z0) -> conviter(z0, cons(0, nil))
   conviter(z0, z1) -> if(zero(z0), z0, z1)
   if(true, z0, z1) -> z1
   if(false, z0, z1) -> conviter(half(z0), cons(lastbit(z0), z1))
Tuples:
   HALF(s(s(z0))) -> c2(HALF(z0))
   LASTBIT(s(s(z0))) -> c5(LASTBIT(z0))
   CONVITER(z0, z1) -> c9(IF(zero(z0), z0, z1), ZERO(z0))
   IF(false, z0, z1) -> c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0))
   IF(false, z0, z1) -> c12(CONVITER(half(z0), cons(lastbit(z0), z1)), LASTBIT(z0))
S tuples:
   HALF(s(s(z0))) -> c2(HALF(z0))
   LASTBIT(s(s(z0))) -> c5(LASTBIT(z0))
   CONVITER(z0, z1) -> c9(IF(zero(z0), z0, z1), ZERO(z0))
   IF(false, z0, z1) -> c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0))
   IF(false, z0, z1) -> c12(CONVITER(half(z0), cons(lastbit(z0), z1)), LASTBIT(z0))
K tuples:none
Defined Rule Symbols:   half_1, lastbit_1, zero_1, conv_1, conviter_2, if_3

Defined Pair Symbols:   HALF_1, LASTBIT_1, CONVITER_2, IF_3

Compound Symbols:   c2_1, c5_1, c9_2, c11_2, c12_2


----------------------------------------

(5) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
Removed 1 trailing tuple parts
----------------------------------------

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(z0))) -> s(half(z0))
   lastbit(0) -> 0
   lastbit(s(0)) -> s(0)
   lastbit(s(s(z0))) -> lastbit(z0)
   zero(0) -> true
   zero(s(z0)) -> false
   conv(z0) -> conviter(z0, cons(0, nil))
   conviter(z0, z1) -> if(zero(z0), z0, z1)
   if(true, z0, z1) -> z1
   if(false, z0, z1) -> conviter(half(z0), cons(lastbit(z0), z1))
Tuples:
   HALF(s(s(z0))) -> c2(HALF(z0))
   LASTBIT(s(s(z0))) -> c5(LASTBIT(z0))
   IF(false, z0, z1) -> c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0))
   IF(false, z0, z1) -> c12(CONVITER(half(z0), cons(lastbit(z0), z1)), LASTBIT(z0))
   CONVITER(z0, z1) -> c9(IF(zero(z0), z0, z1))
S tuples:
   HALF(s(s(z0))) -> c2(HALF(z0))
   LASTBIT(s(s(z0))) -> c5(LASTBIT(z0))
   IF(false, z0, z1) -> c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0))
   IF(false, z0, z1) -> c12(CONVITER(half(z0), cons(lastbit(z0), z1)), LASTBIT(z0))
   CONVITER(z0, z1) -> c9(IF(zero(z0), z0, z1))
K tuples:none
Defined Rule Symbols:   half_1, lastbit_1, zero_1, conv_1, conviter_2, if_3

Defined Pair Symbols:   HALF_1, LASTBIT_1, IF_3, CONVITER_2

Compound Symbols:   c2_1, c5_1, c11_2, c12_2, c9_1


----------------------------------------

(7) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   conv(z0) -> conviter(z0, cons(0, nil))
   conviter(z0, z1) -> if(zero(z0), z0, z1)
   if(true, z0, z1) -> z1
   if(false, z0, z1) -> conviter(half(z0), cons(lastbit(z0), z1))

----------------------------------------

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(z0))) -> s(half(z0))
   lastbit(0) -> 0
   lastbit(s(0)) -> s(0)
   lastbit(s(s(z0))) -> lastbit(z0)
   zero(0) -> true
   zero(s(z0)) -> false
Tuples:
   HALF(s(s(z0))) -> c2(HALF(z0))
   LASTBIT(s(s(z0))) -> c5(LASTBIT(z0))
   IF(false, z0, z1) -> c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0))
   IF(false, z0, z1) -> c12(CONVITER(half(z0), cons(lastbit(z0), z1)), LASTBIT(z0))
   CONVITER(z0, z1) -> c9(IF(zero(z0), z0, z1))
S tuples:
   HALF(s(s(z0))) -> c2(HALF(z0))
   LASTBIT(s(s(z0))) -> c5(LASTBIT(z0))
   IF(false, z0, z1) -> c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0))
   IF(false, z0, z1) -> c12(CONVITER(half(z0), cons(lastbit(z0), z1)), LASTBIT(z0))
   CONVITER(z0, z1) -> c9(IF(zero(z0), z0, z1))
K tuples:none
Defined Rule Symbols:   half_1, lastbit_1, zero_1

Defined Pair Symbols:   HALF_1, LASTBIT_1, IF_3, CONVITER_2

Compound Symbols:   c2_1, c5_1, c11_2, c12_2, c9_1


----------------------------------------

(9) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

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


The TRS R consists of the following rules:

   HALF(s(s(z0))) -> c2(HALF(z0))
   LASTBIT(s(s(z0))) -> c5(LASTBIT(z0))
   IF(false, z0, z1) -> c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0))
   IF(false, z0, z1) -> c12(CONVITER(half(z0), cons(lastbit(z0), z1)), LASTBIT(z0))
   CONVITER(z0, z1) -> c9(IF(zero(z0), z0, z1))

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

   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(z0))) -> s(half(z0))
   lastbit(0) -> 0
   lastbit(s(0)) -> s(0)
   lastbit(s(s(z0))) -> lastbit(z0)
   zero(0) -> true
   zero(s(z0)) -> false

Rewrite Strategy: INNERMOST
----------------------------------------

(11) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID))
Transformed relative TRS to weighted TRS
----------------------------------------

(12)
Obligation:
The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

   HALF(s(s(z0))) -> c2(HALF(z0)) [1]
   LASTBIT(s(s(z0))) -> c5(LASTBIT(z0)) [1]
   IF(false, z0, z1) -> c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0)) [1]
   IF(false, z0, z1) -> c12(CONVITER(half(z0), cons(lastbit(z0), z1)), LASTBIT(z0)) [1]
   CONVITER(z0, z1) -> c9(IF(zero(z0), z0, z1)) [1]
   half(0) -> 0 [0]
   half(s(0)) -> 0 [0]
   half(s(s(z0))) -> s(half(z0)) [0]
   lastbit(0) -> 0 [0]
   lastbit(s(0)) -> s(0) [0]
   lastbit(s(s(z0))) -> lastbit(z0) [0]
   zero(0) -> true [0]
   zero(s(z0)) -> false [0]

Rewrite Strategy: INNERMOST
----------------------------------------

(13) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Infered types.
----------------------------------------

(14)
Obligation:
Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   HALF(s(s(z0))) -> c2(HALF(z0)) [1]
   LASTBIT(s(s(z0))) -> c5(LASTBIT(z0)) [1]
   IF(false, z0, z1) -> c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0)) [1]
   IF(false, z0, z1) -> c12(CONVITER(half(z0), cons(lastbit(z0), z1)), LASTBIT(z0)) [1]
   CONVITER(z0, z1) -> c9(IF(zero(z0), z0, z1)) [1]
   half(0) -> 0 [0]
   half(s(0)) -> 0 [0]
   half(s(s(z0))) -> s(half(z0)) [0]
   lastbit(0) -> 0 [0]
   lastbit(s(0)) -> s(0) [0]
   lastbit(s(s(z0))) -> lastbit(z0) [0]
   zero(0) -> true [0]
   zero(s(z0)) -> false [0]

The TRS has the following type information:
HALF :: s:0 -> c2
s :: s:0 -> s:0
c2 :: c2 -> c2
LASTBIT :: s:0 -> c5
c5 :: c5 -> c5
IF :: false:true -> s:0 -> cons -> c11:c12
false :: false:true
c11 :: c9 -> c2 -> c11:c12
CONVITER :: s:0 -> cons -> c9
half :: s:0 -> s:0
cons :: s:0 -> cons -> cons
lastbit :: s:0 -> s:0
c12 :: c9 -> c5 -> c11:c12
c9 :: c11:c12 -> c9
zero :: s:0 -> false:true
0 :: s:0
true :: false:true

Rewrite Strategy: INNERMOST
----------------------------------------

(15) CompletionProof (UPPER BOUND(ID))
The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:

   half(v0) -> null_half [0]
   lastbit(v0) -> null_lastbit [0]
   zero(v0) -> null_zero [0]
   HALF(v0) -> null_HALF [0]
   LASTBIT(v0) -> null_LASTBIT [0]
   IF(v0, v1, v2) -> null_IF [0]

And the following fresh constants:    null_half, null_lastbit, null_zero, null_HALF, null_LASTBIT, null_IF, const, const1

----------------------------------------

(16)
Obligation:
Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   HALF(s(s(z0))) -> c2(HALF(z0)) [1]
   LASTBIT(s(s(z0))) -> c5(LASTBIT(z0)) [1]
   IF(false, z0, z1) -> c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0)) [1]
   IF(false, z0, z1) -> c12(CONVITER(half(z0), cons(lastbit(z0), z1)), LASTBIT(z0)) [1]
   CONVITER(z0, z1) -> c9(IF(zero(z0), z0, z1)) [1]
   half(0) -> 0 [0]
   half(s(0)) -> 0 [0]
   half(s(s(z0))) -> s(half(z0)) [0]
   lastbit(0) -> 0 [0]
   lastbit(s(0)) -> s(0) [0]
   lastbit(s(s(z0))) -> lastbit(z0) [0]
   zero(0) -> true [0]
   zero(s(z0)) -> false [0]
   half(v0) -> null_half [0]
   lastbit(v0) -> null_lastbit [0]
   zero(v0) -> null_zero [0]
   HALF(v0) -> null_HALF [0]
   LASTBIT(v0) -> null_LASTBIT [0]
   IF(v0, v1, v2) -> null_IF [0]

The TRS has the following type information:
HALF :: s:0:null_half:null_lastbit -> c2:null_HALF
s :: s:0:null_half:null_lastbit -> s:0:null_half:null_lastbit
c2 :: c2:null_HALF -> c2:null_HALF
LASTBIT :: s:0:null_half:null_lastbit -> c5:null_LASTBIT
c5 :: c5:null_LASTBIT -> c5:null_LASTBIT
IF :: false:true:null_zero -> s:0:null_half:null_lastbit -> cons -> c11:c12:null_IF
false :: false:true:null_zero
c11 :: c9 -> c2:null_HALF -> c11:c12:null_IF
CONVITER :: s:0:null_half:null_lastbit -> cons -> c9
half :: s:0:null_half:null_lastbit -> s:0:null_half:null_lastbit
cons :: s:0:null_half:null_lastbit -> cons -> cons
lastbit :: s:0:null_half:null_lastbit -> s:0:null_half:null_lastbit
c12 :: c9 -> c5:null_LASTBIT -> c11:c12:null_IF
c9 :: c11:c12:null_IF -> c9
zero :: s:0:null_half:null_lastbit -> false:true:null_zero
0 :: s:0:null_half:null_lastbit
true :: false:true:null_zero
null_half :: s:0:null_half:null_lastbit
null_lastbit :: s:0:null_half:null_lastbit
null_zero :: false:true:null_zero
null_HALF :: c2:null_HALF
null_LASTBIT :: c5:null_LASTBIT
null_IF :: c11:c12:null_IF
const :: cons
const1 :: c9

Rewrite Strategy: INNERMOST
----------------------------------------

(17) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID))
Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

   false => 1
   0 => 0
   true => 2
   null_half => 0
   null_lastbit => 0
   null_zero => 0
   null_HALF => 0
   null_LASTBIT => 0
   null_IF => 0
   const => 0
   const1 => 0

----------------------------------------

(18)
Obligation:
Complexity RNTS consisting of the following rules:

   CONVITER(z, z') -{ 1 }-> 1 + IF(zero(z0), z0, z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   HALF(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   HALF(z) -{ 1 }-> 1 + HALF(z0) :|: z0 >= 0, z = 1 + (1 + z0)
   IF(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   IF(z, z', z'') -{ 1 }-> 1 + CONVITER(half(z0), 1 + lastbit(z0) + z1) + LASTBIT(z0) :|: z1 >= 0, z = 1, z0 >= 0, z' = z0, z'' = z1
   IF(z, z', z'') -{ 1 }-> 1 + CONVITER(half(z0), 1 + lastbit(z0) + z1) + HALF(z0) :|: z1 >= 0, z = 1, z0 >= 0, z' = z0, z'' = z1
   LASTBIT(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   LASTBIT(z) -{ 1 }-> 1 + LASTBIT(z0) :|: z0 >= 0, z = 1 + (1 + z0)
   half(z) -{ 0 }-> 0 :|: z = 0
   half(z) -{ 0 }-> 0 :|: z = 1 + 0
   half(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   half(z) -{ 0 }-> 1 + half(z0) :|: z0 >= 0, z = 1 + (1 + z0)
   lastbit(z) -{ 0 }-> lastbit(z0) :|: z0 >= 0, z = 1 + (1 + z0)
   lastbit(z) -{ 0 }-> 0 :|: z = 0
   lastbit(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   lastbit(z) -{ 0 }-> 1 + 0 :|: z = 1 + 0
   zero(z) -{ 0 }-> 2 :|: z = 0
   zero(z) -{ 0 }-> 1 :|: z = 1 + z0, z0 >= 0
   zero(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0

Only complete derivations are relevant for the runtime complexity.

----------------------------------------

(19) CompleteCoflocoProof (FINISHED)
Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo:

eq(start(V, V3, V4),0,[fun(V, Out)],[V >= 0]).
eq(start(V, V3, V4),0,[fun1(V, Out)],[V >= 0]).
eq(start(V, V3, V4),0,[fun2(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]).
eq(start(V, V3, V4),0,[fun3(V, V3, Out)],[V >= 0,V3 >= 0]).
eq(start(V, V3, V4),0,[half(V, Out)],[V >= 0]).
eq(start(V, V3, V4),0,[lastbit(V, Out)],[V >= 0]).
eq(start(V, V3, V4),0,[zero(V, Out)],[V >= 0]).
eq(fun(V, Out),1,[fun(V1, Ret1)],[Out = 1 + Ret1,V1 >= 0,V = 2 + V1]).
eq(fun1(V, Out),1,[fun1(V2, Ret11)],[Out = 1 + Ret11,V2 >= 0,V = 2 + V2]).
eq(fun2(V, V3, V4, Out),1,[half(V6, Ret010),lastbit(V6, Ret01101),fun3(Ret010, 1 + Ret01101 + V5, Ret01),fun(V6, Ret12)],[Out = 1 + Ret01 + Ret12,V5 >= 0,V = 1,V6 >= 0,V3 = V6,V4 = V5]).
eq(fun2(V, V3, V4, Out),1,[half(V7, Ret0101),lastbit(V7, Ret011011),fun3(Ret0101, 1 + Ret011011 + V8, Ret011),fun1(V7, Ret13)],[Out = 1 + Ret011 + Ret13,V8 >= 0,V = 1,V7 >= 0,V3 = V7,V4 = V8]).
eq(fun3(V, V3, Out),1,[zero(V9, Ret10),fun2(Ret10, V9, V10, Ret14)],[Out = 1 + Ret14,V = V9,V10 >= 0,V3 = V10,V9 >= 0]).
eq(half(V, Out),0,[],[Out = 0,V = 0]).
eq(half(V, Out),0,[],[Out = 0,V = 1]).
eq(half(V, Out),0,[half(V11, Ret15)],[Out = 1 + Ret15,V11 >= 0,V = 2 + V11]).
eq(lastbit(V, Out),0,[],[Out = 0,V = 0]).
eq(lastbit(V, Out),0,[],[Out = 1,V = 1]).
eq(lastbit(V, Out),0,[lastbit(V12, Ret)],[Out = Ret,V12 >= 0,V = 2 + V12]).
eq(zero(V, Out),0,[],[Out = 2,V = 0]).
eq(zero(V, Out),0,[],[Out = 1,V = 1 + V13,V13 >= 0]).
eq(half(V, Out),0,[],[Out = 0,V14 >= 0,V = V14]).
eq(lastbit(V, Out),0,[],[Out = 0,V15 >= 0,V = V15]).
eq(zero(V, Out),0,[],[Out = 0,V16 >= 0,V = V16]).
eq(fun(V, Out),0,[],[Out = 0,V17 >= 0,V = V17]).
eq(fun1(V, Out),0,[],[Out = 0,V18 >= 0,V = V18]).
eq(fun2(V, V3, V4, Out),0,[],[Out = 0,V19 >= 0,V4 = V21,V20 >= 0,V = V19,V3 = V20,V21 >= 0]).
input_output_vars(fun(V,Out),[V],[Out]).
input_output_vars(fun1(V,Out),[V],[Out]).
input_output_vars(fun2(V,V3,V4,Out),[V,V3,V4],[Out]).
input_output_vars(fun3(V,V3,Out),[V,V3],[Out]).
input_output_vars(half(V,Out),[V],[Out]).
input_output_vars(lastbit(V,Out),[V],[Out]).
input_output_vars(zero(V,Out),[V],[Out]).


CoFloCo proof output:
Preprocessing Cost Relations
=====================================

#### Computed strongly connected components 
0. recursive  : [fun/2]
1. recursive  : [fun1/2]
2. non_recursive  : [zero/2]
3. recursive  : [half/2]
4. recursive  : [lastbit/2]
5. recursive [non_tail] : [fun2/4,fun3/3]
6. non_recursive  : [start/3]

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into fun/2
1. SCC is partially evaluated into fun1/2
2. SCC is partially evaluated into zero/2
3. SCC is partially evaluated into half/2
4. SCC is partially evaluated into lastbit/2
5. SCC is partially evaluated into fun3/3
6. SCC is partially evaluated into start/3

Control-Flow Refinement of Cost Relations
=====================================

### Specialization of cost equations fun/2 
* CE 22 is refined into CE [26] 
* CE 21 is refined into CE [27] 


### Cost equations --> "Loop" of fun/2 
* CEs [27] --> Loop 16 
* CEs [26] --> Loop 17 

### Ranking functions of CR fun(V,Out) 
* RF of phase [16]: [V-1]

#### Partial ranking functions of CR fun(V,Out) 
* Partial RF of phase [16]:
  - RF of loop [16:1]:
    V-1


### Specialization of cost equations fun1/2 
* CE 20 is refined into CE [28] 
* CE 19 is refined into CE [29] 


### Cost equations --> "Loop" of fun1/2 
* CEs [29] --> Loop 18 
* CEs [28] --> Loop 19 

### Ranking functions of CR fun1(V,Out) 
* RF of phase [18]: [V-1]

#### Partial ranking functions of CR fun1(V,Out) 
* Partial RF of phase [18]:
  - RF of loop [18:1]:
    V-1


### Specialization of cost equations zero/2 
* CE 24 is refined into CE [30] 
* CE 25 is refined into CE [31] 
* CE 23 is refined into CE [32] 


### Cost equations --> "Loop" of zero/2 
* CEs [30] --> Loop 20 
* CEs [31] --> Loop 21 
* CEs [32] --> Loop 22 

### Ranking functions of CR zero(V,Out) 

#### Partial ranking functions of CR zero(V,Out) 


### Specialization of cost equations half/2 
* CE 10 is refined into CE [33] 
* CE 11 is refined into CE [34] 
* CE 12 is refined into CE [35] 


### Cost equations --> "Loop" of half/2 
* CEs [35] --> Loop 23 
* CEs [33,34] --> Loop 24 

### Ranking functions of CR half(V,Out) 
* RF of phase [23]: [V-1]

#### Partial ranking functions of CR half(V,Out) 
* Partial RF of phase [23]:
  - RF of loop [23:1]:
    V-1


### Specialization of cost equations lastbit/2 
* CE 13 is refined into CE [36] 
* CE 14 is refined into CE [37] 
* CE 15 is refined into CE [38] 


### Cost equations --> "Loop" of lastbit/2 
* CEs [38] --> Loop 25 
* CEs [36] --> Loop 26 
* CEs [37] --> Loop 27 

### Ranking functions of CR lastbit(V,Out) 
* RF of phase [25]: [V-1]

#### Partial ranking functions of CR lastbit(V,Out) 
* Partial RF of phase [25]:
  - RF of loop [25:1]:
    V-1


### Specialization of cost equations fun3/3 
* CE 17 is refined into CE [39,40,41,42,43,44,45,46,47] 
* CE 18 is refined into CE [48,49,50,51,52,53,54,55,56] 
* CE 16 is refined into CE [57,58,59] 


### Cost equations --> "Loop" of fun3/3 
* CEs [57,58,59] --> Loop 28 
* CEs [45,54] --> Loop 29 
* CEs [44,53] --> Loop 30 
* CEs [47,56] --> Loop 31 
* CEs [46,55] --> Loop 32 
* CEs [41,50] --> Loop 33 
* CEs [40,49] --> Loop 34 
* CEs [43,52] --> Loop 35 
* CEs [42,51] --> Loop 36 
* CEs [39,48] --> Loop 37 

### Ranking functions of CR fun3(V,V3,Out) 
* RF of phase [29,30,31,32]: [V-1,2*V+V3-3]

#### Partial ranking functions of CR fun3(V,V3,Out) 
* Partial RF of phase [29,30,31,32]:
  - RF of loop [29:1,30:1]:
    V-1
  - RF of loop [31:1,32:1]:
    V-2
    2/3*V-5/3


### Specialization of cost equations start/3 
* CE 1 is refined into CE [60] 
* CE 2 is refined into CE [61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81] 
* CE 3 is refined into CE [82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102] 
* CE 4 is refined into CE [103,104] 
* CE 5 is refined into CE [105,106] 
* CE 6 is refined into CE [107,108,109,110] 
* CE 7 is refined into CE [111,112] 
* CE 8 is refined into CE [113,114,115] 
* CE 9 is refined into CE [116,117,118] 


### Cost equations --> "Loop" of start/3 
* CEs [61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,113] --> Loop 38 
* CEs [60,103,104,105,106,107,108,109,110,111,112,114,115,116,117,118] --> Loop 39 

### Ranking functions of CR start(V,V3,V4) 

#### Partial ranking functions of CR start(V,V3,V4) 


Computing Bounds
=====================================

#### Cost of chains of fun(V,Out):
* Chain [[16],17]: 1*it(16)+0
  Such that:it(16) =< 2*Out

  with precondition: [Out>=1,V>=2*Out] 

* Chain [17]: 0
  with precondition: [Out=0,V>=0] 


#### Cost of chains of fun1(V,Out):
* Chain [[18],19]: 1*it(18)+0
  Such that:it(18) =< 2*Out

  with precondition: [Out>=1,V>=2*Out] 

* Chain [19]: 0
  with precondition: [Out=0,V>=0] 


#### Cost of chains of zero(V,Out):
* Chain [22]: 0
  with precondition: [V=0,Out=2] 

* Chain [21]: 0
  with precondition: [Out=0,V>=0] 

* Chain [20]: 0
  with precondition: [Out=1,V>=1] 


#### Cost of chains of half(V,Out):
* Chain [[23],24]: 0
  with precondition: [Out>=1,V>=2*Out] 

* Chain [24]: 0
  with precondition: [Out=0,V>=0] 


#### Cost of chains of lastbit(V,Out):
* Chain [[25],27]: 0
  with precondition: [Out=1,V>=3] 

* Chain [[25],26]: 0
  with precondition: [Out=0,V>=2] 

* Chain [27]: 0
  with precondition: [V=1,Out=1] 

* Chain [26]: 0
  with precondition: [Out=0,V>=0] 


#### Cost of chains of fun3(V,V3,Out):
* Chain [[29,30,31,32],37,28]: 4*it(29)+2*it(31)+2*it(32)+2*s(9)+2*s(11)+3
  Such that:aux(6) =< 2*V+1
aux(7) =< 2*V+V3
aux(12) =< V
aux(13) =< 2*V
aux(14) =< 2/3*V
it(29) =< aux(12)
it(31) =< aux(12)
it(32) =< aux(12)
it(29) =< aux(13)
it(31) =< aux(13)
it(32) =< aux(13)
it(32) =< aux(6)
s(12) =< aux(6)
it(29) =< aux(7)
it(31) =< aux(7)
it(32) =< aux(7)
s(12) =< aux(13)
it(31) =< aux(14)
it(32) =< aux(14)
s(11) =< s(12)
s(9) =< aux(13)

  with precondition: [V>=2,V3>=0,Out>=5,2*V+2>=Out] 

* Chain [[29,30,31,32],36,28]: 4*it(29)+2*it(31)+2*it(32)+2*s(9)+2*s(11)+3
  Such that:aux(6) =< 2*V+1
aux(7) =< 2*V+V3
aux(15) =< V
aux(16) =< 2*V
aux(17) =< 2/3*V
it(29) =< aux(15)
it(31) =< aux(15)
it(32) =< aux(15)
it(29) =< aux(16)
it(31) =< aux(16)
it(32) =< aux(16)
it(32) =< aux(6)
s(12) =< aux(6)
it(29) =< aux(7)
it(31) =< aux(7)
it(32) =< aux(7)
s(12) =< aux(16)
it(31) =< aux(17)
it(32) =< aux(17)
s(11) =< s(12)
s(9) =< aux(16)

  with precondition: [V>=6,V3>=0,Out>=5,4*V>=3*Out] 

* Chain [[29,30,31,32],35,28]: 4*it(29)+2*it(31)+2*it(32)+4*s(9)+2*s(11)+3
  Such that:aux(6) =< 2*V+1
aux(7) =< 2*V+V3
aux(10) =< 2/3*V
aux(19) =< V
aux(20) =< 2*V
s(9) =< aux(20)
it(29) =< aux(19)
it(31) =< aux(19)
it(32) =< aux(19)
it(29) =< aux(20)
it(31) =< aux(20)
it(32) =< aux(20)
it(32) =< aux(6)
s(12) =< aux(6)
it(29) =< aux(7)
it(31) =< aux(7)
it(32) =< aux(7)
s(12) =< aux(20)
it(31) =< aux(10)
it(32) =< aux(10)
s(11) =< s(12)

  with precondition: [V>=6,V3>=0,Out>=6,8*V+9>=6*Out] 

* Chain [[29,30,31,32],34,28]: 4*it(29)+2*it(31)+2*it(32)+2*s(9)+2*s(11)+3
  Such that:aux(6) =< 2*V+1
aux(7) =< 2*V+V3
aux(21) =< V
aux(22) =< 2*V
aux(23) =< 2/3*V
it(29) =< aux(21)
it(31) =< aux(21)
it(32) =< aux(21)
it(29) =< aux(22)
it(31) =< aux(22)
it(32) =< aux(22)
it(32) =< aux(6)
s(12) =< aux(6)
it(29) =< aux(7)
it(31) =< aux(7)
it(32) =< aux(7)
s(12) =< aux(22)
it(31) =< aux(23)
it(32) =< aux(23)
s(11) =< s(12)
s(9) =< aux(22)

  with precondition: [V>=2,V3>=0,Out>=5,2*V+2>=Out] 

* Chain [[29,30,31,32],33,28]: 4*it(29)+2*it(31)+2*it(32)+4*s(9)+2*s(11)+3
  Such that:aux(6) =< 2*V+1
aux(7) =< 2*V+V3
aux(10) =< 2/3*V
aux(25) =< V
aux(26) =< 2*V
s(9) =< aux(26)
it(29) =< aux(25)
it(31) =< aux(25)
it(32) =< aux(25)
it(29) =< aux(26)
it(31) =< aux(26)
it(32) =< aux(26)
it(32) =< aux(6)
s(12) =< aux(6)
it(29) =< aux(7)
it(31) =< aux(7)
it(32) =< aux(7)
s(12) =< aux(26)
it(31) =< aux(10)
it(32) =< aux(10)
s(11) =< s(12)

  with precondition: [V>=4,V3>=0,Out>=6,3*V+4>=2*Out] 

* Chain [[29,30,31,32],28]: 4*it(29)+2*it(31)+2*it(32)+2*s(9)+2*s(11)+1
  Such that:aux(6) =< 2*V+1
aux(7) =< 2*V+V3
aux(27) =< V
aux(28) =< 2*V
aux(29) =< 2/3*V
it(29) =< aux(27)
it(31) =< aux(27)
it(32) =< aux(27)
it(29) =< aux(28)
it(31) =< aux(28)
it(32) =< aux(28)
it(32) =< aux(6)
s(12) =< aux(6)
it(29) =< aux(7)
it(31) =< aux(7)
it(32) =< aux(7)
s(12) =< aux(28)
it(31) =< aux(29)
it(32) =< aux(29)
s(11) =< s(12)
s(9) =< aux(28)

  with precondition: [V>=2,V3>=0,Out>=3,2*V>=Out] 

* Chain [37,28]: 3
  with precondition: [V=1,Out=3,V3>=0] 

* Chain [36,28]: 3
  with precondition: [Out=3,V>=3,V3>=0] 

* Chain [35,28]: 2*s(13)+3
  Such that:aux(18) =< V
s(13) =< aux(18)

  with precondition: [V>=3,V3>=0,Out>=4,V+6>=2*Out] 

* Chain [34,28]: 3
  with precondition: [Out=3,V>=1,V3>=0] 

* Chain [33,28]: 2*s(15)+3
  Such that:aux(24) =< V
s(15) =< aux(24)

  with precondition: [V3>=0,Out>=4,V+6>=2*Out] 

* Chain [28]: 1
  with precondition: [Out=1,V>=0,V3>=0] 


#### Cost of chains of start(V,V3,V4):
* Chain [39]: 6*s(87)+24*s(95)+12*s(96)+12*s(97)+12*s(99)+16*s(100)+3
  Such that:aux(40) =< V
aux(41) =< 2*V
aux(42) =< 2*V+1
aux(43) =< 2*V+V3
aux(44) =< 2/3*V
s(87) =< aux(40)
s(95) =< aux(40)
s(96) =< aux(40)
s(97) =< aux(40)
s(95) =< aux(41)
s(96) =< aux(41)
s(97) =< aux(41)
s(97) =< aux(42)
s(98) =< aux(42)
s(95) =< aux(43)
s(96) =< aux(43)
s(97) =< aux(43)
s(98) =< aux(41)
s(96) =< aux(44)
s(97) =< aux(44)
s(99) =< s(98)
s(100) =< aux(41)

  with precondition: [V>=0] 

* Chain [38]: 148*s(112)+32*s(121)+96*s(122)+48*s(123)+48*s(124)+96*s(126)+96*s(172)+48*s(173)+48*s(174)+4
  Such that:aux(53) =< V3
aux(54) =< V3+1
aux(55) =< V3+V4+1
aux(56) =< V3+V4+2
aux(57) =< V3/2
aux(58) =< V3/3
s(112) =< aux(53)
s(121) =< aux(57)
s(122) =< aux(57)
s(123) =< aux(57)
s(124) =< aux(57)
s(122) =< aux(53)
s(123) =< aux(53)
s(124) =< aux(53)
s(124) =< aux(54)
s(125) =< aux(54)
s(122) =< aux(55)
s(123) =< aux(55)
s(124) =< aux(55)
s(125) =< aux(53)
s(123) =< aux(58)
s(124) =< aux(58)
s(126) =< s(125)
s(172) =< aux(57)
s(173) =< aux(57)
s(174) =< aux(57)
s(172) =< aux(53)
s(173) =< aux(53)
s(174) =< aux(53)
s(174) =< aux(54)
s(172) =< aux(56)
s(173) =< aux(56)
s(174) =< aux(56)
s(173) =< aux(58)
s(174) =< aux(58)

  with precondition: [V=1] 


Closed-form bounds of start(V,V3,V4): 
-------------------------------------
* Chain [39] with precondition: [V>=0] 
    - Upper bound: 110*V+15 
    - Complexity: n 
* Chain [38] with precondition: [V=1] 
    - Upper bound: nat(V3)*148+4+nat(V3+1)*96+nat(V3/2)*416 
    - Complexity: n 

### Maximum cost of start(V,V3,V4): max([110*V+12,nat(V3)*148+1+nat(V3+1)*96+nat(V3/2)*416])+3 
Asymptotic class: n 
* Total analysis performed in 1126 ms.


----------------------------------------

(20)
BOUNDS(1, n^1)

----------------------------------------

(21) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(22)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(z0))) -> s(half(z0))
   lastbit(0) -> 0
   lastbit(s(0)) -> s(0)
   lastbit(s(s(z0))) -> lastbit(z0)
   zero(0) -> true
   zero(s(z0)) -> false
   conv(z0) -> conviter(z0, cons(0, nil))
   conviter(z0, z1) -> if(zero(z0), z0, z1)
   if(true, z0, z1) -> z1
   if(false, z0, z1) -> conviter(half(z0), cons(lastbit(z0), z1))
Tuples:
   HALF(0) -> c
   HALF(s(0)) -> c1
   HALF(s(s(z0))) -> c2(HALF(z0))
   LASTBIT(0) -> c3
   LASTBIT(s(0)) -> c4
   LASTBIT(s(s(z0))) -> c5(LASTBIT(z0))
   ZERO(0) -> c6
   ZERO(s(z0)) -> c7
   CONV(z0) -> c8(CONVITER(z0, cons(0, nil)))
   CONVITER(z0, z1) -> c9(IF(zero(z0), z0, z1), ZERO(z0))
   IF(true, z0, z1) -> c10
   IF(false, z0, z1) -> c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0))
   IF(false, z0, z1) -> c12(CONVITER(half(z0), cons(lastbit(z0), z1)), LASTBIT(z0))
S tuples:
   HALF(0) -> c
   HALF(s(0)) -> c1
   HALF(s(s(z0))) -> c2(HALF(z0))
   LASTBIT(0) -> c3
   LASTBIT(s(0)) -> c4
   LASTBIT(s(s(z0))) -> c5(LASTBIT(z0))
   ZERO(0) -> c6
   ZERO(s(z0)) -> c7
   CONV(z0) -> c8(CONVITER(z0, cons(0, nil)))
   CONVITER(z0, z1) -> c9(IF(zero(z0), z0, z1), ZERO(z0))
   IF(true, z0, z1) -> c10
   IF(false, z0, z1) -> c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0))
   IF(false, z0, z1) -> c12(CONVITER(half(z0), cons(lastbit(z0), z1)), LASTBIT(z0))
K tuples:none
Defined Rule Symbols:   half_1, lastbit_1, zero_1, conv_1, conviter_2, if_3

Defined Pair Symbols:   HALF_1, LASTBIT_1, ZERO_1, CONV_1, CONVITER_2, IF_3

Compound Symbols:   c, c1, c2_1, c3, c4, c5_1, c6, c7, c8_1, c9_2, c10, c11_2, c12_2


----------------------------------------

(23) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

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


The TRS R consists of the following rules:

   HALF(0) -> c
   HALF(s(0)) -> c1
   HALF(s(s(z0))) -> c2(HALF(z0))
   LASTBIT(0) -> c3
   LASTBIT(s(0)) -> c4
   LASTBIT(s(s(z0))) -> c5(LASTBIT(z0))
   ZERO(0) -> c6
   ZERO(s(z0)) -> c7
   CONV(z0) -> c8(CONVITER(z0, cons(0, nil)))
   CONVITER(z0, z1) -> c9(IF(zero(z0), z0, z1), ZERO(z0))
   IF(true, z0, z1) -> c10
   IF(false, z0, z1) -> c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0))
   IF(false, z0, z1) -> c12(CONVITER(half(z0), cons(lastbit(z0), z1)), LASTBIT(z0))

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

   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(z0))) -> s(half(z0))
   lastbit(0) -> 0
   lastbit(s(0)) -> s(0)
   lastbit(s(s(z0))) -> lastbit(z0)
   zero(0) -> true
   zero(s(z0)) -> false
   conv(z0) -> conviter(z0, cons(0, nil))
   conviter(z0, z1) -> if(zero(z0), z0, z1)
   if(true, z0, z1) -> z1
   if(false, z0, z1) -> conviter(half(z0), cons(lastbit(z0), z1))

Rewrite Strategy: INNERMOST
----------------------------------------

(25) RenamingProof (BOTH BOUNDS(ID, ID))
Renamed function symbols to avoid clashes with predefined symbol.
----------------------------------------

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


The TRS R consists of the following rules:

   HALF(0') -> c
   HALF(s(0')) -> c1
   HALF(s(s(z0))) -> c2(HALF(z0))
   LASTBIT(0') -> c3
   LASTBIT(s(0')) -> c4
   LASTBIT(s(s(z0))) -> c5(LASTBIT(z0))
   ZERO(0') -> c6
   ZERO(s(z0)) -> c7
   CONV(z0) -> c8(CONVITER(z0, cons(0', nil)))
   CONVITER(z0, z1) -> c9(IF(zero(z0), z0, z1), ZERO(z0))
   IF(true, z0, z1) -> c10
   IF(false, z0, z1) -> c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0))
   IF(false, z0, z1) -> c12(CONVITER(half(z0), cons(lastbit(z0), z1)), LASTBIT(z0))

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

   half(0') -> 0'
   half(s(0')) -> 0'
   half(s(s(z0))) -> s(half(z0))
   lastbit(0') -> 0'
   lastbit(s(0')) -> s(0')
   lastbit(s(s(z0))) -> lastbit(z0)
   zero(0') -> true
   zero(s(z0)) -> false
   conv(z0) -> conviter(z0, cons(0', nil))
   conviter(z0, z1) -> if(zero(z0), z0, z1)
   if(true, z0, z1) -> z1
   if(false, z0, z1) -> conviter(half(z0), cons(lastbit(z0), z1))

Rewrite Strategy: INNERMOST
----------------------------------------

(27) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Inferred types.
----------------------------------------

(28)
Obligation:
Innermost TRS:
Rules:
HALF(0') -> c
HALF(s(0')) -> c1
HALF(s(s(z0))) -> c2(HALF(z0))
LASTBIT(0') -> c3
LASTBIT(s(0')) -> c4
LASTBIT(s(s(z0))) -> c5(LASTBIT(z0))
ZERO(0') -> c6
ZERO(s(z0)) -> c7
CONV(z0) -> c8(CONVITER(z0, cons(0', nil)))
CONVITER(z0, z1) -> c9(IF(zero(z0), z0, z1), ZERO(z0))
IF(true, z0, z1) -> c10
IF(false, z0, z1) -> c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0))
IF(false, z0, z1) -> c12(CONVITER(half(z0), cons(lastbit(z0), z1)), LASTBIT(z0))
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
lastbit(0') -> 0'
lastbit(s(0')) -> s(0')
lastbit(s(s(z0))) -> lastbit(z0)
zero(0') -> true
zero(s(z0)) -> false
conv(z0) -> conviter(z0, cons(0', nil))
conviter(z0, z1) -> if(zero(z0), z0, z1)
if(true, z0, z1) -> z1
if(false, z0, z1) -> conviter(half(z0), cons(lastbit(z0), z1))

Types:
HALF :: 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
LASTBIT :: 0':s -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
ZERO :: 0':s -> c6:c7
c6 :: c6:c7
c7 :: c6:c7
CONV :: 0':s -> c8
c8 :: c9 -> c8
CONVITER :: 0':s -> nil:cons -> c9
cons :: 0':s -> nil:cons -> nil:cons
nil :: nil:cons
c9 :: c10:c11:c12 -> c6:c7 -> c9
IF :: true:false -> 0':s -> nil:cons -> c10:c11:c12
zero :: 0':s -> true:false
true :: true:false
c10 :: c10:c11:c12
false :: true:false
c11 :: c9 -> c:c1:c2 -> c10:c11:c12
half :: 0':s -> 0':s
lastbit :: 0':s -> 0':s
c12 :: c9 -> c3:c4:c5 -> c10:c11:c12
conv :: 0':s -> nil:cons
conviter :: 0':s -> nil:cons -> nil:cons
if :: true:false -> 0':s -> nil:cons -> nil:cons
hole_c:c1:c21_13 :: c:c1:c2
hole_0':s2_13 :: 0':s
hole_c3:c4:c53_13 :: c3:c4:c5
hole_c6:c74_13 :: c6:c7
hole_c85_13 :: c8
hole_c96_13 :: c9
hole_nil:cons7_13 :: nil:cons
hole_c10:c11:c128_13 :: c10:c11:c12
hole_true:false9_13 :: true:false
gen_c:c1:c210_13 :: Nat -> c:c1:c2
gen_0':s11_13 :: Nat -> 0':s
gen_c3:c4:c512_13 :: Nat -> c3:c4:c5
gen_nil:cons13_13 :: Nat -> nil:cons

----------------------------------------

(29) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
HALF, LASTBIT, CONVITER, half, lastbit, conviter

They will be analysed ascendingly in the following order:
HALF < CONVITER
LASTBIT < CONVITER
half < CONVITER
lastbit < CONVITER
half < conviter
lastbit < conviter

----------------------------------------

(30)
Obligation:
Innermost TRS:
Rules:
HALF(0') -> c
HALF(s(0')) -> c1
HALF(s(s(z0))) -> c2(HALF(z0))
LASTBIT(0') -> c3
LASTBIT(s(0')) -> c4
LASTBIT(s(s(z0))) -> c5(LASTBIT(z0))
ZERO(0') -> c6
ZERO(s(z0)) -> c7
CONV(z0) -> c8(CONVITER(z0, cons(0', nil)))
CONVITER(z0, z1) -> c9(IF(zero(z0), z0, z1), ZERO(z0))
IF(true, z0, z1) -> c10
IF(false, z0, z1) -> c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0))
IF(false, z0, z1) -> c12(CONVITER(half(z0), cons(lastbit(z0), z1)), LASTBIT(z0))
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
lastbit(0') -> 0'
lastbit(s(0')) -> s(0')
lastbit(s(s(z0))) -> lastbit(z0)
zero(0') -> true
zero(s(z0)) -> false
conv(z0) -> conviter(z0, cons(0', nil))
conviter(z0, z1) -> if(zero(z0), z0, z1)
if(true, z0, z1) -> z1
if(false, z0, z1) -> conviter(half(z0), cons(lastbit(z0), z1))

Types:
HALF :: 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
LASTBIT :: 0':s -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
ZERO :: 0':s -> c6:c7
c6 :: c6:c7
c7 :: c6:c7
CONV :: 0':s -> c8
c8 :: c9 -> c8
CONVITER :: 0':s -> nil:cons -> c9
cons :: 0':s -> nil:cons -> nil:cons
nil :: nil:cons
c9 :: c10:c11:c12 -> c6:c7 -> c9
IF :: true:false -> 0':s -> nil:cons -> c10:c11:c12
zero :: 0':s -> true:false
true :: true:false
c10 :: c10:c11:c12
false :: true:false
c11 :: c9 -> c:c1:c2 -> c10:c11:c12
half :: 0':s -> 0':s
lastbit :: 0':s -> 0':s
c12 :: c9 -> c3:c4:c5 -> c10:c11:c12
conv :: 0':s -> nil:cons
conviter :: 0':s -> nil:cons -> nil:cons
if :: true:false -> 0':s -> nil:cons -> nil:cons
hole_c:c1:c21_13 :: c:c1:c2
hole_0':s2_13 :: 0':s
hole_c3:c4:c53_13 :: c3:c4:c5
hole_c6:c74_13 :: c6:c7
hole_c85_13 :: c8
hole_c96_13 :: c9
hole_nil:cons7_13 :: nil:cons
hole_c10:c11:c128_13 :: c10:c11:c12
hole_true:false9_13 :: true:false
gen_c:c1:c210_13 :: Nat -> c:c1:c2
gen_0':s11_13 :: Nat -> 0':s
gen_c3:c4:c512_13 :: Nat -> c3:c4:c5
gen_nil:cons13_13 :: Nat -> nil:cons


Generator Equations:
gen_c:c1:c210_13(0) <=> c
gen_c:c1:c210_13(+(x, 1)) <=> c2(gen_c:c1:c210_13(x))
gen_0':s11_13(0) <=> 0'
gen_0':s11_13(+(x, 1)) <=> s(gen_0':s11_13(x))
gen_c3:c4:c512_13(0) <=> c3
gen_c3:c4:c512_13(+(x, 1)) <=> c5(gen_c3:c4:c512_13(x))
gen_nil:cons13_13(0) <=> nil
gen_nil:cons13_13(+(x, 1)) <=> cons(0', gen_nil:cons13_13(x))


The following defined symbols remain to be analysed:
HALF, LASTBIT, CONVITER, half, lastbit, conviter

They will be analysed ascendingly in the following order:
HALF < CONVITER
LASTBIT < CONVITER
half < CONVITER
lastbit < CONVITER
half < conviter
lastbit < conviter

----------------------------------------

(31) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
HALF(gen_0':s11_13(*(2, n15_13))) -> gen_c:c1:c210_13(n15_13), rt in Omega(1 + n15_13)

Induction Base:
HALF(gen_0':s11_13(*(2, 0))) ->_R^Omega(1)
c

Induction Step:
HALF(gen_0':s11_13(*(2, +(n15_13, 1)))) ->_R^Omega(1)
c2(HALF(gen_0':s11_13(*(2, n15_13)))) ->_IH
c2(gen_c:c1:c210_13(c16_13))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(32)
Complex Obligation (BEST)

----------------------------------------

(33)
Obligation:
Proved the lower bound n^1 for the following obligation:

Innermost TRS:
Rules:
HALF(0') -> c
HALF(s(0')) -> c1
HALF(s(s(z0))) -> c2(HALF(z0))
LASTBIT(0') -> c3
LASTBIT(s(0')) -> c4
LASTBIT(s(s(z0))) -> c5(LASTBIT(z0))
ZERO(0') -> c6
ZERO(s(z0)) -> c7
CONV(z0) -> c8(CONVITER(z0, cons(0', nil)))
CONVITER(z0, z1) -> c9(IF(zero(z0), z0, z1), ZERO(z0))
IF(true, z0, z1) -> c10
IF(false, z0, z1) -> c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0))
IF(false, z0, z1) -> c12(CONVITER(half(z0), cons(lastbit(z0), z1)), LASTBIT(z0))
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
lastbit(0') -> 0'
lastbit(s(0')) -> s(0')
lastbit(s(s(z0))) -> lastbit(z0)
zero(0') -> true
zero(s(z0)) -> false
conv(z0) -> conviter(z0, cons(0', nil))
conviter(z0, z1) -> if(zero(z0), z0, z1)
if(true, z0, z1) -> z1
if(false, z0, z1) -> conviter(half(z0), cons(lastbit(z0), z1))

Types:
HALF :: 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
LASTBIT :: 0':s -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
ZERO :: 0':s -> c6:c7
c6 :: c6:c7
c7 :: c6:c7
CONV :: 0':s -> c8
c8 :: c9 -> c8
CONVITER :: 0':s -> nil:cons -> c9
cons :: 0':s -> nil:cons -> nil:cons
nil :: nil:cons
c9 :: c10:c11:c12 -> c6:c7 -> c9
IF :: true:false -> 0':s -> nil:cons -> c10:c11:c12
zero :: 0':s -> true:false
true :: true:false
c10 :: c10:c11:c12
false :: true:false
c11 :: c9 -> c:c1:c2 -> c10:c11:c12
half :: 0':s -> 0':s
lastbit :: 0':s -> 0':s
c12 :: c9 -> c3:c4:c5 -> c10:c11:c12
conv :: 0':s -> nil:cons
conviter :: 0':s -> nil:cons -> nil:cons
if :: true:false -> 0':s -> nil:cons -> nil:cons
hole_c:c1:c21_13 :: c:c1:c2
hole_0':s2_13 :: 0':s
hole_c3:c4:c53_13 :: c3:c4:c5
hole_c6:c74_13 :: c6:c7
hole_c85_13 :: c8
hole_c96_13 :: c9
hole_nil:cons7_13 :: nil:cons
hole_c10:c11:c128_13 :: c10:c11:c12
hole_true:false9_13 :: true:false
gen_c:c1:c210_13 :: Nat -> c:c1:c2
gen_0':s11_13 :: Nat -> 0':s
gen_c3:c4:c512_13 :: Nat -> c3:c4:c5
gen_nil:cons13_13 :: Nat -> nil:cons


Generator Equations:
gen_c:c1:c210_13(0) <=> c
gen_c:c1:c210_13(+(x, 1)) <=> c2(gen_c:c1:c210_13(x))
gen_0':s11_13(0) <=> 0'
gen_0':s11_13(+(x, 1)) <=> s(gen_0':s11_13(x))
gen_c3:c4:c512_13(0) <=> c3
gen_c3:c4:c512_13(+(x, 1)) <=> c5(gen_c3:c4:c512_13(x))
gen_nil:cons13_13(0) <=> nil
gen_nil:cons13_13(+(x, 1)) <=> cons(0', gen_nil:cons13_13(x))


The following defined symbols remain to be analysed:
HALF, LASTBIT, CONVITER, half, lastbit, conviter

They will be analysed ascendingly in the following order:
HALF < CONVITER
LASTBIT < CONVITER
half < CONVITER
lastbit < CONVITER
half < conviter
lastbit < conviter

----------------------------------------

(34) LowerBoundPropagationProof (FINISHED)
Propagated lower bound.
----------------------------------------

(35)
BOUNDS(n^1, INF)

----------------------------------------

(36)
Obligation:
Innermost TRS:
Rules:
HALF(0') -> c
HALF(s(0')) -> c1
HALF(s(s(z0))) -> c2(HALF(z0))
LASTBIT(0') -> c3
LASTBIT(s(0')) -> c4
LASTBIT(s(s(z0))) -> c5(LASTBIT(z0))
ZERO(0') -> c6
ZERO(s(z0)) -> c7
CONV(z0) -> c8(CONVITER(z0, cons(0', nil)))
CONVITER(z0, z1) -> c9(IF(zero(z0), z0, z1), ZERO(z0))
IF(true, z0, z1) -> c10
IF(false, z0, z1) -> c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0))
IF(false, z0, z1) -> c12(CONVITER(half(z0), cons(lastbit(z0), z1)), LASTBIT(z0))
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
lastbit(0') -> 0'
lastbit(s(0')) -> s(0')
lastbit(s(s(z0))) -> lastbit(z0)
zero(0') -> true
zero(s(z0)) -> false
conv(z0) -> conviter(z0, cons(0', nil))
conviter(z0, z1) -> if(zero(z0), z0, z1)
if(true, z0, z1) -> z1
if(false, z0, z1) -> conviter(half(z0), cons(lastbit(z0), z1))

Types:
HALF :: 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
LASTBIT :: 0':s -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
ZERO :: 0':s -> c6:c7
c6 :: c6:c7
c7 :: c6:c7
CONV :: 0':s -> c8
c8 :: c9 -> c8
CONVITER :: 0':s -> nil:cons -> c9
cons :: 0':s -> nil:cons -> nil:cons
nil :: nil:cons
c9 :: c10:c11:c12 -> c6:c7 -> c9
IF :: true:false -> 0':s -> nil:cons -> c10:c11:c12
zero :: 0':s -> true:false
true :: true:false
c10 :: c10:c11:c12
false :: true:false
c11 :: c9 -> c:c1:c2 -> c10:c11:c12
half :: 0':s -> 0':s
lastbit :: 0':s -> 0':s
c12 :: c9 -> c3:c4:c5 -> c10:c11:c12
conv :: 0':s -> nil:cons
conviter :: 0':s -> nil:cons -> nil:cons
if :: true:false -> 0':s -> nil:cons -> nil:cons
hole_c:c1:c21_13 :: c:c1:c2
hole_0':s2_13 :: 0':s
hole_c3:c4:c53_13 :: c3:c4:c5
hole_c6:c74_13 :: c6:c7
hole_c85_13 :: c8
hole_c96_13 :: c9
hole_nil:cons7_13 :: nil:cons
hole_c10:c11:c128_13 :: c10:c11:c12
hole_true:false9_13 :: true:false
gen_c:c1:c210_13 :: Nat -> c:c1:c2
gen_0':s11_13 :: Nat -> 0':s
gen_c3:c4:c512_13 :: Nat -> c3:c4:c5
gen_nil:cons13_13 :: Nat -> nil:cons


Lemmas:
HALF(gen_0':s11_13(*(2, n15_13))) -> gen_c:c1:c210_13(n15_13), rt in Omega(1 + n15_13)


Generator Equations:
gen_c:c1:c210_13(0) <=> c
gen_c:c1:c210_13(+(x, 1)) <=> c2(gen_c:c1:c210_13(x))
gen_0':s11_13(0) <=> 0'
gen_0':s11_13(+(x, 1)) <=> s(gen_0':s11_13(x))
gen_c3:c4:c512_13(0) <=> c3
gen_c3:c4:c512_13(+(x, 1)) <=> c5(gen_c3:c4:c512_13(x))
gen_nil:cons13_13(0) <=> nil
gen_nil:cons13_13(+(x, 1)) <=> cons(0', gen_nil:cons13_13(x))


The following defined symbols remain to be analysed:
LASTBIT, CONVITER, half, lastbit, conviter

They will be analysed ascendingly in the following order:
LASTBIT < CONVITER
half < CONVITER
lastbit < CONVITER
half < conviter
lastbit < conviter

----------------------------------------

(37) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LASTBIT(gen_0':s11_13(*(2, n457_13))) -> gen_c3:c4:c512_13(n457_13), rt in Omega(1 + n457_13)

Induction Base:
LASTBIT(gen_0':s11_13(*(2, 0))) ->_R^Omega(1)
c3

Induction Step:
LASTBIT(gen_0':s11_13(*(2, +(n457_13, 1)))) ->_R^Omega(1)
c5(LASTBIT(gen_0':s11_13(*(2, n457_13)))) ->_IH
c5(gen_c3:c4:c512_13(c458_13))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(38)
Obligation:
Innermost TRS:
Rules:
HALF(0') -> c
HALF(s(0')) -> c1
HALF(s(s(z0))) -> c2(HALF(z0))
LASTBIT(0') -> c3
LASTBIT(s(0')) -> c4
LASTBIT(s(s(z0))) -> c5(LASTBIT(z0))
ZERO(0') -> c6
ZERO(s(z0)) -> c7
CONV(z0) -> c8(CONVITER(z0, cons(0', nil)))
CONVITER(z0, z1) -> c9(IF(zero(z0), z0, z1), ZERO(z0))
IF(true, z0, z1) -> c10
IF(false, z0, z1) -> c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0))
IF(false, z0, z1) -> c12(CONVITER(half(z0), cons(lastbit(z0), z1)), LASTBIT(z0))
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
lastbit(0') -> 0'
lastbit(s(0')) -> s(0')
lastbit(s(s(z0))) -> lastbit(z0)
zero(0') -> true
zero(s(z0)) -> false
conv(z0) -> conviter(z0, cons(0', nil))
conviter(z0, z1) -> if(zero(z0), z0, z1)
if(true, z0, z1) -> z1
if(false, z0, z1) -> conviter(half(z0), cons(lastbit(z0), z1))

Types:
HALF :: 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
LASTBIT :: 0':s -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
ZERO :: 0':s -> c6:c7
c6 :: c6:c7
c7 :: c6:c7
CONV :: 0':s -> c8
c8 :: c9 -> c8
CONVITER :: 0':s -> nil:cons -> c9
cons :: 0':s -> nil:cons -> nil:cons
nil :: nil:cons
c9 :: c10:c11:c12 -> c6:c7 -> c9
IF :: true:false -> 0':s -> nil:cons -> c10:c11:c12
zero :: 0':s -> true:false
true :: true:false
c10 :: c10:c11:c12
false :: true:false
c11 :: c9 -> c:c1:c2 -> c10:c11:c12
half :: 0':s -> 0':s
lastbit :: 0':s -> 0':s
c12 :: c9 -> c3:c4:c5 -> c10:c11:c12
conv :: 0':s -> nil:cons
conviter :: 0':s -> nil:cons -> nil:cons
if :: true:false -> 0':s -> nil:cons -> nil:cons
hole_c:c1:c21_13 :: c:c1:c2
hole_0':s2_13 :: 0':s
hole_c3:c4:c53_13 :: c3:c4:c5
hole_c6:c74_13 :: c6:c7
hole_c85_13 :: c8
hole_c96_13 :: c9
hole_nil:cons7_13 :: nil:cons
hole_c10:c11:c128_13 :: c10:c11:c12
hole_true:false9_13 :: true:false
gen_c:c1:c210_13 :: Nat -> c:c1:c2
gen_0':s11_13 :: Nat -> 0':s
gen_c3:c4:c512_13 :: Nat -> c3:c4:c5
gen_nil:cons13_13 :: Nat -> nil:cons


Lemmas:
HALF(gen_0':s11_13(*(2, n15_13))) -> gen_c:c1:c210_13(n15_13), rt in Omega(1 + n15_13)
LASTBIT(gen_0':s11_13(*(2, n457_13))) -> gen_c3:c4:c512_13(n457_13), rt in Omega(1 + n457_13)


Generator Equations:
gen_c:c1:c210_13(0) <=> c
gen_c:c1:c210_13(+(x, 1)) <=> c2(gen_c:c1:c210_13(x))
gen_0':s11_13(0) <=> 0'
gen_0':s11_13(+(x, 1)) <=> s(gen_0':s11_13(x))
gen_c3:c4:c512_13(0) <=> c3
gen_c3:c4:c512_13(+(x, 1)) <=> c5(gen_c3:c4:c512_13(x))
gen_nil:cons13_13(0) <=> nil
gen_nil:cons13_13(+(x, 1)) <=> cons(0', gen_nil:cons13_13(x))


The following defined symbols remain to be analysed:
half, CONVITER, lastbit, conviter

They will be analysed ascendingly in the following order:
half < CONVITER
lastbit < CONVITER
half < conviter
lastbit < conviter

----------------------------------------

(39) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
half(gen_0':s11_13(*(2, n971_13))) -> gen_0':s11_13(n971_13), rt in Omega(0)

Induction Base:
half(gen_0':s11_13(*(2, 0))) ->_R^Omega(0)
0'

Induction Step:
half(gen_0':s11_13(*(2, +(n971_13, 1)))) ->_R^Omega(0)
s(half(gen_0':s11_13(*(2, n971_13)))) ->_IH
s(gen_0':s11_13(c972_13))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(40)
Obligation:
Innermost TRS:
Rules:
HALF(0') -> c
HALF(s(0')) -> c1
HALF(s(s(z0))) -> c2(HALF(z0))
LASTBIT(0') -> c3
LASTBIT(s(0')) -> c4
LASTBIT(s(s(z0))) -> c5(LASTBIT(z0))
ZERO(0') -> c6
ZERO(s(z0)) -> c7
CONV(z0) -> c8(CONVITER(z0, cons(0', nil)))
CONVITER(z0, z1) -> c9(IF(zero(z0), z0, z1), ZERO(z0))
IF(true, z0, z1) -> c10
IF(false, z0, z1) -> c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0))
IF(false, z0, z1) -> c12(CONVITER(half(z0), cons(lastbit(z0), z1)), LASTBIT(z0))
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
lastbit(0') -> 0'
lastbit(s(0')) -> s(0')
lastbit(s(s(z0))) -> lastbit(z0)
zero(0') -> true
zero(s(z0)) -> false
conv(z0) -> conviter(z0, cons(0', nil))
conviter(z0, z1) -> if(zero(z0), z0, z1)
if(true, z0, z1) -> z1
if(false, z0, z1) -> conviter(half(z0), cons(lastbit(z0), z1))

Types:
HALF :: 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
LASTBIT :: 0':s -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
ZERO :: 0':s -> c6:c7
c6 :: c6:c7
c7 :: c6:c7
CONV :: 0':s -> c8
c8 :: c9 -> c8
CONVITER :: 0':s -> nil:cons -> c9
cons :: 0':s -> nil:cons -> nil:cons
nil :: nil:cons
c9 :: c10:c11:c12 -> c6:c7 -> c9
IF :: true:false -> 0':s -> nil:cons -> c10:c11:c12
zero :: 0':s -> true:false
true :: true:false
c10 :: c10:c11:c12
false :: true:false
c11 :: c9 -> c:c1:c2 -> c10:c11:c12
half :: 0':s -> 0':s
lastbit :: 0':s -> 0':s
c12 :: c9 -> c3:c4:c5 -> c10:c11:c12
conv :: 0':s -> nil:cons
conviter :: 0':s -> nil:cons -> nil:cons
if :: true:false -> 0':s -> nil:cons -> nil:cons
hole_c:c1:c21_13 :: c:c1:c2
hole_0':s2_13 :: 0':s
hole_c3:c4:c53_13 :: c3:c4:c5
hole_c6:c74_13 :: c6:c7
hole_c85_13 :: c8
hole_c96_13 :: c9
hole_nil:cons7_13 :: nil:cons
hole_c10:c11:c128_13 :: c10:c11:c12
hole_true:false9_13 :: true:false
gen_c:c1:c210_13 :: Nat -> c:c1:c2
gen_0':s11_13 :: Nat -> 0':s
gen_c3:c4:c512_13 :: Nat -> c3:c4:c5
gen_nil:cons13_13 :: Nat -> nil:cons


Lemmas:
HALF(gen_0':s11_13(*(2, n15_13))) -> gen_c:c1:c210_13(n15_13), rt in Omega(1 + n15_13)
LASTBIT(gen_0':s11_13(*(2, n457_13))) -> gen_c3:c4:c512_13(n457_13), rt in Omega(1 + n457_13)
half(gen_0':s11_13(*(2, n971_13))) -> gen_0':s11_13(n971_13), rt in Omega(0)


Generator Equations:
gen_c:c1:c210_13(0) <=> c
gen_c:c1:c210_13(+(x, 1)) <=> c2(gen_c:c1:c210_13(x))
gen_0':s11_13(0) <=> 0'
gen_0':s11_13(+(x, 1)) <=> s(gen_0':s11_13(x))
gen_c3:c4:c512_13(0) <=> c3
gen_c3:c4:c512_13(+(x, 1)) <=> c5(gen_c3:c4:c512_13(x))
gen_nil:cons13_13(0) <=> nil
gen_nil:cons13_13(+(x, 1)) <=> cons(0', gen_nil:cons13_13(x))


The following defined symbols remain to be analysed:
lastbit, CONVITER, conviter

They will be analysed ascendingly in the following order:
lastbit < CONVITER
lastbit < conviter

----------------------------------------

(41) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
lastbit(gen_0':s11_13(*(2, n1431_13))) -> gen_0':s11_13(0), rt in Omega(0)

Induction Base:
lastbit(gen_0':s11_13(*(2, 0))) ->_R^Omega(0)
0'

Induction Step:
lastbit(gen_0':s11_13(*(2, +(n1431_13, 1)))) ->_R^Omega(0)
lastbit(gen_0':s11_13(*(2, n1431_13))) ->_IH
gen_0':s11_13(0)

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(42)
Obligation:
Innermost TRS:
Rules:
HALF(0') -> c
HALF(s(0')) -> c1
HALF(s(s(z0))) -> c2(HALF(z0))
LASTBIT(0') -> c3
LASTBIT(s(0')) -> c4
LASTBIT(s(s(z0))) -> c5(LASTBIT(z0))
ZERO(0') -> c6
ZERO(s(z0)) -> c7
CONV(z0) -> c8(CONVITER(z0, cons(0', nil)))
CONVITER(z0, z1) -> c9(IF(zero(z0), z0, z1), ZERO(z0))
IF(true, z0, z1) -> c10
IF(false, z0, z1) -> c11(CONVITER(half(z0), cons(lastbit(z0), z1)), HALF(z0))
IF(false, z0, z1) -> c12(CONVITER(half(z0), cons(lastbit(z0), z1)), LASTBIT(z0))
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
lastbit(0') -> 0'
lastbit(s(0')) -> s(0')
lastbit(s(s(z0))) -> lastbit(z0)
zero(0') -> true
zero(s(z0)) -> false
conv(z0) -> conviter(z0, cons(0', nil))
conviter(z0, z1) -> if(zero(z0), z0, z1)
if(true, z0, z1) -> z1
if(false, z0, z1) -> conviter(half(z0), cons(lastbit(z0), z1))

Types:
HALF :: 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
LASTBIT :: 0':s -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
ZERO :: 0':s -> c6:c7
c6 :: c6:c7
c7 :: c6:c7
CONV :: 0':s -> c8
c8 :: c9 -> c8
CONVITER :: 0':s -> nil:cons -> c9
cons :: 0':s -> nil:cons -> nil:cons
nil :: nil:cons
c9 :: c10:c11:c12 -> c6:c7 -> c9
IF :: true:false -> 0':s -> nil:cons -> c10:c11:c12
zero :: 0':s -> true:false
true :: true:false
c10 :: c10:c11:c12
false :: true:false
c11 :: c9 -> c:c1:c2 -> c10:c11:c12
half :: 0':s -> 0':s
lastbit :: 0':s -> 0':s
c12 :: c9 -> c3:c4:c5 -> c10:c11:c12
conv :: 0':s -> nil:cons
conviter :: 0':s -> nil:cons -> nil:cons
if :: true:false -> 0':s -> nil:cons -> nil:cons
hole_c:c1:c21_13 :: c:c1:c2
hole_0':s2_13 :: 0':s
hole_c3:c4:c53_13 :: c3:c4:c5
hole_c6:c74_13 :: c6:c7
hole_c85_13 :: c8
hole_c96_13 :: c9
hole_nil:cons7_13 :: nil:cons
hole_c10:c11:c128_13 :: c10:c11:c12
hole_true:false9_13 :: true:false
gen_c:c1:c210_13 :: Nat -> c:c1:c2
gen_0':s11_13 :: Nat -> 0':s
gen_c3:c4:c512_13 :: Nat -> c3:c4:c5
gen_nil:cons13_13 :: Nat -> nil:cons


Lemmas:
HALF(gen_0':s11_13(*(2, n15_13))) -> gen_c:c1:c210_13(n15_13), rt in Omega(1 + n15_13)
LASTBIT(gen_0':s11_13(*(2, n457_13))) -> gen_c3:c4:c512_13(n457_13), rt in Omega(1 + n457_13)
half(gen_0':s11_13(*(2, n971_13))) -> gen_0':s11_13(n971_13), rt in Omega(0)
lastbit(gen_0':s11_13(*(2, n1431_13))) -> gen_0':s11_13(0), rt in Omega(0)


Generator Equations:
gen_c:c1:c210_13(0) <=> c
gen_c:c1:c210_13(+(x, 1)) <=> c2(gen_c:c1:c210_13(x))
gen_0':s11_13(0) <=> 0'
gen_0':s11_13(+(x, 1)) <=> s(gen_0':s11_13(x))
gen_c3:c4:c512_13(0) <=> c3
gen_c3:c4:c512_13(+(x, 1)) <=> c5(gen_c3:c4:c512_13(x))
gen_nil:cons13_13(0) <=> nil
gen_nil:cons13_13(+(x, 1)) <=> cons(0', gen_nil:cons13_13(x))


The following defined symbols remain to be analysed:
CONVITER, conviter