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