Termination Proof using AProVE

Term Rewriting System R:
[x, y, z]
f(x, nil) -> g(nil, x)
f(x, g(y, z)) -> g(f(x, y), z)
++(x, nil) -> x
++(x, g(y, z)) -> g(++(x, y), z)
null(nil) -> true
null(g(x, y)) -> false
mem(nil, y) -> false
mem(g(x, y), z) -> or(=(y, z), mem(x, z))
mem(x, max(x)) -> not(null(x))
max(g(g(nil, x), y)) -> max'(x, y)
max(g(g(g(x, y), z), u)) -> max'(max(g(g(x, y), z)), u)

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

F(x, g(y, z)) -> F(x, y)
++'(x, g(y, z)) -> ++'(x, y)
MEM(g(x, y), z) -> MEM(x, z)
MEM(x, max(x)) -> NULL(x)
MAX(g(g(g(x, y), z), u)) -> MAX(g(g(x, y), z))

Furthermore, R contains four SCCs.

     ↳DPs

       →DP Problem 1

         ↳Argument Filtering and Ordering

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

Dependency Pair:

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

Rules:

f(x, nil) -> g(nil, x)
f(x, g(y, z)) -> g(f(x, y), z)
++(x, nil) -> x
++(x, g(y, z)) -> g(++(x, y), z)
null(nil) -> true
null(g(x, y)) -> false
mem(nil, y) -> false
mem(g(x, y), z) -> or(=(y, z), mem(x, z))
mem(x, max(x)) -> not(null(x))
max(g(g(nil, x), y)) -> max'(x, y)
max(g(g(g(x, y), z), u)) -> max'(max(g(g(x, y), z)), u)

Strategy:

innermost

The following dependency pair can be strictly oriented:

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

There are no usable rules for innermost that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(g(x₁, x₂)) = 1 + x₁ + x₂

POL(F(x₁, x₂)) = x₁ + x₂

resulting in one new DP problem.
Used Argument Filtering System:

F(x₁, x₂) -> F(x₁, x₂)
g(x₁, x₂) -> g(x₁, x₂)

     ↳DPs

       →DP Problem 1

         ↳AFS

           →DP Problem 5

             ↳Dependency Graph

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

Dependency Pair:

Rules:

f(x, nil) -> g(nil, x)
f(x, g(y, z)) -> g(f(x, y), z)
++(x, nil) -> x
++(x, g(y, z)) -> g(++(x, y), z)
null(nil) -> true
null(g(x, y)) -> false
mem(nil, y) -> false
mem(g(x, y), z) -> or(=(y, z), mem(x, z))
mem(x, max(x)) -> not(null(x))
max(g(g(nil, x), y)) -> max'(x, y)
max(g(g(g(x, y), z), u)) -> max'(max(g(g(x, y), z)), u)

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳Argument Filtering and Ordering

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

Dependency Pair:

++'(x, g(y, z)) -> ++'(x, y)

Rules:

f(x, nil) -> g(nil, x)
f(x, g(y, z)) -> g(f(x, y), z)
++(x, nil) -> x
++(x, g(y, z)) -> g(++(x, y), z)
null(nil) -> true
null(g(x, y)) -> false
mem(nil, y) -> false
mem(g(x, y), z) -> or(=(y, z), mem(x, z))
mem(x, max(x)) -> not(null(x))
max(g(g(nil, x), y)) -> max'(x, y)
max(g(g(g(x, y), z), u)) -> max'(max(g(g(x, y), z)), u)

Strategy:

innermost

The following dependency pair can be strictly oriented:

++'(x, g(y, z)) -> ++'(x, y)

There are no usable rules for innermost that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(++'(x₁, x₂)) = x₁ + x₂

POL(g(x₁, x₂)) = 1 + x₁ + x₂

resulting in one new DP problem.
Used Argument Filtering System:

++'(x₁, x₂) -> ++'(x₁, x₂)
g(x₁, x₂) -> g(x₁, x₂)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

           →DP Problem 6

             ↳Dependency Graph

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

Dependency Pair:

Rules:

f(x, nil) -> g(nil, x)
f(x, g(y, z)) -> g(f(x, y), z)
++(x, nil) -> x
++(x, g(y, z)) -> g(++(x, y), z)
null(nil) -> true
null(g(x, y)) -> false
mem(nil, y) -> false
mem(g(x, y), z) -> or(=(y, z), mem(x, z))
mem(x, max(x)) -> not(null(x))
max(g(g(nil, x), y)) -> max'(x, y)
max(g(g(g(x, y), z), u)) -> max'(max(g(g(x, y), z)), u)

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Argument Filtering and Ordering

       →DP Problem 4

         ↳AFS

Dependency Pair:

MEM(g(x, y), z) -> MEM(x, z)

Rules:

f(x, nil) -> g(nil, x)
f(x, g(y, z)) -> g(f(x, y), z)
++(x, nil) -> x
++(x, g(y, z)) -> g(++(x, y), z)
null(nil) -> true
null(g(x, y)) -> false
mem(nil, y) -> false
mem(g(x, y), z) -> or(=(y, z), mem(x, z))
mem(x, max(x)) -> not(null(x))
max(g(g(nil, x), y)) -> max'(x, y)
max(g(g(g(x, y), z), u)) -> max'(max(g(g(x, y), z)), u)

Strategy:

innermost

The following dependency pair can be strictly oriented:

MEM(g(x, y), z) -> MEM(x, z)

There are no usable rules for innermost that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(MEM(x₁, x₂)) = x₁ + x₂

POL(g(x₁, x₂)) = 1 + x₁ + x₂

resulting in one new DP problem.
Used Argument Filtering System:

MEM(x₁, x₂) -> MEM(x₁, x₂)
g(x₁, x₂) -> g(x₁, x₂)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

           →DP Problem 7

             ↳Dependency Graph

       →DP Problem 4

         ↳AFS

Dependency Pair:

Rules:

f(x, nil) -> g(nil, x)
f(x, g(y, z)) -> g(f(x, y), z)
++(x, nil) -> x
++(x, g(y, z)) -> g(++(x, y), z)
null(nil) -> true
null(g(x, y)) -> false
mem(nil, y) -> false
mem(g(x, y), z) -> or(=(y, z), mem(x, z))
mem(x, max(x)) -> not(null(x))
max(g(g(nil, x), y)) -> max'(x, y)
max(g(g(g(x, y), z), u)) -> max'(max(g(g(x, y), z)), u)

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳Argument Filtering and Ordering

Dependency Pair:

MAX(g(g(g(x, y), z), u)) -> MAX(g(g(x, y), z))

Rules:

f(x, nil) -> g(nil, x)
f(x, g(y, z)) -> g(f(x, y), z)
++(x, nil) -> x
++(x, g(y, z)) -> g(++(x, y), z)
null(nil) -> true
null(g(x, y)) -> false
mem(nil, y) -> false
mem(g(x, y), z) -> or(=(y, z), mem(x, z))
mem(x, max(x)) -> not(null(x))
max(g(g(nil, x), y)) -> max'(x, y)
max(g(g(g(x, y), z), u)) -> max'(max(g(g(x, y), z)), u)

Strategy:

innermost

The following dependency pair can be strictly oriented:

MAX(g(g(g(x, y), z), u)) -> MAX(g(g(x, y), z))

There are no usable rules for innermost that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(MAX(x₁)) = 1 + x₁

POL(g(x₁, x₂)) = 1 + x₁ + x₂

POL(u) = 0

resulting in one new DP problem.
Used Argument Filtering System:

MAX(x₁) -> MAX(x₁)
g(x₁, x₂) -> g(x₁, x₂)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

           →DP Problem 8

             ↳Dependency Graph

Dependency Pair:

Rules:

f(x, nil) -> g(nil, x)
f(x, g(y, z)) -> g(f(x, y), z)
++(x, nil) -> x
++(x, g(y, z)) -> g(++(x, y), z)
null(nil) -> true
null(g(x, y)) -> false
mem(nil, y) -> false
mem(g(x, y), z) -> or(=(y, z), mem(x, z))
mem(x, max(x)) -> not(null(x))
max(g(g(nil, x), y)) -> max'(x, y)
max(g(g(g(x, y), z), u)) -> max'(max(g(g(x, y), z)), u)

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

Innermost Termination of R successfully shown.
Duration:
0:00 minutes

POL(g(x₁, x₂))	= 1 + x₁ + x₂
POL(F(x₁, x₂))	= x₁ + x₂

POL(++'(x₁, x₂))	= x₁ + x₂
POL(g(x₁, x₂))	= 1 + x₁ + x₂

POL(MEM(x₁, x₂))	= x₁ + x₂
POL(g(x₁, x₂))	= 1 + x₁ + x₂

POL(MAX(x₁))	= 1 + x₁
POL(g(x₁, x₂))	= 1 + x₁ + x₂
POL(u)	= 0