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 QDPOrderProof (⇔, 0 ms)
↳41 QDP
↳42 PisEmptyProof (⇔, 0 ms)
↳43 YES
↳44 QDP
↳45 UsableRulesProof (⇔, 0 ms)
↳46 QDP
↳47 QReductionProof (⇔, 0 ms)
↳48 QDP
↳49 Induction-Processor (⇒, 44 ms)
↳50 AND
↳51 QDP
↳52 PisEmptyProof (⇔, 0 ms)
↳53 YES
↳54 QTRS
↳55 Overlay + Local Confluence (⇔, 0 ms)
↳56 QTRS
↳57 DependencyPairsProof (⇔, 0 ms)
↳58 QDP
↳59 DependencyGraphProof (⇔, 0 ms)
↳60 AND
↳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 QDPSizeChangeProof (⇔, 0 ms)
↳95 YES
↳96 QDP
↳97 UsableRulesProof (⇔, 0 ms)
↳98 QDP
↳99 QReductionProof (⇔, 0 ms)
↳100 QDP
↳101 QDPSizeChangeProof (⇔, 0 ms)
↳102 YES
↳103 QDP
↳104 UsableRulesProof (⇔, 0 ms)
↳105 QDP
↳106 QReductionProof (⇔, 0 ms)
↳107 QDP
↳108 QDPOrderProof (⇔, 0 ms)
↳109 QDP
↳110 PisEmptyProof (⇔, 0 ms)
↳111 YES
↳112 QDP
↳113 UsableRulesProof (⇔, 0 ms)
↳114 QDP
↳115 QReductionProof (⇔, 0 ms)
↳116 QDP
↳117 QDPSizeChangeProof (⇔, 0 ms)
↳118 YES
max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, 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)
sort(nil) → nil
sort(cons(x, xs)) → cons(max(cons(x, xs)), sort(h(del(max(cons(x, xs)), cons(x, xs)))))
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))
max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, 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)
sort(nil) → nil
sort(cons(x, xs)) → cons(max(cons(x, xs)), sort(h(del(max(cons(x, xs)), cons(x, xs)))))
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(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))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))
MAX(cons(x, cons(y, xs))) → IF1(ge(x, y), x, y, xs)
MAX(cons(x, cons(y, xs))) → GE(x, y)
IF1(true, x, y, xs) → MAX(cons(x, xs))
IF1(false, x, y, xs) → MAX(cons(y, xs))
DEL(x, cons(y, xs)) → IF2(eq(x, y), x, y, xs)
DEL(x, cons(y, xs)) → EQ(x, y)
IF2(false, x, y, xs) → DEL(x, xs)
EQ(s(x), s(y)) → EQ(x, y)
SORT(cons(x, xs)) → MAX(cons(x, xs))
SORT(cons(x, xs)) → SORT(h(del(max(cons(x, xs)), cons(x, xs))))
SORT(cons(x, xs)) → H(del(max(cons(x, xs)), cons(x, xs)))
SORT(cons(x, xs)) → DEL(max(cons(x, xs)), cons(x, xs))
GE(s(x), s(y)) → GE(x, y)
H(cons(x, xs)) → H(xs)
max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, 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)
sort(nil) → nil
sort(cons(x, xs)) → cons(max(cons(x, xs)), sort(h(del(max(cons(x, xs)), cons(x, xs)))))
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(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))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))
H(cons(x, xs)) → H(xs)
max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, 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)
sort(nil) → nil
sort(cons(x, xs)) → cons(max(cons(x, xs)), sort(h(del(max(cons(x, xs)), cons(x, xs)))))
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(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))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))
H(cons(x, xs)) → H(xs)
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(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))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(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))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))
H(cons(x, xs)) → H(xs)
From the DPs we obtained the following set of size-change graphs:
GE(s(x), s(y)) → GE(x, y)
max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, 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)
sort(nil) → nil
sort(cons(x, xs)) → cons(max(cons(x, xs)), sort(h(del(max(cons(x, xs)), cons(x, xs)))))
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(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))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))
GE(s(x), s(y)) → GE(x, y)
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(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))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(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))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))
GE(s(x), s(y)) → GE(x, y)
From the DPs we obtained the following set of size-change graphs:
EQ(s(x), s(y)) → EQ(x, y)
max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, 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)
sort(nil) → nil
sort(cons(x, xs)) → cons(max(cons(x, xs)), sort(h(del(max(cons(x, xs)), cons(x, xs)))))
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(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))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))
EQ(s(x), s(y)) → EQ(x, y)
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(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))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(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))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))
EQ(s(x), s(y)) → EQ(x, y)
From the DPs we obtained the following set of size-change graphs:
IF2(false, x, y, xs) → DEL(x, xs)
DEL(x, cons(y, xs)) → IF2(eq(x, y), x, y, xs)
max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, 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)
sort(nil) → nil
sort(cons(x, xs)) → cons(max(cons(x, xs)), sort(h(del(max(cons(x, xs)), cons(x, xs)))))
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(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))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))
IF2(false, x, y, xs) → DEL(x, xs)
DEL(x, cons(y, xs)) → IF2(eq(x, y), x, y, xs)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(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))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))
IF2(false, x, y, xs) → DEL(x, xs)
DEL(x, cons(y, xs)) → IF2(eq(x, y), x, y, 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:
IF1(true, x, y, xs) → MAX(cons(x, xs))
MAX(cons(x, cons(y, xs))) → IF1(ge(x, y), x, y, xs)
IF1(false, x, y, xs) → MAX(cons(y, xs))
max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, 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)
sort(nil) → nil
sort(cons(x, xs)) → cons(max(cons(x, xs)), sort(h(del(max(cons(x, xs)), cons(x, xs)))))
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(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))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))
IF1(true, x, y, xs) → MAX(cons(x, xs))
MAX(cons(x, cons(y, xs))) → IF1(ge(x, y), x, y, xs)
IF1(false, x, y, xs) → MAX(cons(y, xs))
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(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))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(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))
sort(nil)
sort(cons(x0, x1))
h(nil)
h(cons(x0, x1))
IF1(true, x, y, xs) → MAX(cons(x, xs))
MAX(cons(x, cons(y, xs))) → IF1(ge(x, y), x, y, xs)
IF1(false, x, y, xs) → MAX(cons(y, xs))
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(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, x, y, xs) → MAX(cons(x, xs))
MAX(cons(x, cons(y, xs))) → IF1(ge(x, y), x, y, xs)
IF1(false, x, y, xs) → MAX(cons(y, xs))
trivial
dummyConstant=1
IF1_1=3
cons_1=2
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
SORT(cons(x, xs)) → SORT(h(del(max(cons(x, xs)), cons(x, xs))))
max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, 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)
sort(nil) → nil
sort(cons(x, xs)) → cons(max(cons(x, xs)), sort(h(del(max(cons(x, xs)), cons(x, xs)))))
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(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))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))
SORT(cons(x, xs)) → SORT(h(del(max(cons(x, xs)), cons(x, xs))))
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))
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
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(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))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))
sort(nil)
sort(cons(x0, x1))
SORT(cons(x, xs)) → SORT(h(del(max(cons(x, xs)), cons(x, xs))))
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))
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
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(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))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))
POL(0) = 0
POL(SORT(x1)) = 3·x1
POL(cons(x1, x2)) = 1 + x1 + x2
POL(del(x1, x2)) = x2
POL(eq(x1, x2)) = 0
POL(false_renamed) = 0
POL(ge(x1, x2)) = 0
POL(h(x1)) = x1
POL(if1(x1, x2, x3, x4)) = 3 + x1 + 2·x2 + 2·x3 + 2·x4
POL(if2(x1, x2, x3, x4)) = 1 + 3·x1 + x3 + x4
POL(max(x1)) = 2·x1
POL(nil) = 0
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, v30, v31, v32, v33, v34, v35, v36, v37, v38, x7, y4, xs4, x8, y5, y1, xs2, x9, x3, x', x'', y, xs', x4, xs3, y2, x5, x6, y3, x10, x11, x12, y6, 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(v30)) -> false equal_sort[a0](s(v31), 0) -> false equal_sort[a0](s(v31), s(v32)) -> equal_sort[a0](v31, v32) equal_sort[a37](cons(v33, v34), cons(v35, v36)) -> equal_sort[a0](v33, v35) and equal_sort[a37](v34, v36) equal_sort[a37](cons(v33, v34), nil) -> false equal_sort[a37](nil, cons(v37, v38)) -> false equal_sort[a37](nil, nil) -> true equal_sort[a45](true_renamed, true_renamed) -> true equal_sort[a45](true_renamed, false_renamed) -> false equal_sort[a45](false_renamed, true_renamed) -> false equal_sort[a45](false_renamed, false_renamed) -> true equal_sort[a65](witness_sort[a65], witness_sort[a65]) -> true if2'(true_renamed, x7, y4, xs4) -> true if2'(false_renamed, x8, y5, cons(y1, xs2)) -> if2'(eq(x8, y1), x8, y1, xs2) if2'(false_renamed, x8, y5, nil) -> false del'(x9, nil) -> false equal_sort[a45](eq(x3, y1), true_renamed) -> true | del'(x3, cons(y1, xs2)) -> true equal_sort[a45](eq(x3, y1), true_renamed) -> false | del'(x3, cons(y1, xs2)) -> del'(x3, xs2) max(cons(x', nil)) -> x' max(nil) -> 0 equal_sort[a45](ge(x'', y), true_renamed) -> true | max(cons(x'', cons(y, xs'))) -> max(cons(x'', xs')) equal_sort[a45](ge(x'', y), true_renamed) -> false | max(cons(x'', cons(y, xs'))) -> max(cons(y, xs')) h(nil) -> nil h(cons(x4, xs3)) -> cons(x4, h(xs3)) eq(0, 0) -> true_renamed eq(0, s(y2)) -> false_renamed eq(s(x5), 0) -> false_renamed eq(s(x6), s(y3)) -> eq(x6, y3) if2(true_renamed, x7, y4, xs4) -> xs4 if2(false_renamed, x8, y5, cons(y1, xs2)) -> cons(y5, if2(eq(x8, y1), x8, y1, xs2)) if2(false_renamed, x8, y5, nil) -> cons(y5, nil) del(x9, nil) -> nil equal_sort[a45](eq(x3, y1), true_renamed) -> true | del(x3, cons(y1, xs2)) -> xs2 equal_sort[a45](eq(x3, y1), true_renamed) -> false | del(x3, cons(y1, xs2)) -> cons(y1, del(x3, xs2)) ge(0, 0) -> true_renamed ge(s(x10), 0) -> true_renamed ge(0, s(x11)) -> false_renamed ge(s(x12), s(y6)) -> ge(x12, y6) if1(true_renamed, x1, y', nil) -> x1 if1(true_renamed, x1, y', cons(y, xs')) -> if1(ge(x1, y), x1, y, xs') if1(false_renamed, x2, y'', nil) -> y'' if1(false_renamed, x2, y'', cons(y, xs')) -> if1(ge(y'', y), y'', y, xs') if1(true_renamed, x1, y', xs'') -> 0 if1(false_renamed, x2, y'', xs1) -> 0 using the following formula: z0:sort[a37].(~(z0=nil)->del'(max(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[a37].(~(z0=nil)->del'(max(z0), z0)=true) There are no hypotheses. ---------------------------------------- (1) Induction by algorithm (EQUIVALENT) Induction by algorithm max(z0) generates the following cases: 1. Base Case: Formula: x':sort[a0].(~(cons(x', nil)=nil)->del'(max(cons(x', nil)), cons(x', nil))=true) There are no hypotheses. 2. Base Case: Formula: (~(nil=nil)->del'(max(nil), nil)=true) There are no hypotheses. 1. Step Case: Formula: x'':sort[a0],y:sort[a0],xs':sort[a37].(~(cons(x'', cons(y, xs'))=nil)->del'(max(cons(x'', cons(y, xs'))), cons(x'', cons(y, xs')))=true) Hypotheses: x'':sort[a0],xs':sort[a37].del'(max(cons(x'', xs')), cons(x'', xs'))=true x'':sort[a0],y:sort[a0].equal_sort[a45](ge(x'', y), true_renamed)=true 2. Step Case: Formula: x'':sort[a0],y:sort[a0],xs':sort[a37].(~(cons(x'', cons(y, xs'))=nil)->del'(max(cons(x'', cons(y, xs'))), cons(x'', cons(y, xs')))=true) Hypotheses: y:sort[a0],xs':sort[a37].del'(max(cons(y, xs')), cons(y, xs'))=true x'':sort[a0],y:sort[a0].equal_sort[a45](ge(x'', y), true_renamed)=false ---------------------------------------- (2) Complex Obligation (AND) ---------------------------------------- (3) Obligation: Formula: x':sort[a0].(~(cons(x', nil)=nil)->del'(max(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].del'(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: del'(0, cons(0, nil))=true There are no hypotheses. 1. Step Case: Formula: n:sort[a0].del'(s(n), cons(s(n), nil))=true Hypotheses: n:sort[a0].del'(n, cons(n, nil))=true ---------------------------------------- (7) Complex Obligation (AND) ---------------------------------------- (8) Obligation: Formula: del'(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].del'(s(n), cons(s(n), nil))=true Hypotheses: n:sort[a0].del'(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].del'(n, cons(n, nil))=true n:sort[a0].equal_sort[a45](eq(s(n), s(n)), true_renamed)=true Formula: n:sort[a0].del'(s(n), nil)=true Hypotheses: n:sort[a0].del'(n, cons(n, nil))=true n:sort[a0].equal_sort[a45](eq(s(n), s(n)), true_renamed)=false ---------------------------------------- (13) Complex Obligation (AND) ---------------------------------------- (14) Obligation: Formula: true=true Hypotheses: n:sort[a0].del'(n, cons(n, nil))=true n:sort[a0].equal_sort[a45](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].del'(s(n), nil)=true Hypotheses: n:sort[a0].del'(n, cons(n, nil))=true n:sort[a0].equal_sort[a45](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].del'(n, cons(n, nil))=true n:sort[a0].equal_sort[a45](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].((del'(n, cons(n, nil))=true/\equal_sort[a45](eq(s(n), s(n)), true_renamed)=false)->False) Hypotheses: n:sort[a0].del'(n, cons(n, nil))=true n:sort[a0].equal_sort[a45](eq(s(n), s(n)), true_renamed)=false ---------------------------------------- (21) Obligation: Formula: n:sort[a0].((del'(n, cons(n, nil))=true/\equal_sort[a45](eq(s(n), s(n)), true_renamed)=false)->False) Hypotheses: n:sort[a0].del'(n, cons(n, nil))=true n:sort[a0].equal_sort[a45](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[a45](eq(n, n), true_renamed)=false) By using the following hypotheses: n:sort[a0].del'(n, cons(n, nil))=true ---------------------------------------- (23) Obligation: Formula: n:sort[a0].~(equal_sort[a45](eq(n, n), true_renamed)=false) Hypotheses: n:sort[a0].del'(n, cons(n, nil))=true n:sort[a0].equal_sort[a45](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[a45](eq(n, n), true_renamed)=false->~(equal_sort[a45](eq(n, n), true_renamed)=false)) Hypotheses: n:sort[a0].del'(n, cons(n, nil))=true ---------------------------------------- (25) Obligation: Formula: n:sort[a0].(equal_sort[a45](eq(n, n), true_renamed)=false->~(equal_sort[a45](eq(n, n), true_renamed)=false)) Hypotheses: n:sort[a0].del'(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].(del'(n, cons(n, nil))=true->(equal_sort[a45](eq(n, n), true_renamed)=false->~(equal_sort[a45](eq(n, n), true_renamed)=false))) There are no hypotheses. ---------------------------------------- (27) Obligation: Formula: n:sort[a0].(del'(n, cons(n, nil))=true->(equal_sort[a45](eq(n, n), true_renamed)=false->~(equal_sort[a45](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[a45](eq(n, n), true_renamed)=false->~(equal_sort[a45](eq(n, n), true_renamed)=false))) Hypotheses: n:sort[a0].equal_sort[a45](eq(n, n), true_renamed)=true Formula: n:sort[a0].(del'(n, nil)=true->(equal_sort[a45](eq(n, n), true_renamed)=false->~(equal_sort[a45](eq(n, n), true_renamed)=false))) Hypotheses: n:sort[a0].equal_sort[a45](eq(n, n), true_renamed)=false ---------------------------------------- (29) Complex Obligation (AND) ---------------------------------------- (30) Obligation: Formula: n:sort[a0].(true=true->(equal_sort[a45](eq(n, n), true_renamed)=false->~(equal_sort[a45](eq(n, n), true_renamed)=false))) Hypotheses: n:sort[a0].equal_sort[a45](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[a45](eq(n, n), true_renamed)=true ---------------------------------------- (32) YES ---------------------------------------- (33) Obligation: Formula: n:sort[a0].(del'(n, nil)=true->(equal_sort[a45](eq(n, n), true_renamed)=false->~(equal_sort[a45](eq(n, n), true_renamed)=false))) Hypotheses: n:sort[a0].equal_sort[a45](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)->del'(max(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[a37].(~(cons(x'', cons(y, xs'))=nil)->del'(max(cons(x'', cons(y, xs'))), cons(x'', cons(y, xs')))=true) Hypotheses: x'':sort[a0],xs':sort[a37].del'(max(cons(x'', xs')), cons(x'', xs'))=true x'':sort[a0],y:sort[a0].equal_sort[a45](ge(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[a37].del'(max(cons(x'', cons(y, xs'))), cons(x'', cons(y, xs')))=true Hypotheses: x'':sort[a0],xs':sort[a37].del'(max(cons(x'', xs')), cons(x'', xs'))=true x'':sort[a0],y:sort[a0].equal_sort[a45](ge(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[a37],y:sort[a0].del'(max(cons(x'', xs')), cons(x'', cons(y, xs')))=true Hypotheses: x'':sort[a0],xs':sort[a37].del'(max(cons(x'', xs')), cons(x'', xs'))=true x'':sort[a0],y:sort[a0].equal_sort[a45](ge(x'', y), true_renamed)=true ---------------------------------------- (43) Obligation: Formula: x'':sort[a0],xs':sort[a37],y:sort[a0].del'(max(cons(x'', xs')), cons(x'', cons(y, xs')))=true Hypotheses: x'':sort[a0],xs':sort[a37].del'(max(cons(x'', xs')), cons(x'', xs'))=true x'':sort[a0],y:sort[a0].equal_sort[a45](ge(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[a37].del'(max(cons(x'', xs')), cons(x'', xs'))=true x'':sort[a0],y:sort[a0].equal_sort[a45](ge(x'', y), true_renamed)=true x'':sort[a0],xs':sort[a37].equal_sort[a45](eq(max(cons(x'', xs')), x''), true_renamed)=true Formula: x'':sort[a0],xs':sort[a37],y:sort[a0].del'(max(cons(x'', xs')), cons(y, xs'))=true Hypotheses: x'':sort[a0],xs':sort[a37].del'(max(cons(x'', xs')), cons(x'', xs'))=true x'':sort[a0],y:sort[a0].equal_sort[a45](ge(x'', y), true_renamed)=true x'':sort[a0],xs':sort[a37].equal_sort[a45](eq(max(cons(x'', xs')), x''), true_renamed)=false ---------------------------------------- (45) Complex Obligation (AND) ---------------------------------------- (46) Obligation: Formula: true=true Hypotheses: x'':sort[a0],xs':sort[a37].del'(max(cons(x'', xs')), cons(x'', xs'))=true x'':sort[a0],y:sort[a0].equal_sort[a45](ge(x'', y), true_renamed)=true x'':sort[a0],xs':sort[a37].equal_sort[a45](eq(max(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[a37],y:sort[a0].del'(max(cons(x'', xs')), cons(y, xs'))=true Hypotheses: x'':sort[a0],xs':sort[a37].del'(max(cons(x'', xs')), cons(x'', xs'))=true x'':sort[a0],y:sort[a0].equal_sort[a45](ge(x'', y), true_renamed)=true x'':sort[a0],xs':sort[a37].equal_sort[a45](eq(max(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[a37].del'(max(cons(x'', xs')), cons(x'', xs'))=true x'':sort[a0],y:sort[a0].equal_sort[a45](ge(x'', y), true_renamed)=true x'':sort[a0],xs':sort[a37].equal_sort[a45](eq(max(cons(x'', xs')), x''), true_renamed)=false x'':sort[a0],xs':sort[a37],y:sort[a0].equal_sort[a45](eq(max(cons(x'', xs')), y), true_renamed)=true Formula: x'':sort[a0],xs':sort[a37].del'(max(cons(x'', xs')), xs')=true Hypotheses: x'':sort[a0],xs':sort[a37].del'(max(cons(x'', xs')), cons(x'', xs'))=true x'':sort[a0],y:sort[a0].equal_sort[a45](ge(x'', y), true_renamed)=true x'':sort[a0],xs':sort[a37].equal_sort[a45](eq(max(cons(x'', xs')), x''), true_renamed)=false x'':sort[a0],xs':sort[a37],y:sort[a0].equal_sort[a45](eq(max(cons(x'', xs')), y), true_renamed)=false ---------------------------------------- (51) Complex Obligation (AND) ---------------------------------------- (52) Obligation: Formula: true=true Hypotheses: x'':sort[a0],xs':sort[a37].del'(max(cons(x'', xs')), cons(x'', xs'))=true x'':sort[a0],y:sort[a0].equal_sort[a45](ge(x'', y), true_renamed)=true x'':sort[a0],xs':sort[a37].equal_sort[a45](eq(max(cons(x'', xs')), x''), true_renamed)=false x'':sort[a0],xs':sort[a37],y:sort[a0].equal_sort[a45](eq(max(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[a37].del'(max(cons(x'', xs')), xs')=true Hypotheses: x'':sort[a0],xs':sort[a37].del'(max(cons(x'', xs')), cons(x'', xs'))=true x'':sort[a0],y:sort[a0].equal_sort[a45](ge(x'', y), true_renamed)=true x'':sort[a0],xs':sort[a37].equal_sort[a45](eq(max(cons(x'', xs')), x''), true_renamed)=false x'':sort[a0],xs':sort[a37],y:sort[a0].equal_sort[a45](eq(max(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[a37].(del'(max(cons(x'', xs')), cons(x'', xs'))=true->del'(max(cons(x'', xs')), xs')=true) Hypotheses: x'':sort[a0],y:sort[a0].equal_sort[a45](ge(x'', y), true_renamed)=true x'':sort[a0],xs':sort[a37].equal_sort[a45](eq(max(cons(x'', xs')), x''), true_renamed)=false x'':sort[a0],xs':sort[a37],y:sort[a0].equal_sort[a45](eq(max(cons(x'', xs')), y), true_renamed)=false ---------------------------------------- (57) Obligation: Formula: x'':sort[a0],xs':sort[a37].(del'(max(cons(x'', xs')), cons(x'', xs'))=true->del'(max(cons(x'', xs')), xs')=true) Hypotheses: x'':sort[a0],y:sort[a0].equal_sort[a45](ge(x'', y), true_renamed)=true x'':sort[a0],xs':sort[a37].equal_sort[a45](eq(max(cons(x'', xs')), x''), true_renamed)=false x'':sort[a0],xs':sort[a37],y:sort[a0].equal_sort[a45](eq(max(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[a37].(del'(max(cons(x'', xs')), xs')=true->del'(max(cons(x'', xs')), xs')=true) Hypotheses: x'':sort[a0],y:sort[a0].equal_sort[a45](ge(x'', y), true_renamed)=true x'':sort[a0],xs':sort[a37].equal_sort[a45](eq(max(cons(x'', xs')), x''), true_renamed)=false x'':sort[a0],xs':sort[a37],y:sort[a0].equal_sort[a45](eq(max(cons(x'', xs')), y), true_renamed)=false ---------------------------------------- (59) Obligation: Formula: x'':sort[a0],xs':sort[a37].(del'(max(cons(x'', xs')), xs')=true->del'(max(cons(x'', xs')), xs')=true) Hypotheses: x'':sort[a0],y:sort[a0].equal_sort[a45](ge(x'', y), true_renamed)=true x'':sort[a0],xs':sort[a37].equal_sort[a45](eq(max(cons(x'', xs')), x''), true_renamed)=false x'':sort[a0],xs':sort[a37],y:sort[a0].equal_sort[a45](eq(max(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[a37].(~(cons(x'', cons(y, xs'))=nil)->del'(max(cons(x'', cons(y, xs'))), cons(x'', cons(y, xs')))=true) Hypotheses: y:sort[a0],xs':sort[a37].del'(max(cons(y, xs')), cons(y, xs'))=true x'':sort[a0],y:sort[a0].equal_sort[a45](ge(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[a37].del'(max(cons(x'', cons(y, xs'))), cons(x'', cons(y, xs')))=true Hypotheses: y:sort[a0],xs':sort[a37].del'(max(cons(y, xs')), cons(y, xs'))=true x'':sort[a0],y:sort[a0].equal_sort[a45](ge(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[a37],x'':sort[a0].del'(max(cons(y, xs')), cons(x'', cons(y, xs')))=true Hypotheses: y:sort[a0],xs':sort[a37].del'(max(cons(y, xs')), cons(y, xs'))=true x'':sort[a0],y:sort[a0].equal_sort[a45](ge(x'', y), true_renamed)=false ---------------------------------------- (66) Obligation: Formula: y:sort[a0],xs':sort[a37],x'':sort[a0].del'(max(cons(y, xs')), cons(x'', cons(y, xs')))=true Hypotheses: y:sort[a0],xs':sort[a37].del'(max(cons(y, xs')), cons(y, xs'))=true x'':sort[a0],y:sort[a0].equal_sort[a45](ge(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[a37].del'(max(cons(y, xs')), cons(y, xs'))=true x'':sort[a0],y:sort[a0].equal_sort[a45](ge(x'', y), true_renamed)=false y:sort[a0],xs':sort[a37],x'':sort[a0].equal_sort[a45](eq(max(cons(y, xs')), x''), true_renamed)=true Formula: y:sort[a0],xs':sort[a37].del'(max(cons(y, xs')), cons(y, xs'))=true Hypotheses: y:sort[a0],xs':sort[a37].del'(max(cons(y, xs')), cons(y, xs'))=true x'':sort[a0],y:sort[a0].equal_sort[a45](ge(x'', y), true_renamed)=false y:sort[a0],xs':sort[a37],x'':sort[a0].equal_sort[a45](eq(max(cons(y, xs')), x''), true_renamed)=false ---------------------------------------- (68) Complex Obligation (AND) ---------------------------------------- (69) Obligation: Formula: true=true Hypotheses: y:sort[a0],xs':sort[a37].del'(max(cons(y, xs')), cons(y, xs'))=true x'':sort[a0],y:sort[a0].equal_sort[a45](ge(x'', y), true_renamed)=false y:sort[a0],xs':sort[a37],x'':sort[a0].equal_sort[a45](eq(max(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[a37].del'(max(cons(y, xs')), cons(y, xs'))=true Hypotheses: y:sort[a0],xs':sort[a37].del'(max(cons(y, xs')), cons(y, xs'))=true x'':sort[a0],y:sort[a0].equal_sort[a45](ge(x'', y), true_renamed)=false y:sort[a0],xs':sort[a37],x'':sort[a0].equal_sort[a45](eq(max(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[a37].del'(max(cons(y, xs')), cons(y, xs'))=true ---------------------------------------- (74) YES
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))
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
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(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))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))
del'(x3, cons(y1, xs2)) → if2'(eq(x3, y1), x3, y1, xs2)
if2'(true_renamed, x7, y4, xs4) → true
if2'(false_renamed, x8, y5, xs5) → del'(x8, xs5)
del'(x9, nil) → false
max(cons(x', nil)) → x'
max(cons(x'', cons(y, xs'))) → if1(ge(x'', y), x'', y, xs')
if1(true_renamed, x1, y', xs'') → max(cons(x1, xs''))
if1(false_renamed, x2, y'', xs1) → max(cons(y'', xs1))
del(x3, cons(y1, xs2)) → if2(eq(x3, y1), x3, y1, xs2)
h(nil) → nil
h(cons(x4, xs3)) → cons(x4, h(xs3))
eq(0, 0) → true_renamed
eq(0, s(y2)) → false_renamed
eq(s(x5), 0) → false_renamed
eq(s(x6), s(y3)) → eq(x6, y3)
if2(true_renamed, x7, y4, xs4) → xs4
if2(false_renamed, x8, y5, xs5) → cons(y5, del(x8, xs5))
del(x9, nil) → nil
ge(0, 0) → true_renamed
ge(s(x10), 0) → true_renamed
ge(0, s(x11)) → false_renamed
ge(s(x12), s(y6)) → ge(x12, y6)
max(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(v30)) → false
equal_sort[a0](s(v31), 0) → false
equal_sort[a0](s(v31), s(v32)) → equal_sort[a0](v31, v32)
equal_sort[a37](cons(v33, v34), cons(v35, v36)) → and(equal_sort[a0](v33, v35), equal_sort[a37](v34, v36))
equal_sort[a37](cons(v33, v34), nil) → false
equal_sort[a37](nil, cons(v37, v38)) → false
equal_sort[a37](nil, nil) → true
equal_sort[a45](true_renamed, true_renamed) → true
equal_sort[a45](true_renamed, false_renamed) → false
equal_sort[a45](false_renamed, true_renamed) → false
equal_sort[a45](false_renamed, false_renamed) → true
equal_sort[a65](witness_sort[a65], witness_sort[a65]) → true
del'(x3, cons(y1, xs2)) → if2'(eq(x3, y1), x3, y1, xs2)
if2'(true_renamed, x7, y4, xs4) → true
if2'(false_renamed, x8, y5, xs5) → del'(x8, xs5)
del'(x9, nil) → false
max(cons(x', nil)) → x'
max(cons(x'', cons(y, xs'))) → if1(ge(x'', y), x'', y, xs')
if1(true_renamed, x1, y', xs'') → max(cons(x1, xs''))
if1(false_renamed, x2, y'', xs1) → max(cons(y'', xs1))
del(x3, cons(y1, xs2)) → if2(eq(x3, y1), x3, y1, xs2)
h(nil) → nil
h(cons(x4, xs3)) → cons(x4, h(xs3))
eq(0, 0) → true_renamed
eq(0, s(y2)) → false_renamed
eq(s(x5), 0) → false_renamed
eq(s(x6), s(y3)) → eq(x6, y3)
if2(true_renamed, x7, y4, xs4) → xs4
if2(false_renamed, x8, y5, xs5) → cons(y5, del(x8, xs5))
del(x9, nil) → nil
ge(0, 0) → true_renamed
ge(s(x10), 0) → true_renamed
ge(0, s(x11)) → false_renamed
ge(s(x12), s(y6)) → ge(x12, y6)
max(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(v30)) → false
equal_sort[a0](s(v31), 0) → false
equal_sort[a0](s(v31), s(v32)) → equal_sort[a0](v31, v32)
equal_sort[a37](cons(v33, v34), cons(v35, v36)) → and(equal_sort[a0](v33, v35), equal_sort[a37](v34, v36))
equal_sort[a37](cons(v33, v34), nil) → false
equal_sort[a37](nil, cons(v37, v38)) → false
equal_sort[a37](nil, nil) → true
equal_sort[a45](true_renamed, true_renamed) → true
equal_sort[a45](true_renamed, false_renamed) → false
equal_sort[a45](false_renamed, true_renamed) → false
equal_sort[a45](false_renamed, false_renamed) → true
equal_sort[a65](witness_sort[a65], witness_sort[a65]) → true
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
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)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(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[a37](cons(x0, x1), cons(x2, x3))
equal_sort[a37](cons(x0, x1), nil)
equal_sort[a37](nil, cons(x0, x1))
equal_sort[a37](nil, nil)
equal_sort[a45](true_renamed, true_renamed)
equal_sort[a45](true_renamed, false_renamed)
equal_sort[a45](false_renamed, true_renamed)
equal_sort[a45](false_renamed, false_renamed)
equal_sort[a65](witness_sort[a65], witness_sort[a65])
DEL'(x3, cons(y1, xs2)) → IF2'(eq(x3, y1), x3, y1, xs2)
DEL'(x3, cons(y1, xs2)) → EQ(x3, y1)
IF2'(false_renamed, x8, y5, xs5) → DEL'(x8, xs5)
MAX(cons(x'', cons(y, xs'))) → IF1(ge(x'', y), x'', y, xs')
MAX(cons(x'', cons(y, xs'))) → GE(x'', y)
IF1(true_renamed, x1, y', xs'') → MAX(cons(x1, xs''))
IF1(false_renamed, x2, y'', xs1) → MAX(cons(y'', xs1))
DEL(x3, cons(y1, xs2)) → IF2(eq(x3, y1), x3, y1, xs2)
DEL(x3, cons(y1, xs2)) → EQ(x3, y1)
H(cons(x4, xs3)) → H(xs3)
EQ(s(x6), s(y3)) → EQ(x6, y3)
IF2(false_renamed, x8, y5, xs5) → DEL(x8, xs5)
GE(s(x12), s(y6)) → GE(x12, y6)
EQUAL_SORT[A0](s(v31), s(v32)) → EQUAL_SORT[A0](v31, v32)
EQUAL_SORT[A37](cons(v33, v34), cons(v35, v36)) → AND(equal_sort[a0](v33, v35), equal_sort[a37](v34, v36))
EQUAL_SORT[A37](cons(v33, v34), cons(v35, v36)) → EQUAL_SORT[A0](v33, v35)
EQUAL_SORT[A37](cons(v33, v34), cons(v35, v36)) → EQUAL_SORT[A37](v34, v36)
del'(x3, cons(y1, xs2)) → if2'(eq(x3, y1), x3, y1, xs2)
if2'(true_renamed, x7, y4, xs4) → true
if2'(false_renamed, x8, y5, xs5) → del'(x8, xs5)
del'(x9, nil) → false
max(cons(x', nil)) → x'
max(cons(x'', cons(y, xs'))) → if1(ge(x'', y), x'', y, xs')
if1(true_renamed, x1, y', xs'') → max(cons(x1, xs''))
if1(false_renamed, x2, y'', xs1) → max(cons(y'', xs1))
del(x3, cons(y1, xs2)) → if2(eq(x3, y1), x3, y1, xs2)
h(nil) → nil
h(cons(x4, xs3)) → cons(x4, h(xs3))
eq(0, 0) → true_renamed
eq(0, s(y2)) → false_renamed
eq(s(x5), 0) → false_renamed
eq(s(x6), s(y3)) → eq(x6, y3)
if2(true_renamed, x7, y4, xs4) → xs4
if2(false_renamed, x8, y5, xs5) → cons(y5, del(x8, xs5))
del(x9, nil) → nil
ge(0, 0) → true_renamed
ge(s(x10), 0) → true_renamed
ge(0, s(x11)) → false_renamed
ge(s(x12), s(y6)) → ge(x12, y6)
max(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(v30)) → false
equal_sort[a0](s(v31), 0) → false
equal_sort[a0](s(v31), s(v32)) → equal_sort[a0](v31, v32)
equal_sort[a37](cons(v33, v34), cons(v35, v36)) → and(equal_sort[a0](v33, v35), equal_sort[a37](v34, v36))
equal_sort[a37](cons(v33, v34), nil) → false
equal_sort[a37](nil, cons(v37, v38)) → false
equal_sort[a37](nil, nil) → true
equal_sort[a45](true_renamed, true_renamed) → true
equal_sort[a45](true_renamed, false_renamed) → false
equal_sort[a45](false_renamed, true_renamed) → false
equal_sort[a45](false_renamed, false_renamed) → true
equal_sort[a65](witness_sort[a65], witness_sort[a65]) → true
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
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)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(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[a37](cons(x0, x1), cons(x2, x3))
equal_sort[a37](cons(x0, x1), nil)
equal_sort[a37](nil, cons(x0, x1))
equal_sort[a37](nil, nil)
equal_sort[a45](true_renamed, true_renamed)
equal_sort[a45](true_renamed, false_renamed)
equal_sort[a45](false_renamed, true_renamed)
equal_sort[a45](false_renamed, false_renamed)
equal_sort[a65](witness_sort[a65], witness_sort[a65])
EQUAL_SORT[A0](s(v31), s(v32)) → EQUAL_SORT[A0](v31, v32)
del'(x3, cons(y1, xs2)) → if2'(eq(x3, y1), x3, y1, xs2)
if2'(true_renamed, x7, y4, xs4) → true
if2'(false_renamed, x8, y5, xs5) → del'(x8, xs5)
del'(x9, nil) → false
max(cons(x', nil)) → x'
max(cons(x'', cons(y, xs'))) → if1(ge(x'', y), x'', y, xs')
if1(true_renamed, x1, y', xs'') → max(cons(x1, xs''))
if1(false_renamed, x2, y'', xs1) → max(cons(y'', xs1))
del(x3, cons(y1, xs2)) → if2(eq(x3, y1), x3, y1, xs2)
h(nil) → nil
h(cons(x4, xs3)) → cons(x4, h(xs3))
eq(0, 0) → true_renamed
eq(0, s(y2)) → false_renamed
eq(s(x5), 0) → false_renamed
eq(s(x6), s(y3)) → eq(x6, y3)
if2(true_renamed, x7, y4, xs4) → xs4
if2(false_renamed, x8, y5, xs5) → cons(y5, del(x8, xs5))
del(x9, nil) → nil
ge(0, 0) → true_renamed
ge(s(x10), 0) → true_renamed
ge(0, s(x11)) → false_renamed
ge(s(x12), s(y6)) → ge(x12, y6)
max(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(v30)) → false
equal_sort[a0](s(v31), 0) → false
equal_sort[a0](s(v31), s(v32)) → equal_sort[a0](v31, v32)
equal_sort[a37](cons(v33, v34), cons(v35, v36)) → and(equal_sort[a0](v33, v35), equal_sort[a37](v34, v36))
equal_sort[a37](cons(v33, v34), nil) → false
equal_sort[a37](nil, cons(v37, v38)) → false
equal_sort[a37](nil, nil) → true
equal_sort[a45](true_renamed, true_renamed) → true
equal_sort[a45](true_renamed, false_renamed) → false
equal_sort[a45](false_renamed, true_renamed) → false
equal_sort[a45](false_renamed, false_renamed) → true
equal_sort[a65](witness_sort[a65], witness_sort[a65]) → true
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
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)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(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[a37](cons(x0, x1), cons(x2, x3))
equal_sort[a37](cons(x0, x1), nil)
equal_sort[a37](nil, cons(x0, x1))
equal_sort[a37](nil, nil)
equal_sort[a45](true_renamed, true_renamed)
equal_sort[a45](true_renamed, false_renamed)
equal_sort[a45](false_renamed, true_renamed)
equal_sort[a45](false_renamed, false_renamed)
equal_sort[a65](witness_sort[a65], witness_sort[a65])
EQUAL_SORT[A0](s(v31), s(v32)) → EQUAL_SORT[A0](v31, v32)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
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)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(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[a37](cons(x0, x1), cons(x2, x3))
equal_sort[a37](cons(x0, x1), nil)
equal_sort[a37](nil, cons(x0, x1))
equal_sort[a37](nil, nil)
equal_sort[a45](true_renamed, true_renamed)
equal_sort[a45](true_renamed, false_renamed)
equal_sort[a45](false_renamed, true_renamed)
equal_sort[a45](false_renamed, false_renamed)
equal_sort[a65](witness_sort[a65], witness_sort[a65])
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
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)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(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[a37](cons(x0, x1), cons(x2, x3))
equal_sort[a37](cons(x0, x1), nil)
equal_sort[a37](nil, cons(x0, x1))
equal_sort[a37](nil, nil)
equal_sort[a45](true_renamed, true_renamed)
equal_sort[a45](true_renamed, false_renamed)
equal_sort[a45](false_renamed, true_renamed)
equal_sort[a45](false_renamed, false_renamed)
equal_sort[a65](witness_sort[a65], witness_sort[a65])
EQUAL_SORT[A0](s(v31), s(v32)) → EQUAL_SORT[A0](v31, v32)
From the DPs we obtained the following set of size-change graphs:
EQUAL_SORT[A37](cons(v33, v34), cons(v35, v36)) → EQUAL_SORT[A37](v34, v36)
del'(x3, cons(y1, xs2)) → if2'(eq(x3, y1), x3, y1, xs2)
if2'(true_renamed, x7, y4, xs4) → true
if2'(false_renamed, x8, y5, xs5) → del'(x8, xs5)
del'(x9, nil) → false
max(cons(x', nil)) → x'
max(cons(x'', cons(y, xs'))) → if1(ge(x'', y), x'', y, xs')
if1(true_renamed, x1, y', xs'') → max(cons(x1, xs''))
if1(false_renamed, x2, y'', xs1) → max(cons(y'', xs1))
del(x3, cons(y1, xs2)) → if2(eq(x3, y1), x3, y1, xs2)
h(nil) → nil
h(cons(x4, xs3)) → cons(x4, h(xs3))
eq(0, 0) → true_renamed
eq(0, s(y2)) → false_renamed
eq(s(x5), 0) → false_renamed
eq(s(x6), s(y3)) → eq(x6, y3)
if2(true_renamed, x7, y4, xs4) → xs4
if2(false_renamed, x8, y5, xs5) → cons(y5, del(x8, xs5))
del(x9, nil) → nil
ge(0, 0) → true_renamed
ge(s(x10), 0) → true_renamed
ge(0, s(x11)) → false_renamed
ge(s(x12), s(y6)) → ge(x12, y6)
max(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(v30)) → false
equal_sort[a0](s(v31), 0) → false
equal_sort[a0](s(v31), s(v32)) → equal_sort[a0](v31, v32)
equal_sort[a37](cons(v33, v34), cons(v35, v36)) → and(equal_sort[a0](v33, v35), equal_sort[a37](v34, v36))
equal_sort[a37](cons(v33, v34), nil) → false
equal_sort[a37](nil, cons(v37, v38)) → false
equal_sort[a37](nil, nil) → true
equal_sort[a45](true_renamed, true_renamed) → true
equal_sort[a45](true_renamed, false_renamed) → false
equal_sort[a45](false_renamed, true_renamed) → false
equal_sort[a45](false_renamed, false_renamed) → true
equal_sort[a65](witness_sort[a65], witness_sort[a65]) → true
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
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)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(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[a37](cons(x0, x1), cons(x2, x3))
equal_sort[a37](cons(x0, x1), nil)
equal_sort[a37](nil, cons(x0, x1))
equal_sort[a37](nil, nil)
equal_sort[a45](true_renamed, true_renamed)
equal_sort[a45](true_renamed, false_renamed)
equal_sort[a45](false_renamed, true_renamed)
equal_sort[a45](false_renamed, false_renamed)
equal_sort[a65](witness_sort[a65], witness_sort[a65])
EQUAL_SORT[A37](cons(v33, v34), cons(v35, v36)) → EQUAL_SORT[A37](v34, v36)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
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)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(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[a37](cons(x0, x1), cons(x2, x3))
equal_sort[a37](cons(x0, x1), nil)
equal_sort[a37](nil, cons(x0, x1))
equal_sort[a37](nil, nil)
equal_sort[a45](true_renamed, true_renamed)
equal_sort[a45](true_renamed, false_renamed)
equal_sort[a45](false_renamed, true_renamed)
equal_sort[a45](false_renamed, false_renamed)
equal_sort[a65](witness_sort[a65], witness_sort[a65])
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
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)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(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[a37](cons(x0, x1), cons(x2, x3))
equal_sort[a37](cons(x0, x1), nil)
equal_sort[a37](nil, cons(x0, x1))
equal_sort[a37](nil, nil)
equal_sort[a45](true_renamed, true_renamed)
equal_sort[a45](true_renamed, false_renamed)
equal_sort[a45](false_renamed, true_renamed)
equal_sort[a45](false_renamed, false_renamed)
equal_sort[a65](witness_sort[a65], witness_sort[a65])
EQUAL_SORT[A37](cons(v33, v34), cons(v35, v36)) → EQUAL_SORT[A37](v34, v36)
From the DPs we obtained the following set of size-change graphs:
GE(s(x12), s(y6)) → GE(x12, y6)
del'(x3, cons(y1, xs2)) → if2'(eq(x3, y1), x3, y1, xs2)
if2'(true_renamed, x7, y4, xs4) → true
if2'(false_renamed, x8, y5, xs5) → del'(x8, xs5)
del'(x9, nil) → false
max(cons(x', nil)) → x'
max(cons(x'', cons(y, xs'))) → if1(ge(x'', y), x'', y, xs')
if1(true_renamed, x1, y', xs'') → max(cons(x1, xs''))
if1(false_renamed, x2, y'', xs1) → max(cons(y'', xs1))
del(x3, cons(y1, xs2)) → if2(eq(x3, y1), x3, y1, xs2)
h(nil) → nil
h(cons(x4, xs3)) → cons(x4, h(xs3))
eq(0, 0) → true_renamed
eq(0, s(y2)) → false_renamed
eq(s(x5), 0) → false_renamed
eq(s(x6), s(y3)) → eq(x6, y3)
if2(true_renamed, x7, y4, xs4) → xs4
if2(false_renamed, x8, y5, xs5) → cons(y5, del(x8, xs5))
del(x9, nil) → nil
ge(0, 0) → true_renamed
ge(s(x10), 0) → true_renamed
ge(0, s(x11)) → false_renamed
ge(s(x12), s(y6)) → ge(x12, y6)
max(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(v30)) → false
equal_sort[a0](s(v31), 0) → false
equal_sort[a0](s(v31), s(v32)) → equal_sort[a0](v31, v32)
equal_sort[a37](cons(v33, v34), cons(v35, v36)) → and(equal_sort[a0](v33, v35), equal_sort[a37](v34, v36))
equal_sort[a37](cons(v33, v34), nil) → false
equal_sort[a37](nil, cons(v37, v38)) → false
equal_sort[a37](nil, nil) → true
equal_sort[a45](true_renamed, true_renamed) → true
equal_sort[a45](true_renamed, false_renamed) → false
equal_sort[a45](false_renamed, true_renamed) → false
equal_sort[a45](false_renamed, false_renamed) → true
equal_sort[a65](witness_sort[a65], witness_sort[a65]) → true
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
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)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(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[a37](cons(x0, x1), cons(x2, x3))
equal_sort[a37](cons(x0, x1), nil)
equal_sort[a37](nil, cons(x0, x1))
equal_sort[a37](nil, nil)
equal_sort[a45](true_renamed, true_renamed)
equal_sort[a45](true_renamed, false_renamed)
equal_sort[a45](false_renamed, true_renamed)
equal_sort[a45](false_renamed, false_renamed)
equal_sort[a65](witness_sort[a65], witness_sort[a65])
GE(s(x12), s(y6)) → GE(x12, y6)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
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)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(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[a37](cons(x0, x1), cons(x2, x3))
equal_sort[a37](cons(x0, x1), nil)
equal_sort[a37](nil, cons(x0, x1))
equal_sort[a37](nil, nil)
equal_sort[a45](true_renamed, true_renamed)
equal_sort[a45](true_renamed, false_renamed)
equal_sort[a45](false_renamed, true_renamed)
equal_sort[a45](false_renamed, false_renamed)
equal_sort[a65](witness_sort[a65], witness_sort[a65])
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
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)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(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[a37](cons(x0, x1), cons(x2, x3))
equal_sort[a37](cons(x0, x1), nil)
equal_sort[a37](nil, cons(x0, x1))
equal_sort[a37](nil, nil)
equal_sort[a45](true_renamed, true_renamed)
equal_sort[a45](true_renamed, false_renamed)
equal_sort[a45](false_renamed, true_renamed)
equal_sort[a45](false_renamed, false_renamed)
equal_sort[a65](witness_sort[a65], witness_sort[a65])
GE(s(x12), s(y6)) → GE(x12, y6)
From the DPs we obtained the following set of size-change graphs:
EQ(s(x6), s(y3)) → EQ(x6, y3)
del'(x3, cons(y1, xs2)) → if2'(eq(x3, y1), x3, y1, xs2)
if2'(true_renamed, x7, y4, xs4) → true
if2'(false_renamed, x8, y5, xs5) → del'(x8, xs5)
del'(x9, nil) → false
max(cons(x', nil)) → x'
max(cons(x'', cons(y, xs'))) → if1(ge(x'', y), x'', y, xs')
if1(true_renamed, x1, y', xs'') → max(cons(x1, xs''))
if1(false_renamed, x2, y'', xs1) → max(cons(y'', xs1))
del(x3, cons(y1, xs2)) → if2(eq(x3, y1), x3, y1, xs2)
h(nil) → nil
h(cons(x4, xs3)) → cons(x4, h(xs3))
eq(0, 0) → true_renamed
eq(0, s(y2)) → false_renamed
eq(s(x5), 0) → false_renamed
eq(s(x6), s(y3)) → eq(x6, y3)
if2(true_renamed, x7, y4, xs4) → xs4
if2(false_renamed, x8, y5, xs5) → cons(y5, del(x8, xs5))
del(x9, nil) → nil
ge(0, 0) → true_renamed
ge(s(x10), 0) → true_renamed
ge(0, s(x11)) → false_renamed
ge(s(x12), s(y6)) → ge(x12, y6)
max(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(v30)) → false
equal_sort[a0](s(v31), 0) → false
equal_sort[a0](s(v31), s(v32)) → equal_sort[a0](v31, v32)
equal_sort[a37](cons(v33, v34), cons(v35, v36)) → and(equal_sort[a0](v33, v35), equal_sort[a37](v34, v36))
equal_sort[a37](cons(v33, v34), nil) → false
equal_sort[a37](nil, cons(v37, v38)) → false
equal_sort[a37](nil, nil) → true
equal_sort[a45](true_renamed, true_renamed) → true
equal_sort[a45](true_renamed, false_renamed) → false
equal_sort[a45](false_renamed, true_renamed) → false
equal_sort[a45](false_renamed, false_renamed) → true
equal_sort[a65](witness_sort[a65], witness_sort[a65]) → true
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
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)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(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[a37](cons(x0, x1), cons(x2, x3))
equal_sort[a37](cons(x0, x1), nil)
equal_sort[a37](nil, cons(x0, x1))
equal_sort[a37](nil, nil)
equal_sort[a45](true_renamed, true_renamed)
equal_sort[a45](true_renamed, false_renamed)
equal_sort[a45](false_renamed, true_renamed)
equal_sort[a45](false_renamed, false_renamed)
equal_sort[a65](witness_sort[a65], witness_sort[a65])
EQ(s(x6), s(y3)) → EQ(x6, y3)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
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)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(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[a37](cons(x0, x1), cons(x2, x3))
equal_sort[a37](cons(x0, x1), nil)
equal_sort[a37](nil, cons(x0, x1))
equal_sort[a37](nil, nil)
equal_sort[a45](true_renamed, true_renamed)
equal_sort[a45](true_renamed, false_renamed)
equal_sort[a45](false_renamed, true_renamed)
equal_sort[a45](false_renamed, false_renamed)
equal_sort[a65](witness_sort[a65], witness_sort[a65])
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
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)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(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[a37](cons(x0, x1), cons(x2, x3))
equal_sort[a37](cons(x0, x1), nil)
equal_sort[a37](nil, cons(x0, x1))
equal_sort[a37](nil, nil)
equal_sort[a45](true_renamed, true_renamed)
equal_sort[a45](true_renamed, false_renamed)
equal_sort[a45](false_renamed, true_renamed)
equal_sort[a45](false_renamed, false_renamed)
equal_sort[a65](witness_sort[a65], witness_sort[a65])
EQ(s(x6), s(y3)) → EQ(x6, y3)
From the DPs we obtained the following set of size-change graphs:
H(cons(x4, xs3)) → H(xs3)
del'(x3, cons(y1, xs2)) → if2'(eq(x3, y1), x3, y1, xs2)
if2'(true_renamed, x7, y4, xs4) → true
if2'(false_renamed, x8, y5, xs5) → del'(x8, xs5)
del'(x9, nil) → false
max(cons(x', nil)) → x'
max(cons(x'', cons(y, xs'))) → if1(ge(x'', y), x'', y, xs')
if1(true_renamed, x1, y', xs'') → max(cons(x1, xs''))
if1(false_renamed, x2, y'', xs1) → max(cons(y'', xs1))
del(x3, cons(y1, xs2)) → if2(eq(x3, y1), x3, y1, xs2)
h(nil) → nil
h(cons(x4, xs3)) → cons(x4, h(xs3))
eq(0, 0) → true_renamed
eq(0, s(y2)) → false_renamed
eq(s(x5), 0) → false_renamed
eq(s(x6), s(y3)) → eq(x6, y3)
if2(true_renamed, x7, y4, xs4) → xs4
if2(false_renamed, x8, y5, xs5) → cons(y5, del(x8, xs5))
del(x9, nil) → nil
ge(0, 0) → true_renamed
ge(s(x10), 0) → true_renamed
ge(0, s(x11)) → false_renamed
ge(s(x12), s(y6)) → ge(x12, y6)
max(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(v30)) → false
equal_sort[a0](s(v31), 0) → false
equal_sort[a0](s(v31), s(v32)) → equal_sort[a0](v31, v32)
equal_sort[a37](cons(v33, v34), cons(v35, v36)) → and(equal_sort[a0](v33, v35), equal_sort[a37](v34, v36))
equal_sort[a37](cons(v33, v34), nil) → false
equal_sort[a37](nil, cons(v37, v38)) → false
equal_sort[a37](nil, nil) → true
equal_sort[a45](true_renamed, true_renamed) → true
equal_sort[a45](true_renamed, false_renamed) → false
equal_sort[a45](false_renamed, true_renamed) → false
equal_sort[a45](false_renamed, false_renamed) → true
equal_sort[a65](witness_sort[a65], witness_sort[a65]) → true
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
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)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(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[a37](cons(x0, x1), cons(x2, x3))
equal_sort[a37](cons(x0, x1), nil)
equal_sort[a37](nil, cons(x0, x1))
equal_sort[a37](nil, nil)
equal_sort[a45](true_renamed, true_renamed)
equal_sort[a45](true_renamed, false_renamed)
equal_sort[a45](false_renamed, true_renamed)
equal_sort[a45](false_renamed, false_renamed)
equal_sort[a65](witness_sort[a65], witness_sort[a65])
H(cons(x4, xs3)) → H(xs3)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
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)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(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[a37](cons(x0, x1), cons(x2, x3))
equal_sort[a37](cons(x0, x1), nil)
equal_sort[a37](nil, cons(x0, x1))
equal_sort[a37](nil, nil)
equal_sort[a45](true_renamed, true_renamed)
equal_sort[a45](true_renamed, false_renamed)
equal_sort[a45](false_renamed, true_renamed)
equal_sort[a45](false_renamed, false_renamed)
equal_sort[a65](witness_sort[a65], witness_sort[a65])
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
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)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(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[a37](cons(x0, x1), cons(x2, x3))
equal_sort[a37](cons(x0, x1), nil)
equal_sort[a37](nil, cons(x0, x1))
equal_sort[a37](nil, nil)
equal_sort[a45](true_renamed, true_renamed)
equal_sort[a45](true_renamed, false_renamed)
equal_sort[a45](false_renamed, true_renamed)
equal_sort[a45](false_renamed, false_renamed)
equal_sort[a65](witness_sort[a65], witness_sort[a65])
H(cons(x4, xs3)) → H(xs3)
From the DPs we obtained the following set of size-change graphs:
IF2(false_renamed, x8, y5, xs5) → DEL(x8, xs5)
DEL(x3, cons(y1, xs2)) → IF2(eq(x3, y1), x3, y1, xs2)
del'(x3, cons(y1, xs2)) → if2'(eq(x3, y1), x3, y1, xs2)
if2'(true_renamed, x7, y4, xs4) → true
if2'(false_renamed, x8, y5, xs5) → del'(x8, xs5)
del'(x9, nil) → false
max(cons(x', nil)) → x'
max(cons(x'', cons(y, xs'))) → if1(ge(x'', y), x'', y, xs')
if1(true_renamed, x1, y', xs'') → max(cons(x1, xs''))
if1(false_renamed, x2, y'', xs1) → max(cons(y'', xs1))
del(x3, cons(y1, xs2)) → if2(eq(x3, y1), x3, y1, xs2)
h(nil) → nil
h(cons(x4, xs3)) → cons(x4, h(xs3))
eq(0, 0) → true_renamed
eq(0, s(y2)) → false_renamed
eq(s(x5), 0) → false_renamed
eq(s(x6), s(y3)) → eq(x6, y3)
if2(true_renamed, x7, y4, xs4) → xs4
if2(false_renamed, x8, y5, xs5) → cons(y5, del(x8, xs5))
del(x9, nil) → nil
ge(0, 0) → true_renamed
ge(s(x10), 0) → true_renamed
ge(0, s(x11)) → false_renamed
ge(s(x12), s(y6)) → ge(x12, y6)
max(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(v30)) → false
equal_sort[a0](s(v31), 0) → false
equal_sort[a0](s(v31), s(v32)) → equal_sort[a0](v31, v32)
equal_sort[a37](cons(v33, v34), cons(v35, v36)) → and(equal_sort[a0](v33, v35), equal_sort[a37](v34, v36))
equal_sort[a37](cons(v33, v34), nil) → false
equal_sort[a37](nil, cons(v37, v38)) → false
equal_sort[a37](nil, nil) → true
equal_sort[a45](true_renamed, true_renamed) → true
equal_sort[a45](true_renamed, false_renamed) → false
equal_sort[a45](false_renamed, true_renamed) → false
equal_sort[a45](false_renamed, false_renamed) → true
equal_sort[a65](witness_sort[a65], witness_sort[a65]) → true
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
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)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(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[a37](cons(x0, x1), cons(x2, x3))
equal_sort[a37](cons(x0, x1), nil)
equal_sort[a37](nil, cons(x0, x1))
equal_sort[a37](nil, nil)
equal_sort[a45](true_renamed, true_renamed)
equal_sort[a45](true_renamed, false_renamed)
equal_sort[a45](false_renamed, true_renamed)
equal_sort[a45](false_renamed, false_renamed)
equal_sort[a65](witness_sort[a65], witness_sort[a65])
IF2(false_renamed, x8, y5, xs5) → DEL(x8, xs5)
DEL(x3, cons(y1, xs2)) → IF2(eq(x3, y1), x3, y1, xs2)
eq(0, 0) → true_renamed
eq(0, s(y2)) → false_renamed
eq(s(x5), 0) → false_renamed
eq(s(x6), s(y3)) → eq(x6, y3)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
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)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(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[a37](cons(x0, x1), cons(x2, x3))
equal_sort[a37](cons(x0, x1), nil)
equal_sort[a37](nil, cons(x0, x1))
equal_sort[a37](nil, nil)
equal_sort[a45](true_renamed, true_renamed)
equal_sort[a45](true_renamed, false_renamed)
equal_sort[a45](false_renamed, true_renamed)
equal_sort[a45](false_renamed, false_renamed)
equal_sort[a65](witness_sort[a65], witness_sort[a65])
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
if2(true_renamed, x0, x1, x2)
if2(false_renamed, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(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[a37](cons(x0, x1), cons(x2, x3))
equal_sort[a37](cons(x0, x1), nil)
equal_sort[a37](nil, cons(x0, x1))
equal_sort[a37](nil, nil)
equal_sort[a45](true_renamed, true_renamed)
equal_sort[a45](true_renamed, false_renamed)
equal_sort[a45](false_renamed, true_renamed)
equal_sort[a45](false_renamed, false_renamed)
equal_sort[a65](witness_sort[a65], witness_sort[a65])
IF2(false_renamed, x8, y5, xs5) → DEL(x8, xs5)
DEL(x3, cons(y1, xs2)) → IF2(eq(x3, y1), x3, y1, xs2)
eq(0, 0) → true_renamed
eq(0, s(y2)) → false_renamed
eq(s(x5), 0) → false_renamed
eq(s(x6), s(y3)) → eq(x6, y3)
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'') → MAX(cons(x1, xs''))
MAX(cons(x'', cons(y, xs'))) → IF1(ge(x'', y), x'', y, xs')
IF1(false_renamed, x2, y'', xs1) → MAX(cons(y'', xs1))
del'(x3, cons(y1, xs2)) → if2'(eq(x3, y1), x3, y1, xs2)
if2'(true_renamed, x7, y4, xs4) → true
if2'(false_renamed, x8, y5, xs5) → del'(x8, xs5)
del'(x9, nil) → false
max(cons(x', nil)) → x'
max(cons(x'', cons(y, xs'))) → if1(ge(x'', y), x'', y, xs')
if1(true_renamed, x1, y', xs'') → max(cons(x1, xs''))
if1(false_renamed, x2, y'', xs1) → max(cons(y'', xs1))
del(x3, cons(y1, xs2)) → if2(eq(x3, y1), x3, y1, xs2)
h(nil) → nil
h(cons(x4, xs3)) → cons(x4, h(xs3))
eq(0, 0) → true_renamed
eq(0, s(y2)) → false_renamed
eq(s(x5), 0) → false_renamed
eq(s(x6), s(y3)) → eq(x6, y3)
if2(true_renamed, x7, y4, xs4) → xs4
if2(false_renamed, x8, y5, xs5) → cons(y5, del(x8, xs5))
del(x9, nil) → nil
ge(0, 0) → true_renamed
ge(s(x10), 0) → true_renamed
ge(0, s(x11)) → false_renamed
ge(s(x12), s(y6)) → ge(x12, y6)
max(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(v30)) → false
equal_sort[a0](s(v31), 0) → false
equal_sort[a0](s(v31), s(v32)) → equal_sort[a0](v31, v32)
equal_sort[a37](cons(v33, v34), cons(v35, v36)) → and(equal_sort[a0](v33, v35), equal_sort[a37](v34, v36))
equal_sort[a37](cons(v33, v34), nil) → false
equal_sort[a37](nil, cons(v37, v38)) → false
equal_sort[a37](nil, nil) → true
equal_sort[a45](true_renamed, true_renamed) → true
equal_sort[a45](true_renamed, false_renamed) → false
equal_sort[a45](false_renamed, true_renamed) → false
equal_sort[a45](false_renamed, false_renamed) → true
equal_sort[a65](witness_sort[a65], witness_sort[a65]) → true
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
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)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(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[a37](cons(x0, x1), cons(x2, x3))
equal_sort[a37](cons(x0, x1), nil)
equal_sort[a37](nil, cons(x0, x1))
equal_sort[a37](nil, nil)
equal_sort[a45](true_renamed, true_renamed)
equal_sort[a45](true_renamed, false_renamed)
equal_sort[a45](false_renamed, true_renamed)
equal_sort[a45](false_renamed, false_renamed)
equal_sort[a65](witness_sort[a65], witness_sort[a65])
IF1(true_renamed, x1, y', xs'') → MAX(cons(x1, xs''))
MAX(cons(x'', cons(y, xs'))) → IF1(ge(x'', y), x'', y, xs')
IF1(false_renamed, x2, y'', xs1) → MAX(cons(y'', xs1))
ge(0, 0) → true_renamed
ge(s(x10), 0) → true_renamed
ge(0, s(x11)) → false_renamed
ge(s(x12), s(y6)) → ge(x12, y6)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
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)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(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[a37](cons(x0, x1), cons(x2, x3))
equal_sort[a37](cons(x0, x1), nil)
equal_sort[a37](nil, cons(x0, x1))
equal_sort[a37](nil, nil)
equal_sort[a45](true_renamed, true_renamed)
equal_sort[a45](true_renamed, false_renamed)
equal_sort[a45](false_renamed, true_renamed)
equal_sort[a45](false_renamed, false_renamed)
equal_sort[a65](witness_sort[a65], witness_sort[a65])
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
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)
max(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[a37](cons(x0, x1), cons(x2, x3))
equal_sort[a37](cons(x0, x1), nil)
equal_sort[a37](nil, cons(x0, x1))
equal_sort[a37](nil, nil)
equal_sort[a45](true_renamed, true_renamed)
equal_sort[a45](true_renamed, false_renamed)
equal_sort[a45](false_renamed, true_renamed)
equal_sort[a45](false_renamed, false_renamed)
equal_sort[a65](witness_sort[a65], witness_sort[a65])
IF1(true_renamed, x1, y', xs'') → MAX(cons(x1, xs''))
MAX(cons(x'', cons(y, xs'))) → IF1(ge(x'', y), x'', y, xs')
IF1(false_renamed, x2, y'', xs1) → MAX(cons(y'', xs1))
ge(0, 0) → true_renamed
ge(s(x10), 0) → true_renamed
ge(0, s(x11)) → false_renamed
ge(s(x12), s(y6)) → ge(x12, y6)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(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'') → MAX(cons(x1, xs''))
MAX(cons(x'', cons(y, xs'))) → IF1(ge(x'', y), x'', y, xs')
IF1(false_renamed, x2, y'', xs1) → MAX(cons(y'', xs1))
trivial
dummyConstant=1
IF1_1=3
cons_1=2
ge(0, 0) → true_renamed
ge(s(x10), 0) → true_renamed
ge(0, s(x11)) → false_renamed
ge(s(x12), s(y6)) → ge(x12, y6)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
IF2'(false_renamed, x8, y5, xs5) → DEL'(x8, xs5)
DEL'(x3, cons(y1, xs2)) → IF2'(eq(x3, y1), x3, y1, xs2)
del'(x3, cons(y1, xs2)) → if2'(eq(x3, y1), x3, y1, xs2)
if2'(true_renamed, x7, y4, xs4) → true
if2'(false_renamed, x8, y5, xs5) → del'(x8, xs5)
del'(x9, nil) → false
max(cons(x', nil)) → x'
max(cons(x'', cons(y, xs'))) → if1(ge(x'', y), x'', y, xs')
if1(true_renamed, x1, y', xs'') → max(cons(x1, xs''))
if1(false_renamed, x2, y'', xs1) → max(cons(y'', xs1))
del(x3, cons(y1, xs2)) → if2(eq(x3, y1), x3, y1, xs2)
h(nil) → nil
h(cons(x4, xs3)) → cons(x4, h(xs3))
eq(0, 0) → true_renamed
eq(0, s(y2)) → false_renamed
eq(s(x5), 0) → false_renamed
eq(s(x6), s(y3)) → eq(x6, y3)
if2(true_renamed, x7, y4, xs4) → xs4
if2(false_renamed, x8, y5, xs5) → cons(y5, del(x8, xs5))
del(x9, nil) → nil
ge(0, 0) → true_renamed
ge(s(x10), 0) → true_renamed
ge(0, s(x11)) → false_renamed
ge(s(x12), s(y6)) → ge(x12, y6)
max(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(v30)) → false
equal_sort[a0](s(v31), 0) → false
equal_sort[a0](s(v31), s(v32)) → equal_sort[a0](v31, v32)
equal_sort[a37](cons(v33, v34), cons(v35, v36)) → and(equal_sort[a0](v33, v35), equal_sort[a37](v34, v36))
equal_sort[a37](cons(v33, v34), nil) → false
equal_sort[a37](nil, cons(v37, v38)) → false
equal_sort[a37](nil, nil) → true
equal_sort[a45](true_renamed, true_renamed) → true
equal_sort[a45](true_renamed, false_renamed) → false
equal_sort[a45](false_renamed, true_renamed) → false
equal_sort[a45](false_renamed, false_renamed) → true
equal_sort[a65](witness_sort[a65], witness_sort[a65]) → true
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
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)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(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[a37](cons(x0, x1), cons(x2, x3))
equal_sort[a37](cons(x0, x1), nil)
equal_sort[a37](nil, cons(x0, x1))
equal_sort[a37](nil, nil)
equal_sort[a45](true_renamed, true_renamed)
equal_sort[a45](true_renamed, false_renamed)
equal_sort[a45](false_renamed, true_renamed)
equal_sort[a45](false_renamed, false_renamed)
equal_sort[a65](witness_sort[a65], witness_sort[a65])
IF2'(false_renamed, x8, y5, xs5) → DEL'(x8, xs5)
DEL'(x3, cons(y1, xs2)) → IF2'(eq(x3, y1), x3, y1, xs2)
eq(0, 0) → true_renamed
eq(0, s(y2)) → false_renamed
eq(s(x5), 0) → false_renamed
eq(s(x6), s(y3)) → eq(x6, y3)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
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)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(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[a37](cons(x0, x1), cons(x2, x3))
equal_sort[a37](cons(x0, x1), nil)
equal_sort[a37](nil, cons(x0, x1))
equal_sort[a37](nil, nil)
equal_sort[a45](true_renamed, true_renamed)
equal_sort[a45](true_renamed, false_renamed)
equal_sort[a45](false_renamed, true_renamed)
equal_sort[a45](false_renamed, false_renamed)
equal_sort[a65](witness_sort[a65], witness_sort[a65])
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true_renamed, x0, x1, x2)
if1(false_renamed, x0, x1, x2)
del(x0, cons(x1, x2))
h(nil)
h(cons(x0, x1))
if2(true_renamed, x0, x1, x2)
if2(false_renamed, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(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[a37](cons(x0, x1), cons(x2, x3))
equal_sort[a37](cons(x0, x1), nil)
equal_sort[a37](nil, cons(x0, x1))
equal_sort[a37](nil, nil)
equal_sort[a45](true_renamed, true_renamed)
equal_sort[a45](true_renamed, false_renamed)
equal_sort[a45](false_renamed, true_renamed)
equal_sort[a45](false_renamed, false_renamed)
equal_sort[a65](witness_sort[a65], witness_sort[a65])
IF2'(false_renamed, x8, y5, xs5) → DEL'(x8, xs5)
DEL'(x3, cons(y1, xs2)) → IF2'(eq(x3, y1), x3, y1, xs2)
eq(0, 0) → true_renamed
eq(0, s(y2)) → false_renamed
eq(s(x5), 0) → false_renamed
eq(s(x6), s(y3)) → eq(x6, y3)
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: