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 QTRSRRRProof (⇔)
↳35 QTRS
↳36 QTRSRRRProof (⇔)
↳37 QTRS
↳38 QTRSRRRProof (⇔)
↳39 QTRS
↳40 QTRSRRRProof (⇔)
↳41 QTRS
↳42 RisEmptyProof (⇔)
↳43 TRUE
↳44 RisEmptyProof (⇔)
↳45 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
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(-(x1, x2)) = x1 + x2
POL(-'(x1, x2)) = 1 + x1 + x2
POL(0) = 1
POL(and(x1, x2)) = 1 + x1 + x2
POL(equal_bool(x1, x2)) = x1 + x2
POL(equal_sort[a0](x1, x2)) = 1 + x1 + x2
POL(equal_sort[a11](x1, x2)) = 1 + x1 + x2
POL(false) = 2
POL(isa_false(x1)) = 3 + x1
POL(isa_true(x1)) = x1
POL(not(x1)) = 3 + x1
POL(or(x1, x2)) = 1 + x1 + x2
POL(s(x1)) = x1
POL(true) = 0
POL(witness_sort[a11]) = 0
-'(s(x), s(y)) → true
-(x1, 0) → x1
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_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a11](witness_sort[a11], witness_sort[a11]) → true
-'(x1, 0) → false
-'(0, s(x0)) → false
-'(s(x2), 0) → false
-(s(x), s(y)) → -(x, y)
-(0, s(x0)) → 0
-(s(x2), 0) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
isa_true(true) → true
isa_true(false) → false
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)
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(-(x1, x2)) = x1 + x2
POL(-'(x1, x2)) = 1 + x1 + x2
POL(0) = 0
POL(equal_bool(x1, x2)) = x1 + x2
POL(equal_sort[a0](x1, x2)) = x1 + x2
POL(false) = 0
POL(isa_true(x1)) = x1
POL(s(x1)) = x1
POL(true) = 0
-'(x1, 0) → false
-'(0, s(x0)) → false
-'(s(x2), 0) → false
-(s(x), s(y)) → -(x, y)
-(0, s(x0)) → 0
-(s(x2), 0) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
isa_true(true) → true
isa_true(false) → false
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)
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(-(x1, x2)) = 1 + x1 + x2
POL(0) = 0
POL(equal_bool(x1, x2)) = x1 + x2
POL(equal_sort[a0](x1, x2)) = x1 + x2
POL(false) = 0
POL(isa_true(x1)) = x1
POL(s(x1)) = x1
POL(true) = 0
-(0, s(x0)) → 0
-(s(x2), 0) → 0
-(s(x), s(y)) → -(x, y)
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
isa_true(true) → true
isa_true(false) → false
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)
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(-(x1, x2)) = x1 + x2
POL(0) = 0
POL(equal_bool(x1, x2)) = 1 + x1 + x2
POL(equal_sort[a0](x1, x2)) = x1 + x2
POL(false) = 0
POL(isa_true(x1)) = x1
POL(s(x1)) = x1
POL(true) = 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
-(s(x), s(y)) → -(x, y)
isa_true(true) → true
isa_true(false) → false
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)
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(-(x1, x2)) = 2·x1 + x2
POL(0) = 2
POL(equal_sort[a0](x1, x2)) = 1 + x1 + x2
POL(false) = 1
POL(isa_true(x1)) = 2 + 2·x1
POL(s(x1)) = 1 + 2·x1
POL(true) = 1
-(s(x), s(y)) → -(x, y)
isa_true(true) → true
isa_true(false) → false
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)