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 Instantiation (⇔)
↳27 QDP
↳28 Induction-Processor (⇐)
↳29 AND
↳30 QDP
↳31 DependencyGraphProof (⇔)
↳32 TRUE
↳33 QTRS
↳34 QTRSRRRProof (⇔)
↳35 QTRS
↳36 QTRSRRRProof (⇔)
↳37 QTRS
↳38 RisEmptyProof (⇔)
↳39 TRUE
↳40 RisEmptyProof (⇔)
↳41 TRUE
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
mod(0, y) → 0
mod(s(x), 0) → 0
mod(s(x), s(y)) → if_mod(le(y, x), s(x), s(y))
if_mod(true, x, y) → mod(minus(x, y), y)
if_mod(false, s(x), s(y)) → s(x)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
mod(0, y) → 0
mod(s(x), 0) → 0
mod(s(x), s(y)) → if_mod(le(y, x), s(x), s(y))
if_mod(true, x, y) → mod(minus(x, y), y)
if_mod(false, s(x), s(y)) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
if_mod(true, x0, x1)
if_mod(false, s(x0), s(x1))
LE(s(x), s(y)) → LE(x, y)
MINUS(s(x), s(y)) → MINUS(x, y)
MOD(s(x), s(y)) → IF_MOD(le(y, x), s(x), s(y))
MOD(s(x), s(y)) → LE(y, x)
IF_MOD(true, x, y) → MOD(minus(x, y), y)
IF_MOD(true, x, y) → MINUS(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
mod(0, y) → 0
mod(s(x), 0) → 0
mod(s(x), s(y)) → if_mod(le(y, x), s(x), s(y))
if_mod(true, x, y) → mod(minus(x, y), y)
if_mod(false, s(x), s(y)) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
if_mod(true, x0, x1)
if_mod(false, s(x0), s(x1))
MINUS(s(x), s(y)) → MINUS(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
mod(0, y) → 0
mod(s(x), 0) → 0
mod(s(x), s(y)) → if_mod(le(y, x), s(x), s(y))
if_mod(true, x, y) → mod(minus(x, y), y)
if_mod(false, s(x), s(y)) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
if_mod(true, x0, x1)
if_mod(false, s(x0), s(x1))
MINUS(s(x), s(y)) → MINUS(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
if_mod(true, x0, x1)
if_mod(false, s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
if_mod(true, x0, x1)
if_mod(false, s(x0), s(x1))
MINUS(s(x), s(y)) → MINUS(x, y)
From the DPs we obtained the following set of size-change graphs:
LE(s(x), s(y)) → LE(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
mod(0, y) → 0
mod(s(x), 0) → 0
mod(s(x), s(y)) → if_mod(le(y, x), s(x), s(y))
if_mod(true, x, y) → mod(minus(x, y), y)
if_mod(false, s(x), s(y)) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
if_mod(true, x0, x1)
if_mod(false, s(x0), s(x1))
LE(s(x), s(y)) → LE(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
if_mod(true, x0, x1)
if_mod(false, s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
if_mod(true, x0, x1)
if_mod(false, s(x0), s(x1))
LE(s(x), s(y)) → LE(x, y)
From the DPs we obtained the following set of size-change graphs:
MOD(s(x), s(y)) → IF_MOD(le(y, x), s(x), s(y))
IF_MOD(true, x, y) → MOD(minus(x, y), y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
mod(0, y) → 0
mod(s(x), 0) → 0
mod(s(x), s(y)) → if_mod(le(y, x), s(x), s(y))
if_mod(true, x, y) → mod(minus(x, y), y)
if_mod(false, s(x), s(y)) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
if_mod(true, x0, x1)
if_mod(false, s(x0), s(x1))
MOD(s(x), s(y)) → IF_MOD(le(y, x), s(x), s(y))
IF_MOD(true, x, y) → MOD(minus(x, y), y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
if_mod(true, x0, x1)
if_mod(false, s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
if_mod(true, x0, x1)
if_mod(false, s(x0), s(x1))
MOD(s(x), s(y)) → IF_MOD(le(y, x), s(x), s(y))
IF_MOD(true, x, y) → MOD(minus(x, y), y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
IF_MOD(true, s(z0), s(z1)) → MOD(minus(s(z0), s(z1)), s(z1))
MOD(s(x), s(y)) → IF_MOD(le(y, x), s(x), s(y))
IF_MOD(true, s(z0), s(z1)) → MOD(minus(s(z0), s(z1)), s(z1))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
POL(0) = 0
POL(IF_MOD(x1, x2, x3)) = x2
POL(MOD(x1, x2)) = x1
POL(false) = 0
POL(le(x1, x2)) = x2
POL(minus(x1, x2)) = x1
POL(s(x1)) = 1 + x1
POL(true) = 0
MOD(s(x), s(y)) → IF_MOD(le(y, x), s(x), s(y))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
minus'(x, 0) → false
minus'(s(x3), s(y1)) → true
minus'(0, s(x0)) → false
minus(x, 0) → x
minus(s(x3), s(y1)) → minus(x3, y1)
le(0, y5) → true
le(s(x12), 0) → false
le(s(x17), s(y12)) → le(x17, y12)
minus(0, s(x0)) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a23](witness_sort[a23], witness_sort[a23]) → true
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(0) = 0
POL(and(x1, x2)) = 2·x1 + x2
POL(equal_bool(x1, x2)) = 2·x1 + x2
POL(equal_sort[a0](x1, x2)) = 1 + x1 + 2·x2
POL(equal_sort[a23](x1, x2)) = 2 + 2·x1 + x2
POL(false) = 1
POL(isa_false(x1)) = 2 + x1
POL(isa_true(x1)) = 2 + x1
POL(le(x1, x2)) = 1 + 2·x1 + 2·x2
POL(minus(x1, x2)) = 2·x1 + 2·x2
POL(minus'(x1, x2)) = 1 + 2·x1 + x2
POL(not(x1)) = 2·x1
POL(or(x1, x2)) = x1 + x2
POL(s(x1)) = 2 + 2·x1
POL(true) = 1
POL(witness_sort[a23]) = 2
minus'(s(x3), s(y1)) → true
minus'(0, s(x0)) → false
minus(s(x3), s(y1)) → minus(x3, y1)
le(s(x12), 0) → false
le(s(x17), s(y12)) → le(x17, y12)
minus(0, s(x0)) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a23](witness_sort[a23], witness_sort[a23]) → true
minus'(x, 0) → false
minus(x, 0) → x
le(0, y5) → true
or(true, x) → true
equal_sort[a0](0, 0) → true
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(0) = 0
POL(equal_sort[a0](x1, x2)) = 1 + x1 + x2
POL(false) = 0
POL(le(x1, x2)) = 1 + x1 + x2
POL(minus(x1, x2)) = 1 + x1 + x2
POL(minus'(x1, x2)) = 1 + x1 + x2
POL(or(x1, x2)) = 1 + x1 + x2
POL(true) = 0
minus'(x, 0) → false
minus(x, 0) → x
le(0, y5) → true
or(true, x) → true
equal_sort[a0](0, 0) → true