YES
0 QTRS
↳1 Overlay + Local Confluence (⇔, 0 ms)
↳2 QTRS
↳3 DependencyPairsProof (⇔, 0 ms)
↳4 QDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 QDP
↳10 QReductionProof (⇔, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 QDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 QDP
↳17 QReductionProof (⇔, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 QDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 QDP
↳24 QReductionProof (⇔, 0 ms)
↳25 QDP
↳26 QDPOrderProof (⇔, 0 ms)
↳27 QDP
↳28 PisEmptyProof (⇔, 0 ms)
↳29 YES
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
lt(x, 0) → false
lt(0, s(y)) → true
lt(s(x), s(y)) → lt(x, y)
if(true, x, y) → x
if(false, x, y) → y
div(x, 0) → 0
div(0, y) → 0
div(s(x), s(y)) → if(lt(x, y), 0, s(div(-(x, y), s(y))))
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
lt(x, 0) → false
lt(0, s(y)) → true
lt(s(x), s(y)) → lt(x, y)
if(true, x, y) → x
if(false, x, y) → y
div(x, 0) → 0
div(0, y) → 0
div(s(x), s(y)) → if(lt(x, y), 0, s(div(-(x, y), s(y))))
-(x0, 0)
-(0, s(x0))
-(s(x0), s(x1))
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
div(x0, 0)
div(0, x0)
div(s(x0), s(x1))
-1(s(x), s(y)) → -1(x, y)
LT(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)) → LT(x, y)
DIV(s(x), s(y)) → DIV(-(x, y), s(y))
DIV(s(x), s(y)) → -1(x, y)
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
lt(x, 0) → false
lt(0, s(y)) → true
lt(s(x), s(y)) → lt(x, y)
if(true, x, y) → x
if(false, x, y) → y
div(x, 0) → 0
div(0, y) → 0
div(s(x), s(y)) → if(lt(x, y), 0, s(div(-(x, y), s(y))))
-(x0, 0)
-(0, s(x0))
-(s(x0), s(x1))
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
div(x0, 0)
div(0, x0)
div(s(x0), s(x1))
LT(s(x), s(y)) → LT(x, y)
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
lt(x, 0) → false
lt(0, s(y)) → true
lt(s(x), s(y)) → lt(x, y)
if(true, x, y) → x
if(false, x, y) → y
div(x, 0) → 0
div(0, y) → 0
div(s(x), s(y)) → if(lt(x, y), 0, s(div(-(x, y), s(y))))
-(x0, 0)
-(0, s(x0))
-(s(x0), s(x1))
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
div(x0, 0)
div(0, x0)
div(s(x0), s(x1))
LT(s(x), s(y)) → LT(x, y)
-(x0, 0)
-(0, s(x0))
-(s(x0), s(x1))
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
div(x0, 0)
div(0, x0)
div(s(x0), s(x1))
-(x0, 0)
-(0, s(x0))
-(s(x0), s(x1))
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
div(x0, 0)
div(0, x0)
div(s(x0), s(x1))
LT(s(x), s(y)) → LT(x, y)
From the DPs we obtained the following set of size-change graphs:
-1(s(x), s(y)) → -1(x, y)
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
lt(x, 0) → false
lt(0, s(y)) → true
lt(s(x), s(y)) → lt(x, y)
if(true, x, y) → x
if(false, x, y) → y
div(x, 0) → 0
div(0, y) → 0
div(s(x), s(y)) → if(lt(x, y), 0, s(div(-(x, y), s(y))))
-(x0, 0)
-(0, s(x0))
-(s(x0), s(x1))
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
div(x0, 0)
div(0, x0)
div(s(x0), s(x1))
-1(s(x), s(y)) → -1(x, y)
-(x0, 0)
-(0, s(x0))
-(s(x0), s(x1))
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
div(x0, 0)
div(0, x0)
div(s(x0), s(x1))
-(x0, 0)
-(0, s(x0))
-(s(x0), s(x1))
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
div(x0, 0)
div(0, x0)
div(s(x0), s(x1))
-1(s(x), s(y)) → -1(x, y)
From the DPs we obtained the following set of size-change graphs:
DIV(s(x), s(y)) → DIV(-(x, y), s(y))
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
lt(x, 0) → false
lt(0, s(y)) → true
lt(s(x), s(y)) → lt(x, y)
if(true, x, y) → x
if(false, x, y) → y
div(x, 0) → 0
div(0, y) → 0
div(s(x), s(y)) → if(lt(x, y), 0, s(div(-(x, y), s(y))))
-(x0, 0)
-(0, s(x0))
-(s(x0), s(x1))
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
div(x0, 0)
div(0, x0)
div(s(x0), s(x1))
DIV(s(x), s(y)) → DIV(-(x, y), s(y))
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
-(x0, 0)
-(0, s(x0))
-(s(x0), s(x1))
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
div(x0, 0)
div(0, x0)
div(s(x0), s(x1))
lt(x0, 0)
lt(0, s(x0))
lt(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
div(x0, 0)
div(0, x0)
div(s(x0), s(x1))
DIV(s(x), s(y)) → DIV(-(x, y), s(y))
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
-(x0, 0)
-(0, s(x0))
-(s(x0), s(x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
DIV(s(x), s(y)) → DIV(-(x, y), s(y))
trivial
s_1=1
0=1
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
-(x0, 0)
-(0, s(x0))
-(s(x0), s(x1))