incr(nil) → nil
incr(cons(X, L)) → cons(s(X), n__incr(activate(L)))
adx(nil) → nil
adx(cons(X, L)) → incr(cons(X, n__adx(activate(L))))
nats → adx(zeros)
zeros → cons(0, n__zeros)
head(cons(X, L)) → X
tail(cons(X, L)) → activate(L)
incr(X) → n__incr(X)
adx(X) → n__adx(X)
zeros → n__zeros
activate(n__incr(X)) → incr(activate(X))
activate(n__adx(X)) → adx(activate(X))
activate(n__zeros) → zeros
activate(X) → X
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
incr'(nil') → nil'
incr'(cons'(X, L)) → cons'(s'(X), n__incr'(activate'(L)))
adx'(nil') → nil'
adx'(cons'(X, L)) → incr'(cons'(X, n__adx'(activate'(L))))
nats' → adx'(zeros')
zeros' → cons'(0', n__zeros')
head'(cons'(X, L)) → X
tail'(cons'(X, L)) → activate'(L)
incr'(X) → n__incr'(X)
adx'(X) → n__adx'(X)
zeros' → n__zeros'
activate'(n__incr'(X)) → incr'(activate'(X))
activate'(n__adx'(X)) → adx'(activate'(X))
activate'(n__zeros') → zeros'
activate'(X) → X
Sliced the following arguments:
s'/0
Runtime Complexity TRS:
The TRS R consists of the following rules:
incr'(nil') → nil'
incr'(cons'(X, L)) → cons'(s', n__incr'(activate'(L)))
adx'(nil') → nil'
adx'(cons'(X, L)) → incr'(cons'(X, n__adx'(activate'(L))))
nats' → adx'(zeros')
zeros' → cons'(0', n__zeros')
head'(cons'(X, L)) → X
tail'(cons'(X, L)) → activate'(L)
incr'(X) → n__incr'(X)
adx'(X) → n__adx'(X)
zeros' → n__zeros'
activate'(n__incr'(X)) → incr'(activate'(X))
activate'(n__adx'(X)) → adx'(activate'(X))
activate'(n__zeros') → zeros'
activate'(X) → X
Infered types.
Rules:
incr'(nil') → nil'
incr'(cons'(X, L)) → cons'(s', n__incr'(activate'(L)))
adx'(nil') → nil'
adx'(cons'(X, L)) → incr'(cons'(X, n__adx'(activate'(L))))
nats' → adx'(zeros')
zeros' → cons'(0', n__zeros')
head'(cons'(X, L)) → X
tail'(cons'(X, L)) → activate'(L)
incr'(X) → n__incr'(X)
adx'(X) → n__adx'(X)
zeros' → n__zeros'
activate'(n__incr'(X)) → incr'(activate'(X))
activate'(n__adx'(X)) → adx'(activate'(X))
activate'(n__zeros') → zeros'
activate'(X) → X
Types:
incr' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
nil' :: nil':cons':n__incr':n__adx':n__zeros'
cons' :: s':0' → nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
s' :: s':0'
n__incr' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
activate' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
adx' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
n__adx' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
nats' :: nil':cons':n__incr':n__adx':n__zeros'
zeros' :: nil':cons':n__incr':n__adx':n__zeros'
0' :: s':0'
n__zeros' :: nil':cons':n__incr':n__adx':n__zeros'
head' :: nil':cons':n__incr':n__adx':n__zeros' → s':0'
tail' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
_hole_nil':cons':n__incr':n__adx':n__zeros'1 :: nil':cons':n__incr':n__adx':n__zeros'
_hole_s':0'2 :: s':0'
_gen_nil':cons':n__incr':n__adx':n__zeros'3 :: Nat → nil':cons':n__incr':n__adx':n__zeros'
Heuristically decided to analyse the following defined symbols:
incr', activate', adx'
They will be analysed ascendingly in the following order:
incr' = activate'
incr' = adx'
activate' = adx'
Rules:
incr'(nil') → nil'
incr'(cons'(X, L)) → cons'(s', n__incr'(activate'(L)))
adx'(nil') → nil'
adx'(cons'(X, L)) → incr'(cons'(X, n__adx'(activate'(L))))
nats' → adx'(zeros')
zeros' → cons'(0', n__zeros')
head'(cons'(X, L)) → X
tail'(cons'(X, L)) → activate'(L)
incr'(X) → n__incr'(X)
adx'(X) → n__adx'(X)
zeros' → n__zeros'
activate'(n__incr'(X)) → incr'(activate'(X))
activate'(n__adx'(X)) → adx'(activate'(X))
activate'(n__zeros') → zeros'
activate'(X) → X
Types:
incr' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
nil' :: nil':cons':n__incr':n__adx':n__zeros'
cons' :: s':0' → nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
s' :: s':0'
n__incr' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
activate' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
adx' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
n__adx' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
nats' :: nil':cons':n__incr':n__adx':n__zeros'
zeros' :: nil':cons':n__incr':n__adx':n__zeros'
0' :: s':0'
n__zeros' :: nil':cons':n__incr':n__adx':n__zeros'
head' :: nil':cons':n__incr':n__adx':n__zeros' → s':0'
tail' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
_hole_nil':cons':n__incr':n__adx':n__zeros'1 :: nil':cons':n__incr':n__adx':n__zeros'
_hole_s':0'2 :: s':0'
_gen_nil':cons':n__incr':n__adx':n__zeros'3 :: Nat → nil':cons':n__incr':n__adx':n__zeros'
Generator Equations:
_gen_nil':cons':n__incr':n__adx':n__zeros'3(0) ⇔ nil'
_gen_nil':cons':n__incr':n__adx':n__zeros'3(+(x, 1)) ⇔ cons'(s', _gen_nil':cons':n__incr':n__adx':n__zeros'3(x))
The following defined symbols remain to be analysed:
activate', incr', adx'
They will be analysed ascendingly in the following order:
incr' = activate'
incr' = adx'
activate' = adx'
Could not prove a rewrite lemma for the defined symbol activate'.
Rules:
incr'(nil') → nil'
incr'(cons'(X, L)) → cons'(s', n__incr'(activate'(L)))
adx'(nil') → nil'
adx'(cons'(X, L)) → incr'(cons'(X, n__adx'(activate'(L))))
nats' → adx'(zeros')
zeros' → cons'(0', n__zeros')
head'(cons'(X, L)) → X
tail'(cons'(X, L)) → activate'(L)
incr'(X) → n__incr'(X)
adx'(X) → n__adx'(X)
zeros' → n__zeros'
activate'(n__incr'(X)) → incr'(activate'(X))
activate'(n__adx'(X)) → adx'(activate'(X))
activate'(n__zeros') → zeros'
activate'(X) → X
Types:
incr' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
nil' :: nil':cons':n__incr':n__adx':n__zeros'
cons' :: s':0' → nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
s' :: s':0'
n__incr' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
activate' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
adx' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
n__adx' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
nats' :: nil':cons':n__incr':n__adx':n__zeros'
zeros' :: nil':cons':n__incr':n__adx':n__zeros'
0' :: s':0'
n__zeros' :: nil':cons':n__incr':n__adx':n__zeros'
head' :: nil':cons':n__incr':n__adx':n__zeros' → s':0'
tail' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
_hole_nil':cons':n__incr':n__adx':n__zeros'1 :: nil':cons':n__incr':n__adx':n__zeros'
_hole_s':0'2 :: s':0'
_gen_nil':cons':n__incr':n__adx':n__zeros'3 :: Nat → nil':cons':n__incr':n__adx':n__zeros'
Generator Equations:
_gen_nil':cons':n__incr':n__adx':n__zeros'3(0) ⇔ nil'
_gen_nil':cons':n__incr':n__adx':n__zeros'3(+(x, 1)) ⇔ cons'(s', _gen_nil':cons':n__incr':n__adx':n__zeros'3(x))
The following defined symbols remain to be analysed:
incr', adx'
They will be analysed ascendingly in the following order:
incr' = activate'
incr' = adx'
activate' = adx'
Could not prove a rewrite lemma for the defined symbol incr'.
Rules:
incr'(nil') → nil'
incr'(cons'(X, L)) → cons'(s', n__incr'(activate'(L)))
adx'(nil') → nil'
adx'(cons'(X, L)) → incr'(cons'(X, n__adx'(activate'(L))))
nats' → adx'(zeros')
zeros' → cons'(0', n__zeros')
head'(cons'(X, L)) → X
tail'(cons'(X, L)) → activate'(L)
incr'(X) → n__incr'(X)
adx'(X) → n__adx'(X)
zeros' → n__zeros'
activate'(n__incr'(X)) → incr'(activate'(X))
activate'(n__adx'(X)) → adx'(activate'(X))
activate'(n__zeros') → zeros'
activate'(X) → X
Types:
incr' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
nil' :: nil':cons':n__incr':n__adx':n__zeros'
cons' :: s':0' → nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
s' :: s':0'
n__incr' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
activate' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
adx' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
n__adx' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
nats' :: nil':cons':n__incr':n__adx':n__zeros'
zeros' :: nil':cons':n__incr':n__adx':n__zeros'
0' :: s':0'
n__zeros' :: nil':cons':n__incr':n__adx':n__zeros'
head' :: nil':cons':n__incr':n__adx':n__zeros' → s':0'
tail' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
_hole_nil':cons':n__incr':n__adx':n__zeros'1 :: nil':cons':n__incr':n__adx':n__zeros'
_hole_s':0'2 :: s':0'
_gen_nil':cons':n__incr':n__adx':n__zeros'3 :: Nat → nil':cons':n__incr':n__adx':n__zeros'
Generator Equations:
_gen_nil':cons':n__incr':n__adx':n__zeros'3(0) ⇔ nil'
_gen_nil':cons':n__incr':n__adx':n__zeros'3(+(x, 1)) ⇔ cons'(s', _gen_nil':cons':n__incr':n__adx':n__zeros'3(x))
The following defined symbols remain to be analysed:
adx'
They will be analysed ascendingly in the following order:
incr' = activate'
incr' = adx'
activate' = adx'
Proved the following rewrite lemma:
adx'(_gen_nil':cons':n__incr':n__adx':n__zeros'3(_n107)) → _*4, rt ∈ Ω(n107)
Induction Base:
adx'(_gen_nil':cons':n__incr':n__adx':n__zeros'3(0))
Induction Step:
adx'(_gen_nil':cons':n__incr':n__adx':n__zeros'3(+(_$n108, 1))) →RΩ(1)
incr'(cons'(s', n__adx'(activate'(_gen_nil':cons':n__incr':n__adx':n__zeros'3(_$n108))))) →RΩ(1)
incr'(cons'(s', n__adx'(_gen_nil':cons':n__incr':n__adx':n__zeros'3(_$n108)))) →RΩ(1)
cons'(s', n__incr'(activate'(n__adx'(_gen_nil':cons':n__incr':n__adx':n__zeros'3(_$n108))))) →RΩ(1)
cons'(s', n__incr'(adx'(activate'(_gen_nil':cons':n__incr':n__adx':n__zeros'3(_$n108))))) →RΩ(1)
cons'(s', n__incr'(adx'(_gen_nil':cons':n__incr':n__adx':n__zeros'3(_$n108)))) →IH
cons'(s', n__incr'(_*4))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
incr'(nil') → nil'
incr'(cons'(X, L)) → cons'(s', n__incr'(activate'(L)))
adx'(nil') → nil'
adx'(cons'(X, L)) → incr'(cons'(X, n__adx'(activate'(L))))
nats' → adx'(zeros')
zeros' → cons'(0', n__zeros')
head'(cons'(X, L)) → X
tail'(cons'(X, L)) → activate'(L)
incr'(X) → n__incr'(X)
adx'(X) → n__adx'(X)
zeros' → n__zeros'
activate'(n__incr'(X)) → incr'(activate'(X))
activate'(n__adx'(X)) → adx'(activate'(X))
activate'(n__zeros') → zeros'
activate'(X) → X
Types:
incr' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
nil' :: nil':cons':n__incr':n__adx':n__zeros'
cons' :: s':0' → nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
s' :: s':0'
n__incr' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
activate' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
adx' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
n__adx' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
nats' :: nil':cons':n__incr':n__adx':n__zeros'
zeros' :: nil':cons':n__incr':n__adx':n__zeros'
0' :: s':0'
n__zeros' :: nil':cons':n__incr':n__adx':n__zeros'
head' :: nil':cons':n__incr':n__adx':n__zeros' → s':0'
tail' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
_hole_nil':cons':n__incr':n__adx':n__zeros'1 :: nil':cons':n__incr':n__adx':n__zeros'
_hole_s':0'2 :: s':0'
_gen_nil':cons':n__incr':n__adx':n__zeros'3 :: Nat → nil':cons':n__incr':n__adx':n__zeros'
Lemmas:
adx'(_gen_nil':cons':n__incr':n__adx':n__zeros'3(_n107)) → _*4, rt ∈ Ω(n107)
Generator Equations:
_gen_nil':cons':n__incr':n__adx':n__zeros'3(0) ⇔ nil'
_gen_nil':cons':n__incr':n__adx':n__zeros'3(+(x, 1)) ⇔ cons'(s', _gen_nil':cons':n__incr':n__adx':n__zeros'3(x))
The following defined symbols remain to be analysed:
activate', incr'
They will be analysed ascendingly in the following order:
incr' = activate'
incr' = adx'
activate' = adx'
Could not prove a rewrite lemma for the defined symbol activate'.
Rules:
incr'(nil') → nil'
incr'(cons'(X, L)) → cons'(s', n__incr'(activate'(L)))
adx'(nil') → nil'
adx'(cons'(X, L)) → incr'(cons'(X, n__adx'(activate'(L))))
nats' → adx'(zeros')
zeros' → cons'(0', n__zeros')
head'(cons'(X, L)) → X
tail'(cons'(X, L)) → activate'(L)
incr'(X) → n__incr'(X)
adx'(X) → n__adx'(X)
zeros' → n__zeros'
activate'(n__incr'(X)) → incr'(activate'(X))
activate'(n__adx'(X)) → adx'(activate'(X))
activate'(n__zeros') → zeros'
activate'(X) → X
Types:
incr' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
nil' :: nil':cons':n__incr':n__adx':n__zeros'
cons' :: s':0' → nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
s' :: s':0'
n__incr' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
activate' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
adx' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
n__adx' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
nats' :: nil':cons':n__incr':n__adx':n__zeros'
zeros' :: nil':cons':n__incr':n__adx':n__zeros'
0' :: s':0'
n__zeros' :: nil':cons':n__incr':n__adx':n__zeros'
head' :: nil':cons':n__incr':n__adx':n__zeros' → s':0'
tail' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
_hole_nil':cons':n__incr':n__adx':n__zeros'1 :: nil':cons':n__incr':n__adx':n__zeros'
_hole_s':0'2 :: s':0'
_gen_nil':cons':n__incr':n__adx':n__zeros'3 :: Nat → nil':cons':n__incr':n__adx':n__zeros'
Lemmas:
adx'(_gen_nil':cons':n__incr':n__adx':n__zeros'3(_n107)) → _*4, rt ∈ Ω(n107)
Generator Equations:
_gen_nil':cons':n__incr':n__adx':n__zeros'3(0) ⇔ nil'
_gen_nil':cons':n__incr':n__adx':n__zeros'3(+(x, 1)) ⇔ cons'(s', _gen_nil':cons':n__incr':n__adx':n__zeros'3(x))
The following defined symbols remain to be analysed:
incr'
They will be analysed ascendingly in the following order:
incr' = activate'
incr' = adx'
activate' = adx'
Could not prove a rewrite lemma for the defined symbol incr'.
Rules:
incr'(nil') → nil'
incr'(cons'(X, L)) → cons'(s', n__incr'(activate'(L)))
adx'(nil') → nil'
adx'(cons'(X, L)) → incr'(cons'(X, n__adx'(activate'(L))))
nats' → adx'(zeros')
zeros' → cons'(0', n__zeros')
head'(cons'(X, L)) → X
tail'(cons'(X, L)) → activate'(L)
incr'(X) → n__incr'(X)
adx'(X) → n__adx'(X)
zeros' → n__zeros'
activate'(n__incr'(X)) → incr'(activate'(X))
activate'(n__adx'(X)) → adx'(activate'(X))
activate'(n__zeros') → zeros'
activate'(X) → X
Types:
incr' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
nil' :: nil':cons':n__incr':n__adx':n__zeros'
cons' :: s':0' → nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
s' :: s':0'
n__incr' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
activate' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
adx' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
n__adx' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
nats' :: nil':cons':n__incr':n__adx':n__zeros'
zeros' :: nil':cons':n__incr':n__adx':n__zeros'
0' :: s':0'
n__zeros' :: nil':cons':n__incr':n__adx':n__zeros'
head' :: nil':cons':n__incr':n__adx':n__zeros' → s':0'
tail' :: nil':cons':n__incr':n__adx':n__zeros' → nil':cons':n__incr':n__adx':n__zeros'
_hole_nil':cons':n__incr':n__adx':n__zeros'1 :: nil':cons':n__incr':n__adx':n__zeros'
_hole_s':0'2 :: s':0'
_gen_nil':cons':n__incr':n__adx':n__zeros'3 :: Nat → nil':cons':n__incr':n__adx':n__zeros'
Lemmas:
adx'(_gen_nil':cons':n__incr':n__adx':n__zeros'3(_n107)) → _*4, rt ∈ Ω(n107)
Generator Equations:
_gen_nil':cons':n__incr':n__adx':n__zeros'3(0) ⇔ nil'
_gen_nil':cons':n__incr':n__adx':n__zeros'3(+(x, 1)) ⇔ cons'(s', _gen_nil':cons':n__incr':n__adx':n__zeros'3(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
adx'(_gen_nil':cons':n__incr':n__adx':n__zeros'3(_n107)) → _*4, rt ∈ Ω(n107)