YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (19ms).
 | – Problem 2 was processed with processor SubtermCriterion (2ms).
 | – Problem 3 was processed with processor PolynomialLinearRange4iUR (156ms).
 | – Problem 4 was processed with processor SubtermCriterion (1ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

div#(s(x), s(y))lt#(x, y)div#(s(x), s(y))if#(lt(x, y), 0, s(div(-(x, y), s(y))))
div#(s(x), s(y))-#(x, y)lt#(s(x), s(y))lt#(x, y)
-#(s(x), s(y))-#(x, y)div#(s(x), s(y))div#(-(x, y), s(y))

Rewrite Rules

-(x, 0)x-(0, s(y))0
-(s(x), s(y))-(x, y)lt(x, 0)false
lt(0, s(y))truelt(s(x), s(y))lt(x, y)
if(true, x, y)xif(false, x, y)y
div(x, 0)0div(0, y)0
div(s(x), s(y))if(lt(x, y), 0, s(div(-(x, y), s(y))))

Original Signature

Termination of terms over the following signature is verified: 0, s, if, div, false, true, lt, -

Strategy


The following SCCs where found

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

div#(s(x), s(y)) → div#(-(x, y), s(y))

-#(s(x), s(y)) → -#(x, y)

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

-(x, 0)x-(0, s(y))0
-(s(x), s(y))-(x, y)lt(x, 0)false
lt(0, s(y))truelt(s(x), s(y))lt(x, y)
if(true, x, y)xif(false, x, y)y
div(x, 0)0div(0, y)0
div(s(x), s(y))if(lt(x, y), 0, s(div(-(x, y), s(y))))

Original Signature

Termination of terms over the following signature is verified: 0, s, if, div, false, true, lt, -

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 3: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

div#(s(x), s(y))div#(-(x, y), s(y))

Rewrite Rules

-(x, 0)x-(0, s(y))0
-(s(x), s(y))-(x, y)lt(x, 0)false
lt(0, s(y))truelt(s(x), s(y))lt(x, y)
if(true, x, y)xif(false, x, y)y
div(x, 0)0div(0, y)0
div(s(x), s(y))if(lt(x, y), 0, s(div(-(x, y), s(y))))

Original Signature

Termination of terms over the following signature is verified: 0, s, if, div, false, true, lt, -

Strategy


Polynomial Interpretation

Improved Usable rules

-(s(x), s(y))-(x, y)-(x, 0)x
-(0, s(y))0

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

div#(s(x), s(y))div#(-(x, y), s(y))

Problem 4: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

-#(s(x), s(y))-#(x, y)

Rewrite Rules

-(x, 0)x-(0, s(y))0
-(s(x), s(y))-(x, y)lt(x, 0)false
lt(0, s(y))truelt(s(x), s(y))lt(x, y)
if(true, x, y)xif(false, x, y)y
div(x, 0)0div(0, y)0
div(s(x), s(y))if(lt(x, y), 0, s(div(-(x, y), s(y))))

Original Signature

Termination of terms over the following signature is verified: 0, s, if, div, false, true, lt, -

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

-#(s(x), s(y))-#(x, y)