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

function(iszero, 0, dummy, dummy2) → true
function(iszero, s(x), dummy, dummy2) → false
function(p, 0, dummy, dummy2) → 0
function(p, s(0), dummy, dummy2) → 0
function(p, s(s(x)), dummy, dummy2) → s(function(p, s(x), x, x))
function(plus, dummy, x, y) → function(if, function(iszero, x, x, x), x, y)
function(if, true, x, y) → y
function(if, false, x, y) → function(plus, function(third, x, y, y), function(p, x, x, y), s(y))
function(third, x, y, z) → z

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

function'(iszero', 0', dummy, dummy2) → true'
function'(iszero', s'(x), dummy, dummy2) → false'
function'(p', 0', dummy, dummy2) → 0'
function'(p', s'(0'), dummy, dummy2) → 0'
function'(p', s'(s'(x)), dummy, dummy2) → s'(function'(p', s'(x), x, x))
function'(plus', dummy, x, y) → function'(if', function'(iszero', x, x, x), x, y)
function'(if', true', x, y) → y
function'(if', false', x, y) → function'(plus', function'(third', x, y, y), function'(p', x, x, y), s'(y))
function'(third', x, y, z) → z

Rewrite Strategy: INNERMOST

Infered types.

Rules:
function'(iszero', 0', dummy, dummy2) → true'
function'(iszero', s'(x), dummy, dummy2) → false'
function'(p', 0', dummy, dummy2) → 0'
function'(p', s'(0'), dummy, dummy2) → 0'
function'(p', s'(s'(x)), dummy, dummy2) → s'(function'(p', s'(x), x, x))
function'(plus', dummy, x, y) → function'(if', function'(iszero', x, x, x), x, y)
function'(if', true', x, y) → y
function'(if', false', x, y) → function'(plus', function'(third', x, y, y), function'(p', x, x, y), s'(y))
function'(third', x, y, z) → z

Types:
function' :: iszero':p':plus':if':third' → 0':true':s':false' → 0':true':s':false' → 0':true':s':false' → 0':true':s':false'
iszero' :: iszero':p':plus':if':third'
0' :: 0':true':s':false'
true' :: 0':true':s':false'
s' :: 0':true':s':false' → 0':true':s':false'
false' :: 0':true':s':false'
p' :: iszero':p':plus':if':third'
plus' :: iszero':p':plus':if':third'
if' :: iszero':p':plus':if':third'
third' :: iszero':p':plus':if':third'
_hole_0':true':s':false'1 :: 0':true':s':false'
_hole_iszero':p':plus':if':third'2 :: iszero':p':plus':if':third'
_gen_0':true':s':false'3 :: Nat → 0':true':s':false'

Heuristically decided to analyse the following defined symbols:
function'

Generator Equations:
_gen_0':true':s':false'3(0) ⇔ 0'
_gen_0':true':s':false'3(+(x, 1)) ⇔ s'(_gen_0':true':s':false'3(x))

The following defined symbols remain to be analysed:
function'

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

Generator Equations:
_gen_0':true':s':false'3(0) ⇔ 0'
_gen_0':true':s':false'3(+(x, 1)) ⇔ s'(_gen_0':true':s':false'3(x))

No more defined symbols left to analyse.