sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(n__s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(X) → X
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
sel'(s'(X), cons'(Y, Z)) → sel'(X, activate'(Z))
sel'(0', cons'(X, Z)) → X
first'(0', Z) → nil'
first'(s'(X), cons'(Y, Z)) → cons'(Y, n__first'(X, activate'(Z)))
from'(X) → cons'(X, n__from'(n__s'(X)))
sel1'(s'(X), cons'(Y, Z)) → sel1'(X, activate'(Z))
sel1'(0', cons'(X, Z)) → quote'(X)
first1'(0', Z) → nil1'
first1'(s'(X), cons'(Y, Z)) → cons1'(quote'(Y), first1'(X, activate'(Z)))
quote'(n__0') → 01'
quote1'(n__cons'(X, Z)) → cons1'(quote'(activate'(X)), quote1'(activate'(Z)))
quote1'(n__nil') → nil1'
quote'(n__s'(X)) → s1'(quote'(activate'(X)))
quote'(n__sel'(X, Z)) → sel1'(activate'(X), activate'(Z))
quote1'(n__first'(X, Z)) → first1'(activate'(X), activate'(Z))
unquote'(01') → 0'
unquote'(s1'(X)) → s'(unquote'(X))
unquote1'(nil1') → nil'
unquote1'(cons1'(X, Z)) → fcons'(unquote'(X), unquote1'(Z))
fcons'(X, Z) → cons'(X, Z)
first'(X1, X2) → n__first'(X1, X2)
from'(X) → n__from'(X)
s'(X) → n__s'(X)
0' → n__0'
cons'(X1, X2) → n__cons'(X1, X2)
nil' → n__nil'
sel'(X1, X2) → n__sel'(X1, X2)
activate'(n__first'(X1, X2)) → first'(activate'(X1), activate'(X2))
activate'(n__from'(X)) → from'(activate'(X))
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__0') → 0'
activate'(n__cons'(X1, X2)) → cons'(activate'(X1), X2)
activate'(n__nil') → nil'
activate'(n__sel'(X1, X2)) → sel'(activate'(X1), activate'(X2))
activate'(X) → X
Infered types.
Rules:
sel'(s'(X), cons'(Y, Z)) → sel'(X, activate'(Z))
sel'(0', cons'(X, Z)) → X
first'(0', Z) → nil'
first'(s'(X), cons'(Y, Z)) → cons'(Y, n__first'(X, activate'(Z)))
from'(X) → cons'(X, n__from'(n__s'(X)))
sel1'(s'(X), cons'(Y, Z)) → sel1'(X, activate'(Z))
sel1'(0', cons'(X, Z)) → quote'(X)
first1'(0', Z) → nil1'
first1'(s'(X), cons'(Y, Z)) → cons1'(quote'(Y), first1'(X, activate'(Z)))
quote'(n__0') → 01'
quote1'(n__cons'(X, Z)) → cons1'(quote'(activate'(X)), quote1'(activate'(Z)))
quote1'(n__nil') → nil1'
quote'(n__s'(X)) → s1'(quote'(activate'(X)))
quote'(n__sel'(X, Z)) → sel1'(activate'(X), activate'(Z))
quote1'(n__first'(X, Z)) → first1'(activate'(X), activate'(Z))
unquote'(01') → 0'
unquote'(s1'(X)) → s'(unquote'(X))
unquote1'(nil1') → nil'
unquote1'(cons1'(X, Z)) → fcons'(unquote'(X), unquote1'(Z))
fcons'(X, Z) → cons'(X, Z)
first'(X1, X2) → n__first'(X1, X2)
from'(X) → n__from'(X)
s'(X) → n__s'(X)
0' → n__0'
cons'(X1, X2) → n__cons'(X1, X2)
nil' → n__nil'
sel'(X1, X2) → n__sel'(X1, X2)
activate'(n__first'(X1, X2)) → first'(activate'(X1), activate'(X2))
activate'(n__from'(X)) → from'(activate'(X))
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__0') → 0'
activate'(n__cons'(X1, X2)) → cons'(activate'(X1), X2)
activate'(n__nil') → nil'
activate'(n__sel'(X1, X2)) → sel'(activate'(X1), activate'(X2))
activate'(X) → X
Types:
sel' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
s' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
cons' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
activate' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
0' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
first' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
nil' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__first' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
from' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__from' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__s' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
sel1' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → 01':s1'
quote' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → 01':s1'
first1' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → nil1':cons1'
nil1' :: nil1':cons1'
cons1' :: 01':s1' → nil1':cons1' → nil1':cons1'
n__0' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
01' :: 01':s1'
quote1' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → nil1':cons1'
n__cons' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__nil' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
s1' :: 01':s1' → 01':s1'
n__sel' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
unquote' :: 01':s1' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
unquote1' :: nil1':cons1' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
fcons' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
_hole_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'1 :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
_hole_01':s1'2 :: 01':s1'
_hole_nil1':cons1'3 :: nil1':cons1'
_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4 :: Nat → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
_gen_01':s1'5 :: Nat → 01':s1'
_gen_nil1':cons1'6 :: Nat → nil1':cons1'
Heuristically decided to analyse the following defined symbols:
sel', activate', sel1', quote', first1', quote1', unquote', unquote1'
They will be analysed ascendingly in the following order:
sel' = activate'
activate' < sel1'
activate' < quote'
activate' < first1'
activate' < quote1'
sel1' = quote'
quote' < first1'
quote' < quote1'
first1' < quote1'
unquote' < unquote1'
Rules:
sel'(s'(X), cons'(Y, Z)) → sel'(X, activate'(Z))
sel'(0', cons'(X, Z)) → X
first'(0', Z) → nil'
first'(s'(X), cons'(Y, Z)) → cons'(Y, n__first'(X, activate'(Z)))
from'(X) → cons'(X, n__from'(n__s'(X)))
sel1'(s'(X), cons'(Y, Z)) → sel1'(X, activate'(Z))
sel1'(0', cons'(X, Z)) → quote'(X)
first1'(0', Z) → nil1'
first1'(s'(X), cons'(Y, Z)) → cons1'(quote'(Y), first1'(X, activate'(Z)))
quote'(n__0') → 01'
quote1'(n__cons'(X, Z)) → cons1'(quote'(activate'(X)), quote1'(activate'(Z)))
quote1'(n__nil') → nil1'
quote'(n__s'(X)) → s1'(quote'(activate'(X)))
quote'(n__sel'(X, Z)) → sel1'(activate'(X), activate'(Z))
quote1'(n__first'(X, Z)) → first1'(activate'(X), activate'(Z))
unquote'(01') → 0'
unquote'(s1'(X)) → s'(unquote'(X))
unquote1'(nil1') → nil'
unquote1'(cons1'(X, Z)) → fcons'(unquote'(X), unquote1'(Z))
fcons'(X, Z) → cons'(X, Z)
first'(X1, X2) → n__first'(X1, X2)
from'(X) → n__from'(X)
s'(X) → n__s'(X)
0' → n__0'
cons'(X1, X2) → n__cons'(X1, X2)
nil' → n__nil'
sel'(X1, X2) → n__sel'(X1, X2)
activate'(n__first'(X1, X2)) → first'(activate'(X1), activate'(X2))
activate'(n__from'(X)) → from'(activate'(X))
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__0') → 0'
activate'(n__cons'(X1, X2)) → cons'(activate'(X1), X2)
activate'(n__nil') → nil'
activate'(n__sel'(X1, X2)) → sel'(activate'(X1), activate'(X2))
activate'(X) → X
Types:
sel' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
s' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
cons' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
activate' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
0' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
first' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
nil' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__first' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
from' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__from' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__s' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
sel1' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → 01':s1'
quote' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → 01':s1'
first1' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → nil1':cons1'
nil1' :: nil1':cons1'
cons1' :: 01':s1' → nil1':cons1' → nil1':cons1'
n__0' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
01' :: 01':s1'
quote1' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → nil1':cons1'
n__cons' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__nil' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
s1' :: 01':s1' → 01':s1'
n__sel' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
unquote' :: 01':s1' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
unquote1' :: nil1':cons1' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
fcons' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
_hole_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'1 :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
_hole_01':s1'2 :: 01':s1'
_hole_nil1':cons1'3 :: nil1':cons1'
_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4 :: Nat → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
_gen_01':s1'5 :: Nat → 01':s1'
_gen_nil1':cons1'6 :: Nat → nil1':cons1'
Generator Equations:
_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(0) ⇔ n__0'
_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(+(x, 1)) ⇔ n__first'(n__0', _gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(x))
_gen_01':s1'5(0) ⇔ 01'
_gen_01':s1'5(+(x, 1)) ⇔ s1'(_gen_01':s1'5(x))
_gen_nil1':cons1'6(0) ⇔ nil1'
_gen_nil1':cons1'6(+(x, 1)) ⇔ cons1'(01', _gen_nil1':cons1'6(x))
The following defined symbols remain to be analysed:
unquote', sel', activate', sel1', quote', first1', quote1', unquote1'
They will be analysed ascendingly in the following order:
sel' = activate'
activate' < sel1'
activate' < quote'
activate' < first1'
activate' < quote1'
sel1' = quote'
quote' < first1'
quote' < quote1'
first1' < quote1'
unquote' < unquote1'
Proved the following rewrite lemma:
unquote'(_gen_01':s1'5(+(1, _n8))) → _*7, rt ∈ Ω(n8)
Induction Base:
unquote'(_gen_01':s1'5(+(1, 0)))
Induction Step:
unquote'(_gen_01':s1'5(+(1, +(_$n9, 1)))) →RΩ(1)
s'(unquote'(_gen_01':s1'5(+(1, _$n9)))) →IH
s'(_*7)
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
sel'(s'(X), cons'(Y, Z)) → sel'(X, activate'(Z))
sel'(0', cons'(X, Z)) → X
first'(0', Z) → nil'
first'(s'(X), cons'(Y, Z)) → cons'(Y, n__first'(X, activate'(Z)))
from'(X) → cons'(X, n__from'(n__s'(X)))
sel1'(s'(X), cons'(Y, Z)) → sel1'(X, activate'(Z))
sel1'(0', cons'(X, Z)) → quote'(X)
first1'(0', Z) → nil1'
first1'(s'(X), cons'(Y, Z)) → cons1'(quote'(Y), first1'(X, activate'(Z)))
quote'(n__0') → 01'
quote1'(n__cons'(X, Z)) → cons1'(quote'(activate'(X)), quote1'(activate'(Z)))
quote1'(n__nil') → nil1'
quote'(n__s'(X)) → s1'(quote'(activate'(X)))
quote'(n__sel'(X, Z)) → sel1'(activate'(X), activate'(Z))
quote1'(n__first'(X, Z)) → first1'(activate'(X), activate'(Z))
unquote'(01') → 0'
unquote'(s1'(X)) → s'(unquote'(X))
unquote1'(nil1') → nil'
unquote1'(cons1'(X, Z)) → fcons'(unquote'(X), unquote1'(Z))
fcons'(X, Z) → cons'(X, Z)
first'(X1, X2) → n__first'(X1, X2)
from'(X) → n__from'(X)
s'(X) → n__s'(X)
0' → n__0'
cons'(X1, X2) → n__cons'(X1, X2)
nil' → n__nil'
sel'(X1, X2) → n__sel'(X1, X2)
activate'(n__first'(X1, X2)) → first'(activate'(X1), activate'(X2))
activate'(n__from'(X)) → from'(activate'(X))
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__0') → 0'
activate'(n__cons'(X1, X2)) → cons'(activate'(X1), X2)
activate'(n__nil') → nil'
activate'(n__sel'(X1, X2)) → sel'(activate'(X1), activate'(X2))
activate'(X) → X
Types:
sel' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
s' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
cons' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
activate' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
0' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
first' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
nil' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__first' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
from' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__from' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__s' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
sel1' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → 01':s1'
quote' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → 01':s1'
first1' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → nil1':cons1'
nil1' :: nil1':cons1'
cons1' :: 01':s1' → nil1':cons1' → nil1':cons1'
n__0' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
01' :: 01':s1'
quote1' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → nil1':cons1'
n__cons' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__nil' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
s1' :: 01':s1' → 01':s1'
n__sel' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
unquote' :: 01':s1' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
unquote1' :: nil1':cons1' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
fcons' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
_hole_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'1 :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
_hole_01':s1'2 :: 01':s1'
_hole_nil1':cons1'3 :: nil1':cons1'
_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4 :: Nat → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
_gen_01':s1'5 :: Nat → 01':s1'
_gen_nil1':cons1'6 :: Nat → nil1':cons1'
Lemmas:
unquote'(_gen_01':s1'5(+(1, _n8))) → _*7, rt ∈ Ω(n8)
Generator Equations:
_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(0) ⇔ n__0'
_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(+(x, 1)) ⇔ n__first'(n__0', _gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(x))
_gen_01':s1'5(0) ⇔ 01'
_gen_01':s1'5(+(x, 1)) ⇔ s1'(_gen_01':s1'5(x))
_gen_nil1':cons1'6(0) ⇔ nil1'
_gen_nil1':cons1'6(+(x, 1)) ⇔ cons1'(01', _gen_nil1':cons1'6(x))
The following defined symbols remain to be analysed:
unquote1', sel', activate', sel1', quote', first1', quote1'
They will be analysed ascendingly in the following order:
sel' = activate'
activate' < sel1'
activate' < quote'
activate' < first1'
activate' < quote1'
sel1' = quote'
quote' < first1'
quote' < quote1'
first1' < quote1'
Proved the following rewrite lemma:
unquote1'(_gen_nil1':cons1'6(_n2342)) → _*7, rt ∈ Ω(n2342)
Induction Base:
unquote1'(_gen_nil1':cons1'6(0))
Induction Step:
unquote1'(_gen_nil1':cons1'6(+(_$n2343, 1))) →RΩ(1)
fcons'(unquote'(01'), unquote1'(_gen_nil1':cons1'6(_$n2343))) →RΩ(1)
fcons'(0', unquote1'(_gen_nil1':cons1'6(_$n2343))) →RΩ(1)
fcons'(n__0', unquote1'(_gen_nil1':cons1'6(_$n2343))) →IH
fcons'(n__0', _*7)
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
sel'(s'(X), cons'(Y, Z)) → sel'(X, activate'(Z))
sel'(0', cons'(X, Z)) → X
first'(0', Z) → nil'
first'(s'(X), cons'(Y, Z)) → cons'(Y, n__first'(X, activate'(Z)))
from'(X) → cons'(X, n__from'(n__s'(X)))
sel1'(s'(X), cons'(Y, Z)) → sel1'(X, activate'(Z))
sel1'(0', cons'(X, Z)) → quote'(X)
first1'(0', Z) → nil1'
first1'(s'(X), cons'(Y, Z)) → cons1'(quote'(Y), first1'(X, activate'(Z)))
quote'(n__0') → 01'
quote1'(n__cons'(X, Z)) → cons1'(quote'(activate'(X)), quote1'(activate'(Z)))
quote1'(n__nil') → nil1'
quote'(n__s'(X)) → s1'(quote'(activate'(X)))
quote'(n__sel'(X, Z)) → sel1'(activate'(X), activate'(Z))
quote1'(n__first'(X, Z)) → first1'(activate'(X), activate'(Z))
unquote'(01') → 0'
unquote'(s1'(X)) → s'(unquote'(X))
unquote1'(nil1') → nil'
unquote1'(cons1'(X, Z)) → fcons'(unquote'(X), unquote1'(Z))
fcons'(X, Z) → cons'(X, Z)
first'(X1, X2) → n__first'(X1, X2)
from'(X) → n__from'(X)
s'(X) → n__s'(X)
0' → n__0'
cons'(X1, X2) → n__cons'(X1, X2)
nil' → n__nil'
sel'(X1, X2) → n__sel'(X1, X2)
activate'(n__first'(X1, X2)) → first'(activate'(X1), activate'(X2))
activate'(n__from'(X)) → from'(activate'(X))
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__0') → 0'
activate'(n__cons'(X1, X2)) → cons'(activate'(X1), X2)
activate'(n__nil') → nil'
activate'(n__sel'(X1, X2)) → sel'(activate'(X1), activate'(X2))
activate'(X) → X
Types:
sel' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
s' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
cons' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
activate' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
0' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
first' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
nil' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__first' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
from' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__from' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__s' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
sel1' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → 01':s1'
quote' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → 01':s1'
first1' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → nil1':cons1'
nil1' :: nil1':cons1'
cons1' :: 01':s1' → nil1':cons1' → nil1':cons1'
n__0' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
01' :: 01':s1'
quote1' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → nil1':cons1'
n__cons' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__nil' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
s1' :: 01':s1' → 01':s1'
n__sel' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
unquote' :: 01':s1' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
unquote1' :: nil1':cons1' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
fcons' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
_hole_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'1 :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
_hole_01':s1'2 :: 01':s1'
_hole_nil1':cons1'3 :: nil1':cons1'
_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4 :: Nat → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
_gen_01':s1'5 :: Nat → 01':s1'
_gen_nil1':cons1'6 :: Nat → nil1':cons1'
Lemmas:
unquote'(_gen_01':s1'5(+(1, _n8))) → _*7, rt ∈ Ω(n8)
unquote1'(_gen_nil1':cons1'6(_n2342)) → _*7, rt ∈ Ω(n2342)
Generator Equations:
_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(0) ⇔ n__0'
_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(+(x, 1)) ⇔ n__first'(n__0', _gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(x))
_gen_01':s1'5(0) ⇔ 01'
_gen_01':s1'5(+(x, 1)) ⇔ s1'(_gen_01':s1'5(x))
_gen_nil1':cons1'6(0) ⇔ nil1'
_gen_nil1':cons1'6(+(x, 1)) ⇔ cons1'(01', _gen_nil1':cons1'6(x))
The following defined symbols remain to be analysed:
activate', sel', sel1', quote', first1', quote1'
They will be analysed ascendingly in the following order:
sel' = activate'
activate' < sel1'
activate' < quote'
activate' < first1'
activate' < quote1'
sel1' = quote'
quote' < first1'
quote' < quote1'
first1' < quote1'
Proved the following rewrite lemma:
activate'(_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(_n24720)) → _gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(_n24720), rt ∈ Ω(1 + n24720)
Induction Base:
activate'(_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(0)) →RΩ(1)
_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(0)
Induction Step:
activate'(_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(+(_$n24721, 1))) →RΩ(1)
first'(activate'(n__0'), activate'(_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(_$n24721))) →RΩ(1)
first'(n__0', activate'(_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(_$n24721))) →IH
first'(n__0', _gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(_$n24721)) →RΩ(1)
n__first'(n__0', _gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(_$n24721))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
sel'(s'(X), cons'(Y, Z)) → sel'(X, activate'(Z))
sel'(0', cons'(X, Z)) → X
first'(0', Z) → nil'
first'(s'(X), cons'(Y, Z)) → cons'(Y, n__first'(X, activate'(Z)))
from'(X) → cons'(X, n__from'(n__s'(X)))
sel1'(s'(X), cons'(Y, Z)) → sel1'(X, activate'(Z))
sel1'(0', cons'(X, Z)) → quote'(X)
first1'(0', Z) → nil1'
first1'(s'(X), cons'(Y, Z)) → cons1'(quote'(Y), first1'(X, activate'(Z)))
quote'(n__0') → 01'
quote1'(n__cons'(X, Z)) → cons1'(quote'(activate'(X)), quote1'(activate'(Z)))
quote1'(n__nil') → nil1'
quote'(n__s'(X)) → s1'(quote'(activate'(X)))
quote'(n__sel'(X, Z)) → sel1'(activate'(X), activate'(Z))
quote1'(n__first'(X, Z)) → first1'(activate'(X), activate'(Z))
unquote'(01') → 0'
unquote'(s1'(X)) → s'(unquote'(X))
unquote1'(nil1') → nil'
unquote1'(cons1'(X, Z)) → fcons'(unquote'(X), unquote1'(Z))
fcons'(X, Z) → cons'(X, Z)
first'(X1, X2) → n__first'(X1, X2)
from'(X) → n__from'(X)
s'(X) → n__s'(X)
0' → n__0'
cons'(X1, X2) → n__cons'(X1, X2)
nil' → n__nil'
sel'(X1, X2) → n__sel'(X1, X2)
activate'(n__first'(X1, X2)) → first'(activate'(X1), activate'(X2))
activate'(n__from'(X)) → from'(activate'(X))
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__0') → 0'
activate'(n__cons'(X1, X2)) → cons'(activate'(X1), X2)
activate'(n__nil') → nil'
activate'(n__sel'(X1, X2)) → sel'(activate'(X1), activate'(X2))
activate'(X) → X
Types:
sel' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
s' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
cons' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
activate' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
0' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
first' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
nil' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__first' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
from' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__from' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__s' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
sel1' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → 01':s1'
quote' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → 01':s1'
first1' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → nil1':cons1'
nil1' :: nil1':cons1'
cons1' :: 01':s1' → nil1':cons1' → nil1':cons1'
n__0' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
01' :: 01':s1'
quote1' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → nil1':cons1'
n__cons' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__nil' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
s1' :: 01':s1' → 01':s1'
n__sel' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
unquote' :: 01':s1' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
unquote1' :: nil1':cons1' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
fcons' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
_hole_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'1 :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
_hole_01':s1'2 :: 01':s1'
_hole_nil1':cons1'3 :: nil1':cons1'
_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4 :: Nat → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
_gen_01':s1'5 :: Nat → 01':s1'
_gen_nil1':cons1'6 :: Nat → nil1':cons1'
Lemmas:
unquote'(_gen_01':s1'5(+(1, _n8))) → _*7, rt ∈ Ω(n8)
unquote1'(_gen_nil1':cons1'6(_n2342)) → _*7, rt ∈ Ω(n2342)
activate'(_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(_n24720)) → _gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(_n24720), rt ∈ Ω(1 + n24720)
Generator Equations:
_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(0) ⇔ n__0'
_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(+(x, 1)) ⇔ n__first'(n__0', _gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(x))
_gen_01':s1'5(0) ⇔ 01'
_gen_01':s1'5(+(x, 1)) ⇔ s1'(_gen_01':s1'5(x))
_gen_nil1':cons1'6(0) ⇔ nil1'
_gen_nil1':cons1'6(+(x, 1)) ⇔ cons1'(01', _gen_nil1':cons1'6(x))
The following defined symbols remain to be analysed:
sel', sel1', quote', first1', quote1'
They will be analysed ascendingly in the following order:
sel' = activate'
activate' < sel1'
activate' < quote'
activate' < first1'
activate' < quote1'
sel1' = quote'
quote' < first1'
quote' < quote1'
first1' < quote1'
Could not prove a rewrite lemma for the defined symbol sel'.
Rules:
sel'(s'(X), cons'(Y, Z)) → sel'(X, activate'(Z))
sel'(0', cons'(X, Z)) → X
first'(0', Z) → nil'
first'(s'(X), cons'(Y, Z)) → cons'(Y, n__first'(X, activate'(Z)))
from'(X) → cons'(X, n__from'(n__s'(X)))
sel1'(s'(X), cons'(Y, Z)) → sel1'(X, activate'(Z))
sel1'(0', cons'(X, Z)) → quote'(X)
first1'(0', Z) → nil1'
first1'(s'(X), cons'(Y, Z)) → cons1'(quote'(Y), first1'(X, activate'(Z)))
quote'(n__0') → 01'
quote1'(n__cons'(X, Z)) → cons1'(quote'(activate'(X)), quote1'(activate'(Z)))
quote1'(n__nil') → nil1'
quote'(n__s'(X)) → s1'(quote'(activate'(X)))
quote'(n__sel'(X, Z)) → sel1'(activate'(X), activate'(Z))
quote1'(n__first'(X, Z)) → first1'(activate'(X), activate'(Z))
unquote'(01') → 0'
unquote'(s1'(X)) → s'(unquote'(X))
unquote1'(nil1') → nil'
unquote1'(cons1'(X, Z)) → fcons'(unquote'(X), unquote1'(Z))
fcons'(X, Z) → cons'(X, Z)
first'(X1, X2) → n__first'(X1, X2)
from'(X) → n__from'(X)
s'(X) → n__s'(X)
0' → n__0'
cons'(X1, X2) → n__cons'(X1, X2)
nil' → n__nil'
sel'(X1, X2) → n__sel'(X1, X2)
activate'(n__first'(X1, X2)) → first'(activate'(X1), activate'(X2))
activate'(n__from'(X)) → from'(activate'(X))
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__0') → 0'
activate'(n__cons'(X1, X2)) → cons'(activate'(X1), X2)
activate'(n__nil') → nil'
activate'(n__sel'(X1, X2)) → sel'(activate'(X1), activate'(X2))
activate'(X) → X
Types:
sel' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
s' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
cons' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
activate' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
0' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
first' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
nil' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__first' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
from' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__from' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__s' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
sel1' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → 01':s1'
quote' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → 01':s1'
first1' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → nil1':cons1'
nil1' :: nil1':cons1'
cons1' :: 01':s1' → nil1':cons1' → nil1':cons1'
n__0' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
01' :: 01':s1'
quote1' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → nil1':cons1'
n__cons' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__nil' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
s1' :: 01':s1' → 01':s1'
n__sel' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
unquote' :: 01':s1' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
unquote1' :: nil1':cons1' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
fcons' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
_hole_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'1 :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
_hole_01':s1'2 :: 01':s1'
_hole_nil1':cons1'3 :: nil1':cons1'
_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4 :: Nat → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
_gen_01':s1'5 :: Nat → 01':s1'
_gen_nil1':cons1'6 :: Nat → nil1':cons1'
Lemmas:
unquote'(_gen_01':s1'5(+(1, _n8))) → _*7, rt ∈ Ω(n8)
unquote1'(_gen_nil1':cons1'6(_n2342)) → _*7, rt ∈ Ω(n2342)
activate'(_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(_n24720)) → _gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(_n24720), rt ∈ Ω(1 + n24720)
Generator Equations:
_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(0) ⇔ n__0'
_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(+(x, 1)) ⇔ n__first'(n__0', _gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(x))
_gen_01':s1'5(0) ⇔ 01'
_gen_01':s1'5(+(x, 1)) ⇔ s1'(_gen_01':s1'5(x))
_gen_nil1':cons1'6(0) ⇔ nil1'
_gen_nil1':cons1'6(+(x, 1)) ⇔ cons1'(01', _gen_nil1':cons1'6(x))
The following defined symbols remain to be analysed:
quote', sel1', first1', quote1'
They will be analysed ascendingly in the following order:
sel1' = quote'
quote' < first1'
quote' < quote1'
first1' < quote1'
Could not prove a rewrite lemma for the defined symbol quote'.
Rules:
sel'(s'(X), cons'(Y, Z)) → sel'(X, activate'(Z))
sel'(0', cons'(X, Z)) → X
first'(0', Z) → nil'
first'(s'(X), cons'(Y, Z)) → cons'(Y, n__first'(X, activate'(Z)))
from'(X) → cons'(X, n__from'(n__s'(X)))
sel1'(s'(X), cons'(Y, Z)) → sel1'(X, activate'(Z))
sel1'(0', cons'(X, Z)) → quote'(X)
first1'(0', Z) → nil1'
first1'(s'(X), cons'(Y, Z)) → cons1'(quote'(Y), first1'(X, activate'(Z)))
quote'(n__0') → 01'
quote1'(n__cons'(X, Z)) → cons1'(quote'(activate'(X)), quote1'(activate'(Z)))
quote1'(n__nil') → nil1'
quote'(n__s'(X)) → s1'(quote'(activate'(X)))
quote'(n__sel'(X, Z)) → sel1'(activate'(X), activate'(Z))
quote1'(n__first'(X, Z)) → first1'(activate'(X), activate'(Z))
unquote'(01') → 0'
unquote'(s1'(X)) → s'(unquote'(X))
unquote1'(nil1') → nil'
unquote1'(cons1'(X, Z)) → fcons'(unquote'(X), unquote1'(Z))
fcons'(X, Z) → cons'(X, Z)
first'(X1, X2) → n__first'(X1, X2)
from'(X) → n__from'(X)
s'(X) → n__s'(X)
0' → n__0'
cons'(X1, X2) → n__cons'(X1, X2)
nil' → n__nil'
sel'(X1, X2) → n__sel'(X1, X2)
activate'(n__first'(X1, X2)) → first'(activate'(X1), activate'(X2))
activate'(n__from'(X)) → from'(activate'(X))
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__0') → 0'
activate'(n__cons'(X1, X2)) → cons'(activate'(X1), X2)
activate'(n__nil') → nil'
activate'(n__sel'(X1, X2)) → sel'(activate'(X1), activate'(X2))
activate'(X) → X
Types:
sel' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
s' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
cons' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
activate' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
0' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
first' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
nil' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__first' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
from' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__from' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__s' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
sel1' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → 01':s1'
quote' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → 01':s1'
first1' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → nil1':cons1'
nil1' :: nil1':cons1'
cons1' :: 01':s1' → nil1':cons1' → nil1':cons1'
n__0' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
01' :: 01':s1'
quote1' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → nil1':cons1'
n__cons' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__nil' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
s1' :: 01':s1' → 01':s1'
n__sel' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
unquote' :: 01':s1' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
unquote1' :: nil1':cons1' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
fcons' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
_hole_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'1 :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
_hole_01':s1'2 :: 01':s1'
_hole_nil1':cons1'3 :: nil1':cons1'
_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4 :: Nat → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
_gen_01':s1'5 :: Nat → 01':s1'
_gen_nil1':cons1'6 :: Nat → nil1':cons1'
Lemmas:
unquote'(_gen_01':s1'5(+(1, _n8))) → _*7, rt ∈ Ω(n8)
unquote1'(_gen_nil1':cons1'6(_n2342)) → _*7, rt ∈ Ω(n2342)
activate'(_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(_n24720)) → _gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(_n24720), rt ∈ Ω(1 + n24720)
Generator Equations:
_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(0) ⇔ n__0'
_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(+(x, 1)) ⇔ n__first'(n__0', _gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(x))
_gen_01':s1'5(0) ⇔ 01'
_gen_01':s1'5(+(x, 1)) ⇔ s1'(_gen_01':s1'5(x))
_gen_nil1':cons1'6(0) ⇔ nil1'
_gen_nil1':cons1'6(+(x, 1)) ⇔ cons1'(01', _gen_nil1':cons1'6(x))
The following defined symbols remain to be analysed:
sel1', first1', quote1'
They will be analysed ascendingly in the following order:
sel1' = quote'
quote' < first1'
quote' < quote1'
first1' < quote1'
Could not prove a rewrite lemma for the defined symbol sel1'.
Rules:
sel'(s'(X), cons'(Y, Z)) → sel'(X, activate'(Z))
sel'(0', cons'(X, Z)) → X
first'(0', Z) → nil'
first'(s'(X), cons'(Y, Z)) → cons'(Y, n__first'(X, activate'(Z)))
from'(X) → cons'(X, n__from'(n__s'(X)))
sel1'(s'(X), cons'(Y, Z)) → sel1'(X, activate'(Z))
sel1'(0', cons'(X, Z)) → quote'(X)
first1'(0', Z) → nil1'
first1'(s'(X), cons'(Y, Z)) → cons1'(quote'(Y), first1'(X, activate'(Z)))
quote'(n__0') → 01'
quote1'(n__cons'(X, Z)) → cons1'(quote'(activate'(X)), quote1'(activate'(Z)))
quote1'(n__nil') → nil1'
quote'(n__s'(X)) → s1'(quote'(activate'(X)))
quote'(n__sel'(X, Z)) → sel1'(activate'(X), activate'(Z))
quote1'(n__first'(X, Z)) → first1'(activate'(X), activate'(Z))
unquote'(01') → 0'
unquote'(s1'(X)) → s'(unquote'(X))
unquote1'(nil1') → nil'
unquote1'(cons1'(X, Z)) → fcons'(unquote'(X), unquote1'(Z))
fcons'(X, Z) → cons'(X, Z)
first'(X1, X2) → n__first'(X1, X2)
from'(X) → n__from'(X)
s'(X) → n__s'(X)
0' → n__0'
cons'(X1, X2) → n__cons'(X1, X2)
nil' → n__nil'
sel'(X1, X2) → n__sel'(X1, X2)
activate'(n__first'(X1, X2)) → first'(activate'(X1), activate'(X2))
activate'(n__from'(X)) → from'(activate'(X))
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__0') → 0'
activate'(n__cons'(X1, X2)) → cons'(activate'(X1), X2)
activate'(n__nil') → nil'
activate'(n__sel'(X1, X2)) → sel'(activate'(X1), activate'(X2))
activate'(X) → X
Types:
sel' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
s' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
cons' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
activate' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
0' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
first' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
nil' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__first' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
from' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__from' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__s' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
sel1' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → 01':s1'
quote' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → 01':s1'
first1' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → nil1':cons1'
nil1' :: nil1':cons1'
cons1' :: 01':s1' → nil1':cons1' → nil1':cons1'
n__0' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
01' :: 01':s1'
quote1' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → nil1':cons1'
n__cons' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__nil' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
s1' :: 01':s1' → 01':s1'
n__sel' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
unquote' :: 01':s1' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
unquote1' :: nil1':cons1' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
fcons' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
_hole_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'1 :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
_hole_01':s1'2 :: 01':s1'
_hole_nil1':cons1'3 :: nil1':cons1'
_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4 :: Nat → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
_gen_01':s1'5 :: Nat → 01':s1'
_gen_nil1':cons1'6 :: Nat → nil1':cons1'
Lemmas:
unquote'(_gen_01':s1'5(+(1, _n8))) → _*7, rt ∈ Ω(n8)
unquote1'(_gen_nil1':cons1'6(_n2342)) → _*7, rt ∈ Ω(n2342)
activate'(_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(_n24720)) → _gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(_n24720), rt ∈ Ω(1 + n24720)
Generator Equations:
_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(0) ⇔ n__0'
_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(+(x, 1)) ⇔ n__first'(n__0', _gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(x))
_gen_01':s1'5(0) ⇔ 01'
_gen_01':s1'5(+(x, 1)) ⇔ s1'(_gen_01':s1'5(x))
_gen_nil1':cons1'6(0) ⇔ nil1'
_gen_nil1':cons1'6(+(x, 1)) ⇔ cons1'(01', _gen_nil1':cons1'6(x))
The following defined symbols remain to be analysed:
first1', quote1'
They will be analysed ascendingly in the following order:
first1' < quote1'
Could not prove a rewrite lemma for the defined symbol first1'.
Rules:
sel'(s'(X), cons'(Y, Z)) → sel'(X, activate'(Z))
sel'(0', cons'(X, Z)) → X
first'(0', Z) → nil'
first'(s'(X), cons'(Y, Z)) → cons'(Y, n__first'(X, activate'(Z)))
from'(X) → cons'(X, n__from'(n__s'(X)))
sel1'(s'(X), cons'(Y, Z)) → sel1'(X, activate'(Z))
sel1'(0', cons'(X, Z)) → quote'(X)
first1'(0', Z) → nil1'
first1'(s'(X), cons'(Y, Z)) → cons1'(quote'(Y), first1'(X, activate'(Z)))
quote'(n__0') → 01'
quote1'(n__cons'(X, Z)) → cons1'(quote'(activate'(X)), quote1'(activate'(Z)))
quote1'(n__nil') → nil1'
quote'(n__s'(X)) → s1'(quote'(activate'(X)))
quote'(n__sel'(X, Z)) → sel1'(activate'(X), activate'(Z))
quote1'(n__first'(X, Z)) → first1'(activate'(X), activate'(Z))
unquote'(01') → 0'
unquote'(s1'(X)) → s'(unquote'(X))
unquote1'(nil1') → nil'
unquote1'(cons1'(X, Z)) → fcons'(unquote'(X), unquote1'(Z))
fcons'(X, Z) → cons'(X, Z)
first'(X1, X2) → n__first'(X1, X2)
from'(X) → n__from'(X)
s'(X) → n__s'(X)
0' → n__0'
cons'(X1, X2) → n__cons'(X1, X2)
nil' → n__nil'
sel'(X1, X2) → n__sel'(X1, X2)
activate'(n__first'(X1, X2)) → first'(activate'(X1), activate'(X2))
activate'(n__from'(X)) → from'(activate'(X))
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__0') → 0'
activate'(n__cons'(X1, X2)) → cons'(activate'(X1), X2)
activate'(n__nil') → nil'
activate'(n__sel'(X1, X2)) → sel'(activate'(X1), activate'(X2))
activate'(X) → X
Types:
sel' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
s' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
cons' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
activate' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
0' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
first' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
nil' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__first' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
from' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__from' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__s' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
sel1' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → 01':s1'
quote' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → 01':s1'
first1' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → nil1':cons1'
nil1' :: nil1':cons1'
cons1' :: 01':s1' → nil1':cons1' → nil1':cons1'
n__0' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
01' :: 01':s1'
quote1' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → nil1':cons1'
n__cons' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__nil' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
s1' :: 01':s1' → 01':s1'
n__sel' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
unquote' :: 01':s1' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
unquote1' :: nil1':cons1' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
fcons' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
_hole_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'1 :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
_hole_01':s1'2 :: 01':s1'
_hole_nil1':cons1'3 :: nil1':cons1'
_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4 :: Nat → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
_gen_01':s1'5 :: Nat → 01':s1'
_gen_nil1':cons1'6 :: Nat → nil1':cons1'
Lemmas:
unquote'(_gen_01':s1'5(+(1, _n8))) → _*7, rt ∈ Ω(n8)
unquote1'(_gen_nil1':cons1'6(_n2342)) → _*7, rt ∈ Ω(n2342)
activate'(_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(_n24720)) → _gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(_n24720), rt ∈ Ω(1 + n24720)
Generator Equations:
_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(0) ⇔ n__0'
_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(+(x, 1)) ⇔ n__first'(n__0', _gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(x))
_gen_01':s1'5(0) ⇔ 01'
_gen_01':s1'5(+(x, 1)) ⇔ s1'(_gen_01':s1'5(x))
_gen_nil1':cons1'6(0) ⇔ nil1'
_gen_nil1':cons1'6(+(x, 1)) ⇔ cons1'(01', _gen_nil1':cons1'6(x))
The following defined symbols remain to be analysed:
quote1'
Could not prove a rewrite lemma for the defined symbol quote1'.
Rules:
sel'(s'(X), cons'(Y, Z)) → sel'(X, activate'(Z))
sel'(0', cons'(X, Z)) → X
first'(0', Z) → nil'
first'(s'(X), cons'(Y, Z)) → cons'(Y, n__first'(X, activate'(Z)))
from'(X) → cons'(X, n__from'(n__s'(X)))
sel1'(s'(X), cons'(Y, Z)) → sel1'(X, activate'(Z))
sel1'(0', cons'(X, Z)) → quote'(X)
first1'(0', Z) → nil1'
first1'(s'(X), cons'(Y, Z)) → cons1'(quote'(Y), first1'(X, activate'(Z)))
quote'(n__0') → 01'
quote1'(n__cons'(X, Z)) → cons1'(quote'(activate'(X)), quote1'(activate'(Z)))
quote1'(n__nil') → nil1'
quote'(n__s'(X)) → s1'(quote'(activate'(X)))
quote'(n__sel'(X, Z)) → sel1'(activate'(X), activate'(Z))
quote1'(n__first'(X, Z)) → first1'(activate'(X), activate'(Z))
unquote'(01') → 0'
unquote'(s1'(X)) → s'(unquote'(X))
unquote1'(nil1') → nil'
unquote1'(cons1'(X, Z)) → fcons'(unquote'(X), unquote1'(Z))
fcons'(X, Z) → cons'(X, Z)
first'(X1, X2) → n__first'(X1, X2)
from'(X) → n__from'(X)
s'(X) → n__s'(X)
0' → n__0'
cons'(X1, X2) → n__cons'(X1, X2)
nil' → n__nil'
sel'(X1, X2) → n__sel'(X1, X2)
activate'(n__first'(X1, X2)) → first'(activate'(X1), activate'(X2))
activate'(n__from'(X)) → from'(activate'(X))
activate'(n__s'(X)) → s'(activate'(X))
activate'(n__0') → 0'
activate'(n__cons'(X1, X2)) → cons'(activate'(X1), X2)
activate'(n__nil') → nil'
activate'(n__sel'(X1, X2)) → sel'(activate'(X1), activate'(X2))
activate'(X) → X
Types:
sel' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
s' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
cons' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
activate' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
0' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
first' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
nil' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__first' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
from' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__from' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__s' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
sel1' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → 01':s1'
quote' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → 01':s1'
first1' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → nil1':cons1'
nil1' :: nil1':cons1'
cons1' :: 01':s1' → nil1':cons1' → nil1':cons1'
n__0' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
01' :: 01':s1'
quote1' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → nil1':cons1'
n__cons' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
n__nil' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
s1' :: 01':s1' → 01':s1'
n__sel' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
unquote' :: 01':s1' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
unquote1' :: nil1':cons1' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
fcons' :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel' → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
_hole_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'1 :: n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
_hole_01':s1'2 :: 01':s1'
_hole_nil1':cons1'3 :: nil1':cons1'
_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4 :: Nat → n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'
_gen_01':s1'5 :: Nat → 01':s1'
_gen_nil1':cons1'6 :: Nat → nil1':cons1'
Lemmas:
unquote'(_gen_01':s1'5(+(1, _n8))) → _*7, rt ∈ Ω(n8)
unquote1'(_gen_nil1':cons1'6(_n2342)) → _*7, rt ∈ Ω(n2342)
activate'(_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(_n24720)) → _gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(_n24720), rt ∈ Ω(1 + n24720)
Generator Equations:
_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(0) ⇔ n__0'
_gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(+(x, 1)) ⇔ n__first'(n__0', _gen_n__first':n__s':n__from':n__0':n__cons':n__nil':n__sel'4(x))
_gen_01':s1'5(0) ⇔ 01'
_gen_01':s1'5(+(x, 1)) ⇔ s1'(_gen_01':s1'5(x))
_gen_nil1':cons1'6(0) ⇔ nil1'
_gen_nil1':cons1'6(+(x, 1)) ⇔ cons1'(01', _gen_nil1':cons1'6(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
unquote'(_gen_01':s1'5(+(1, _n8))) → _*7, rt ∈ Ω(n8)