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 QDPSizeChangeProof (⇔)
↳34 TRUE
↳35 QDP
↳36 UsableRulesProof (⇔)
↳37 QDP
↳38 QReductionProof (⇔)
↳39 QDP
↳40 Induction-Processor (⇐)
↳41 AND
↳42 QDP
↳43 PisEmptyProof (⇔)
↳44 TRUE
↳45 QTRS
↳46 Overlay + Local Confluence (⇔)
↳47 QTRS
↳48 DependencyPairsProof (⇔)
↳49 QDP
↳50 DependencyGraphProof (⇔)
↳51 AND
↳52 QDP
↳53 UsableRulesProof (⇔)
↳54 QDP
↳55 QReductionProof (⇔)
↳56 QDP
↳57 QDPSizeChangeProof (⇔)
↳58 TRUE
↳59 QDP
↳60 UsableRulesProof (⇔)
↳61 QDP
↳62 QReductionProof (⇔)
↳63 QDP
↳64 QDPSizeChangeProof (⇔)
↳65 TRUE
↳66 QDP
↳67 UsableRulesProof (⇔)
↳68 QDP
↳69 QReductionProof (⇔)
↳70 QDP
↳71 QDPSizeChangeProof (⇔)
↳72 TRUE
↳73 QDP
↳74 UsableRulesProof (⇔)
↳75 QDP
↳76 QReductionProof (⇔)
↳77 QDP
↳78 QDPSizeChangeProof (⇔)
↳79 TRUE
↳80 QDP
↳81 UsableRulesProof (⇔)
↳82 QDP
↳83 QReductionProof (⇔)
↳84 QDP
↳85 QDPSizeChangeProof (⇔)
↳86 TRUE
↳87 QDP
↳88 UsableRulesProof (⇔)
↳89 QDP
↳90 QReductionProof (⇔)
↳91 QDP
↳92 QDPSizeChangeProof (⇔)
↳93 TRUE
↳94 QDP
↳95 UsableRulesProof (⇔)
↳96 QDP
↳97 QReductionProof (⇔)
↳98 QDP
↳99 QDPSizeChangeProof (⇔)
↳100 TRUE
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if1(true, x, y, xs) → min(x, xs)
if1(false, x, y, xs) → min(y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
minsort(nil) → nil
minsort(cons(x, y)) → cons(min(x, y), minsort(del(min(x, y), cons(x, y))))
min(x, nil) → x
min(x, cons(y, z)) → if1(le(x, y), x, y, z)
del(x, nil) → nil
del(x, cons(y, z)) → if2(eq(x, y), x, y, z)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if1(true, x, y, xs) → min(x, xs)
if1(false, x, y, xs) → min(y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
minsort(nil) → nil
minsort(cons(x, y)) → cons(min(x, y), minsort(del(min(x, y), cons(x, y))))
min(x, nil) → x
min(x, cons(y, z)) → if1(le(x, y), x, y, z)
del(x, nil) → nil
del(x, cons(y, z)) → if2(eq(x, y), x, y, z)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
LE(s(x), s(y)) → LE(x, y)
EQ(s(x), s(y)) → EQ(x, y)
IF1(true, x, y, xs) → MIN(x, xs)
IF1(false, x, y, xs) → MIN(y, xs)
IF2(false, x, y, xs) → DEL(x, xs)
MINSORT(cons(x, y)) → MIN(x, y)
MINSORT(cons(x, y)) → MINSORT(del(min(x, y), cons(x, y)))
MINSORT(cons(x, y)) → DEL(min(x, y), cons(x, y))
MIN(x, cons(y, z)) → IF1(le(x, y), x, y, z)
MIN(x, cons(y, z)) → LE(x, y)
DEL(x, cons(y, z)) → IF2(eq(x, y), x, y, z)
DEL(x, cons(y, z)) → EQ(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if1(true, x, y, xs) → min(x, xs)
if1(false, x, y, xs) → min(y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
minsort(nil) → nil
minsort(cons(x, y)) → cons(min(x, y), minsort(del(min(x, y), cons(x, y))))
min(x, nil) → x
min(x, cons(y, z)) → if1(le(x, y), x, y, z)
del(x, nil) → nil
del(x, cons(y, z)) → if2(eq(x, y), x, y, z)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
EQ(s(x), s(y)) → EQ(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if1(true, x, y, xs) → min(x, xs)
if1(false, x, y, xs) → min(y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
minsort(nil) → nil
minsort(cons(x, y)) → cons(min(x, y), minsort(del(min(x, y), cons(x, y))))
min(x, nil) → x
min(x, cons(y, z)) → if1(le(x, y), x, y, z)
del(x, nil) → nil
del(x, cons(y, z)) → if2(eq(x, y), x, y, z)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
EQ(s(x), s(y)) → EQ(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
EQ(s(x), s(y)) → EQ(x, y)
From the DPs we obtained the following set of size-change graphs:
DEL(x, cons(y, z)) → IF2(eq(x, y), x, y, z)
IF2(false, x, y, xs) → DEL(x, xs)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if1(true, x, y, xs) → min(x, xs)
if1(false, x, y, xs) → min(y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
minsort(nil) → nil
minsort(cons(x, y)) → cons(min(x, y), minsort(del(min(x, y), cons(x, y))))
min(x, nil) → x
min(x, cons(y, z)) → if1(le(x, y), x, y, z)
del(x, nil) → nil
del(x, cons(y, z)) → if2(eq(x, y), x, y, z)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
DEL(x, cons(y, z)) → IF2(eq(x, y), x, y, z)
IF2(false, x, y, xs) → DEL(x, xs)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
DEL(x, cons(y, z)) → IF2(eq(x, y), x, y, z)
IF2(false, x, y, xs) → DEL(x, xs)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
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)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if1(true, x, y, xs) → min(x, xs)
if1(false, x, y, xs) → min(y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
minsort(nil) → nil
minsort(cons(x, y)) → cons(min(x, y), minsort(del(min(x, y), cons(x, y))))
min(x, nil) → x
min(x, cons(y, z)) → if1(le(x, y), x, y, z)
del(x, nil) → nil
del(x, cons(y, z)) → if2(eq(x, y), x, y, z)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
LE(s(x), s(y)) → LE(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
LE(s(x), s(y)) → LE(x, y)
From the DPs we obtained the following set of size-change graphs:
MIN(x, cons(y, z)) → IF1(le(x, y), x, y, z)
IF1(true, x, y, xs) → MIN(x, xs)
IF1(false, x, y, xs) → MIN(y, xs)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if1(true, x, y, xs) → min(x, xs)
if1(false, x, y, xs) → min(y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
minsort(nil) → nil
minsort(cons(x, y)) → cons(min(x, y), minsort(del(min(x, y), cons(x, y))))
min(x, nil) → x
min(x, cons(y, z)) → if1(le(x, y), x, y, z)
del(x, nil) → nil
del(x, cons(y, z)) → if2(eq(x, y), x, y, z)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
MIN(x, cons(y, z)) → IF1(le(x, y), x, y, z)
IF1(true, x, y, xs) → MIN(x, xs)
IF1(false, x, y, xs) → MIN(y, xs)
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))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
MIN(x, cons(y, z)) → IF1(le(x, y), x, y, z)
IF1(true, x, y, xs) → MIN(x, xs)
IF1(false, x, y, xs) → MIN(y, xs)
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))
From the DPs we obtained the following set of size-change graphs:
MINSORT(cons(x, y)) → MINSORT(del(min(x, y), cons(x, y)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if1(true, x, y, xs) → min(x, xs)
if1(false, x, y, xs) → min(y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
minsort(nil) → nil
minsort(cons(x, y)) → cons(min(x, y), minsort(del(min(x, y), cons(x, y))))
min(x, nil) → x
min(x, cons(y, z)) → if1(le(x, y), x, y, z)
del(x, nil) → nil
del(x, cons(y, z)) → if2(eq(x, y), x, y, z)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
MINSORT(cons(x, y)) → MINSORT(del(min(x, y), cons(x, y)))
min(x, nil) → x
if1(true, x, y, xs) → min(x, xs)
min(x, cons(y, z)) → if1(le(x, y), x, y, z)
if1(false, x, y, xs) → min(y, xs)
del(x, cons(y, z)) → if2(eq(x, y), x, y, z)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
del(x, nil) → nil
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))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
minsort(nil)
minsort(cons(x0, x1))
MINSORT(cons(x, y)) → MINSORT(del(min(x, y), cons(x, y)))
min(x, nil) → x
if1(true, x, y, xs) → min(x, xs)
min(x, cons(y, z)) → if1(le(x, y), x, y, z)
if1(false, x, y, xs) → min(y, xs)
del(x, cons(y, z)) → if2(eq(x, y), x, y, z)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
del(x, nil) → nil
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))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
POL(0) = 0
POL(MINSORT(x1)) = x1
POL(cons(x1, x2)) = 1 + x1 + x2
POL(del(x1, x2)) = x2
POL(eq(x1, x2)) = x2
POL(false) = 0
POL(if1(x1, x2, x3, x4)) = 1 + x2 + x3 + x4
POL(if2(x1, x2, x3, x4)) = 1 + x3 + x4
POL(le(x1, x2)) = 1
POL(min(x1, x2)) = 1 + x1 + x2
POL(nil) = 0
POL(s(x1)) = 1 + x1
POL(true) = 0
min(x, nil) → x
if1(true, x, y, xs) → min(x, xs)
min(x, cons(y, z)) → if1(le(x, y), x, y, z)
if1(false, x, y, xs) → min(y, xs)
del(x, cons(y, z)) → if2(eq(x, y), x, y, z)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
del(x, nil) → nil
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))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
min(x0, nil)
min(x0, cons(x1, x2))
del(x0, nil)
del(x0, cons(x1, x2))
del'(x49, cons(y40, z7)) → if2'(eq(x49, y40), x49, y40, z7)
if2'(true, x112, y93, xs35) → true
if2'(false, x125, y104, xs40) → del'(x125, xs40)
del'(x138, nil) → false
min(x, nil) → x
if1(true, x10, y7, xs1) → min(x10, xs1)
min(x23, cons(y18, z2)) → if1(le(x23, y18), x23, y18, z2)
if1(false, x36, y29, xs10) → min(y29, xs10)
del(x49, cons(y40, z7)) → if2(eq(x49, y40), x49, y40, z7)
eq(0, 0) → true
eq(0, s(y61)) → false
eq(s(x86), 0) → false
eq(s(x99), s(y82)) → eq(x99, y82)
if2(true, x112, y93, xs35) → xs35
if2(false, x125, y104, xs40) → cons(y104, del(x125, xs40))
del(x138, nil) → nil
le(0, y125) → true
le(s(x163), 0) → false
le(s(x176), s(y146)) → le(x176, y146)
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](nil, nil) → true
equal_sort[a32](nil, cons(x0, x1)) → false
equal_sort[a32](cons(x0, x1), nil) → false
equal_sort[a32](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a32](x0, x2), equal_sort[a32](x1, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61]) → true
del'(x49, cons(y40, z7)) → if2'(eq(x49, y40), x49, y40, z7)
if2'(true, x112, y93, xs35) → true
if2'(false, x125, y104, xs40) → del'(x125, xs40)
del'(x138, nil) → false
min(x, nil) → x
if1(true, x10, y7, xs1) → min(x10, xs1)
min(x23, cons(y18, z2)) → if1(le(x23, y18), x23, y18, z2)
if1(false, x36, y29, xs10) → min(y29, xs10)
del(x49, cons(y40, z7)) → if2(eq(x49, y40), x49, y40, z7)
eq(0, 0) → true
eq(0, s(y61)) → false
eq(s(x86), 0) → false
eq(s(x99), s(y82)) → eq(x99, y82)
if2(true, x112, y93, xs35) → xs35
if2(false, x125, y104, xs40) → cons(y104, del(x125, xs40))
del(x138, nil) → nil
le(0, y125) → true
le(s(x163), 0) → false
le(s(x176), s(y146)) → le(x176, y146)
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](nil, nil) → true
equal_sort[a32](nil, cons(x0, x1)) → false
equal_sort[a32](cons(x0, x1), nil) → false
equal_sort[a32](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a32](x0, x2), equal_sort[a32](x1, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61]) → true
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
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](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
DEL'(x49, cons(y40, z7)) → IF2'(eq(x49, y40), x49, y40, z7)
DEL'(x49, cons(y40, z7)) → EQ(x49, y40)
IF2'(false, x125, y104, xs40) → DEL'(x125, xs40)
IF1(true, x10, y7, xs1) → MIN(x10, xs1)
MIN(x23, cons(y18, z2)) → IF1(le(x23, y18), x23, y18, z2)
MIN(x23, cons(y18, z2)) → LE(x23, y18)
IF1(false, x36, y29, xs10) → MIN(y29, xs10)
DEL(x49, cons(y40, z7)) → IF2(eq(x49, y40), x49, y40, z7)
DEL(x49, cons(y40, z7)) → EQ(x49, y40)
EQ(s(x99), s(y82)) → EQ(x99, y82)
IF2(false, x125, y104, xs40) → DEL(x125, xs40)
LE(s(x176), s(y146)) → LE(x176, y146)
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
EQUAL_SORT[A32](cons(x0, x1), cons(x2, x3)) → AND(equal_sort[a32](x0, x2), equal_sort[a32](x1, x3))
EQUAL_SORT[A32](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A32](x0, x2)
EQUAL_SORT[A32](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A32](x1, x3)
del'(x49, cons(y40, z7)) → if2'(eq(x49, y40), x49, y40, z7)
if2'(true, x112, y93, xs35) → true
if2'(false, x125, y104, xs40) → del'(x125, xs40)
del'(x138, nil) → false
min(x, nil) → x
if1(true, x10, y7, xs1) → min(x10, xs1)
min(x23, cons(y18, z2)) → if1(le(x23, y18), x23, y18, z2)
if1(false, x36, y29, xs10) → min(y29, xs10)
del(x49, cons(y40, z7)) → if2(eq(x49, y40), x49, y40, z7)
eq(0, 0) → true
eq(0, s(y61)) → false
eq(s(x86), 0) → false
eq(s(x99), s(y82)) → eq(x99, y82)
if2(true, x112, y93, xs35) → xs35
if2(false, x125, y104, xs40) → cons(y104, del(x125, xs40))
del(x138, nil) → nil
le(0, y125) → true
le(s(x163), 0) → false
le(s(x176), s(y146)) → le(x176, y146)
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](nil, nil) → true
equal_sort[a32](nil, cons(x0, x1)) → false
equal_sort[a32](cons(x0, x1), nil) → false
equal_sort[a32](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a32](x0, x2), equal_sort[a32](x1, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61]) → true
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
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](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
EQUAL_SORT[A32](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A32](x1, x3)
EQUAL_SORT[A32](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A32](x0, x2)
del'(x49, cons(y40, z7)) → if2'(eq(x49, y40), x49, y40, z7)
if2'(true, x112, y93, xs35) → true
if2'(false, x125, y104, xs40) → del'(x125, xs40)
del'(x138, nil) → false
min(x, nil) → x
if1(true, x10, y7, xs1) → min(x10, xs1)
min(x23, cons(y18, z2)) → if1(le(x23, y18), x23, y18, z2)
if1(false, x36, y29, xs10) → min(y29, xs10)
del(x49, cons(y40, z7)) → if2(eq(x49, y40), x49, y40, z7)
eq(0, 0) → true
eq(0, s(y61)) → false
eq(s(x86), 0) → false
eq(s(x99), s(y82)) → eq(x99, y82)
if2(true, x112, y93, xs35) → xs35
if2(false, x125, y104, xs40) → cons(y104, del(x125, xs40))
del(x138, nil) → nil
le(0, y125) → true
le(s(x163), 0) → false
le(s(x176), s(y146)) → le(x176, y146)
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](nil, nil) → true
equal_sort[a32](nil, cons(x0, x1)) → false
equal_sort[a32](cons(x0, x1), nil) → false
equal_sort[a32](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a32](x0, x2), equal_sort[a32](x1, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61]) → true
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
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](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
EQUAL_SORT[A32](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A32](x1, x3)
EQUAL_SORT[A32](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A32](x0, x2)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
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](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
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](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
EQUAL_SORT[A32](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A32](x1, x3)
EQUAL_SORT[A32](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A32](x0, x2)
From the DPs we obtained the following set of size-change graphs:
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
del'(x49, cons(y40, z7)) → if2'(eq(x49, y40), x49, y40, z7)
if2'(true, x112, y93, xs35) → true
if2'(false, x125, y104, xs40) → del'(x125, xs40)
del'(x138, nil) → false
min(x, nil) → x
if1(true, x10, y7, xs1) → min(x10, xs1)
min(x23, cons(y18, z2)) → if1(le(x23, y18), x23, y18, z2)
if1(false, x36, y29, xs10) → min(y29, xs10)
del(x49, cons(y40, z7)) → if2(eq(x49, y40), x49, y40, z7)
eq(0, 0) → true
eq(0, s(y61)) → false
eq(s(x86), 0) → false
eq(s(x99), s(y82)) → eq(x99, y82)
if2(true, x112, y93, xs35) → xs35
if2(false, x125, y104, xs40) → cons(y104, del(x125, xs40))
del(x138, nil) → nil
le(0, y125) → true
le(s(x163), 0) → false
le(s(x176), s(y146)) → le(x176, y146)
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](nil, nil) → true
equal_sort[a32](nil, cons(x0, x1)) → false
equal_sort[a32](cons(x0, x1), nil) → false
equal_sort[a32](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a32](x0, x2), equal_sort[a32](x1, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61]) → true
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
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](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
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](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
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](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
From the DPs we obtained the following set of size-change graphs:
LE(s(x176), s(y146)) → LE(x176, y146)
del'(x49, cons(y40, z7)) → if2'(eq(x49, y40), x49, y40, z7)
if2'(true, x112, y93, xs35) → true
if2'(false, x125, y104, xs40) → del'(x125, xs40)
del'(x138, nil) → false
min(x, nil) → x
if1(true, x10, y7, xs1) → min(x10, xs1)
min(x23, cons(y18, z2)) → if1(le(x23, y18), x23, y18, z2)
if1(false, x36, y29, xs10) → min(y29, xs10)
del(x49, cons(y40, z7)) → if2(eq(x49, y40), x49, y40, z7)
eq(0, 0) → true
eq(0, s(y61)) → false
eq(s(x86), 0) → false
eq(s(x99), s(y82)) → eq(x99, y82)
if2(true, x112, y93, xs35) → xs35
if2(false, x125, y104, xs40) → cons(y104, del(x125, xs40))
del(x138, nil) → nil
le(0, y125) → true
le(s(x163), 0) → false
le(s(x176), s(y146)) → le(x176, y146)
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](nil, nil) → true
equal_sort[a32](nil, cons(x0, x1)) → false
equal_sort[a32](cons(x0, x1), nil) → false
equal_sort[a32](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a32](x0, x2), equal_sort[a32](x1, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61]) → true
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
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](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
LE(s(x176), s(y146)) → LE(x176, y146)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
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](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
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](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
LE(s(x176), s(y146)) → LE(x176, y146)
From the DPs we obtained the following set of size-change graphs:
EQ(s(x99), s(y82)) → EQ(x99, y82)
del'(x49, cons(y40, z7)) → if2'(eq(x49, y40), x49, y40, z7)
if2'(true, x112, y93, xs35) → true
if2'(false, x125, y104, xs40) → del'(x125, xs40)
del'(x138, nil) → false
min(x, nil) → x
if1(true, x10, y7, xs1) → min(x10, xs1)
min(x23, cons(y18, z2)) → if1(le(x23, y18), x23, y18, z2)
if1(false, x36, y29, xs10) → min(y29, xs10)
del(x49, cons(y40, z7)) → if2(eq(x49, y40), x49, y40, z7)
eq(0, 0) → true
eq(0, s(y61)) → false
eq(s(x86), 0) → false
eq(s(x99), s(y82)) → eq(x99, y82)
if2(true, x112, y93, xs35) → xs35
if2(false, x125, y104, xs40) → cons(y104, del(x125, xs40))
del(x138, nil) → nil
le(0, y125) → true
le(s(x163), 0) → false
le(s(x176), s(y146)) → le(x176, y146)
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](nil, nil) → true
equal_sort[a32](nil, cons(x0, x1)) → false
equal_sort[a32](cons(x0, x1), nil) → false
equal_sort[a32](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a32](x0, x2), equal_sort[a32](x1, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61]) → true
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
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](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
EQ(s(x99), s(y82)) → EQ(x99, y82)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
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](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
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](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
EQ(s(x99), s(y82)) → EQ(x99, y82)
From the DPs we obtained the following set of size-change graphs:
IF2(false, x125, y104, xs40) → DEL(x125, xs40)
DEL(x49, cons(y40, z7)) → IF2(eq(x49, y40), x49, y40, z7)
del'(x49, cons(y40, z7)) → if2'(eq(x49, y40), x49, y40, z7)
if2'(true, x112, y93, xs35) → true
if2'(false, x125, y104, xs40) → del'(x125, xs40)
del'(x138, nil) → false
min(x, nil) → x
if1(true, x10, y7, xs1) → min(x10, xs1)
min(x23, cons(y18, z2)) → if1(le(x23, y18), x23, y18, z2)
if1(false, x36, y29, xs10) → min(y29, xs10)
del(x49, cons(y40, z7)) → if2(eq(x49, y40), x49, y40, z7)
eq(0, 0) → true
eq(0, s(y61)) → false
eq(s(x86), 0) → false
eq(s(x99), s(y82)) → eq(x99, y82)
if2(true, x112, y93, xs35) → xs35
if2(false, x125, y104, xs40) → cons(y104, del(x125, xs40))
del(x138, nil) → nil
le(0, y125) → true
le(s(x163), 0) → false
le(s(x176), s(y146)) → le(x176, y146)
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](nil, nil) → true
equal_sort[a32](nil, cons(x0, x1)) → false
equal_sort[a32](cons(x0, x1), nil) → false
equal_sort[a32](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a32](x0, x2), equal_sort[a32](x1, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61]) → true
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
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](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
IF2(false, x125, y104, xs40) → DEL(x125, xs40)
DEL(x49, cons(y40, z7)) → IF2(eq(x49, y40), x49, y40, z7)
eq(0, 0) → true
eq(0, s(y61)) → false
eq(s(x86), 0) → false
eq(s(x99), s(y82)) → eq(x99, y82)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
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](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
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](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
IF2(false, x125, y104, xs40) → DEL(x125, xs40)
DEL(x49, cons(y40, z7)) → IF2(eq(x49, y40), x49, y40, z7)
eq(0, 0) → true
eq(0, s(y61)) → false
eq(s(x86), 0) → false
eq(s(x99), s(y82)) → eq(x99, y82)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
From the DPs we obtained the following set of size-change graphs:
MIN(x23, cons(y18, z2)) → IF1(le(x23, y18), x23, y18, z2)
IF1(true, x10, y7, xs1) → MIN(x10, xs1)
IF1(false, x36, y29, xs10) → MIN(y29, xs10)
del'(x49, cons(y40, z7)) → if2'(eq(x49, y40), x49, y40, z7)
if2'(true, x112, y93, xs35) → true
if2'(false, x125, y104, xs40) → del'(x125, xs40)
del'(x138, nil) → false
min(x, nil) → x
if1(true, x10, y7, xs1) → min(x10, xs1)
min(x23, cons(y18, z2)) → if1(le(x23, y18), x23, y18, z2)
if1(false, x36, y29, xs10) → min(y29, xs10)
del(x49, cons(y40, z7)) → if2(eq(x49, y40), x49, y40, z7)
eq(0, 0) → true
eq(0, s(y61)) → false
eq(s(x86), 0) → false
eq(s(x99), s(y82)) → eq(x99, y82)
if2(true, x112, y93, xs35) → xs35
if2(false, x125, y104, xs40) → cons(y104, del(x125, xs40))
del(x138, nil) → nil
le(0, y125) → true
le(s(x163), 0) → false
le(s(x176), s(y146)) → le(x176, y146)
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](nil, nil) → true
equal_sort[a32](nil, cons(x0, x1)) → false
equal_sort[a32](cons(x0, x1), nil) → false
equal_sort[a32](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a32](x0, x2), equal_sort[a32](x1, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61]) → true
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
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](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
MIN(x23, cons(y18, z2)) → IF1(le(x23, y18), x23, y18, z2)
IF1(true, x10, y7, xs1) → MIN(x10, xs1)
IF1(false, x36, y29, xs10) → MIN(y29, xs10)
le(0, y125) → true
le(s(x163), 0) → false
le(s(x176), s(y146)) → le(x176, y146)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
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](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
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](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
MIN(x23, cons(y18, z2)) → IF1(le(x23, y18), x23, y18, z2)
IF1(true, x10, y7, xs1) → MIN(x10, xs1)
IF1(false, x36, y29, xs10) → MIN(y29, xs10)
le(0, y125) → true
le(s(x163), 0) → false
le(s(x176), s(y146)) → le(x176, y146)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
From the DPs we obtained the following set of size-change graphs:
IF2'(false, x125, y104, xs40) → DEL'(x125, xs40)
DEL'(x49, cons(y40, z7)) → IF2'(eq(x49, y40), x49, y40, z7)
del'(x49, cons(y40, z7)) → if2'(eq(x49, y40), x49, y40, z7)
if2'(true, x112, y93, xs35) → true
if2'(false, x125, y104, xs40) → del'(x125, xs40)
del'(x138, nil) → false
min(x, nil) → x
if1(true, x10, y7, xs1) → min(x10, xs1)
min(x23, cons(y18, z2)) → if1(le(x23, y18), x23, y18, z2)
if1(false, x36, y29, xs10) → min(y29, xs10)
del(x49, cons(y40, z7)) → if2(eq(x49, y40), x49, y40, z7)
eq(0, 0) → true
eq(0, s(y61)) → false
eq(s(x86), 0) → false
eq(s(x99), s(y82)) → eq(x99, y82)
if2(true, x112, y93, xs35) → xs35
if2(false, x125, y104, xs40) → cons(y104, del(x125, xs40))
del(x138, nil) → nil
le(0, y125) → true
le(s(x163), 0) → false
le(s(x176), s(y146)) → le(x176, y146)
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](nil, nil) → true
equal_sort[a32](nil, cons(x0, x1)) → false
equal_sort[a32](cons(x0, x1), nil) → false
equal_sort[a32](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a32](x0, x2), equal_sort[a32](x1, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61]) → true
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
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](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
IF2'(false, x125, y104, xs40) → DEL'(x125, xs40)
DEL'(x49, cons(y40, z7)) → IF2'(eq(x49, y40), x49, y40, z7)
eq(0, 0) → true
eq(0, s(y61)) → false
eq(s(x86), 0) → false
eq(s(x99), s(y82)) → eq(x99, y82)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
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](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
if1(true, x0, x1, x2)
min(x0, cons(x1, x2))
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
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](nil, nil)
equal_sort[a32](nil, cons(x0, x1))
equal_sort[a32](cons(x0, x1), nil)
equal_sort[a32](cons(x0, x1), cons(x2, x3))
equal_sort[a61](witness_sort[a61], witness_sort[a61])
IF2'(false, x125, y104, xs40) → DEL'(x125, xs40)
DEL'(x49, cons(y40, z7)) → IF2'(eq(x49, y40), x49, y40, z7)
eq(0, 0) → true
eq(0, s(y61)) → false
eq(s(x86), 0) → false
eq(s(x99), s(y82)) → eq(x99, y82)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
From the DPs we obtained the following set of size-change graphs: