+(0,

+(s(

+(s(

R

↳Dependency Pair Analysis

+'(s(x), s(y)) -> +'(s(x), +(y, 0))

+'(s(x), s(y)) -> +'(y, 0)

Furthermore,

R

↳DPs

→DP Problem 1

↳Remaining Obligation(s)

The following remains to be proven:

**+'(s( x), s(y)) -> +'(s(x), +(y, 0))**

+(0,y) ->y

+(s(x), 0) -> s(x)

+(s(x), s(y)) -> s(+(s(x), +(y, 0)))

innermost

Duration:

0:00 minutes