Runtime Complexity TRS:
The TRS R consists of the following rules:

h(x, c(y, z)) → h(c(s(y), x), z)
h(c(s(x), c(s(0), y)), z) → h(y, c(s(0), c(x, z)))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

Runtime Complexity TRS:
The TRS R consists of the following rules:

h'(x, c'(y, z)) → h'(c'(s'(y), x), z)
h'(c'(s'(x), c'(s'(0'), y)), z) → h'(y, c'(s'(0'), c'(x, z)))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
h'(x, c'(y, z)) → h'(c'(s'(y), x), z)
h'(c'(s'(x), c'(s'(0'), y)), z) → h'(y, c'(s'(0'), c'(x, z)))

Types:
h' :: c' → c' → h'
c' :: s':0' → c' → c'
s' :: s':0' → s':0'
0' :: s':0'
_hole_h'1 :: h'
_hole_c'2 :: c'
_hole_s':0'3 :: s':0'
_gen_c'4 :: Nat → c'
_gen_s':0'5 :: Nat → s':0'

Heuristically decided to analyse the following defined symbols:
h'

Rules:
h'(x, c'(y, z)) → h'(c'(s'(y), x), z)
h'(c'(s'(x), c'(s'(0'), y)), z) → h'(y, c'(s'(0'), c'(x, z)))

Types:
h' :: c' → c' → h'
c' :: s':0' → c' → c'
s' :: s':0' → s':0'
0' :: s':0'
_hole_h'1 :: h'
_hole_c'2 :: c'
_hole_s':0'3 :: s':0'
_gen_c'4 :: Nat → c'
_gen_s':0'5 :: Nat → s':0'

Generator Equations:
_gen_c'4(0) ⇔ _hole_c'2
_gen_c'4(+(x, 1)) ⇔ c'(0', _gen_c'4(x))
_gen_s':0'5(0) ⇔ 0'
_gen_s':0'5(+(x, 1)) ⇔ s'(_gen_s':0'5(x))

The following defined symbols remain to be analysed:
h'

Could not prove a rewrite lemma for the defined symbol h'.

The following conjecture could not be proven:

h'(_gen_c'4(a), _gen_c'4(+(1, _n7))) →? _*6

Rules:
h'(x, c'(y, z)) → h'(c'(s'(y), x), z)
h'(c'(s'(x), c'(s'(0'), y)), z) → h'(y, c'(s'(0'), c'(x, z)))

Types:
h' :: c' → c' → h'
c' :: s':0' → c' → c'
s' :: s':0' → s':0'
0' :: s':0'
_hole_h'1 :: h'
_hole_c'2 :: c'
_hole_s':0'3 :: s':0'
_gen_c'4 :: Nat → c'
_gen_s':0'5 :: Nat → s':0'

Generator Equations:
_gen_c'4(0) ⇔ _hole_c'2
_gen_c'4(+(x, 1)) ⇔ c'(0', _gen_c'4(x))
_gen_s':0'5(0) ⇔ 0'
_gen_s':0'5(+(x, 1)) ⇔ s'(_gen_s':0'5(x))

No more defined symbols left to analyse.