WORST_CASE(Omega(n^1),O(n^1))
proof of input_Lw9PCS1kXa.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 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 [BOTH BOUNDS(ID, ID), 0 ms]
    (4) CdtProblem
    (5) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
    (6) CdtProblem
    (7) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CdtProblem
    (9) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (10) CdtProblem
    (11) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (12) CpxRelTRS
    (13) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (14) CpxWeightedTrs
    (15) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (16) CpxTypedWeightedTrs
    (17) CompletionProof [UPPER BOUND(ID), 0 ms]
    (18) CpxTypedWeightedCompleteTrs
    (19) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
    (20) CpxRNTS
    (21) CompleteCoflocoProof [FINISHED, 2337 ms]
    (22) BOUNDS(1, n^1)
(23) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(24) CdtProblem
    (25) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (26) CpxRelTRS
    (27) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (28) CpxRelTRS
    (29) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (30) typed CpxTrs
    (31) OrderProof [LOWER BOUND(ID), 10 ms]
    (32) typed CpxTrs
    (33) RewriteLemmaProof [LOWER BOUND(ID), 365 ms]
    (34) BEST
        (35) proven lower bound
            (36) LowerBoundPropagationProof [FINISHED, 0 ms]
            (37) BOUNDS(n^1, INF)
        (38) typed CpxTrs
            (39) RewriteLemmaProof [LOWER BOUND(ID), 16 ms]
            (40) typed CpxTrs
            (41) RewriteLemmaProof [LOWER BOUND(ID), 98 ms]
            (42) typed CpxTrs
            (43) RewriteLemmaProof [LOWER BOUND(ID), 78 ms]
            (44) 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:

   lt(0, s(x)) -> true
   lt(x, 0) -> false
   lt(s(x), s(y)) -> lt(x, y)
   logarithm(x) -> ifa(lt(0, x), x)
   ifa(true, x) -> help(x, 1)
   ifa(false, x) -> logZeroError
   help(x, y) -> ifb(lt(y, x), x, y)
   ifb(true, x, y) -> help(half(x), s(y))
   ifb(false, x, y) -> y
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))

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:
   lt(0, s(z0)) -> true
   lt(z0, 0) -> false
   lt(s(z0), s(z1)) -> lt(z0, z1)
   logarithm(z0) -> ifa(lt(0, z0), z0)
   ifa(true, z0) -> help(z0, 1)
   ifa(false, z0) -> logZeroError
   help(z0, z1) -> ifb(lt(z1, z0), z0, z1)
   ifb(true, z0, z1) -> help(half(z0), s(z1))
   ifb(false, z0, z1) -> z1
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(z0))) -> s(half(z0))
Tuples:
   LT(0, s(z0)) -> c
   LT(z0, 0) -> c1
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   LOGARITHM(z0) -> c3(IFA(lt(0, z0), z0), LT(0, z0))
   IFA(true, z0) -> c4(HELP(z0, 1))
   IFA(false, z0) -> c5
   HELP(z0, z1) -> c6(IFB(lt(z1, z0), z0, z1), LT(z1, z0))
   IFB(true, z0, z1) -> c7(HELP(half(z0), s(z1)), HALF(z0))
   IFB(false, z0, z1) -> c8
   HALF(0) -> c9
   HALF(s(0)) -> c10
   HALF(s(s(z0))) -> c11(HALF(z0))
S tuples:
   LT(0, s(z0)) -> c
   LT(z0, 0) -> c1
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   LOGARITHM(z0) -> c3(IFA(lt(0, z0), z0), LT(0, z0))
   IFA(true, z0) -> c4(HELP(z0, 1))
   IFA(false, z0) -> c5
   HELP(z0, z1) -> c6(IFB(lt(z1, z0), z0, z1), LT(z1, z0))
   IFB(true, z0, z1) -> c7(HELP(half(z0), s(z1)), HALF(z0))
   IFB(false, z0, z1) -> c8
   HALF(0) -> c9
   HALF(s(0)) -> c10
   HALF(s(s(z0))) -> c11(HALF(z0))
K tuples:none
Defined Rule Symbols:   lt_2, logarithm_1, ifa_2, help_2, ifb_3, half_1

Defined Pair Symbols:   LT_2, LOGARITHM_1, IFA_2, HELP_2, IFB_3, HALF_1

Compound Symbols:   c, c1, c2_1, c3_2, c4_1, c5, c6_2, c7_2, c8, c9, c10, c11_1


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

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 6 trailing nodes:
   HALF(s(0)) -> c10
   LT(0, s(z0)) -> c
   IFB(false, z0, z1) -> c8
   LT(z0, 0) -> c1
   HALF(0) -> c9
   IFA(false, z0) -> c5

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

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   lt(0, s(z0)) -> true
   lt(z0, 0) -> false
   lt(s(z0), s(z1)) -> lt(z0, z1)
   logarithm(z0) -> ifa(lt(0, z0), z0)
   ifa(true, z0) -> help(z0, 1)
   ifa(false, z0) -> logZeroError
   help(z0, z1) -> ifb(lt(z1, z0), z0, z1)
   ifb(true, z0, z1) -> help(half(z0), s(z1))
   ifb(false, z0, z1) -> z1
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(z0))) -> s(half(z0))
Tuples:
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   LOGARITHM(z0) -> c3(IFA(lt(0, z0), z0), LT(0, z0))
   IFA(true, z0) -> c4(HELP(z0, 1))
   HELP(z0, z1) -> c6(IFB(lt(z1, z0), z0, z1), LT(z1, z0))
   IFB(true, z0, z1) -> c7(HELP(half(z0), s(z1)), HALF(z0))
   HALF(s(s(z0))) -> c11(HALF(z0))
S tuples:
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   LOGARITHM(z0) -> c3(IFA(lt(0, z0), z0), LT(0, z0))
   IFA(true, z0) -> c4(HELP(z0, 1))
   HELP(z0, z1) -> c6(IFB(lt(z1, z0), z0, z1), LT(z1, z0))
   IFB(true, z0, z1) -> c7(HELP(half(z0), s(z1)), HALF(z0))
   HALF(s(s(z0))) -> c11(HALF(z0))
K tuples:none
Defined Rule Symbols:   lt_2, logarithm_1, ifa_2, help_2, ifb_3, half_1

Defined Pair Symbols:   LT_2, LOGARITHM_1, IFA_2, HELP_2, IFB_3, HALF_1

Compound Symbols:   c2_1, c3_2, c4_1, c6_2, c7_2, c11_1


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

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   lt(0, s(z0)) -> true
   lt(z0, 0) -> false
   lt(s(z0), s(z1)) -> lt(z0, z1)
   logarithm(z0) -> ifa(lt(0, z0), z0)
   ifa(true, z0) -> help(z0, 1)
   ifa(false, z0) -> logZeroError
   help(z0, z1) -> ifb(lt(z1, z0), z0, z1)
   ifb(true, z0, z1) -> help(half(z0), s(z1))
   ifb(false, z0, z1) -> z1
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(z0))) -> s(half(z0))
Tuples:
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   IFA(true, z0) -> c4(HELP(z0, 1))
   HELP(z0, z1) -> c6(IFB(lt(z1, z0), z0, z1), LT(z1, z0))
   IFB(true, z0, z1) -> c7(HELP(half(z0), s(z1)), HALF(z0))
   HALF(s(s(z0))) -> c11(HALF(z0))
   LOGARITHM(z0) -> c3(IFA(lt(0, z0), z0))
S tuples:
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   IFA(true, z0) -> c4(HELP(z0, 1))
   HELP(z0, z1) -> c6(IFB(lt(z1, z0), z0, z1), LT(z1, z0))
   IFB(true, z0, z1) -> c7(HELP(half(z0), s(z1)), HALF(z0))
   HALF(s(s(z0))) -> c11(HALF(z0))
   LOGARITHM(z0) -> c3(IFA(lt(0, z0), z0))
K tuples:none
Defined Rule Symbols:   lt_2, logarithm_1, ifa_2, help_2, ifb_3, half_1

Defined Pair Symbols:   LT_2, IFA_2, HELP_2, IFB_3, HALF_1, LOGARITHM_1

Compound Symbols:   c2_1, c4_1, c6_2, c7_2, c11_1, c3_1


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

(7) CdtKnowledgeProof (BOTH BOUNDS(ID, ID))
The following tuples could be moved from S to K by knowledge propagation:
   LOGARITHM(z0) -> c3(IFA(lt(0, z0), z0))
   IFA(true, z0) -> c4(HELP(z0, 1))

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

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   lt(0, s(z0)) -> true
   lt(z0, 0) -> false
   lt(s(z0), s(z1)) -> lt(z0, z1)
   logarithm(z0) -> ifa(lt(0, z0), z0)
   ifa(true, z0) -> help(z0, 1)
   ifa(false, z0) -> logZeroError
   help(z0, z1) -> ifb(lt(z1, z0), z0, z1)
   ifb(true, z0, z1) -> help(half(z0), s(z1))
   ifb(false, z0, z1) -> z1
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(z0))) -> s(half(z0))
Tuples:
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   IFA(true, z0) -> c4(HELP(z0, 1))
   HELP(z0, z1) -> c6(IFB(lt(z1, z0), z0, z1), LT(z1, z0))
   IFB(true, z0, z1) -> c7(HELP(half(z0), s(z1)), HALF(z0))
   HALF(s(s(z0))) -> c11(HALF(z0))
   LOGARITHM(z0) -> c3(IFA(lt(0, z0), z0))
S tuples:
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   HELP(z0, z1) -> c6(IFB(lt(z1, z0), z0, z1), LT(z1, z0))
   IFB(true, z0, z1) -> c7(HELP(half(z0), s(z1)), HALF(z0))
   HALF(s(s(z0))) -> c11(HALF(z0))
K tuples:
   LOGARITHM(z0) -> c3(IFA(lt(0, z0), z0))
   IFA(true, z0) -> c4(HELP(z0, 1))
Defined Rule Symbols:   lt_2, logarithm_1, ifa_2, help_2, ifb_3, half_1

Defined Pair Symbols:   LT_2, IFA_2, HELP_2, IFB_3, HALF_1, LOGARITHM_1

Compound Symbols:   c2_1, c4_1, c6_2, c7_2, c11_1, c3_1


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

(9) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   logarithm(z0) -> ifa(lt(0, z0), z0)
   ifa(true, z0) -> help(z0, 1)
   ifa(false, z0) -> logZeroError
   help(z0, z1) -> ifb(lt(z1, z0), z0, z1)
   ifb(true, z0, z1) -> help(half(z0), s(z1))
   ifb(false, z0, z1) -> z1

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

(10)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   lt(0, s(z0)) -> true
   lt(z0, 0) -> false
   lt(s(z0), s(z1)) -> lt(z0, z1)
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(z0))) -> s(half(z0))
Tuples:
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   IFA(true, z0) -> c4(HELP(z0, 1))
   HELP(z0, z1) -> c6(IFB(lt(z1, z0), z0, z1), LT(z1, z0))
   IFB(true, z0, z1) -> c7(HELP(half(z0), s(z1)), HALF(z0))
   HALF(s(s(z0))) -> c11(HALF(z0))
   LOGARITHM(z0) -> c3(IFA(lt(0, z0), z0))
S tuples:
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   HELP(z0, z1) -> c6(IFB(lt(z1, z0), z0, z1), LT(z1, z0))
   IFB(true, z0, z1) -> c7(HELP(half(z0), s(z1)), HALF(z0))
   HALF(s(s(z0))) -> c11(HALF(z0))
K tuples:
   LOGARITHM(z0) -> c3(IFA(lt(0, z0), z0))
   IFA(true, z0) -> c4(HELP(z0, 1))
Defined Rule Symbols:   lt_2, half_1

Defined Pair Symbols:   LT_2, IFA_2, HELP_2, IFB_3, HALF_1, LOGARITHM_1

Compound Symbols:   c2_1, c4_1, c6_2, c7_2, c11_1, c3_1


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

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

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

   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   HELP(z0, z1) -> c6(IFB(lt(z1, z0), z0, z1), LT(z1, z0))
   IFB(true, z0, z1) -> c7(HELP(half(z0), s(z1)), HALF(z0))
   HALF(s(s(z0))) -> c11(HALF(z0))

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

   IFA(true, z0) -> c4(HELP(z0, 1))
   LOGARITHM(z0) -> c3(IFA(lt(0, z0), z0))
   lt(0, s(z0)) -> true
   lt(z0, 0) -> false
   lt(s(z0), s(z1)) -> lt(z0, z1)
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(z0))) -> s(half(z0))

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

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

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

   LT(s(z0), s(z1)) -> c2(LT(z0, z1)) [1]
   HELP(z0, z1) -> c6(IFB(lt(z1, z0), z0, z1), LT(z1, z0)) [1]
   IFB(true, z0, z1) -> c7(HELP(half(z0), s(z1)), HALF(z0)) [1]
   HALF(s(s(z0))) -> c11(HALF(z0)) [1]
   IFA(true, z0) -> c4(HELP(z0, 1)) [0]
   LOGARITHM(z0) -> c3(IFA(lt(0, z0), z0)) [0]
   lt(0, s(z0)) -> true [0]
   lt(z0, 0) -> false [0]
   lt(s(z0), s(z1)) -> lt(z0, z1) [0]
   half(0) -> 0 [0]
   half(s(0)) -> 0 [0]
   half(s(s(z0))) -> s(half(z0)) [0]

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

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

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

   LT(s(z0), s(z1)) -> c2(LT(z0, z1)) [1]
   HELP(z0, z1) -> c6(IFB(lt(z1, z0), z0, z1), LT(z1, z0)) [1]
   IFB(true, z0, z1) -> c7(HELP(half(z0), s(z1)), HALF(z0)) [1]
   HALF(s(s(z0))) -> c11(HALF(z0)) [1]
   IFA(true, z0) -> c4(HELP(z0, 1)) [0]
   LOGARITHM(z0) -> c3(IFA(lt(0, z0), z0)) [0]
   lt(0, s(z0)) -> true [0]
   lt(z0, 0) -> false [0]
   lt(s(z0), s(z1)) -> lt(z0, z1) [0]
   half(0) -> 0 [0]
   half(s(0)) -> 0 [0]
   half(s(s(z0))) -> s(half(z0)) [0]

The TRS has the following type information:
LT :: s:1:0 -> s:1:0 -> c2
s :: s:1:0 -> s:1:0
c2 :: c2 -> c2
HELP :: s:1:0 -> s:1:0 -> c6
c6 :: c7 -> c2 -> c6
IFB :: true:false -> s:1:0 -> s:1:0 -> c7
lt :: s:1:0 -> s:1:0 -> true:false
true :: true:false
c7 :: c6 -> c11 -> c7
half :: s:1:0 -> s:1:0
HALF :: s:1:0 -> c11
c11 :: c11 -> c11
IFA :: true:false -> s:1:0 -> c4
c4 :: c6 -> c4
1 :: s:1:0
LOGARITHM :: s:1:0 -> c3
c3 :: c4 -> c3
0 :: s:1:0
false :: true:false

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

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

   IFA(v0, v1) -> null_IFA [0]
   LOGARITHM(v0) -> null_LOGARITHM [0]
   lt(v0, v1) -> null_lt [0]
   half(v0) -> null_half [0]
   LT(v0, v1) -> null_LT [0]
   IFB(v0, v1, v2) -> null_IFB [0]
   HALF(v0) -> null_HALF [0]

And the following fresh constants:    null_IFA, null_LOGARITHM, null_lt, null_half, null_LT, null_IFB, null_HALF, const

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

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

   LT(s(z0), s(z1)) -> c2(LT(z0, z1)) [1]
   HELP(z0, z1) -> c6(IFB(lt(z1, z0), z0, z1), LT(z1, z0)) [1]
   IFB(true, z0, z1) -> c7(HELP(half(z0), s(z1)), HALF(z0)) [1]
   HALF(s(s(z0))) -> c11(HALF(z0)) [1]
   IFA(true, z0) -> c4(HELP(z0, 1)) [0]
   LOGARITHM(z0) -> c3(IFA(lt(0, z0), z0)) [0]
   lt(0, s(z0)) -> true [0]
   lt(z0, 0) -> false [0]
   lt(s(z0), s(z1)) -> lt(z0, z1) [0]
   half(0) -> 0 [0]
   half(s(0)) -> 0 [0]
   half(s(s(z0))) -> s(half(z0)) [0]
   IFA(v0, v1) -> null_IFA [0]
   LOGARITHM(v0) -> null_LOGARITHM [0]
   lt(v0, v1) -> null_lt [0]
   half(v0) -> null_half [0]
   LT(v0, v1) -> null_LT [0]
   IFB(v0, v1, v2) -> null_IFB [0]
   HALF(v0) -> null_HALF [0]

The TRS has the following type information:
LT :: s:1:0:null_half -> s:1:0:null_half -> c2:null_LT
s :: s:1:0:null_half -> s:1:0:null_half
c2 :: c2:null_LT -> c2:null_LT
HELP :: s:1:0:null_half -> s:1:0:null_half -> c6
c6 :: c7:null_IFB -> c2:null_LT -> c6
IFB :: true:false:null_lt -> s:1:0:null_half -> s:1:0:null_half -> c7:null_IFB
lt :: s:1:0:null_half -> s:1:0:null_half -> true:false:null_lt
true :: true:false:null_lt
c7 :: c6 -> c11:null_HALF -> c7:null_IFB
half :: s:1:0:null_half -> s:1:0:null_half
HALF :: s:1:0:null_half -> c11:null_HALF
c11 :: c11:null_HALF -> c11:null_HALF
IFA :: true:false:null_lt -> s:1:0:null_half -> c4:null_IFA
c4 :: c6 -> c4:null_IFA
1 :: s:1:0:null_half
LOGARITHM :: s:1:0:null_half -> c3:null_LOGARITHM
c3 :: c4:null_IFA -> c3:null_LOGARITHM
0 :: s:1:0:null_half
false :: true:false:null_lt
null_IFA :: c4:null_IFA
null_LOGARITHM :: c3:null_LOGARITHM
null_lt :: true:false:null_lt
null_half :: s:1:0:null_half
null_LT :: c2:null_LT
null_IFB :: c7:null_IFB
null_HALF :: c11:null_HALF
const :: c6

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

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

   true => 2
   1 => 1
   0 => 0
   false => 1
   null_IFA => 0
   null_LOGARITHM => 0
   null_lt => 0
   null_half => 0
   null_LT => 0
   null_IFB => 0
   null_HALF => 0
   const => 0

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

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

   HALF(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   HALF(z) -{ 1 }-> 1 + HALF(z0) :|: z0 >= 0, z = 1 + (1 + z0)
   HELP(z, z') -{ 1 }-> 1 + IFB(lt(z1, z0), z0, z1) + LT(z1, z0) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   IFA(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   IFA(z, z') -{ 0 }-> 1 + HELP(z0, 1) :|: z = 2, z0 >= 0, z' = z0
   IFB(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   IFB(z, z', z'') -{ 1 }-> 1 + HELP(half(z0), 1 + z1) + HALF(z0) :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1
   LOGARITHM(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   LOGARITHM(z) -{ 0 }-> 1 + IFA(lt(0, z0), z0) :|: z = z0, z0 >= 0
   LT(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   LT(z, z') -{ 1 }-> 1 + LT(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   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)
   lt(z, z') -{ 0 }-> lt(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   lt(z, z') -{ 0 }-> 2 :|: z0 >= 0, z' = 1 + z0, z = 0
   lt(z, z') -{ 0 }-> 1 :|: z = z0, z0 >= 0, z' = 0
   lt(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1

Only complete derivations are relevant for the runtime complexity.

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

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

eq(start(V1, V, V6),0,[fun(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V6),0,[fun1(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V6),0,[fun2(V1, V, V6, Out)],[V1 >= 0,V >= 0,V6 >= 0]).
eq(start(V1, V, V6),0,[fun3(V1, Out)],[V1 >= 0]).
eq(start(V1, V, V6),0,[fun4(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V6),0,[fun5(V1, Out)],[V1 >= 0]).
eq(start(V1, V, V6),0,[lt(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V6),0,[half(V1, Out)],[V1 >= 0]).
eq(fun(V1, V, Out),1,[fun(V3, V2, Ret1)],[Out = 1 + Ret1,V2 >= 0,V1 = 1 + V3,V3 >= 0,V = 1 + V2]).
eq(fun1(V1, V, Out),1,[lt(V4, V5, Ret010),fun2(Ret010, V5, V4, Ret01),fun(V4, V5, Ret11)],[Out = 1 + Ret01 + Ret11,V1 = V5,V4 >= 0,V = V4,V5 >= 0]).
eq(fun2(V1, V, V6, Out),1,[half(V8, Ret0101),fun1(Ret0101, 1 + V7, Ret011),fun3(V8, Ret12)],[Out = 1 + Ret011 + Ret12,V1 = 2,V7 >= 0,V8 >= 0,V = V8,V6 = V7]).
eq(fun3(V1, Out),1,[fun3(V9, Ret13)],[Out = 1 + Ret13,V9 >= 0,V1 = 2 + V9]).
eq(fun4(V1, V, Out),0,[fun1(V10, 1, Ret14)],[Out = 1 + Ret14,V1 = 2,V10 >= 0,V = V10]).
eq(fun5(V1, Out),0,[lt(0, V11, Ret10),fun4(Ret10, V11, Ret15)],[Out = 1 + Ret15,V1 = V11,V11 >= 0]).
eq(lt(V1, V, Out),0,[],[Out = 2,V12 >= 0,V = 1 + V12,V1 = 0]).
eq(lt(V1, V, Out),0,[],[Out = 1,V1 = V13,V13 >= 0,V = 0]).
eq(lt(V1, V, Out),0,[lt(V15, V14, Ret)],[Out = Ret,V14 >= 0,V1 = 1 + V15,V15 >= 0,V = 1 + V14]).
eq(half(V1, Out),0,[],[Out = 0,V1 = 0]).
eq(half(V1, Out),0,[],[Out = 0,V1 = 1]).
eq(half(V1, Out),0,[half(V16, Ret16)],[Out = 1 + Ret16,V16 >= 0,V1 = 2 + V16]).
eq(fun4(V1, V, Out),0,[],[Out = 0,V18 >= 0,V17 >= 0,V1 = V18,V = V17]).
eq(fun5(V1, Out),0,[],[Out = 0,V19 >= 0,V1 = V19]).
eq(lt(V1, V, Out),0,[],[Out = 0,V21 >= 0,V20 >= 0,V1 = V21,V = V20]).
eq(half(V1, Out),0,[],[Out = 0,V22 >= 0,V1 = V22]).
eq(fun(V1, V, Out),0,[],[Out = 0,V23 >= 0,V24 >= 0,V1 = V23,V = V24]).
eq(fun2(V1, V, V6, Out),0,[],[Out = 0,V25 >= 0,V6 = V27,V26 >= 0,V1 = V25,V = V26,V27 >= 0]).
eq(fun3(V1, Out),0,[],[Out = 0,V28 >= 0,V1 = V28]).
input_output_vars(fun(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun1(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun2(V1,V,V6,Out),[V1,V,V6],[Out]).
input_output_vars(fun3(V1,Out),[V1],[Out]).
input_output_vars(fun4(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun5(V1,Out),[V1],[Out]).
input_output_vars(lt(V1,V,Out),[V1,V],[Out]).
input_output_vars(half(V1,Out),[V1],[Out]).


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

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

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

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

### Specialization of cost equations fun/3 
* CE 18 is refined into CE [27] 
* CE 17 is refined into CE [28] 


### Cost equations --> "Loop" of fun/3 
* CEs [28] --> Loop 17 
* CEs [27] --> Loop 18 

### Ranking functions of CR fun(V1,V,Out) 
* RF of phase [17]: [V,V1]

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


### Specialization of cost equations fun3/2 
* CE 16 is refined into CE [29] 
* CE 15 is refined into CE [30] 


### Cost equations --> "Loop" of fun3/2 
* CEs [30] --> Loop 19 
* CEs [29] --> Loop 20 

### Ranking functions of CR fun3(V1,Out) 
* RF of phase [19]: [V1-1]

#### Partial ranking functions of CR fun3(V1,Out) 
* Partial RF of phase [19]:
  - RF of loop [19:1]:
    V1-1


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


### Cost equations --> "Loop" of half/2 
* CEs [33] --> Loop 21 
* CEs [31,32] --> Loop 22 

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

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


### Specialization of cost equations lt/3 
* CE 26 is refined into CE [34] 
* CE 24 is refined into CE [35] 
* CE 23 is refined into CE [36] 
* CE 25 is refined into CE [37] 


### Cost equations --> "Loop" of lt/3 
* CEs [37] --> Loop 23 
* CEs [34] --> Loop 24 
* CEs [35] --> Loop 25 
* CEs [36] --> Loop 26 

### Ranking functions of CR lt(V1,V,Out) 
* RF of phase [23]: [V,V1]

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


### Specialization of cost equations fun1/3 
* CE 14 is refined into CE [38,39,40,41,42,43,44,45,46,47,48,49] 
* CE 13 is refined into CE [50,51,52,53,54,55,56,57] 


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

### Ranking functions of CR fun1(V1,V,Out) 
* RF of phase [31,32,33,34]: [V1-1,V1/2-V/2]

#### Partial ranking functions of CR fun1(V1,V,Out) 
* Partial RF of phase [31,32,33,34]:
  - RF of loop [31:1,32:1,33:1,34:1]:
    V1-1
    V1/2-V/2


### Specialization of cost equations fun4/3 
* CE 20 is refined into CE [58] 
* CE 19 is refined into CE [59,60,61,62] 


### Cost equations --> "Loop" of fun4/3 
* CEs [58] --> Loop 43 
* CEs [61] --> Loop 44 
* CEs [60] --> Loop 45 
* CEs [62] --> Loop 46 
* CEs [59] --> Loop 47 

### Ranking functions of CR fun4(V1,V,Out) 

#### Partial ranking functions of CR fun4(V1,V,Out) 


### Specialization of cost equations fun5/2 
* CE 21 is refined into CE [63,64,65,66,67,68,69] 
* CE 22 is refined into CE [70] 


### Cost equations --> "Loop" of fun5/2 
* CEs [66] --> Loop 48 
* CEs [65] --> Loop 49 
* CEs [64] --> Loop 50 
* CEs [63] --> Loop 51 
* CEs [70] --> Loop 52 
* CEs [67,68,69] --> Loop 53 

### Ranking functions of CR fun5(V1,Out) 

#### Partial ranking functions of CR fun5(V1,Out) 


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


### Cost equations --> "Loop" of start/3 
* CEs [85,86,87,88,89,90,108] --> Loop 54 
* CEs [72,73,74,75,76,77,78,79,80,81,96,97,98,99] --> Loop 55 
* CEs [71,82,83,84,91,92,93,94,95,100,101,102,103,104,105,106,107,109,110,111,112,113] --> Loop 56 

### Ranking functions of CR start(V1,V,V6) 

#### Partial ranking functions of CR start(V1,V,V6) 


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

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

  with precondition: [Out>=1,V1>=Out,V>=Out] 

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


#### Cost of chains of fun3(V1,Out):
* Chain [[19],20]: 1*it(19)+0
  Such that:it(19) =< 2*Out

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

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


#### Cost of chains of half(V1,Out):
* Chain [[21],22]: 0
  with precondition: [Out>=1,V1>=2*Out] 

* Chain [22]: 0
  with precondition: [Out=0,V1>=0] 


#### Cost of chains of lt(V1,V,Out):
* Chain [[23],26]: 0
  with precondition: [Out=2,V1>=1,V>=V1+1] 

* Chain [[23],25]: 0
  with precondition: [Out=1,V>=1,V1>=V] 

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

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

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

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


#### Cost of chains of fun1(V1,V,Out):
* Chain [[31,32,33,34],38,30]: 4*it(31)+2*it(33)+2*it(34)+1*s(1)+1*s(10)+2*s(11)+1*s(12)+3
  Such that:aux(3) =< 2*V1-V
aux(5) =< 3*V1+V
aux(6) =< 3*V1+V+1
aux(9) =< 4*V1
aux(8) =< V1/2-V/2
aux(10) =< V1
aux(11) =< 5*V1
s(1) =< aux(11)
it(31) =< aux(10)
it(33) =< aux(10)
it(34) =< aux(10)
it(34) =< aux(3)
s(11) =< aux(3)
it(34) =< aux(11)
s(11) =< aux(11)
it(33) =< aux(5)
it(34) =< aux(5)
s(10) =< aux(5)
it(34) =< aux(6)
s(12) =< aux(6)
it(33) =< aux(11)
s(10) =< aux(11)
s(12) =< aux(11)
it(31) =< aux(8)
it(33) =< aux(8)
it(34) =< aux(8)
it(31) =< aux(9)
it(33) =< aux(9)
it(34) =< aux(9)

  with precondition: [V>=1,Out>=6,V1>=2*V+4,2*V+27*V1+46>=20*Out,3*V1+4>=2*Out+V] 

* Chain [[31,32,33,34],37,30]: 4*it(31)+2*it(33)+2*it(34)+1*s(10)+2*s(11)+1*s(12)+1*s(14)+1*s(15)+3
  Such that:aux(3) =< 2*V1-V
aux(5) =< 3*V1+V
aux(9) =< 4*V1
aux(8) =< V1/2-V/2
aux(12) =< V1
aux(13) =< 3*V1+V+1
aux(14) =< 5*V1
s(15) =< aux(13)
s(14) =< aux(14)
it(31) =< aux(12)
it(33) =< aux(12)
it(34) =< aux(12)
it(34) =< aux(3)
s(11) =< aux(3)
it(34) =< aux(14)
s(11) =< aux(14)
it(33) =< aux(5)
it(34) =< aux(5)
s(10) =< aux(5)
it(34) =< aux(13)
s(12) =< aux(13)
it(33) =< aux(14)
s(10) =< aux(14)
s(12) =< aux(14)
it(31) =< aux(8)
it(33) =< aux(8)
it(34) =< aux(8)
it(31) =< aux(9)
it(33) =< aux(9)
it(34) =< aux(9)

  with precondition: [V>=1,Out>=7,V1>=2*V+4,14*V+29*V1+62>=20*Out,V+3*V1+6>=2*Out] 

* Chain [[31,32,33,34],36,30]: 4*it(31)+2*it(33)+2*it(34)+1*s(10)+3*s(11)+1*s(12)+3
  Such that:aux(5) =< 3*V1+V
aux(15) =< V1
aux(16) =< 2*V1-V
aux(17) =< 3*V1+V+1
aux(18) =< V1/2-V/2
s(11) =< aux(16)
it(31) =< aux(15)
it(33) =< aux(15)
it(34) =< aux(15)
it(34) =< aux(16)
it(33) =< aux(5)
it(34) =< aux(5)
s(10) =< aux(5)
it(34) =< aux(17)
s(12) =< aux(17)
it(33) =< aux(17)
s(10) =< aux(17)
it(31) =< aux(18)
it(33) =< aux(18)
it(34) =< aux(18)

  with precondition: [V>=1,Out>=6,V1>=2*V+4,3*V1+4>=2*Out,2*V+7*V1+11>=5*Out] 

* Chain [[31,32,33,34],35,30]: 4*it(31)+2*it(33)+2*it(34)+1*s(10)+2*s(11)+1*s(12)+3
  Such that:aux(1) =< V1
aux(2) =< V1-V
aux(4) =< 2*V1-2*V
aux(3) =< 2*V1-V
aux(7) =< 3*V1-3*V
aux(5) =< 3*V1+V
aux(6) =< 3*V1+V+1
aux(19) =< V1/2-V/2
it(31) =< aux(1)
it(33) =< aux(1)
it(34) =< aux(1)
it(31) =< aux(2)
it(33) =< aux(2)
it(34) =< aux(2)
it(34) =< aux(3)
s(11) =< aux(3)
it(34) =< aux(4)
s(11) =< aux(4)
it(33) =< aux(5)
it(34) =< aux(5)
s(10) =< aux(5)
it(34) =< aux(6)
s(12) =< aux(6)
it(33) =< aux(7)
it(34) =< aux(7)
s(10) =< aux(7)
s(12) =< aux(7)
it(31) =< aux(19)
it(33) =< aux(19)
it(34) =< aux(19)

  with precondition: [V>=1,Out>=5,V1>=2*V+4,13*V1+14>=10*Out+2*V,3*V1+2>=2*Out+2*V] 

* Chain [[31,32,33,34],30]: 4*it(31)+2*it(33)+2*it(34)+1*s(10)+2*s(11)+1*s(12)+1
  Such that:aux(3) =< 2*V1-V
aux(5) =< 3*V1+V
aux(6) =< 3*V1+V+1
aux(4) =< 5*V1
aux(8) =< V1/2-V/2
aux(20) =< V1
aux(21) =< 4*V1
it(31) =< aux(20)
it(33) =< aux(20)
it(34) =< aux(20)
it(34) =< aux(3)
s(11) =< aux(3)
it(34) =< aux(4)
s(11) =< aux(4)
it(33) =< aux(5)
it(34) =< aux(5)
s(10) =< aux(5)
it(34) =< aux(6)
s(12) =< aux(6)
it(33) =< aux(21)
it(34) =< aux(21)
s(10) =< aux(21)
s(12) =< aux(21)
it(31) =< aux(8)
it(33) =< aux(8)
it(34) =< aux(8)
it(31) =< aux(21)

  with precondition: [V>=1,Out>=3,V1>=V+1,15*V1+12>=8*Out+2*V,4*V1+3>=2*Out+V] 

* Chain [[31,32,33,34],28]: 4*it(31)+2*it(33)+2*it(34)+3*s(10)+2*s(11)+1*s(12)+1
  Such that:aux(3) =< 2*V1-V
aux(6) =< 3*V1+V+1
aux(9) =< 4*V1
aux(4) =< 5*V1
aux(8) =< V1/2-V/2
aux(22) =< V1
aux(23) =< 3*V1+V
s(10) =< aux(23)
it(31) =< aux(22)
it(33) =< aux(22)
it(34) =< aux(22)
it(34) =< aux(3)
s(11) =< aux(3)
it(34) =< aux(4)
s(11) =< aux(4)
it(33) =< aux(23)
it(34) =< aux(23)
it(34) =< aux(6)
s(12) =< aux(6)
s(12) =< aux(23)
it(31) =< aux(8)
it(33) =< aux(8)
it(34) =< aux(8)
it(31) =< aux(9)
it(33) =< aux(9)
it(34) =< aux(9)

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

* Chain [[31,32,33,34],27]: 4*it(31)+2*it(33)+2*it(34)+1*s(10)+3*s(11)+1*s(12)+1
  Such that:aux(6) =< 3*V1+V+1
aux(24) =< V1
aux(25) =< 2*V1-V
aux(26) =< 3*V1+V
aux(27) =< V1/2-V/2
s(11) =< aux(25)
it(31) =< aux(24)
it(33) =< aux(24)
it(34) =< aux(24)
it(34) =< aux(25)
it(33) =< aux(26)
it(34) =< aux(26)
s(10) =< aux(26)
it(34) =< aux(6)
s(12) =< aux(6)
s(12) =< aux(26)
it(31) =< aux(27)
it(33) =< aux(27)
it(34) =< aux(27)

  with precondition: [V>=1,Out>=4,V1>=2*V+4,3*V1>=2*Out,2*V+7*V1+1>=5*Out] 

* Chain [42,30]: 3
  with precondition: [V=0,Out=3,V1>=1] 

* Chain [41,30]: 1*s(20)+3
  Such that:s(20) =< V1

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

* Chain [40,[31,32,33,34],38,30]: 4*it(31)+2*it(33)+2*it(34)+1*s(1)+1*s(10)+2*s(11)+1*s(12)+5
  Such that:aux(3) =< V1
aux(9) =< 2*V1
aux(10) =< V1/2
aux(8) =< V1/4
aux(5) =< 3/2*V1+1
aux(6) =< 3/2*V1+2
aux(11) =< 5/2*V1
s(1) =< aux(11)
it(31) =< aux(10)
it(33) =< aux(10)
it(34) =< aux(10)
it(34) =< aux(3)
s(11) =< aux(3)
it(34) =< aux(11)
s(11) =< aux(11)
it(33) =< aux(5)
it(34) =< aux(5)
s(10) =< aux(5)
it(34) =< aux(6)
s(12) =< aux(6)
it(33) =< aux(11)
s(10) =< aux(11)
s(12) =< aux(11)
it(31) =< aux(8)
it(33) =< aux(8)
it(34) =< aux(8)
it(31) =< aux(9)
it(33) =< aux(9)
it(34) =< aux(9)

  with precondition: [V=0,V1>=12,Out>=8,27*V1+176>=40*Out] 

* Chain [40,[31,32,33,34],37,30]: 4*it(31)+2*it(33)+2*it(34)+1*s(10)+2*s(11)+1*s(12)+1*s(14)+1*s(15)+5
  Such that:aux(3) =< V1
aux(9) =< 2*V1
aux(12) =< V1/2
aux(8) =< V1/4
aux(5) =< 3/2*V1+1
aux(13) =< 3/2*V1+2
aux(14) =< 5/2*V1
s(15) =< aux(13)
s(14) =< aux(14)
it(31) =< aux(12)
it(33) =< aux(12)
it(34) =< aux(12)
it(34) =< aux(3)
s(11) =< aux(3)
it(34) =< aux(14)
s(11) =< aux(14)
it(33) =< aux(5)
it(34) =< aux(5)
s(10) =< aux(5)
it(34) =< aux(13)
s(12) =< aux(13)
it(33) =< aux(14)
s(10) =< aux(14)
s(12) =< aux(14)
it(31) =< aux(8)
it(33) =< aux(8)
it(34) =< aux(8)
it(31) =< aux(9)
it(33) =< aux(9)
it(34) =< aux(9)

  with precondition: [V=0,V1>=12,Out>=9,29*V1+232>=40*Out] 

* Chain [40,[31,32,33,34],36,30]: 4*it(31)+2*it(33)+2*it(34)+1*s(10)+3*s(11)+1*s(12)+5
  Such that:aux(16) =< V1
aux(15) =< V1/2
aux(18) =< V1/4
aux(5) =< 3/2*V1+1
aux(17) =< 3/2*V1+2
s(11) =< aux(16)
it(31) =< aux(15)
it(33) =< aux(15)
it(34) =< aux(15)
it(34) =< aux(16)
it(33) =< aux(5)
it(34) =< aux(5)
s(10) =< aux(5)
it(34) =< aux(17)
s(12) =< aux(17)
it(33) =< aux(17)
s(10) =< aux(17)
it(31) =< aux(18)
it(33) =< aux(18)
it(34) =< aux(18)

  with precondition: [V=0,V1>=12,Out>=8,7*V1+46>=10*Out] 

* Chain [40,[31,32,33,34],35,30]: 4*it(31)+2*it(33)+2*it(34)+1*s(10)+2*s(11)+1*s(12)+5
  Such that:aux(19) =< V1/4
aux(7) =< 3/2*V1
aux(5) =< 3/2*V1+1
aux(6) =< 3/2*V1+2
aux(28) =< V1
aux(29) =< V1/2
it(31) =< aux(29)
it(33) =< aux(29)
it(34) =< aux(29)
it(34) =< aux(28)
s(11) =< aux(28)
it(33) =< aux(5)
it(34) =< aux(5)
s(10) =< aux(5)
it(34) =< aux(6)
s(12) =< aux(6)
it(33) =< aux(7)
it(34) =< aux(7)
s(10) =< aux(7)
s(12) =< aux(7)
it(31) =< aux(19)
it(33) =< aux(19)
it(34) =< aux(19)

  with precondition: [V=0,V1>=12,Out>=7,13*V1+64>=20*Out] 

* Chain [40,[31,32,33,34],30]: 4*it(31)+2*it(33)+2*it(34)+1*s(10)+2*s(11)+1*s(12)+3
  Such that:aux(3) =< V1
aux(21) =< 2*V1
aux(20) =< V1/2
aux(8) =< V1/4
aux(5) =< 3/2*V1+1
aux(6) =< 3/2*V1+2
aux(4) =< 5/2*V1
it(31) =< aux(20)
it(33) =< aux(20)
it(34) =< aux(20)
it(34) =< aux(3)
s(11) =< aux(3)
it(34) =< aux(4)
s(11) =< aux(4)
it(33) =< aux(5)
it(34) =< aux(5)
s(10) =< aux(5)
it(34) =< aux(6)
s(12) =< aux(6)
it(33) =< aux(21)
it(34) =< aux(21)
s(10) =< aux(21)
s(12) =< aux(21)
it(31) =< aux(8)
it(33) =< aux(8)
it(34) =< aux(8)
it(31) =< aux(21)

  with precondition: [V=0,V1>=4,Out>=5,15*V1+52>=16*Out] 

* Chain [40,[31,32,33,34],28]: 4*it(31)+2*it(33)+2*it(34)+3*s(10)+2*s(11)+1*s(12)+3
  Such that:aux(3) =< V1
aux(9) =< 2*V1
aux(22) =< V1/2
aux(8) =< V1/4
aux(23) =< 3/2*V1+1
aux(6) =< 3/2*V1+2
aux(4) =< 5/2*V1
s(10) =< aux(23)
it(31) =< aux(22)
it(33) =< aux(22)
it(34) =< aux(22)
it(34) =< aux(3)
s(11) =< aux(3)
it(34) =< aux(4)
s(11) =< aux(4)
it(33) =< aux(23)
it(34) =< aux(23)
it(34) =< aux(6)
s(12) =< aux(6)
s(12) =< aux(23)
it(31) =< aux(8)
it(33) =< aux(8)
it(34) =< aux(8)
it(31) =< aux(9)
it(33) =< aux(9)
it(34) =< aux(9)

  with precondition: [V=0,V1>=4,Out>=6,V1+4>=Out] 

* Chain [40,[31,32,33,34],27]: 4*it(31)+2*it(33)+2*it(34)+1*s(10)+3*s(11)+1*s(12)+3
  Such that:aux(25) =< V1
aux(24) =< V1/2
aux(27) =< V1/4
aux(26) =< 3/2*V1+1
aux(6) =< 3/2*V1+2
s(11) =< aux(25)
it(31) =< aux(24)
it(33) =< aux(24)
it(34) =< aux(24)
it(34) =< aux(25)
it(33) =< aux(26)
it(34) =< aux(26)
s(10) =< aux(26)
it(34) =< aux(6)
s(12) =< aux(6)
s(12) =< aux(26)
it(31) =< aux(27)
it(33) =< aux(27)
it(34) =< aux(27)

  with precondition: [V=0,V1>=12,Out>=6,7*V1+26>=10*Out] 

* Chain [40,38,30]: 1*s(1)+5
  Such that:s(1) =< V1/2

  with precondition: [V=0,Out>=6,V1+20>=4*Out] 

* Chain [40,37,30]: 1*s(14)+1*s(15)+5
  Such that:s(15) =< 2
s(14) =< V1/2

  with precondition: [V=0,Out>=7,V1+24>=4*Out] 

* Chain [40,36,30]: 1*s(16)+5
  Such that:s(16) =< 2

  with precondition: [V=0,Out=6,V1>=4] 

* Chain [40,35,30]: 5
  with precondition: [V=0,Out=5,V1>=4] 

* Chain [40,30]: 3
  with precondition: [V=0,Out=3,V1>=2] 

* Chain [40,28]: 1*s(17)+1*s(18)+3
  Such that:s(17) =< 1
s(18) =< V1/2

  with precondition: [V=0,Out=4,V1>=2] 

* Chain [40,27]: 1*s(19)+3
  Such that:s(19) =< 1

  with precondition: [V=0,Out=4,V1>=4] 

* Chain [39,[31,32,33,34],38,30]: 4*it(31)+2*it(33)+2*it(34)+1*s(1)+1*s(10)+2*s(11)+1*s(12)+1*s(21)+5
  Such that:aux(9) =< 2*V1
aux(10) =< V1/2
aux(8) =< V1/4
aux(5) =< 3/2*V1+1
aux(6) =< 3/2*V1+2
aux(11) =< 5/2*V1
aux(30) =< V1
s(21) =< aux(30)
s(1) =< aux(11)
it(31) =< aux(10)
it(33) =< aux(10)
it(34) =< aux(10)
it(34) =< aux(30)
s(11) =< aux(30)
it(34) =< aux(11)
s(11) =< aux(11)
it(33) =< aux(5)
it(34) =< aux(5)
s(10) =< aux(5)
it(34) =< aux(6)
s(12) =< aux(6)
it(33) =< aux(11)
s(10) =< aux(11)
s(12) =< aux(11)
it(31) =< aux(8)
it(33) =< aux(8)
it(34) =< aux(8)
it(31) =< aux(9)
it(33) =< aux(9)
it(34) =< aux(9)

  with precondition: [V=0,V1>=12,Out>=9,47*V1+176>=40*Out] 

* Chain [39,[31,32,33,34],37,30]: 4*it(31)+2*it(33)+2*it(34)+1*s(10)+2*s(11)+1*s(12)+1*s(14)+1*s(15)+1*s(21)+5
  Such that:aux(9) =< 2*V1
aux(12) =< V1/2
aux(8) =< V1/4
aux(5) =< 3/2*V1+1
aux(13) =< 3/2*V1+2
aux(14) =< 5/2*V1
aux(31) =< V1
s(21) =< aux(31)
s(15) =< aux(13)
s(14) =< aux(14)
it(31) =< aux(12)
it(33) =< aux(12)
it(34) =< aux(12)
it(34) =< aux(31)
s(11) =< aux(31)
it(34) =< aux(14)
s(11) =< aux(14)
it(33) =< aux(5)
it(34) =< aux(5)
s(10) =< aux(5)
it(34) =< aux(13)
s(12) =< aux(13)
it(33) =< aux(14)
s(10) =< aux(14)
s(12) =< aux(14)
it(31) =< aux(8)
it(33) =< aux(8)
it(34) =< aux(8)
it(31) =< aux(9)
it(33) =< aux(9)
it(34) =< aux(9)

  with precondition: [V=0,V1>=12,Out>=10,49*V1+232>=40*Out] 

* Chain [39,[31,32,33,34],36,30]: 4*it(31)+2*it(33)+2*it(34)+1*s(10)+4*s(11)+1*s(12)+5
  Such that:aux(15) =< V1/2
aux(18) =< V1/4
aux(5) =< 3/2*V1+1
aux(17) =< 3/2*V1+2
aux(32) =< V1
s(11) =< aux(32)
it(31) =< aux(15)
it(33) =< aux(15)
it(34) =< aux(15)
it(34) =< aux(32)
it(33) =< aux(5)
it(34) =< aux(5)
s(10) =< aux(5)
it(34) =< aux(17)
s(12) =< aux(17)
it(33) =< aux(17)
s(10) =< aux(17)
it(31) =< aux(18)
it(33) =< aux(18)
it(34) =< aux(18)

  with precondition: [V=0,V1>=12,Out>=9,6*V1+23>=5*Out] 

* Chain [39,[31,32,33,34],35,30]: 4*it(31)+2*it(33)+2*it(34)+1*s(10)+3*s(11)+1*s(12)+5
  Such that:aux(19) =< V1/4
aux(7) =< 3/2*V1
aux(5) =< 3/2*V1+1
aux(6) =< 3/2*V1+2
aux(33) =< V1
aux(34) =< V1/2
s(11) =< aux(33)
it(31) =< aux(34)
it(33) =< aux(34)
it(34) =< aux(34)
it(34) =< aux(33)
it(33) =< aux(5)
it(34) =< aux(5)
s(10) =< aux(5)
it(34) =< aux(6)
s(12) =< aux(6)
it(33) =< aux(7)
it(34) =< aux(7)
s(10) =< aux(7)
s(12) =< aux(7)
it(31) =< aux(19)
it(33) =< aux(19)
it(34) =< aux(19)

  with precondition: [V=0,V1>=12,Out>=8,23*V1+64>=20*Out] 

* Chain [39,[31,32,33,34],30]: 4*it(31)+2*it(33)+2*it(34)+1*s(10)+2*s(11)+1*s(12)+1*s(21)+3
  Such that:aux(21) =< 2*V1
aux(20) =< V1/2
aux(8) =< V1/4
aux(5) =< 3/2*V1+1
aux(6) =< 3/2*V1+2
aux(4) =< 5/2*V1
aux(35) =< V1
s(21) =< aux(35)
it(31) =< aux(20)
it(33) =< aux(20)
it(34) =< aux(20)
it(34) =< aux(35)
s(11) =< aux(35)
it(34) =< aux(4)
s(11) =< aux(4)
it(33) =< aux(5)
it(34) =< aux(5)
s(10) =< aux(5)
it(34) =< aux(6)
s(12) =< aux(6)
it(33) =< aux(21)
it(34) =< aux(21)
s(10) =< aux(21)
s(12) =< aux(21)
it(31) =< aux(8)
it(33) =< aux(8)
it(34) =< aux(8)
it(31) =< aux(21)

  with precondition: [V=0,V1>=4,Out>=6,23*V1+52>=16*Out] 

* Chain [39,[31,32,33,34],28]: 4*it(31)+2*it(33)+2*it(34)+3*s(10)+2*s(11)+1*s(12)+1*s(21)+3
  Such that:aux(9) =< 2*V1
aux(22) =< V1/2
aux(8) =< V1/4
aux(23) =< 3/2*V1+1
aux(6) =< 3/2*V1+2
aux(4) =< 5/2*V1
aux(36) =< V1
s(21) =< aux(36)
s(10) =< aux(23)
it(31) =< aux(22)
it(33) =< aux(22)
it(34) =< aux(22)
it(34) =< aux(36)
s(11) =< aux(36)
it(34) =< aux(4)
s(11) =< aux(4)
it(33) =< aux(23)
it(34) =< aux(23)
it(34) =< aux(6)
s(12) =< aux(6)
s(12) =< aux(23)
it(31) =< aux(8)
it(33) =< aux(8)
it(34) =< aux(8)
it(31) =< aux(9)
it(33) =< aux(9)
it(34) =< aux(9)

  with precondition: [V=0,V1>=4,Out>=7,3*V1+8>=2*Out] 

* Chain [39,[31,32,33,34],27]: 4*it(31)+2*it(33)+2*it(34)+1*s(10)+4*s(11)+1*s(12)+3
  Such that:aux(24) =< V1/2
aux(27) =< V1/4
aux(26) =< 3/2*V1+1
aux(6) =< 3/2*V1+2
aux(37) =< V1
s(11) =< aux(37)
it(31) =< aux(24)
it(33) =< aux(24)
it(34) =< aux(24)
it(34) =< aux(37)
it(33) =< aux(26)
it(34) =< aux(26)
s(10) =< aux(26)
it(34) =< aux(6)
s(12) =< aux(6)
s(12) =< aux(26)
it(31) =< aux(27)
it(33) =< aux(27)
it(34) =< aux(27)

  with precondition: [V=0,V1>=12,Out>=7,6*V1+13>=5*Out] 

* Chain [39,38,30]: 1*s(1)+1*s(21)+5
  Such that:s(21) =< V1
s(1) =< V1/2

  with precondition: [V=0,V1>=4,Out>=7,3*V1+20>=4*Out] 

* Chain [39,37,30]: 1*s(14)+1*s(15)+1*s(21)+5
  Such that:s(15) =< 2
s(21) =< V1
s(14) =< V1/2

  with precondition: [V=0,V1>=4,Out>=8,3*V1+24>=4*Out] 

* Chain [39,36,30]: 1*s(16)+1*s(21)+5
  Such that:s(16) =< 2
s(21) =< V1

  with precondition: [V=0,V1>=4,Out>=7,V1+12>=2*Out] 

* Chain [39,35,30]: 1*s(21)+5
  Such that:s(21) =< V1

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

* Chain [39,30]: 1*s(21)+3
  Such that:s(21) =< V1

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

* Chain [39,28]: 1*s(17)+1*s(18)+1*s(21)+3
  Such that:s(17) =< 1
s(21) =< V1
s(18) =< V1/2

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

* Chain [39,27]: 1*s(19)+1*s(21)+3
  Such that:s(19) =< 1
s(21) =< V1

  with precondition: [V=0,V1>=4,Out>=5,V1+8>=2*Out] 

* Chain [38,30]: 1*s(1)+3
  Such that:s(1) =< V1

  with precondition: [V>=1,Out>=4,V1+6>=2*Out,V1>=V+1] 

* Chain [37,30]: 1*s(14)+1*s(15)+3
  Such that:s(14) =< V1
s(15) =< V+1

  with precondition: [V>=1,Out>=5,V1>=V+1,V1+2*V+6>=2*Out] 

* Chain [36,30]: 1*s(16)+3
  Such that:s(16) =< V+1

  with precondition: [Out>=4,V1>=V+1,V+3>=Out] 

* Chain [35,30]: 3
  with precondition: [Out=3,V>=1,V1>=V+1] 

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

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

* Chain [28]: 1*s(17)+1*s(18)+1
  Such that:s(18) =< V1
s(17) =< V

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

* Chain [27]: 1*s(19)+1
  Such that:s(19) =< V

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


#### Cost of chains of fun4(V1,V,Out):
* Chain [47]: 1
  with precondition: [V1=2,Out=2,V>=0] 

* Chain [46]: 1*s(294)+2*s(296)+1
  Such that:s(295) =< 1
s(294) =< V
s(296) =< s(295)

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

* Chain [45]: 2*s(308)+2*s(309)+12*s(310)+2*s(311)+2*s(312)+8*s(313)+1*s(314)+1*s(315)+12*s(316)+2*s(317)+6*s(318)+6*s(319)+1*s(320)+1*s(321)+2*s(322)+2*s(323)+4*s(324)+2*s(325)+2*s(326)+2*s(329)+4*s(330)+2*s(331)+2*s(332)+1*s(333)+3
  Such that:s(307) =< 2
s(299) =< 3*V
s(302) =< 3*V+1
s(303) =< 3*V+2
s(304) =< 4*V
s(305) =< 5*V
s(306) =< V/2
aux(64) =< V
aux(65) =< 2*V
s(308) =< aux(64)
s(309) =< s(307)
s(310) =< aux(64)
s(311) =< aux(64)
s(312) =< aux(64)
s(312) =< aux(65)
s(313) =< aux(65)
s(311) =< s(302)
s(312) =< s(302)
s(314) =< s(302)
s(312) =< s(303)
s(315) =< s(303)
s(311) =< s(299)
s(312) =< s(299)
s(314) =< s(299)
s(315) =< s(299)
s(310) =< s(306)
s(311) =< s(306)
s(312) =< s(306)
s(316) =< aux(64)
s(317) =< aux(64)
s(318) =< aux(64)
s(318) =< aux(65)
s(319) =< aux(65)
s(318) =< s(305)
s(319) =< s(305)
s(317) =< s(302)
s(318) =< s(302)
s(320) =< s(302)
s(318) =< s(303)
s(321) =< s(303)
s(317) =< s(304)
s(318) =< s(304)
s(320) =< s(304)
s(321) =< s(304)
s(316) =< s(306)
s(317) =< s(306)
s(318) =< s(306)
s(316) =< s(304)
s(322) =< s(303)
s(323) =< s(305)
s(324) =< aux(64)
s(324) =< s(302)
s(325) =< s(302)
s(326) =< s(303)
s(324) =< s(305)
s(325) =< s(305)
s(326) =< s(305)
s(324) =< s(306)
s(324) =< s(304)
s(329) =< aux(64)
s(330) =< aux(64)
s(330) =< aux(65)
s(329) =< s(302)
s(330) =< s(302)
s(331) =< s(302)
s(330) =< s(303)
s(329) =< s(303)
s(331) =< s(303)
s(329) =< s(306)
s(330) =< s(306)
s(332) =< aux(64)
s(332) =< s(302)
s(333) =< s(302)
s(332) =< s(306)

  with precondition: [V1=2,V>=2,Out>=4,15*V+18>=8*Out] 

* Chain [44]: 3*s(341)+4*s(342)+2*s(343)+2*s(344)+2*s(345)+1*s(346)+1
  Such that:s(339) =< V
s(334) =< 2*V
s(340) =< 3*V+1
s(335) =< 3*V+2
s(336) =< 4*V
s(337) =< 5*V
s(338) =< V/2
s(341) =< s(340)
s(342) =< s(339)
s(343) =< s(339)
s(344) =< s(339)
s(344) =< s(334)
s(345) =< s(334)
s(344) =< s(337)
s(345) =< s(337)
s(343) =< s(340)
s(344) =< s(340)
s(344) =< s(335)
s(346) =< s(335)
s(346) =< s(340)
s(342) =< s(338)
s(343) =< s(338)
s(344) =< s(338)
s(342) =< s(336)
s(343) =< s(336)
s(344) =< s(336)

  with precondition: [V1=2,V>=2,Out>=5,2*V+3>=Out] 

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


#### Cost of chains of fun5(V1,Out):
* Chain [53]: 0
  with precondition: [Out=1,V1>=0] 

* Chain [52]: 0
  with precondition: [Out=0,V1>=0] 

* Chain [51]: 1
  with precondition: [Out=3,V1>=1] 

* Chain [50]: 1*s(348)+2*s(349)+1
  Such that:s(347) =< 1
s(348) =< V1
s(349) =< s(347)

  with precondition: [Out=4,V1>=1] 

* Chain [49]: 2*s(359)+2*s(360)+12*s(361)+2*s(362)+2*s(363)+8*s(364)+1*s(365)+1*s(366)+12*s(367)+2*s(368)+6*s(369)+6*s(370)+1*s(371)+1*s(372)+2*s(373)+2*s(374)+4*s(375)+2*s(376)+2*s(377)+2*s(378)+4*s(379)+2*s(380)+2*s(381)+1*s(382)+3
  Such that:s(350) =< 2
s(357) =< V1
s(358) =< 2*V1
s(351) =< 3*V1
s(352) =< 3*V1+1
s(353) =< 3*V1+2
s(354) =< 4*V1
s(355) =< 5*V1
s(356) =< V1/2
s(359) =< s(357)
s(360) =< s(350)
s(361) =< s(357)
s(362) =< s(357)
s(363) =< s(357)
s(363) =< s(358)
s(364) =< s(358)
s(362) =< s(352)
s(363) =< s(352)
s(365) =< s(352)
s(363) =< s(353)
s(366) =< s(353)
s(362) =< s(351)
s(363) =< s(351)
s(365) =< s(351)
s(366) =< s(351)
s(361) =< s(356)
s(362) =< s(356)
s(363) =< s(356)
s(367) =< s(357)
s(368) =< s(357)
s(369) =< s(357)
s(369) =< s(358)
s(370) =< s(358)
s(369) =< s(355)
s(370) =< s(355)
s(368) =< s(352)
s(369) =< s(352)
s(371) =< s(352)
s(369) =< s(353)
s(372) =< s(353)
s(368) =< s(354)
s(369) =< s(354)
s(371) =< s(354)
s(372) =< s(354)
s(367) =< s(356)
s(368) =< s(356)
s(369) =< s(356)
s(367) =< s(354)
s(373) =< s(353)
s(374) =< s(355)
s(375) =< s(357)
s(375) =< s(352)
s(376) =< s(352)
s(377) =< s(353)
s(375) =< s(355)
s(376) =< s(355)
s(377) =< s(355)
s(375) =< s(356)
s(375) =< s(354)
s(378) =< s(357)
s(379) =< s(357)
s(379) =< s(358)
s(378) =< s(352)
s(379) =< s(352)
s(380) =< s(352)
s(379) =< s(353)
s(378) =< s(353)
s(380) =< s(353)
s(378) =< s(356)
s(379) =< s(356)
s(381) =< s(357)
s(381) =< s(352)
s(382) =< s(352)
s(381) =< s(356)

  with precondition: [V1>=2,Out>=5,15*V1+26>=8*Out] 

* Chain [48]: 3*s(390)+4*s(391)+2*s(392)+2*s(393)+2*s(394)+1*s(395)+1
  Such that:s(383) =< V1
s(384) =< 2*V1
s(385) =< 3*V1+1
s(386) =< 3*V1+2
s(387) =< 4*V1
s(388) =< 5*V1
s(389) =< V1/2
s(390) =< s(385)
s(391) =< s(383)
s(392) =< s(383)
s(393) =< s(383)
s(393) =< s(384)
s(394) =< s(384)
s(393) =< s(388)
s(394) =< s(388)
s(392) =< s(385)
s(393) =< s(385)
s(393) =< s(386)
s(395) =< s(386)
s(395) =< s(385)
s(391) =< s(389)
s(392) =< s(389)
s(393) =< s(389)
s(391) =< s(387)
s(392) =< s(387)
s(393) =< s(387)

  with precondition: [V1>=2,Out>=6,2*V1+4>=Out] 


#### Cost of chains of start(V1,V,V6):
* Chain [56]: 3*s(396)+7*s(408)+2*s(409)+4*s(410)+2*s(411)+2*s(412)+2*s(413)+1*s(414)+1*s(415)+16*s(416)+4*s(417)+8*s(418)+8*s(419)+1*s(420)+1*s(421)+2*s(422)+4*s(423)+4*s(424)+2*s(425)+2*s(426)+6*s(427)+8*s(428)+2*s(429)+4*s(430)+3*s(431)+2*s(432)+4*s(433)+2*s(453)+2*s(464)+12*s(465)+2*s(466)+2*s(467)+8*s(468)+1*s(469)+1*s(470)+16*s(471)+4*s(472)+8*s(473)+8*s(474)+1*s(475)+1*s(476)+2*s(477)+4*s(479)+2*s(480)+2*s(481)+2*s(482)+4*s(483)+3*s(484)+2*s(485)+4*s(486)+3
  Such that:s(451) =< 1
s(454) =< 2
s(397) =< V1-V
s(398) =< 2*V1-2*V
s(457) =< 3*V1
s(399) =< 3*V1-3*V
s(407) =< V+1
aux(66) =< V1
aux(67) =< 2*V1
aux(68) =< 2*V1-V
aux(69) =< 3*V1+1
aux(70) =< 3*V1+2
aux(71) =< 3*V1+V
aux(72) =< 3*V1+V+1
aux(73) =< 4*V1
aux(74) =< 5*V1
aux(75) =< V1/2
aux(76) =< V1/2-V/2
aux(77) =< V
s(408) =< aux(66)
s(396) =< aux(77)
s(453) =< s(451)
s(464) =< s(454)
s(465) =< aux(66)
s(466) =< aux(66)
s(467) =< aux(66)
s(467) =< aux(67)
s(468) =< aux(67)
s(466) =< aux(69)
s(467) =< aux(69)
s(469) =< aux(69)
s(467) =< aux(70)
s(470) =< aux(70)
s(466) =< s(457)
s(467) =< s(457)
s(469) =< s(457)
s(470) =< s(457)
s(465) =< aux(75)
s(466) =< aux(75)
s(467) =< aux(75)
s(471) =< aux(66)
s(472) =< aux(66)
s(473) =< aux(66)
s(473) =< aux(67)
s(474) =< aux(67)
s(473) =< aux(74)
s(474) =< aux(74)
s(472) =< aux(69)
s(473) =< aux(69)
s(475) =< aux(69)
s(473) =< aux(70)
s(476) =< aux(70)
s(472) =< aux(73)
s(473) =< aux(73)
s(475) =< aux(73)
s(476) =< aux(73)
s(471) =< aux(75)
s(472) =< aux(75)
s(473) =< aux(75)
s(471) =< aux(73)
s(477) =< aux(70)
s(423) =< aux(74)
s(479) =< aux(66)
s(479) =< aux(69)
s(480) =< aux(69)
s(481) =< aux(70)
s(479) =< aux(74)
s(480) =< aux(74)
s(481) =< aux(74)
s(479) =< aux(75)
s(479) =< aux(73)
s(482) =< aux(66)
s(483) =< aux(66)
s(483) =< aux(67)
s(482) =< aux(69)
s(483) =< aux(69)
s(484) =< aux(69)
s(483) =< aux(70)
s(482) =< aux(70)
s(484) =< aux(70)
s(482) =< aux(75)
s(483) =< aux(75)
s(485) =< aux(66)
s(485) =< aux(69)
s(486) =< aux(69)
s(485) =< aux(75)
s(409) =< s(407)
s(410) =< aux(66)
s(411) =< aux(66)
s(412) =< aux(66)
s(410) =< s(397)
s(411) =< s(397)
s(412) =< s(397)
s(412) =< aux(68)
s(413) =< aux(68)
s(412) =< s(398)
s(413) =< s(398)
s(411) =< aux(71)
s(412) =< aux(71)
s(414) =< aux(71)
s(412) =< aux(72)
s(415) =< aux(72)
s(411) =< s(399)
s(412) =< s(399)
s(414) =< s(399)
s(415) =< s(399)
s(410) =< aux(76)
s(411) =< aux(76)
s(412) =< aux(76)
s(416) =< aux(66)
s(417) =< aux(66)
s(418) =< aux(66)
s(418) =< aux(68)
s(419) =< aux(68)
s(418) =< aux(74)
s(419) =< aux(74)
s(417) =< aux(71)
s(418) =< aux(71)
s(420) =< aux(71)
s(418) =< aux(72)
s(421) =< aux(72)
s(417) =< aux(73)
s(418) =< aux(73)
s(420) =< aux(73)
s(421) =< aux(73)
s(416) =< aux(76)
s(417) =< aux(76)
s(418) =< aux(76)
s(416) =< aux(73)
s(422) =< aux(72)
s(424) =< aux(66)
s(424) =< aux(71)
s(425) =< aux(71)
s(426) =< aux(72)
s(424) =< aux(74)
s(425) =< aux(74)
s(426) =< aux(74)
s(424) =< aux(76)
s(424) =< aux(73)
s(427) =< aux(68)
s(428) =< aux(66)
s(429) =< aux(66)
s(430) =< aux(66)
s(430) =< aux(68)
s(429) =< aux(71)
s(430) =< aux(71)
s(431) =< aux(71)
s(430) =< aux(72)
s(429) =< aux(72)
s(431) =< aux(72)
s(428) =< aux(76)
s(429) =< aux(76)
s(430) =< aux(76)
s(432) =< aux(66)
s(432) =< aux(71)
s(433) =< aux(71)
s(432) =< aux(76)

  with precondition: [V1>=0] 

* Chain [55]: 8*s(500)+6*s(513)+4*s(514)+8*s(515)+4*s(516)+4*s(517)+4*s(518)+2*s(519)+2*s(520)+32*s(521)+8*s(522)+16*s(523)+16*s(524)+2*s(525)+2*s(526)+4*s(527)+4*s(528)+8*s(529)+4*s(530)+4*s(531)+12*s(532)+16*s(533)+4*s(534)+8*s(535)+6*s(536)+4*s(537)+8*s(538)+4*s(606)+2*s(613)+2*s(624)+12*s(625)+2*s(626)+2*s(627)+8*s(628)+1*s(629)+1*s(630)+16*s(631)+4*s(632)+8*s(633)+8*s(634)+1*s(635)+1*s(636)+2*s(637)+2*s(638)+4*s(639)+2*s(640)+2*s(641)+2*s(642)+4*s(643)+3*s(644)+2*s(645)+4*s(646)+4
  Such that:s(611) =< 1
s(614) =< 2
s(615) =< 3*V
aux(78) =< V
aux(79) =< V-2*V6
aux(80) =< V-V6
aux(81) =< 2*V
aux(82) =< 3*V+1
aux(83) =< 3*V+2
aux(84) =< 4*V
aux(85) =< 5*V
aux(86) =< V/2
aux(87) =< V/2-V6
aux(88) =< V/4-V6/2
aux(89) =< 3/2*V-3*V6
aux(90) =< 3/2*V+V6+1
aux(91) =< 3/2*V+V6+2
aux(92) =< 5/2*V
aux(93) =< V6+1
aux(94) =< V6+2
s(500) =< aux(78)
s(513) =< aux(86)
s(613) =< s(611)
s(624) =< s(614)
s(625) =< aux(78)
s(626) =< aux(78)
s(627) =< aux(78)
s(627) =< aux(81)
s(628) =< aux(81)
s(626) =< aux(82)
s(627) =< aux(82)
s(629) =< aux(82)
s(627) =< aux(83)
s(630) =< aux(83)
s(626) =< s(615)
s(627) =< s(615)
s(629) =< s(615)
s(630) =< s(615)
s(625) =< aux(86)
s(626) =< aux(86)
s(627) =< aux(86)
s(631) =< aux(78)
s(632) =< aux(78)
s(633) =< aux(78)
s(633) =< aux(81)
s(634) =< aux(81)
s(633) =< aux(85)
s(634) =< aux(85)
s(632) =< aux(82)
s(633) =< aux(82)
s(635) =< aux(82)
s(633) =< aux(83)
s(636) =< aux(83)
s(632) =< aux(84)
s(633) =< aux(84)
s(635) =< aux(84)
s(636) =< aux(84)
s(631) =< aux(86)
s(632) =< aux(86)
s(633) =< aux(86)
s(631) =< aux(84)
s(637) =< aux(83)
s(638) =< aux(85)
s(639) =< aux(78)
s(639) =< aux(82)
s(640) =< aux(82)
s(641) =< aux(83)
s(639) =< aux(85)
s(640) =< aux(85)
s(641) =< aux(85)
s(639) =< aux(86)
s(639) =< aux(84)
s(642) =< aux(78)
s(643) =< aux(78)
s(643) =< aux(81)
s(642) =< aux(82)
s(643) =< aux(82)
s(644) =< aux(82)
s(643) =< aux(83)
s(642) =< aux(83)
s(644) =< aux(83)
s(642) =< aux(86)
s(643) =< aux(86)
s(645) =< aux(78)
s(645) =< aux(82)
s(646) =< aux(82)
s(645) =< aux(86)
s(514) =< aux(94)
s(515) =< aux(86)
s(516) =< aux(86)
s(517) =< aux(86)
s(515) =< aux(87)
s(516) =< aux(87)
s(517) =< aux(87)
s(517) =< aux(80)
s(518) =< aux(80)
s(517) =< aux(79)
s(518) =< aux(79)
s(516) =< aux(90)
s(517) =< aux(90)
s(519) =< aux(90)
s(517) =< aux(91)
s(520) =< aux(91)
s(516) =< aux(89)
s(517) =< aux(89)
s(519) =< aux(89)
s(520) =< aux(89)
s(515) =< aux(88)
s(516) =< aux(88)
s(517) =< aux(88)
s(521) =< aux(86)
s(522) =< aux(86)
s(523) =< aux(86)
s(523) =< aux(80)
s(524) =< aux(80)
s(523) =< aux(92)
s(524) =< aux(92)
s(522) =< aux(90)
s(523) =< aux(90)
s(525) =< aux(90)
s(523) =< aux(91)
s(526) =< aux(91)
s(522) =< aux(81)
s(523) =< aux(81)
s(525) =< aux(81)
s(526) =< aux(81)
s(521) =< aux(88)
s(522) =< aux(88)
s(523) =< aux(88)
s(521) =< aux(81)
s(527) =< aux(91)
s(528) =< aux(92)
s(529) =< aux(86)
s(529) =< aux(90)
s(530) =< aux(90)
s(531) =< aux(91)
s(529) =< aux(92)
s(530) =< aux(92)
s(531) =< aux(92)
s(529) =< aux(88)
s(529) =< aux(81)
s(532) =< aux(80)
s(533) =< aux(86)
s(534) =< aux(86)
s(535) =< aux(86)
s(535) =< aux(80)
s(534) =< aux(90)
s(535) =< aux(90)
s(536) =< aux(90)
s(535) =< aux(91)
s(534) =< aux(91)
s(536) =< aux(91)
s(533) =< aux(88)
s(534) =< aux(88)
s(535) =< aux(88)
s(537) =< aux(86)
s(537) =< aux(90)
s(538) =< aux(90)
s(537) =< aux(88)
s(606) =< aux(93)

  with precondition: [V1=2,V>=0] 

* Chain [54]: 6*s(660)+4*s(663)+31*s(664)+4*s(666)+24*s(677)+4*s(678)+8*s(679)+8*s(680)+6*s(681)+32*s(682)+8*s(683)+16*s(684)+16*s(685)+2*s(686)+2*s(687)+4*s(688)+4*s(689)+4*s(690)+8*s(691)+4*s(692)+4*s(693)+4*s(694)+4*s(695)+2*s(696)+2*s(697)+5
  Such that:aux(95) =< 1
aux(96) =< 2
aux(97) =< V1
aux(98) =< 2*V1
aux(99) =< V1/2
aux(100) =< V1/4
aux(101) =< 3/2*V1
aux(102) =< 3/2*V1+1
aux(103) =< 3/2*V1+2
aux(104) =< 5/2*V1
s(663) =< aux(95)
s(666) =< aux(96)
s(664) =< aux(97)
s(660) =< aux(99)
s(677) =< aux(99)
s(678) =< aux(99)
s(679) =< aux(99)
s(679) =< aux(97)
s(678) =< aux(102)
s(679) =< aux(102)
s(680) =< aux(102)
s(679) =< aux(103)
s(681) =< aux(103)
s(681) =< aux(102)
s(677) =< aux(100)
s(678) =< aux(100)
s(679) =< aux(100)
s(682) =< aux(99)
s(683) =< aux(99)
s(684) =< aux(99)
s(684) =< aux(97)
s(685) =< aux(97)
s(684) =< aux(104)
s(685) =< aux(104)
s(683) =< aux(102)
s(684) =< aux(102)
s(686) =< aux(102)
s(684) =< aux(103)
s(687) =< aux(103)
s(683) =< aux(98)
s(684) =< aux(98)
s(686) =< aux(98)
s(687) =< aux(98)
s(682) =< aux(100)
s(683) =< aux(100)
s(684) =< aux(100)
s(682) =< aux(98)
s(688) =< aux(99)
s(688) =< aux(102)
s(689) =< aux(103)
s(688) =< aux(103)
s(688) =< aux(100)
s(690) =< aux(104)
s(691) =< aux(99)
s(691) =< aux(102)
s(692) =< aux(102)
s(693) =< aux(103)
s(691) =< aux(104)
s(692) =< aux(104)
s(693) =< aux(104)
s(691) =< aux(100)
s(691) =< aux(98)
s(694) =< aux(99)
s(695) =< aux(99)
s(695) =< aux(97)
s(694) =< aux(102)
s(695) =< aux(102)
s(696) =< aux(102)
s(695) =< aux(103)
s(697) =< aux(103)
s(694) =< aux(101)
s(695) =< aux(101)
s(696) =< aux(101)
s(697) =< aux(101)
s(694) =< aux(100)
s(695) =< aux(100)

  with precondition: [V=0,V1>=0] 


Closed-form bounds of start(V1,V,V6): 
-------------------------------------
* Chain [56] with precondition: [V1>=0] 
    - Upper bound: 119*V1+9+nat(V)*3+32*V1+20*V1+nat(V+1)*2+nat(3*V1+V)*11+(33*V1+11)+(18*V1+12)+nat(3*V1+V+1)*6+nat(2*V1-V)*16 
    - Complexity: n 
* Chain [55] with precondition: [V1=2,V>=0] 
    - Upper bound: 116*V+10+nat(V6+1)*4+nat(V6+2)*4+(33*V+11)+(18*V+12)+nat(3/2*V+V6+1)*22+nat(3/2*V+V6+2)*12+nat(V-V6)*32+59*V 
    - Complexity: n 
* Chain [54] with precondition: [V=0,V1>=0] 
    - Upper bound: 167*V1+69 
    - Complexity: n 

### Maximum cost of start(V1,V,V6): max([47*V1+max([120*V1+60,nat(V)*3+72*V1+32*V1+20*V1+nat(V+1)*2+nat(3*V1+V)*11+(33*V1+11)+(18*V1+12)+nat(3*V1+V+1)*6+nat(2*V1-V)*16]),nat(V)*64+1+nat(2*V)*16+nat(5*V)*2+nat(5/2*V)*4+nat(V6+1)*4+nat(V6+2)*4+nat(3*V+1)*11+nat(3*V+2)*6+nat(3/2*V+V6+1)*22+nat(3/2*V+V6+2)*12+nat(V-V6)*32+nat(V/2)*118])+9 
Asymptotic class: n 
* Total analysis performed in 2159 ms.


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

(22)
BOUNDS(1, n^1)

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

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

(24)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   lt(0, s(z0)) -> true
   lt(z0, 0) -> false
   lt(s(z0), s(z1)) -> lt(z0, z1)
   logarithm(z0) -> ifa(lt(0, z0), z0)
   ifa(true, z0) -> help(z0, 1)
   ifa(false, z0) -> logZeroError
   help(z0, z1) -> ifb(lt(z1, z0), z0, z1)
   ifb(true, z0, z1) -> help(half(z0), s(z1))
   ifb(false, z0, z1) -> z1
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(z0))) -> s(half(z0))
Tuples:
   LT(0, s(z0)) -> c
   LT(z0, 0) -> c1
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   LOGARITHM(z0) -> c3(IFA(lt(0, z0), z0), LT(0, z0))
   IFA(true, z0) -> c4(HELP(z0, 1))
   IFA(false, z0) -> c5
   HELP(z0, z1) -> c6(IFB(lt(z1, z0), z0, z1), LT(z1, z0))
   IFB(true, z0, z1) -> c7(HELP(half(z0), s(z1)), HALF(z0))
   IFB(false, z0, z1) -> c8
   HALF(0) -> c9
   HALF(s(0)) -> c10
   HALF(s(s(z0))) -> c11(HALF(z0))
S tuples:
   LT(0, s(z0)) -> c
   LT(z0, 0) -> c1
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   LOGARITHM(z0) -> c3(IFA(lt(0, z0), z0), LT(0, z0))
   IFA(true, z0) -> c4(HELP(z0, 1))
   IFA(false, z0) -> c5
   HELP(z0, z1) -> c6(IFB(lt(z1, z0), z0, z1), LT(z1, z0))
   IFB(true, z0, z1) -> c7(HELP(half(z0), s(z1)), HALF(z0))
   IFB(false, z0, z1) -> c8
   HALF(0) -> c9
   HALF(s(0)) -> c10
   HALF(s(s(z0))) -> c11(HALF(z0))
K tuples:none
Defined Rule Symbols:   lt_2, logarithm_1, ifa_2, help_2, ifb_3, half_1

Defined Pair Symbols:   LT_2, LOGARITHM_1, IFA_2, HELP_2, IFB_3, HALF_1

Compound Symbols:   c, c1, c2_1, c3_2, c4_1, c5, c6_2, c7_2, c8, c9, c10, c11_1


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

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

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

   LT(0, s(z0)) -> c
   LT(z0, 0) -> c1
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   LOGARITHM(z0) -> c3(IFA(lt(0, z0), z0), LT(0, z0))
   IFA(true, z0) -> c4(HELP(z0, 1))
   IFA(false, z0) -> c5
   HELP(z0, z1) -> c6(IFB(lt(z1, z0), z0, z1), LT(z1, z0))
   IFB(true, z0, z1) -> c7(HELP(half(z0), s(z1)), HALF(z0))
   IFB(false, z0, z1) -> c8
   HALF(0) -> c9
   HALF(s(0)) -> c10
   HALF(s(s(z0))) -> c11(HALF(z0))

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

   lt(0, s(z0)) -> true
   lt(z0, 0) -> false
   lt(s(z0), s(z1)) -> lt(z0, z1)
   logarithm(z0) -> ifa(lt(0, z0), z0)
   ifa(true, z0) -> help(z0, 1)
   ifa(false, z0) -> logZeroError
   help(z0, z1) -> ifb(lt(z1, z0), z0, z1)
   ifb(true, z0, z1) -> help(half(z0), s(z1))
   ifb(false, z0, z1) -> z1
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(z0))) -> s(half(z0))

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

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

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

   LT(0', s(z0)) -> c
   LT(z0, 0') -> c1
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   LOGARITHM(z0) -> c3(IFA(lt(0', z0), z0), LT(0', z0))
   IFA(true, z0) -> c4(HELP(z0, 1'))
   IFA(false, z0) -> c5
   HELP(z0, z1) -> c6(IFB(lt(z1, z0), z0, z1), LT(z1, z0))
   IFB(true, z0, z1) -> c7(HELP(half(z0), s(z1)), HALF(z0))
   IFB(false, z0, z1) -> c8
   HALF(0') -> c9
   HALF(s(0')) -> c10
   HALF(s(s(z0))) -> c11(HALF(z0))

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

   lt(0', s(z0)) -> true
   lt(z0, 0') -> false
   lt(s(z0), s(z1)) -> lt(z0, z1)
   logarithm(z0) -> ifa(lt(0', z0), z0)
   ifa(true, z0) -> help(z0, 1')
   ifa(false, z0) -> logZeroError
   help(z0, z1) -> ifb(lt(z1, z0), z0, z1)
   ifb(true, z0, z1) -> help(half(z0), s(z1))
   ifb(false, z0, z1) -> z1
   half(0') -> 0'
   half(s(0')) -> 0'
   half(s(s(z0))) -> s(half(z0))

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

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

(30)
Obligation:
Innermost TRS:
Rules:
LT(0', s(z0)) -> c
LT(z0, 0') -> c1
LT(s(z0), s(z1)) -> c2(LT(z0, z1))
LOGARITHM(z0) -> c3(IFA(lt(0', z0), z0), LT(0', z0))
IFA(true, z0) -> c4(HELP(z0, 1'))
IFA(false, z0) -> c5
HELP(z0, z1) -> c6(IFB(lt(z1, z0), z0, z1), LT(z1, z0))
IFB(true, z0, z1) -> c7(HELP(half(z0), s(z1)), HALF(z0))
IFB(false, z0, z1) -> c8
HALF(0') -> c9
HALF(s(0')) -> c10
HALF(s(s(z0))) -> c11(HALF(z0))
lt(0', s(z0)) -> true
lt(z0, 0') -> false
lt(s(z0), s(z1)) -> lt(z0, z1)
logarithm(z0) -> ifa(lt(0', z0), z0)
ifa(true, z0) -> help(z0, 1')
ifa(false, z0) -> logZeroError
help(z0, z1) -> ifb(lt(z1, z0), z0, z1)
ifb(true, z0, z1) -> help(half(z0), s(z1))
ifb(false, z0, z1) -> z1
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))

Types:
LT :: 0':s:1':logZeroError -> 0':s:1':logZeroError -> c:c1:c2
0' :: 0':s:1':logZeroError
s :: 0':s:1':logZeroError -> 0':s:1':logZeroError
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
LOGARITHM :: 0':s:1':logZeroError -> c3
c3 :: c4:c5 -> c:c1:c2 -> c3
IFA :: true:false -> 0':s:1':logZeroError -> c4:c5
lt :: 0':s:1':logZeroError -> 0':s:1':logZeroError -> true:false
true :: true:false
c4 :: c6 -> c4:c5
HELP :: 0':s:1':logZeroError -> 0':s:1':logZeroError -> c6
1' :: 0':s:1':logZeroError
false :: true:false
c5 :: c4:c5
c6 :: c7:c8 -> c:c1:c2 -> c6
IFB :: true:false -> 0':s:1':logZeroError -> 0':s:1':logZeroError -> c7:c8
c7 :: c6 -> c9:c10:c11 -> c7:c8
half :: 0':s:1':logZeroError -> 0':s:1':logZeroError
HALF :: 0':s:1':logZeroError -> c9:c10:c11
c8 :: c7:c8
c9 :: c9:c10:c11
c10 :: c9:c10:c11
c11 :: c9:c10:c11 -> c9:c10:c11
logarithm :: 0':s:1':logZeroError -> 0':s:1':logZeroError
ifa :: true:false -> 0':s:1':logZeroError -> 0':s:1':logZeroError
help :: 0':s:1':logZeroError -> 0':s:1':logZeroError -> 0':s:1':logZeroError
logZeroError :: 0':s:1':logZeroError
ifb :: true:false -> 0':s:1':logZeroError -> 0':s:1':logZeroError -> 0':s:1':logZeroError
hole_c:c1:c21_12 :: c:c1:c2
hole_0':s:1':logZeroError2_12 :: 0':s:1':logZeroError
hole_c33_12 :: c3
hole_c4:c54_12 :: c4:c5
hole_true:false5_12 :: true:false
hole_c66_12 :: c6
hole_c7:c87_12 :: c7:c8
hole_c9:c10:c118_12 :: c9:c10:c11
gen_c:c1:c29_12 :: Nat -> c:c1:c2
gen_0':s:1':logZeroError10_12 :: Nat -> 0':s:1':logZeroError
gen_c9:c10:c1111_12 :: Nat -> c9:c10:c11

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

(31) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
LT, lt, HELP, half, HALF, help

They will be analysed ascendingly in the following order:
LT < HELP
lt < HELP
lt < help
half < HELP
HALF < HELP
half < help

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

(32)
Obligation:
Innermost TRS:
Rules:
LT(0', s(z0)) -> c
LT(z0, 0') -> c1
LT(s(z0), s(z1)) -> c2(LT(z0, z1))
LOGARITHM(z0) -> c3(IFA(lt(0', z0), z0), LT(0', z0))
IFA(true, z0) -> c4(HELP(z0, 1'))
IFA(false, z0) -> c5
HELP(z0, z1) -> c6(IFB(lt(z1, z0), z0, z1), LT(z1, z0))
IFB(true, z0, z1) -> c7(HELP(half(z0), s(z1)), HALF(z0))
IFB(false, z0, z1) -> c8
HALF(0') -> c9
HALF(s(0')) -> c10
HALF(s(s(z0))) -> c11(HALF(z0))
lt(0', s(z0)) -> true
lt(z0, 0') -> false
lt(s(z0), s(z1)) -> lt(z0, z1)
logarithm(z0) -> ifa(lt(0', z0), z0)
ifa(true, z0) -> help(z0, 1')
ifa(false, z0) -> logZeroError
help(z0, z1) -> ifb(lt(z1, z0), z0, z1)
ifb(true, z0, z1) -> help(half(z0), s(z1))
ifb(false, z0, z1) -> z1
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))

Types:
LT :: 0':s:1':logZeroError -> 0':s:1':logZeroError -> c:c1:c2
0' :: 0':s:1':logZeroError
s :: 0':s:1':logZeroError -> 0':s:1':logZeroError
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
LOGARITHM :: 0':s:1':logZeroError -> c3
c3 :: c4:c5 -> c:c1:c2 -> c3
IFA :: true:false -> 0':s:1':logZeroError -> c4:c5
lt :: 0':s:1':logZeroError -> 0':s:1':logZeroError -> true:false
true :: true:false
c4 :: c6 -> c4:c5
HELP :: 0':s:1':logZeroError -> 0':s:1':logZeroError -> c6
1' :: 0':s:1':logZeroError
false :: true:false
c5 :: c4:c5
c6 :: c7:c8 -> c:c1:c2 -> c6
IFB :: true:false -> 0':s:1':logZeroError -> 0':s:1':logZeroError -> c7:c8
c7 :: c6 -> c9:c10:c11 -> c7:c8
half :: 0':s:1':logZeroError -> 0':s:1':logZeroError
HALF :: 0':s:1':logZeroError -> c9:c10:c11
c8 :: c7:c8
c9 :: c9:c10:c11
c10 :: c9:c10:c11
c11 :: c9:c10:c11 -> c9:c10:c11
logarithm :: 0':s:1':logZeroError -> 0':s:1':logZeroError
ifa :: true:false -> 0':s:1':logZeroError -> 0':s:1':logZeroError
help :: 0':s:1':logZeroError -> 0':s:1':logZeroError -> 0':s:1':logZeroError
logZeroError :: 0':s:1':logZeroError
ifb :: true:false -> 0':s:1':logZeroError -> 0':s:1':logZeroError -> 0':s:1':logZeroError
hole_c:c1:c21_12 :: c:c1:c2
hole_0':s:1':logZeroError2_12 :: 0':s:1':logZeroError
hole_c33_12 :: c3
hole_c4:c54_12 :: c4:c5
hole_true:false5_12 :: true:false
hole_c66_12 :: c6
hole_c7:c87_12 :: c7:c8
hole_c9:c10:c118_12 :: c9:c10:c11
gen_c:c1:c29_12 :: Nat -> c:c1:c2
gen_0':s:1':logZeroError10_12 :: Nat -> 0':s:1':logZeroError
gen_c9:c10:c1111_12 :: Nat -> c9:c10:c11


Generator Equations:
gen_c:c1:c29_12(0) <=> c
gen_c:c1:c29_12(+(x, 1)) <=> c2(gen_c:c1:c29_12(x))
gen_0':s:1':logZeroError10_12(0) <=> 0'
gen_0':s:1':logZeroError10_12(+(x, 1)) <=> s(gen_0':s:1':logZeroError10_12(x))
gen_c9:c10:c1111_12(0) <=> c9
gen_c9:c10:c1111_12(+(x, 1)) <=> c11(gen_c9:c10:c1111_12(x))


The following defined symbols remain to be analysed:
LT, lt, HELP, half, HALF, help

They will be analysed ascendingly in the following order:
LT < HELP
lt < HELP
lt < help
half < HELP
HALF < HELP
half < help

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

(33) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LT(gen_0':s:1':logZeroError10_12(n13_12), gen_0':s:1':logZeroError10_12(+(1, n13_12))) -> gen_c:c1:c29_12(n13_12), rt in Omega(1 + n13_12)

Induction Base:
LT(gen_0':s:1':logZeroError10_12(0), gen_0':s:1':logZeroError10_12(+(1, 0))) ->_R^Omega(1)
c

Induction Step:
LT(gen_0':s:1':logZeroError10_12(+(n13_12, 1)), gen_0':s:1':logZeroError10_12(+(1, +(n13_12, 1)))) ->_R^Omega(1)
c2(LT(gen_0':s:1':logZeroError10_12(n13_12), gen_0':s:1':logZeroError10_12(+(1, n13_12)))) ->_IH
c2(gen_c:c1:c29_12(c14_12))

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

(34)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
LT(0', s(z0)) -> c
LT(z0, 0') -> c1
LT(s(z0), s(z1)) -> c2(LT(z0, z1))
LOGARITHM(z0) -> c3(IFA(lt(0', z0), z0), LT(0', z0))
IFA(true, z0) -> c4(HELP(z0, 1'))
IFA(false, z0) -> c5
HELP(z0, z1) -> c6(IFB(lt(z1, z0), z0, z1), LT(z1, z0))
IFB(true, z0, z1) -> c7(HELP(half(z0), s(z1)), HALF(z0))
IFB(false, z0, z1) -> c8
HALF(0') -> c9
HALF(s(0')) -> c10
HALF(s(s(z0))) -> c11(HALF(z0))
lt(0', s(z0)) -> true
lt(z0, 0') -> false
lt(s(z0), s(z1)) -> lt(z0, z1)
logarithm(z0) -> ifa(lt(0', z0), z0)
ifa(true, z0) -> help(z0, 1')
ifa(false, z0) -> logZeroError
help(z0, z1) -> ifb(lt(z1, z0), z0, z1)
ifb(true, z0, z1) -> help(half(z0), s(z1))
ifb(false, z0, z1) -> z1
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))

Types:
LT :: 0':s:1':logZeroError -> 0':s:1':logZeroError -> c:c1:c2
0' :: 0':s:1':logZeroError
s :: 0':s:1':logZeroError -> 0':s:1':logZeroError
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
LOGARITHM :: 0':s:1':logZeroError -> c3
c3 :: c4:c5 -> c:c1:c2 -> c3
IFA :: true:false -> 0':s:1':logZeroError -> c4:c5
lt :: 0':s:1':logZeroError -> 0':s:1':logZeroError -> true:false
true :: true:false
c4 :: c6 -> c4:c5
HELP :: 0':s:1':logZeroError -> 0':s:1':logZeroError -> c6
1' :: 0':s:1':logZeroError
false :: true:false
c5 :: c4:c5
c6 :: c7:c8 -> c:c1:c2 -> c6
IFB :: true:false -> 0':s:1':logZeroError -> 0':s:1':logZeroError -> c7:c8
c7 :: c6 -> c9:c10:c11 -> c7:c8
half :: 0':s:1':logZeroError -> 0':s:1':logZeroError
HALF :: 0':s:1':logZeroError -> c9:c10:c11
c8 :: c7:c8
c9 :: c9:c10:c11
c10 :: c9:c10:c11
c11 :: c9:c10:c11 -> c9:c10:c11
logarithm :: 0':s:1':logZeroError -> 0':s:1':logZeroError
ifa :: true:false -> 0':s:1':logZeroError -> 0':s:1':logZeroError
help :: 0':s:1':logZeroError -> 0':s:1':logZeroError -> 0':s:1':logZeroError
logZeroError :: 0':s:1':logZeroError
ifb :: true:false -> 0':s:1':logZeroError -> 0':s:1':logZeroError -> 0':s:1':logZeroError
hole_c:c1:c21_12 :: c:c1:c2
hole_0':s:1':logZeroError2_12 :: 0':s:1':logZeroError
hole_c33_12 :: c3
hole_c4:c54_12 :: c4:c5
hole_true:false5_12 :: true:false
hole_c66_12 :: c6
hole_c7:c87_12 :: c7:c8
hole_c9:c10:c118_12 :: c9:c10:c11
gen_c:c1:c29_12 :: Nat -> c:c1:c2
gen_0':s:1':logZeroError10_12 :: Nat -> 0':s:1':logZeroError
gen_c9:c10:c1111_12 :: Nat -> c9:c10:c11


Generator Equations:
gen_c:c1:c29_12(0) <=> c
gen_c:c1:c29_12(+(x, 1)) <=> c2(gen_c:c1:c29_12(x))
gen_0':s:1':logZeroError10_12(0) <=> 0'
gen_0':s:1':logZeroError10_12(+(x, 1)) <=> s(gen_0':s:1':logZeroError10_12(x))
gen_c9:c10:c1111_12(0) <=> c9
gen_c9:c10:c1111_12(+(x, 1)) <=> c11(gen_c9:c10:c1111_12(x))


The following defined symbols remain to be analysed:
LT, lt, HELP, half, HALF, help

They will be analysed ascendingly in the following order:
LT < HELP
lt < HELP
lt < help
half < HELP
HALF < HELP
half < help

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

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

(37)
BOUNDS(n^1, INF)

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

(38)
Obligation:
Innermost TRS:
Rules:
LT(0', s(z0)) -> c
LT(z0, 0') -> c1
LT(s(z0), s(z1)) -> c2(LT(z0, z1))
LOGARITHM(z0) -> c3(IFA(lt(0', z0), z0), LT(0', z0))
IFA(true, z0) -> c4(HELP(z0, 1'))
IFA(false, z0) -> c5
HELP(z0, z1) -> c6(IFB(lt(z1, z0), z0, z1), LT(z1, z0))
IFB(true, z0, z1) -> c7(HELP(half(z0), s(z1)), HALF(z0))
IFB(false, z0, z1) -> c8
HALF(0') -> c9
HALF(s(0')) -> c10
HALF(s(s(z0))) -> c11(HALF(z0))
lt(0', s(z0)) -> true
lt(z0, 0') -> false
lt(s(z0), s(z1)) -> lt(z0, z1)
logarithm(z0) -> ifa(lt(0', z0), z0)
ifa(true, z0) -> help(z0, 1')
ifa(false, z0) -> logZeroError
help(z0, z1) -> ifb(lt(z1, z0), z0, z1)
ifb(true, z0, z1) -> help(half(z0), s(z1))
ifb(false, z0, z1) -> z1
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))

Types:
LT :: 0':s:1':logZeroError -> 0':s:1':logZeroError -> c:c1:c2
0' :: 0':s:1':logZeroError
s :: 0':s:1':logZeroError -> 0':s:1':logZeroError
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
LOGARITHM :: 0':s:1':logZeroError -> c3
c3 :: c4:c5 -> c:c1:c2 -> c3
IFA :: true:false -> 0':s:1':logZeroError -> c4:c5
lt :: 0':s:1':logZeroError -> 0':s:1':logZeroError -> true:false
true :: true:false
c4 :: c6 -> c4:c5
HELP :: 0':s:1':logZeroError -> 0':s:1':logZeroError -> c6
1' :: 0':s:1':logZeroError
false :: true:false
c5 :: c4:c5
c6 :: c7:c8 -> c:c1:c2 -> c6
IFB :: true:false -> 0':s:1':logZeroError -> 0':s:1':logZeroError -> c7:c8
c7 :: c6 -> c9:c10:c11 -> c7:c8
half :: 0':s:1':logZeroError -> 0':s:1':logZeroError
HALF :: 0':s:1':logZeroError -> c9:c10:c11
c8 :: c7:c8
c9 :: c9:c10:c11
c10 :: c9:c10:c11
c11 :: c9:c10:c11 -> c9:c10:c11
logarithm :: 0':s:1':logZeroError -> 0':s:1':logZeroError
ifa :: true:false -> 0':s:1':logZeroError -> 0':s:1':logZeroError
help :: 0':s:1':logZeroError -> 0':s:1':logZeroError -> 0':s:1':logZeroError
logZeroError :: 0':s:1':logZeroError
ifb :: true:false -> 0':s:1':logZeroError -> 0':s:1':logZeroError -> 0':s:1':logZeroError
hole_c:c1:c21_12 :: c:c1:c2
hole_0':s:1':logZeroError2_12 :: 0':s:1':logZeroError
hole_c33_12 :: c3
hole_c4:c54_12 :: c4:c5
hole_true:false5_12 :: true:false
hole_c66_12 :: c6
hole_c7:c87_12 :: c7:c8
hole_c9:c10:c118_12 :: c9:c10:c11
gen_c:c1:c29_12 :: Nat -> c:c1:c2
gen_0':s:1':logZeroError10_12 :: Nat -> 0':s:1':logZeroError
gen_c9:c10:c1111_12 :: Nat -> c9:c10:c11


Lemmas:
LT(gen_0':s:1':logZeroError10_12(n13_12), gen_0':s:1':logZeroError10_12(+(1, n13_12))) -> gen_c:c1:c29_12(n13_12), rt in Omega(1 + n13_12)


Generator Equations:
gen_c:c1:c29_12(0) <=> c
gen_c:c1:c29_12(+(x, 1)) <=> c2(gen_c:c1:c29_12(x))
gen_0':s:1':logZeroError10_12(0) <=> 0'
gen_0':s:1':logZeroError10_12(+(x, 1)) <=> s(gen_0':s:1':logZeroError10_12(x))
gen_c9:c10:c1111_12(0) <=> c9
gen_c9:c10:c1111_12(+(x, 1)) <=> c11(gen_c9:c10:c1111_12(x))


The following defined symbols remain to be analysed:
lt, HELP, half, HALF, help

They will be analysed ascendingly in the following order:
lt < HELP
lt < help
half < HELP
HALF < HELP
half < help

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

(39) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
lt(gen_0':s:1':logZeroError10_12(n628_12), gen_0':s:1':logZeroError10_12(+(1, n628_12))) -> true, rt in Omega(0)

Induction Base:
lt(gen_0':s:1':logZeroError10_12(0), gen_0':s:1':logZeroError10_12(+(1, 0))) ->_R^Omega(0)
true

Induction Step:
lt(gen_0':s:1':logZeroError10_12(+(n628_12, 1)), gen_0':s:1':logZeroError10_12(+(1, +(n628_12, 1)))) ->_R^Omega(0)
lt(gen_0':s:1':logZeroError10_12(n628_12), gen_0':s:1':logZeroError10_12(+(1, n628_12))) ->_IH
true

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:
LT(0', s(z0)) -> c
LT(z0, 0') -> c1
LT(s(z0), s(z1)) -> c2(LT(z0, z1))
LOGARITHM(z0) -> c3(IFA(lt(0', z0), z0), LT(0', z0))
IFA(true, z0) -> c4(HELP(z0, 1'))
IFA(false, z0) -> c5
HELP(z0, z1) -> c6(IFB(lt(z1, z0), z0, z1), LT(z1, z0))
IFB(true, z0, z1) -> c7(HELP(half(z0), s(z1)), HALF(z0))
IFB(false, z0, z1) -> c8
HALF(0') -> c9
HALF(s(0')) -> c10
HALF(s(s(z0))) -> c11(HALF(z0))
lt(0', s(z0)) -> true
lt(z0, 0') -> false
lt(s(z0), s(z1)) -> lt(z0, z1)
logarithm(z0) -> ifa(lt(0', z0), z0)
ifa(true, z0) -> help(z0, 1')
ifa(false, z0) -> logZeroError
help(z0, z1) -> ifb(lt(z1, z0), z0, z1)
ifb(true, z0, z1) -> help(half(z0), s(z1))
ifb(false, z0, z1) -> z1
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))

Types:
LT :: 0':s:1':logZeroError -> 0':s:1':logZeroError -> c:c1:c2
0' :: 0':s:1':logZeroError
s :: 0':s:1':logZeroError -> 0':s:1':logZeroError
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
LOGARITHM :: 0':s:1':logZeroError -> c3
c3 :: c4:c5 -> c:c1:c2 -> c3
IFA :: true:false -> 0':s:1':logZeroError -> c4:c5
lt :: 0':s:1':logZeroError -> 0':s:1':logZeroError -> true:false
true :: true:false
c4 :: c6 -> c4:c5
HELP :: 0':s:1':logZeroError -> 0':s:1':logZeroError -> c6
1' :: 0':s:1':logZeroError
false :: true:false
c5 :: c4:c5
c6 :: c7:c8 -> c:c1:c2 -> c6
IFB :: true:false -> 0':s:1':logZeroError -> 0':s:1':logZeroError -> c7:c8
c7 :: c6 -> c9:c10:c11 -> c7:c8
half :: 0':s:1':logZeroError -> 0':s:1':logZeroError
HALF :: 0':s:1':logZeroError -> c9:c10:c11
c8 :: c7:c8
c9 :: c9:c10:c11
c10 :: c9:c10:c11
c11 :: c9:c10:c11 -> c9:c10:c11
logarithm :: 0':s:1':logZeroError -> 0':s:1':logZeroError
ifa :: true:false -> 0':s:1':logZeroError -> 0':s:1':logZeroError
help :: 0':s:1':logZeroError -> 0':s:1':logZeroError -> 0':s:1':logZeroError
logZeroError :: 0':s:1':logZeroError
ifb :: true:false -> 0':s:1':logZeroError -> 0':s:1':logZeroError -> 0':s:1':logZeroError
hole_c:c1:c21_12 :: c:c1:c2
hole_0':s:1':logZeroError2_12 :: 0':s:1':logZeroError
hole_c33_12 :: c3
hole_c4:c54_12 :: c4:c5
hole_true:false5_12 :: true:false
hole_c66_12 :: c6
hole_c7:c87_12 :: c7:c8
hole_c9:c10:c118_12 :: c9:c10:c11
gen_c:c1:c29_12 :: Nat -> c:c1:c2
gen_0':s:1':logZeroError10_12 :: Nat -> 0':s:1':logZeroError
gen_c9:c10:c1111_12 :: Nat -> c9:c10:c11


Lemmas:
LT(gen_0':s:1':logZeroError10_12(n13_12), gen_0':s:1':logZeroError10_12(+(1, n13_12))) -> gen_c:c1:c29_12(n13_12), rt in Omega(1 + n13_12)
lt(gen_0':s:1':logZeroError10_12(n628_12), gen_0':s:1':logZeroError10_12(+(1, n628_12))) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c29_12(0) <=> c
gen_c:c1:c29_12(+(x, 1)) <=> c2(gen_c:c1:c29_12(x))
gen_0':s:1':logZeroError10_12(0) <=> 0'
gen_0':s:1':logZeroError10_12(+(x, 1)) <=> s(gen_0':s:1':logZeroError10_12(x))
gen_c9:c10:c1111_12(0) <=> c9
gen_c9:c10:c1111_12(+(x, 1)) <=> c11(gen_c9:c10:c1111_12(x))


The following defined symbols remain to be analysed:
half, HELP, HALF, help

They will be analysed ascendingly in the following order:
half < HELP
HALF < HELP
half < help

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

(41) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
half(gen_0':s:1':logZeroError10_12(*(2, n1024_12))) -> gen_0':s:1':logZeroError10_12(n1024_12), rt in Omega(0)

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

Induction Step:
half(gen_0':s:1':logZeroError10_12(*(2, +(n1024_12, 1)))) ->_R^Omega(0)
s(half(gen_0':s:1':logZeroError10_12(*(2, n1024_12)))) ->_IH
s(gen_0':s:1':logZeroError10_12(c1025_12))

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:
LT(0', s(z0)) -> c
LT(z0, 0') -> c1
LT(s(z0), s(z1)) -> c2(LT(z0, z1))
LOGARITHM(z0) -> c3(IFA(lt(0', z0), z0), LT(0', z0))
IFA(true, z0) -> c4(HELP(z0, 1'))
IFA(false, z0) -> c5
HELP(z0, z1) -> c6(IFB(lt(z1, z0), z0, z1), LT(z1, z0))
IFB(true, z0, z1) -> c7(HELP(half(z0), s(z1)), HALF(z0))
IFB(false, z0, z1) -> c8
HALF(0') -> c9
HALF(s(0')) -> c10
HALF(s(s(z0))) -> c11(HALF(z0))
lt(0', s(z0)) -> true
lt(z0, 0') -> false
lt(s(z0), s(z1)) -> lt(z0, z1)
logarithm(z0) -> ifa(lt(0', z0), z0)
ifa(true, z0) -> help(z0, 1')
ifa(false, z0) -> logZeroError
help(z0, z1) -> ifb(lt(z1, z0), z0, z1)
ifb(true, z0, z1) -> help(half(z0), s(z1))
ifb(false, z0, z1) -> z1
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))

Types:
LT :: 0':s:1':logZeroError -> 0':s:1':logZeroError -> c:c1:c2
0' :: 0':s:1':logZeroError
s :: 0':s:1':logZeroError -> 0':s:1':logZeroError
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
LOGARITHM :: 0':s:1':logZeroError -> c3
c3 :: c4:c5 -> c:c1:c2 -> c3
IFA :: true:false -> 0':s:1':logZeroError -> c4:c5
lt :: 0':s:1':logZeroError -> 0':s:1':logZeroError -> true:false
true :: true:false
c4 :: c6 -> c4:c5
HELP :: 0':s:1':logZeroError -> 0':s:1':logZeroError -> c6
1' :: 0':s:1':logZeroError
false :: true:false
c5 :: c4:c5
c6 :: c7:c8 -> c:c1:c2 -> c6
IFB :: true:false -> 0':s:1':logZeroError -> 0':s:1':logZeroError -> c7:c8
c7 :: c6 -> c9:c10:c11 -> c7:c8
half :: 0':s:1':logZeroError -> 0':s:1':logZeroError
HALF :: 0':s:1':logZeroError -> c9:c10:c11
c8 :: c7:c8
c9 :: c9:c10:c11
c10 :: c9:c10:c11
c11 :: c9:c10:c11 -> c9:c10:c11
logarithm :: 0':s:1':logZeroError -> 0':s:1':logZeroError
ifa :: true:false -> 0':s:1':logZeroError -> 0':s:1':logZeroError
help :: 0':s:1':logZeroError -> 0':s:1':logZeroError -> 0':s:1':logZeroError
logZeroError :: 0':s:1':logZeroError
ifb :: true:false -> 0':s:1':logZeroError -> 0':s:1':logZeroError -> 0':s:1':logZeroError
hole_c:c1:c21_12 :: c:c1:c2
hole_0':s:1':logZeroError2_12 :: 0':s:1':logZeroError
hole_c33_12 :: c3
hole_c4:c54_12 :: c4:c5
hole_true:false5_12 :: true:false
hole_c66_12 :: c6
hole_c7:c87_12 :: c7:c8
hole_c9:c10:c118_12 :: c9:c10:c11
gen_c:c1:c29_12 :: Nat -> c:c1:c2
gen_0':s:1':logZeroError10_12 :: Nat -> 0':s:1':logZeroError
gen_c9:c10:c1111_12 :: Nat -> c9:c10:c11


Lemmas:
LT(gen_0':s:1':logZeroError10_12(n13_12), gen_0':s:1':logZeroError10_12(+(1, n13_12))) -> gen_c:c1:c29_12(n13_12), rt in Omega(1 + n13_12)
lt(gen_0':s:1':logZeroError10_12(n628_12), gen_0':s:1':logZeroError10_12(+(1, n628_12))) -> true, rt in Omega(0)
half(gen_0':s:1':logZeroError10_12(*(2, n1024_12))) -> gen_0':s:1':logZeroError10_12(n1024_12), rt in Omega(0)


Generator Equations:
gen_c:c1:c29_12(0) <=> c
gen_c:c1:c29_12(+(x, 1)) <=> c2(gen_c:c1:c29_12(x))
gen_0':s:1':logZeroError10_12(0) <=> 0'
gen_0':s:1':logZeroError10_12(+(x, 1)) <=> s(gen_0':s:1':logZeroError10_12(x))
gen_c9:c10:c1111_12(0) <=> c9
gen_c9:c10:c1111_12(+(x, 1)) <=> c11(gen_c9:c10:c1111_12(x))


The following defined symbols remain to be analysed:
HALF, HELP, help

They will be analysed ascendingly in the following order:
HALF < HELP

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

(43) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
HALF(gen_0':s:1':logZeroError10_12(*(2, n1484_12))) -> gen_c9:c10:c1111_12(n1484_12), rt in Omega(1 + n1484_12)

Induction Base:
HALF(gen_0':s:1':logZeroError10_12(*(2, 0))) ->_R^Omega(1)
c9

Induction Step:
HALF(gen_0':s:1':logZeroError10_12(*(2, +(n1484_12, 1)))) ->_R^Omega(1)
c11(HALF(gen_0':s:1':logZeroError10_12(*(2, n1484_12)))) ->_IH
c11(gen_c9:c10:c1111_12(c1485_12))

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

(44)
Obligation:
Innermost TRS:
Rules:
LT(0', s(z0)) -> c
LT(z0, 0') -> c1
LT(s(z0), s(z1)) -> c2(LT(z0, z1))
LOGARITHM(z0) -> c3(IFA(lt(0', z0), z0), LT(0', z0))
IFA(true, z0) -> c4(HELP(z0, 1'))
IFA(false, z0) -> c5
HELP(z0, z1) -> c6(IFB(lt(z1, z0), z0, z1), LT(z1, z0))
IFB(true, z0, z1) -> c7(HELP(half(z0), s(z1)), HALF(z0))
IFB(false, z0, z1) -> c8
HALF(0') -> c9
HALF(s(0')) -> c10
HALF(s(s(z0))) -> c11(HALF(z0))
lt(0', s(z0)) -> true
lt(z0, 0') -> false
lt(s(z0), s(z1)) -> lt(z0, z1)
logarithm(z0) -> ifa(lt(0', z0), z0)
ifa(true, z0) -> help(z0, 1')
ifa(false, z0) -> logZeroError
help(z0, z1) -> ifb(lt(z1, z0), z0, z1)
ifb(true, z0, z1) -> help(half(z0), s(z1))
ifb(false, z0, z1) -> z1
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))

Types:
LT :: 0':s:1':logZeroError -> 0':s:1':logZeroError -> c:c1:c2
0' :: 0':s:1':logZeroError
s :: 0':s:1':logZeroError -> 0':s:1':logZeroError
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
LOGARITHM :: 0':s:1':logZeroError -> c3
c3 :: c4:c5 -> c:c1:c2 -> c3
IFA :: true:false -> 0':s:1':logZeroError -> c4:c5
lt :: 0':s:1':logZeroError -> 0':s:1':logZeroError -> true:false
true :: true:false
c4 :: c6 -> c4:c5
HELP :: 0':s:1':logZeroError -> 0':s:1':logZeroError -> c6
1' :: 0':s:1':logZeroError
false :: true:false
c5 :: c4:c5
c6 :: c7:c8 -> c:c1:c2 -> c6
IFB :: true:false -> 0':s:1':logZeroError -> 0':s:1':logZeroError -> c7:c8
c7 :: c6 -> c9:c10:c11 -> c7:c8
half :: 0':s:1':logZeroError -> 0':s:1':logZeroError
HALF :: 0':s:1':logZeroError -> c9:c10:c11
c8 :: c7:c8
c9 :: c9:c10:c11
c10 :: c9:c10:c11
c11 :: c9:c10:c11 -> c9:c10:c11
logarithm :: 0':s:1':logZeroError -> 0':s:1':logZeroError
ifa :: true:false -> 0':s:1':logZeroError -> 0':s:1':logZeroError
help :: 0':s:1':logZeroError -> 0':s:1':logZeroError -> 0':s:1':logZeroError
logZeroError :: 0':s:1':logZeroError
ifb :: true:false -> 0':s:1':logZeroError -> 0':s:1':logZeroError -> 0':s:1':logZeroError
hole_c:c1:c21_12 :: c:c1:c2
hole_0':s:1':logZeroError2_12 :: 0':s:1':logZeroError
hole_c33_12 :: c3
hole_c4:c54_12 :: c4:c5
hole_true:false5_12 :: true:false
hole_c66_12 :: c6
hole_c7:c87_12 :: c7:c8
hole_c9:c10:c118_12 :: c9:c10:c11
gen_c:c1:c29_12 :: Nat -> c:c1:c2
gen_0':s:1':logZeroError10_12 :: Nat -> 0':s:1':logZeroError
gen_c9:c10:c1111_12 :: Nat -> c9:c10:c11


Lemmas:
LT(gen_0':s:1':logZeroError10_12(n13_12), gen_0':s:1':logZeroError10_12(+(1, n13_12))) -> gen_c:c1:c29_12(n13_12), rt in Omega(1 + n13_12)
lt(gen_0':s:1':logZeroError10_12(n628_12), gen_0':s:1':logZeroError10_12(+(1, n628_12))) -> true, rt in Omega(0)
half(gen_0':s:1':logZeroError10_12(*(2, n1024_12))) -> gen_0':s:1':logZeroError10_12(n1024_12), rt in Omega(0)
HALF(gen_0':s:1':logZeroError10_12(*(2, n1484_12))) -> gen_c9:c10:c1111_12(n1484_12), rt in Omega(1 + n1484_12)


Generator Equations:
gen_c:c1:c29_12(0) <=> c
gen_c:c1:c29_12(+(x, 1)) <=> c2(gen_c:c1:c29_12(x))
gen_0':s:1':logZeroError10_12(0) <=> 0'
gen_0':s:1':logZeroError10_12(+(x, 1)) <=> s(gen_0':s:1':logZeroError10_12(x))
gen_c9:c10:c1111_12(0) <=> c9
gen_c9:c10:c1111_12(+(x, 1)) <=> c11(gen_c9:c10:c1111_12(x))


The following defined symbols remain to be analysed:
HELP, help