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), 354 ms] (2) CpxRelTRS (3) RenamingProof [BOTH BOUNDS(ID, ID), 1 ms] (4) CpxRelTRS (5) SlicingProof [LOWER BOUND(ID), 0 ms] (6) CpxRelTRS (7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (8) typed CpxTrs (9) OrderProof [LOWER BOUND(ID), 0 ms] (10) typed CpxTrs (11) RewriteLemmaProof [LOWER BOUND(ID), 229 ms] (12) BEST (13) proven lower bound (14) LowerBoundPropagationProof [FINISHED, 0 ms] (15) BOUNDS(n^1, INF) (16) typed CpxTrs ---------------------------------------- (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: rw(Val(n), c) -> Op(Val(n), rewrite(c)) rewrite(Op(x, y)) -> rw(x, y) rw(Op(x, y), c) -> rw[Let](Op(x, y), c, rewrite(x)) rewrite(Val(n)) -> Val(n) second(Op(x, y)) -> y isOp(Val(n)) -> False isOp(Op(x, y)) -> True first(Val(n)) -> Val(n) first(Op(x, y)) -> x assrewrite(exp) -> rewrite(exp) The (relative) TRS S consists of the following rules: rw[Let](Op(x, y), c, a1) -> rw[Let][Let](Op(x, y), c, a1, rewrite(y)) rw[Let][Let](ab, c, a1, b1) -> rw[Let][Let][Let](c, a1, b1, rewrite(c)) rw[Let][Let][Let](c, a1, b1, c1) -> rw(a1, Op(b1, c1)) 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: rw(Val(n), c) -> Op(Val(n), rewrite(c)) rewrite(Op(x, y)) -> rw(x, y) rw(Op(x, y), c) -> rw[Let](Op(x, y), c, rewrite(x)) rewrite(Val(n)) -> Val(n) second(Op(x, y)) -> y isOp(Val(n)) -> False isOp(Op(x, y)) -> True first(Val(n)) -> Val(n) first(Op(x, y)) -> x assrewrite(exp) -> rewrite(exp) The (relative) TRS S consists of the following rules: rw[Let](Op(x, y), c, a1) -> rw[Let][Let](Op(x, y), c, a1, rewrite(y)) rw[Let][Let](ab, c, a1, b1) -> rw[Let][Let][Let](c, a1, b1, rewrite(c)) rw[Let][Let][Let](c, a1, b1, c1) -> rw(a1, Op(b1, c1)) Rewrite Strategy: INNERMOST ---------------------------------------- (3) RenamingProof (BOTH BOUNDS(ID, ID)) Renamed function symbols to avoid clashes with predefined symbol. ---------------------------------------- (4) 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: rw(Val(n), c) -> Op(Val(n), rewrite(c)) rewrite(Op(x, y)) -> rw(x, y) rw(Op(x, y), c) -> rw[Let](Op(x, y), c, rewrite(x)) rewrite(Val(n)) -> Val(n) second(Op(x, y)) -> y isOp(Val(n)) -> False isOp(Op(x, y)) -> True first(Val(n)) -> Val(n) first(Op(x, y)) -> x assrewrite(exp) -> rewrite(exp) The (relative) TRS S consists of the following rules: rw[Let](Op(x, y), c, a1) -> rw[Let][Let](Op(x, y), c, a1, rewrite(y)) rw[Let][Let](ab, c, a1, b1) -> rw[Let][Let][Let](c, a1, b1, rewrite(c)) rw[Let][Let][Let](c, a1, b1, c1) -> rw(a1, Op(b1, c1)) Rewrite Strategy: INNERMOST ---------------------------------------- (5) SlicingProof (LOWER BOUND(ID)) Sliced the following arguments: Val/0 rw[Let][Let]/0 rw[Let][Let][Let]/0 ---------------------------------------- (6) 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: rw(Val, c) -> Op(Val, rewrite(c)) rewrite(Op(x, y)) -> rw(x, y) rw(Op(x, y), c) -> rw[Let](Op(x, y), c, rewrite(x)) rewrite(Val) -> Val second(Op(x, y)) -> y isOp(Val) -> False isOp(Op(x, y)) -> True first(Val) -> Val first(Op(x, y)) -> x assrewrite(exp) -> rewrite(exp) The (relative) TRS S consists of the following rules: rw[Let](Op(x, y), c, a1) -> rw[Let][Let](c, a1, rewrite(y)) rw[Let][Let](c, a1, b1) -> rw[Let][Let][Let](a1, b1, rewrite(c)) rw[Let][Let][Let](a1, b1, c1) -> rw(a1, Op(b1, c1)) Rewrite Strategy: INNERMOST ---------------------------------------- (7) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (8) Obligation: Innermost TRS: Rules: rw(Val, c) -> Op(Val, rewrite(c)) rewrite(Op(x, y)) -> rw(x, y) rw(Op(x, y), c) -> rw[Let](Op(x, y), c, rewrite(x)) rewrite(Val) -> Val second(Op(x, y)) -> y isOp(Val) -> False isOp(Op(x, y)) -> True first(Val) -> Val first(Op(x, y)) -> x assrewrite(exp) -> rewrite(exp) rw[Let](Op(x, y), c, a1) -> rw[Let][Let](c, a1, rewrite(y)) rw[Let][Let](c, a1, b1) -> rw[Let][Let][Let](a1, b1, rewrite(c)) rw[Let][Let][Let](a1, b1, c1) -> rw(a1, Op(b1, c1)) Types: rw :: Val:Op -> Val:Op -> Val:Op Val :: Val:Op Op :: Val:Op -> Val:Op -> Val:Op rewrite :: Val:Op -> Val:Op rw[Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op second :: Val:Op -> Val:Op isOp :: Val:Op -> False:True False :: False:True True :: False:True first :: Val:Op -> Val:Op assrewrite :: Val:Op -> Val:Op rw[Let][Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op rw[Let][Let][Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op hole_Val:Op1_0 :: Val:Op hole_False:True2_0 :: False:True gen_Val:Op3_0 :: Nat -> Val:Op ---------------------------------------- (9) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: rw, rewrite They will be analysed ascendingly in the following order: rw = rewrite ---------------------------------------- (10) Obligation: Innermost TRS: Rules: rw(Val, c) -> Op(Val, rewrite(c)) rewrite(Op(x, y)) -> rw(x, y) rw(Op(x, y), c) -> rw[Let](Op(x, y), c, rewrite(x)) rewrite(Val) -> Val second(Op(x, y)) -> y isOp(Val) -> False isOp(Op(x, y)) -> True first(Val) -> Val first(Op(x, y)) -> x assrewrite(exp) -> rewrite(exp) rw[Let](Op(x, y), c, a1) -> rw[Let][Let](c, a1, rewrite(y)) rw[Let][Let](c, a1, b1) -> rw[Let][Let][Let](a1, b1, rewrite(c)) rw[Let][Let][Let](a1, b1, c1) -> rw(a1, Op(b1, c1)) Types: rw :: Val:Op -> Val:Op -> Val:Op Val :: Val:Op Op :: Val:Op -> Val:Op -> Val:Op rewrite :: Val:Op -> Val:Op rw[Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op second :: Val:Op -> Val:Op isOp :: Val:Op -> False:True False :: False:True True :: False:True first :: Val:Op -> Val:Op assrewrite :: Val:Op -> Val:Op rw[Let][Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op rw[Let][Let][Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op hole_Val:Op1_0 :: Val:Op hole_False:True2_0 :: False:True gen_Val:Op3_0 :: Nat -> Val:Op Generator Equations: gen_Val:Op3_0(0) <=> Val gen_Val:Op3_0(+(x, 1)) <=> Op(Val, gen_Val:Op3_0(x)) The following defined symbols remain to be analysed: rewrite, rw They will be analysed ascendingly in the following order: rw = rewrite ---------------------------------------- (11) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: rewrite(gen_Val:Op3_0(n5_0)) -> gen_Val:Op3_0(n5_0), rt in Omega(1 + n5_0) Induction Base: rewrite(gen_Val:Op3_0(0)) ->_R^Omega(1) Val Induction Step: rewrite(gen_Val:Op3_0(+(n5_0, 1))) ->_R^Omega(1) rw(Val, gen_Val:Op3_0(n5_0)) ->_R^Omega(1) Op(Val, rewrite(gen_Val:Op3_0(n5_0))) ->_IH Op(Val, gen_Val:Op3_0(c6_0)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (12) Complex Obligation (BEST) ---------------------------------------- (13) Obligation: Proved the lower bound n^1 for the following obligation: Innermost TRS: Rules: rw(Val, c) -> Op(Val, rewrite(c)) rewrite(Op(x, y)) -> rw(x, y) rw(Op(x, y), c) -> rw[Let](Op(x, y), c, rewrite(x)) rewrite(Val) -> Val second(Op(x, y)) -> y isOp(Val) -> False isOp(Op(x, y)) -> True first(Val) -> Val first(Op(x, y)) -> x assrewrite(exp) -> rewrite(exp) rw[Let](Op(x, y), c, a1) -> rw[Let][Let](c, a1, rewrite(y)) rw[Let][Let](c, a1, b1) -> rw[Let][Let][Let](a1, b1, rewrite(c)) rw[Let][Let][Let](a1, b1, c1) -> rw(a1, Op(b1, c1)) Types: rw :: Val:Op -> Val:Op -> Val:Op Val :: Val:Op Op :: Val:Op -> Val:Op -> Val:Op rewrite :: Val:Op -> Val:Op rw[Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op second :: Val:Op -> Val:Op isOp :: Val:Op -> False:True False :: False:True True :: False:True first :: Val:Op -> Val:Op assrewrite :: Val:Op -> Val:Op rw[Let][Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op rw[Let][Let][Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op hole_Val:Op1_0 :: Val:Op hole_False:True2_0 :: False:True gen_Val:Op3_0 :: Nat -> Val:Op Generator Equations: gen_Val:Op3_0(0) <=> Val gen_Val:Op3_0(+(x, 1)) <=> Op(Val, gen_Val:Op3_0(x)) The following defined symbols remain to be analysed: rewrite, rw They will be analysed ascendingly in the following order: rw = rewrite ---------------------------------------- (14) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (15) BOUNDS(n^1, INF) ---------------------------------------- (16) Obligation: Innermost TRS: Rules: rw(Val, c) -> Op(Val, rewrite(c)) rewrite(Op(x, y)) -> rw(x, y) rw(Op(x, y), c) -> rw[Let](Op(x, y), c, rewrite(x)) rewrite(Val) -> Val second(Op(x, y)) -> y isOp(Val) -> False isOp(Op(x, y)) -> True first(Val) -> Val first(Op(x, y)) -> x assrewrite(exp) -> rewrite(exp) rw[Let](Op(x, y), c, a1) -> rw[Let][Let](c, a1, rewrite(y)) rw[Let][Let](c, a1, b1) -> rw[Let][Let][Let](a1, b1, rewrite(c)) rw[Let][Let][Let](a1, b1, c1) -> rw(a1, Op(b1, c1)) Types: rw :: Val:Op -> Val:Op -> Val:Op Val :: Val:Op Op :: Val:Op -> Val:Op -> Val:Op rewrite :: Val:Op -> Val:Op rw[Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op second :: Val:Op -> Val:Op isOp :: Val:Op -> False:True False :: False:True True :: False:True first :: Val:Op -> Val:Op assrewrite :: Val:Op -> Val:Op rw[Let][Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op rw[Let][Let][Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op hole_Val:Op1_0 :: Val:Op hole_False:True2_0 :: False:True gen_Val:Op3_0 :: Nat -> Val:Op Lemmas: rewrite(gen_Val:Op3_0(n5_0)) -> gen_Val:Op3_0(n5_0), rt in Omega(1 + n5_0) Generator Equations: gen_Val:Op3_0(0) <=> Val gen_Val:Op3_0(+(x, 1)) <=> Op(Val, gen_Val:Op3_0(x)) The following defined symbols remain to be analysed: rw They will be analysed ascendingly in the following order: rw = rewrite