f(x, x) → f(i(x), g(g(x)))
f(x, y) → x
g(x) → i(x)
f(x, i(x)) → f(x, x)
f(i(x), i(g(x))) → a
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
f'(x, x) → f'(i'(x), g'(g'(x)))
f'(x, y) → x
g'(x) → i'(x)
f'(x, i'(x)) → f'(x, x)
f'(i'(x), i'(g'(x))) → a'
Infered types.
Rules:
f'(x, x) → f'(i'(x), g'(g'(x)))
f'(x, y) → x
g'(x) → i'(x)
f'(x, i'(x)) → f'(x, x)
f'(i'(x), i'(g'(x))) → a'
Types:
f' :: i':a' → i':a' → i':a'
i' :: i':a' → i':a'
g' :: i':a' → i':a'
a' :: i':a'
_hole_i':a'1 :: i':a'
_gen_i':a'2 :: Nat → i':a'
Heuristically decided to analyse the following defined symbols:
f'
Rules:
f'(x, x) → f'(i'(x), g'(g'(x)))
f'(x, y) → x
g'(x) → i'(x)
f'(x, i'(x)) → f'(x, x)
f'(i'(x), i'(g'(x))) → a'
Types:
f' :: i':a' → i':a' → i':a'
i' :: i':a' → i':a'
g' :: i':a' → i':a'
a' :: i':a'
_hole_i':a'1 :: i':a'
_gen_i':a'2 :: Nat → i':a'
Generator Equations:
_gen_i':a'2(0) ⇔ a'
_gen_i':a'2(+(x, 1)) ⇔ i'(_gen_i':a'2(x))
The following defined symbols remain to be analysed:
f'
Could not prove a rewrite lemma for the defined symbol f'.
Rules:
f'(x, x) → f'(i'(x), g'(g'(x)))
f'(x, y) → x
g'(x) → i'(x)
f'(x, i'(x)) → f'(x, x)
f'(i'(x), i'(g'(x))) → a'
Types:
f' :: i':a' → i':a' → i':a'
i' :: i':a' → i':a'
g' :: i':a' → i':a'
a' :: i':a'
_hole_i':a'1 :: i':a'
_gen_i':a'2 :: Nat → i':a'
Generator Equations:
_gen_i':a'2(0) ⇔ a'
_gen_i':a'2(+(x, 1)) ⇔ i'(_gen_i':a'2(x))
No more defined symbols left to analyse.