-(

-(s(

min(

min(0,

min(s(

twice(0) -> 0

twice(s(

f(s(

f(s(

R

↳Dependency Pair Analysis

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

MIN(s(x), s(y)) -> MIN(x,y)

TWICE(s(x)) -> TWICE(x)

F(s(x), s(y)) -> F(-(y, min(x,y)), s(twice(min(x,y))))

F(s(x), s(y)) -> -'(y, min(x,y))

F(s(x), s(y)) -> MIN(x,y)

F(s(x), s(y)) -> TWICE(min(x,y))

F(s(x), s(y)) -> F(-(x, min(x,y)), s(twice(min(x,y))))

F(s(x), s(y)) -> -'(x, min(x,y))

Furthermore,

R

↳DPs

→DP Problem 1

↳Remaining Obligation(s)

→DP Problem 2

↳Remaining Obligation(s)

→DP Problem 3

↳Remaining Obligation(s)

→DP Problem 4

↳Remaining Obligation(s)

The following remains to be proven:

**Dependency Pair:****-'(s(***x*), s(*y*)) -> -'(*x*,*y*)**Rules:**

-(*x*, 0) ->*x*

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

min(*x*, 0) -> 0

min(0,*y*) -> 0

min(s(*x*), s(*y*)) -> s(min(*x*,*y*))

twice(0) -> 0

twice(s(*x*)) -> s(s(twice(*x*)))

f(s(*x*), s(*y*)) -> f(-(*y*, min(*x*,*y*)), s(twice(min(*x*,*y*))))

f(s(*x*), s(*y*)) -> f(-(*x*, min(*x*,*y*)), s(twice(min(*x*,*y*))))**Dependency Pair:****MIN(s(***x*), s(*y*)) -> MIN(*x*,*y*)**Rules:**

-(*x*, 0) ->*x*

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

min(*x*, 0) -> 0

min(0,*y*) -> 0

min(s(*x*), s(*y*)) -> s(min(*x*,*y*))

twice(0) -> 0

twice(s(*x*)) -> s(s(twice(*x*)))

f(s(*x*), s(*y*)) -> f(-(*y*, min(*x*,*y*)), s(twice(min(*x*,*y*))))

f(s(*x*), s(*y*)) -> f(-(*x*, min(*x*,*y*)), s(twice(min(*x*,*y*))))**Dependency Pair:****TWICE(s(***x*)) -> TWICE(*x*)**Rules:**

-(*x*, 0) ->*x*

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

min(*x*, 0) -> 0

min(0,*y*) -> 0

min(s(*x*), s(*y*)) -> s(min(*x*,*y*))

twice(0) -> 0

twice(s(*x*)) -> s(s(twice(*x*)))

f(s(*x*), s(*y*)) -> f(-(*y*, min(*x*,*y*)), s(twice(min(*x*,*y*))))

f(s(*x*), s(*y*)) -> f(-(*x*, min(*x*,*y*)), s(twice(min(*x*,*y*))))**Dependency Pairs:****F(s(***x*), s(*y*)) -> F(-(*x*, min(*x*,*y*)), s(twice(min(*x*,*y*))))**F(s(***x*), s(*y*)) -> F(-(*y*, min(*x*,*y*)), s(twice(min(*x*,*y*))))**Rules:**

-(*x*, 0) ->*x*

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

min(*x*, 0) -> 0

min(0,*y*) -> 0

min(s(*x*), s(*y*)) -> s(min(*x*,*y*))

twice(0) -> 0

twice(s(*x*)) -> s(s(twice(*x*)))

f(s(*x*), s(*y*)) -> f(-(*y*, min(*x*,*y*)), s(twice(min(*x*,*y*))))

f(s(*x*), s(*y*)) -> f(-(*x*, min(*x*,*y*)), s(twice(min(*x*,*y*))))

R

↳DPs

→DP Problem 1

↳Remaining Obligation(s)

→DP Problem 2

↳Remaining Obligation(s)

→DP Problem 3

↳Remaining Obligation(s)

→DP Problem 4

↳Remaining Obligation(s)

The following remains to be proven:

**Dependency Pair:****-'(s(***x*), s(*y*)) -> -'(*x*,*y*)**Rules:**

-(*x*, 0) ->*x*

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

min(*x*, 0) -> 0

min(0,*y*) -> 0

min(s(*x*), s(*y*)) -> s(min(*x*,*y*))

twice(0) -> 0

twice(s(*x*)) -> s(s(twice(*x*)))

f(s(*x*), s(*y*)) -> f(-(*y*, min(*x*,*y*)), s(twice(min(*x*,*y*))))

f(s(*x*), s(*y*)) -> f(-(*x*, min(*x*,*y*)), s(twice(min(*x*,*y*))))**Dependency Pair:****MIN(s(***x*), s(*y*)) -> MIN(*x*,*y*)**Rules:**

-(*x*, 0) ->*x*

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

min(*x*, 0) -> 0

min(0,*y*) -> 0

min(s(*x*), s(*y*)) -> s(min(*x*,*y*))

twice(0) -> 0

twice(s(*x*)) -> s(s(twice(*x*)))

f(s(*x*), s(*y*)) -> f(-(*y*, min(*x*,*y*)), s(twice(min(*x*,*y*))))

f(s(*x*), s(*y*)) -> f(-(*x*, min(*x*,*y*)), s(twice(min(*x*,*y*))))**Dependency Pair:****TWICE(s(***x*)) -> TWICE(*x*)**Rules:**

-(*x*, 0) ->*x*

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

min(*x*, 0) -> 0

min(0,*y*) -> 0

min(s(*x*), s(*y*)) -> s(min(*x*,*y*))

twice(0) -> 0

twice(s(*x*)) -> s(s(twice(*x*)))

f(s(*x*), s(*y*)) -> f(-(*y*, min(*x*,*y*)), s(twice(min(*x*,*y*))))

f(s(*x*), s(*y*)) -> f(-(*x*, min(*x*,*y*)), s(twice(min(*x*,*y*))))**Dependency Pairs:****F(s(***x*), s(*y*)) -> F(-(*x*, min(*x*,*y*)), s(twice(min(*x*,*y*))))**F(s(***x*), s(*y*)) -> F(-(*y*, min(*x*,*y*)), s(twice(min(*x*,*y*))))**Rules:**

-(*x*, 0) ->*x*

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

min(*x*, 0) -> 0

min(0,*y*) -> 0

min(s(*x*), s(*y*)) -> s(min(*x*,*y*))

twice(0) -> 0

twice(s(*x*)) -> s(s(twice(*x*)))

f(s(*x*), s(*y*)) -> f(-(*y*, min(*x*,*y*)), s(twice(min(*x*,*y*))))

f(s(*x*), s(*y*)) -> f(-(*x*, min(*x*,*y*)), s(twice(min(*x*,*y*))))

R

↳DPs

→DP Problem 1

↳Remaining Obligation(s)

→DP Problem 2

↳Remaining Obligation(s)

→DP Problem 3

↳Remaining Obligation(s)

→DP Problem 4

↳Remaining Obligation(s)

The following remains to be proven:

**Dependency Pair:****-'(s(***x*), s(*y*)) -> -'(*x*,*y*)**Rules:**

-(*x*, 0) ->*x*

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

min(*x*, 0) -> 0

min(0,*y*) -> 0

min(s(*x*), s(*y*)) -> s(min(*x*,*y*))

twice(0) -> 0

twice(s(*x*)) -> s(s(twice(*x*)))

f(s(*x*), s(*y*)) -> f(-(*y*, min(*x*,*y*)), s(twice(min(*x*,*y*))))

f(s(*x*), s(*y*)) -> f(-(*x*, min(*x*,*y*)), s(twice(min(*x*,*y*))))**Dependency Pair:****MIN(s(***x*), s(*y*)) -> MIN(*x*,*y*)**Rules:**

-(*x*, 0) ->*x*

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

min(*x*, 0) -> 0

min(0,*y*) -> 0

min(s(*x*), s(*y*)) -> s(min(*x*,*y*))

twice(0) -> 0

twice(s(*x*)) -> s(s(twice(*x*)))

f(s(*x*), s(*y*)) -> f(-(*y*, min(*x*,*y*)), s(twice(min(*x*,*y*))))

f(s(*x*), s(*y*)) -> f(-(*x*, min(*x*,*y*)), s(twice(min(*x*,*y*))))**Dependency Pair:****TWICE(s(***x*)) -> TWICE(*x*)**Rules:**

-(*x*, 0) ->*x*

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

min(*x*, 0) -> 0

min(0,*y*) -> 0

min(s(*x*), s(*y*)) -> s(min(*x*,*y*))

twice(0) -> 0

twice(s(*x*)) -> s(s(twice(*x*)))

f(s(*x*), s(*y*)) -> f(-(*y*, min(*x*,*y*)), s(twice(min(*x*,*y*))))

f(s(*x*), s(*y*)) -> f(-(*x*, min(*x*,*y*)), s(twice(min(*x*,*y*))))**Dependency Pairs:****F(s(***x*), s(*y*)) -> F(-(*x*, min(*x*,*y*)), s(twice(min(*x*,*y*))))**F(s(***x*), s(*y*)) -> F(-(*y*, min(*x*,*y*)), s(twice(min(*x*,*y*))))**Rules:**

-(*x*, 0) ->*x*

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

min(*x*, 0) -> 0

min(0,*y*) -> 0

min(s(*x*), s(*y*)) -> s(min(*x*,*y*))

twice(0) -> 0

twice(s(*x*)) -> s(s(twice(*x*)))

f(s(*x*), s(*y*)) -> f(-(*y*, min(*x*,*y*)), s(twice(min(*x*,*y*))))

f(s(*x*), s(*y*)) -> f(-(*x*, min(*x*,*y*)), s(twice(min(*x*,*y*))))

R

↳DPs

→DP Problem 1

↳Remaining Obligation(s)

→DP Problem 2

↳Remaining Obligation(s)

→DP Problem 3

↳Remaining Obligation(s)

→DP Problem 4

↳Remaining Obligation(s)

The following remains to be proven:

**Dependency Pair:****-'(s(***x*), s(*y*)) -> -'(*x*,*y*)**Rules:**

-(*x*, 0) ->*x*

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

min(*x*, 0) -> 0

min(0,*y*) -> 0

min(s(*x*), s(*y*)) -> s(min(*x*,*y*))

twice(0) -> 0

twice(s(*x*)) -> s(s(twice(*x*)))

f(s(*x*), s(*y*)) -> f(-(*y*, min(*x*,*y*)), s(twice(min(*x*,*y*))))

f(s(*x*), s(*y*)) -> f(-(*x*, min(*x*,*y*)), s(twice(min(*x*,*y*))))**Dependency Pair:****MIN(s(***x*), s(*y*)) -> MIN(*x*,*y*)**Rules:**

-(*x*, 0) ->*x*

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

min(*x*, 0) -> 0

min(0,*y*) -> 0

min(s(*x*), s(*y*)) -> s(min(*x*,*y*))

twice(0) -> 0

twice(s(*x*)) -> s(s(twice(*x*)))

f(s(*x*), s(*y*)) -> f(-(*y*, min(*x*,*y*)), s(twice(min(*x*,*y*))))

f(s(*x*), s(*y*)) -> f(-(*x*, min(*x*,*y*)), s(twice(min(*x*,*y*))))**Dependency Pair:****TWICE(s(***x*)) -> TWICE(*x*)**Rules:**

-(*x*, 0) ->*x*

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

min(*x*, 0) -> 0

min(0,*y*) -> 0

min(s(*x*), s(*y*)) -> s(min(*x*,*y*))

twice(0) -> 0

twice(s(*x*)) -> s(s(twice(*x*)))

f(s(*x*), s(*y*)) -> f(-(*y*, min(*x*,*y*)), s(twice(min(*x*,*y*))))

f(s(*x*), s(*y*)) -> f(-(*x*, min(*x*,*y*)), s(twice(min(*x*,*y*))))**Dependency Pairs:****F(s(***x*), s(*y*)) -> F(-(*x*, min(*x*,*y*)), s(twice(min(*x*,*y*))))**F(s(***x*), s(*y*)) -> F(-(*y*, min(*x*,*y*)), s(twice(min(*x*,*y*))))**Rules:**

-(*x*, 0) ->*x*

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

min(*x*, 0) -> 0

min(0,*y*) -> 0

min(s(*x*), s(*y*)) -> s(min(*x*,*y*))

twice(0) -> 0

twice(s(*x*)) -> s(s(twice(*x*)))

f(s(*x*), s(*y*)) -> f(-(*y*, min(*x*,*y*)), s(twice(min(*x*,*y*))))

f(s(*x*), s(*y*)) -> f(-(*x*, min(*x*,*y*)), s(twice(min(*x*,*y*))))

Duration:

0:04 minutes