MAYBE

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (0ms).
 | – Problem 2 was processed with processor SubtermCriterion (0ms).
 | – Problem 3 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (0ms), PolynomialLinearRange4iUR (65ms), DependencyGraph (1ms), PolynomialLinearRange8NegiUR (69ms), DependencyGraph (1ms), ReductionPairSAT (66ms), DependencyGraph (1ms), SizeChangePrinciple (6ms)].
 | – Problem 4 was processed with processor SubtermCriterion (0ms).

The following open problems remain:

Open Dependency Pair Problem 3

Dependency Pairs

fact#(X) → fact#(p(X))

Rewrite Rules

fact(X) → if(zero(X), n__s(0), n__prod(X, fact(p(X))))add(0, X) → X
add(s(X), Y) → s(add(X, Y))prod(0, X) → 0
prod(s(X), Y) → add(Y, prod(X, Y))if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)zero(0) → true
zero(s(X)) → falsep(s(X)) → X
s(X) → n__s(X)prod(X1, X2) → n__prod(X1, X2)
activate(n__s(X)) → s(X)activate(n__prod(X1, X2)) → prod(X1, X2)
activate(X) → X

Original Signature

Termination of terms over the following signature is verified: true, zero, add, n__s, activate, n__prod, 0, fact, s, if, p, false, prod

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

add#(s(X), Y) → add#(X, Y)prod#(s(X), Y) → prod#(X, Y)
prod#(s(X), Y) → add#(Y, prod(X, Y))fact#(X) → if#(zero(X), n__s(0), n__prod(X, fact(p(X))))
activate#(n__prod(X1, X2)) → prod#(X1, X2)if#(true, X, Y) → activate#(X)
if#(false, X, Y) → activate#(Y)fact#(X) → zero#(X)
fact#(X) → fact#(p(X))add#(s(X), Y) → s#(add(X, Y))
fact#(X) → p#(X)activate#(n__s(X)) → s#(X)

Rewrite Rules

fact(X) → if(zero(X), n__s(0), n__prod(X, fact(p(X))))add(0, X) → X
add(s(X), Y) → s(add(X, Y))prod(0, X) → 0
prod(s(X), Y) → add(Y, prod(X, Y))if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)zero(0) → true
zero(s(X)) → falsep(s(X)) → X
s(X) → n__s(X)prod(X1, X2) → n__prod(X1, X2)
activate(n__s(X)) → s(X)activate(n__prod(X1, X2)) → prod(X1, X2)
activate(X) → X

Original Signature

Termination of terms over the following signature is verified: true, zero, add, n__s, activate, n__prod, 0, fact, s, if, p, false, prod

Strategy

The following SCCs where found

add#(s(X), Y) → add#(X, Y)
prod#(s(X), Y) → prod#(X, Y)
fact#(X) → fact#(p(X))

Problem 2: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

add#(s(X), Y) → add#(X, Y)

Rewrite Rules

fact(X) → if(zero(X), n__s(0), n__prod(X, fact(p(X))))add(0, X) → X
add(s(X), Y) → s(add(X, Y))prod(0, X) → 0
prod(s(X), Y) → add(Y, prod(X, Y))if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)zero(0) → true
zero(s(X)) → falsep(s(X)) → X
s(X) → n__s(X)prod(X1, X2) → n__prod(X1, X2)
activate(n__s(X)) → s(X)activate(n__prod(X1, X2)) → prod(X1, X2)
activate(X) → X

Original Signature

Termination of terms over the following signature is verified: true, zero, add, n__s, activate, n__prod, 0, fact, s, if, p, false, prod

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

add#(s(X), Y) → add#(X, Y)

Problem 4: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

prod#(s(X), Y) → prod#(X, Y)

Rewrite Rules

fact(X) → if(zero(X), n__s(0), n__prod(X, fact(p(X))))add(0, X) → X
add(s(X), Y) → s(add(X, Y))prod(0, X) → 0
prod(s(X), Y) → add(Y, prod(X, Y))if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)zero(0) → true
zero(s(X)) → falsep(s(X)) → X
s(X) → n__s(X)prod(X1, X2) → n__prod(X1, X2)
activate(n__s(X)) → s(X)activate(n__prod(X1, X2)) → prod(X1, X2)
activate(X) → X

Original Signature

Termination of terms over the following signature is verified: true, zero, add, n__s, activate, n__prod, 0, fact, s, if, p, false, prod

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

prod#(s(X), Y) → prod#(X, Y)