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

not(not(x)) → x
not(or(x, y)) → and(not(x), not(y))
not(and(x, y)) → or(not(x), not(y))
and(x, or(y, z)) → or(and(x, y), and(x, z))
and(or(y, z), x) → or(and(x, y), and(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:

not'(not'(x)) → x
not'(or'(x, y)) → and'(not'(x), not'(y))
not'(and'(x, y)) → or'(not'(x), not'(y))
and'(x, or'(y, z)) → or'(and'(x, y), and'(x, z))
and'(or'(y, z), x) → or'(and'(x, y), and'(x, z))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
not'(not'(x)) → x
not'(or'(x, y)) → and'(not'(x), not'(y))
not'(and'(x, y)) → or'(not'(x), not'(y))
and'(x, or'(y, z)) → or'(and'(x, y), and'(x, z))
and'(or'(y, z), x) → or'(and'(x, y), and'(x, z))

Types:
not' :: or' → or'
or' :: or' → or' → or'
and' :: or' → or' → or'
_hole_or'1 :: or'
_gen_or'2 :: Nat → or'

Heuristically decided to analyse the following defined symbols:
not', and'

They will be analysed ascendingly in the following order:
and' < not'

Rules:
not'(not'(x)) → x
not'(or'(x, y)) → and'(not'(x), not'(y))
not'(and'(x, y)) → or'(not'(x), not'(y))
and'(x, or'(y, z)) → or'(and'(x, y), and'(x, z))
and'(or'(y, z), x) → or'(and'(x, y), and'(x, z))

Types:
not' :: or' → or'
or' :: or' → or' → or'
and' :: or' → or' → or'
_hole_or'1 :: or'
_gen_or'2 :: Nat → or'

Generator Equations:
_gen_or'2(0) ⇔ _hole_or'1
_gen_or'2(+(x, 1)) ⇔ or'(_hole_or'1, _gen_or'2(x))

The following defined symbols remain to be analysed:
and', not'

They will be analysed ascendingly in the following order:
and' < not'

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

The following conjecture could not be proven:

and'(_gen_or'2(_n4), _gen_or'2(1)) →? _*3

Rules:
not'(not'(x)) → x
not'(or'(x, y)) → and'(not'(x), not'(y))
not'(and'(x, y)) → or'(not'(x), not'(y))
and'(x, or'(y, z)) → or'(and'(x, y), and'(x, z))
and'(or'(y, z), x) → or'(and'(x, y), and'(x, z))

Types:
not' :: or' → or'
or' :: or' → or' → or'
and' :: or' → or' → or'
_hole_or'1 :: or'
_gen_or'2 :: Nat → or'

Generator Equations:
_gen_or'2(0) ⇔ _hole_or'1
_gen_or'2(+(x, 1)) ⇔ or'(_hole_or'1, _gen_or'2(x))

The following defined symbols remain to be analysed:
not'

Proved the following rewrite lemma:
not'(_gen_or'2(+(1, _n12387))) → _*3, rt ∈ Ω(n12387)

Induction Base:
not'(_gen_or'2(+(1, 0)))

Induction Step:
not'(_gen_or'2(+(1, +(_\$n12388, 1)))) →RΩ(1)
and'(not'(_hole_or'1), not'(_gen_or'2(+(1, _\$n12388)))) →IH
and'(not'(_hole_or'1), _*3)

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

Rules:
not'(not'(x)) → x
not'(or'(x, y)) → and'(not'(x), not'(y))
not'(and'(x, y)) → or'(not'(x), not'(y))
and'(x, or'(y, z)) → or'(and'(x, y), and'(x, z))
and'(or'(y, z), x) → or'(and'(x, y), and'(x, z))

Types:
not' :: or' → or'
or' :: or' → or' → or'
and' :: or' → or' → or'
_hole_or'1 :: or'
_gen_or'2 :: Nat → or'

Lemmas:
not'(_gen_or'2(+(1, _n12387))) → _*3, rt ∈ Ω(n12387)

Generator Equations:
_gen_or'2(0) ⇔ _hole_or'1
_gen_or'2(+(x, 1)) ⇔ or'(_hole_or'1, _gen_or'2(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
not'(_gen_or'2(+(1, _n12387))) → _*3, rt ∈ Ω(n12387)