TIMEOUT

The TRS could not be proven terminating. The proof attempt took 60000 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (21ms).
 | – Problem 2 was processed with processor BackwardInstantiation (1ms).
 |    | – Problem 4 was processed with processor BackwardInstantiation (5ms).
 |    |    | – Problem 5 was processed with processor Propagation (2ms).
 |    |    |    | – Problem 6 remains open; application of the following processors failed [ForwardNarrowing (1ms), BackwardInstantiation (1ms), ForwardInstantiation (0ms), Propagation (0ms)].
 | – Problem 3 was processed with processor SubtermCriterion (2ms).

The following open problems remain:



Open Dependency Pair Problem 2

Dependency Pairs

cond#(true, x, y)minus#(x, s(y))minus#(x, y)cond#(ge(x, s(y)), x, y)

Rewrite Rules

minus(x, y)cond(ge(x, s(y)), x, y)cond(false, x, y)0
cond(true, x, y)s(minus(x, s(y)))ge(u, 0)true
ge(0, s(v))falsege(s(u), s(v))ge(u, v)

Original Signature

Termination of terms over the following signature is verified: 0, minus, s, true, false, ge, cond


Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

minus#(x, y)ge#(x, s(y))cond#(true, x, y)minus#(x, s(y))
minus#(x, y)cond#(ge(x, s(y)), x, y)ge#(s(u), s(v))ge#(u, v)

Rewrite Rules

minus(x, y)cond(ge(x, s(y)), x, y)cond(false, x, y)0
cond(true, x, y)s(minus(x, s(y)))ge(u, 0)true
ge(0, s(v))falsege(s(u), s(v))ge(u, v)

Original Signature

Termination of terms over the following signature is verified: minus, 0, s, false, true, ge, cond

Strategy


The following SCCs where found

ge#(s(u), s(v)) → ge#(u, v)

cond#(true, x, y) → minus#(x, s(y))minus#(x, y) → cond#(ge(x, s(y)), x, y)

Problem 2: BackwardInstantiation



Dependency Pair Problem

Dependency Pairs

cond#(true, x, y)minus#(x, s(y))minus#(x, y)cond#(ge(x, s(y)), x, y)

Rewrite Rules

minus(x, y)cond(ge(x, s(y)), x, y)cond(false, x, y)0
cond(true, x, y)s(minus(x, s(y)))ge(u, 0)true
ge(0, s(v))falsege(s(u), s(v))ge(u, v)

Original Signature

Termination of terms over the following signature is verified: minus, 0, s, false, true, ge, cond

Strategy


Instantiation

For all potential predecessors l → r of the rule minus#(x, y) → cond#(ge(x, s(y)), x, y) on dependency pair chains it holds that: Thus, minus#(x, y) → cond#(ge(x, s(y)), x, y) is replaced by instances determined through the above matching. These instances are:
minus#(_x, s(_y)) → cond#(ge(_x, s(s(_y))), _x, s(_y))

Problem 4: BackwardInstantiation



Dependency Pair Problem

Dependency Pairs

cond#(true, x, y)minus#(x, s(y))minus#(_x, s(_y))cond#(ge(_x, s(s(_y))), _x, s(_y))

Rewrite Rules

minus(x, y)cond(ge(x, s(y)), x, y)cond(false, x, y)0
cond(true, x, y)s(minus(x, s(y)))ge(u, 0)true
ge(0, s(v))falsege(s(u), s(v))ge(u, v)

Original Signature

Termination of terms over the following signature is verified: 0, minus, s, true, false, ge, cond

Strategy


Instantiation

For all potential predecessors l → r of the rule minus#(_x, s(_y)) → cond#(ge(_x, s(s(_y))), _x, s(_y)) on dependency pair chains it holds that: Thus, minus#(_x, s(_y)) → cond#(ge(_x, s(s(_y))), _x, s(_y)) is replaced by instances determined through the above matching. These instances are:
minus#(x, s(y)) → cond#(ge(x, s(s(y))), x, s(y))

Problem 5: Propagation



Dependency Pair Problem

Dependency Pairs

cond#(true, x, y)minus#(x, s(y))minus#(x, s(y))cond#(ge(x, s(s(y))), x, s(y))

Rewrite Rules

minus(x, y)cond(ge(x, s(y)), x, y)cond(false, x, y)0
cond(true, x, y)s(minus(x, s(y)))ge(u, 0)true
ge(0, s(v))falsege(s(u), s(v))ge(u, v)

Original Signature

Termination of terms over the following signature is verified: minus, 0, s, false, true, ge, cond

Strategy


The dependency pairs cond#(true, x, y) → minus#(x, s(y)) and minus#(x, s(y)) → cond#(ge(x, s(s(y))), x, s(y)) are consolidated into the rule cond#(true, x, y) → cond#(ge(x, s(s(y))), x, s(y)) .

This is possible as

The dependency pairs cond#(true, x, y) → minus#(x, s(y)) and minus#(x, s(y)) → cond#(ge(x, s(s(y))), x, s(y)) are consolidated into the rule cond#(true, x, y) → cond#(ge(x, s(s(y))), x, s(y)) .

This is possible as


Summary

Removed Dependency PairsAdded Dependency Pairs
cond#(true, x, y) → minus#(x, s(y))cond#(true, x, y) → cond#(ge(x, s(s(y))), x, s(y))
minus#(x, s(y)) → cond#(ge(x, s(s(y))), x, s(y)) 

Problem 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

ge#(s(u), s(v))ge#(u, v)

Rewrite Rules

minus(x, y)cond(ge(x, s(y)), x, y)cond(false, x, y)0
cond(true, x, y)s(minus(x, s(y)))ge(u, 0)true
ge(0, s(v))falsege(s(u), s(v))ge(u, v)

Original Signature

Termination of terms over the following signature is verified: minus, 0, s, false, true, ge, cond

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

ge#(s(u), s(v))ge#(u, v)