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), 200 ms] (2) CpxRelTRS (3) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (4) CpxRelTRS (5) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (6) typed CpxTrs (7) OrderProof [LOWER BOUND(ID), 0 ms] (8) typed CpxTrs (9) RewriteLemmaProof [LOWER BOUND(ID), 285 ms] (10) typed CpxTrs (11) RewriteLemmaProof [LOWER BOUND(ID), 90 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: mergesort(Cons(x', Cons(x, xs))) -> splitmerge(Cons(x', Cons(x, xs)), Nil, Nil) mergesort(Cons(x, Nil)) -> Cons(x, Nil) merge(Cons(x', xs'), Cons(x, xs)) -> merge[Ite](<=(x', x), Cons(x', xs'), Cons(x, xs)) merge(Cons(x, xs), Nil) -> Cons(x, xs) splitmerge(Cons(x, xs), xs1, xs2) -> splitmerge(xs, Cons(x, xs2), xs1) splitmerge(Nil, xs1, xs2) -> merge(mergesort(xs1), mergesort(xs2)) mergesort(Nil) -> Nil merge(Nil, xs2) -> xs2 notEmpty(Cons(x, xs)) -> True notEmpty(Nil) -> False goal(xs) -> mergesort(xs) The (relative) TRS S consists of the following rules: <=(S(x), S(y)) -> <=(x, y) <=(0, y) -> True <=(S(x), 0) -> False merge[Ite](False, xs1, Cons(x, xs)) -> Cons(x, merge(xs1, xs)) merge[Ite](True, Cons(x, xs), xs2) -> Cons(x, merge(xs, xs2)) 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: mergesort(Cons(x', Cons(x, xs))) -> splitmerge(Cons(x', Cons(x, xs)), Nil, Nil) mergesort(Cons(x, Nil)) -> Cons(x, Nil) merge(Cons(x', xs'), Cons(x, xs)) -> merge[Ite](<=(x', x), Cons(x', xs'), Cons(x, xs)) merge(Cons(x, xs), Nil) -> Cons(x, xs) splitmerge(Cons(x, xs), xs1, xs2) -> splitmerge(xs, Cons(x, xs2), xs1) splitmerge(Nil, xs1, xs2) -> merge(mergesort(xs1), mergesort(xs2)) mergesort(Nil) -> Nil merge(Nil, xs2) -> xs2 notEmpty(Cons(x, xs)) -> True notEmpty(Nil) -> False goal(xs) -> mergesort(xs) The (relative) TRS S consists of the following rules: <=(S(x), S(y)) -> <=(x, y) <=(0, y) -> True <=(S(x), 0) -> False merge[Ite](False, xs1, Cons(x, xs)) -> Cons(x, merge(xs1, xs)) merge[Ite](True, Cons(x, xs), xs2) -> Cons(x, merge(xs, xs2)) 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: mergesort(Cons(x', Cons(x, xs))) -> splitmerge(Cons(x', Cons(x, xs)), Nil, Nil) mergesort(Cons(x, Nil)) -> Cons(x, Nil) merge(Cons(x', xs'), Cons(x, xs)) -> merge[Ite](<=(x', x), Cons(x', xs'), Cons(x, xs)) merge(Cons(x, xs), Nil) -> Cons(x, xs) splitmerge(Cons(x, xs), xs1, xs2) -> splitmerge(xs, Cons(x, xs2), xs1) splitmerge(Nil, xs1, xs2) -> merge(mergesort(xs1), mergesort(xs2)) mergesort(Nil) -> Nil merge(Nil, xs2) -> xs2 notEmpty(Cons(x, xs)) -> True notEmpty(Nil) -> False goal(xs) -> mergesort(xs) The (relative) TRS S consists of the following rules: <=(S(x), S(y)) -> <=(x, y) <=(0', y) -> True <=(S(x), 0') -> False merge[Ite](False, xs1, Cons(x, xs)) -> Cons(x, merge(xs1, xs)) merge[Ite](True, Cons(x, xs), xs2) -> Cons(x, merge(xs, xs2)) Rewrite Strategy: INNERMOST ---------------------------------------- (5) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (6) Obligation: Innermost TRS: Rules: mergesort(Cons(x', Cons(x, xs))) -> splitmerge(Cons(x', Cons(x, xs)), Nil, Nil) mergesort(Cons(x, Nil)) -> Cons(x, Nil) merge(Cons(x', xs'), Cons(x, xs)) -> merge[Ite](<=(x', x), Cons(x', xs'), Cons(x, xs)) merge(Cons(x, xs), Nil) -> Cons(x, xs) splitmerge(Cons(x, xs), xs1, xs2) -> splitmerge(xs, Cons(x, xs2), xs1) splitmerge(Nil, xs1, xs2) -> merge(mergesort(xs1), mergesort(xs2)) mergesort(Nil) -> Nil merge(Nil, xs2) -> xs2 notEmpty(Cons(x, xs)) -> True notEmpty(Nil) -> False goal(xs) -> mergesort(xs) <=(S(x), S(y)) -> <=(x, y) <=(0', y) -> True <=(S(x), 0') -> False merge[Ite](False, xs1, Cons(x, xs)) -> Cons(x, merge(xs1, xs)) merge[Ite](True, Cons(x, xs), xs2) -> Cons(x, merge(xs, xs2)) Types: mergesort :: Cons:Nil -> Cons:Nil Cons :: S:0' -> Cons:Nil -> Cons:Nil splitmerge :: Cons:Nil -> Cons:Nil -> Cons:Nil -> Cons:Nil Nil :: Cons:Nil merge :: Cons:Nil -> Cons:Nil -> Cons:Nil merge[Ite] :: True:False -> Cons:Nil -> Cons:Nil -> Cons:Nil <= :: S:0' -> S:0' -> True:False notEmpty :: Cons:Nil -> True:False True :: True:False False :: True:False goal :: Cons:Nil -> Cons:Nil S :: S:0' -> S:0' 0' :: S:0' hole_Cons:Nil1_0 :: Cons:Nil hole_S:0'2_0 :: S:0' hole_True:False3_0 :: True:False gen_Cons:Nil4_0 :: Nat -> Cons:Nil gen_S:0'5_0 :: Nat -> S:0' ---------------------------------------- (7) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: mergesort, splitmerge, merge, <= They will be analysed ascendingly in the following order: mergesort = splitmerge merge < splitmerge <= < merge ---------------------------------------- (8) Obligation: Innermost TRS: Rules: mergesort(Cons(x', Cons(x, xs))) -> splitmerge(Cons(x', Cons(x, xs)), Nil, Nil) mergesort(Cons(x, Nil)) -> Cons(x, Nil) merge(Cons(x', xs'), Cons(x, xs)) -> merge[Ite](<=(x', x), Cons(x', xs'), Cons(x, xs)) merge(Cons(x, xs), Nil) -> Cons(x, xs) splitmerge(Cons(x, xs), xs1, xs2) -> splitmerge(xs, Cons(x, xs2), xs1) splitmerge(Nil, xs1, xs2) -> merge(mergesort(xs1), mergesort(xs2)) mergesort(Nil) -> Nil merge(Nil, xs2) -> xs2 notEmpty(Cons(x, xs)) -> True notEmpty(Nil) -> False goal(xs) -> mergesort(xs) <=(S(x), S(y)) -> <=(x, y) <=(0', y) -> True <=(S(x), 0') -> False merge[Ite](False, xs1, Cons(x, xs)) -> Cons(x, merge(xs1, xs)) merge[Ite](True, Cons(x, xs), xs2) -> Cons(x, merge(xs, xs2)) Types: mergesort :: Cons:Nil -> Cons:Nil Cons :: S:0' -> Cons:Nil -> Cons:Nil splitmerge :: Cons:Nil -> Cons:Nil -> Cons:Nil -> Cons:Nil Nil :: Cons:Nil merge :: Cons:Nil -> Cons:Nil -> Cons:Nil merge[Ite] :: True:False -> Cons:Nil -> Cons:Nil -> Cons:Nil <= :: S:0' -> S:0' -> True:False notEmpty :: Cons:Nil -> True:False True :: True:False False :: True:False goal :: Cons:Nil -> Cons:Nil S :: S:0' -> S:0' 0' :: S:0' hole_Cons:Nil1_0 :: Cons:Nil hole_S:0'2_0 :: S:0' hole_True:False3_0 :: True:False gen_Cons:Nil4_0 :: Nat -> Cons:Nil gen_S:0'5_0 :: Nat -> S:0' Generator Equations: gen_Cons:Nil4_0(0) <=> Nil gen_Cons:Nil4_0(+(x, 1)) <=> Cons(0', gen_Cons:Nil4_0(x)) gen_S:0'5_0(0) <=> 0' gen_S:0'5_0(+(x, 1)) <=> S(gen_S:0'5_0(x)) The following defined symbols remain to be analysed: <=, mergesort, splitmerge, merge They will be analysed ascendingly in the following order: mergesort = splitmerge merge < splitmerge <= < merge ---------------------------------------- (9) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: <=(gen_S:0'5_0(n7_0), gen_S:0'5_0(n7_0)) -> True, rt in Omega(0) Induction Base: <=(gen_S:0'5_0(0), gen_S:0'5_0(0)) ->_R^Omega(0) True Induction Step: <=(gen_S:0'5_0(+(n7_0, 1)), gen_S:0'5_0(+(n7_0, 1))) ->_R^Omega(0) <=(gen_S:0'5_0(n7_0), gen_S:0'5_0(n7_0)) ->_IH True We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (10) Obligation: Innermost TRS: Rules: mergesort(Cons(x', Cons(x, xs))) -> splitmerge(Cons(x', Cons(x, xs)), Nil, Nil) mergesort(Cons(x, Nil)) -> Cons(x, Nil) merge(Cons(x', xs'), Cons(x, xs)) -> merge[Ite](<=(x', x), Cons(x', xs'), Cons(x, xs)) merge(Cons(x, xs), Nil) -> Cons(x, xs) splitmerge(Cons(x, xs), xs1, xs2) -> splitmerge(xs, Cons(x, xs2), xs1) splitmerge(Nil, xs1, xs2) -> merge(mergesort(xs1), mergesort(xs2)) mergesort(Nil) -> Nil merge(Nil, xs2) -> xs2 notEmpty(Cons(x, xs)) -> True notEmpty(Nil) -> False goal(xs) -> mergesort(xs) <=(S(x), S(y)) -> <=(x, y) <=(0', y) -> True <=(S(x), 0') -> False merge[Ite](False, xs1, Cons(x, xs)) -> Cons(x, merge(xs1, xs)) merge[Ite](True, Cons(x, xs), xs2) -> Cons(x, merge(xs, xs2)) Types: mergesort :: Cons:Nil -> Cons:Nil Cons :: S:0' -> Cons:Nil -> Cons:Nil splitmerge :: Cons:Nil -> Cons:Nil -> Cons:Nil -> Cons:Nil Nil :: Cons:Nil merge :: Cons:Nil -> Cons:Nil -> Cons:Nil merge[Ite] :: True:False -> Cons:Nil -> Cons:Nil -> Cons:Nil <= :: S:0' -> S:0' -> True:False notEmpty :: Cons:Nil -> True:False True :: True:False False :: True:False goal :: Cons:Nil -> Cons:Nil S :: S:0' -> S:0' 0' :: S:0' hole_Cons:Nil1_0 :: Cons:Nil hole_S:0'2_0 :: S:0' hole_True:False3_0 :: True:False gen_Cons:Nil4_0 :: Nat -> Cons:Nil gen_S:0'5_0 :: Nat -> S:0' Lemmas: <=(gen_S:0'5_0(n7_0), gen_S:0'5_0(n7_0)) -> True, rt in Omega(0) Generator Equations: gen_Cons:Nil4_0(0) <=> Nil gen_Cons:Nil4_0(+(x, 1)) <=> Cons(0', gen_Cons:Nil4_0(x)) gen_S:0'5_0(0) <=> 0' gen_S:0'5_0(+(x, 1)) <=> S(gen_S:0'5_0(x)) The following defined symbols remain to be analysed: merge, mergesort, splitmerge They will be analysed ascendingly in the following order: mergesort = splitmerge merge < splitmerge ---------------------------------------- (11) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: merge(gen_Cons:Nil4_0(n258_0), gen_Cons:Nil4_0(1)) -> gen_Cons:Nil4_0(+(1, n258_0)), rt in Omega(1 + n258_0) Induction Base: merge(gen_Cons:Nil4_0(0), gen_Cons:Nil4_0(1)) ->_R^Omega(1) gen_Cons:Nil4_0(1) Induction Step: merge(gen_Cons:Nil4_0(+(n258_0, 1)), gen_Cons:Nil4_0(1)) ->_R^Omega(1) merge[Ite](<=(0', 0'), Cons(0', gen_Cons:Nil4_0(n258_0)), Cons(0', gen_Cons:Nil4_0(0))) ->_L^Omega(0) merge[Ite](True, Cons(0', gen_Cons:Nil4_0(n258_0)), Cons(0', gen_Cons:Nil4_0(0))) ->_R^Omega(0) Cons(0', merge(gen_Cons:Nil4_0(n258_0), Cons(0', gen_Cons:Nil4_0(0)))) ->_IH Cons(0', gen_Cons:Nil4_0(+(1, c259_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: mergesort(Cons(x', Cons(x, xs))) -> splitmerge(Cons(x', Cons(x, xs)), Nil, Nil) mergesort(Cons(x, Nil)) -> Cons(x, Nil) merge(Cons(x', xs'), Cons(x, xs)) -> merge[Ite](<=(x', x), Cons(x', xs'), Cons(x, xs)) merge(Cons(x, xs), Nil) -> Cons(x, xs) splitmerge(Cons(x, xs), xs1, xs2) -> splitmerge(xs, Cons(x, xs2), xs1) splitmerge(Nil, xs1, xs2) -> merge(mergesort(xs1), mergesort(xs2)) mergesort(Nil) -> Nil merge(Nil, xs2) -> xs2 notEmpty(Cons(x, xs)) -> True notEmpty(Nil) -> False goal(xs) -> mergesort(xs) <=(S(x), S(y)) -> <=(x, y) <=(0', y) -> True <=(S(x), 0') -> False merge[Ite](False, xs1, Cons(x, xs)) -> Cons(x, merge(xs1, xs)) merge[Ite](True, Cons(x, xs), xs2) -> Cons(x, merge(xs, xs2)) Types: mergesort :: Cons:Nil -> Cons:Nil Cons :: S:0' -> Cons:Nil -> Cons:Nil splitmerge :: Cons:Nil -> Cons:Nil -> Cons:Nil -> Cons:Nil Nil :: Cons:Nil merge :: Cons:Nil -> Cons:Nil -> Cons:Nil merge[Ite] :: True:False -> Cons:Nil -> Cons:Nil -> Cons:Nil <= :: S:0' -> S:0' -> True:False notEmpty :: Cons:Nil -> True:False True :: True:False False :: True:False goal :: Cons:Nil -> Cons:Nil S :: S:0' -> S:0' 0' :: S:0' hole_Cons:Nil1_0 :: Cons:Nil hole_S:0'2_0 :: S:0' hole_True:False3_0 :: True:False gen_Cons:Nil4_0 :: Nat -> Cons:Nil gen_S:0'5_0 :: Nat -> S:0' Lemmas: <=(gen_S:0'5_0(n7_0), gen_S:0'5_0(n7_0)) -> True, rt in Omega(0) Generator Equations: gen_Cons:Nil4_0(0) <=> Nil gen_Cons:Nil4_0(+(x, 1)) <=> Cons(0', gen_Cons:Nil4_0(x)) gen_S:0'5_0(0) <=> 0' gen_S:0'5_0(+(x, 1)) <=> S(gen_S:0'5_0(x)) The following defined symbols remain to be analysed: merge, mergesort, splitmerge They will be analysed ascendingly in the following order: mergesort = splitmerge merge < splitmerge ---------------------------------------- (14) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (15) BOUNDS(n^1, INF) ---------------------------------------- (16) Obligation: Innermost TRS: Rules: mergesort(Cons(x', Cons(x, xs))) -> splitmerge(Cons(x', Cons(x, xs)), Nil, Nil) mergesort(Cons(x, Nil)) -> Cons(x, Nil) merge(Cons(x', xs'), Cons(x, xs)) -> merge[Ite](<=(x', x), Cons(x', xs'), Cons(x, xs)) merge(Cons(x, xs), Nil) -> Cons(x, xs) splitmerge(Cons(x, xs), xs1, xs2) -> splitmerge(xs, Cons(x, xs2), xs1) splitmerge(Nil, xs1, xs2) -> merge(mergesort(xs1), mergesort(xs2)) mergesort(Nil) -> Nil merge(Nil, xs2) -> xs2 notEmpty(Cons(x, xs)) -> True notEmpty(Nil) -> False goal(xs) -> mergesort(xs) <=(S(x), S(y)) -> <=(x, y) <=(0', y) -> True <=(S(x), 0') -> False merge[Ite](False, xs1, Cons(x, xs)) -> Cons(x, merge(xs1, xs)) merge[Ite](True, Cons(x, xs), xs2) -> Cons(x, merge(xs, xs2)) Types: mergesort :: Cons:Nil -> Cons:Nil Cons :: S:0' -> Cons:Nil -> Cons:Nil splitmerge :: Cons:Nil -> Cons:Nil -> Cons:Nil -> Cons:Nil Nil :: Cons:Nil merge :: Cons:Nil -> Cons:Nil -> Cons:Nil merge[Ite] :: True:False -> Cons:Nil -> Cons:Nil -> Cons:Nil <= :: S:0' -> S:0' -> True:False notEmpty :: Cons:Nil -> True:False True :: True:False False :: True:False goal :: Cons:Nil -> Cons:Nil S :: S:0' -> S:0' 0' :: S:0' hole_Cons:Nil1_0 :: Cons:Nil hole_S:0'2_0 :: S:0' hole_True:False3_0 :: True:False gen_Cons:Nil4_0 :: Nat -> Cons:Nil gen_S:0'5_0 :: Nat -> S:0' Lemmas: <=(gen_S:0'5_0(n7_0), gen_S:0'5_0(n7_0)) -> True, rt in Omega(0) merge(gen_Cons:Nil4_0(n258_0), gen_Cons:Nil4_0(1)) -> gen_Cons:Nil4_0(+(1, n258_0)), rt in Omega(1 + n258_0) Generator Equations: gen_Cons:Nil4_0(0) <=> Nil gen_Cons:Nil4_0(+(x, 1)) <=> Cons(0', gen_Cons:Nil4_0(x)) gen_S:0'5_0(0) <=> 0' gen_S:0'5_0(+(x, 1)) <=> S(gen_S:0'5_0(x)) The following defined symbols remain to be analysed: splitmerge, mergesort They will be analysed ascendingly in the following order: mergesort = splitmerge