f(

f(0,

f(0, 0,

f(s(0),

f(s(

f(s(

f(0, s(0), s(0)) -> s(s(0))

f(s(

f(0, s(s(

f(0, s(0), s(s(

f(0, s(s(

R

↳Dependency Pair Analysis

F(s(0),y,z) -> F(0, s(y), s(z))

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

F(s(x), 0, s(z)) -> F(x, s(0),z)

F(s(x), s(y), s(z)) -> F(x,y, f(s(x), s(y),z))

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

F(0, s(s(y)), s(0)) -> F(0,y, s(0))

F(0, s(0), s(s(z))) -> F(0, s(0),z)

F(0, s(s(y)), s(s(z))) -> F(0,y, f(0, s(s(y)), s(z)))

F(0, s(s(y)), s(s(z))) -> F(0, s(s(y)), s(z))

Furthermore,

R

↳DPs

→DP Problem 1

↳Argument Filtering and Ordering

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

→DP Problem 4

↳AFS

**F(0, s(s( y)), s(0)) -> F(0, y, s(0))**

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

f(0,y, 0) -> s(y)

f(0, 0,z) -> s(z)

f(s(0),y,z) -> f(0, s(y), s(z))

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

f(s(x), 0, s(z)) -> f(x, s(0),z)

f(0, s(0), s(0)) -> s(s(0))

f(s(x), s(y), s(z)) -> f(x,y, f(s(x), s(y),z))

f(0, s(s(y)), s(0)) -> f(0,y, s(0))

f(0, s(0), s(s(z))) -> f(0, s(0),z)

f(0, s(s(y)), s(s(z))) -> f(0,y, f(0, s(s(y)), s(z)))

The following dependency pair can be strictly oriented:

F(0, s(s(y)), s(0)) -> F(0,y, s(0))

There are no usable rules w.r.t. to the AFS that need to be oriented.

Used ordering: Homeomorphic Embedding Order with EMB

resulting in one new DP problem.

Used Argument Filtering System:

F(x,_{1}x,_{2}x) -> F(_{3}x,_{1}x,_{2}x)_{3}

s(x) -> s(_{1}x)_{1}

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 5

↳Dependency Graph

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

→DP Problem 4

↳AFS

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

f(0,y, 0) -> s(y)

f(0, 0,z) -> s(z)

f(s(0),y,z) -> f(0, s(y), s(z))

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

f(s(x), 0, s(z)) -> f(x, s(0),z)

f(0, s(0), s(0)) -> s(s(0))

f(s(x), s(y), s(z)) -> f(x,y, f(s(x), s(y),z))

f(0, s(s(y)), s(0)) -> f(0,y, s(0))

f(0, s(0), s(s(z))) -> f(0, s(0),z)

f(0, s(s(y)), s(s(z))) -> f(0,y, f(0, s(s(y)), s(z)))

Using the Dependency Graph resulted in no new DP problems.

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳Argument Filtering and Ordering

→DP Problem 3

↳AFS

→DP Problem 4

↳AFS

**F(0, s(0), s(s( z))) -> F(0, s(0), z)**

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

f(0,y, 0) -> s(y)

f(0, 0,z) -> s(z)

f(s(0),y,z) -> f(0, s(y), s(z))

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

f(s(x), 0, s(z)) -> f(x, s(0),z)

f(0, s(0), s(0)) -> s(s(0))

f(s(x), s(y), s(z)) -> f(x,y, f(s(x), s(y),z))

f(0, s(s(y)), s(0)) -> f(0,y, s(0))

f(0, s(0), s(s(z))) -> f(0, s(0),z)

f(0, s(s(y)), s(s(z))) -> f(0,y, f(0, s(s(y)), s(z)))

The following dependency pair can be strictly oriented:

F(0, s(0), s(s(z))) -> F(0, s(0),z)

There are no usable rules w.r.t. to the AFS that need to be oriented.

Used ordering: Homeomorphic Embedding Order with EMB

resulting in one new DP problem.

Used Argument Filtering System:

F(x,_{1}x,_{2}x) -> F(_{3}x,_{1}x,_{2}x)_{3}

s(x) -> s(_{1}x)_{1}

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 6

↳Dependency Graph

→DP Problem 3

↳AFS

→DP Problem 4

↳AFS

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

f(0,y, 0) -> s(y)

f(0, 0,z) -> s(z)

f(s(0),y,z) -> f(0, s(y), s(z))

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

f(s(x), 0, s(z)) -> f(x, s(0),z)

f(0, s(0), s(0)) -> s(s(0))

f(s(x), s(y), s(z)) -> f(x,y, f(s(x), s(y),z))

f(0, s(s(y)), s(0)) -> f(0,y, s(0))

f(0, s(0), s(s(z))) -> f(0, s(0),z)

f(0, s(s(y)), s(s(z))) -> f(0,y, f(0, s(s(y)), s(z)))

Using the Dependency Graph resulted in no new DP problems.

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 3

↳Argument Filtering and Ordering

→DP Problem 4

↳AFS

**F(0, s(s( y)), s(s(z))) -> F(0, s(s(y)), s(z))**

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

f(0,y, 0) -> s(y)

f(0, 0,z) -> s(z)

f(s(0),y,z) -> f(0, s(y), s(z))

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

f(s(x), 0, s(z)) -> f(x, s(0),z)

f(0, s(0), s(0)) -> s(s(0))

f(s(x), s(y), s(z)) -> f(x,y, f(s(x), s(y),z))

f(0, s(s(y)), s(0)) -> f(0,y, s(0))

f(0, s(0), s(s(z))) -> f(0, s(0),z)

f(0, s(s(y)), s(s(z))) -> f(0,y, f(0, s(s(y)), s(z)))

The following dependency pair can be strictly oriented:

F(0, s(s(y)), s(s(z))) -> F(0,y, f(0, s(s(y)), s(z)))

There are no usable rules w.r.t. to the AFS that need to be oriented.

Used ordering: Homeomorphic Embedding Order with EMB

resulting in one new DP problem.

Used Argument Filtering System:

F(x,_{1}x,_{2}x) ->_{3}x_{2}

s(x) -> s(_{1}x)_{1}

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

→DP Problem 7

↳Argument Filtering and Ordering

→DP Problem 4

↳AFS

**F(0, s(s( y)), s(s(z))) -> F(0, s(s(y)), s(z))**

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

f(0,y, 0) -> s(y)

f(0, 0,z) -> s(z)

f(s(0),y,z) -> f(0, s(y), s(z))

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

f(s(x), 0, s(z)) -> f(x, s(0),z)

f(0, s(0), s(0)) -> s(s(0))

f(s(x), s(y), s(z)) -> f(x,y, f(s(x), s(y),z))

f(0, s(s(y)), s(0)) -> f(0,y, s(0))

f(0, s(0), s(s(z))) -> f(0, s(0),z)

f(0, s(s(y)), s(s(z))) -> f(0,y, f(0, s(s(y)), s(z)))

The following dependency pair can be strictly oriented:

F(0, s(s(y)), s(s(z))) -> F(0, s(s(y)), s(z))

There are no usable rules w.r.t. to the AFS that need to be oriented.

Used ordering: Homeomorphic Embedding Order with EMB

resulting in one new DP problem.

Used Argument Filtering System:

F(x,_{1}x,_{2}x) -> F(_{3}x,_{1}x,_{2}x)_{3}

s(x) -> s(_{1}x)_{1}

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

→DP Problem 7

↳AFS

...

→DP Problem 8

↳Dependency Graph

→DP Problem 4

↳AFS

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

f(0,y, 0) -> s(y)

f(0, 0,z) -> s(z)

f(s(0),y,z) -> f(0, s(y), s(z))

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

f(s(x), 0, s(z)) -> f(x, s(0),z)

f(0, s(0), s(0)) -> s(s(0))

f(s(x), s(y), s(z)) -> f(x,y, f(s(x), s(y),z))

f(0, s(s(y)), s(0)) -> f(0,y, s(0))

f(0, s(0), s(s(z))) -> f(0, s(0),z)

f(0, s(s(y)), s(s(z))) -> f(0,y, f(0, s(s(y)), s(z)))

Using the Dependency Graph resulted in no new DP problems.

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

→DP Problem 4

↳Argument Filtering and Ordering

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

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

f(0,y, 0) -> s(y)

f(0, 0,z) -> s(z)

f(s(0),y,z) -> f(0, s(y), s(z))

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

f(s(x), 0, s(z)) -> f(x, s(0),z)

f(0, s(0), s(0)) -> s(s(0))

f(s(x), s(y), s(z)) -> f(x,y, f(s(x), s(y),z))

f(0, s(s(y)), s(0)) -> f(0,y, s(0))

f(0, s(0), s(s(z))) -> f(0, s(0),z)

f(0, s(s(y)), s(s(z))) -> f(0,y, f(0, s(s(y)), s(z)))

The following dependency pairs can be strictly oriented:

F(s(x), s(y), s(z)) -> F(x,y, f(s(x), s(y),z))

F(s(x), 0, s(z)) -> F(x, s(0),z)

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

There are no usable rules w.r.t. to the AFS that need to be oriented.

Used ordering: Homeomorphic Embedding Order with EMB

resulting in one new DP problem.

Used Argument Filtering System:

F(x,_{1}x,_{2}x) ->_{3}x_{1}

s(x) -> s(_{1}x)_{1}

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

→DP Problem 4

↳AFS

→DP Problem 9

↳Argument Filtering and Ordering

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

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

f(0,y, 0) -> s(y)

f(0, 0,z) -> s(z)

f(s(0),y,z) -> f(0, s(y), s(z))

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

f(s(x), 0, s(z)) -> f(x, s(0),z)

f(0, s(0), s(0)) -> s(s(0))

f(s(x), s(y), s(z)) -> f(x,y, f(s(x), s(y),z))

f(0, s(s(y)), s(0)) -> f(0,y, s(0))

f(0, s(0), s(s(z))) -> f(0, s(0),z)

f(0, s(s(y)), s(s(z))) -> f(0,y, f(0, s(s(y)), s(z)))

The following dependency pair can be strictly oriented:

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

There are no usable rules w.r.t. to the AFS that need to be oriented.

Used ordering: Homeomorphic Embedding Order with EMB

resulting in one new DP problem.

Used Argument Filtering System:

F(x,_{1}x,_{2}x) -> F(_{3}x,_{1}x,_{2}x)_{3}

s(x) -> s(_{1}x)_{1}

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

→DP Problem 3

↳AFS

→DP Problem 4

↳AFS

→DP Problem 9

↳AFS

...

→DP Problem 10

↳Dependency Graph

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

f(0,y, 0) -> s(y)

f(0, 0,z) -> s(z)

f(s(0),y,z) -> f(0, s(y), s(z))

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

f(s(x), 0, s(z)) -> f(x, s(0),z)

f(0, s(0), s(0)) -> s(s(0))

f(s(x), s(y), s(z)) -> f(x,y, f(s(x), s(y),z))

f(0, s(s(y)), s(0)) -> f(0,y, s(0))

f(0, s(0), s(s(z))) -> f(0, s(0),z)

f(0, s(s(y)), s(s(z))) -> f(0,y, f(0, s(s(y)), s(z)))

Using the Dependency Graph resulted in no new DP problems.

Duration:

0:00 minutes