(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
a__2nd(cons1(X, cons(Y, Z))) → mark(Y)
a__2nd(cons(X, X1)) → a__2nd(cons1(mark(X), mark(X1)))
a__from(X) → cons(mark(X), from(s(X)))
mark(2nd(X)) → a__2nd(mark(X))
mark(from(X)) → a__from(mark(X))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(s(X)) → s(mark(X))
mark(cons1(X1, X2)) → cons1(mark(X1), mark(X2))
a__2nd(X) → 2nd(X)
a__from(X) → from(X)
Rewrite Strategy: INNERMOST
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
a__2nd(cons(X, 2nd(cons(X11014_0, X21015_0)))) →+ a__2nd(cons1(mark(X), a__2nd(cons(mark(X11014_0), X21015_0))))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0,1].
The pumping substitution is [X21015_0 / 2nd(cons(X11014_0, X21015_0))].
The result substitution is [X / mark(X11014_0)].
(2) BOUNDS(n^1, INF)
(3) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.
(4) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
a__2nd(cons1(X, cons(Y, Z))) → mark(Y)
a__2nd(cons(X, X1)) → a__2nd(cons1(mark(X), mark(X1)))
a__from(X) → cons(mark(X), from(s(X)))
mark(2nd(X)) → a__2nd(mark(X))
mark(from(X)) → a__from(mark(X))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(s(X)) → s(mark(X))
mark(cons1(X1, X2)) → cons1(mark(X1), mark(X2))
a__2nd(X) → 2nd(X)
a__from(X) → from(X)
S is empty.
Rewrite Strategy: INNERMOST
(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.
(6) Obligation:
Innermost TRS:
Rules:
a__2nd(cons1(X, cons(Y, Z))) → mark(Y)
a__2nd(cons(X, X1)) → a__2nd(cons1(mark(X), mark(X1)))
a__from(X) → cons(mark(X), from(s(X)))
mark(2nd(X)) → a__2nd(mark(X))
mark(from(X)) → a__from(mark(X))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(s(X)) → s(mark(X))
mark(cons1(X1, X2)) → cons1(mark(X1), mark(X2))
a__2nd(X) → 2nd(X)
a__from(X) → from(X)
Types:
a__2nd :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
cons1 :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
cons :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
mark :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
a__from :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
from :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
s :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
2nd :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
hole_cons:cons1:s:from:2nd1_0 :: cons:cons1:s:from:2nd
gen_cons:cons1:s:from:2nd2_0 :: Nat → cons:cons1:s:from:2nd
(7) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
a__2nd,
mark,
a__fromThey will be analysed ascendingly in the following order:
a__2nd = mark
a__2nd = a__from
mark = a__from
(8) Obligation:
Innermost TRS:
Rules:
a__2nd(
cons1(
X,
cons(
Y,
Z))) →
mark(
Y)
a__2nd(
cons(
X,
X1)) →
a__2nd(
cons1(
mark(
X),
mark(
X1)))
a__from(
X) →
cons(
mark(
X),
from(
s(
X)))
mark(
2nd(
X)) →
a__2nd(
mark(
X))
mark(
from(
X)) →
a__from(
mark(
X))
mark(
cons(
X1,
X2)) →
cons(
mark(
X1),
X2)
mark(
s(
X)) →
s(
mark(
X))
mark(
cons1(
X1,
X2)) →
cons1(
mark(
X1),
mark(
X2))
a__2nd(
X) →
2nd(
X)
a__from(
X) →
from(
X)
Types:
a__2nd :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
cons1 :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
cons :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
mark :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
a__from :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
from :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
s :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
2nd :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
hole_cons:cons1:s:from:2nd1_0 :: cons:cons1:s:from:2nd
gen_cons:cons1:s:from:2nd2_0 :: Nat → cons:cons1:s:from:2nd
Generator Equations:
gen_cons:cons1:s:from:2nd2_0(0) ⇔ hole_cons:cons1:s:from:2nd1_0
gen_cons:cons1:s:from:2nd2_0(+(x, 1)) ⇔ cons1(hole_cons:cons1:s:from:2nd1_0, gen_cons:cons1:s:from:2nd2_0(x))
The following defined symbols remain to be analysed:
mark, a__2nd, a__from
They will be analysed ascendingly in the following order:
a__2nd = mark
a__2nd = a__from
mark = a__from
(9) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol mark.
(10) Obligation:
Innermost TRS:
Rules:
a__2nd(
cons1(
X,
cons(
Y,
Z))) →
mark(
Y)
a__2nd(
cons(
X,
X1)) →
a__2nd(
cons1(
mark(
X),
mark(
X1)))
a__from(
X) →
cons(
mark(
X),
from(
s(
X)))
mark(
2nd(
X)) →
a__2nd(
mark(
X))
mark(
from(
X)) →
a__from(
mark(
X))
mark(
cons(
X1,
X2)) →
cons(
mark(
X1),
X2)
mark(
s(
X)) →
s(
mark(
X))
mark(
cons1(
X1,
X2)) →
cons1(
mark(
X1),
mark(
X2))
a__2nd(
X) →
2nd(
X)
a__from(
X) →
from(
X)
Types:
a__2nd :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
cons1 :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
cons :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
mark :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
a__from :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
from :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
s :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
2nd :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
hole_cons:cons1:s:from:2nd1_0 :: cons:cons1:s:from:2nd
gen_cons:cons1:s:from:2nd2_0 :: Nat → cons:cons1:s:from:2nd
Generator Equations:
gen_cons:cons1:s:from:2nd2_0(0) ⇔ hole_cons:cons1:s:from:2nd1_0
gen_cons:cons1:s:from:2nd2_0(+(x, 1)) ⇔ cons1(hole_cons:cons1:s:from:2nd1_0, gen_cons:cons1:s:from:2nd2_0(x))
The following defined symbols remain to be analysed:
a__2nd, a__from
They will be analysed ascendingly in the following order:
a__2nd = mark
a__2nd = a__from
mark = a__from
(11) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol a__2nd.
(12) Obligation:
Innermost TRS:
Rules:
a__2nd(
cons1(
X,
cons(
Y,
Z))) →
mark(
Y)
a__2nd(
cons(
X,
X1)) →
a__2nd(
cons1(
mark(
X),
mark(
X1)))
a__from(
X) →
cons(
mark(
X),
from(
s(
X)))
mark(
2nd(
X)) →
a__2nd(
mark(
X))
mark(
from(
X)) →
a__from(
mark(
X))
mark(
cons(
X1,
X2)) →
cons(
mark(
X1),
X2)
mark(
s(
X)) →
s(
mark(
X))
mark(
cons1(
X1,
X2)) →
cons1(
mark(
X1),
mark(
X2))
a__2nd(
X) →
2nd(
X)
a__from(
X) →
from(
X)
Types:
a__2nd :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
cons1 :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
cons :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
mark :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
a__from :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
from :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
s :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
2nd :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
hole_cons:cons1:s:from:2nd1_0 :: cons:cons1:s:from:2nd
gen_cons:cons1:s:from:2nd2_0 :: Nat → cons:cons1:s:from:2nd
Generator Equations:
gen_cons:cons1:s:from:2nd2_0(0) ⇔ hole_cons:cons1:s:from:2nd1_0
gen_cons:cons1:s:from:2nd2_0(+(x, 1)) ⇔ cons1(hole_cons:cons1:s:from:2nd1_0, gen_cons:cons1:s:from:2nd2_0(x))
The following defined symbols remain to be analysed:
a__from
They will be analysed ascendingly in the following order:
a__2nd = mark
a__2nd = a__from
mark = a__from
(13) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol a__from.
(14) Obligation:
Innermost TRS:
Rules:
a__2nd(
cons1(
X,
cons(
Y,
Z))) →
mark(
Y)
a__2nd(
cons(
X,
X1)) →
a__2nd(
cons1(
mark(
X),
mark(
X1)))
a__from(
X) →
cons(
mark(
X),
from(
s(
X)))
mark(
2nd(
X)) →
a__2nd(
mark(
X))
mark(
from(
X)) →
a__from(
mark(
X))
mark(
cons(
X1,
X2)) →
cons(
mark(
X1),
X2)
mark(
s(
X)) →
s(
mark(
X))
mark(
cons1(
X1,
X2)) →
cons1(
mark(
X1),
mark(
X2))
a__2nd(
X) →
2nd(
X)
a__from(
X) →
from(
X)
Types:
a__2nd :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
cons1 :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
cons :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
mark :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
a__from :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
from :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
s :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
2nd :: cons:cons1:s:from:2nd → cons:cons1:s:from:2nd
hole_cons:cons1:s:from:2nd1_0 :: cons:cons1:s:from:2nd
gen_cons:cons1:s:from:2nd2_0 :: Nat → cons:cons1:s:from:2nd
Generator Equations:
gen_cons:cons1:s:from:2nd2_0(0) ⇔ hole_cons:cons1:s:from:2nd1_0
gen_cons:cons1:s:from:2nd2_0(+(x, 1)) ⇔ cons1(hole_cons:cons1:s:from:2nd1_0, gen_cons:cons1:s:from:2nd2_0(x))
No more defined symbols left to analyse.