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