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

p(m, n, s(r)) → p(m, r, n)
p(m, s(n), 0) → p(0, n, m)
p(m, 0, 0) → m

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

p'(m, n, s'(r)) → p'(m, r, n)
p'(m, s'(n), 0') → p'(0', n, m)
p'(m, 0', 0') → m

Rewrite Strategy: INNERMOST

Infered types.

Rules:
p'(m, n, s'(r)) → p'(m, r, n)
p'(m, s'(n), 0') → p'(0', n, m)
p'(m, 0', 0') → m

Types:
p' :: s':0' → s':0' → s':0' → s':0'
s' :: s':0' → s':0'
0' :: s':0'
_hole_s':0'1 :: s':0'
_gen_s':0'2 :: Nat → s':0'

Heuristically decided to analyse the following defined symbols:
p'

Rules:
p'(m, n, s'(r)) → p'(m, r, n)
p'(m, s'(n), 0') → p'(0', n, m)
p'(m, 0', 0') → m

Types:
p' :: s':0' → s':0' → s':0' → s':0'
s' :: s':0' → s':0'
0' :: s':0'
_hole_s':0'1 :: s':0'
_gen_s':0'2 :: Nat → s':0'

Generator Equations:
_gen_s':0'2(0) ⇔ 0'
_gen_s':0'2(+(x, 1)) ⇔ s'(_gen_s':0'2(x))

The following defined symbols remain to be analysed:
p'

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

Rules:
p'(m, n, s'(r)) → p'(m, r, n)
p'(m, s'(n), 0') → p'(0', n, m)
p'(m, 0', 0') → m

Types:
p' :: s':0' → s':0' → s':0' → s':0'
s' :: s':0' → s':0'
0' :: s':0'
_hole_s':0'1 :: s':0'
_gen_s':0'2 :: Nat → s':0'

Generator Equations:
_gen_s':0'2(0) ⇔ 0'
_gen_s':0'2(+(x, 1)) ⇔ s'(_gen_s':0'2(x))

No more defined symbols left to analyse.