a__nats → cons(0, incr(nats))
a__pairs → cons(0, incr(odds))
a__odds → a__incr(a__pairs)
a__incr(cons(X, XS)) → cons(s(mark(X)), incr(XS))
a__head(cons(X, XS)) → mark(X)
a__tail(cons(X, XS)) → mark(XS)
mark(nats) → a__nats
mark(incr(X)) → a__incr(mark(X))
mark(pairs) → a__pairs
mark(odds) → a__odds
mark(head(X)) → a__head(mark(X))
mark(tail(X)) → a__tail(mark(X))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(0) → 0
mark(s(X)) → s(mark(X))
a__nats → nats
a__incr(X) → incr(X)
a__pairs → pairs
a__odds → odds
a__head(X) → head(X)
a__tail(X) → tail(X)
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
a__nats' → cons'(0', incr'(nats'))
a__pairs' → cons'(0', incr'(odds'))
a__odds' → a__incr'(a__pairs')
a__incr'(cons'(X, XS)) → cons'(s'(mark'(X)), incr'(XS))
a__head'(cons'(X, XS)) → mark'(X)
a__tail'(cons'(X, XS)) → mark'(XS)
mark'(nats') → a__nats'
mark'(incr'(X)) → a__incr'(mark'(X))
mark'(pairs') → a__pairs'
mark'(odds') → a__odds'
mark'(head'(X)) → a__head'(mark'(X))
mark'(tail'(X)) → a__tail'(mark'(X))
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
a__nats' → nats'
a__incr'(X) → incr'(X)
a__pairs' → pairs'
a__odds' → odds'
a__head'(X) → head'(X)
a__tail'(X) → tail'(X)
Infered types.
Rules:
a__nats' → cons'(0', incr'(nats'))
a__pairs' → cons'(0', incr'(odds'))
a__odds' → a__incr'(a__pairs')
a__incr'(cons'(X, XS)) → cons'(s'(mark'(X)), incr'(XS))
a__head'(cons'(X, XS)) → mark'(X)
a__tail'(cons'(X, XS)) → mark'(XS)
mark'(nats') → a__nats'
mark'(incr'(X)) → a__incr'(mark'(X))
mark'(pairs') → a__pairs'
mark'(odds') → a__odds'
mark'(head'(X)) → a__head'(mark'(X))
mark'(tail'(X)) → a__tail'(mark'(X))
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
a__nats' → nats'
a__incr'(X) → incr'(X)
a__pairs' → pairs'
a__odds' → odds'
a__head'(X) → head'(X)
a__tail'(X) → tail'(X)
Types:
a__nats' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
cons' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
0' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
incr' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
nats' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
a__pairs' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
odds' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
a__odds' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
a__incr' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
s' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
mark' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
a__head' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
a__tail' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
pairs' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
head' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
tail' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
_hole_0':nats':incr':cons':odds':s':pairs':head':tail'1 :: 0':nats':incr':cons':odds':s':pairs':head':tail'
_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2 :: Nat → 0':nats':incr':cons':odds':s':pairs':head':tail'
Heuristically decided to analyse the following defined symbols:
a__odds', a__incr', mark', a__head', a__tail'
They will be analysed ascendingly in the following order:
a__odds' = a__incr'
a__odds' = mark'
a__odds' = a__head'
a__odds' = a__tail'
a__incr' = mark'
a__incr' = a__head'
a__incr' = a__tail'
mark' = a__head'
mark' = a__tail'
a__head' = a__tail'
Rules:
a__nats' → cons'(0', incr'(nats'))
a__pairs' → cons'(0', incr'(odds'))
a__odds' → a__incr'(a__pairs')
a__incr'(cons'(X, XS)) → cons'(s'(mark'(X)), incr'(XS))
a__head'(cons'(X, XS)) → mark'(X)
a__tail'(cons'(X, XS)) → mark'(XS)
mark'(nats') → a__nats'
mark'(incr'(X)) → a__incr'(mark'(X))
mark'(pairs') → a__pairs'
mark'(odds') → a__odds'
mark'(head'(X)) → a__head'(mark'(X))
mark'(tail'(X)) → a__tail'(mark'(X))
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
a__nats' → nats'
a__incr'(X) → incr'(X)
a__pairs' → pairs'
a__odds' → odds'
a__head'(X) → head'(X)
a__tail'(X) → tail'(X)
Types:
a__nats' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
cons' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
0' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
incr' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
nats' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
a__pairs' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
odds' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
a__odds' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
a__incr' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
s' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
mark' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
a__head' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
a__tail' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
pairs' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
head' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
tail' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
_hole_0':nats':incr':cons':odds':s':pairs':head':tail'1 :: 0':nats':incr':cons':odds':s':pairs':head':tail'
_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2 :: Nat → 0':nats':incr':cons':odds':s':pairs':head':tail'
Generator Equations:
_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(0) ⇔ 0'
_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(+(x, 1)) ⇔ cons'(_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(x), 0')
The following defined symbols remain to be analysed:
a__incr', a__odds', mark', a__head', a__tail'
They will be analysed ascendingly in the following order:
a__odds' = a__incr'
a__odds' = mark'
a__odds' = a__head'
a__odds' = a__tail'
a__incr' = mark'
a__incr' = a__head'
a__incr' = a__tail'
mark' = a__head'
mark' = a__tail'
a__head' = a__tail'
Could not prove a rewrite lemma for the defined symbol a__incr'.
Rules:
a__nats' → cons'(0', incr'(nats'))
a__pairs' → cons'(0', incr'(odds'))
a__odds' → a__incr'(a__pairs')
a__incr'(cons'(X, XS)) → cons'(s'(mark'(X)), incr'(XS))
a__head'(cons'(X, XS)) → mark'(X)
a__tail'(cons'(X, XS)) → mark'(XS)
mark'(nats') → a__nats'
mark'(incr'(X)) → a__incr'(mark'(X))
mark'(pairs') → a__pairs'
mark'(odds') → a__odds'
mark'(head'(X)) → a__head'(mark'(X))
mark'(tail'(X)) → a__tail'(mark'(X))
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
a__nats' → nats'
a__incr'(X) → incr'(X)
a__pairs' → pairs'
a__odds' → odds'
a__head'(X) → head'(X)
a__tail'(X) → tail'(X)
Types:
a__nats' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
cons' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
0' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
incr' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
nats' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
a__pairs' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
odds' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
a__odds' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
a__incr' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
s' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
mark' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
a__head' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
a__tail' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
pairs' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
head' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
tail' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
_hole_0':nats':incr':cons':odds':s':pairs':head':tail'1 :: 0':nats':incr':cons':odds':s':pairs':head':tail'
_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2 :: Nat → 0':nats':incr':cons':odds':s':pairs':head':tail'
Generator Equations:
_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(0) ⇔ 0'
_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(+(x, 1)) ⇔ cons'(_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(x), 0')
The following defined symbols remain to be analysed:
mark', a__odds', a__head', a__tail'
They will be analysed ascendingly in the following order:
a__odds' = a__incr'
a__odds' = mark'
a__odds' = a__head'
a__odds' = a__tail'
a__incr' = mark'
a__incr' = a__head'
a__incr' = a__tail'
mark' = a__head'
mark' = a__tail'
a__head' = a__tail'
Proved the following rewrite lemma:
mark'(_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(_n35255)) → _gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(_n35255), rt ∈ Ω(1 + n35255)
Induction Base:
mark'(_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(0)) →RΩ(1)
0'
Induction Step:
mark'(_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(+(_$n35256, 1))) →RΩ(1)
cons'(mark'(_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(_$n35256)), 0') →IH
cons'(_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(_$n35256), 0')
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
a__nats' → cons'(0', incr'(nats'))
a__pairs' → cons'(0', incr'(odds'))
a__odds' → a__incr'(a__pairs')
a__incr'(cons'(X, XS)) → cons'(s'(mark'(X)), incr'(XS))
a__head'(cons'(X, XS)) → mark'(X)
a__tail'(cons'(X, XS)) → mark'(XS)
mark'(nats') → a__nats'
mark'(incr'(X)) → a__incr'(mark'(X))
mark'(pairs') → a__pairs'
mark'(odds') → a__odds'
mark'(head'(X)) → a__head'(mark'(X))
mark'(tail'(X)) → a__tail'(mark'(X))
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
a__nats' → nats'
a__incr'(X) → incr'(X)
a__pairs' → pairs'
a__odds' → odds'
a__head'(X) → head'(X)
a__tail'(X) → tail'(X)
Types:
a__nats' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
cons' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
0' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
incr' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
nats' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
a__pairs' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
odds' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
a__odds' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
a__incr' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
s' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
mark' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
a__head' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
a__tail' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
pairs' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
head' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
tail' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
_hole_0':nats':incr':cons':odds':s':pairs':head':tail'1 :: 0':nats':incr':cons':odds':s':pairs':head':tail'
_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2 :: Nat → 0':nats':incr':cons':odds':s':pairs':head':tail'
Lemmas:
mark'(_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(_n35255)) → _gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(_n35255), rt ∈ Ω(1 + n35255)
Generator Equations:
_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(0) ⇔ 0'
_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(+(x, 1)) ⇔ cons'(_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(x), 0')
The following defined symbols remain to be analysed:
a__odds', a__incr', a__head', a__tail'
They will be analysed ascendingly in the following order:
a__odds' = a__incr'
a__odds' = mark'
a__odds' = a__head'
a__odds' = a__tail'
a__incr' = mark'
a__incr' = a__head'
a__incr' = a__tail'
mark' = a__head'
mark' = a__tail'
a__head' = a__tail'
Could not prove a rewrite lemma for the defined symbol a__odds'.
Rules:
a__nats' → cons'(0', incr'(nats'))
a__pairs' → cons'(0', incr'(odds'))
a__odds' → a__incr'(a__pairs')
a__incr'(cons'(X, XS)) → cons'(s'(mark'(X)), incr'(XS))
a__head'(cons'(X, XS)) → mark'(X)
a__tail'(cons'(X, XS)) → mark'(XS)
mark'(nats') → a__nats'
mark'(incr'(X)) → a__incr'(mark'(X))
mark'(pairs') → a__pairs'
mark'(odds') → a__odds'
mark'(head'(X)) → a__head'(mark'(X))
mark'(tail'(X)) → a__tail'(mark'(X))
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
a__nats' → nats'
a__incr'(X) → incr'(X)
a__pairs' → pairs'
a__odds' → odds'
a__head'(X) → head'(X)
a__tail'(X) → tail'(X)
Types:
a__nats' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
cons' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
0' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
incr' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
nats' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
a__pairs' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
odds' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
a__odds' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
a__incr' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
s' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
mark' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
a__head' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
a__tail' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
pairs' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
head' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
tail' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
_hole_0':nats':incr':cons':odds':s':pairs':head':tail'1 :: 0':nats':incr':cons':odds':s':pairs':head':tail'
_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2 :: Nat → 0':nats':incr':cons':odds':s':pairs':head':tail'
Lemmas:
mark'(_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(_n35255)) → _gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(_n35255), rt ∈ Ω(1 + n35255)
Generator Equations:
_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(0) ⇔ 0'
_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(+(x, 1)) ⇔ cons'(_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(x), 0')
The following defined symbols remain to be analysed:
a__head', a__incr', a__tail'
They will be analysed ascendingly in the following order:
a__odds' = a__incr'
a__odds' = mark'
a__odds' = a__head'
a__odds' = a__tail'
a__incr' = mark'
a__incr' = a__head'
a__incr' = a__tail'
mark' = a__head'
mark' = a__tail'
a__head' = a__tail'
Could not prove a rewrite lemma for the defined symbol a__head'.
Rules:
a__nats' → cons'(0', incr'(nats'))
a__pairs' → cons'(0', incr'(odds'))
a__odds' → a__incr'(a__pairs')
a__incr'(cons'(X, XS)) → cons'(s'(mark'(X)), incr'(XS))
a__head'(cons'(X, XS)) → mark'(X)
a__tail'(cons'(X, XS)) → mark'(XS)
mark'(nats') → a__nats'
mark'(incr'(X)) → a__incr'(mark'(X))
mark'(pairs') → a__pairs'
mark'(odds') → a__odds'
mark'(head'(X)) → a__head'(mark'(X))
mark'(tail'(X)) → a__tail'(mark'(X))
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
a__nats' → nats'
a__incr'(X) → incr'(X)
a__pairs' → pairs'
a__odds' → odds'
a__head'(X) → head'(X)
a__tail'(X) → tail'(X)
Types:
a__nats' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
cons' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
0' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
incr' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
nats' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
a__pairs' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
odds' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
a__odds' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
a__incr' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
s' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
mark' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
a__head' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
a__tail' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
pairs' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
head' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
tail' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
_hole_0':nats':incr':cons':odds':s':pairs':head':tail'1 :: 0':nats':incr':cons':odds':s':pairs':head':tail'
_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2 :: Nat → 0':nats':incr':cons':odds':s':pairs':head':tail'
Lemmas:
mark'(_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(_n35255)) → _gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(_n35255), rt ∈ Ω(1 + n35255)
Generator Equations:
_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(0) ⇔ 0'
_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(+(x, 1)) ⇔ cons'(_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(x), 0')
The following defined symbols remain to be analysed:
a__tail', a__incr'
They will be analysed ascendingly in the following order:
a__odds' = a__incr'
a__odds' = mark'
a__odds' = a__head'
a__odds' = a__tail'
a__incr' = mark'
a__incr' = a__head'
a__incr' = a__tail'
mark' = a__head'
mark' = a__tail'
a__head' = a__tail'
Could not prove a rewrite lemma for the defined symbol a__tail'.
Rules:
a__nats' → cons'(0', incr'(nats'))
a__pairs' → cons'(0', incr'(odds'))
a__odds' → a__incr'(a__pairs')
a__incr'(cons'(X, XS)) → cons'(s'(mark'(X)), incr'(XS))
a__head'(cons'(X, XS)) → mark'(X)
a__tail'(cons'(X, XS)) → mark'(XS)
mark'(nats') → a__nats'
mark'(incr'(X)) → a__incr'(mark'(X))
mark'(pairs') → a__pairs'
mark'(odds') → a__odds'
mark'(head'(X)) → a__head'(mark'(X))
mark'(tail'(X)) → a__tail'(mark'(X))
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
a__nats' → nats'
a__incr'(X) → incr'(X)
a__pairs' → pairs'
a__odds' → odds'
a__head'(X) → head'(X)
a__tail'(X) → tail'(X)
Types:
a__nats' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
cons' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
0' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
incr' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
nats' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
a__pairs' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
odds' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
a__odds' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
a__incr' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
s' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
mark' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
a__head' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
a__tail' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
pairs' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
head' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
tail' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
_hole_0':nats':incr':cons':odds':s':pairs':head':tail'1 :: 0':nats':incr':cons':odds':s':pairs':head':tail'
_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2 :: Nat → 0':nats':incr':cons':odds':s':pairs':head':tail'
Lemmas:
mark'(_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(_n35255)) → _gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(_n35255), rt ∈ Ω(1 + n35255)
Generator Equations:
_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(0) ⇔ 0'
_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(+(x, 1)) ⇔ cons'(_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(x), 0')
The following defined symbols remain to be analysed:
a__incr'
They will be analysed ascendingly in the following order:
a__odds' = a__incr'
a__odds' = mark'
a__odds' = a__head'
a__odds' = a__tail'
a__incr' = mark'
a__incr' = a__head'
a__incr' = a__tail'
mark' = a__head'
mark' = a__tail'
a__head' = a__tail'
Could not prove a rewrite lemma for the defined symbol a__incr'.
Rules:
a__nats' → cons'(0', incr'(nats'))
a__pairs' → cons'(0', incr'(odds'))
a__odds' → a__incr'(a__pairs')
a__incr'(cons'(X, XS)) → cons'(s'(mark'(X)), incr'(XS))
a__head'(cons'(X, XS)) → mark'(X)
a__tail'(cons'(X, XS)) → mark'(XS)
mark'(nats') → a__nats'
mark'(incr'(X)) → a__incr'(mark'(X))
mark'(pairs') → a__pairs'
mark'(odds') → a__odds'
mark'(head'(X)) → a__head'(mark'(X))
mark'(tail'(X)) → a__tail'(mark'(X))
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
a__nats' → nats'
a__incr'(X) → incr'(X)
a__pairs' → pairs'
a__odds' → odds'
a__head'(X) → head'(X)
a__tail'(X) → tail'(X)
Types:
a__nats' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
cons' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
0' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
incr' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
nats' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
a__pairs' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
odds' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
a__odds' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
a__incr' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
s' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
mark' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
a__head' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
a__tail' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
pairs' :: 0':nats':incr':cons':odds':s':pairs':head':tail'
head' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
tail' :: 0':nats':incr':cons':odds':s':pairs':head':tail' → 0':nats':incr':cons':odds':s':pairs':head':tail'
_hole_0':nats':incr':cons':odds':s':pairs':head':tail'1 :: 0':nats':incr':cons':odds':s':pairs':head':tail'
_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2 :: Nat → 0':nats':incr':cons':odds':s':pairs':head':tail'
Lemmas:
mark'(_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(_n35255)) → _gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(_n35255), rt ∈ Ω(1 + n35255)
Generator Equations:
_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(0) ⇔ 0'
_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(+(x, 1)) ⇔ cons'(_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(x), 0')
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
mark'(_gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(_n35255)) → _gen_0':nats':incr':cons':odds':s':pairs':head':tail'2(_n35255), rt ∈ Ω(1 + n35255)