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)

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)

The following dependency pair can be strictly oriented:

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

The following rules can be oriented:

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)

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(false) = 0

POL(true) = 0

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

POL(not(x₁)) = x₁

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

POL(u) = 0

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

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

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

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

POL(null(x₁)) = x₁

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

POL(nil) = 0

POL(max(x₁)) = x₁

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

F(x₁, x₂) -> F(x₁, x₂)
g(x₁, x₂) -> g(x₁, x₂)
f(x₁, x₂) -> f(x₁, x₂)
++(x₁, x₂) -> ++(x₁, x₂)
null(x₁) -> null(x₁)
mem(x₁, x₂) -> mem(x₁, x₂)
or(x₁, x₂) -> or(x₁, x₂)
=(x₁, x₂) -> x₁
max(x₁) -> max(x₁)
not(x₁) -> not(x₁)
max'(x₁, x₂) -> max'(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)

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)

The following dependency pair can be strictly oriented:

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

The following rules can be oriented:

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)

Used ordering: Polynomial ordering with Polynomial interpretation:

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

POL(false) = 0

POL(true) = 0

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

POL(not(x₁)) = x₁

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

POL(u) = 0

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

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

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

POL(null(x₁)) = x₁

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

POL(nil) = 0

POL(max(x₁)) = x₁

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

++'(x₁, x₂) -> ++'(x₁, x₂)
g(x₁, x₂) -> g(x₁, x₂)
f(x₁, x₂) -> f(x₁, x₂)
++(x₁, x₂) -> ++(x₁, x₂)
null(x₁) -> null(x₁)
mem(x₁, x₂) -> mem(x₁, x₂)
or(x₁, x₂) -> or(x₁, x₂)
=(x₁, x₂) -> x₁
max(x₁) -> max(x₁)
not(x₁) -> not(x₁)
max'(x₁, x₂) -> max'(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)

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)

The following dependency pair can be strictly oriented:

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

The following rules can be oriented:

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)

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(false) = 0

POL(true) = 0

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

POL(not(x₁)) = x₁

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

POL(u) = 0

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

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

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

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

POL(null(x₁)) = x₁

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

POL(nil) = 0

POL(max(x₁)) = x₁

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

MEM(x₁, x₂) -> MEM(x₁, x₂)
g(x₁, x₂) -> g(x₁, x₂)
f(x₁, x₂) -> f(x₁, x₂)
++(x₁, x₂) -> ++(x₁, x₂)
null(x₁) -> null(x₁)
mem(x₁, x₂) -> mem(x₁, x₂)
or(x₁, x₂) -> or(x₁, x₂)
=(x₁, x₂) -> x₁
max(x₁) -> max(x₁)
not(x₁) -> not(x₁)
max'(x₁, x₂) -> max'(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)

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)

The following dependency pair can be strictly oriented:

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

The following rules can be oriented:

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)

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(false) = 0

POL(true) = 0

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

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

POL(not(x₁)) = x₁

POL(u) = 1

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

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

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

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

POL(null(x₁)) = x₁

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

POL(nil) = 0

POL(max(x₁)) = x₁

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

MAX(x₁) -> MAX(x₁)
g(x₁, x₂) -> g(x₁, x₂)
f(x₁, x₂) -> f(x₁, x₂)
++(x₁, x₂) -> ++(x₁, x₂)
null(x₁) -> null(x₁)
mem(x₁, x₂) -> mem(x₁, x₂)
or(x₁, x₂) -> or(x₁, x₂)
=(x₁, x₂) -> x₁
max(x₁) -> max(x₁)
not(x₁) -> not(x₁)
max'(x₁, x₂) -> max'(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)

Using the Dependency Graph resulted in no new DP problems.

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

POL(false)	= 0
POL(true)	= 0
POL(or(x₁, x₂))	= x₁ + x₂
POL(not(x₁))	= x₁
POL(max'(x₁, x₂))	= x₁ + x₂
POL(u)	= 0
POL(F(x₁, x₂))	= 1 + x₁ + x₂
POL(f(x₁, x₂))	= 1 + x₁ + x₂
POL(mem(x₁, x₂))	= x₁ + x₂
POL(g(x₁, x₂))	= 1 + x₁ + x₂
POL(null(x₁))	= x₁
POL(++(x₁, x₂))	= x₁ + x₂
POL(nil)	= 0
POL(max(x₁))	= x₁

POL(++'(x₁, x₂))	= 1 + x₁ + x₂
POL(false)	= 0
POL(true)	= 0
POL(or(x₁, x₂))	= x₁ + x₂
POL(not(x₁))	= x₁
POL(max'(x₁, x₂))	= x₁ + x₂
POL(u)	= 0
POL(f(x₁, x₂))	= 1 + x₁ + x₂
POL(mem(x₁, x₂))	= x₁ + x₂
POL(g(x₁, x₂))	= 1 + x₁ + x₂
POL(null(x₁))	= x₁
POL(++(x₁, x₂))	= x₁ + x₂
POL(nil)	= 0
POL(max(x₁))	= x₁