g(f(x, y)) → f(f(g(g(x)), g(g(y))), f(g(g(x)), g(g(y))))
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
g'(f'(x, y)) → f'(f'(g'(g'(x)), g'(g'(y))), f'(g'(g'(x)), g'(g'(y))))
Infered types.
Rules:
g'(f'(x, y)) → f'(f'(g'(g'(x)), g'(g'(y))), f'(g'(g'(x)), g'(g'(y))))
Types:
g' :: f' → f'
f' :: f' → f' → f'
_hole_f'1 :: f'
_gen_f'2 :: Nat → f'
Heuristically decided to analyse the following defined symbols:
g'
Rules:
g'(f'(x, y)) → f'(f'(g'(g'(x)), g'(g'(y))), f'(g'(g'(x)), g'(g'(y))))
Types:
g' :: f' → f'
f' :: f' → f' → f'
_hole_f'1 :: f'
_gen_f'2 :: Nat → f'
Generator Equations:
_gen_f'2(0) ⇔ _hole_f'1
_gen_f'2(+(x, 1)) ⇔ f'(_hole_f'1, _gen_f'2(x))
The following defined symbols remain to be analysed:
g'
Proved the following rewrite lemma:
g'(_gen_f'2(+(1, _n4))) → _*3, rt ∈ Ω(2n)
Induction Base:
g'(_gen_f'2(+(1, 0)))
Induction Step:
g'(_gen_f'2(+(1, +(_$n5, 1)))) →RΩ(1)
f'(f'(g'(g'(_hole_f'1)), g'(g'(_gen_f'2(+(1, _$n5))))), f'(g'(g'(_hole_f'1)), g'(g'(_gen_f'2(+(1, _$n5)))))) →IH
f'(f'(g'(g'(_hole_f'1)), g'(_*3)), f'(g'(g'(_hole_f'1)), g'(g'(_gen_f'2(+(1, _$n5)))))) →IH
f'(f'(g'(g'(_hole_f'1)), g'(_*3)), f'(g'(g'(_hole_f'1)), g'(_*3)))
We have rt ∈ Ω(2n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(2n)