YES

The TRS could be proven terminating. The proof took 3492 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (260ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (2278ms).
 |    | – Problem 3 was processed with processor PolynomialLinearRange4iUR (606ms).
 |    |    | – Problem 4 was processed with processor PolynomialLinearRange4iUR (200ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

app#(app(member, w), app(app(app(fork, x), y), z)) → app#(app(eq, w), y)app#(app(member, w), app(app(app(fork, x), y), z)) → app#(app(app(if, app(app(eq, w), y)), true), app(app(member, w), z))
app#(app(member, w), app(app(app(fork, x), y), z)) → app#(lt, w)app#(app(member, w), app(app(app(fork, x), y), z)) → app#(member, w)
app#(app(lt, app(s, x)), app(s, y)) → app#(app(lt, x), y)app#(app(member, w), app(app(app(fork, x), y), z)) → app#(app(app(if, app(app(lt, w), y)), app(app(member, w), x)), app(app(app(if, app(app(eq, w), y)), true), app(app(member, w), z)))
app#(app(member, w), app(app(app(fork, x), y), z)) → app#(app(if, app(app(eq, w), y)), true)app#(app(lt, app(s, x)), app(s, y)) → app#(lt, x)
app#(app(member, w), app(app(app(fork, x), y), z)) → app#(if, app(app(eq, w), y))app#(app(member, w), app(app(app(fork, x), y), z)) → app#(eq, w)
app#(app(member, w), app(app(app(fork, x), y), z)) → app#(app(member, w), x)app#(app(member, w), app(app(app(fork, x), y), z)) → app#(app(member, w), z)
app#(app(member, w), app(app(app(fork, x), y), z)) → app#(app(lt, w), y)app#(app(member, w), app(app(app(fork, x), y), z)) → app#(if, app(app(lt, w), y))
app#(app(member, w), app(app(app(fork, x), y), z)) → app#(app(if, app(app(lt, w), y)), app(app(member, w), x))

Rewrite Rules

app(app(lt, app(s, x)), app(s, y)) → app(app(lt, x), y)app(app(lt, 0), app(s, y)) → true
app(app(lt, y), 0) → falseapp(app(eq, x), x) → true
app(app(eq, app(s, x)), 0) → falseapp(app(eq, 0), app(s, x)) → false
app(app(member, w), null) → falseapp(app(member, w), app(app(app(fork, x), y), z)) → app(app(app(if, app(app(lt, w), y)), app(app(member, w), x)), app(app(app(if, app(app(eq, w), y)), true), app(app(member, w), z)))

Original Signature

Termination of terms over the following signature is verified: member, app, fork, 0, s, if, true, false, lt, null, eq

Strategy

The following SCCs where found

app#(app(member, w), app(app(app(fork, x), y), z)) → app#(app(eq, w), y)app#(app(member, w), app(app(app(fork, x), y), z)) → app#(app(app(if, app(app(eq, w), y)), true), app(app(member, w), z))
app#(app(lt, app(s, x)), app(s, y)) → app#(app(lt, x), y)app#(app(member, w), app(app(app(fork, x), y), z)) → app#(app(member, w), z)
app#(app(member, w), app(app(app(fork, x), y), z)) → app#(app(app(if, app(app(lt, w), y)), app(app(member, w), x)), app(app(app(if, app(app(eq, w), y)), true), app(app(member, w), z)))app#(app(member, w), app(app(app(fork, x), y), z)) → app#(app(lt, w), y)
app#(app(member, w), app(app(app(fork, x), y), z)) → app#(app(if, app(app(lt, w), y)), app(app(member, w), x))app#(app(member, w), app(app(app(fork, x), y), z)) → app#(app(member, w), x)

Problem 2: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

app#(app(member, w), app(app(app(fork, x), y), z)) → app#(app(eq, w), y)app#(app(member, w), app(app(app(fork, x), y), z)) → app#(app(app(if, app(app(eq, w), y)), true), app(app(member, w), z))
app#(app(lt, app(s, x)), app(s, y)) → app#(app(lt, x), y)app#(app(member, w), app(app(app(fork, x), y), z)) → app#(app(member, w), z)
app#(app(member, w), app(app(app(fork, x), y), z)) → app#(app(app(if, app(app(lt, w), y)), app(app(member, w), x)), app(app(app(if, app(app(eq, w), y)), true), app(app(member, w), z)))app#(app(member, w), app(app(app(fork, x), y), z)) → app#(app(lt, w), y)
app#(app(member, w), app(app(app(fork, x), y), z)) → app#(app(if, app(app(lt, w), y)), app(app(member, w), x))app#(app(member, w), app(app(app(fork, x), y), z)) → app#(app(member, w), x)

Rewrite Rules

app(app(lt, app(s, x)), app(s, y)) → app(app(lt, x), y)app(app(lt, 0), app(s, y)) → true
app(app(lt, y), 0) → falseapp(app(eq, x), x) → true
app(app(eq, app(s, x)), 0) → falseapp(app(eq, 0), app(s, x)) → false
app(app(member, w), null) → falseapp(app(member, w), app(app(app(fork, x), y), z)) → app(app(app(if, app(app(lt, w), y)), app(app(member, w), x)), app(app(app(if, app(app(eq, w), y)), true), app(app(member, w), z)))

Original Signature

Termination of terms over the following signature is verified: member, app, fork, 0, s, if, true, false, lt, null, eq

Strategy

Polynomial Interpretation

Improved Usable rules

app(app(lt, app(s, x)), app(s, y)) → app(app(lt, x), y)app(app(eq, app(s, x)), 0) → false
app(app(lt, 0), app(s, y)) → trueapp(app(eq, 0), app(s, x)) → false
app(app(member, w), app(app(app(fork, x), y), z)) → app(app(app(if, app(app(lt, w), y)), app(app(member, w), x)), app(app(app(if, app(app(eq, w), y)), true), app(app(member, w), z)))app(app(member, w), null) → false
app(app(lt, y), 0) → falseapp(app(eq, x), x) → true

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

app#(app(member, w), app(app(app(fork, x), y), z)) → app#(app(app(if, app(app(eq, w), y)), true), app(app(member, w), z))app#(app(member, w), app(app(app(fork, x), y), z)) → app#(app(app(if, app(app(lt, w), y)), app(app(member, w), x)), app(app(app(if, app(app(eq, w), y)), true), app(app(member, w), z)))
app#(app(member, w), app(app(app(fork, x), y), z)) → app#(app(if, app(app(lt, w), y)), app(app(member, w), x))

Problem 3: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

app#(app(member, w), app(app(app(fork, x), y), z)) → app#(app(eq, w), y)app#(app(lt, app(s, x)), app(s, y)) → app#(app(lt, x), y)
app#(app(member, w), app(app(app(fork, x), y), z)) → app#(app(member, w), z)app#(app(member, w), app(app(app(fork, x), y), z)) → app#(app(lt, w), y)
app#(app(member, w), app(app(app(fork, x), y), z)) → app#(app(member, w), x)

Rewrite Rules

app(app(lt, app(s, x)), app(s, y)) → app(app(lt, x), y)app(app(lt, 0), app(s, y)) → true
app(app(lt, y), 0) → falseapp(app(eq, x), x) → true
app(app(eq, app(s, x)), 0) → falseapp(app(eq, 0), app(s, x)) → false
app(app(member, w), null) → falseapp(app(member, w), app(app(app(fork, x), y), z)) → app(app(app(if, app(app(lt, w), y)), app(app(member, w), x)), app(app(app(if, app(app(eq, w), y)), true), app(app(member, w), z)))

Original Signature

Termination of terms over the following signature is verified: member, app, fork, 0, s, if, false, true, lt, null, eq

Strategy

Polynomial Interpretation

Improved Usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

app#(app(member, w), app(app(app(fork, x), y), z)) → app#(app(eq, w), y)app#(app(member, w), app(app(app(fork, x), y), z)) → app#(app(member, w), z)
app#(app(member, w), app(app(app(fork, x), y), z)) → app#(app(lt, w), y)app#(app(member, w), app(app(app(fork, x), y), z)) → app#(app(member, w), x)

Problem 4: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

app#(app(lt, app(s, x)), app(s, y)) → app#(app(lt, x), y)

Rewrite Rules

app(app(lt, app(s, x)), app(s, y)) → app(app(lt, x), y)app(app(lt, 0), app(s, y)) → true
app(app(lt, y), 0) → falseapp(app(eq, x), x) → true
app(app(eq, app(s, x)), 0) → falseapp(app(eq, 0), app(s, x)) → false
app(app(member, w), null) → falseapp(app(member, w), app(app(app(fork, x), y), z)) → app(app(app(if, app(app(lt, w), y)), app(app(member, w), x)), app(app(app(if, app(app(eq, w), y)), true), app(app(member, w), z)))

Original Signature

Termination of terms over the following signature is verified: member, app, fork, 0, s, if, true, false, lt, null, eq

Strategy

Polynomial Interpretation

Improved Usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

app#(app(lt, app(s, x)), app(s, y)) → app#(app(lt, x), y)