0 QTRS
↳1 Overlay + Local Confluence (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔)
↳9 QDP
↳10 QReductionProof (⇔)
↳11 QDP
↳12 QDPSizeChangeProof (⇔)
↳13 TRUE
↳14 QDP
↳15 UsableRulesProof (⇔)
↳16 QDP
↳17 QReductionProof (⇔)
↳18 QDP
↳19 QDPSizeChangeProof (⇔)
↳20 TRUE
↳21 QDP
↳22 UsableRulesProof (⇔)
↳23 QDP
↳24 QReductionProof (⇔)
↳25 QDP
↳26 QDPSizeChangeProof (⇔)
↳27 TRUE
↳28 QDP
↳29 UsableRulesProof (⇔)
↳30 QDP
↳31 QReductionProof (⇔)
↳32 QDP
↳33 Instantiation (⇔)
↳34 QDP
↳35 NonInfProof (⇔)
↳36 QDP
↳37 DependencyGraphProof (⇔)
↳38 TRUE
lt(0, s(x)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
fac(x) → loop(x, s(0), s(0))
loop(x, c, y) → if(lt(x, c), x, c, y)
if(false, x, c, y) → loop(x, s(c), times(y, s(c)))
if(true, x, c, y) → y
lt(0, s(x)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
fac(x) → loop(x, s(0), s(0))
loop(x, c, y) → if(lt(x, c), x, c, y)
if(false, x, c, y) → loop(x, s(c), times(y, s(c)))
if(true, x, c, y) → y
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
times(0, x0)
times(s(x0), x1)
plus(0, x0)
plus(s(x0), x1)
fac(x0)
loop(x0, x1, x2)
if(false, x0, x1, x2)
if(true, x0, x1, x2)
LT(s(x), s(y)) → LT(x, y)
TIMES(s(x), y) → PLUS(y, times(x, y))
TIMES(s(x), y) → TIMES(x, y)
PLUS(s(x), y) → PLUS(x, y)
FAC(x) → LOOP(x, s(0), s(0))
LOOP(x, c, y) → IF(lt(x, c), x, c, y)
LOOP(x, c, y) → LT(x, c)
IF(false, x, c, y) → LOOP(x, s(c), times(y, s(c)))
IF(false, x, c, y) → TIMES(y, s(c))
lt(0, s(x)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
fac(x) → loop(x, s(0), s(0))
loop(x, c, y) → if(lt(x, c), x, c, y)
if(false, x, c, y) → loop(x, s(c), times(y, s(c)))
if(true, x, c, y) → y
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
times(0, x0)
times(s(x0), x1)
plus(0, x0)
plus(s(x0), x1)
fac(x0)
loop(x0, x1, x2)
if(false, x0, x1, x2)
if(true, x0, x1, x2)
PLUS(s(x), y) → PLUS(x, y)
lt(0, s(x)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
fac(x) → loop(x, s(0), s(0))
loop(x, c, y) → if(lt(x, c), x, c, y)
if(false, x, c, y) → loop(x, s(c), times(y, s(c)))
if(true, x, c, y) → y
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
times(0, x0)
times(s(x0), x1)
plus(0, x0)
plus(s(x0), x1)
fac(x0)
loop(x0, x1, x2)
if(false, x0, x1, x2)
if(true, x0, x1, x2)
PLUS(s(x), y) → PLUS(x, y)
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
times(0, x0)
times(s(x0), x1)
plus(0, x0)
plus(s(x0), x1)
fac(x0)
loop(x0, x1, x2)
if(false, x0, x1, x2)
if(true, x0, x1, x2)
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
times(0, x0)
times(s(x0), x1)
plus(0, x0)
plus(s(x0), x1)
fac(x0)
loop(x0, x1, x2)
if(false, x0, x1, x2)
if(true, x0, x1, x2)
PLUS(s(x), y) → PLUS(x, y)
From the DPs we obtained the following set of size-change graphs:
TIMES(s(x), y) → TIMES(x, y)
lt(0, s(x)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
fac(x) → loop(x, s(0), s(0))
loop(x, c, y) → if(lt(x, c), x, c, y)
if(false, x, c, y) → loop(x, s(c), times(y, s(c)))
if(true, x, c, y) → y
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
times(0, x0)
times(s(x0), x1)
plus(0, x0)
plus(s(x0), x1)
fac(x0)
loop(x0, x1, x2)
if(false, x0, x1, x2)
if(true, x0, x1, x2)
TIMES(s(x), y) → TIMES(x, y)
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
times(0, x0)
times(s(x0), x1)
plus(0, x0)
plus(s(x0), x1)
fac(x0)
loop(x0, x1, x2)
if(false, x0, x1, x2)
if(true, x0, x1, x2)
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
times(0, x0)
times(s(x0), x1)
plus(0, x0)
plus(s(x0), x1)
fac(x0)
loop(x0, x1, x2)
if(false, x0, x1, x2)
if(true, x0, x1, x2)
TIMES(s(x), y) → TIMES(x, y)
From the DPs we obtained the following set of size-change graphs:
LT(s(x), s(y)) → LT(x, y)
lt(0, s(x)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
fac(x) → loop(x, s(0), s(0))
loop(x, c, y) → if(lt(x, c), x, c, y)
if(false, x, c, y) → loop(x, s(c), times(y, s(c)))
if(true, x, c, y) → y
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
times(0, x0)
times(s(x0), x1)
plus(0, x0)
plus(s(x0), x1)
fac(x0)
loop(x0, x1, x2)
if(false, x0, x1, x2)
if(true, x0, x1, x2)
LT(s(x), s(y)) → LT(x, y)
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
times(0, x0)
times(s(x0), x1)
plus(0, x0)
plus(s(x0), x1)
fac(x0)
loop(x0, x1, x2)
if(false, x0, x1, x2)
if(true, x0, x1, x2)
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
times(0, x0)
times(s(x0), x1)
plus(0, x0)
plus(s(x0), x1)
fac(x0)
loop(x0, x1, x2)
if(false, x0, x1, x2)
if(true, x0, x1, x2)
LT(s(x), s(y)) → LT(x, y)
From the DPs we obtained the following set of size-change graphs:
LOOP(x, c, y) → IF(lt(x, c), x, c, y)
IF(false, x, c, y) → LOOP(x, s(c), times(y, s(c)))
lt(0, s(x)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
fac(x) → loop(x, s(0), s(0))
loop(x, c, y) → if(lt(x, c), x, c, y)
if(false, x, c, y) → loop(x, s(c), times(y, s(c)))
if(true, x, c, y) → y
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
times(0, x0)
times(s(x0), x1)
plus(0, x0)
plus(s(x0), x1)
fac(x0)
loop(x0, x1, x2)
if(false, x0, x1, x2)
if(true, x0, x1, x2)
LOOP(x, c, y) → IF(lt(x, c), x, c, y)
IF(false, x, c, y) → LOOP(x, s(c), times(y, s(c)))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
lt(0, s(x)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
times(0, x0)
times(s(x0), x1)
plus(0, x0)
plus(s(x0), x1)
fac(x0)
loop(x0, x1, x2)
if(false, x0, x1, x2)
if(true, x0, x1, x2)
fac(x0)
loop(x0, x1, x2)
if(false, x0, x1, x2)
if(true, x0, x1, x2)
LOOP(x, c, y) → IF(lt(x, c), x, c, y)
IF(false, x, c, y) → LOOP(x, s(c), times(y, s(c)))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
lt(0, s(x)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
times(0, x0)
times(s(x0), x1)
plus(0, x0)
plus(s(x0), x1)
LOOP(z0, s(z1), y_0) → IF(lt(z0, s(z1)), z0, s(z1), y_0)
IF(false, x, c, y) → LOOP(x, s(c), times(y, s(c)))
LOOP(z0, s(z1), y_0) → IF(lt(z0, s(z1)), z0, s(z1), y_0)
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
lt(0, s(x)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
times(0, x0)
times(s(x0), x1)
plus(0, x0)
plus(s(x0), x1)
(1) (LOOP(x3, s(x4), times(x5, s(x4)))=LOOP(x6, x7, x8) ⇒ LOOP(x6, x7, x8)≥IF(lt(x6, x7), x6, x7, x8))
(2) (LOOP(x3, s(x4), x8)≥IF(lt(x3, s(x4)), x3, s(x4), x8))
(3) (IF(lt(x9, x10), x9, x10, x11)=IF(false, x12, x13, x14) ⇒ IF(false, x12, x13, x14)≥LOOP(x12, s(x13), times(x14, s(x13))))
(4) (lt(x9, x10)=false ⇒ IF(false, x9, x10, x11)≥LOOP(x9, s(x10), times(x11, s(x10))))
(5) (false=false ⇒ IF(false, x20, 0, x11)≥LOOP(x20, s(0), times(x11, s(0))))
(6) (lt(x22, x21)=false∧(∀x23:lt(x22, x21)=false ⇒ IF(false, x22, x21, x23)≥LOOP(x22, s(x21), times(x23, s(x21)))) ⇒ IF(false, s(x22), s(x21), x11)≥LOOP(s(x22), s(s(x21)), times(x11, s(s(x21)))))
(7) (IF(false, x20, 0, x11)≥LOOP(x20, s(0), times(x11, s(0))))
(8) (IF(false, x22, x21, x11)≥LOOP(x22, s(x21), times(x11, s(x21))) ⇒ IF(false, s(x22), s(x21), x11)≥LOOP(s(x22), s(s(x21)), times(x11, s(s(x21)))))
POL(0) = 1
POL(IF(x1, x2, x3, x4)) = -1 - x1 + x2 - x3
POL(LOOP(x1, x2, x3)) = -1 + x1 - x2
POL(c) = -2
POL(false) = 0
POL(lt(x1, x2)) = 0
POL(plus(x1, x2)) = 0
POL(s(x1)) = 1 + x1
POL(times(x1, x2)) = 0
POL(true) = 0
The following pairs are in Pbound:
IF(false, x, c, y) → LOOP(x, s(c), times(y, s(c)))
The following rules are usable:
IF(false, x, c, y) → LOOP(x, s(c), times(y, s(c)))
true → lt(0, s(x))
lt(x, y) → lt(s(x), s(y))
false → lt(x, 0)
LOOP(x, c, y) → IF(lt(x, c), x, c, y)
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
lt(0, s(x)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
times(0, x0)
times(s(x0), x1)
plus(0, x0)
plus(s(x0), x1)