Runtime Complexity TRS:
The TRS R consists of the following rules:

0(#) → #
+(x, #) → x
+(#, x) → x
+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))
+(1(x), 0(y)) → 1(+(x, y))
+(1(x), 1(y)) → 0(+(+(x, y), 1(#)))
+(+(x, y), z) → +(x, +(y, z))
-(#, x) → #
-(x, #) → x
-(0(x), 0(y)) → 0(-(x, y))
-(0(x), 1(y)) → 1(-(-(x, y), 1(#)))
-(1(x), 0(y)) → 1(-(x, y))
-(1(x), 1(y)) → 0(-(x, y))
not(true) → false
not(false) → true
if(true, x, y) → x
if(false, x, y) → y
eq(#, #) → true
eq(#, 1(y)) → false
eq(1(x), #) → false
eq(#, 0(y)) → eq(#, y)
eq(0(x), #) → eq(x, #)
eq(1(x), 1(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(0(x), 0(y)) → eq(x, y)
ge(0(x), 0(y)) → ge(x, y)
ge(0(x), 1(y)) → not(ge(y, x))
ge(1(x), 0(y)) → ge(x, y)
ge(1(x), 1(y)) → ge(x, y)
ge(x, #) → true
ge(#, 0(x)) → ge(#, x)
ge(#, 1(x)) → false
log(x) → -(log'(x), 1(#))
log'(#) → #
log'(1(x)) → +(log'(x), 1(#))
log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)
*(#, x) → #
*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)
*(*(x, y), z) → *(x, *(y, z))
*(x, +(y, z)) → +(*(x, y), *(x, z))
app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))
sum(nil) → 0(#)
sum(cons(x, l)) → +(x, sum(l))
sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → 1(#)
prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))
mem(x, nil) → false
mem(x, cons(y, l)) → if(eq(x, y), true, mem(x, l))
inter(x, nil) → nil
inter(nil, x) → nil
inter(app(l1, l2), l3) → app(inter(l1, l3), inter(l2, l3))
inter(l1, app(l2, l3)) → app(inter(l1, l2), inter(l1, l3))
inter(cons(x, l1), l2) → ifinter(mem(x, l2), x, l1, l2)
inter(l1, cons(x, l2)) → ifinter(mem(x, l1), x, l2, l1)
ifinter(true, x, l1, l2) → cons(x, inter(l1, l2))
ifinter(false, x, l1, l2) → inter(l1, l2)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

Runtime Complexity TRS:
The TRS R consists of the following rules:

0'(#') → #'
+'(x, #') → x
+'(#', x) → x
+'(0'(x), 0'(y)) → 0'(+'(x, y))
+'(0'(x), 1'(y)) → 1'(+'(x, y))
+'(1'(x), 0'(y)) → 1'(+'(x, y))
+'(1'(x), 1'(y)) → 0'(+'(+'(x, y), 1'(#')))
+'(+'(x, y), z) → +'(x, +'(y, z))
-'(#', x) → #'
-'(x, #') → x
-'(0'(x), 0'(y)) → 0'(-'(x, y))
-'(0'(x), 1'(y)) → 1'(-'(-'(x, y), 1'(#')))
-'(1'(x), 0'(y)) → 1'(-'(x, y))
-'(1'(x), 1'(y)) → 0'(-'(x, y))
not'(true') → false'
not'(false') → true'
if'(true', x, y) → x
if'(false', x, y) → y
eq'(#', #') → true'
eq'(#', 1'(y)) → false'
eq'(1'(x), #') → false'
eq'(#', 0'(y)) → eq'(#', y)
eq'(0'(x), #') → eq'(x, #')
eq'(1'(x), 1'(y)) → eq'(x, y)
eq'(0'(x), 1'(y)) → false'
eq'(1'(x), 0'(y)) → false'
eq'(0'(x), 0'(y)) → eq'(x, y)
ge'(0'(x), 0'(y)) → ge'(x, y)
ge'(0'(x), 1'(y)) → not'(ge'(y, x))
ge'(1'(x), 0'(y)) → ge'(x, y)
ge'(1'(x), 1'(y)) → ge'(x, y)
ge'(x, #') → true'
ge'(#', 0'(x)) → ge'(#', x)
ge'(#', 1'(x)) → false'
log''(x) → -'(log'''(x), 1'(#'))
log'''(#') → #'
log'''(1'(x)) → +'(log'''(x), 1'(#'))
log'''(0'(x)) → if'(ge'(x, 1'(#')), +'(log'''(x), 1'(#')), #')
*'(#', x) → #'
*'(0'(x), y) → 0'(*'(x, y))
*'(1'(x), y) → +'(0'(*'(x, y)), y)
*'(*'(x, y), z) → *'(x, *'(y, z))
*'(x, +'(y, z)) → +'(*'(x, y), *'(x, z))
app'(nil', l) → l
app'(cons'(x, l1), l2) → cons'(x, app'(l1, l2))
sum'(nil') → 0'(#')
sum'(cons'(x, l)) → +'(x, sum'(l))
sum'(app'(l1, l2)) → +'(sum'(l1), sum'(l2))
prod'(nil') → 1'(#')
prod'(cons'(x, l)) → *'(x, prod'(l))
prod'(app'(l1, l2)) → *'(prod'(l1), prod'(l2))
mem'(x, nil') → false'
mem'(x, cons'(y, l)) → if'(eq'(x, y), true', mem'(x, l))
inter'(x, nil') → nil'
inter'(nil', x) → nil'
inter'(app'(l1, l2), l3) → app'(inter'(l1, l3), inter'(l2, l3))
inter'(l1, app'(l2, l3)) → app'(inter'(l1, l2), inter'(l1, l3))
inter'(cons'(x, l1), l2) → ifinter'(mem'(x, l2), x, l1, l2)
inter'(l1, cons'(x, l2)) → ifinter'(mem'(x, l1), x, l2, l1)
ifinter'(true', x, l1, l2) → cons'(x, inter'(l1, l2))
ifinter'(false', x, l1, l2) → inter'(l1, l2)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
0'(#') → #'
+'(x, #') → x
+'(#', x) → x
+'(0'(x), 0'(y)) → 0'(+'(x, y))
+'(0'(x), 1'(y)) → 1'(+'(x, y))
+'(1'(x), 0'(y)) → 1'(+'(x, y))
+'(1'(x), 1'(y)) → 0'(+'(+'(x, y), 1'(#')))
+'(+'(x, y), z) → +'(x, +'(y, z))
-'(#', x) → #'
-'(x, #') → x
-'(0'(x), 0'(y)) → 0'(-'(x, y))
-'(0'(x), 1'(y)) → 1'(-'(-'(x, y), 1'(#')))
-'(1'(x), 0'(y)) → 1'(-'(x, y))
-'(1'(x), 1'(y)) → 0'(-'(x, y))
not'(true') → false'
not'(false') → true'
if'(true', x, y) → x
if'(false', x, y) → y
eq'(#', #') → true'
eq'(#', 1'(y)) → false'
eq'(1'(x), #') → false'
eq'(#', 0'(y)) → eq'(#', y)
eq'(0'(x), #') → eq'(x, #')
eq'(1'(x), 1'(y)) → eq'(x, y)
eq'(0'(x), 1'(y)) → false'
eq'(1'(x), 0'(y)) → false'
eq'(0'(x), 0'(y)) → eq'(x, y)
ge'(0'(x), 0'(y)) → ge'(x, y)
ge'(0'(x), 1'(y)) → not'(ge'(y, x))
ge'(1'(x), 0'(y)) → ge'(x, y)
ge'(1'(x), 1'(y)) → ge'(x, y)
ge'(x, #') → true'
ge'(#', 0'(x)) → ge'(#', x)
ge'(#', 1'(x)) → false'
log''(x) → -'(log'''(x), 1'(#'))
log'''(#') → #'
log'''(1'(x)) → +'(log'''(x), 1'(#'))
log'''(0'(x)) → if'(ge'(x, 1'(#')), +'(log'''(x), 1'(#')), #')
*'(#', x) → #'
*'(0'(x), y) → 0'(*'(x, y))
*'(1'(x), y) → +'(0'(*'(x, y)), y)
*'(*'(x, y), z) → *'(x, *'(y, z))
*'(x, +'(y, z)) → +'(*'(x, y), *'(x, z))
app'(nil', l) → l
app'(cons'(x, l1), l2) → cons'(x, app'(l1, l2))
sum'(nil') → 0'(#')
sum'(cons'(x, l)) → +'(x, sum'(l))
sum'(app'(l1, l2)) → +'(sum'(l1), sum'(l2))
prod'(nil') → 1'(#')
prod'(cons'(x, l)) → *'(x, prod'(l))
prod'(app'(l1, l2)) → *'(prod'(l1), prod'(l2))
mem'(x, nil') → false'
mem'(x, cons'(y, l)) → if'(eq'(x, y), true', mem'(x, l))
inter'(x, nil') → nil'
inter'(nil', x) → nil'
inter'(app'(l1, l2), l3) → app'(inter'(l1, l3), inter'(l2, l3))
inter'(l1, app'(l2, l3)) → app'(inter'(l1, l2), inter'(l1, l3))
inter'(cons'(x, l1), l2) → ifinter'(mem'(x, l2), x, l1, l2)
inter'(l1, cons'(x, l2)) → ifinter'(mem'(x, l1), x, l2, l1)
ifinter'(true', x, l1, l2) → cons'(x, inter'(l1, l2))
ifinter'(false', x, l1, l2) → inter'(l1, l2)

Types:
0' :: #':1':true':false' → #':1':true':false'
#' :: #':1':true':false'
+' :: #':1':true':false' → #':1':true':false' → #':1':true':false'
1' :: #':1':true':false' → #':1':true':false'
-' :: #':1':true':false' → #':1':true':false' → #':1':true':false'
not' :: #':1':true':false' → #':1':true':false'
true' :: #':1':true':false'
false' :: #':1':true':false'
if' :: #':1':true':false' → #':1':true':false' → #':1':true':false' → #':1':true':false'
eq' :: #':1':true':false' → #':1':true':false' → #':1':true':false'
ge' :: #':1':true':false' → #':1':true':false' → #':1':true':false'
log'' :: #':1':true':false' → #':1':true':false'
log''' :: #':1':true':false' → #':1':true':false'
*' :: #':1':true':false' → #':1':true':false' → #':1':true':false'
app' :: nil':cons' → nil':cons' → nil':cons'
nil' :: nil':cons'
cons' :: #':1':true':false' → nil':cons' → nil':cons'
sum' :: nil':cons' → #':1':true':false'
prod' :: nil':cons' → #':1':true':false'
mem' :: #':1':true':false' → nil':cons' → #':1':true':false'
inter' :: nil':cons' → nil':cons' → nil':cons'
ifinter' :: #':1':true':false' → #':1':true':false' → nil':cons' → nil':cons' → nil':cons'
_hole_#':1':true':false'1 :: #':1':true':false'
_hole_nil':cons'2 :: nil':cons'
_gen_#':1':true':false'3 :: Nat → #':1':true':false'
_gen_nil':cons'4 :: Nat → nil':cons'

Heuristically decided to analyse the following defined symbols:
+', -', eq', ge', log''', *', app', sum', prod', mem', inter'

They will be analysed ascendingly in the following order:
+' < log'''
+' < *'
+' < sum'
eq' < mem'
ge' < log'''
*' < prod'
app' < inter'
mem' < inter'

Generator Equations:
_gen_#':1':true':false'3(0) ⇔ #'
_gen_#':1':true':false'3(+(x, 1)) ⇔ 1'(_gen_#':1':true':false'3(x))
_gen_nil':cons'4(0) ⇔ nil'
_gen_nil':cons'4(+(x, 1)) ⇔ cons'(#', _gen_nil':cons'4(x))

The following defined symbols remain to be analysed:
+', -', eq', ge', log''', *', app', sum', prod', mem', inter'

They will be analysed ascendingly in the following order:
+' < log'''
+' < *'
+' < sum'
eq' < mem'
ge' < log'''
*' < prod'
app' < inter'
mem' < inter'

Proved the following rewrite lemma:
+'(_gen_#':1':true':false'3(_n6), _gen_#':1':true':false'3(_n6)) → _*5, rt ∈ Ω(_n6)

Induction Base:
+'(_gen_#':1':true':false'3(0), _gen_#':1':true':false'3(0))

Induction Step:
+'(_gen_#':1':true':false'3(+(_$n7, 1)), _gen_#':1':true':false'3(+(_$n7, 1))) →_R^Ω(1)
0'(+'(+'(_gen_#':1':true':false'3(_$n7), _gen_#':1':true':false'3(_$n7)), 1'(#'))) →_IH
0'(+'(_*5, 1'(#')))

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Lemmas:
+'(_gen_#':1':true':false'3(_n6), _gen_#':1':true':false'3(_n6)) → _*5, rt ∈ Ω(_n6)

The following defined symbols remain to be analysed:
-', eq', ge', log''', *', app', sum', prod', mem', inter'

They will be analysed ascendingly in the following order:
eq' < mem'
ge' < log'''
*' < prod'
app' < inter'
mem' < inter'

Proved the following rewrite lemma:
-'(_gen_#':1':true':false'3(_n45824), _gen_#':1':true':false'3(_n45824)) → _gen_#':1':true':false'3(0), rt ∈ Ω(1 + _n45824)

Induction Base:
-'(_gen_#':1':true':false'3(0), _gen_#':1':true':false'3(0)) →_R^Ω(1)
#'

Induction Step:
-'(_gen_#':1':true':false'3(+(_$n45825, 1)), _gen_#':1':true':false'3(+(_$n45825, 1))) →_R^Ω(1)
0'(-'(_gen_#':1':true':false'3(_$n45825), _gen_#':1':true':false'3(_$n45825))) →_IH
0'(_gen_#':1':true':false'3(0)) →_R^Ω(1)
#'

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

The following defined symbols remain to be analysed:
eq', ge', log''', *', app', sum', prod', mem', inter'

They will be analysed ascendingly in the following order:
eq' < mem'
ge' < log'''
*' < prod'
app' < inter'
mem' < inter'

Proved the following rewrite lemma:
eq'(_gen_#':1':true':false'3(_n50806), _gen_#':1':true':false'3(_n50806)) → true', rt ∈ Ω(1 + _n50806)

Induction Base:
eq'(_gen_#':1':true':false'3(0), _gen_#':1':true':false'3(0)) →_R^Ω(1)
true'

Induction Step:
eq'(_gen_#':1':true':false'3(+(_$n50807, 1)), _gen_#':1':true':false'3(+(_$n50807, 1))) →_R^Ω(1)
eq'(_gen_#':1':true':false'3(_$n50807), _gen_#':1':true':false'3(_$n50807)) →_IH
true'

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

The following defined symbols remain to be analysed:
ge', log''', *', app', sum', prod', mem', inter'

They will be analysed ascendingly in the following order:
ge' < log'''
*' < prod'
app' < inter'
mem' < inter'

Proved the following rewrite lemma:
ge'(_gen_#':1':true':false'3(_n68048), _gen_#':1':true':false'3(_n68048)) → true', rt ∈ Ω(1 + _n68048)

Induction Base:
ge'(_gen_#':1':true':false'3(0), _gen_#':1':true':false'3(0)) →_R^Ω(1)
true'

Induction Step:
ge'(_gen_#':1':true':false'3(+(_$n68049, 1)), _gen_#':1':true':false'3(+(_$n68049, 1))) →_R^Ω(1)
ge'(_gen_#':1':true':false'3(_$n68049), _gen_#':1':true':false'3(_$n68049)) →_IH
true'

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

The following defined symbols remain to be analysed:
log''', *', app', sum', prod', mem', inter'

They will be analysed ascendingly in the following order:
*' < prod'
app' < inter'
mem' < inter'

Proved the following rewrite lemma:
log'''(_gen_#':1':true':false'3(+(1, _n72836))) → _*5, rt ∈ Ω(_n72836)

Induction Base:
log'''(_gen_#':1':true':false'3(+(1, 0)))

Induction Step:
log'''(_gen_#':1':true':false'3(+(1, +(_$n72837, 1)))) →_R^Ω(1)
+'(log'''(_gen_#':1':true':false'3(+(1, _$n72837))), 1'(#')) →_IH
+'(_*5, 1'(#'))

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

The following defined symbols remain to be analysed:
*', app', sum', prod', mem', inter'

They will be analysed ascendingly in the following order:
*' < prod'
app' < inter'
mem' < inter'

Proved the following rewrite lemma:
*'(_gen_#':1':true':false'3(_n312304), _gen_#':1':true':false'3(0)) → _gen_#':1':true':false'3(0), rt ∈ Ω(1 + _n312304)

Induction Base:
*'(_gen_#':1':true':false'3(0), _gen_#':1':true':false'3(0)) →_R^Ω(1)
#'

Induction Step:
*'(_gen_#':1':true':false'3(+(_$n312305, 1)), _gen_#':1':true':false'3(0)) →_R^Ω(1)
+'(0'(*'(_gen_#':1':true':false'3(_$n312305), _gen_#':1':true':false'3(0))), _gen_#':1':true':false'3(0)) →_IH
+'(0'(_gen_#':1':true':false'3(0)), _gen_#':1':true':false'3(0)) →_R^Ω(1)
+'(#', _gen_#':1':true':false'3(0)) →_R^Ω(1)
#'

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

The following defined symbols remain to be analysed:
app', sum', prod', mem', inter'

They will be analysed ascendingly in the following order:
app' < inter'
mem' < inter'

Proved the following rewrite lemma:
app'(_gen_nil':cons'4(_n329356), _gen_nil':cons'4(b)) → _gen_nil':cons'4(+(_n329356, b)), rt ∈ Ω(1 + _n329356)

Induction Base:
app'(_gen_nil':cons'4(0), _gen_nil':cons'4(b)) →_R^Ω(1)
_gen_nil':cons'4(b)

Induction Step:
app'(_gen_nil':cons'4(+(_$n329357, 1)), _gen_nil':cons'4(_b329671)) →_R^Ω(1)
cons'(#', app'(_gen_nil':cons'4(_$n329357), _gen_nil':cons'4(_b329671))) →_IH
cons'(#', _gen_nil':cons'4(+(_$n329357, _b329671)))

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Lemmas:
+'(_gen_#':1':true':false'3(_n6), _gen_#':1':true':false'3(_n6)) → _*5, rt ∈ Ω(_n6)
-'(_gen_#':1':true':false'3(_n45824), _gen_#':1':true':false'3(_n45824)) → _gen_#':1':true':false'3(0), rt ∈ Ω(1 + _n45824)
eq'(_gen_#':1':true':false'3(_n50806), _gen_#':1':true':false'3(_n50806)) → true', rt ∈ Ω(1 + _n50806)
ge'(_gen_#':1':true':false'3(_n68048), _gen_#':1':true':false'3(_n68048)) → true', rt ∈ Ω(1 + _n68048)
log'''(_gen_#':1':true':false'3(+(1, _n72836))) → _*5, rt ∈ Ω(_n72836)
*'(_gen_#':1':true':false'3(_n312304), _gen_#':1':true':false'3(0)) → _gen_#':1':true':false'3(0), rt ∈ Ω(1 + _n312304)
app'(_gen_nil':cons'4(_n329356), _gen_nil':cons'4(b)) → _gen_nil':cons'4(+(_n329356, b)), rt ∈ Ω(1 + _n329356)

The following defined symbols remain to be analysed:
sum', prod', mem', inter'

They will be analysed ascendingly in the following order:
mem' < inter'

Proved the following rewrite lemma:
sum'(_gen_nil':cons'4(_n333080)) → _gen_#':1':true':false'3(0), rt ∈ Ω(1 + _n333080)

Induction Base:
sum'(_gen_nil':cons'4(0)) →_R^Ω(1)
0'(#') →_R^Ω(1)
#'

Induction Step:
sum'(_gen_nil':cons'4(+(_$n333081, 1))) →_R^Ω(1)
+'(#', sum'(_gen_nil':cons'4(_$n333081))) →_IH
+'(#', _gen_#':1':true':false'3(0)) →_R^Ω(1)
#'

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

The following defined symbols remain to be analysed:
prod', mem', inter'

They will be analysed ascendingly in the following order:
mem' < inter'

Proved the following rewrite lemma:
prod'(_gen_nil':cons'4(_n341262)) → _*5, rt ∈ Ω(_n341262)

Induction Base:
prod'(_gen_nil':cons'4(0))

Induction Step:
prod'(_gen_nil':cons'4(+(_$n341263, 1))) →_R^Ω(1)
*'(#', prod'(_gen_nil':cons'4(_$n341263))) →_IH
*'(#', _*5)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

The following defined symbols remain to be analysed:
mem', inter'

They will be analysed ascendingly in the following order:
mem' < inter'

Proved the following rewrite lemma:
mem'(_gen_#':1':true':false'3(0), _gen_nil':cons'4(_n346638)) → _*5, rt ∈ Ω(_n346638)

Induction Base:
mem'(_gen_#':1':true':false'3(0), _gen_nil':cons'4(0))

Induction Step:
mem'(_gen_#':1':true':false'3(0), _gen_nil':cons'4(+(_$n346639, 1))) →_R^Ω(1)
if'(eq'(_gen_#':1':true':false'3(0), #'), true', mem'(_gen_#':1':true':false'3(0), _gen_nil':cons'4(_$n346639))) →_L^Ω(1)
if'(true', true', mem'(_gen_#':1':true':false'3(0), _gen_nil':cons'4(_$n346639))) →_IH
if'(true', true', _*5)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

The following defined symbols remain to be analysed:
inter'

Could not prove a rewrite lemma for the defined symbol inter'.

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
+'(_gen_#':1':true':false'3(_n6), _gen_#':1':true':false'3(_n6)) → _*5, rt ∈ Ω(_n6)