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 CpxTRS could be proven to be BOUNDS(n^1, INF). (0) CpxTRS (1) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (2) CpxTRS (3) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (4) typed CpxTrs (5) OrderProof [LOWER BOUND(ID), 7 ms] (6) typed CpxTrs (7) RewriteLemmaProof [LOWER BOUND(ID), 10.6 s] (8) BEST (9) proven lower bound (10) LowerBoundPropagationProof [FINISHED, 0 ms] (11) BOUNDS(n^1, INF) (12) typed CpxTrs ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(0, Z) -> rnil a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(0, Z) -> rnil a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) a__pi(X) -> a__2ndspos(mark(X), a__from(0)) a__plus(0, Y) -> mark(Y) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__times(0, Y) -> 0 a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) a__square(X) -> a__times(mark(X), mark(X)) mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) mark(square(X)) -> a__square(mark(X)) mark(0) -> 0 mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__from(X) -> from(X) a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__times(X1, X2) -> times(X1, X2) a__square(X) -> square(X) S is empty. Rewrite Strategy: INNERMOST ---------------------------------------- (1) RenamingProof (BOTH BOUNDS(ID, ID)) Renamed function symbols to avoid clashes with predefined symbol. ---------------------------------------- (2) Obligation: The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(0', Z) -> rnil a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(0', Z) -> rnil a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) a__pi(X) -> a__2ndspos(mark(X), a__from(0')) a__plus(0', Y) -> mark(Y) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__times(0', Y) -> 0' a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) a__square(X) -> a__times(mark(X), mark(X)) mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) mark(square(X)) -> a__square(mark(X)) mark(0') -> 0' mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__from(X) -> from(X) a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__times(X1, X2) -> times(X1, X2) a__square(X) -> square(X) S is empty. Rewrite Strategy: INNERMOST ---------------------------------------- (3) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (4) Obligation: Innermost TRS: Rules: a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(0', Z) -> rnil a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(0', Z) -> rnil a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) a__pi(X) -> a__2ndspos(mark(X), a__from(0')) a__plus(0', Y) -> mark(Y) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__times(0', Y) -> 0' a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) a__square(X) -> a__times(mark(X), mark(X)) mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) mark(square(X)) -> a__square(mark(X)) mark(0') -> 0' mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__from(X) -> from(X) a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__times(X1, X2) -> times(X1, X2) a__square(X) -> square(X) Types: a__from :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil cons :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil mark :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil from :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil s :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil a__2ndspos :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil 0' :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil rnil :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil rcons :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil posrecip :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil a__2ndsneg :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil negrecip :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil a__pi :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil a__plus :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil a__times :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil a__square :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil 2ndspos :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil 2ndsneg :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil pi :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil plus :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil times :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil square :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil nil :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil hole_s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil1_0 :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil gen_s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil2_0 :: Nat -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil ---------------------------------------- (5) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: a__from, mark, a__2ndspos, a__2ndsneg, a__pi, a__plus, a__times, a__square They will be analysed ascendingly in the following order: a__from = mark a__from = a__2ndspos a__from = a__2ndsneg a__from = a__pi a__from = a__plus a__from = a__times a__from = a__square mark = a__2ndspos mark = a__2ndsneg mark = a__pi mark = a__plus mark = a__times mark = a__square a__2ndspos = a__2ndsneg a__2ndspos = a__pi a__2ndspos = a__plus a__2ndspos = a__times a__2ndspos = a__square a__2ndsneg = a__pi a__2ndsneg = a__plus a__2ndsneg = a__times a__2ndsneg = a__square a__pi = a__plus a__pi = a__times a__pi = a__square a__plus = a__times a__plus = a__square a__times = a__square ---------------------------------------- (6) Obligation: Innermost TRS: Rules: a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(0', Z) -> rnil a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(0', Z) -> rnil a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) a__pi(X) -> a__2ndspos(mark(X), a__from(0')) a__plus(0', Y) -> mark(Y) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__times(0', Y) -> 0' a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) a__square(X) -> a__times(mark(X), mark(X)) mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) mark(square(X)) -> a__square(mark(X)) mark(0') -> 0' mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__from(X) -> from(X) a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__times(X1, X2) -> times(X1, X2) a__square(X) -> square(X) Types: a__from :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil cons :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil mark :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil from :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil s :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil a__2ndspos :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil 0' :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil rnil :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil rcons :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil posrecip :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil a__2ndsneg :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil negrecip :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil a__pi :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil a__plus :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil a__times :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil a__square :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil 2ndspos :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil 2ndsneg :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil pi :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil plus :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil times :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil square :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil nil :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil hole_s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil1_0 :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil gen_s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil2_0 :: Nat -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil Generator Equations: gen_s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil2_0(0) <=> 0' gen_s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil2_0(+(x, 1)) <=> cons(gen_s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil2_0(x), 0') The following defined symbols remain to be analysed: mark, a__from, a__2ndspos, a__2ndsneg, a__pi, a__plus, a__times, a__square They will be analysed ascendingly in the following order: a__from = mark a__from = a__2ndspos a__from = a__2ndsneg a__from = a__pi a__from = a__plus a__from = a__times a__from = a__square mark = a__2ndspos mark = a__2ndsneg mark = a__pi mark = a__plus mark = a__times mark = a__square a__2ndspos = a__2ndsneg a__2ndspos = a__pi a__2ndspos = a__plus a__2ndspos = a__times a__2ndspos = a__square a__2ndsneg = a__pi a__2ndsneg = a__plus a__2ndsneg = a__times a__2ndsneg = a__square a__pi = a__plus a__pi = a__times a__pi = a__square a__plus = a__times a__plus = a__square a__times = a__square ---------------------------------------- (7) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: mark(gen_s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil2_0(n4_0)) -> gen_s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil2_0(n4_0), rt in Omega(1 + n4_0) Induction Base: mark(gen_s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil2_0(0)) ->_R^Omega(1) 0' Induction Step: mark(gen_s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil2_0(+(n4_0, 1))) ->_R^Omega(1) cons(mark(gen_s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil2_0(n4_0)), 0') ->_IH cons(gen_s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil2_0(c5_0), 0') We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (8) Complex Obligation (BEST) ---------------------------------------- (9) Obligation: Proved the lower bound n^1 for the following obligation: Innermost TRS: Rules: a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(0', Z) -> rnil a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(0', Z) -> rnil a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) a__pi(X) -> a__2ndspos(mark(X), a__from(0')) a__plus(0', Y) -> mark(Y) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__times(0', Y) -> 0' a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) a__square(X) -> a__times(mark(X), mark(X)) mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) mark(square(X)) -> a__square(mark(X)) mark(0') -> 0' mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__from(X) -> from(X) a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__times(X1, X2) -> times(X1, X2) a__square(X) -> square(X) Types: a__from :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil cons :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil mark :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil from :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil s :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil a__2ndspos :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil 0' :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil rnil :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil rcons :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil posrecip :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil a__2ndsneg :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil negrecip :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil a__pi :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil a__plus :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil a__times :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil a__square :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil 2ndspos :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil 2ndsneg :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil pi :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil plus :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil times :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil square :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil nil :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil hole_s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil1_0 :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil gen_s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil2_0 :: Nat -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil Generator Equations: gen_s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil2_0(0) <=> 0' gen_s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil2_0(+(x, 1)) <=> cons(gen_s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil2_0(x), 0') The following defined symbols remain to be analysed: mark, a__from, a__2ndspos, a__2ndsneg, a__pi, a__plus, a__times, a__square They will be analysed ascendingly in the following order: a__from = mark a__from = a__2ndspos a__from = a__2ndsneg a__from = a__pi a__from = a__plus a__from = a__times a__from = a__square mark = a__2ndspos mark = a__2ndsneg mark = a__pi mark = a__plus mark = a__times mark = a__square a__2ndspos = a__2ndsneg a__2ndspos = a__pi a__2ndspos = a__plus a__2ndspos = a__times a__2ndspos = a__square a__2ndsneg = a__pi a__2ndsneg = a__plus a__2ndsneg = a__times a__2ndsneg = a__square a__pi = a__plus a__pi = a__times a__pi = a__square a__plus = a__times a__plus = a__square a__times = a__square ---------------------------------------- (10) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (11) BOUNDS(n^1, INF) ---------------------------------------- (12) Obligation: Innermost TRS: Rules: a__from(X) -> cons(mark(X), from(s(X))) a__2ndspos(0', Z) -> rnil a__2ndspos(s(N), cons(X, cons(Y, Z))) -> rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) a__2ndsneg(0', Z) -> rnil a__2ndsneg(s(N), cons(X, cons(Y, Z))) -> rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) a__pi(X) -> a__2ndspos(mark(X), a__from(0')) a__plus(0', Y) -> mark(Y) a__plus(s(X), Y) -> s(a__plus(mark(X), mark(Y))) a__times(0', Y) -> 0' a__times(s(X), Y) -> a__plus(mark(Y), a__times(mark(X), mark(Y))) a__square(X) -> a__times(mark(X), mark(X)) mark(from(X)) -> a__from(mark(X)) mark(2ndspos(X1, X2)) -> a__2ndspos(mark(X1), mark(X2)) mark(2ndsneg(X1, X2)) -> a__2ndsneg(mark(X1), mark(X2)) mark(pi(X)) -> a__pi(mark(X)) mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) mark(times(X1, X2)) -> a__times(mark(X1), mark(X2)) mark(square(X)) -> a__square(mark(X)) mark(0') -> 0' mark(s(X)) -> s(mark(X)) mark(posrecip(X)) -> posrecip(mark(X)) mark(negrecip(X)) -> negrecip(mark(X)) mark(nil) -> nil mark(cons(X1, X2)) -> cons(mark(X1), X2) mark(rnil) -> rnil mark(rcons(X1, X2)) -> rcons(mark(X1), mark(X2)) a__from(X) -> from(X) a__2ndspos(X1, X2) -> 2ndspos(X1, X2) a__2ndsneg(X1, X2) -> 2ndsneg(X1, X2) a__pi(X) -> pi(X) a__plus(X1, X2) -> plus(X1, X2) a__times(X1, X2) -> times(X1, X2) a__square(X) -> square(X) Types: a__from :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil cons :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil mark :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil from :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil s :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil a__2ndspos :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil 0' :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil rnil :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil rcons :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil posrecip :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil a__2ndsneg :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil negrecip :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil a__pi :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil a__plus :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil a__times :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil a__square :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil 2ndspos :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil 2ndsneg :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil pi :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil plus :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil times :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil square :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil nil :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil hole_s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil1_0 :: s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil gen_s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil2_0 :: Nat -> s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil Lemmas: mark(gen_s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil2_0(n4_0)) -> gen_s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil2_0(n4_0), rt in Omega(1 + n4_0) Generator Equations: gen_s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil2_0(0) <=> 0' gen_s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil2_0(+(x, 1)) <=> cons(gen_s:from:cons:0':rnil:posrecip:rcons:negrecip:2ndspos:2ndsneg:pi:plus:times:square:nil2_0(x), 0') The following defined symbols remain to be analysed: a__from, a__2ndspos, a__2ndsneg, a__pi, a__plus, a__times, a__square They will be analysed ascendingly in the following order: a__from = mark a__from = a__2ndspos a__from = a__2ndsneg a__from = a__pi a__from = a__plus a__from = a__times a__from = a__square mark = a__2ndspos mark = a__2ndsneg mark = a__pi mark = a__plus mark = a__times mark = a__square a__2ndspos = a__2ndsneg a__2ndspos = a__pi a__2ndspos = a__plus a__2ndspos = a__times a__2ndspos = a__square a__2ndsneg = a__pi a__2ndsneg = a__plus a__2ndsneg = a__times a__2ndsneg = a__square a__pi = a__plus a__pi = a__times a__pi = a__square a__plus = a__times a__plus = a__square a__times = a__square