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

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


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

Rewrite Strategy: INNERMOST

Infered types.

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

Types:
implies' :: not' → or' → or'
not' :: not' → not'
or' :: not' → or' → or'
_hole_or'1 :: or'
_hole_not'2 :: not'
_gen_or'3 :: Nat → or'
_gen_not'4 :: Nat → not'

Heuristically decided to analyse the following defined symbols:
implies'

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

Types:
implies' :: not' → or' → or'
not' :: not' → not'
or' :: not' → or' → or'
_hole_or'1 :: or'
_hole_not'2 :: not'
_gen_or'3 :: Nat → or'
_gen_not'4 :: Nat → not'

Generator Equations:
_gen_or'3(0) ⇔ _hole_or'1
_gen_or'3(+(x, 1)) ⇔ or'(_hole_not'2, _gen_or'3(x))
_gen_not'4(0) ⇔ _hole_not'2
_gen_not'4(+(x, 1)) ⇔ not'(_gen_not'4(x))

The following defined symbols remain to be analysed:
implies'

Proved the following rewrite lemma:
implies'(_gen_not'4(1), _gen_or'3(_n6)) → _*5, rt ∈ Ω(n6)

Induction Base:
implies'(_gen_not'4(1), _gen_or'3(0))

Induction Step:
implies'(_gen_not'4(1), _gen_or'3(+(_$n7, 1))) →RΩ(1)
or'(_hole_not'2, implies'(_gen_not'4(1), _gen_or'3(_$n7))) →IH
or'(_hole_not'2, _*5)

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

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

Types:
implies' :: not' → or' → or'
not' :: not' → not'
or' :: not' → or' → or'
_hole_or'1 :: or'
_hole_not'2 :: not'
_gen_or'3 :: Nat → or'
_gen_not'4 :: Nat → not'

Lemmas:
implies'(_gen_not'4(1), _gen_or'3(_n6)) → _*5, rt ∈ Ω(n6)

Generator Equations:
_gen_or'3(0) ⇔ _hole_or'1
_gen_or'3(+(x, 1)) ⇔ or'(_hole_not'2, _gen_or'3(x))
_gen_not'4(0) ⇔ _hole_not'2
_gen_not'4(+(x, 1)) ⇔ not'(_gen_not'4(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
implies'(_gen_not'4(1), _gen_or'3(_n6)) → _*5, rt ∈ Ω(n6)