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

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

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

Rewrite Strategy: INNERMOST

Infered types.

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

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

Heuristically decided to analyse the following defined symbols:
not'

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

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

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

The following defined symbols remain to be analysed:
not'

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

Induction Base:
not'(_gen_or':and'2(0))

Induction Step:
not'(_gen_or':and'2(+(_$n5, 1))) →RΩ(1)
and'(not'(not'(not'(_hole_or':and'1))), not'(not'(not'(_gen_or':and'2(_$n5))))) →RΩ(1)
and'(not'(_hole_or':and'1), not'(not'(not'(_gen_or':and'2(_$n5))))) →IH
and'(not'(_hole_or':and'1), not'(not'(_*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'(not'(not'(x))), not'(not'(not'(y))))
not'(and'(x, y)) → or'(not'(not'(not'(x))), not'(not'(not'(y))))

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

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

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

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
not'(_gen_or':and'2(_n4)) → _*3, rt ∈ Ω(n4)