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), 32.9 s] (2) CpxRelTRS (3) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 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: FSTSPLIT(0, z0) -> c FSTSPLIT(s(z0), nil) -> c1 FSTSPLIT(s(z0), cons(z1, z2)) -> c2(FSTSPLIT(z0, z2)) SNDSPLIT(0, z0) -> c3 SNDSPLIT(s(z0), nil) -> c4 SNDSPLIT(s(z0), cons(z1, z2)) -> c5(SNDSPLIT(z0, z2)) EMPTY(nil) -> c6 EMPTY(cons(z0, z1)) -> c7 LEQ(0, z0) -> c8 LEQ(s(z0), 0) -> c9 LEQ(s(z0), s(z1)) -> c10(LEQ(z0, z1)) LENGTH(nil) -> c11 LENGTH(cons(z0, z1)) -> c12(LENGTH(z1)) APP(nil, z0) -> c13 APP(cons(z0, z1), z2) -> c14(APP(z1, z2)) MAP_F(z0, nil) -> c15 MAP_F(z0, cons(z1, z2)) -> c16(APP(f(z0, z1), map_f(z0, z2)), MAP_F(z0, z2)) PROCESS(z0, z1) -> c17(IF1(z0, z1, leq(z1, length(z0))), LEQ(z1, length(z0)), LENGTH(z0)) IF1(z0, z1, true) -> c18(IF2(z0, z1, empty(fstsplit(z1, z0))), EMPTY(fstsplit(z1, z0)), FSTSPLIT(z1, z0)) IF1(z0, z1, false) -> c19(IF3(z0, z1, empty(fstsplit(z1, app(map_f(self, nil), z0)))), EMPTY(fstsplit(z1, app(map_f(self, nil), z0))), FSTSPLIT(z1, app(map_f(self, nil), z0)), APP(map_f(self, nil), z0), MAP_F(self, nil)) IF2(z0, z1, false) -> c20(PROCESS(app(map_f(self, nil), sndsplit(z1, z0)), z1), APP(map_f(self, nil), sndsplit(z1, z0)), MAP_F(self, nil)) IF2(z0, z1, false) -> c21(PROCESS(app(map_f(self, nil), sndsplit(z1, z0)), z1), APP(map_f(self, nil), sndsplit(z1, z0)), SNDSPLIT(z1, z0)) IF3(z0, z1, false) -> c22(PROCESS(sndsplit(z1, app(map_f(self, nil), z0)), z1), SNDSPLIT(z1, app(map_f(self, nil), z0)), APP(map_f(self, nil), z0), MAP_F(self, nil)) The (relative) TRS S consists of the following rules: fstsplit(0, z0) -> nil fstsplit(s(z0), nil) -> nil fstsplit(s(z0), cons(z1, z2)) -> cons(z1, fstsplit(z0, z2)) sndsplit(0, z0) -> z0 sndsplit(s(z0), nil) -> nil sndsplit(s(z0), cons(z1, z2)) -> sndsplit(z0, z2) empty(nil) -> true empty(cons(z0, z1)) -> false leq(0, z0) -> true leq(s(z0), 0) -> false leq(s(z0), s(z1)) -> leq(z0, z1) length(nil) -> 0 length(cons(z0, z1)) -> s(length(z1)) app(nil, z0) -> z0 app(cons(z0, z1), z2) -> cons(z0, app(z1, z2)) map_f(z0, nil) -> nil map_f(z0, cons(z1, z2)) -> app(f(z0, z1), map_f(z0, z2)) process(z0, z1) -> if1(z0, z1, leq(z1, length(z0))) if1(z0, z1, true) -> if2(z0, z1, empty(fstsplit(z1, z0))) if1(z0, z1, false) -> if3(z0, z1, empty(fstsplit(z1, app(map_f(self, nil), z0)))) if2(z0, z1, false) -> process(app(map_f(self, nil), sndsplit(z1, z0)), z1) if3(z0, z1, false) -> process(sndsplit(z1, app(map_f(self, nil), z0)), 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: FSTSPLIT(0, z0) -> c FSTSPLIT(s(z0), nil) -> c1 FSTSPLIT(s(z0), cons(z1, z2)) -> c2(FSTSPLIT(z0, z2)) SNDSPLIT(0, z0) -> c3 SNDSPLIT(s(z0), nil) -> c4 SNDSPLIT(s(z0), cons(z1, z2)) -> c5(SNDSPLIT(z0, z2)) EMPTY(nil) -> c6 EMPTY(cons(z0, z1)) -> c7 LEQ(0, z0) -> c8 LEQ(s(z0), 0) -> c9 LEQ(s(z0), s(z1)) -> c10(LEQ(z0, z1)) LENGTH(nil) -> c11 LENGTH(cons(z0, z1)) -> c12(LENGTH(z1)) APP(nil, z0) -> c13 APP(cons(z0, z1), z2) -> c14(APP(z1, z2)) MAP_F(z0, nil) -> c15 MAP_F(z0, cons(z1, z2)) -> c16(APP(f(z0, z1), map_f(z0, z2)), MAP_F(z0, z2)) PROCESS(z0, z1) -> c17(IF1(z0, z1, leq(z1, length(z0))), LEQ(z1, length(z0)), LENGTH(z0)) IF1(z0, z1, true) -> c18(IF2(z0, z1, empty(fstsplit(z1, z0))), EMPTY(fstsplit(z1, z0)), FSTSPLIT(z1, z0)) IF1(z0, z1, false) -> c19(IF3(z0, z1, empty(fstsplit(z1, app(map_f(self, nil), z0)))), EMPTY(fstsplit(z1, app(map_f(self, nil), z0))), FSTSPLIT(z1, app(map_f(self, nil), z0)), APP(map_f(self, nil), z0), MAP_F(self, nil)) IF2(z0, z1, false) -> c20(PROCESS(app(map_f(self, nil), sndsplit(z1, z0)), z1), APP(map_f(self, nil), sndsplit(z1, z0)), MAP_F(self, nil)) IF2(z0, z1, false) -> c21(PROCESS(app(map_f(self, nil), sndsplit(z1, z0)), z1), APP(map_f(self, nil), sndsplit(z1, z0)), SNDSPLIT(z1, z0)) IF3(z0, z1, false) -> c22(PROCESS(sndsplit(z1, app(map_f(self, nil), z0)), z1), SNDSPLIT(z1, app(map_f(self, nil), z0)), APP(map_f(self, nil), z0), MAP_F(self, nil)) The (relative) TRS S consists of the following rules: fstsplit(0, z0) -> nil fstsplit(s(z0), nil) -> nil fstsplit(s(z0), cons(z1, z2)) -> cons(z1, fstsplit(z0, z2)) sndsplit(0, z0) -> z0 sndsplit(s(z0), nil) -> nil sndsplit(s(z0), cons(z1, z2)) -> sndsplit(z0, z2) empty(nil) -> true empty(cons(z0, z1)) -> false leq(0, z0) -> true leq(s(z0), 0) -> false leq(s(z0), s(z1)) -> leq(z0, z1) length(nil) -> 0 length(cons(z0, z1)) -> s(length(z1)) app(nil, z0) -> z0 app(cons(z0, z1), z2) -> cons(z0, app(z1, z2)) map_f(z0, nil) -> nil map_f(z0, cons(z1, z2)) -> app(f(z0, z1), map_f(z0, z2)) process(z0, z1) -> if1(z0, z1, leq(z1, length(z0))) if1(z0, z1, true) -> if2(z0, z1, empty(fstsplit(z1, z0))) if1(z0, z1, false) -> if3(z0, z1, empty(fstsplit(z1, app(map_f(self, nil), z0)))) if2(z0, z1, false) -> process(app(map_f(self, nil), sndsplit(z1, z0)), z1) if3(z0, z1, false) -> process(sndsplit(z1, app(map_f(self, nil), z0)), 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: FSTSPLIT(0, z0) -> c FSTSPLIT(s(z0), nil) -> c1 FSTSPLIT(s(z0), cons(z1, z2)) -> c2(FSTSPLIT(z0, z2)) SNDSPLIT(0, z0) -> c3 SNDSPLIT(s(z0), nil) -> c4 SNDSPLIT(s(z0), cons(z1, z2)) -> c5(SNDSPLIT(z0, z2)) EMPTY(nil) -> c6 EMPTY(cons(z0, z1)) -> c7 LEQ(0, z0) -> c8 LEQ(s(z0), 0) -> c9 LEQ(s(z0), s(z1)) -> c10(LEQ(z0, z1)) LENGTH(nil) -> c11 LENGTH(cons(z0, z1)) -> c12(LENGTH(z1)) APP(nil, z0) -> c13 APP(cons(z0, z1), z2) -> c14(APP(z1, z2)) MAP_F(z0, nil) -> c15 MAP_F(z0, cons(z1, z2)) -> c16(APP(f(z0, z1), map_f(z0, z2)), MAP_F(z0, z2)) PROCESS(z0, z1) -> c17(IF1(z0, z1, leq(z1, length(z0))), LEQ(z1, length(z0)), LENGTH(z0)) IF1(z0, z1, true) -> c18(IF2(z0, z1, empty(fstsplit(z1, z0))), EMPTY(fstsplit(z1, z0)), FSTSPLIT(z1, z0)) IF1(z0, z1, false) -> c19(IF3(z0, z1, empty(fstsplit(z1, app(map_f(self, nil), z0)))), EMPTY(fstsplit(z1, app(map_f(self, nil), z0))), FSTSPLIT(z1, app(map_f(self, nil), z0)), APP(map_f(self, nil), z0), MAP_F(self, nil)) IF2(z0, z1, false) -> c20(PROCESS(app(map_f(self, nil), sndsplit(z1, z0)), z1), APP(map_f(self, nil), sndsplit(z1, z0)), MAP_F(self, nil)) IF2(z0, z1, false) -> c21(PROCESS(app(map_f(self, nil), sndsplit(z1, z0)), z1), APP(map_f(self, nil), sndsplit(z1, z0)), SNDSPLIT(z1, z0)) IF3(z0, z1, false) -> c22(PROCESS(sndsplit(z1, app(map_f(self, nil), z0)), z1), SNDSPLIT(z1, app(map_f(self, nil), z0)), APP(map_f(self, nil), z0), MAP_F(self, nil)) The (relative) TRS S consists of the following rules: fstsplit(0, z0) -> nil fstsplit(s(z0), nil) -> nil fstsplit(s(z0), cons(z1, z2)) -> cons(z1, fstsplit(z0, z2)) sndsplit(0, z0) -> z0 sndsplit(s(z0), nil) -> nil sndsplit(s(z0), cons(z1, z2)) -> sndsplit(z0, z2) empty(nil) -> true empty(cons(z0, z1)) -> false leq(0, z0) -> true leq(s(z0), 0) -> false leq(s(z0), s(z1)) -> leq(z0, z1) length(nil) -> 0 length(cons(z0, z1)) -> s(length(z1)) app(nil, z0) -> z0 app(cons(z0, z1), z2) -> cons(z0, app(z1, z2)) map_f(z0, nil) -> nil map_f(z0, cons(z1, z2)) -> app(f(z0, z1), map_f(z0, z2)) process(z0, z1) -> if1(z0, z1, leq(z1, length(z0))) if1(z0, z1, true) -> if2(z0, z1, empty(fstsplit(z1, z0))) if1(z0, z1, false) -> if3(z0, z1, empty(fstsplit(z1, app(map_f(self, nil), z0)))) if2(z0, z1, false) -> process(app(map_f(self, nil), sndsplit(z1, z0)), z1) if3(z0, z1, false) -> process(sndsplit(z1, app(map_f(self, nil), z0)), 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 FSTSPLIT(s(z0), cons(z1, z2)) ->^+ c2(FSTSPLIT(z0, z2)) gives rise to a decreasing loop by considering the right hand sides subterm at position [0]. The pumping substitution is [z0 / s(z0), z2 / cons(z1, z2)]. 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: FSTSPLIT(0, z0) -> c FSTSPLIT(s(z0), nil) -> c1 FSTSPLIT(s(z0), cons(z1, z2)) -> c2(FSTSPLIT(z0, z2)) SNDSPLIT(0, z0) -> c3 SNDSPLIT(s(z0), nil) -> c4 SNDSPLIT(s(z0), cons(z1, z2)) -> c5(SNDSPLIT(z0, z2)) EMPTY(nil) -> c6 EMPTY(cons(z0, z1)) -> c7 LEQ(0, z0) -> c8 LEQ(s(z0), 0) -> c9 LEQ(s(z0), s(z1)) -> c10(LEQ(z0, z1)) LENGTH(nil) -> c11 LENGTH(cons(z0, z1)) -> c12(LENGTH(z1)) APP(nil, z0) -> c13 APP(cons(z0, z1), z2) -> c14(APP(z1, z2)) MAP_F(z0, nil) -> c15 MAP_F(z0, cons(z1, z2)) -> c16(APP(f(z0, z1), map_f(z0, z2)), MAP_F(z0, z2)) PROCESS(z0, z1) -> c17(IF1(z0, z1, leq(z1, length(z0))), LEQ(z1, length(z0)), LENGTH(z0)) IF1(z0, z1, true) -> c18(IF2(z0, z1, empty(fstsplit(z1, z0))), EMPTY(fstsplit(z1, z0)), FSTSPLIT(z1, z0)) IF1(z0, z1, false) -> c19(IF3(z0, z1, empty(fstsplit(z1, app(map_f(self, nil), z0)))), EMPTY(fstsplit(z1, app(map_f(self, nil), z0))), FSTSPLIT(z1, app(map_f(self, nil), z0)), APP(map_f(self, nil), z0), MAP_F(self, nil)) IF2(z0, z1, false) -> c20(PROCESS(app(map_f(self, nil), sndsplit(z1, z0)), z1), APP(map_f(self, nil), sndsplit(z1, z0)), MAP_F(self, nil)) IF2(z0, z1, false) -> c21(PROCESS(app(map_f(self, nil), sndsplit(z1, z0)), z1), APP(map_f(self, nil), sndsplit(z1, z0)), SNDSPLIT(z1, z0)) IF3(z0, z1, false) -> c22(PROCESS(sndsplit(z1, app(map_f(self, nil), z0)), z1), SNDSPLIT(z1, app(map_f(self, nil), z0)), APP(map_f(self, nil), z0), MAP_F(self, nil)) The (relative) TRS S consists of the following rules: fstsplit(0, z0) -> nil fstsplit(s(z0), nil) -> nil fstsplit(s(z0), cons(z1, z2)) -> cons(z1, fstsplit(z0, z2)) sndsplit(0, z0) -> z0 sndsplit(s(z0), nil) -> nil sndsplit(s(z0), cons(z1, z2)) -> sndsplit(z0, z2) empty(nil) -> true empty(cons(z0, z1)) -> false leq(0, z0) -> true leq(s(z0), 0) -> false leq(s(z0), s(z1)) -> leq(z0, z1) length(nil) -> 0 length(cons(z0, z1)) -> s(length(z1)) app(nil, z0) -> z0 app(cons(z0, z1), z2) -> cons(z0, app(z1, z2)) map_f(z0, nil) -> nil map_f(z0, cons(z1, z2)) -> app(f(z0, z1), map_f(z0, z2)) process(z0, z1) -> if1(z0, z1, leq(z1, length(z0))) if1(z0, z1, true) -> if2(z0, z1, empty(fstsplit(z1, z0))) if1(z0, z1, false) -> if3(z0, z1, empty(fstsplit(z1, app(map_f(self, nil), z0)))) if2(z0, z1, false) -> process(app(map_f(self, nil), sndsplit(z1, z0)), z1) if3(z0, z1, false) -> process(sndsplit(z1, app(map_f(self, nil), z0)), 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: FSTSPLIT(0, z0) -> c FSTSPLIT(s(z0), nil) -> c1 FSTSPLIT(s(z0), cons(z1, z2)) -> c2(FSTSPLIT(z0, z2)) SNDSPLIT(0, z0) -> c3 SNDSPLIT(s(z0), nil) -> c4 SNDSPLIT(s(z0), cons(z1, z2)) -> c5(SNDSPLIT(z0, z2)) EMPTY(nil) -> c6 EMPTY(cons(z0, z1)) -> c7 LEQ(0, z0) -> c8 LEQ(s(z0), 0) -> c9 LEQ(s(z0), s(z1)) -> c10(LEQ(z0, z1)) LENGTH(nil) -> c11 LENGTH(cons(z0, z1)) -> c12(LENGTH(z1)) APP(nil, z0) -> c13 APP(cons(z0, z1), z2) -> c14(APP(z1, z2)) MAP_F(z0, nil) -> c15 MAP_F(z0, cons(z1, z2)) -> c16(APP(f(z0, z1), map_f(z0, z2)), MAP_F(z0, z2)) PROCESS(z0, z1) -> c17(IF1(z0, z1, leq(z1, length(z0))), LEQ(z1, length(z0)), LENGTH(z0)) IF1(z0, z1, true) -> c18(IF2(z0, z1, empty(fstsplit(z1, z0))), EMPTY(fstsplit(z1, z0)), FSTSPLIT(z1, z0)) IF1(z0, z1, false) -> c19(IF3(z0, z1, empty(fstsplit(z1, app(map_f(self, nil), z0)))), EMPTY(fstsplit(z1, app(map_f(self, nil), z0))), FSTSPLIT(z1, app(map_f(self, nil), z0)), APP(map_f(self, nil), z0), MAP_F(self, nil)) IF2(z0, z1, false) -> c20(PROCESS(app(map_f(self, nil), sndsplit(z1, z0)), z1), APP(map_f(self, nil), sndsplit(z1, z0)), MAP_F(self, nil)) IF2(z0, z1, false) -> c21(PROCESS(app(map_f(self, nil), sndsplit(z1, z0)), z1), APP(map_f(self, nil), sndsplit(z1, z0)), SNDSPLIT(z1, z0)) IF3(z0, z1, false) -> c22(PROCESS(sndsplit(z1, app(map_f(self, nil), z0)), z1), SNDSPLIT(z1, app(map_f(self, nil), z0)), APP(map_f(self, nil), z0), MAP_F(self, nil)) The (relative) TRS S consists of the following rules: fstsplit(0, z0) -> nil fstsplit(s(z0), nil) -> nil fstsplit(s(z0), cons(z1, z2)) -> cons(z1, fstsplit(z0, z2)) sndsplit(0, z0) -> z0 sndsplit(s(z0), nil) -> nil sndsplit(s(z0), cons(z1, z2)) -> sndsplit(z0, z2) empty(nil) -> true empty(cons(z0, z1)) -> false leq(0, z0) -> true leq(s(z0), 0) -> false leq(s(z0), s(z1)) -> leq(z0, z1) length(nil) -> 0 length(cons(z0, z1)) -> s(length(z1)) app(nil, z0) -> z0 app(cons(z0, z1), z2) -> cons(z0, app(z1, z2)) map_f(z0, nil) -> nil map_f(z0, cons(z1, z2)) -> app(f(z0, z1), map_f(z0, z2)) process(z0, z1) -> if1(z0, z1, leq(z1, length(z0))) if1(z0, z1, true) -> if2(z0, z1, empty(fstsplit(z1, z0))) if1(z0, z1, false) -> if3(z0, z1, empty(fstsplit(z1, app(map_f(self, nil), z0)))) if2(z0, z1, false) -> process(app(map_f(self, nil), sndsplit(z1, z0)), z1) if3(z0, z1, false) -> process(sndsplit(z1, app(map_f(self, nil), z0)), z1) Rewrite Strategy: INNERMOST