WORST_CASE(Omega(n^1),?) proof of /export/starexec/sandbox/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), 1538 ms] (2) CpxRelTRS (3) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 3 ms] (4) TRS for Loop Detection (5) DecreasingLoopProof [LOWER BOUND(ID), 0 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: A__PAIRNS -> c A__PAIRNS -> c1 A__ODDNS -> c2(A__INCR(a__pairNs), A__PAIRNS) A__ODDNS -> c3 A__INCR(cons(z0, z1)) -> c4(MARK(z0)) A__INCR(z0) -> c5 A__TAKE(0, z0) -> c6 A__TAKE(s(z0), cons(z1, z2)) -> c7(MARK(z1)) A__TAKE(z0, z1) -> c8 A__ZIP(nil, z0) -> c9 A__ZIP(z0, nil) -> c10 A__ZIP(cons(z0, z1), cons(z2, z3)) -> c11(MARK(z0)) A__ZIP(cons(z0, z1), cons(z2, z3)) -> c12(MARK(z2)) A__ZIP(z0, z1) -> c13 A__TAIL(cons(z0, z1)) -> c14(MARK(z1)) A__TAIL(z0) -> c15 A__REPITEMS(nil) -> c16 A__REPITEMS(cons(z0, z1)) -> c17(MARK(z0)) A__REPITEMS(z0) -> c18 MARK(pairNs) -> c19(A__PAIRNS) MARK(incr(z0)) -> c20(A__INCR(mark(z0)), MARK(z0)) MARK(oddNs) -> c21(A__ODDNS) MARK(take(z0, z1)) -> c22(A__TAKE(mark(z0), mark(z1)), MARK(z0)) MARK(take(z0, z1)) -> c23(A__TAKE(mark(z0), mark(z1)), MARK(z1)) MARK(zip(z0, z1)) -> c24(A__ZIP(mark(z0), mark(z1)), MARK(z0)) MARK(zip(z0, z1)) -> c25(A__ZIP(mark(z0), mark(z1)), MARK(z1)) MARK(tail(z0)) -> c26(A__TAIL(mark(z0)), MARK(z0)) MARK(repItems(z0)) -> c27(A__REPITEMS(mark(z0)), MARK(z0)) MARK(cons(z0, z1)) -> c28(MARK(z0)) MARK(0) -> c29 MARK(s(z0)) -> c30(MARK(z0)) MARK(nil) -> c31 MARK(pair(z0, z1)) -> c32(MARK(z0)) MARK(pair(z0, z1)) -> c33(MARK(z1)) The (relative) TRS S consists of the following rules: a__pairNs -> cons(0, incr(oddNs)) a__pairNs -> pairNs a__oddNs -> a__incr(a__pairNs) a__oddNs -> oddNs a__incr(cons(z0, z1)) -> cons(s(mark(z0)), incr(z1)) a__incr(z0) -> incr(z0) a__take(0, z0) -> nil a__take(s(z0), cons(z1, z2)) -> cons(mark(z1), take(z0, z2)) a__take(z0, z1) -> take(z0, z1) a__zip(nil, z0) -> nil a__zip(z0, nil) -> nil a__zip(cons(z0, z1), cons(z2, z3)) -> cons(pair(mark(z0), mark(z2)), zip(z1, z3)) a__zip(z0, z1) -> zip(z0, z1) a__tail(cons(z0, z1)) -> mark(z1) a__tail(z0) -> tail(z0) a__repItems(nil) -> nil a__repItems(cons(z0, z1)) -> cons(mark(z0), cons(z0, repItems(z1))) a__repItems(z0) -> repItems(z0) mark(pairNs) -> a__pairNs mark(incr(z0)) -> a__incr(mark(z0)) mark(oddNs) -> a__oddNs mark(take(z0, z1)) -> a__take(mark(z0), mark(z1)) mark(zip(z0, z1)) -> a__zip(mark(z0), mark(z1)) mark(tail(z0)) -> a__tail(mark(z0)) mark(repItems(z0)) -> a__repItems(mark(z0)) mark(cons(z0, z1)) -> cons(mark(z0), z1) mark(0) -> 0 mark(s(z0)) -> s(mark(z0)) mark(nil) -> nil mark(pair(z0, z1)) -> pair(mark(z0), mark(z1)) 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: A__PAIRNS -> c A__PAIRNS -> c1 A__ODDNS -> c2(A__INCR(a__pairNs), A__PAIRNS) A__ODDNS -> c3 A__INCR(cons(z0, z1)) -> c4(MARK(z0)) A__INCR(z0) -> c5 A__TAKE(0, z0) -> c6 A__TAKE(s(z0), cons(z1, z2)) -> c7(MARK(z1)) A__TAKE(z0, z1) -> c8 A__ZIP(nil, z0) -> c9 A__ZIP(z0, nil) -> c10 A__ZIP(cons(z0, z1), cons(z2, z3)) -> c11(MARK(z0)) A__ZIP(cons(z0, z1), cons(z2, z3)) -> c12(MARK(z2)) A__ZIP(z0, z1) -> c13 A__TAIL(cons(z0, z1)) -> c14(MARK(z1)) A__TAIL(z0) -> c15 A__REPITEMS(nil) -> c16 A__REPITEMS(cons(z0, z1)) -> c17(MARK(z0)) A__REPITEMS(z0) -> c18 MARK(pairNs) -> c19(A__PAIRNS) MARK(incr(z0)) -> c20(A__INCR(mark(z0)), MARK(z0)) MARK(oddNs) -> c21(A__ODDNS) MARK(take(z0, z1)) -> c22(A__TAKE(mark(z0), mark(z1)), MARK(z0)) MARK(take(z0, z1)) -> c23(A__TAKE(mark(z0), mark(z1)), MARK(z1)) MARK(zip(z0, z1)) -> c24(A__ZIP(mark(z0), mark(z1)), MARK(z0)) MARK(zip(z0, z1)) -> c25(A__ZIP(mark(z0), mark(z1)), MARK(z1)) MARK(tail(z0)) -> c26(A__TAIL(mark(z0)), MARK(z0)) MARK(repItems(z0)) -> c27(A__REPITEMS(mark(z0)), MARK(z0)) MARK(cons(z0, z1)) -> c28(MARK(z0)) MARK(0) -> c29 MARK(s(z0)) -> c30(MARK(z0)) MARK(nil) -> c31 MARK(pair(z0, z1)) -> c32(MARK(z0)) MARK(pair(z0, z1)) -> c33(MARK(z1)) The (relative) TRS S consists of the following rules: a__pairNs -> cons(0, incr(oddNs)) a__pairNs -> pairNs a__oddNs -> a__incr(a__pairNs) a__oddNs -> oddNs a__incr(cons(z0, z1)) -> cons(s(mark(z0)), incr(z1)) a__incr(z0) -> incr(z0) a__take(0, z0) -> nil a__take(s(z0), cons(z1, z2)) -> cons(mark(z1), take(z0, z2)) a__take(z0, z1) -> take(z0, z1) a__zip(nil, z0) -> nil a__zip(z0, nil) -> nil a__zip(cons(z0, z1), cons(z2, z3)) -> cons(pair(mark(z0), mark(z2)), zip(z1, z3)) a__zip(z0, z1) -> zip(z0, z1) a__tail(cons(z0, z1)) -> mark(z1) a__tail(z0) -> tail(z0) a__repItems(nil) -> nil a__repItems(cons(z0, z1)) -> cons(mark(z0), cons(z0, repItems(z1))) a__repItems(z0) -> repItems(z0) mark(pairNs) -> a__pairNs mark(incr(z0)) -> a__incr(mark(z0)) mark(oddNs) -> a__oddNs mark(take(z0, z1)) -> a__take(mark(z0), mark(z1)) mark(zip(z0, z1)) -> a__zip(mark(z0), mark(z1)) mark(tail(z0)) -> a__tail(mark(z0)) mark(repItems(z0)) -> a__repItems(mark(z0)) mark(cons(z0, z1)) -> cons(mark(z0), z1) mark(0) -> 0 mark(s(z0)) -> s(mark(z0)) mark(nil) -> nil mark(pair(z0, z1)) -> pair(mark(z0), mark(z1)) 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: A__PAIRNS -> c A__PAIRNS -> c1 A__ODDNS -> c2(A__INCR(a__pairNs), A__PAIRNS) A__ODDNS -> c3 A__INCR(cons(z0, z1)) -> c4(MARK(z0)) A__INCR(z0) -> c5 A__TAKE(0, z0) -> c6 A__TAKE(s(z0), cons(z1, z2)) -> c7(MARK(z1)) A__TAKE(z0, z1) -> c8 A__ZIP(nil, z0) -> c9 A__ZIP(z0, nil) -> c10 A__ZIP(cons(z0, z1), cons(z2, z3)) -> c11(MARK(z0)) A__ZIP(cons(z0, z1), cons(z2, z3)) -> c12(MARK(z2)) A__ZIP(z0, z1) -> c13 A__TAIL(cons(z0, z1)) -> c14(MARK(z1)) A__TAIL(z0) -> c15 A__REPITEMS(nil) -> c16 A__REPITEMS(cons(z0, z1)) -> c17(MARK(z0)) A__REPITEMS(z0) -> c18 MARK(pairNs) -> c19(A__PAIRNS) MARK(incr(z0)) -> c20(A__INCR(mark(z0)), MARK(z0)) MARK(oddNs) -> c21(A__ODDNS) MARK(take(z0, z1)) -> c22(A__TAKE(mark(z0), mark(z1)), MARK(z0)) MARK(take(z0, z1)) -> c23(A__TAKE(mark(z0), mark(z1)), MARK(z1)) MARK(zip(z0, z1)) -> c24(A__ZIP(mark(z0), mark(z1)), MARK(z0)) MARK(zip(z0, z1)) -> c25(A__ZIP(mark(z0), mark(z1)), MARK(z1)) MARK(tail(z0)) -> c26(A__TAIL(mark(z0)), MARK(z0)) MARK(repItems(z0)) -> c27(A__REPITEMS(mark(z0)), MARK(z0)) MARK(cons(z0, z1)) -> c28(MARK(z0)) MARK(0) -> c29 MARK(s(z0)) -> c30(MARK(z0)) MARK(nil) -> c31 MARK(pair(z0, z1)) -> c32(MARK(z0)) MARK(pair(z0, z1)) -> c33(MARK(z1)) The (relative) TRS S consists of the following rules: a__pairNs -> cons(0, incr(oddNs)) a__pairNs -> pairNs a__oddNs -> a__incr(a__pairNs) a__oddNs -> oddNs a__incr(cons(z0, z1)) -> cons(s(mark(z0)), incr(z1)) a__incr(z0) -> incr(z0) a__take(0, z0) -> nil a__take(s(z0), cons(z1, z2)) -> cons(mark(z1), take(z0, z2)) a__take(z0, z1) -> take(z0, z1) a__zip(nil, z0) -> nil a__zip(z0, nil) -> nil a__zip(cons(z0, z1), cons(z2, z3)) -> cons(pair(mark(z0), mark(z2)), zip(z1, z3)) a__zip(z0, z1) -> zip(z0, z1) a__tail(cons(z0, z1)) -> mark(z1) a__tail(z0) -> tail(z0) a__repItems(nil) -> nil a__repItems(cons(z0, z1)) -> cons(mark(z0), cons(z0, repItems(z1))) a__repItems(z0) -> repItems(z0) mark(pairNs) -> a__pairNs mark(incr(z0)) -> a__incr(mark(z0)) mark(oddNs) -> a__oddNs mark(take(z0, z1)) -> a__take(mark(z0), mark(z1)) mark(zip(z0, z1)) -> a__zip(mark(z0), mark(z1)) mark(tail(z0)) -> a__tail(mark(z0)) mark(repItems(z0)) -> a__repItems(mark(z0)) mark(cons(z0, z1)) -> cons(mark(z0), z1) mark(0) -> 0 mark(s(z0)) -> s(mark(z0)) mark(nil) -> nil mark(pair(z0, z1)) -> pair(mark(z0), mark(z1)) 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 MARK(incr(z0)) ->^+ c20(A__INCR(mark(z0)), MARK(z0)) gives rise to a decreasing loop by considering the right hand sides subterm at position [1]. The pumping substitution is [z0 / incr(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: A__PAIRNS -> c A__PAIRNS -> c1 A__ODDNS -> c2(A__INCR(a__pairNs), A__PAIRNS) A__ODDNS -> c3 A__INCR(cons(z0, z1)) -> c4(MARK(z0)) A__INCR(z0) -> c5 A__TAKE(0, z0) -> c6 A__TAKE(s(z0), cons(z1, z2)) -> c7(MARK(z1)) A__TAKE(z0, z1) -> c8 A__ZIP(nil, z0) -> c9 A__ZIP(z0, nil) -> c10 A__ZIP(cons(z0, z1), cons(z2, z3)) -> c11(MARK(z0)) A__ZIP(cons(z0, z1), cons(z2, z3)) -> c12(MARK(z2)) A__ZIP(z0, z1) -> c13 A__TAIL(cons(z0, z1)) -> c14(MARK(z1)) A__TAIL(z0) -> c15 A__REPITEMS(nil) -> c16 A__REPITEMS(cons(z0, z1)) -> c17(MARK(z0)) A__REPITEMS(z0) -> c18 MARK(pairNs) -> c19(A__PAIRNS) MARK(incr(z0)) -> c20(A__INCR(mark(z0)), MARK(z0)) MARK(oddNs) -> c21(A__ODDNS) MARK(take(z0, z1)) -> c22(A__TAKE(mark(z0), mark(z1)), MARK(z0)) MARK(take(z0, z1)) -> c23(A__TAKE(mark(z0), mark(z1)), MARK(z1)) MARK(zip(z0, z1)) -> c24(A__ZIP(mark(z0), mark(z1)), MARK(z0)) MARK(zip(z0, z1)) -> c25(A__ZIP(mark(z0), mark(z1)), MARK(z1)) MARK(tail(z0)) -> c26(A__TAIL(mark(z0)), MARK(z0)) MARK(repItems(z0)) -> c27(A__REPITEMS(mark(z0)), MARK(z0)) MARK(cons(z0, z1)) -> c28(MARK(z0)) MARK(0) -> c29 MARK(s(z0)) -> c30(MARK(z0)) MARK(nil) -> c31 MARK(pair(z0, z1)) -> c32(MARK(z0)) MARK(pair(z0, z1)) -> c33(MARK(z1)) The (relative) TRS S consists of the following rules: a__pairNs -> cons(0, incr(oddNs)) a__pairNs -> pairNs a__oddNs -> a__incr(a__pairNs) a__oddNs -> oddNs a__incr(cons(z0, z1)) -> cons(s(mark(z0)), incr(z1)) a__incr(z0) -> incr(z0) a__take(0, z0) -> nil a__take(s(z0), cons(z1, z2)) -> cons(mark(z1), take(z0, z2)) a__take(z0, z1) -> take(z0, z1) a__zip(nil, z0) -> nil a__zip(z0, nil) -> nil a__zip(cons(z0, z1), cons(z2, z3)) -> cons(pair(mark(z0), mark(z2)), zip(z1, z3)) a__zip(z0, z1) -> zip(z0, z1) a__tail(cons(z0, z1)) -> mark(z1) a__tail(z0) -> tail(z0) a__repItems(nil) -> nil a__repItems(cons(z0, z1)) -> cons(mark(z0), cons(z0, repItems(z1))) a__repItems(z0) -> repItems(z0) mark(pairNs) -> a__pairNs mark(incr(z0)) -> a__incr(mark(z0)) mark(oddNs) -> a__oddNs mark(take(z0, z1)) -> a__take(mark(z0), mark(z1)) mark(zip(z0, z1)) -> a__zip(mark(z0), mark(z1)) mark(tail(z0)) -> a__tail(mark(z0)) mark(repItems(z0)) -> a__repItems(mark(z0)) mark(cons(z0, z1)) -> cons(mark(z0), z1) mark(0) -> 0 mark(s(z0)) -> s(mark(z0)) mark(nil) -> nil mark(pair(z0, z1)) -> pair(mark(z0), mark(z1)) 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: A__PAIRNS -> c A__PAIRNS -> c1 A__ODDNS -> c2(A__INCR(a__pairNs), A__PAIRNS) A__ODDNS -> c3 A__INCR(cons(z0, z1)) -> c4(MARK(z0)) A__INCR(z0) -> c5 A__TAKE(0, z0) -> c6 A__TAKE(s(z0), cons(z1, z2)) -> c7(MARK(z1)) A__TAKE(z0, z1) -> c8 A__ZIP(nil, z0) -> c9 A__ZIP(z0, nil) -> c10 A__ZIP(cons(z0, z1), cons(z2, z3)) -> c11(MARK(z0)) A__ZIP(cons(z0, z1), cons(z2, z3)) -> c12(MARK(z2)) A__ZIP(z0, z1) -> c13 A__TAIL(cons(z0, z1)) -> c14(MARK(z1)) A__TAIL(z0) -> c15 A__REPITEMS(nil) -> c16 A__REPITEMS(cons(z0, z1)) -> c17(MARK(z0)) A__REPITEMS(z0) -> c18 MARK(pairNs) -> c19(A__PAIRNS) MARK(incr(z0)) -> c20(A__INCR(mark(z0)), MARK(z0)) MARK(oddNs) -> c21(A__ODDNS) MARK(take(z0, z1)) -> c22(A__TAKE(mark(z0), mark(z1)), MARK(z0)) MARK(take(z0, z1)) -> c23(A__TAKE(mark(z0), mark(z1)), MARK(z1)) MARK(zip(z0, z1)) -> c24(A__ZIP(mark(z0), mark(z1)), MARK(z0)) MARK(zip(z0, z1)) -> c25(A__ZIP(mark(z0), mark(z1)), MARK(z1)) MARK(tail(z0)) -> c26(A__TAIL(mark(z0)), MARK(z0)) MARK(repItems(z0)) -> c27(A__REPITEMS(mark(z0)), MARK(z0)) MARK(cons(z0, z1)) -> c28(MARK(z0)) MARK(0) -> c29 MARK(s(z0)) -> c30(MARK(z0)) MARK(nil) -> c31 MARK(pair(z0, z1)) -> c32(MARK(z0)) MARK(pair(z0, z1)) -> c33(MARK(z1)) The (relative) TRS S consists of the following rules: a__pairNs -> cons(0, incr(oddNs)) a__pairNs -> pairNs a__oddNs -> a__incr(a__pairNs) a__oddNs -> oddNs a__incr(cons(z0, z1)) -> cons(s(mark(z0)), incr(z1)) a__incr(z0) -> incr(z0) a__take(0, z0) -> nil a__take(s(z0), cons(z1, z2)) -> cons(mark(z1), take(z0, z2)) a__take(z0, z1) -> take(z0, z1) a__zip(nil, z0) -> nil a__zip(z0, nil) -> nil a__zip(cons(z0, z1), cons(z2, z3)) -> cons(pair(mark(z0), mark(z2)), zip(z1, z3)) a__zip(z0, z1) -> zip(z0, z1) a__tail(cons(z0, z1)) -> mark(z1) a__tail(z0) -> tail(z0) a__repItems(nil) -> nil a__repItems(cons(z0, z1)) -> cons(mark(z0), cons(z0, repItems(z1))) a__repItems(z0) -> repItems(z0) mark(pairNs) -> a__pairNs mark(incr(z0)) -> a__incr(mark(z0)) mark(oddNs) -> a__oddNs mark(take(z0, z1)) -> a__take(mark(z0), mark(z1)) mark(zip(z0, z1)) -> a__zip(mark(z0), mark(z1)) mark(tail(z0)) -> a__tail(mark(z0)) mark(repItems(z0)) -> a__repItems(mark(z0)) mark(cons(z0, z1)) -> cons(mark(z0), z1) mark(0) -> 0 mark(s(z0)) -> s(mark(z0)) mark(nil) -> nil mark(pair(z0, z1)) -> pair(mark(z0), mark(z1)) Rewrite Strategy: INNERMOST