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 QDPOrderProof (⇔)
↳34 QDP
↳35 PisEmptyProof (⇔)
↳36 TRUE
↳37 QDP
↳38 UsableRulesProof (⇔)
↳39 QDP
↳40 QReductionProof (⇔)
↳41 QDP
↳42 Induction-Processor (⇐)
↳43 AND
↳44 QDP
↳45 DependencyGraphProof (⇔)
↳46 TRUE
↳47 QTRS
↳48 Overlay + Local Confluence (⇔)
↳49 QTRS
↳50 DependencyPairsProof (⇔)
↳51 QDP
↳52 DependencyGraphProof (⇔)
↳53 AND
↳54 QDP
↳55 UsableRulesProof (⇔)
↳56 QDP
↳57 QReductionProof (⇔)
↳58 QDP
↳59 QDPSizeChangeProof (⇔)
↳60 TRUE
↳61 QDP
↳62 UsableRulesProof (⇔)
↳63 QDP
↳64 QReductionProof (⇔)
↳65 QDP
↳66 QDPSizeChangeProof (⇔)
↳67 TRUE
↳68 QDP
↳69 UsableRulesProof (⇔)
↳70 QDP
↳71 QReductionProof (⇔)
↳72 QDP
↳73 QDPSizeChangeProof (⇔)
↳74 TRUE
↳75 QDP
↳76 UsableRulesProof (⇔)
↳77 QDP
↳78 QReductionProof (⇔)
↳79 QDP
↳80 QDPOrderProof (⇔)
↳81 QDP
↳82 PisEmptyProof (⇔)
↳83 TRUE
↳84 QDP
↳85 UsableRulesProof (⇔)
↳86 QDP
↳87 QReductionProof (⇔)
↳88 QDP
↳89 QDPSizeChangeProof (⇔)
↳90 TRUE
↳91 QDP
↳92 UsableRulesProof (⇔)
↳93 QDP
↳94 QReductionProof (⇔)
↳95 QDP
↳96 QDPSizeChangeProof (⇔)
↳97 TRUE
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
log(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
log(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
MINUS(s(x), s(y)) → MINUS(x, y)
QUOT(s(x), s(y)) → QUOT(minus(x, y), s(y))
QUOT(s(x), s(y)) → MINUS(x, y)
LE(s(x), s(y)) → LE(x, y)
INC(s(x)) → INC(x)
LOG(x) → LOGITER(x, 0)
LOGITER(x, y) → IF(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
LOGITER(x, y) → LE(s(0), x)
LOGITER(x, y) → LE(s(s(0)), x)
LOGITER(x, y) → QUOT(x, s(s(0)))
LOGITER(x, y) → INC(y)
IF(true, true, x, y) → LOGITER(x, y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
log(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
INC(s(x)) → INC(x)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
log(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
INC(s(x)) → INC(x)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
INC(s(x)) → INC(x)
From the DPs we obtained the following set of size-change graphs:
LE(s(x), s(y)) → LE(x, y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
log(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
LE(s(x), s(y)) → LE(x, y)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
LE(s(x), s(y)) → LE(x, y)
From the DPs we obtained the following set of size-change graphs:
MINUS(s(x), s(y)) → MINUS(x, y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
log(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
MINUS(s(x), s(y)) → MINUS(x, y)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
MINUS(s(x), s(y)) → MINUS(x, y)
From the DPs we obtained the following set of size-change graphs:
QUOT(s(x), s(y)) → QUOT(minus(x, y), s(y))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
log(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
QUOT(s(x), s(y)) → QUOT(minus(x, y), s(y))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
QUOT(s(x), s(y)) → QUOT(minus(x, y), s(y))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(x0, 0)
minus(s(x0), s(x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
QUOT(s(x), s(y)) → QUOT(minus(x, y), s(y))
POL(0) = 0
POL(QUOT(x1, x2)) = x1
POL(minus(x1, x2)) = x1
POL(s(x1)) = 1 + x1
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(x0, 0)
minus(s(x0), s(x1))
LOGITER(x, y) → IF(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
IF(true, true, x, y) → LOGITER(x, y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
log(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
LOGITER(x, y) → IF(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
IF(true, true, x, y) → LOGITER(x, y)
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
LOGITER(x, y) → IF(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
IF(true, true, x, y) → LOGITER(x, y)
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
POL(0) = 0
POL(IF(x1, x2, x3, x4)) = x1 + 2·x2 + x3
POL(LOGITER(x1, x2)) = 3
POL(false) = 0
POL(inc(x1)) = 0
POL(le(x1, x2)) = 1
POL(minus(x1, x2)) = 2 + x1
POL(quot(x1, x2)) = 0
POL(s(x1)) = 2·x1
POL(true) = 1
IF(true, true, x, y) → LOGITER(x, y)
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
le'(s(x), 0) → true
le'(s(x5), s(y3)) → le'(x5, y3)
le'(0, y42) → false
le(s(x), 0) → false
le(s(x5), s(y3)) → le(x5, y3)
quot(0, s(y9)) → 0
quot(s(x18), s(y15)) → s(quot(minus(x18, y15), s(y15)))
inc(s(x25)) → s(inc(x25))
inc(0) → s(0)
minus(x38, 0) → x38
minus(s(x45), s(y36)) → minus(x45, y36)
le(0, y42) → true
quot(0, 0) → 0
quot(s(x2), 0) → 0
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[a32](witness_sort[a32], witness_sort[a32]) → true
le'(s(x), 0) → true
le'(s(x5), s(y3)) → le'(x5, y3)
le'(0, y42) → false
le(s(x), 0) → false
le(s(x5), s(y3)) → le(x5, y3)
quot(0, s(y9)) → 0
quot(s(x18), s(y15)) → s(quot(minus(x18, y15), s(y15)))
inc(s(x25)) → s(inc(x25))
inc(0) → s(0)
minus(x38, 0) → x38
minus(s(x45), s(y36)) → minus(x45, y36)
le(0, y42) → true
quot(0, 0) → 0
quot(s(x2), 0) → 0
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[a32](witness_sort[a32], witness_sort[a32]) → true
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
LE'(s(x5), s(y3)) → LE'(x5, y3)
LE(s(x5), s(y3)) → LE(x5, y3)
QUOT(s(x18), s(y15)) → QUOT(minus(x18, y15), s(y15))
QUOT(s(x18), s(y15)) → MINUS(x18, y15)
INC(s(x25)) → INC(x25)
MINUS(s(x45), s(y36)) → MINUS(x45, y36)
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
le'(s(x), 0) → true
le'(s(x5), s(y3)) → le'(x5, y3)
le'(0, y42) → false
le(s(x), 0) → false
le(s(x5), s(y3)) → le(x5, y3)
quot(0, s(y9)) → 0
quot(s(x18), s(y15)) → s(quot(minus(x18, y15), s(y15)))
inc(s(x25)) → s(inc(x25))
inc(0) → s(0)
minus(x38, 0) → x38
minus(s(x45), s(y36)) → minus(x45, y36)
le(0, y42) → true
quot(0, 0) → 0
quot(s(x2), 0) → 0
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[a32](witness_sort[a32], witness_sort[a32]) → true
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
le'(s(x), 0) → true
le'(s(x5), s(y3)) → le'(x5, y3)
le'(0, y42) → false
le(s(x), 0) → false
le(s(x5), s(y3)) → le(x5, y3)
quot(0, s(y9)) → 0
quot(s(x18), s(y15)) → s(quot(minus(x18, y15), s(y15)))
inc(s(x25)) → s(inc(x25))
inc(0) → s(0)
minus(x38, 0) → x38
minus(s(x45), s(y36)) → minus(x45, y36)
le(0, y42) → true
quot(0, 0) → 0
quot(s(x2), 0) → 0
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[a32](witness_sort[a32], witness_sort[a32]) → true
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
From the DPs we obtained the following set of size-change graphs:
MINUS(s(x45), s(y36)) → MINUS(x45, y36)
le'(s(x), 0) → true
le'(s(x5), s(y3)) → le'(x5, y3)
le'(0, y42) → false
le(s(x), 0) → false
le(s(x5), s(y3)) → le(x5, y3)
quot(0, s(y9)) → 0
quot(s(x18), s(y15)) → s(quot(minus(x18, y15), s(y15)))
inc(s(x25)) → s(inc(x25))
inc(0) → s(0)
minus(x38, 0) → x38
minus(s(x45), s(y36)) → minus(x45, y36)
le(0, y42) → true
quot(0, 0) → 0
quot(s(x2), 0) → 0
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[a32](witness_sort[a32], witness_sort[a32]) → true
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
MINUS(s(x45), s(y36)) → MINUS(x45, y36)
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
MINUS(s(x45), s(y36)) → MINUS(x45, y36)
From the DPs we obtained the following set of size-change graphs:
INC(s(x25)) → INC(x25)
le'(s(x), 0) → true
le'(s(x5), s(y3)) → le'(x5, y3)
le'(0, y42) → false
le(s(x), 0) → false
le(s(x5), s(y3)) → le(x5, y3)
quot(0, s(y9)) → 0
quot(s(x18), s(y15)) → s(quot(minus(x18, y15), s(y15)))
inc(s(x25)) → s(inc(x25))
inc(0) → s(0)
minus(x38, 0) → x38
minus(s(x45), s(y36)) → minus(x45, y36)
le(0, y42) → true
quot(0, 0) → 0
quot(s(x2), 0) → 0
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[a32](witness_sort[a32], witness_sort[a32]) → true
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
INC(s(x25)) → INC(x25)
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
INC(s(x25)) → INC(x25)
From the DPs we obtained the following set of size-change graphs:
QUOT(s(x18), s(y15)) → QUOT(minus(x18, y15), s(y15))
le'(s(x), 0) → true
le'(s(x5), s(y3)) → le'(x5, y3)
le'(0, y42) → false
le(s(x), 0) → false
le(s(x5), s(y3)) → le(x5, y3)
quot(0, s(y9)) → 0
quot(s(x18), s(y15)) → s(quot(minus(x18, y15), s(y15)))
inc(s(x25)) → s(inc(x25))
inc(0) → s(0)
minus(x38, 0) → x38
minus(s(x45), s(y36)) → minus(x45, y36)
le(0, y42) → true
quot(0, 0) → 0
quot(s(x2), 0) → 0
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[a32](witness_sort[a32], witness_sort[a32]) → true
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
QUOT(s(x18), s(y15)) → QUOT(minus(x18, y15), s(y15))
minus(x38, 0) → x38
minus(s(x45), s(y36)) → minus(x45, y36)
minus(0, s(x0)) → 0
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
QUOT(s(x18), s(y15)) → QUOT(minus(x18, y15), s(y15))
minus(x38, 0) → x38
minus(s(x45), s(y36)) → minus(x45, y36)
minus(0, s(x0)) → 0
minus(x0, 0)
minus(s(x0), s(x1))
minus(0, s(x0))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
QUOT(s(x18), s(y15)) → QUOT(minus(x18, y15), s(y15))
POL(0) = 0
POL(QUOT(x1, x2)) = x1
POL(minus(x1, x2)) = x1
POL(s(x1)) = 1 + x1
minus(x38, 0) → x38
minus(0, s(x0)) → 0
minus(s(x45), s(y36)) → minus(x45, y36)
minus(x38, 0) → x38
minus(s(x45), s(y36)) → minus(x45, y36)
minus(0, s(x0)) → 0
minus(x0, 0)
minus(s(x0), s(x1))
minus(0, s(x0))
LE(s(x5), s(y3)) → LE(x5, y3)
le'(s(x), 0) → true
le'(s(x5), s(y3)) → le'(x5, y3)
le'(0, y42) → false
le(s(x), 0) → false
le(s(x5), s(y3)) → le(x5, y3)
quot(0, s(y9)) → 0
quot(s(x18), s(y15)) → s(quot(minus(x18, y15), s(y15)))
inc(s(x25)) → s(inc(x25))
inc(0) → s(0)
minus(x38, 0) → x38
minus(s(x45), s(y36)) → minus(x45, y36)
le(0, y42) → true
quot(0, 0) → 0
quot(s(x2), 0) → 0
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[a32](witness_sort[a32], witness_sort[a32]) → true
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
LE(s(x5), s(y3)) → LE(x5, y3)
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
LE(s(x5), s(y3)) → LE(x5, y3)
From the DPs we obtained the following set of size-change graphs:
LE'(s(x5), s(y3)) → LE'(x5, y3)
le'(s(x), 0) → true
le'(s(x5), s(y3)) → le'(x5, y3)
le'(0, y42) → false
le(s(x), 0) → false
le(s(x5), s(y3)) → le(x5, y3)
quot(0, s(y9)) → 0
quot(s(x18), s(y15)) → s(quot(minus(x18, y15), s(y15)))
inc(s(x25)) → s(inc(x25))
inc(0) → s(0)
minus(x38, 0) → x38
minus(s(x45), s(y36)) → minus(x45, y36)
le(0, y42) → true
quot(0, 0) → 0
quot(s(x2), 0) → 0
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[a32](witness_sort[a32], witness_sort[a32]) → true
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
LE'(s(x5), s(y3)) → LE'(x5, y3)
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
le'(s(x0), 0)
le'(s(x0), s(x1))
le'(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
minus(x0, 0)
minus(s(x0), s(x1))
le(0, x0)
quot(0, 0)
quot(s(x0), 0)
minus(0, s(x0))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a32](witness_sort[a32], witness_sort[a32])
LE'(s(x5), s(y3)) → LE'(x5, y3)
From the DPs we obtained the following set of size-change graphs: