-(0,

-(

-(

p(0) -> 0

p(s(

R

↳Dependency Pair Analysis

-'(x, s(y)) -> -'(x, p(s(y)))

-'(x, s(y)) -> P(s(y))

Furthermore,

R

↳DPs

→DP Problem 1

↳Remaining Obligation(s)

The following remains to be proven:

**-'( x, s(y)) -> -'(x, p(s(y)))**

-(0,y) -> 0

-(x, 0) ->x

-(x, s(y)) -> if(greater(x, s(y)), s(-(x, p(s(y)))), 0)

p(0) -> 0

p(s(x)) ->x

innermost

Duration:

0:00 minutes