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

or(true, y) → true
or(x, true) → true
or(false, false) → false
mem(x, nil) → false
mem(x, set(y)) → =(x, y)
mem(x, union(y, z)) → or(mem(x, y), mem(x, z))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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


or'(true', y) → true'
or'(x, true') → true'
or'(false', false') → false'
mem'(x, nil') → false'
mem'(x, set'(y)) → ='(x, y)
mem'(x, union'(y, z)) → or'(mem'(x, y), mem'(x, z))

Rewrite Strategy: INNERMOST

Sliced the following arguments:
mem'/0
set'/0
='/0
='/1

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


or'(true', y) → true'
or'(x, true') → true'
or'(false', false') → false'
mem'(nil') → false'
mem'(set') → ='
mem'(union'(y, z)) → or'(mem'(y), mem'(z))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
or'(true', y) → true'
or'(x, true') → true'
or'(false', false') → false'
mem'(nil') → false'
mem'(set') → ='
mem'(union'(y, z)) → or'(mem'(y), mem'(z))

Types:
or' :: true':false':=' → true':false':=' → true':false':='
true' :: true':false':='
false' :: true':false':='
mem' :: nil':set':union' → true':false':='
nil' :: nil':set':union'
set' :: nil':set':union'
=' :: true':false':='
union' :: nil':set':union' → nil':set':union' → nil':set':union'
_hole_true':false':='1 :: true':false':='
_hole_nil':set':union'2 :: nil':set':union'
_gen_nil':set':union'3 :: Nat → nil':set':union'

Heuristically decided to analyse the following defined symbols:
mem'

Rules:
or'(true', y) → true'
or'(x, true') → true'
or'(false', false') → false'
mem'(nil') → false'
mem'(set') → ='
mem'(union'(y, z)) → or'(mem'(y), mem'(z))

Types:
or' :: true':false':=' → true':false':=' → true':false':='
true' :: true':false':='
false' :: true':false':='
mem' :: nil':set':union' → true':false':='
nil' :: nil':set':union'
set' :: nil':set':union'
=' :: true':false':='
union' :: nil':set':union' → nil':set':union' → nil':set':union'
_hole_true':false':='1 :: true':false':='
_hole_nil':set':union'2 :: nil':set':union'
_gen_nil':set':union'3 :: Nat → nil':set':union'

Generator Equations:
_gen_nil':set':union'3(0) ⇔ nil'
_gen_nil':set':union'3(+(x, 1)) ⇔ union'(nil', _gen_nil':set':union'3(x))

The following defined symbols remain to be analysed:
mem'

Proved the following rewrite lemma:
mem'(_gen_nil':set':union'3(_n5)) → false', rt ∈ Ω(1 + n5)

Induction Base:
mem'(_gen_nil':set':union'3(0)) →RΩ(1)
false'

Induction Step:
mem'(_gen_nil':set':union'3(+(_$n6, 1))) →RΩ(1)
or'(mem'(nil'), mem'(_gen_nil':set':union'3(_$n6))) →RΩ(1)
or'(false', mem'(_gen_nil':set':union'3(_$n6))) →IH
or'(false', false') →RΩ(1)
false'

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

Rules:
or'(true', y) → true'
or'(x, true') → true'
or'(false', false') → false'
mem'(nil') → false'
mem'(set') → ='
mem'(union'(y, z)) → or'(mem'(y), mem'(z))

Types:
or' :: true':false':=' → true':false':=' → true':false':='
true' :: true':false':='
false' :: true':false':='
mem' :: nil':set':union' → true':false':='
nil' :: nil':set':union'
set' :: nil':set':union'
=' :: true':false':='
union' :: nil':set':union' → nil':set':union' → nil':set':union'
_hole_true':false':='1 :: true':false':='
_hole_nil':set':union'2 :: nil':set':union'
_gen_nil':set':union'3 :: Nat → nil':set':union'

Lemmas:
mem'(_gen_nil':set':union'3(_n5)) → false', rt ∈ Ω(1 + n5)

Generator Equations:
_gen_nil':set':union'3(0) ⇔ nil'
_gen_nil':set':union'3(+(x, 1)) ⇔ union'(nil', _gen_nil':set':union'3(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
mem'(_gen_nil':set':union'3(_n5)) → false', rt ∈ Ω(1 + n5)