WORST_CASE(Omega(n^1),?)
proof of /export/starexec/sandbox2/benchmark/theBenchmark.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished


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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 4067 ms]
(2) CpxRelTRS
(3) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms]
(4) TRS for Loop Detection
(5) DecreasingLoopProof [LOWER BOUND(ID), 6 ms]
(6) BEST
    (7) proven lower bound
        (8) LowerBoundPropagationProof [FINISHED, 0 ms]
        (9) BOUNDS(n^1, INF)
    (10) TRS for Loop Detection


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

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

   TIMES(z0, z1) -> c1(SUM(generate(z0, z1)), GENERATE(z0, z1))
   GENERATE(z0, z1) -> c2(GEN(z0, z1, 0))
   GEN(z0, z1, z2) -> c3(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0))
   IF(true, z0, z1, z2) -> c4
   IF(false, z0, z1, z2) -> c5(GEN(z0, z1, s(z2)))
   SUM(z0) -> c6(SUM2(z0, 0))
   SUM2(z0, z1) -> c7(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISNIL(z0))
   SUM2(z0, z1) -> c8(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISZERO(head(z0)), HEAD(z0))
   IFSUM(true, z0, z1, z2) -> c9
   IFSUM(false, z0, z1, z2) -> c10(IFSUM2(z0, z1, z2))
   IFSUM2(true, z0, z1) -> c11(SUM2(tail(z0), z1), TAIL(z0))
   IFSUM2(false, z0, z1) -> c12(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), P(head(z0)), HEAD(z0))
   IFSUM2(false, z0, z1) -> c13(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), TAIL(z0))
   ISNIL(nil) -> c14
   ISNIL(cons(z0, z1)) -> c15
   TAIL(nil) -> c16
   TAIL(cons(z0, z1)) -> c17
   HEAD(cons(z0, z1)) -> c18
   HEAD(nil) -> c19
   ISZERO(0) -> c20
   ISZERO(s(0)) -> c21
   ISZERO(s(s(z0))) -> c22(ISZERO(s(z0)))
   P(0) -> c23
   P(s(0)) -> c24
   P(s(s(z0))) -> c25(P(s(z0)))
   GE(z0, 0) -> c26
   GE(0, s(z0)) -> c27
   GE(s(z0), s(z1)) -> c28(GE(z0, z1))
   A -> c29
   A -> c30

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

   times(z0, z1) -> sum(generate(z0, z1))
   generate(z0, z1) -> gen(z0, z1, 0)
   gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2)
   if(true, z0, z1, z2) -> nil
   if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2)))
   sum(z0) -> sum2(z0, 0)
   sum2(z0, z1) -> ifsum(isNil(z0), isZero(head(z0)), z0, z1)
   ifsum(true, z0, z1, z2) -> z2
   ifsum(false, z0, z1, z2) -> ifsum2(z0, z1, z2)
   ifsum2(true, z0, z1) -> sum2(tail(z0), z1)
   ifsum2(false, z0, z1) -> sum2(cons(p(head(z0)), tail(z0)), s(z1))
   isNil(nil) -> true
   isNil(cons(z0, z1)) -> false
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   head(cons(z0, z1)) -> z0
   head(nil) -> error
   isZero(0) -> true
   isZero(s(0)) -> false
   isZero(s(s(z0))) -> isZero(s(z0))
   p(0) -> s(s(0))
   p(s(0)) -> 0
   p(s(s(z0))) -> s(p(s(z0)))
   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   a -> c
   a -> d

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

(1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID))
proved innermost termination of relative rules
----------------------------------------

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

   TIMES(z0, z1) -> c1(SUM(generate(z0, z1)), GENERATE(z0, z1))
   GENERATE(z0, z1) -> c2(GEN(z0, z1, 0))
   GEN(z0, z1, z2) -> c3(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0))
   IF(true, z0, z1, z2) -> c4
   IF(false, z0, z1, z2) -> c5(GEN(z0, z1, s(z2)))
   SUM(z0) -> c6(SUM2(z0, 0))
   SUM2(z0, z1) -> c7(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISNIL(z0))
   SUM2(z0, z1) -> c8(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISZERO(head(z0)), HEAD(z0))
   IFSUM(true, z0, z1, z2) -> c9
   IFSUM(false, z0, z1, z2) -> c10(IFSUM2(z0, z1, z2))
   IFSUM2(true, z0, z1) -> c11(SUM2(tail(z0), z1), TAIL(z0))
   IFSUM2(false, z0, z1) -> c12(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), P(head(z0)), HEAD(z0))
   IFSUM2(false, z0, z1) -> c13(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), TAIL(z0))
   ISNIL(nil) -> c14
   ISNIL(cons(z0, z1)) -> c15
   TAIL(nil) -> c16
   TAIL(cons(z0, z1)) -> c17
   HEAD(cons(z0, z1)) -> c18
   HEAD(nil) -> c19
   ISZERO(0) -> c20
   ISZERO(s(0)) -> c21
   ISZERO(s(s(z0))) -> c22(ISZERO(s(z0)))
   P(0) -> c23
   P(s(0)) -> c24
   P(s(s(z0))) -> c25(P(s(z0)))
   GE(z0, 0) -> c26
   GE(0, s(z0)) -> c27
   GE(s(z0), s(z1)) -> c28(GE(z0, z1))
   A -> c29
   A -> c30

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

   times(z0, z1) -> sum(generate(z0, z1))
   generate(z0, z1) -> gen(z0, z1, 0)
   gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2)
   if(true, z0, z1, z2) -> nil
   if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2)))
   sum(z0) -> sum2(z0, 0)
   sum2(z0, z1) -> ifsum(isNil(z0), isZero(head(z0)), z0, z1)
   ifsum(true, z0, z1, z2) -> z2
   ifsum(false, z0, z1, z2) -> ifsum2(z0, z1, z2)
   ifsum2(true, z0, z1) -> sum2(tail(z0), z1)
   ifsum2(false, z0, z1) -> sum2(cons(p(head(z0)), tail(z0)), s(z1))
   isNil(nil) -> true
   isNil(cons(z0, z1)) -> false
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   head(cons(z0, z1)) -> z0
   head(nil) -> error
   isZero(0) -> true
   isZero(s(0)) -> false
   isZero(s(s(z0))) -> isZero(s(z0))
   p(0) -> s(s(0))
   p(s(0)) -> 0
   p(s(s(z0))) -> s(p(s(z0)))
   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   a -> c
   a -> d

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

(3) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID))
Transformed a relative TRS into a decreasing-loop problem.
----------------------------------------

(4)
Obligation:
Analyzing the following TRS for decreasing loops:

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:

   TIMES(z0, z1) -> c1(SUM(generate(z0, z1)), GENERATE(z0, z1))
   GENERATE(z0, z1) -> c2(GEN(z0, z1, 0))
   GEN(z0, z1, z2) -> c3(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0))
   IF(true, z0, z1, z2) -> c4
   IF(false, z0, z1, z2) -> c5(GEN(z0, z1, s(z2)))
   SUM(z0) -> c6(SUM2(z0, 0))
   SUM2(z0, z1) -> c7(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISNIL(z0))
   SUM2(z0, z1) -> c8(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISZERO(head(z0)), HEAD(z0))
   IFSUM(true, z0, z1, z2) -> c9
   IFSUM(false, z0, z1, z2) -> c10(IFSUM2(z0, z1, z2))
   IFSUM2(true, z0, z1) -> c11(SUM2(tail(z0), z1), TAIL(z0))
   IFSUM2(false, z0, z1) -> c12(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), P(head(z0)), HEAD(z0))
   IFSUM2(false, z0, z1) -> c13(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), TAIL(z0))
   ISNIL(nil) -> c14
   ISNIL(cons(z0, z1)) -> c15
   TAIL(nil) -> c16
   TAIL(cons(z0, z1)) -> c17
   HEAD(cons(z0, z1)) -> c18
   HEAD(nil) -> c19
   ISZERO(0) -> c20
   ISZERO(s(0)) -> c21
   ISZERO(s(s(z0))) -> c22(ISZERO(s(z0)))
   P(0) -> c23
   P(s(0)) -> c24
   P(s(s(z0))) -> c25(P(s(z0)))
   GE(z0, 0) -> c26
   GE(0, s(z0)) -> c27
   GE(s(z0), s(z1)) -> c28(GE(z0, z1))
   A -> c29
   A -> c30

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

   times(z0, z1) -> sum(generate(z0, z1))
   generate(z0, z1) -> gen(z0, z1, 0)
   gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2)
   if(true, z0, z1, z2) -> nil
   if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2)))
   sum(z0) -> sum2(z0, 0)
   sum2(z0, z1) -> ifsum(isNil(z0), isZero(head(z0)), z0, z1)
   ifsum(true, z0, z1, z2) -> z2
   ifsum(false, z0, z1, z2) -> ifsum2(z0, z1, z2)
   ifsum2(true, z0, z1) -> sum2(tail(z0), z1)
   ifsum2(false, z0, z1) -> sum2(cons(p(head(z0)), tail(z0)), s(z1))
   isNil(nil) -> true
   isNil(cons(z0, z1)) -> false
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   head(cons(z0, z1)) -> z0
   head(nil) -> error
   isZero(0) -> true
   isZero(s(0)) -> false
   isZero(s(s(z0))) -> isZero(s(z0))
   p(0) -> s(s(0))
   p(s(0)) -> 0
   p(s(s(z0))) -> s(p(s(z0)))
   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   a -> c
   a -> d

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

(5) DecreasingLoopProof (LOWER BOUND(ID))
The following loop(s) give(s) rise to the lower bound Omega(n^1):

The rewrite sequence

ISZERO(s(s(z0))) ->^+ c22(ISZERO(s(z0)))

gives rise to a decreasing loop by considering the right hand sides subterm at position [0].

The pumping substitution is [z0 / s(z0)].

The result substitution is [ ].




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

(6)
Complex Obligation (BEST)

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

(7)
Obligation:
Proved the lower bound n^1 for the following 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:

   TIMES(z0, z1) -> c1(SUM(generate(z0, z1)), GENERATE(z0, z1))
   GENERATE(z0, z1) -> c2(GEN(z0, z1, 0))
   GEN(z0, z1, z2) -> c3(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0))
   IF(true, z0, z1, z2) -> c4
   IF(false, z0, z1, z2) -> c5(GEN(z0, z1, s(z2)))
   SUM(z0) -> c6(SUM2(z0, 0))
   SUM2(z0, z1) -> c7(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISNIL(z0))
   SUM2(z0, z1) -> c8(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISZERO(head(z0)), HEAD(z0))
   IFSUM(true, z0, z1, z2) -> c9
   IFSUM(false, z0, z1, z2) -> c10(IFSUM2(z0, z1, z2))
   IFSUM2(true, z0, z1) -> c11(SUM2(tail(z0), z1), TAIL(z0))
   IFSUM2(false, z0, z1) -> c12(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), P(head(z0)), HEAD(z0))
   IFSUM2(false, z0, z1) -> c13(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), TAIL(z0))
   ISNIL(nil) -> c14
   ISNIL(cons(z0, z1)) -> c15
   TAIL(nil) -> c16
   TAIL(cons(z0, z1)) -> c17
   HEAD(cons(z0, z1)) -> c18
   HEAD(nil) -> c19
   ISZERO(0) -> c20
   ISZERO(s(0)) -> c21
   ISZERO(s(s(z0))) -> c22(ISZERO(s(z0)))
   P(0) -> c23
   P(s(0)) -> c24
   P(s(s(z0))) -> c25(P(s(z0)))
   GE(z0, 0) -> c26
   GE(0, s(z0)) -> c27
   GE(s(z0), s(z1)) -> c28(GE(z0, z1))
   A -> c29
   A -> c30

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

   times(z0, z1) -> sum(generate(z0, z1))
   generate(z0, z1) -> gen(z0, z1, 0)
   gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2)
   if(true, z0, z1, z2) -> nil
   if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2)))
   sum(z0) -> sum2(z0, 0)
   sum2(z0, z1) -> ifsum(isNil(z0), isZero(head(z0)), z0, z1)
   ifsum(true, z0, z1, z2) -> z2
   ifsum(false, z0, z1, z2) -> ifsum2(z0, z1, z2)
   ifsum2(true, z0, z1) -> sum2(tail(z0), z1)
   ifsum2(false, z0, z1) -> sum2(cons(p(head(z0)), tail(z0)), s(z1))
   isNil(nil) -> true
   isNil(cons(z0, z1)) -> false
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   head(cons(z0, z1)) -> z0
   head(nil) -> error
   isZero(0) -> true
   isZero(s(0)) -> false
   isZero(s(s(z0))) -> isZero(s(z0))
   p(0) -> s(s(0))
   p(s(0)) -> 0
   p(s(s(z0))) -> s(p(s(z0)))
   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   a -> c
   a -> d

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

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

(9)
BOUNDS(n^1, INF)

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

(10)
Obligation:
Analyzing the following TRS for decreasing loops:

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:

   TIMES(z0, z1) -> c1(SUM(generate(z0, z1)), GENERATE(z0, z1))
   GENERATE(z0, z1) -> c2(GEN(z0, z1, 0))
   GEN(z0, z1, z2) -> c3(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0))
   IF(true, z0, z1, z2) -> c4
   IF(false, z0, z1, z2) -> c5(GEN(z0, z1, s(z2)))
   SUM(z0) -> c6(SUM2(z0, 0))
   SUM2(z0, z1) -> c7(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISNIL(z0))
   SUM2(z0, z1) -> c8(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISZERO(head(z0)), HEAD(z0))
   IFSUM(true, z0, z1, z2) -> c9
   IFSUM(false, z0, z1, z2) -> c10(IFSUM2(z0, z1, z2))
   IFSUM2(true, z0, z1) -> c11(SUM2(tail(z0), z1), TAIL(z0))
   IFSUM2(false, z0, z1) -> c12(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), P(head(z0)), HEAD(z0))
   IFSUM2(false, z0, z1) -> c13(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), TAIL(z0))
   ISNIL(nil) -> c14
   ISNIL(cons(z0, z1)) -> c15
   TAIL(nil) -> c16
   TAIL(cons(z0, z1)) -> c17
   HEAD(cons(z0, z1)) -> c18
   HEAD(nil) -> c19
   ISZERO(0) -> c20
   ISZERO(s(0)) -> c21
   ISZERO(s(s(z0))) -> c22(ISZERO(s(z0)))
   P(0) -> c23
   P(s(0)) -> c24
   P(s(s(z0))) -> c25(P(s(z0)))
   GE(z0, 0) -> c26
   GE(0, s(z0)) -> c27
   GE(s(z0), s(z1)) -> c28(GE(z0, z1))
   A -> c29
   A -> c30

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

   times(z0, z1) -> sum(generate(z0, z1))
   generate(z0, z1) -> gen(z0, z1, 0)
   gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2)
   if(true, z0, z1, z2) -> nil
   if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2)))
   sum(z0) -> sum2(z0, 0)
   sum2(z0, z1) -> ifsum(isNil(z0), isZero(head(z0)), z0, z1)
   ifsum(true, z0, z1, z2) -> z2
   ifsum(false, z0, z1, z2) -> ifsum2(z0, z1, z2)
   ifsum2(true, z0, z1) -> sum2(tail(z0), z1)
   ifsum2(false, z0, z1) -> sum2(cons(p(head(z0)), tail(z0)), s(z1))
   isNil(nil) -> true
   isNil(cons(z0, z1)) -> false
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   head(cons(z0, z1)) -> z0
   head(nil) -> error
   isZero(0) -> true
   isZero(s(0)) -> false
   isZero(s(s(z0))) -> isZero(s(z0))
   p(0) -> s(s(0))
   p(s(0)) -> 0
   p(s(s(z0))) -> s(p(s(z0)))
   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   a -> c
   a -> d

Rewrite Strategy: INNERMOST