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

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

Rewrite Strategy: INNERMOST

Infered types.

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

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

Types:
not' :: or' → or'
and' :: or' → or' → or'
or' :: 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'

Proved the following rewrite lemma:
and'(_gen_or'2(a), _gen_or'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)

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

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

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

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

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

Lemmas:
and'(_gen_or'2(a), _gen_or'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)

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, _n4417))) → _*3, rt ∈ Ω(n4417)

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

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

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

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

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

Lemmas:
and'(_gen_or'2(a), _gen_or'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)
not'(_gen_or'2(+(1, _n4417))) → _*3, rt ∈ Ω(n4417)

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:
and'(_gen_or'2(a), _gen_or'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)