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