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))
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))
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)