YES
0 QTRS
↳1 Overlay + Local Confluence (⇔, 0 ms)
↳2 QTRS
↳3 DependencyPairsProof (⇔, 0 ms)
↳4 QDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 QDP
↳10 QReductionProof (⇔, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 QDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 QDP
↳17 QReductionProof (⇔, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 QDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 QDP
↳24 QReductionProof (⇔, 0 ms)
↳25 QDP
↳26 QDPSizeChangeProof (⇔, 0 ms)
↳27 YES
↳28 QDP
↳29 UsableRulesProof (⇔, 0 ms)
↳30 QDP
↳31 QReductionProof (⇔, 0 ms)
↳32 QDP
↳33 QDPSizeChangeProof (⇔, 0 ms)
↳34 YES
↳35 QDP
↳36 UsableRulesProof (⇔, 0 ms)
↳37 QDP
↳38 QReductionProof (⇔, 0 ms)
↳39 QDP
↳40 Induction-Processor (⇒, 466 ms)
↳41 AND
↳42 QDP
↳43 PisEmptyProof (⇔, 0 ms)
↳44 YES
↳45 QTRS
↳46 Overlay + Local Confluence (⇔, 5 ms)
↳47 QTRS
↳48 DependencyPairsProof (⇔, 0 ms)
↳49 QDP
↳50 DependencyGraphProof (⇔, 0 ms)
↳51 AND
↳52 QDP
↳53 UsableRulesProof (⇔, 0 ms)
↳54 QDP
↳55 QReductionProof (⇔, 0 ms)
↳56 QDP
↳57 QDPSizeChangeProof (⇔, 0 ms)
↳58 YES
↳59 QDP
↳60 UsableRulesProof (⇔, 0 ms)
↳61 QDP
↳62 QReductionProof (⇔, 0 ms)
↳63 QDP
↳64 QDPSizeChangeProof (⇔, 0 ms)
↳65 YES
↳66 QDP
↳67 UsableRulesProof (⇔, 0 ms)
↳68 QDP
↳69 QReductionProof (⇔, 0 ms)
↳70 QDP
↳71 QDPSizeChangeProof (⇔, 0 ms)
↳72 YES
↳73 QDP
↳74 UsableRulesProof (⇔, 0 ms)
↳75 QDP
↳76 QReductionProof (⇔, 0 ms)
↳77 QDP
↳78 QDPSizeChangeProof (⇔, 0 ms)
↳79 YES
↳80 QDP
↳81 UsableRulesProof (⇔, 0 ms)
↳82 QDP
↳83 QReductionProof (⇔, 0 ms)
↳84 QDP
↳85 QDPSizeChangeProof (⇔, 0 ms)
↳86 YES
↳87 QDP
↳88 UsableRulesProof (⇔, 0 ms)
↳89 QDP
↳90 QReductionProof (⇔, 0 ms)
↳91 QDP
↳92 QDPSizeChangeProof (⇔, 0 ms)
↳93 YES
↳94 QDP
↳95 UsableRulesProof (⇔, 0 ms)
↳96 QDP
↳97 QReductionProof (⇔, 0 ms)
↳98 QDP
↳99 QDPSizeChangeProof (⇔, 0 ms)
↳100 YES
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
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)
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
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)
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)) = x1
POL(false_renamed) = 0
POL(if1(x1, x2, x3, x4)) = x2 + x3 + x4
POL(if2(x1, x2, x3, x4)) = 1 + x3 + x4
POL(le(x1, x2)) = 1 + x2
POL(min(x1, x2)) = x1 + x2
POL(nil) = 0
POL(s(x1)) = x1
POL(true_renamed) = 0
proof of internal # AProVE Commit ID: 3a20a6ef7432c3f292db1a8838479c42bf5e3b22 root 20240618 unpublished Partial correctness of the following Program [x, v25, v26, v27, v28, v29, v30, v31, v32, v33, x6, y5, xs'', x7, y6, y2, z', x8, x3, x', x'', y', z, y3, x4, x5, y4, y7, x9, x10, y8, x1, y'', x2, y1] equal_bool(true, false) -> false equal_bool(false, true) -> false equal_bool(true, true) -> true equal_bool(false, false) -> true true and x -> x false and x -> false true or x -> true false or 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(v25)) -> false equal_sort[a0](s(v26), 0) -> false equal_sort[a0](s(v26), s(v27)) -> equal_sort[a0](v26, v27) equal_sort[a33](nil, nil) -> true equal_sort[a33](nil, cons(v28, v29)) -> false equal_sort[a33](cons(v30, v31), nil) -> false equal_sort[a33](cons(v30, v31), cons(v32, v33)) -> equal_sort[a0](v30, v32) and equal_sort[a33](v31, v33) equal_sort[a44](true_renamed, true_renamed) -> true equal_sort[a44](true_renamed, false_renamed) -> false equal_sort[a44](false_renamed, true_renamed) -> false equal_sort[a44](false_renamed, false_renamed) -> true equal_sort[a62](witness_sort[a62], witness_sort[a62]) -> true if2'(true_renamed, x6, y5, xs'') -> true if2'(false_renamed, x7, y6, cons(y2, z')) -> if2'(eq(x7, y2), x7, y2, z') if2'(false_renamed, x7, y6, nil) -> false del'(x8, nil) -> false equal_sort[a44](eq(x3, y2), true_renamed) -> true | del'(x3, cons(y2, z')) -> true equal_sort[a44](eq(x3, y2), true_renamed) -> false | del'(x3, cons(y2, z')) -> del'(x3, z') min(x', nil) -> x' equal_sort[a44](le(x'', y'), true_renamed) -> true | min(x'', cons(y', z)) -> min(x'', z) equal_sort[a44](le(x'', y'), true_renamed) -> false | min(x'', cons(y', z)) -> min(y', z) eq(0, 0) -> true_renamed eq(0, s(y3)) -> false_renamed eq(s(x4), 0) -> false_renamed eq(s(x5), s(y4)) -> eq(x5, y4) if2(true_renamed, x6, y5, xs'') -> xs'' if2(false_renamed, x7, y6, cons(y2, z')) -> cons(y6, if2(eq(x7, y2), x7, y2, z')) if2(false_renamed, x7, y6, nil) -> cons(y6, nil) del(x8, nil) -> nil equal_sort[a44](eq(x3, y2), true_renamed) -> true | del(x3, cons(y2, z')) -> z' equal_sort[a44](eq(x3, y2), true_renamed) -> false | del(x3, cons(y2, z')) -> cons(y2, del(x3, z')) le(0, y7) -> true_renamed le(s(x9), 0) -> false_renamed le(s(x10), s(y8)) -> le(x10, y8) if1(true_renamed, x1, y'', nil) -> x1 if1(true_renamed, x1, y'', cons(y', z)) -> if1(le(x1, y'), x1, y', z) if1(false_renamed, x2, y1, nil) -> y1 if1(false_renamed, x2, y1, cons(y', z)) -> if1(le(y1, y'), y1, y', z) using the following formula: x:sort[a0],y:sort[a33].del'(min(x, y), cons(x, y))=true could be successfully shown: (0) Formula (1) Conditional Evaluation [EQUIVALENT, 0 ms] (2) AND (3) Formula (4) Symbolic evaluation [EQUIVALENT, 0 ms] (5) YES (6) Formula (7) Hypothesis Lifting [EQUIVALENT, 0 ms] (8) Formula (9) Induction by algorithm [EQUIVALENT, 0 ms] (10) AND (11) Formula (12) Symbolic evaluation [EQUIVALENT, 0 ms] (13) Formula (14) Induction by data structure [EQUIVALENT, 0 ms] (15) AND (16) Formula (17) Symbolic evaluation [EQUIVALENT, 0 ms] (18) YES (19) Formula (20) Symbolic evaluation under hypothesis [EQUIVALENT, 0 ms] (21) YES (22) Formula (23) Conditional Evaluation [EQUIVALENT, 0 ms] (24) Formula (25) Conditional Evaluation [EQUIVALENT, 0 ms] (26) Formula (27) Conditional Evaluation [EQUIVALENT, 0 ms] (28) AND (29) Formula (30) Symbolic evaluation [EQUIVALENT, 0 ms] (31) YES (32) Formula (33) Symbolic evaluation under hypothesis [EQUIVALENT, 0 ms] (34) YES (35) Formula (36) Conditional Evaluation [EQUIVALENT, 0 ms] (37) Formula (38) Conditional Evaluation [EQUIVALENT, 0 ms] (39) Formula (40) Conditional Evaluation [EQUIVALENT, 0 ms] (41) AND (42) Formula (43) Symbolic evaluation [EQUIVALENT, 0 ms] (44) YES (45) Formula (46) Symbolic evaluation under hypothesis [EQUIVALENT, 0 ms] (47) YES ---------------------------------------- (0) Obligation: Formula: x:sort[a0],y:sort[a33].del'(min(x, y), cons(x, y))=true There are no hypotheses. ---------------------------------------- (1) Conditional Evaluation (EQUIVALENT) The formula could be reduced to the following new obligations by conditional evaluation: Formula: true=true Hypotheses: x:sort[a0],y:sort[a33].equal_sort[a44](eq(min(x, y), x), true_renamed)=true Formula: x:sort[a0],y:sort[a33].del'(min(x, y), y)=true Hypotheses: x:sort[a0],y:sort[a33].equal_sort[a44](eq(min(x, y), x), true_renamed)=false ---------------------------------------- (2) Complex Obligation (AND) ---------------------------------------- (3) Obligation: Formula: true=true Hypotheses: x:sort[a0],y:sort[a33].equal_sort[a44](eq(min(x, y), x), true_renamed)=true ---------------------------------------- (4) Symbolic evaluation (EQUIVALENT) Could be reduced to the following new obligation by simple symbolic evaluation: True ---------------------------------------- (5) YES ---------------------------------------- (6) Obligation: Formula: x:sort[a0],y:sort[a33].del'(min(x, y), y)=true Hypotheses: x:sort[a0],y:sort[a33].equal_sort[a44](eq(min(x, y), x), true_renamed)=false ---------------------------------------- (7) Hypothesis Lifting (EQUIVALENT) Formula could be generalised by hypothesis lifting to the following new obligation: Formula: x:sort[a0],y:sort[a33].(equal_sort[a44](eq(min(x, y), x), true_renamed)=false->del'(min(x, y), y)=true) There are no hypotheses. ---------------------------------------- (8) Obligation: Formula: x:sort[a0],y:sort[a33].(equal_sort[a44](eq(min(x, y), x), true_renamed)=false->del'(min(x, y), y)=true) There are no hypotheses. ---------------------------------------- (9) Induction by algorithm (EQUIVALENT) Induction by algorithm min(x, y) generates the following cases: 1. Base Case: Formula: x':sort[a0].(equal_sort[a44](eq(min(x', nil), x'), true_renamed)=false->del'(min(x', nil), nil)=true) There are no hypotheses. 1. Step Case: Formula: x'':sort[a0],y':sort[a0],z:sort[a33].(equal_sort[a44](eq(min(x'', cons(y', z)), x''), true_renamed)=false->del'(min(x'', cons(y', z)), cons(y', z))=true) Hypotheses: x'':sort[a0],z:sort[a33].(equal_sort[a44](eq(min(x'', z), x''), true_renamed)=false->del'(min(x'', z), z)=true) x'':sort[a0],y':sort[a0].equal_sort[a44](le(x'', y'), true_renamed)=true 2. Step Case: Formula: x'':sort[a0],y':sort[a0],z:sort[a33].(equal_sort[a44](eq(min(x'', cons(y', z)), x''), true_renamed)=false->del'(min(x'', cons(y', z)), cons(y', z))=true) Hypotheses: y':sort[a0],z:sort[a33].(equal_sort[a44](eq(min(y', z), y'), true_renamed)=false->del'(min(y', z), z)=true) x'':sort[a0],y':sort[a0].equal_sort[a44](le(x'', y'), true_renamed)=false ---------------------------------------- (10) Complex Obligation (AND) ---------------------------------------- (11) Obligation: Formula: x':sort[a0].(equal_sort[a44](eq(min(x', nil), x'), true_renamed)=false->del'(min(x', nil), nil)=true) There are no hypotheses. ---------------------------------------- (12) Symbolic evaluation (EQUIVALENT) Could be shown by simple symbolic evaluation. ---------------------------------------- (13) Obligation: Formula: x':sort[a0].~(equal_sort[a44](eq(x', x'), true_renamed)=false) There are no hypotheses. ---------------------------------------- (14) Induction by data structure (EQUIVALENT) Induction by data structure sort[a0] generates the following cases: 1. Base Case: Formula: ~(equal_sort[a44](eq(0, 0), true_renamed)=false) There are no hypotheses. 1. Step Case: Formula: n:sort[a0].~(equal_sort[a44](eq(s(n), s(n)), true_renamed)=false) Hypotheses: n:sort[a0].~(equal_sort[a44](eq(n, n), true_renamed)=false) ---------------------------------------- (15) Complex Obligation (AND) ---------------------------------------- (16) Obligation: Formula: ~(equal_sort[a44](eq(0, 0), true_renamed)=false) There are no hypotheses. ---------------------------------------- (17) Symbolic evaluation (EQUIVALENT) Could be reduced to the following new obligation by simple symbolic evaluation: True ---------------------------------------- (18) YES ---------------------------------------- (19) Obligation: Formula: n:sort[a0].~(equal_sort[a44](eq(s(n), s(n)), true_renamed)=false) Hypotheses: n:sort[a0].~(equal_sort[a44](eq(n, n), true_renamed)=false) ---------------------------------------- (20) Symbolic evaluation under hypothesis (EQUIVALENT) Could be shown using symbolic evaluation under hypothesis, by using the following hypotheses: n:sort[a0].~(equal_sort[a44](eq(n, n), true_renamed)=false) ---------------------------------------- (21) YES ---------------------------------------- (22) Obligation: Formula: x'':sort[a0],y':sort[a0],z:sort[a33].(equal_sort[a44](eq(min(x'', cons(y', z)), x''), true_renamed)=false->del'(min(x'', cons(y', z)), cons(y', z))=true) Hypotheses: x'':sort[a0],z:sort[a33].(equal_sort[a44](eq(min(x'', z), x''), true_renamed)=false->del'(min(x'', z), z)=true) x'':sort[a0],y':sort[a0].equal_sort[a44](le(x'', y'), true_renamed)=true ---------------------------------------- (23) Conditional Evaluation (EQUIVALENT) The formula could be reduced to the following new obligations by conditional evaluation: Formula: x'':sort[a0],z:sort[a33],y':sort[a0].(equal_sort[a44](eq(min(x'', z), x''), true_renamed)=false->del'(min(x'', cons(y', z)), cons(y', z))=true) Hypotheses: x'':sort[a0],z:sort[a33].(equal_sort[a44](eq(min(x'', z), x''), true_renamed)=false->del'(min(x'', z), z)=true) x'':sort[a0],y':sort[a0].equal_sort[a44](le(x'', y'), true_renamed)=true ---------------------------------------- (24) Obligation: Formula: x'':sort[a0],z:sort[a33],y':sort[a0].(equal_sort[a44](eq(min(x'', z), x''), true_renamed)=false->del'(min(x'', cons(y', z)), cons(y', z))=true) Hypotheses: x'':sort[a0],z:sort[a33].(equal_sort[a44](eq(min(x'', z), x''), true_renamed)=false->del'(min(x'', z), z)=true) x'':sort[a0],y':sort[a0].equal_sort[a44](le(x'', y'), true_renamed)=true ---------------------------------------- (25) Conditional Evaluation (EQUIVALENT) The formula could be reduced to the following new obligations by conditional evaluation: Formula: x'':sort[a0],z:sort[a33],y':sort[a0].(equal_sort[a44](eq(min(x'', z), x''), true_renamed)=false->del'(min(x'', z), cons(y', z))=true) Hypotheses: x'':sort[a0],z:sort[a33].(equal_sort[a44](eq(min(x'', z), x''), true_renamed)=false->del'(min(x'', z), z)=true) x'':sort[a0],y':sort[a0].equal_sort[a44](le(x'', y'), true_renamed)=true ---------------------------------------- (26) Obligation: Formula: x'':sort[a0],z:sort[a33],y':sort[a0].(equal_sort[a44](eq(min(x'', z), x''), true_renamed)=false->del'(min(x'', z), cons(y', z))=true) Hypotheses: x'':sort[a0],z:sort[a33].(equal_sort[a44](eq(min(x'', z), x''), true_renamed)=false->del'(min(x'', z), z)=true) x'':sort[a0],y':sort[a0].equal_sort[a44](le(x'', y'), true_renamed)=true ---------------------------------------- (27) Conditional Evaluation (EQUIVALENT) The formula could be reduced to the following new obligations by conditional evaluation: Formula: x'':sort[a0],z:sort[a33].(equal_sort[a44](eq(min(x'', z), x''), true_renamed)=false->true=true) Hypotheses: x'':sort[a0],z:sort[a33].(equal_sort[a44](eq(min(x'', z), x''), true_renamed)=false->del'(min(x'', z), z)=true) x'':sort[a0],y':sort[a0].equal_sort[a44](le(x'', y'), true_renamed)=true x'':sort[a0],z:sort[a33],y':sort[a0].equal_sort[a44](eq(min(x'', z), y'), true_renamed)=true Formula: x'':sort[a0],z:sort[a33].(equal_sort[a44](eq(min(x'', z), x''), true_renamed)=false->del'(min(x'', z), z)=true) Hypotheses: x'':sort[a0],z:sort[a33].(equal_sort[a44](eq(min(x'', z), x''), true_renamed)=false->del'(min(x'', z), z)=true) x'':sort[a0],y':sort[a0].equal_sort[a44](le(x'', y'), true_renamed)=true x'':sort[a0],z:sort[a33],y':sort[a0].equal_sort[a44](eq(min(x'', z), y'), true_renamed)=false ---------------------------------------- (28) Complex Obligation (AND) ---------------------------------------- (29) Obligation: Formula: x'':sort[a0],z:sort[a33].(equal_sort[a44](eq(min(x'', z), x''), true_renamed)=false->true=true) Hypotheses: x'':sort[a0],z:sort[a33].(equal_sort[a44](eq(min(x'', z), x''), true_renamed)=false->del'(min(x'', z), z)=true) x'':sort[a0],y':sort[a0].equal_sort[a44](le(x'', y'), true_renamed)=true x'':sort[a0],z:sort[a33],y':sort[a0].equal_sort[a44](eq(min(x'', z), y'), true_renamed)=true ---------------------------------------- (30) Symbolic evaluation (EQUIVALENT) Could be reduced to the following new obligation by simple symbolic evaluation: True ---------------------------------------- (31) YES ---------------------------------------- (32) Obligation: Formula: x'':sort[a0],z:sort[a33].(equal_sort[a44](eq(min(x'', z), x''), true_renamed)=false->del'(min(x'', z), z)=true) Hypotheses: x'':sort[a0],z:sort[a33].(equal_sort[a44](eq(min(x'', z), x''), true_renamed)=false->del'(min(x'', z), z)=true) x'':sort[a0],y':sort[a0].equal_sort[a44](le(x'', y'), true_renamed)=true x'':sort[a0],z:sort[a33],y':sort[a0].equal_sort[a44](eq(min(x'', z), y'), true_renamed)=false ---------------------------------------- (33) Symbolic evaluation under hypothesis (EQUIVALENT) Could be shown using symbolic evaluation under hypothesis, by using the following hypotheses: x'':sort[a0],z:sort[a33].(equal_sort[a44](eq(min(x'', z), x''), true_renamed)=false->del'(min(x'', z), z)=true) ---------------------------------------- (34) YES ---------------------------------------- (35) Obligation: Formula: x'':sort[a0],y':sort[a0],z:sort[a33].(equal_sort[a44](eq(min(x'', cons(y', z)), x''), true_renamed)=false->del'(min(x'', cons(y', z)), cons(y', z))=true) Hypotheses: y':sort[a0],z:sort[a33].(equal_sort[a44](eq(min(y', z), y'), true_renamed)=false->del'(min(y', z), z)=true) x'':sort[a0],y':sort[a0].equal_sort[a44](le(x'', y'), true_renamed)=false ---------------------------------------- (36) Conditional Evaluation (EQUIVALENT) The formula could be reduced to the following new obligations by conditional evaluation: Formula: y':sort[a0],z:sort[a33],x'':sort[a0].(equal_sort[a44](eq(min(y', z), x''), true_renamed)=false->del'(min(x'', cons(y', z)), cons(y', z))=true) Hypotheses: y':sort[a0],z:sort[a33].(equal_sort[a44](eq(min(y', z), y'), true_renamed)=false->del'(min(y', z), z)=true) x'':sort[a0],y':sort[a0].equal_sort[a44](le(x'', y'), true_renamed)=false ---------------------------------------- (37) Obligation: Formula: y':sort[a0],z:sort[a33],x'':sort[a0].(equal_sort[a44](eq(min(y', z), x''), true_renamed)=false->del'(min(x'', cons(y', z)), cons(y', z))=true) Hypotheses: y':sort[a0],z:sort[a33].(equal_sort[a44](eq(min(y', z), y'), true_renamed)=false->del'(min(y', z), z)=true) x'':sort[a0],y':sort[a0].equal_sort[a44](le(x'', y'), true_renamed)=false ---------------------------------------- (38) Conditional Evaluation (EQUIVALENT) The formula could be reduced to the following new obligations by conditional evaluation: Formula: y':sort[a0],z:sort[a33],x'':sort[a0].(equal_sort[a44](eq(min(y', z), x''), true_renamed)=false->del'(min(y', z), cons(y', z))=true) Hypotheses: y':sort[a0],z:sort[a33].(equal_sort[a44](eq(min(y', z), y'), true_renamed)=false->del'(min(y', z), z)=true) x'':sort[a0],y':sort[a0].equal_sort[a44](le(x'', y'), true_renamed)=false ---------------------------------------- (39) Obligation: Formula: y':sort[a0],z:sort[a33],x'':sort[a0].(equal_sort[a44](eq(min(y', z), x''), true_renamed)=false->del'(min(y', z), cons(y', z))=true) Hypotheses: y':sort[a0],z:sort[a33].(equal_sort[a44](eq(min(y', z), y'), true_renamed)=false->del'(min(y', z), z)=true) x'':sort[a0],y':sort[a0].equal_sort[a44](le(x'', y'), true_renamed)=false ---------------------------------------- (40) Conditional Evaluation (EQUIVALENT) The formula could be reduced to the following new obligations by conditional evaluation: Formula: y':sort[a0],z:sort[a33],x'':sort[a0].(equal_sort[a44](eq(min(y', z), x''), true_renamed)=false->true=true) Hypotheses: y':sort[a0],z:sort[a33].(equal_sort[a44](eq(min(y', z), y'), true_renamed)=false->del'(min(y', z), z)=true) x'':sort[a0],y':sort[a0].equal_sort[a44](le(x'', y'), true_renamed)=false y':sort[a0],z:sort[a33].equal_sort[a44](eq(min(y', z), y'), true_renamed)=true Formula: y':sort[a0],z:sort[a33],x'':sort[a0].(equal_sort[a44](eq(min(y', z), x''), true_renamed)=false->del'(min(y', z), z)=true) Hypotheses: y':sort[a0],z:sort[a33].(equal_sort[a44](eq(min(y', z), y'), true_renamed)=false->del'(min(y', z), z)=true) x'':sort[a0],y':sort[a0].equal_sort[a44](le(x'', y'), true_renamed)=false y':sort[a0],z:sort[a33].equal_sort[a44](eq(min(y', z), y'), true_renamed)=false ---------------------------------------- (41) Complex Obligation (AND) ---------------------------------------- (42) Obligation: Formula: y':sort[a0],z:sort[a33],x'':sort[a0].(equal_sort[a44](eq(min(y', z), x''), true_renamed)=false->true=true) Hypotheses: y':sort[a0],z:sort[a33].(equal_sort[a44](eq(min(y', z), y'), true_renamed)=false->del'(min(y', z), z)=true) x'':sort[a0],y':sort[a0].equal_sort[a44](le(x'', y'), true_renamed)=false y':sort[a0],z:sort[a33].equal_sort[a44](eq(min(y', z), y'), true_renamed)=true ---------------------------------------- (43) Symbolic evaluation (EQUIVALENT) Could be reduced to the following new obligation by simple symbolic evaluation: True ---------------------------------------- (44) YES ---------------------------------------- (45) Obligation: Formula: y':sort[a0],z:sort[a33],x'':sort[a0].(equal_sort[a44](eq(min(y', z), x''), true_renamed)=false->del'(min(y', z), z)=true) Hypotheses: y':sort[a0],z:sort[a33].(equal_sort[a44](eq(min(y', z), y'), true_renamed)=false->del'(min(y', z), z)=true) x'':sort[a0],y':sort[a0].equal_sort[a44](le(x'', y'), true_renamed)=false y':sort[a0],z:sort[a33].equal_sort[a44](eq(min(y', z), y'), true_renamed)=false ---------------------------------------- (46) Symbolic evaluation under hypothesis (EQUIVALENT) Could be shown using symbolic evaluation under hypothesis, by using the following hypotheses: y':sort[a0],z:sort[a33].(equal_sort[a44](eq(min(y', z), y'), true_renamed)=false->del'(min(y', z), z)=true) y':sort[a0],z:sort[a33].equal_sort[a44](eq(min(y', z), y'), true_renamed)=false ---------------------------------------- (47) YES
min(x, nil) → x
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)
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'(x3, cons(y2, z')) → if2'(eq(x3, y2), x3, y2, z')
if2'(true_renamed, x6, y5, xs'') → true
if2'(false_renamed, x7, y6, xs1) → del'(x7, xs1)
del'(x8, nil) → false
min(x', nil) → x'
min(x'', cons(y', z)) → if1(le(x'', y'), x'', y', z)
if1(true_renamed, x1, y'', xs) → min(x1, xs)
if1(false_renamed, x2, y1, xs') → min(y1, xs')
del(x3, cons(y2, z')) → if2(eq(x3, y2), x3, y2, z')
eq(0, 0) → true_renamed
eq(0, s(y3)) → false_renamed
eq(s(x4), 0) → false_renamed
eq(s(x5), s(y4)) → eq(x5, y4)
if2(true_renamed, x6, y5, xs'') → xs''
if2(false_renamed, x7, y6, xs1) → cons(y6, del(x7, xs1))
del(x8, nil) → nil
le(0, y7) → true_renamed
le(s(x9), 0) → false_renamed
le(s(x10), s(y8)) → le(x10, y8)
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(v25)) → false
equal_sort[a0](s(v26), 0) → false
equal_sort[a0](s(v26), s(v27)) → equal_sort[a0](v26, v27)
equal_sort[a33](nil, nil) → true
equal_sort[a33](nil, cons(v28, v29)) → false
equal_sort[a33](cons(v30, v31), nil) → false
equal_sort[a33](cons(v30, v31), cons(v32, v33)) → and(equal_sort[a0](v30, v32), equal_sort[a33](v31, v33))
equal_sort[a44](true_renamed, true_renamed) → true
equal_sort[a44](true_renamed, false_renamed) → false
equal_sort[a44](false_renamed, true_renamed) → false
equal_sort[a44](false_renamed, false_renamed) → true
equal_sort[a62](witness_sort[a62], witness_sort[a62]) → true
del'(x3, cons(y2, z')) → if2'(eq(x3, y2), x3, y2, z')
if2'(true_renamed, x6, y5, xs'') → true
if2'(false_renamed, x7, y6, xs1) → del'(x7, xs1)
del'(x8, nil) → false
min(x', nil) → x'
min(x'', cons(y', z)) → if1(le(x'', y'), x'', y', z)
if1(true_renamed, x1, y'', xs) → min(x1, xs)
if1(false_renamed, x2, y1, xs') → min(y1, xs')
del(x3, cons(y2, z')) → if2(eq(x3, y2), x3, y2, z')
eq(0, 0) → true_renamed
eq(0, s(y3)) → false_renamed
eq(s(x4), 0) → false_renamed
eq(s(x5), s(y4)) → eq(x5, y4)
if2(true_renamed, x6, y5, xs'') → xs''
if2(false_renamed, x7, y6, xs1) → cons(y6, del(x7, xs1))
del(x8, nil) → nil
le(0, y7) → true_renamed
le(s(x9), 0) → false_renamed
le(s(x10), s(y8)) → le(x10, y8)
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(v25)) → false
equal_sort[a0](s(v26), 0) → false
equal_sort[a0](s(v26), s(v27)) → equal_sort[a0](v26, v27)
equal_sort[a33](nil, nil) → true
equal_sort[a33](nil, cons(v28, v29)) → false
equal_sort[a33](cons(v30, v31), nil) → false
equal_sort[a33](cons(v30, v31), cons(v32, v33)) → and(equal_sort[a0](v30, v32), equal_sort[a33](v31, v33))
equal_sort[a44](true_renamed, true_renamed) → true
equal_sort[a44](true_renamed, false_renamed) → false
equal_sort[a44](false_renamed, true_renamed) → false
equal_sort[a44](false_renamed, false_renamed) → true
equal_sort[a62](witness_sort[a62], witness_sort[a62]) → true
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
min(x0, cons(x1, x2))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, 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_renamed, x0, x1, x2)
if2(false_renamed, 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[a33](nil, nil)
equal_sort[a33](nil, cons(x0, x1))
equal_sort[a33](cons(x0, x1), nil)
equal_sort[a33](cons(x0, x1), cons(x2, x3))
equal_sort[a44](true_renamed, true_renamed)
equal_sort[a44](true_renamed, false_renamed)
equal_sort[a44](false_renamed, true_renamed)
equal_sort[a44](false_renamed, false_renamed)
equal_sort[a62](witness_sort[a62], witness_sort[a62])
DEL'(x3, cons(y2, z')) → IF2'(eq(x3, y2), x3, y2, z')
DEL'(x3, cons(y2, z')) → EQ(x3, y2)
IF2'(false_renamed, x7, y6, xs1) → DEL'(x7, xs1)
MIN(x'', cons(y', z)) → IF1(le(x'', y'), x'', y', z)
MIN(x'', cons(y', z)) → LE(x'', y')
IF1(true_renamed, x1, y'', xs) → MIN(x1, xs)
IF1(false_renamed, x2, y1, xs') → MIN(y1, xs')
DEL(x3, cons(y2, z')) → IF2(eq(x3, y2), x3, y2, z')
DEL(x3, cons(y2, z')) → EQ(x3, y2)
EQ(s(x5), s(y4)) → EQ(x5, y4)
IF2(false_renamed, x7, y6, xs1) → DEL(x7, xs1)
LE(s(x10), s(y8)) → LE(x10, y8)
EQUAL_SORT[A0](s(v26), s(v27)) → EQUAL_SORT[A0](v26, v27)
EQUAL_SORT[A33](cons(v30, v31), cons(v32, v33)) → AND(equal_sort[a0](v30, v32), equal_sort[a33](v31, v33))
EQUAL_SORT[A33](cons(v30, v31), cons(v32, v33)) → EQUAL_SORT[A0](v30, v32)
EQUAL_SORT[A33](cons(v30, v31), cons(v32, v33)) → EQUAL_SORT[A33](v31, v33)
del'(x3, cons(y2, z')) → if2'(eq(x3, y2), x3, y2, z')
if2'(true_renamed, x6, y5, xs'') → true
if2'(false_renamed, x7, y6, xs1) → del'(x7, xs1)
del'(x8, nil) → false
min(x', nil) → x'
min(x'', cons(y', z)) → if1(le(x'', y'), x'', y', z)
if1(true_renamed, x1, y'', xs) → min(x1, xs)
if1(false_renamed, x2, y1, xs') → min(y1, xs')
del(x3, cons(y2, z')) → if2(eq(x3, y2), x3, y2, z')
eq(0, 0) → true_renamed
eq(0, s(y3)) → false_renamed
eq(s(x4), 0) → false_renamed
eq(s(x5), s(y4)) → eq(x5, y4)
if2(true_renamed, x6, y5, xs'') → xs''
if2(false_renamed, x7, y6, xs1) → cons(y6, del(x7, xs1))
del(x8, nil) → nil
le(0, y7) → true_renamed
le(s(x9), 0) → false_renamed
le(s(x10), s(y8)) → le(x10, y8)
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(v25)) → false
equal_sort[a0](s(v26), 0) → false
equal_sort[a0](s(v26), s(v27)) → equal_sort[a0](v26, v27)
equal_sort[a33](nil, nil) → true
equal_sort[a33](nil, cons(v28, v29)) → false
equal_sort[a33](cons(v30, v31), nil) → false
equal_sort[a33](cons(v30, v31), cons(v32, v33)) → and(equal_sort[a0](v30, v32), equal_sort[a33](v31, v33))
equal_sort[a44](true_renamed, true_renamed) → true
equal_sort[a44](true_renamed, false_renamed) → false
equal_sort[a44](false_renamed, true_renamed) → false
equal_sort[a44](false_renamed, false_renamed) → true
equal_sort[a62](witness_sort[a62], witness_sort[a62]) → true
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
min(x0, cons(x1, x2))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, 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_renamed, x0, x1, x2)
if2(false_renamed, 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[a33](nil, nil)
equal_sort[a33](nil, cons(x0, x1))
equal_sort[a33](cons(x0, x1), nil)
equal_sort[a33](cons(x0, x1), cons(x2, x3))
equal_sort[a44](true_renamed, true_renamed)
equal_sort[a44](true_renamed, false_renamed)
equal_sort[a44](false_renamed, true_renamed)
equal_sort[a44](false_renamed, false_renamed)
equal_sort[a62](witness_sort[a62], witness_sort[a62])
EQUAL_SORT[A0](s(v26), s(v27)) → EQUAL_SORT[A0](v26, v27)
del'(x3, cons(y2, z')) → if2'(eq(x3, y2), x3, y2, z')
if2'(true_renamed, x6, y5, xs'') → true
if2'(false_renamed, x7, y6, xs1) → del'(x7, xs1)
del'(x8, nil) → false
min(x', nil) → x'
min(x'', cons(y', z)) → if1(le(x'', y'), x'', y', z)
if1(true_renamed, x1, y'', xs) → min(x1, xs)
if1(false_renamed, x2, y1, xs') → min(y1, xs')
del(x3, cons(y2, z')) → if2(eq(x3, y2), x3, y2, z')
eq(0, 0) → true_renamed
eq(0, s(y3)) → false_renamed
eq(s(x4), 0) → false_renamed
eq(s(x5), s(y4)) → eq(x5, y4)
if2(true_renamed, x6, y5, xs'') → xs''
if2(false_renamed, x7, y6, xs1) → cons(y6, del(x7, xs1))
del(x8, nil) → nil
le(0, y7) → true_renamed
le(s(x9), 0) → false_renamed
le(s(x10), s(y8)) → le(x10, y8)
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(v25)) → false
equal_sort[a0](s(v26), 0) → false
equal_sort[a0](s(v26), s(v27)) → equal_sort[a0](v26, v27)
equal_sort[a33](nil, nil) → true
equal_sort[a33](nil, cons(v28, v29)) → false
equal_sort[a33](cons(v30, v31), nil) → false
equal_sort[a33](cons(v30, v31), cons(v32, v33)) → and(equal_sort[a0](v30, v32), equal_sort[a33](v31, v33))
equal_sort[a44](true_renamed, true_renamed) → true
equal_sort[a44](true_renamed, false_renamed) → false
equal_sort[a44](false_renamed, true_renamed) → false
equal_sort[a44](false_renamed, false_renamed) → true
equal_sort[a62](witness_sort[a62], witness_sort[a62]) → true
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
min(x0, cons(x1, x2))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, 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_renamed, x0, x1, x2)
if2(false_renamed, 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[a33](nil, nil)
equal_sort[a33](nil, cons(x0, x1))
equal_sort[a33](cons(x0, x1), nil)
equal_sort[a33](cons(x0, x1), cons(x2, x3))
equal_sort[a44](true_renamed, true_renamed)
equal_sort[a44](true_renamed, false_renamed)
equal_sort[a44](false_renamed, true_renamed)
equal_sort[a44](false_renamed, false_renamed)
equal_sort[a62](witness_sort[a62], witness_sort[a62])
EQUAL_SORT[A0](s(v26), s(v27)) → EQUAL_SORT[A0](v26, v27)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
min(x0, cons(x1, x2))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, 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_renamed, x0, x1, x2)
if2(false_renamed, 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[a33](nil, nil)
equal_sort[a33](nil, cons(x0, x1))
equal_sort[a33](cons(x0, x1), nil)
equal_sort[a33](cons(x0, x1), cons(x2, x3))
equal_sort[a44](true_renamed, true_renamed)
equal_sort[a44](true_renamed, false_renamed)
equal_sort[a44](false_renamed, true_renamed)
equal_sort[a44](false_renamed, false_renamed)
equal_sort[a62](witness_sort[a62], witness_sort[a62])
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
min(x0, cons(x1, x2))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, 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_renamed, x0, x1, x2)
if2(false_renamed, 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[a33](nil, nil)
equal_sort[a33](nil, cons(x0, x1))
equal_sort[a33](cons(x0, x1), nil)
equal_sort[a33](cons(x0, x1), cons(x2, x3))
equal_sort[a44](true_renamed, true_renamed)
equal_sort[a44](true_renamed, false_renamed)
equal_sort[a44](false_renamed, true_renamed)
equal_sort[a44](false_renamed, false_renamed)
equal_sort[a62](witness_sort[a62], witness_sort[a62])
EQUAL_SORT[A0](s(v26), s(v27)) → EQUAL_SORT[A0](v26, v27)
From the DPs we obtained the following set of size-change graphs:
EQUAL_SORT[A33](cons(v30, v31), cons(v32, v33)) → EQUAL_SORT[A33](v31, v33)
del'(x3, cons(y2, z')) → if2'(eq(x3, y2), x3, y2, z')
if2'(true_renamed, x6, y5, xs'') → true
if2'(false_renamed, x7, y6, xs1) → del'(x7, xs1)
del'(x8, nil) → false
min(x', nil) → x'
min(x'', cons(y', z)) → if1(le(x'', y'), x'', y', z)
if1(true_renamed, x1, y'', xs) → min(x1, xs)
if1(false_renamed, x2, y1, xs') → min(y1, xs')
del(x3, cons(y2, z')) → if2(eq(x3, y2), x3, y2, z')
eq(0, 0) → true_renamed
eq(0, s(y3)) → false_renamed
eq(s(x4), 0) → false_renamed
eq(s(x5), s(y4)) → eq(x5, y4)
if2(true_renamed, x6, y5, xs'') → xs''
if2(false_renamed, x7, y6, xs1) → cons(y6, del(x7, xs1))
del(x8, nil) → nil
le(0, y7) → true_renamed
le(s(x9), 0) → false_renamed
le(s(x10), s(y8)) → le(x10, y8)
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(v25)) → false
equal_sort[a0](s(v26), 0) → false
equal_sort[a0](s(v26), s(v27)) → equal_sort[a0](v26, v27)
equal_sort[a33](nil, nil) → true
equal_sort[a33](nil, cons(v28, v29)) → false
equal_sort[a33](cons(v30, v31), nil) → false
equal_sort[a33](cons(v30, v31), cons(v32, v33)) → and(equal_sort[a0](v30, v32), equal_sort[a33](v31, v33))
equal_sort[a44](true_renamed, true_renamed) → true
equal_sort[a44](true_renamed, false_renamed) → false
equal_sort[a44](false_renamed, true_renamed) → false
equal_sort[a44](false_renamed, false_renamed) → true
equal_sort[a62](witness_sort[a62], witness_sort[a62]) → true
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
min(x0, cons(x1, x2))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, 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_renamed, x0, x1, x2)
if2(false_renamed, 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[a33](nil, nil)
equal_sort[a33](nil, cons(x0, x1))
equal_sort[a33](cons(x0, x1), nil)
equal_sort[a33](cons(x0, x1), cons(x2, x3))
equal_sort[a44](true_renamed, true_renamed)
equal_sort[a44](true_renamed, false_renamed)
equal_sort[a44](false_renamed, true_renamed)
equal_sort[a44](false_renamed, false_renamed)
equal_sort[a62](witness_sort[a62], witness_sort[a62])
EQUAL_SORT[A33](cons(v30, v31), cons(v32, v33)) → EQUAL_SORT[A33](v31, v33)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
min(x0, cons(x1, x2))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, 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_renamed, x0, x1, x2)
if2(false_renamed, 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[a33](nil, nil)
equal_sort[a33](nil, cons(x0, x1))
equal_sort[a33](cons(x0, x1), nil)
equal_sort[a33](cons(x0, x1), cons(x2, x3))
equal_sort[a44](true_renamed, true_renamed)
equal_sort[a44](true_renamed, false_renamed)
equal_sort[a44](false_renamed, true_renamed)
equal_sort[a44](false_renamed, false_renamed)
equal_sort[a62](witness_sort[a62], witness_sort[a62])
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
min(x0, cons(x1, x2))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, 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_renamed, x0, x1, x2)
if2(false_renamed, 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[a33](nil, nil)
equal_sort[a33](nil, cons(x0, x1))
equal_sort[a33](cons(x0, x1), nil)
equal_sort[a33](cons(x0, x1), cons(x2, x3))
equal_sort[a44](true_renamed, true_renamed)
equal_sort[a44](true_renamed, false_renamed)
equal_sort[a44](false_renamed, true_renamed)
equal_sort[a44](false_renamed, false_renamed)
equal_sort[a62](witness_sort[a62], witness_sort[a62])
EQUAL_SORT[A33](cons(v30, v31), cons(v32, v33)) → EQUAL_SORT[A33](v31, v33)
From the DPs we obtained the following set of size-change graphs:
LE(s(x10), s(y8)) → LE(x10, y8)
del'(x3, cons(y2, z')) → if2'(eq(x3, y2), x3, y2, z')
if2'(true_renamed, x6, y5, xs'') → true
if2'(false_renamed, x7, y6, xs1) → del'(x7, xs1)
del'(x8, nil) → false
min(x', nil) → x'
min(x'', cons(y', z)) → if1(le(x'', y'), x'', y', z)
if1(true_renamed, x1, y'', xs) → min(x1, xs)
if1(false_renamed, x2, y1, xs') → min(y1, xs')
del(x3, cons(y2, z')) → if2(eq(x3, y2), x3, y2, z')
eq(0, 0) → true_renamed
eq(0, s(y3)) → false_renamed
eq(s(x4), 0) → false_renamed
eq(s(x5), s(y4)) → eq(x5, y4)
if2(true_renamed, x6, y5, xs'') → xs''
if2(false_renamed, x7, y6, xs1) → cons(y6, del(x7, xs1))
del(x8, nil) → nil
le(0, y7) → true_renamed
le(s(x9), 0) → false_renamed
le(s(x10), s(y8)) → le(x10, y8)
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(v25)) → false
equal_sort[a0](s(v26), 0) → false
equal_sort[a0](s(v26), s(v27)) → equal_sort[a0](v26, v27)
equal_sort[a33](nil, nil) → true
equal_sort[a33](nil, cons(v28, v29)) → false
equal_sort[a33](cons(v30, v31), nil) → false
equal_sort[a33](cons(v30, v31), cons(v32, v33)) → and(equal_sort[a0](v30, v32), equal_sort[a33](v31, v33))
equal_sort[a44](true_renamed, true_renamed) → true
equal_sort[a44](true_renamed, false_renamed) → false
equal_sort[a44](false_renamed, true_renamed) → false
equal_sort[a44](false_renamed, false_renamed) → true
equal_sort[a62](witness_sort[a62], witness_sort[a62]) → true
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
min(x0, cons(x1, x2))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, 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_renamed, x0, x1, x2)
if2(false_renamed, 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[a33](nil, nil)
equal_sort[a33](nil, cons(x0, x1))
equal_sort[a33](cons(x0, x1), nil)
equal_sort[a33](cons(x0, x1), cons(x2, x3))
equal_sort[a44](true_renamed, true_renamed)
equal_sort[a44](true_renamed, false_renamed)
equal_sort[a44](false_renamed, true_renamed)
equal_sort[a44](false_renamed, false_renamed)
equal_sort[a62](witness_sort[a62], witness_sort[a62])
LE(s(x10), s(y8)) → LE(x10, y8)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
min(x0, cons(x1, x2))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, 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_renamed, x0, x1, x2)
if2(false_renamed, 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[a33](nil, nil)
equal_sort[a33](nil, cons(x0, x1))
equal_sort[a33](cons(x0, x1), nil)
equal_sort[a33](cons(x0, x1), cons(x2, x3))
equal_sort[a44](true_renamed, true_renamed)
equal_sort[a44](true_renamed, false_renamed)
equal_sort[a44](false_renamed, true_renamed)
equal_sort[a44](false_renamed, false_renamed)
equal_sort[a62](witness_sort[a62], witness_sort[a62])
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
min(x0, cons(x1, x2))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, 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_renamed, x0, x1, x2)
if2(false_renamed, 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[a33](nil, nil)
equal_sort[a33](nil, cons(x0, x1))
equal_sort[a33](cons(x0, x1), nil)
equal_sort[a33](cons(x0, x1), cons(x2, x3))
equal_sort[a44](true_renamed, true_renamed)
equal_sort[a44](true_renamed, false_renamed)
equal_sort[a44](false_renamed, true_renamed)
equal_sort[a44](false_renamed, false_renamed)
equal_sort[a62](witness_sort[a62], witness_sort[a62])
LE(s(x10), s(y8)) → LE(x10, y8)
From the DPs we obtained the following set of size-change graphs:
EQ(s(x5), s(y4)) → EQ(x5, y4)
del'(x3, cons(y2, z')) → if2'(eq(x3, y2), x3, y2, z')
if2'(true_renamed, x6, y5, xs'') → true
if2'(false_renamed, x7, y6, xs1) → del'(x7, xs1)
del'(x8, nil) → false
min(x', nil) → x'
min(x'', cons(y', z)) → if1(le(x'', y'), x'', y', z)
if1(true_renamed, x1, y'', xs) → min(x1, xs)
if1(false_renamed, x2, y1, xs') → min(y1, xs')
del(x3, cons(y2, z')) → if2(eq(x3, y2), x3, y2, z')
eq(0, 0) → true_renamed
eq(0, s(y3)) → false_renamed
eq(s(x4), 0) → false_renamed
eq(s(x5), s(y4)) → eq(x5, y4)
if2(true_renamed, x6, y5, xs'') → xs''
if2(false_renamed, x7, y6, xs1) → cons(y6, del(x7, xs1))
del(x8, nil) → nil
le(0, y7) → true_renamed
le(s(x9), 0) → false_renamed
le(s(x10), s(y8)) → le(x10, y8)
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(v25)) → false
equal_sort[a0](s(v26), 0) → false
equal_sort[a0](s(v26), s(v27)) → equal_sort[a0](v26, v27)
equal_sort[a33](nil, nil) → true
equal_sort[a33](nil, cons(v28, v29)) → false
equal_sort[a33](cons(v30, v31), nil) → false
equal_sort[a33](cons(v30, v31), cons(v32, v33)) → and(equal_sort[a0](v30, v32), equal_sort[a33](v31, v33))
equal_sort[a44](true_renamed, true_renamed) → true
equal_sort[a44](true_renamed, false_renamed) → false
equal_sort[a44](false_renamed, true_renamed) → false
equal_sort[a44](false_renamed, false_renamed) → true
equal_sort[a62](witness_sort[a62], witness_sort[a62]) → true
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
min(x0, cons(x1, x2))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, 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_renamed, x0, x1, x2)
if2(false_renamed, 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[a33](nil, nil)
equal_sort[a33](nil, cons(x0, x1))
equal_sort[a33](cons(x0, x1), nil)
equal_sort[a33](cons(x0, x1), cons(x2, x3))
equal_sort[a44](true_renamed, true_renamed)
equal_sort[a44](true_renamed, false_renamed)
equal_sort[a44](false_renamed, true_renamed)
equal_sort[a44](false_renamed, false_renamed)
equal_sort[a62](witness_sort[a62], witness_sort[a62])
EQ(s(x5), s(y4)) → EQ(x5, y4)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
min(x0, cons(x1, x2))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, 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_renamed, x0, x1, x2)
if2(false_renamed, 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[a33](nil, nil)
equal_sort[a33](nil, cons(x0, x1))
equal_sort[a33](cons(x0, x1), nil)
equal_sort[a33](cons(x0, x1), cons(x2, x3))
equal_sort[a44](true_renamed, true_renamed)
equal_sort[a44](true_renamed, false_renamed)
equal_sort[a44](false_renamed, true_renamed)
equal_sort[a44](false_renamed, false_renamed)
equal_sort[a62](witness_sort[a62], witness_sort[a62])
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
min(x0, cons(x1, x2))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, 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_renamed, x0, x1, x2)
if2(false_renamed, 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[a33](nil, nil)
equal_sort[a33](nil, cons(x0, x1))
equal_sort[a33](cons(x0, x1), nil)
equal_sort[a33](cons(x0, x1), cons(x2, x3))
equal_sort[a44](true_renamed, true_renamed)
equal_sort[a44](true_renamed, false_renamed)
equal_sort[a44](false_renamed, true_renamed)
equal_sort[a44](false_renamed, false_renamed)
equal_sort[a62](witness_sort[a62], witness_sort[a62])
EQ(s(x5), s(y4)) → EQ(x5, y4)
From the DPs we obtained the following set of size-change graphs:
IF2(false_renamed, x7, y6, xs1) → DEL(x7, xs1)
DEL(x3, cons(y2, z')) → IF2(eq(x3, y2), x3, y2, z')
del'(x3, cons(y2, z')) → if2'(eq(x3, y2), x3, y2, z')
if2'(true_renamed, x6, y5, xs'') → true
if2'(false_renamed, x7, y6, xs1) → del'(x7, xs1)
del'(x8, nil) → false
min(x', nil) → x'
min(x'', cons(y', z)) → if1(le(x'', y'), x'', y', z)
if1(true_renamed, x1, y'', xs) → min(x1, xs)
if1(false_renamed, x2, y1, xs') → min(y1, xs')
del(x3, cons(y2, z')) → if2(eq(x3, y2), x3, y2, z')
eq(0, 0) → true_renamed
eq(0, s(y3)) → false_renamed
eq(s(x4), 0) → false_renamed
eq(s(x5), s(y4)) → eq(x5, y4)
if2(true_renamed, x6, y5, xs'') → xs''
if2(false_renamed, x7, y6, xs1) → cons(y6, del(x7, xs1))
del(x8, nil) → nil
le(0, y7) → true_renamed
le(s(x9), 0) → false_renamed
le(s(x10), s(y8)) → le(x10, y8)
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(v25)) → false
equal_sort[a0](s(v26), 0) → false
equal_sort[a0](s(v26), s(v27)) → equal_sort[a0](v26, v27)
equal_sort[a33](nil, nil) → true
equal_sort[a33](nil, cons(v28, v29)) → false
equal_sort[a33](cons(v30, v31), nil) → false
equal_sort[a33](cons(v30, v31), cons(v32, v33)) → and(equal_sort[a0](v30, v32), equal_sort[a33](v31, v33))
equal_sort[a44](true_renamed, true_renamed) → true
equal_sort[a44](true_renamed, false_renamed) → false
equal_sort[a44](false_renamed, true_renamed) → false
equal_sort[a44](false_renamed, false_renamed) → true
equal_sort[a62](witness_sort[a62], witness_sort[a62]) → true
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
min(x0, cons(x1, x2))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, 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_renamed, x0, x1, x2)
if2(false_renamed, 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[a33](nil, nil)
equal_sort[a33](nil, cons(x0, x1))
equal_sort[a33](cons(x0, x1), nil)
equal_sort[a33](cons(x0, x1), cons(x2, x3))
equal_sort[a44](true_renamed, true_renamed)
equal_sort[a44](true_renamed, false_renamed)
equal_sort[a44](false_renamed, true_renamed)
equal_sort[a44](false_renamed, false_renamed)
equal_sort[a62](witness_sort[a62], witness_sort[a62])
IF2(false_renamed, x7, y6, xs1) → DEL(x7, xs1)
DEL(x3, cons(y2, z')) → IF2(eq(x3, y2), x3, y2, z')
eq(0, 0) → true_renamed
eq(0, s(y3)) → false_renamed
eq(s(x4), 0) → false_renamed
eq(s(x5), s(y4)) → eq(x5, y4)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
min(x0, cons(x1, x2))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, 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_renamed, x0, x1, x2)
if2(false_renamed, 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[a33](nil, nil)
equal_sort[a33](nil, cons(x0, x1))
equal_sort[a33](cons(x0, x1), nil)
equal_sort[a33](cons(x0, x1), cons(x2, x3))
equal_sort[a44](true_renamed, true_renamed)
equal_sort[a44](true_renamed, false_renamed)
equal_sort[a44](false_renamed, true_renamed)
equal_sort[a44](false_renamed, false_renamed)
equal_sort[a62](witness_sort[a62], witness_sort[a62])
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
min(x0, cons(x1, x2))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, x0, x1, x2)
del(x0, cons(x1, x2))
if2(true_renamed, x0, x1, x2)
if2(false_renamed, 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[a33](nil, nil)
equal_sort[a33](nil, cons(x0, x1))
equal_sort[a33](cons(x0, x1), nil)
equal_sort[a33](cons(x0, x1), cons(x2, x3))
equal_sort[a44](true_renamed, true_renamed)
equal_sort[a44](true_renamed, false_renamed)
equal_sort[a44](false_renamed, true_renamed)
equal_sort[a44](false_renamed, false_renamed)
equal_sort[a62](witness_sort[a62], witness_sort[a62])
IF2(false_renamed, x7, y6, xs1) → DEL(x7, xs1)
DEL(x3, cons(y2, z')) → IF2(eq(x3, y2), x3, y2, z')
eq(0, 0) → true_renamed
eq(0, s(y3)) → false_renamed
eq(s(x4), 0) → false_renamed
eq(s(x5), s(y4)) → eq(x5, y4)
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:
IF1(true_renamed, x1, y'', xs) → MIN(x1, xs)
MIN(x'', cons(y', z)) → IF1(le(x'', y'), x'', y', z)
IF1(false_renamed, x2, y1, xs') → MIN(y1, xs')
del'(x3, cons(y2, z')) → if2'(eq(x3, y2), x3, y2, z')
if2'(true_renamed, x6, y5, xs'') → true
if2'(false_renamed, x7, y6, xs1) → del'(x7, xs1)
del'(x8, nil) → false
min(x', nil) → x'
min(x'', cons(y', z)) → if1(le(x'', y'), x'', y', z)
if1(true_renamed, x1, y'', xs) → min(x1, xs)
if1(false_renamed, x2, y1, xs') → min(y1, xs')
del(x3, cons(y2, z')) → if2(eq(x3, y2), x3, y2, z')
eq(0, 0) → true_renamed
eq(0, s(y3)) → false_renamed
eq(s(x4), 0) → false_renamed
eq(s(x5), s(y4)) → eq(x5, y4)
if2(true_renamed, x6, y5, xs'') → xs''
if2(false_renamed, x7, y6, xs1) → cons(y6, del(x7, xs1))
del(x8, nil) → nil
le(0, y7) → true_renamed
le(s(x9), 0) → false_renamed
le(s(x10), s(y8)) → le(x10, y8)
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(v25)) → false
equal_sort[a0](s(v26), 0) → false
equal_sort[a0](s(v26), s(v27)) → equal_sort[a0](v26, v27)
equal_sort[a33](nil, nil) → true
equal_sort[a33](nil, cons(v28, v29)) → false
equal_sort[a33](cons(v30, v31), nil) → false
equal_sort[a33](cons(v30, v31), cons(v32, v33)) → and(equal_sort[a0](v30, v32), equal_sort[a33](v31, v33))
equal_sort[a44](true_renamed, true_renamed) → true
equal_sort[a44](true_renamed, false_renamed) → false
equal_sort[a44](false_renamed, true_renamed) → false
equal_sort[a44](false_renamed, false_renamed) → true
equal_sort[a62](witness_sort[a62], witness_sort[a62]) → true
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
min(x0, cons(x1, x2))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, 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_renamed, x0, x1, x2)
if2(false_renamed, 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[a33](nil, nil)
equal_sort[a33](nil, cons(x0, x1))
equal_sort[a33](cons(x0, x1), nil)
equal_sort[a33](cons(x0, x1), cons(x2, x3))
equal_sort[a44](true_renamed, true_renamed)
equal_sort[a44](true_renamed, false_renamed)
equal_sort[a44](false_renamed, true_renamed)
equal_sort[a44](false_renamed, false_renamed)
equal_sort[a62](witness_sort[a62], witness_sort[a62])
IF1(true_renamed, x1, y'', xs) → MIN(x1, xs)
MIN(x'', cons(y', z)) → IF1(le(x'', y'), x'', y', z)
IF1(false_renamed, x2, y1, xs') → MIN(y1, xs')
le(0, y7) → true_renamed
le(s(x9), 0) → false_renamed
le(s(x10), s(y8)) → le(x10, y8)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
min(x0, cons(x1, x2))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, 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_renamed, x0, x1, x2)
if2(false_renamed, 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[a33](nil, nil)
equal_sort[a33](nil, cons(x0, x1))
equal_sort[a33](cons(x0, x1), nil)
equal_sort[a33](cons(x0, x1), cons(x2, x3))
equal_sort[a44](true_renamed, true_renamed)
equal_sort[a44](true_renamed, false_renamed)
equal_sort[a44](false_renamed, true_renamed)
equal_sort[a44](false_renamed, false_renamed)
equal_sort[a62](witness_sort[a62], witness_sort[a62])
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
min(x0, cons(x1, x2))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, 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_renamed, x0, x1, x2)
if2(false_renamed, 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[a33](nil, nil)
equal_sort[a33](nil, cons(x0, x1))
equal_sort[a33](cons(x0, x1), nil)
equal_sort[a33](cons(x0, x1), cons(x2, x3))
equal_sort[a44](true_renamed, true_renamed)
equal_sort[a44](true_renamed, false_renamed)
equal_sort[a44](false_renamed, true_renamed)
equal_sort[a44](false_renamed, false_renamed)
equal_sort[a62](witness_sort[a62], witness_sort[a62])
IF1(true_renamed, x1, y'', xs) → MIN(x1, xs)
MIN(x'', cons(y', z)) → IF1(le(x'', y'), x'', y', z)
IF1(false_renamed, x2, y1, xs') → MIN(y1, xs')
le(0, y7) → true_renamed
le(s(x9), 0) → false_renamed
le(s(x10), s(y8)) → le(x10, y8)
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_renamed, x7, y6, xs1) → DEL'(x7, xs1)
DEL'(x3, cons(y2, z')) → IF2'(eq(x3, y2), x3, y2, z')
del'(x3, cons(y2, z')) → if2'(eq(x3, y2), x3, y2, z')
if2'(true_renamed, x6, y5, xs'') → true
if2'(false_renamed, x7, y6, xs1) → del'(x7, xs1)
del'(x8, nil) → false
min(x', nil) → x'
min(x'', cons(y', z)) → if1(le(x'', y'), x'', y', z)
if1(true_renamed, x1, y'', xs) → min(x1, xs)
if1(false_renamed, x2, y1, xs') → min(y1, xs')
del(x3, cons(y2, z')) → if2(eq(x3, y2), x3, y2, z')
eq(0, 0) → true_renamed
eq(0, s(y3)) → false_renamed
eq(s(x4), 0) → false_renamed
eq(s(x5), s(y4)) → eq(x5, y4)
if2(true_renamed, x6, y5, xs'') → xs''
if2(false_renamed, x7, y6, xs1) → cons(y6, del(x7, xs1))
del(x8, nil) → nil
le(0, y7) → true_renamed
le(s(x9), 0) → false_renamed
le(s(x10), s(y8)) → le(x10, y8)
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(v25)) → false
equal_sort[a0](s(v26), 0) → false
equal_sort[a0](s(v26), s(v27)) → equal_sort[a0](v26, v27)
equal_sort[a33](nil, nil) → true
equal_sort[a33](nil, cons(v28, v29)) → false
equal_sort[a33](cons(v30, v31), nil) → false
equal_sort[a33](cons(v30, v31), cons(v32, v33)) → and(equal_sort[a0](v30, v32), equal_sort[a33](v31, v33))
equal_sort[a44](true_renamed, true_renamed) → true
equal_sort[a44](true_renamed, false_renamed) → false
equal_sort[a44](false_renamed, true_renamed) → false
equal_sort[a44](false_renamed, false_renamed) → true
equal_sort[a62](witness_sort[a62], witness_sort[a62]) → true
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
min(x0, cons(x1, x2))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, 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_renamed, x0, x1, x2)
if2(false_renamed, 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[a33](nil, nil)
equal_sort[a33](nil, cons(x0, x1))
equal_sort[a33](cons(x0, x1), nil)
equal_sort[a33](cons(x0, x1), cons(x2, x3))
equal_sort[a44](true_renamed, true_renamed)
equal_sort[a44](true_renamed, false_renamed)
equal_sort[a44](false_renamed, true_renamed)
equal_sort[a44](false_renamed, false_renamed)
equal_sort[a62](witness_sort[a62], witness_sort[a62])
IF2'(false_renamed, x7, y6, xs1) → DEL'(x7, xs1)
DEL'(x3, cons(y2, z')) → IF2'(eq(x3, y2), x3, y2, z')
eq(0, 0) → true_renamed
eq(0, s(y3)) → false_renamed
eq(s(x4), 0) → false_renamed
eq(s(x5), s(y4)) → eq(x5, y4)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
min(x0, cons(x1, x2))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, 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_renamed, x0, x1, x2)
if2(false_renamed, 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[a33](nil, nil)
equal_sort[a33](nil, cons(x0, x1))
equal_sort[a33](cons(x0, x1), nil)
equal_sort[a33](cons(x0, x1), cons(x2, x3))
equal_sort[a44](true_renamed, true_renamed)
equal_sort[a44](true_renamed, false_renamed)
equal_sort[a44](false_renamed, true_renamed)
equal_sort[a44](false_renamed, false_renamed)
equal_sort[a62](witness_sort[a62], witness_sort[a62])
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
min(x0, nil)
min(x0, cons(x1, x2))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, x0, x1, x2)
del(x0, cons(x1, x2))
if2(true_renamed, x0, x1, x2)
if2(false_renamed, 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[a33](nil, nil)
equal_sort[a33](nil, cons(x0, x1))
equal_sort[a33](cons(x0, x1), nil)
equal_sort[a33](cons(x0, x1), cons(x2, x3))
equal_sort[a44](true_renamed, true_renamed)
equal_sort[a44](true_renamed, false_renamed)
equal_sort[a44](false_renamed, true_renamed)
equal_sort[a44](false_renamed, false_renamed)
equal_sort[a62](witness_sort[a62], witness_sort[a62])
IF2'(false_renamed, x7, y6, xs1) → DEL'(x7, xs1)
DEL'(x3, cons(y2, z')) → IF2'(eq(x3, y2), x3, y2, z')
eq(0, 0) → true_renamed
eq(0, s(y3)) → false_renamed
eq(s(x4), 0) → false_renamed
eq(s(x5), s(y4)) → eq(x5, y4)
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: