WORST_CASE(?,O(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(1, 1). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 227 ms] (2) CpxRelTRS (3) NarrowingOnBasicTermsTerminatesProof [FINISHED, 20 ms] (4) BOUNDS(1, 1) ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, 1). The TRS R consists of the following rules: G(z0) -> c1(U(h(z0), h(z0), z0), H(z0)) G(z0) -> c2(U(h(z0), h(z0), z0), H(z0)) U(d, c(z0), z1) -> c3 H(d) -> c4 H(d) -> c5 F(k(a), k(b), z0) -> c6(F(z0, z0, z0)) The (relative) TRS S consists of the following rules: g(z0) -> u(h(z0), h(z0), z0) u(d, c(z0), z1) -> k(z0) h(d) -> c(a) h(d) -> c(b) f(k(a), k(b), z0) -> f(z0, z0, z0) 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(1, 1). The TRS R consists of the following rules: G(z0) -> c1(U(h(z0), h(z0), z0), H(z0)) G(z0) -> c2(U(h(z0), h(z0), z0), H(z0)) U(d, c(z0), z1) -> c3 H(d) -> c4 H(d) -> c5 F(k(a), k(b), z0) -> c6(F(z0, z0, z0)) The (relative) TRS S consists of the following rules: g(z0) -> u(h(z0), h(z0), z0) u(d, c(z0), z1) -> k(z0) h(d) -> c(a) h(d) -> c(b) f(k(a), k(b), z0) -> f(z0, z0, z0) Rewrite Strategy: INNERMOST ---------------------------------------- (3) NarrowingOnBasicTermsTerminatesProof (FINISHED) Constant runtime complexity proven by termination of constructor-based narrowing. The maximal most general narrowing sequences give rise to the following rewrite sequences: f(k(a), k(b), x0) ->^* f(x0, x0, x0) h(d) ->^* c(b) h(d) ->^* c(a) u(d, c(x0), x1) ->^* k(x0) g(d) ->^* u(c(b), c(b), d) g(d) ->^* u(c(a), c(b), d) g(d) ->^* u(c(b), c(a), d) g(d) ->^* u(c(a), c(a), d) g(d) ->^* u(c(b), c(b), d) g(d) ->^* u(c(b), c(a), d) g(d) ->^* u(c(a), c(b), d) g(d) ->^* u(c(a), c(a), d) F(k(a), k(b), x0) ->^* c6(F(x0, x0, x0)) H(d) ->^* c5 H(d) ->^* c4 U(d, c(x0), x1) ->^* c3 G(d) ->^* c2(U(c(b), c(b), d), c5) G(d) ->^* c2(U(c(a), c(b), d), c5) G(d) ->^* c2(U(c(b), c(a), d), c5) G(d) ->^* c2(U(c(a), c(a), d), c5) G(d) ->^* c2(U(c(b), c(b), d), c5) G(d) ->^* c2(U(c(b), c(a), d), c5) G(d) ->^* c2(U(c(a), c(b), d), c5) G(d) ->^* c2(U(c(a), c(a), d), c5) G(d) ->^* c2(U(c(b), c(b), d), c4) G(d) ->^* c2(U(c(a), c(b), d), c4) G(d) ->^* c2(U(c(b), c(a), d), c4) G(d) ->^* c2(U(c(a), c(a), d), c4) G(d) ->^* c2(U(c(b), c(b), d), c4) G(d) ->^* c2(U(c(b), c(a), d), c4) G(d) ->^* c2(U(c(a), c(b), d), c4) G(d) ->^* c2(U(c(a), c(a), d), c4) G(d) ->^* c2(U(c(b), c(b), d), c5) G(d) ->^* c2(U(c(a), c(b), d), c5) G(d) ->^* c2(U(c(b), c(b), d), c4) G(d) ->^* c2(U(c(a), c(b), d), c4) G(d) ->^* c2(U(c(b), c(b), d), c5) G(d) ->^* c2(U(c(b), c(b), d), c4) G(d) ->^* c2(U(c(a), c(b), d), c5) G(d) ->^* c2(U(c(a), c(b), d), c4) G(d) ->^* c2(U(c(b), c(a), d), c5) G(d) ->^* c2(U(c(a), c(a), d), c5) G(d) ->^* c2(U(c(b), c(a), d), c4) G(d) ->^* c2(U(c(a), c(a), d), c4) G(d) ->^* c2(U(c(b), c(a), d), c5) G(d) ->^* c2(U(c(b), c(a), d), c4) G(d) ->^* c2(U(c(a), c(a), d), c5) G(d) ->^* c2(U(c(a), c(a), d), c4) G(d) ->^* c2(U(c(b), c(b), d), c5) G(d) ->^* c2(U(c(b), c(a), d), c5) G(d) ->^* c2(U(c(b), c(b), d), c4) G(d) ->^* c2(U(c(b), c(a), d), c4) G(d) ->^* c2(U(c(b), c(b), d), c5) G(d) ->^* c2(U(c(b), c(b), d), c4) G(d) ->^* c2(U(c(b), c(a), d), c5) G(d) ->^* c2(U(c(b), c(a), d), c4) G(d) ->^* c2(U(c(a), c(b), d), c5) G(d) ->^* c2(U(c(a), c(a), d), c5) G(d) ->^* c2(U(c(a), c(b), d), c4) G(d) ->^* c2(U(c(a), c(a), d), c4) G(d) ->^* c2(U(c(a), c(b), d), c5) G(d) ->^* c2(U(c(a), c(b), d), c4) G(d) ->^* c2(U(c(a), c(a), d), c5) G(d) ->^* c2(U(c(a), c(a), d), c4) G(d) ->^* c1(U(c(b), c(b), d), c5) G(d) ->^* c1(U(c(a), c(b), d), c5) G(d) ->^* c1(U(c(b), c(a), d), c5) G(d) ->^* c1(U(c(a), c(a), d), c5) G(d) ->^* c1(U(c(b), c(b), d), c5) G(d) ->^* c1(U(c(b), c(a), d), c5) G(d) ->^* c1(U(c(a), c(b), d), c5) G(d) ->^* c1(U(c(a), c(a), d), c5) G(d) ->^* c1(U(c(b), c(b), d), c4) G(d) ->^* c1(U(c(a), c(b), d), c4) G(d) ->^* c1(U(c(b), c(a), d), c4) G(d) ->^* c1(U(c(a), c(a), d), c4) G(d) ->^* c1(U(c(b), c(b), d), c4) G(d) ->^* c1(U(c(b), c(a), d), c4) G(d) ->^* c1(U(c(a), c(b), d), c4) G(d) ->^* c1(U(c(a), c(a), d), c4) G(d) ->^* c1(U(c(b), c(b), d), c5) G(d) ->^* c1(U(c(a), c(b), d), c5) G(d) ->^* c1(U(c(b), c(b), d), c4) G(d) ->^* c1(U(c(a), c(b), d), c4) G(d) ->^* c1(U(c(b), c(b), d), c5) G(d) ->^* c1(U(c(b), c(b), d), c4) G(d) ->^* c1(U(c(a), c(b), d), c5) G(d) ->^* c1(U(c(a), c(b), d), c4) G(d) ->^* c1(U(c(b), c(a), d), c5) G(d) ->^* c1(U(c(a), c(a), d), c5) G(d) ->^* c1(U(c(b), c(a), d), c4) G(d) ->^* c1(U(c(a), c(a), d), c4) G(d) ->^* c1(U(c(b), c(a), d), c5) G(d) ->^* c1(U(c(b), c(a), d), c4) G(d) ->^* c1(U(c(a), c(a), d), c5) G(d) ->^* c1(U(c(a), c(a), d), c4) G(d) ->^* c1(U(c(b), c(b), d), c5) G(d) ->^* c1(U(c(b), c(a), d), c5) G(d) ->^* c1(U(c(b), c(b), d), c4) G(d) ->^* c1(U(c(b), c(a), d), c4) G(d) ->^* c1(U(c(b), c(b), d), c5) G(d) ->^* c1(U(c(b), c(b), d), c4) G(d) ->^* c1(U(c(b), c(a), d), c5) G(d) ->^* c1(U(c(b), c(a), d), c4) G(d) ->^* c1(U(c(a), c(b), d), c5) G(d) ->^* c1(U(c(a), c(a), d), c5) G(d) ->^* c1(U(c(a), c(b), d), c4) G(d) ->^* c1(U(c(a), c(a), d), c4) G(d) ->^* c1(U(c(a), c(b), d), c5) G(d) ->^* c1(U(c(a), c(b), d), c4) G(d) ->^* c1(U(c(a), c(a), d), c5) G(d) ->^* c1(U(c(a), c(a), d), c4) ---------------------------------------- (4) BOUNDS(1, 1)