p(m, n, s(r)) → p(m, r, n)
p(m, s(n), 0) → p(0, n, m)
p(m, 0, 0) → m
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
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.