a__incr(nil) → nil
a__incr(cons(X, L)) → cons(s(mark(X)), incr(L))
a__adx(nil) → nil
a__adx(cons(X, L)) → a__incr(cons(mark(X), adx(L)))
a__nats → a__adx(a__zeros)
a__zeros → cons(0, zeros)
a__head(cons(X, L)) → mark(X)
a__tail(cons(X, L)) → mark(L)
mark(incr(X)) → a__incr(mark(X))
mark(adx(X)) → a__adx(mark(X))
mark(nats) → a__nats
mark(zeros) → a__zeros
mark(head(X)) → a__head(mark(X))
mark(tail(X)) → a__tail(mark(X))
mark(nil) → nil
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(s(X)) → s(mark(X))
mark(0) → 0
a__incr(X) → incr(X)
a__adx(X) → adx(X)
a__nats → nats
a__zeros → zeros
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__incr'(nil') → nil'
a__incr'(cons'(X, L)) → cons'(s'(mark'(X)), incr'(L))
a__adx'(nil') → nil'
a__adx'(cons'(X, L)) → a__incr'(cons'(mark'(X), adx'(L)))
a__nats' → a__adx'(a__zeros')
a__zeros' → cons'(0', zeros')
a__head'(cons'(X, L)) → mark'(X)
a__tail'(cons'(X, L)) → mark'(L)
mark'(incr'(X)) → a__incr'(mark'(X))
mark'(adx'(X)) → a__adx'(mark'(X))
mark'(nats') → a__nats'
mark'(zeros') → a__zeros'
mark'(head'(X)) → a__head'(mark'(X))
mark'(tail'(X)) → a__tail'(mark'(X))
mark'(nil') → nil'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
a__incr'(X) → incr'(X)
a__adx'(X) → adx'(X)
a__nats' → nats'
a__zeros' → zeros'
a__head'(X) → head'(X)
a__tail'(X) → tail'(X)
Infered types.
Rules:
a__incr'(nil') → nil'
a__incr'(cons'(X, L)) → cons'(s'(mark'(X)), incr'(L))
a__adx'(nil') → nil'
a__adx'(cons'(X, L)) → a__incr'(cons'(mark'(X), adx'(L)))
a__nats' → a__adx'(a__zeros')
a__zeros' → cons'(0', zeros')
a__head'(cons'(X, L)) → mark'(X)
a__tail'(cons'(X, L)) → mark'(L)
mark'(incr'(X)) → a__incr'(mark'(X))
mark'(adx'(X)) → a__adx'(mark'(X))
mark'(nats') → a__nats'
mark'(zeros') → a__zeros'
mark'(head'(X)) → a__head'(mark'(X))
mark'(tail'(X)) → a__tail'(mark'(X))
mark'(nil') → nil'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
a__incr'(X) → incr'(X)
a__adx'(X) → adx'(X)
a__nats' → nats'
a__zeros' → zeros'
a__head'(X) → head'(X)
a__tail'(X) → tail'(X)
Types:
a__incr' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
nil' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
cons' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
s' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
mark' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
incr' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__adx' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
adx' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__nats' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__zeros' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
0' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
zeros' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__head' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__tail' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
nats' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
head' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
tail' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
_hole_nil':cons':s':incr':adx':0':zeros':nats':head':tail'1 :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2 :: Nat → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
Heuristically decided to analyse the following defined symbols:
a__incr', mark', a__adx', a__nats', a__head', a__tail'
They will be analysed ascendingly in the following order:
a__incr' = mark'
a__incr' = a__adx'
a__incr' = a__nats'
a__incr' = a__head'
a__incr' = a__tail'
mark' = a__adx'
mark' = a__nats'
mark' = a__head'
mark' = a__tail'
a__adx' = a__nats'
a__adx' = a__head'
a__adx' = a__tail'
a__nats' = a__head'
a__nats' = a__tail'
a__head' = a__tail'
Rules:
a__incr'(nil') → nil'
a__incr'(cons'(X, L)) → cons'(s'(mark'(X)), incr'(L))
a__adx'(nil') → nil'
a__adx'(cons'(X, L)) → a__incr'(cons'(mark'(X), adx'(L)))
a__nats' → a__adx'(a__zeros')
a__zeros' → cons'(0', zeros')
a__head'(cons'(X, L)) → mark'(X)
a__tail'(cons'(X, L)) → mark'(L)
mark'(incr'(X)) → a__incr'(mark'(X))
mark'(adx'(X)) → a__adx'(mark'(X))
mark'(nats') → a__nats'
mark'(zeros') → a__zeros'
mark'(head'(X)) → a__head'(mark'(X))
mark'(tail'(X)) → a__tail'(mark'(X))
mark'(nil') → nil'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
a__incr'(X) → incr'(X)
a__adx'(X) → adx'(X)
a__nats' → nats'
a__zeros' → zeros'
a__head'(X) → head'(X)
a__tail'(X) → tail'(X)
Types:
a__incr' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
nil' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
cons' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
s' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
mark' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
incr' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__adx' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
adx' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__nats' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__zeros' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
0' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
zeros' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__head' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__tail' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
nats' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
head' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
tail' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
_hole_nil':cons':s':incr':adx':0':zeros':nats':head':tail'1 :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2 :: Nat → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
Generator Equations:
_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(0) ⇔ nil'
_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(+(x, 1)) ⇔ cons'(_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(x), nil')
The following defined symbols remain to be analysed:
mark', a__incr', a__adx', a__nats', a__head', a__tail'
They will be analysed ascendingly in the following order:
a__incr' = mark'
a__incr' = a__adx'
a__incr' = a__nats'
a__incr' = a__head'
a__incr' = a__tail'
mark' = a__adx'
mark' = a__nats'
mark' = a__head'
mark' = a__tail'
a__adx' = a__nats'
a__adx' = a__head'
a__adx' = a__tail'
a__nats' = a__head'
a__nats' = a__tail'
a__head' = a__tail'
Proved the following rewrite lemma:
mark'(_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(_n4)) → _gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(_n4), rt ∈ Ω(1 + n4)
Induction Base:
mark'(_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(0)) →RΩ(1)
nil'
Induction Step:
mark'(_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(+(_$n5, 1))) →RΩ(1)
cons'(mark'(_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(_$n5)), nil') →IH
cons'(_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(_$n5), nil')
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
a__incr'(nil') → nil'
a__incr'(cons'(X, L)) → cons'(s'(mark'(X)), incr'(L))
a__adx'(nil') → nil'
a__adx'(cons'(X, L)) → a__incr'(cons'(mark'(X), adx'(L)))
a__nats' → a__adx'(a__zeros')
a__zeros' → cons'(0', zeros')
a__head'(cons'(X, L)) → mark'(X)
a__tail'(cons'(X, L)) → mark'(L)
mark'(incr'(X)) → a__incr'(mark'(X))
mark'(adx'(X)) → a__adx'(mark'(X))
mark'(nats') → a__nats'
mark'(zeros') → a__zeros'
mark'(head'(X)) → a__head'(mark'(X))
mark'(tail'(X)) → a__tail'(mark'(X))
mark'(nil') → nil'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
a__incr'(X) → incr'(X)
a__adx'(X) → adx'(X)
a__nats' → nats'
a__zeros' → zeros'
a__head'(X) → head'(X)
a__tail'(X) → tail'(X)
Types:
a__incr' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
nil' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
cons' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
s' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
mark' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
incr' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__adx' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
adx' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__nats' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__zeros' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
0' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
zeros' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__head' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__tail' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
nats' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
head' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
tail' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
_hole_nil':cons':s':incr':adx':0':zeros':nats':head':tail'1 :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2 :: Nat → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
Lemmas:
mark'(_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(_n4)) → _gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(_n4), rt ∈ Ω(1 + n4)
Generator Equations:
_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(0) ⇔ nil'
_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(+(x, 1)) ⇔ cons'(_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(x), nil')
The following defined symbols remain to be analysed:
a__incr', a__adx', a__nats', a__head', a__tail'
They will be analysed ascendingly in the following order:
a__incr' = mark'
a__incr' = a__adx'
a__incr' = a__nats'
a__incr' = a__head'
a__incr' = a__tail'
mark' = a__adx'
mark' = a__nats'
mark' = a__head'
mark' = a__tail'
a__adx' = a__nats'
a__adx' = a__head'
a__adx' = a__tail'
a__nats' = a__head'
a__nats' = a__tail'
a__head' = a__tail'
Could not prove a rewrite lemma for the defined symbol a__incr'.
Rules:
a__incr'(nil') → nil'
a__incr'(cons'(X, L)) → cons'(s'(mark'(X)), incr'(L))
a__adx'(nil') → nil'
a__adx'(cons'(X, L)) → a__incr'(cons'(mark'(X), adx'(L)))
a__nats' → a__adx'(a__zeros')
a__zeros' → cons'(0', zeros')
a__head'(cons'(X, L)) → mark'(X)
a__tail'(cons'(X, L)) → mark'(L)
mark'(incr'(X)) → a__incr'(mark'(X))
mark'(adx'(X)) → a__adx'(mark'(X))
mark'(nats') → a__nats'
mark'(zeros') → a__zeros'
mark'(head'(X)) → a__head'(mark'(X))
mark'(tail'(X)) → a__tail'(mark'(X))
mark'(nil') → nil'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
a__incr'(X) → incr'(X)
a__adx'(X) → adx'(X)
a__nats' → nats'
a__zeros' → zeros'
a__head'(X) → head'(X)
a__tail'(X) → tail'(X)
Types:
a__incr' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
nil' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
cons' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
s' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
mark' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
incr' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__adx' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
adx' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__nats' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__zeros' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
0' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
zeros' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__head' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__tail' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
nats' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
head' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
tail' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
_hole_nil':cons':s':incr':adx':0':zeros':nats':head':tail'1 :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2 :: Nat → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
Lemmas:
mark'(_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(_n4)) → _gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(_n4), rt ∈ Ω(1 + n4)
Generator Equations:
_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(0) ⇔ nil'
_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(+(x, 1)) ⇔ cons'(_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(x), nil')
The following defined symbols remain to be analysed:
a__adx', a__nats', a__head', a__tail'
They will be analysed ascendingly in the following order:
a__incr' = mark'
a__incr' = a__adx'
a__incr' = a__nats'
a__incr' = a__head'
a__incr' = a__tail'
mark' = a__adx'
mark' = a__nats'
mark' = a__head'
mark' = a__tail'
a__adx' = a__nats'
a__adx' = a__head'
a__adx' = a__tail'
a__nats' = a__head'
a__nats' = a__tail'
a__head' = a__tail'
Could not prove a rewrite lemma for the defined symbol a__adx'.
Rules:
a__incr'(nil') → nil'
a__incr'(cons'(X, L)) → cons'(s'(mark'(X)), incr'(L))
a__adx'(nil') → nil'
a__adx'(cons'(X, L)) → a__incr'(cons'(mark'(X), adx'(L)))
a__nats' → a__adx'(a__zeros')
a__zeros' → cons'(0', zeros')
a__head'(cons'(X, L)) → mark'(X)
a__tail'(cons'(X, L)) → mark'(L)
mark'(incr'(X)) → a__incr'(mark'(X))
mark'(adx'(X)) → a__adx'(mark'(X))
mark'(nats') → a__nats'
mark'(zeros') → a__zeros'
mark'(head'(X)) → a__head'(mark'(X))
mark'(tail'(X)) → a__tail'(mark'(X))
mark'(nil') → nil'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
a__incr'(X) → incr'(X)
a__adx'(X) → adx'(X)
a__nats' → nats'
a__zeros' → zeros'
a__head'(X) → head'(X)
a__tail'(X) → tail'(X)
Types:
a__incr' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
nil' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
cons' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
s' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
mark' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
incr' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__adx' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
adx' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__nats' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__zeros' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
0' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
zeros' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__head' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__tail' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
nats' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
head' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
tail' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
_hole_nil':cons':s':incr':adx':0':zeros':nats':head':tail'1 :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2 :: Nat → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
Lemmas:
mark'(_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(_n4)) → _gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(_n4), rt ∈ Ω(1 + n4)
Generator Equations:
_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(0) ⇔ nil'
_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(+(x, 1)) ⇔ cons'(_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(x), nil')
The following defined symbols remain to be analysed:
a__nats', a__head', a__tail'
They will be analysed ascendingly in the following order:
a__incr' = mark'
a__incr' = a__adx'
a__incr' = a__nats'
a__incr' = a__head'
a__incr' = a__tail'
mark' = a__adx'
mark' = a__nats'
mark' = a__head'
mark' = a__tail'
a__adx' = a__nats'
a__adx' = a__head'
a__adx' = a__tail'
a__nats' = a__head'
a__nats' = a__tail'
a__head' = a__tail'
Could not prove a rewrite lemma for the defined symbol a__nats'.
Rules:
a__incr'(nil') → nil'
a__incr'(cons'(X, L)) → cons'(s'(mark'(X)), incr'(L))
a__adx'(nil') → nil'
a__adx'(cons'(X, L)) → a__incr'(cons'(mark'(X), adx'(L)))
a__nats' → a__adx'(a__zeros')
a__zeros' → cons'(0', zeros')
a__head'(cons'(X, L)) → mark'(X)
a__tail'(cons'(X, L)) → mark'(L)
mark'(incr'(X)) → a__incr'(mark'(X))
mark'(adx'(X)) → a__adx'(mark'(X))
mark'(nats') → a__nats'
mark'(zeros') → a__zeros'
mark'(head'(X)) → a__head'(mark'(X))
mark'(tail'(X)) → a__tail'(mark'(X))
mark'(nil') → nil'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
a__incr'(X) → incr'(X)
a__adx'(X) → adx'(X)
a__nats' → nats'
a__zeros' → zeros'
a__head'(X) → head'(X)
a__tail'(X) → tail'(X)
Types:
a__incr' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
nil' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
cons' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
s' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
mark' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
incr' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__adx' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
adx' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__nats' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__zeros' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
0' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
zeros' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__head' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__tail' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
nats' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
head' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
tail' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
_hole_nil':cons':s':incr':adx':0':zeros':nats':head':tail'1 :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2 :: Nat → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
Lemmas:
mark'(_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(_n4)) → _gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(_n4), rt ∈ Ω(1 + n4)
Generator Equations:
_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(0) ⇔ nil'
_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(+(x, 1)) ⇔ cons'(_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(x), nil')
The following defined symbols remain to be analysed:
a__head', a__tail'
They will be analysed ascendingly in the following order:
a__incr' = mark'
a__incr' = a__adx'
a__incr' = a__nats'
a__incr' = a__head'
a__incr' = a__tail'
mark' = a__adx'
mark' = a__nats'
mark' = a__head'
mark' = a__tail'
a__adx' = a__nats'
a__adx' = a__head'
a__adx' = a__tail'
a__nats' = a__head'
a__nats' = a__tail'
a__head' = a__tail'
Could not prove a rewrite lemma for the defined symbol a__head'.
Rules:
a__incr'(nil') → nil'
a__incr'(cons'(X, L)) → cons'(s'(mark'(X)), incr'(L))
a__adx'(nil') → nil'
a__adx'(cons'(X, L)) → a__incr'(cons'(mark'(X), adx'(L)))
a__nats' → a__adx'(a__zeros')
a__zeros' → cons'(0', zeros')
a__head'(cons'(X, L)) → mark'(X)
a__tail'(cons'(X, L)) → mark'(L)
mark'(incr'(X)) → a__incr'(mark'(X))
mark'(adx'(X)) → a__adx'(mark'(X))
mark'(nats') → a__nats'
mark'(zeros') → a__zeros'
mark'(head'(X)) → a__head'(mark'(X))
mark'(tail'(X)) → a__tail'(mark'(X))
mark'(nil') → nil'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
a__incr'(X) → incr'(X)
a__adx'(X) → adx'(X)
a__nats' → nats'
a__zeros' → zeros'
a__head'(X) → head'(X)
a__tail'(X) → tail'(X)
Types:
a__incr' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
nil' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
cons' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
s' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
mark' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
incr' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__adx' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
adx' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__nats' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__zeros' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
0' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
zeros' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__head' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__tail' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
nats' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
head' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
tail' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
_hole_nil':cons':s':incr':adx':0':zeros':nats':head':tail'1 :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2 :: Nat → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
Lemmas:
mark'(_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(_n4)) → _gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(_n4), rt ∈ Ω(1 + n4)
Generator Equations:
_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(0) ⇔ nil'
_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(+(x, 1)) ⇔ cons'(_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(x), nil')
The following defined symbols remain to be analysed:
a__tail'
They will be analysed ascendingly in the following order:
a__incr' = mark'
a__incr' = a__adx'
a__incr' = a__nats'
a__incr' = a__head'
a__incr' = a__tail'
mark' = a__adx'
mark' = a__nats'
mark' = a__head'
mark' = a__tail'
a__adx' = a__nats'
a__adx' = a__head'
a__adx' = a__tail'
a__nats' = a__head'
a__nats' = a__tail'
a__head' = a__tail'
Could not prove a rewrite lemma for the defined symbol a__tail'.
Rules:
a__incr'(nil') → nil'
a__incr'(cons'(X, L)) → cons'(s'(mark'(X)), incr'(L))
a__adx'(nil') → nil'
a__adx'(cons'(X, L)) → a__incr'(cons'(mark'(X), adx'(L)))
a__nats' → a__adx'(a__zeros')
a__zeros' → cons'(0', zeros')
a__head'(cons'(X, L)) → mark'(X)
a__tail'(cons'(X, L)) → mark'(L)
mark'(incr'(X)) → a__incr'(mark'(X))
mark'(adx'(X)) → a__adx'(mark'(X))
mark'(nats') → a__nats'
mark'(zeros') → a__zeros'
mark'(head'(X)) → a__head'(mark'(X))
mark'(tail'(X)) → a__tail'(mark'(X))
mark'(nil') → nil'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
a__incr'(X) → incr'(X)
a__adx'(X) → adx'(X)
a__nats' → nats'
a__zeros' → zeros'
a__head'(X) → head'(X)
a__tail'(X) → tail'(X)
Types:
a__incr' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
nil' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
cons' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
s' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
mark' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
incr' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__adx' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
adx' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__nats' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__zeros' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
0' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
zeros' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__head' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
a__tail' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
nats' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
head' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
tail' :: nil':cons':s':incr':adx':0':zeros':nats':head':tail' → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
_hole_nil':cons':s':incr':adx':0':zeros':nats':head':tail'1 :: nil':cons':s':incr':adx':0':zeros':nats':head':tail'
_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2 :: Nat → nil':cons':s':incr':adx':0':zeros':nats':head':tail'
Lemmas:
mark'(_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(_n4)) → _gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(_n4), rt ∈ Ω(1 + n4)
Generator Equations:
_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(0) ⇔ nil'
_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(+(x, 1)) ⇔ cons'(_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(x), nil')
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
mark'(_gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(_n4)) → _gen_nil':cons':s':incr':adx':0':zeros':nats':head':tail'2(_n4), rt ∈ Ω(1 + n4)