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 Induction-Processor (⇐)
↳27 AND
↳28 QDP
↳29 PisEmptyProof (⇔)
↳30 TRUE
↳31 QTRS
↳32 QTRSRRRProof (⇔)
↳33 QTRS
↳34 RisEmptyProof (⇔)
↳35 TRUE
↳36 RisEmptyProof (⇔)
↳37 TRUE
↳38 RisEmptyProof (⇔)
↳39 TRUE
leq(0, y) → true
leq(s(x), 0) → false
leq(s(x), s(y)) → leq(x, y)
if(true, x, y) → x
if(false, x, y) → y
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
mod(0, y) → 0
mod(s(x), 0) → 0
mod(s(x), s(y)) → if(leq(y, x), mod(-(s(x), s(y)), s(y)), s(x))
leq(0, y) → true
leq(s(x), 0) → false
leq(s(x), s(y)) → leq(x, y)
if(true, x, y) → x
if(false, x, y) → y
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
mod(0, y) → 0
mod(s(x), 0) → 0
mod(s(x), s(y)) → if(leq(y, x), mod(-(s(x), s(y)), s(y)), s(x))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
-(x0, 0)
-(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
LEQ(s(x), s(y)) → LEQ(x, y)
-1(s(x), s(y)) → -1(x, y)
MOD(s(x), s(y)) → IF(leq(y, x), mod(-(s(x), s(y)), s(y)), s(x))
MOD(s(x), s(y)) → LEQ(y, x)
MOD(s(x), s(y)) → MOD(-(s(x), s(y)), s(y))
MOD(s(x), s(y)) → -1(s(x), s(y))
leq(0, y) → true
leq(s(x), 0) → false
leq(s(x), s(y)) → leq(x, y)
if(true, x, y) → x
if(false, x, y) → y
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
mod(0, y) → 0
mod(s(x), 0) → 0
mod(s(x), s(y)) → if(leq(y, x), mod(-(s(x), s(y)), s(y)), s(x))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
-(x0, 0)
-(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
-1(s(x), s(y)) → -1(x, y)
leq(0, y) → true
leq(s(x), 0) → false
leq(s(x), s(y)) → leq(x, y)
if(true, x, y) → x
if(false, x, y) → y
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
mod(0, y) → 0
mod(s(x), 0) → 0
mod(s(x), s(y)) → if(leq(y, x), mod(-(s(x), s(y)), s(y)), s(x))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
-(x0, 0)
-(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
-1(s(x), s(y)) → -1(x, y)
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
-(x0, 0)
-(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
-(x0, 0)
-(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
-1(s(x), s(y)) → -1(x, y)
From the DPs we obtained the following set of size-change graphs:
LEQ(s(x), s(y)) → LEQ(x, y)
leq(0, y) → true
leq(s(x), 0) → false
leq(s(x), s(y)) → leq(x, y)
if(true, x, y) → x
if(false, x, y) → y
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
mod(0, y) → 0
mod(s(x), 0) → 0
mod(s(x), s(y)) → if(leq(y, x), mod(-(s(x), s(y)), s(y)), s(x))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
-(x0, 0)
-(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
LEQ(s(x), s(y)) → LEQ(x, y)
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
-(x0, 0)
-(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
-(x0, 0)
-(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
LEQ(s(x), s(y)) → LEQ(x, y)
From the DPs we obtained the following set of size-change graphs:
MOD(s(x), s(y)) → MOD(-(s(x), s(y)), s(y))
leq(0, y) → true
leq(s(x), 0) → false
leq(s(x), s(y)) → leq(x, y)
if(true, x, y) → x
if(false, x, y) → y
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
mod(0, y) → 0
mod(s(x), 0) → 0
mod(s(x), s(y)) → if(leq(y, x), mod(-(s(x), s(y)), s(y)), s(x))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
-(x0, 0)
-(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
MOD(s(x), s(y)) → MOD(-(s(x), s(y)), s(y))
-(s(x), s(y)) → -(x, y)
-(x, 0) → x
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
-(x0, 0)
-(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
MOD(s(x), s(y)) → MOD(-(s(x), s(y)), s(y))
-(s(x), s(y)) → -(x, y)
-(x, 0) → x
-(x0, 0)
-(s(x0), s(x1))
POL(-(x1, x2)) = x1
POL(0) = 0
POL(MOD(x1, x2)) = x1
POL(s(x1)) = 1 + x1
-(s(x), s(y)) → -(x, y)
-(x, 0) → x
-(x0, 0)
-(s(x0), s(x1))
-'(s(x), s(y)) → true
-'(x1, 0) → false
-'(0, s(x0)) → false
-'(s(x2), 0) → false
-(s(x), s(y)) → -(x, y)
-(x1, 0) → x1
-(0, s(x0)) → 0
-(s(x2), 0) → 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[a11](witness_sort[a11], witness_sort[a11]) → true
-'2 > true
-'2 > false
equalbool2 > true
not1 > true
not1 > false
isafalse1 > true
isafalse1 > false
equalsort[a0]2 > true
equalsort[a0]2 > false
equalsort[a11]2 > true
trivial
-'(s(x), s(y)) → true
-'(x1, 0) → false
-'(0, s(x0)) → false
-'(s(x2), 0) → false
-(s(x), s(y)) → -(x, y)
-(x1, 0) → x1
-(0, s(x0)) → 0
-(s(x2), 0) → 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[a11](witness_sort[a11], witness_sort[a11]) → true