YES
0 QTRS
↳1 Overlay + Local Confluence (⇔, 0 ms)
↳2 QTRS
↳3 DependencyPairsProof (⇔, 0 ms)
↳4 QDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 QDP
↳10 QReductionProof (⇔, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 QDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 QDP
↳17 QReductionProof (⇔, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 QDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 QDP
↳24 QReductionProof (⇔, 0 ms)
↳25 QDP
↳26 QDPSizeChangeProof (⇔, 0 ms)
↳27 YES
↳28 QDP
↳29 UsableRulesProof (⇔, 0 ms)
↳30 QDP
↳31 QReductionProof (⇔, 0 ms)
↳32 QDP
↳33 QDPOrderProof (⇔, 0 ms)
↳34 QDP
↳35 PisEmptyProof (⇔, 0 ms)
↳36 YES
↳37 QDP
↳38 UsableRulesProof (⇔, 0 ms)
↳39 QDP
↳40 QReductionProof (⇔, 0 ms)
↳41 QDP
↳42 TransformationProof (⇔, 2 ms)
↳43 QDP
↳44 DependencyGraphProof (⇔, 0 ms)
↳45 QDP
↳46 UsableRulesProof (⇔, 0 ms)
↳47 QDP
↳48 QReductionProof (⇔, 0 ms)
↳49 QDP
↳50 TransformationProof (⇔, 0 ms)
↳51 QDP
↳52 Induction-Processor (⇒, 45 ms)
↳53 AND
↳54 QDP
↳55 DependencyGraphProof (⇔, 0 ms)
↳56 TRUE
↳57 QTRS
↳58 Overlay + Local Confluence (⇔, 0 ms)
↳59 QTRS
↳60 DependencyPairsProof (⇔, 0 ms)
↳61 QDP
↳62 DependencyGraphProof (⇔, 0 ms)
↳63 AND
↳64 QDP
↳65 UsableRulesProof (⇔, 0 ms)
↳66 QDP
↳67 QReductionProof (⇔, 0 ms)
↳68 QDP
↳69 QDPSizeChangeProof (⇔, 0 ms)
↳70 YES
↳71 QDP
↳72 UsableRulesProof (⇔, 0 ms)
↳73 QDP
↳74 QReductionProof (⇔, 0 ms)
↳75 QDP
↳76 QDPSizeChangeProof (⇔, 0 ms)
↳77 YES
↳78 QDP
↳79 UsableRulesProof (⇔, 0 ms)
↳80 QDP
↳81 QReductionProof (⇔, 0 ms)
↳82 QDP
↳83 QDPSizeChangeProof (⇔, 0 ms)
↳84 YES
↳85 QDP
↳86 UsableRulesProof (⇔, 0 ms)
↳87 QDP
↳88 QReductionProof (⇔, 0 ms)
↳89 QDP
↳90 QDPSizeChangeProof (⇔, 0 ms)
↳91 YES
↳92 QDP
↳93 UsableRulesProof (⇔, 0 ms)
↳94 QDP
↳95 QReductionProof (⇔, 0 ms)
↳96 QDP
↳97 QDPSizeChangeProof (⇔, 0 ms)
↳98 YES
↳99 QDP
↳100 UsableRulesProof (⇔, 0 ms)
↳101 QDP
↳102 QReductionProof (⇔, 0 ms)
↳103 QDP
↳104 QDPOrderProof (⇔, 0 ms)
↳105 QDP
↳106 PisEmptyProof (⇔, 0 ms)
↳107 YES
↳108 QDP
↳109 UsableRulesProof (⇔, 0 ms)
↳110 QDP
↳111 QReductionProof (⇔, 0 ms)
↳112 QDP
↳113 QDPSizeChangeProof (⇔, 0 ms)
↳114 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(xs) → if3(empty(xs), xs)
if3(true, xs) → nil
if3(false, xs) → sort(del(max(xs), xs))
empty(nil) → true
empty(cons(x, xs)) → false
ge(x, 0) → true
ge(0, s(x)) → false
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(xs) → if3(empty(xs), xs)
if3(true, xs) → nil
if3(false, xs) → sort(del(max(xs), xs))
empty(nil) → true
empty(cons(x, xs)) → false
ge(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(x0)
if3(true, x0)
if3(false, x0)
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(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(xs) → IF3(empty(xs), xs)
SORT(xs) → EMPTY(xs)
IF3(false, xs) → SORT(del(max(xs), xs))
IF3(false, xs) → DEL(max(xs), xs)
IF3(false, xs) → MAX(xs)
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(xs) → if3(empty(xs), xs)
if3(true, xs) → nil
if3(false, xs) → sort(del(max(xs), xs))
empty(nil) → true
empty(cons(x, xs)) → false
ge(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(x0)
if3(true, x0)
if3(false, x0)
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
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(xs) → if3(empty(xs), xs)
if3(true, xs) → nil
if3(false, xs) → sort(del(max(xs), xs))
empty(nil) → true
empty(cons(x, xs)) → false
ge(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(x0)
if3(true, x0)
if3(false, x0)
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(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(x0)
if3(true, x0)
if3(false, x0)
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(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(x0)
if3(true, x0)
if3(false, x0)
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(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(xs) → if3(empty(xs), xs)
if3(true, xs) → nil
if3(false, xs) → sort(del(max(xs), xs))
empty(nil) → true
empty(cons(x, xs)) → false
ge(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(x0)
if3(true, x0)
if3(false, x0)
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(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(x0)
if3(true, x0)
if3(false, x0)
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(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(x0)
if3(true, x0)
if3(false, x0)
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(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(xs) → if3(empty(xs), xs)
if3(true, xs) → nil
if3(false, xs) → sort(del(max(xs), xs))
empty(nil) → true
empty(cons(x, xs)) → false
ge(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(x0)
if3(true, x0)
if3(false, x0)
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(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(x0)
if3(true, x0)
if3(false, x0)
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(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(x0)
if3(true, x0)
if3(false, x0)
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(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(xs) → if3(empty(xs), xs)
if3(true, xs) → nil
if3(false, xs) → sort(del(max(xs), xs))
empty(nil) → true
empty(cons(x, xs)) → false
ge(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(x0)
if3(true, x0)
if3(false, x0)
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(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(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(x0)
if3(true, x0)
if3(false, x0)
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(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(x0)
if3(true, x0)
if3(false, x0)
empty(nil)
empty(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(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
ge(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(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
IF3(false, xs) → SORT(del(max(xs), xs))
SORT(xs) → IF3(empty(xs), 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(xs) → if3(empty(xs), xs)
if3(true, xs) → nil
if3(false, xs) → sort(del(max(xs), xs))
empty(nil) → true
empty(cons(x, xs)) → false
ge(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(x0)
if3(true, x0)
if3(false, x0)
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
IF3(false, xs) → SORT(del(max(xs), xs))
SORT(xs) → IF3(empty(xs), xs)
empty(nil) → true
empty(cons(x, xs)) → false
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)
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))
ge(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(x0)
if3(true, x0)
if3(false, x0)
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
sort(x0)
if3(true, x0)
if3(false, x0)
IF3(false, xs) → SORT(del(max(xs), xs))
SORT(xs) → IF3(empty(xs), xs)
empty(nil) → true
empty(cons(x, xs)) → false
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)
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))
ge(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))
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
SORT(nil) → IF3(true, nil) → SORT(nil) → IF3(true, nil)
SORT(cons(x0, x1)) → IF3(false, cons(x0, x1)) → SORT(cons(x0, x1)) → IF3(false, cons(x0, x1))
IF3(false, xs) → SORT(del(max(xs), xs))
SORT(nil) → IF3(true, nil)
SORT(cons(x0, x1)) → IF3(false, cons(x0, x1))
empty(nil) → true
empty(cons(x, xs)) → false
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)
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))
ge(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))
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
SORT(cons(x0, x1)) → IF3(false, cons(x0, x1))
IF3(false, xs) → SORT(del(max(xs), xs))
empty(nil) → true
empty(cons(x, xs)) → false
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)
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))
ge(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))
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
SORT(cons(x0, x1)) → IF3(false, cons(x0, x1))
IF3(false, xs) → SORT(del(max(xs), 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)
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))
ge(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))
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
empty(nil)
empty(cons(x0, x1))
SORT(cons(x0, x1)) → IF3(false, cons(x0, x1))
IF3(false, xs) → SORT(del(max(xs), 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)
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))
ge(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(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
IF3(false, cons(z0, z1)) → SORT(del(max(cons(z0, z1)), cons(z0, z1))) → IF3(false, cons(z0, z1)) → SORT(del(max(cons(z0, z1)), cons(z0, z1)))
SORT(cons(x0, x1)) → IF3(false, cons(x0, x1))
IF3(false, cons(z0, z1)) → SORT(del(max(cons(z0, z1)), cons(z0, z1)))
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)
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))
ge(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(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
POL(0) = 1
POL(IF3(x1, x2)) = x2
POL(SORT(x1)) = x1
POL(cons(x1, x2)) = 1 + x1 + x2
POL(del(x1, x2)) = x2
POL(eq(x1, x2)) = 1 + x1 + x2
POL(false_renamed) = 0
POL(ge(x1, x2)) = 1
POL(if1(x1, x2, x3, x4)) = 1 + x2 + x3 + x4
POL(if2(x1, x2, x3, x4)) = 1 + x3 + x4
POL(max(x1)) = x1
POL(nil) = 1
POL(s(x1)) = x1
POL(true_renamed) = 1
proof of internal # AProVE Commit ID: 3a20a6ef7432c3f292db1a8838479c42bf5e3b22 root 20240618 unpublished Partial correctness of the following Program [x, v54, v55, v56, v57, v58, v59, v60, v61, v62, x3, x4, y1, xs1, x7, y4, xs2, x8, y5, x', y, xs, y2, x5, x6, y3, x9, x10, x11, y6, x'', y', x2, y'', xs', xs''] 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[a33](0, 0) -> true equal_sort[a33](0, s(v54)) -> false equal_sort[a33](s(v55), 0) -> false equal_sort[a33](s(v55), s(v56)) -> equal_sort[a33](v55, v56) equal_sort[a34](nil, nil) -> true equal_sort[a34](nil, cons(v57, v58)) -> false equal_sort[a34](cons(v59, v60), nil) -> false equal_sort[a34](cons(v59, v60), cons(v61, v62)) -> equal_sort[a33](v59, v61) and equal_sort[a34](v60, v62) equal_sort[a46](true_renamed, true_renamed) -> true equal_sort[a46](true_renamed, false_renamed) -> false equal_sort[a46](false_renamed, true_renamed) -> false equal_sort[a46](false_renamed, false_renamed) -> true equal_sort[a63](witness_sort[a63], witness_sort[a63]) -> true del'(x3, nil) -> false equal_sort[a46](eq(x4, y1), true_renamed) -> true | del'(x4, cons(y1, xs1)) -> true equal_sort[a46](eq(x4, y1), true_renamed) -> false | del'(x4, cons(y1, xs1)) -> del'(x4, xs1) if2'(true_renamed, x7, y4, xs2) -> true if2'(false_renamed, x8, y5, nil) -> false if2'(false_renamed, x8, y5, cons(y1, xs1)) -> if2'(eq(x8, y1), x8, y1, xs1) max(nil) -> 0 max(cons(x, nil)) -> x equal_sort[a46](ge(x', y), true_renamed) -> true | max(cons(x', cons(y, xs))) -> max(cons(x', xs)) equal_sort[a46](ge(x', y), true_renamed) -> false | max(cons(x', cons(y, xs))) -> max(cons(y, xs)) del(x3, nil) -> nil equal_sort[a46](eq(x4, y1), true_renamed) -> true | del(x4, cons(y1, xs1)) -> xs1 equal_sort[a46](eq(x4, y1), true_renamed) -> false | del(x4, cons(y1, xs1)) -> cons(y1, del(x4, xs1)) 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, xs2) -> xs2 if2(false_renamed, x8, y5, nil) -> cons(y5, nil) if2(false_renamed, x8, y5, cons(y1, xs1)) -> cons(y5, if2(eq(x8, y1), x8, y1, xs1)) ge(x9, 0) -> true_renamed ge(0, s(x10)) -> false_renamed ge(s(x11), s(y6)) -> ge(x11, y6) if1(true_renamed, x'', y', nil) -> x'' if1(true_renamed, x'', y', cons(y, xs)) -> if1(ge(x'', y), x'', 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, x'', y', xs') -> 0 if1(false_renamed, x2, y'', xs'') -> 0 using the following formula: z2:sort[a34].(~(z2=nil)->del'(max(z2), z2)=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) YES (6) Formula (7) Symbolic evaluation [EQUIVALENT, 0 ms] (8) Formula (9) Induction by data structure [EQUIVALENT, 0 ms] (10) AND (11) Formula (12) Symbolic evaluation [EQUIVALENT, 0 ms] (13) YES (14) Formula (15) Conditional Evaluation [EQUIVALENT, 0 ms] (16) AND (17) Formula (18) Symbolic evaluation [EQUIVALENT, 0 ms] (19) YES (20) Formula (21) Symbolic evaluation [EQUIVALENT, 0 ms] (22) Formula (23) Hypothesis Lifting [EQUIVALENT, 0 ms] (24) Formula (25) Symbolic evaluation under hypothesis [SOUND, 0 ms] (26) Formula (27) Hypothesis Lifting [EQUIVALENT, 0 ms] (28) Formula (29) Hypothesis Lifting [EQUIVALENT, 0 ms] (30) Formula (31) Conditional Evaluation [EQUIVALENT, 0 ms] (32) AND (33) Formula (34) Symbolic evaluation under hypothesis [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: z2:sort[a34].(~(z2=nil)->del'(max(z2), z2)=true) There are no hypotheses. ---------------------------------------- (1) Induction by algorithm (EQUIVALENT) Induction by algorithm max(z2) generates the following cases: 1. Base Case: Formula: (~(nil=nil)->del'(max(nil), nil)=true) There are no hypotheses. 2. Base Case: Formula: x:sort[a33].(~(cons(x, nil)=nil)->del'(max(cons(x, nil)), cons(x, nil))=true) There are no hypotheses. 1. Step Case: Formula: x':sort[a33],y:sort[a33],xs:sort[a34].(~(cons(x', cons(y, xs))=nil)->del'(max(cons(x', cons(y, xs))), cons(x', cons(y, xs)))=true) Hypotheses: x':sort[a33],xs:sort[a34].del'(max(cons(x', xs)), cons(x', xs))=true x':sort[a33],y:sort[a33].equal_sort[a46](ge(x', y), true_renamed)=true 2. Step Case: Formula: x':sort[a33],y:sort[a33],xs:sort[a34].(~(cons(x', cons(y, xs))=nil)->del'(max(cons(x', cons(y, xs))), cons(x', cons(y, xs)))=true) Hypotheses: y:sort[a33],xs:sort[a34].del'(max(cons(y, xs)), cons(y, xs))=true x':sort[a33],y:sort[a33].equal_sort[a46](ge(x', y), true_renamed)=false ---------------------------------------- (2) Complex Obligation (AND) ---------------------------------------- (3) Obligation: Formula: (~(nil=nil)->del'(max(nil), nil)=true) There are no hypotheses. ---------------------------------------- (4) Symbolic evaluation (EQUIVALENT) Could be reduced to the following new obligation by simple symbolic evaluation: True ---------------------------------------- (5) YES ---------------------------------------- (6) Obligation: Formula: x:sort[a33].(~(cons(x, nil)=nil)->del'(max(cons(x, nil)), cons(x, nil))=true) There are no hypotheses. ---------------------------------------- (7) Symbolic evaluation (EQUIVALENT) Could be shown by simple symbolic evaluation. ---------------------------------------- (8) Obligation: Formula: x:sort[a33].del'(x, cons(x, nil))=true There are no hypotheses. ---------------------------------------- (9) Induction by data structure (EQUIVALENT) Induction by data structure sort[a33] generates the following cases: 1. Base Case: Formula: del'(0, cons(0, nil))=true There are no hypotheses. 1. Step Case: Formula: n:sort[a33].del'(s(n), cons(s(n), nil))=true Hypotheses: n:sort[a33].del'(n, cons(n, nil))=true ---------------------------------------- (10) Complex Obligation (AND) ---------------------------------------- (11) Obligation: Formula: del'(0, cons(0, nil))=true There are no hypotheses. ---------------------------------------- (12) Symbolic evaluation (EQUIVALENT) Could be reduced to the following new obligation by simple symbolic evaluation: True ---------------------------------------- (13) YES ---------------------------------------- (14) Obligation: Formula: n:sort[a33].del'(s(n), cons(s(n), nil))=true Hypotheses: n:sort[a33].del'(n, cons(n, nil))=true ---------------------------------------- (15) Conditional Evaluation (EQUIVALENT) The formula could be reduced to the following new obligations by conditional evaluation: Formula: true=true Hypotheses: n:sort[a33].del'(n, cons(n, nil))=true n:sort[a33].equal_sort[a46](eq(s(n), s(n)), true_renamed)=true Formula: n:sort[a33].del'(s(n), nil)=true Hypotheses: n:sort[a33].del'(n, cons(n, nil))=true n:sort[a33].equal_sort[a46](eq(s(n), s(n)), true_renamed)=false ---------------------------------------- (16) Complex Obligation (AND) ---------------------------------------- (17) Obligation: Formula: true=true Hypotheses: n:sort[a33].del'(n, cons(n, nil))=true n:sort[a33].equal_sort[a46](eq(s(n), s(n)), true_renamed)=true ---------------------------------------- (18) Symbolic evaluation (EQUIVALENT) Could be reduced to the following new obligation by simple symbolic evaluation: True ---------------------------------------- (19) YES ---------------------------------------- (20) Obligation: Formula: n:sort[a33].del'(s(n), nil)=true Hypotheses: n:sort[a33].del'(n, cons(n, nil))=true n:sort[a33].equal_sort[a46](eq(s(n), s(n)), true_renamed)=false ---------------------------------------- (21) Symbolic evaluation (EQUIVALENT) Could be shown by simple symbolic evaluation. ---------------------------------------- (22) Obligation: Formula: False Hypotheses: n:sort[a33].del'(n, cons(n, nil))=true n:sort[a33].equal_sort[a46](eq(s(n), s(n)), true_renamed)=false ---------------------------------------- (23) Hypothesis Lifting (EQUIVALENT) Formula could be generalised by hypothesis lifting to the following new obligation: Formula: n:sort[a33].((del'(n, cons(n, nil))=true/\equal_sort[a46](eq(s(n), s(n)), true_renamed)=false)->False) Hypotheses: n:sort[a33].del'(n, cons(n, nil))=true n:sort[a33].equal_sort[a46](eq(s(n), s(n)), true_renamed)=false ---------------------------------------- (24) Obligation: Formula: n:sort[a33].((del'(n, cons(n, nil))=true/\equal_sort[a46](eq(s(n), s(n)), true_renamed)=false)->False) Hypotheses: n:sort[a33].del'(n, cons(n, nil))=true n:sort[a33].equal_sort[a46](eq(s(n), s(n)), true_renamed)=false ---------------------------------------- (25) Symbolic evaluation under hypothesis (SOUND) Could be reduced by symbolic evaluation under hypothesis to: n:sort[a33].~(equal_sort[a46](eq(n, n), true_renamed)=false) By using the following hypotheses: n:sort[a33].del'(n, cons(n, nil))=true ---------------------------------------- (26) Obligation: Formula: n:sort[a33].~(equal_sort[a46](eq(n, n), true_renamed)=false) Hypotheses: n:sort[a33].del'(n, cons(n, nil))=true n:sort[a33].equal_sort[a46](eq(s(n), s(n)), true_renamed)=false ---------------------------------------- (27) Hypothesis Lifting (EQUIVALENT) Formula could be generalised by hypothesis lifting to the following new obligation: Formula: n:sort[a33].(equal_sort[a46](eq(n, n), true_renamed)=false->~(equal_sort[a46](eq(n, n), true_renamed)=false)) Hypotheses: n:sort[a33].del'(n, cons(n, nil))=true ---------------------------------------- (28) Obligation: Formula: n:sort[a33].(equal_sort[a46](eq(n, n), true_renamed)=false->~(equal_sort[a46](eq(n, n), true_renamed)=false)) Hypotheses: n:sort[a33].del'(n, cons(n, nil))=true ---------------------------------------- (29) Hypothesis Lifting (EQUIVALENT) Formula could be generalised by hypothesis lifting to the following new obligation: Formula: n:sort[a33].(del'(n, cons(n, nil))=true->(equal_sort[a46](eq(n, n), true_renamed)=false->~(equal_sort[a46](eq(n, n), true_renamed)=false))) There are no hypotheses. ---------------------------------------- (30) Obligation: Formula: n:sort[a33].(del'(n, cons(n, nil))=true->(equal_sort[a46](eq(n, n), true_renamed)=false->~(equal_sort[a46](eq(n, n), true_renamed)=false))) There are no hypotheses. ---------------------------------------- (31) Conditional Evaluation (EQUIVALENT) The formula could be reduced to the following new obligations by conditional evaluation: Formula: n:sort[a33].(true=true->(equal_sort[a46](eq(n, n), true_renamed)=false->~(equal_sort[a46](eq(n, n), true_renamed)=false))) Hypotheses: n:sort[a33].equal_sort[a46](eq(n, n), true_renamed)=true Formula: n:sort[a33].(del'(n, nil)=true->(equal_sort[a46](eq(n, n), true_renamed)=false->~(equal_sort[a46](eq(n, n), true_renamed)=false))) Hypotheses: n:sort[a33].equal_sort[a46](eq(n, n), true_renamed)=false ---------------------------------------- (32) Complex Obligation (AND) ---------------------------------------- (33) Obligation: Formula: n:sort[a33].(true=true->(equal_sort[a46](eq(n, n), true_renamed)=false->~(equal_sort[a46](eq(n, n), true_renamed)=false))) Hypotheses: n:sort[a33].equal_sort[a46](eq(n, n), true_renamed)=true ---------------------------------------- (34) Symbolic evaluation under hypothesis (EQUIVALENT) Could be shown using symbolic evaluation under hypothesis, by using the following hypotheses: n:sort[a33].equal_sort[a46](eq(n, n), true_renamed)=true ---------------------------------------- (35) YES ---------------------------------------- (36) Obligation: Formula: n:sort[a33].(del'(n, nil)=true->(equal_sort[a46](eq(n, n), true_renamed)=false->~(equal_sort[a46](eq(n, n), true_renamed)=false))) Hypotheses: n:sort[a33].equal_sort[a46](eq(n, n), true_renamed)=false ---------------------------------------- (37) Symbolic evaluation (EQUIVALENT) Could be reduced to the following new obligation by simple symbolic evaluation: True ---------------------------------------- (38) YES ---------------------------------------- (39) Obligation: Formula: x':sort[a33],y:sort[a33],xs:sort[a34].(~(cons(x', cons(y, xs))=nil)->del'(max(cons(x', cons(y, xs))), cons(x', cons(y, xs)))=true) Hypotheses: x':sort[a33],xs:sort[a34].del'(max(cons(x', xs)), cons(x', xs))=true x':sort[a33],y:sort[a33].equal_sort[a46](ge(x', y), true_renamed)=true ---------------------------------------- (40) Symbolic evaluation (EQUIVALENT) Could be shown by simple symbolic evaluation. ---------------------------------------- (41) Obligation: Formula: x':sort[a33],y:sort[a33],xs:sort[a34].del'(max(cons(x', cons(y, xs))), cons(x', cons(y, xs)))=true Hypotheses: x':sort[a33],xs:sort[a34].del'(max(cons(x', xs)), cons(x', xs))=true x':sort[a33],y:sort[a33].equal_sort[a46](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[a33],xs:sort[a34],y:sort[a33].del'(max(cons(x', xs)), cons(x', cons(y, xs)))=true Hypotheses: x':sort[a33],xs:sort[a34].del'(max(cons(x', xs)), cons(x', xs))=true x':sort[a33],y:sort[a33].equal_sort[a46](ge(x', y), true_renamed)=true ---------------------------------------- (43) Obligation: Formula: x':sort[a33],xs:sort[a34],y:sort[a33].del'(max(cons(x', xs)), cons(x', cons(y, xs)))=true Hypotheses: x':sort[a33],xs:sort[a34].del'(max(cons(x', xs)), cons(x', xs))=true x':sort[a33],y:sort[a33].equal_sort[a46](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[a33],xs:sort[a34].del'(max(cons(x', xs)), cons(x', xs))=true x':sort[a33],y:sort[a33].equal_sort[a46](ge(x', y), true_renamed)=true x':sort[a33],xs:sort[a34].equal_sort[a46](eq(max(cons(x', xs)), x'), true_renamed)=true Formula: x':sort[a33],xs:sort[a34],y:sort[a33].del'(max(cons(x', xs)), cons(y, xs))=true Hypotheses: x':sort[a33],xs:sort[a34].del'(max(cons(x', xs)), cons(x', xs))=true x':sort[a33],y:sort[a33].equal_sort[a46](ge(x', y), true_renamed)=true x':sort[a33],xs:sort[a34].equal_sort[a46](eq(max(cons(x', xs)), x'), true_renamed)=false ---------------------------------------- (45) Complex Obligation (AND) ---------------------------------------- (46) Obligation: Formula: true=true Hypotheses: x':sort[a33],xs:sort[a34].del'(max(cons(x', xs)), cons(x', xs))=true x':sort[a33],y:sort[a33].equal_sort[a46](ge(x', y), true_renamed)=true x':sort[a33],xs:sort[a34].equal_sort[a46](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[a33],xs:sort[a34],y:sort[a33].del'(max(cons(x', xs)), cons(y, xs))=true Hypotheses: x':sort[a33],xs:sort[a34].del'(max(cons(x', xs)), cons(x', xs))=true x':sort[a33],y:sort[a33].equal_sort[a46](ge(x', y), true_renamed)=true x':sort[a33],xs:sort[a34].equal_sort[a46](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[a33],xs:sort[a34].del'(max(cons(x', xs)), cons(x', xs))=true x':sort[a33],y:sort[a33].equal_sort[a46](ge(x', y), true_renamed)=true x':sort[a33],xs:sort[a34].equal_sort[a46](eq(max(cons(x', xs)), x'), true_renamed)=false x':sort[a33],xs:sort[a34],y:sort[a33].equal_sort[a46](eq(max(cons(x', xs)), y), true_renamed)=true Formula: x':sort[a33],xs:sort[a34].del'(max(cons(x', xs)), xs)=true Hypotheses: x':sort[a33],xs:sort[a34].del'(max(cons(x', xs)), cons(x', xs))=true x':sort[a33],y:sort[a33].equal_sort[a46](ge(x', y), true_renamed)=true x':sort[a33],xs:sort[a34].equal_sort[a46](eq(max(cons(x', xs)), x'), true_renamed)=false x':sort[a33],xs:sort[a34],y:sort[a33].equal_sort[a46](eq(max(cons(x', xs)), y), true_renamed)=false ---------------------------------------- (51) Complex Obligation (AND) ---------------------------------------- (52) Obligation: Formula: true=true Hypotheses: x':sort[a33],xs:sort[a34].del'(max(cons(x', xs)), cons(x', xs))=true x':sort[a33],y:sort[a33].equal_sort[a46](ge(x', y), true_renamed)=true x':sort[a33],xs:sort[a34].equal_sort[a46](eq(max(cons(x', xs)), x'), true_renamed)=false x':sort[a33],xs:sort[a34],y:sort[a33].equal_sort[a46](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[a33],xs:sort[a34].del'(max(cons(x', xs)), xs)=true Hypotheses: x':sort[a33],xs:sort[a34].del'(max(cons(x', xs)), cons(x', xs))=true x':sort[a33],y:sort[a33].equal_sort[a46](ge(x', y), true_renamed)=true x':sort[a33],xs:sort[a34].equal_sort[a46](eq(max(cons(x', xs)), x'), true_renamed)=false x':sort[a33],xs:sort[a34],y:sort[a33].equal_sort[a46](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[a33],xs:sort[a34].(del'(max(cons(x', xs)), cons(x', xs))=true->del'(max(cons(x', xs)), xs)=true) Hypotheses: x':sort[a33],y:sort[a33].equal_sort[a46](ge(x', y), true_renamed)=true x':sort[a33],xs:sort[a34].equal_sort[a46](eq(max(cons(x', xs)), x'), true_renamed)=false x':sort[a33],xs:sort[a34],y:sort[a33].equal_sort[a46](eq(max(cons(x', xs)), y), true_renamed)=false ---------------------------------------- (57) Obligation: Formula: x':sort[a33],xs:sort[a34].(del'(max(cons(x', xs)), cons(x', xs))=true->del'(max(cons(x', xs)), xs)=true) Hypotheses: x':sort[a33],y:sort[a33].equal_sort[a46](ge(x', y), true_renamed)=true x':sort[a33],xs:sort[a34].equal_sort[a46](eq(max(cons(x', xs)), x'), true_renamed)=false x':sort[a33],xs:sort[a34],y:sort[a33].equal_sort[a46](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[a33],xs:sort[a34].(del'(max(cons(x', xs)), xs)=true->del'(max(cons(x', xs)), xs)=true) Hypotheses: x':sort[a33],y:sort[a33].equal_sort[a46](ge(x', y), true_renamed)=true x':sort[a33],xs:sort[a34].equal_sort[a46](eq(max(cons(x', xs)), x'), true_renamed)=false x':sort[a33],xs:sort[a34],y:sort[a33].equal_sort[a46](eq(max(cons(x', xs)), y), true_renamed)=false ---------------------------------------- (59) Obligation: Formula: x':sort[a33],xs:sort[a34].(del'(max(cons(x', xs)), xs)=true->del'(max(cons(x', xs)), xs)=true) Hypotheses: x':sort[a33],y:sort[a33].equal_sort[a46](ge(x', y), true_renamed)=true x':sort[a33],xs:sort[a34].equal_sort[a46](eq(max(cons(x', xs)), x'), true_renamed)=false x':sort[a33],xs:sort[a34],y:sort[a33].equal_sort[a46](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[a33],y:sort[a33],xs:sort[a34].(~(cons(x', cons(y, xs))=nil)->del'(max(cons(x', cons(y, xs))), cons(x', cons(y, xs)))=true) Hypotheses: y:sort[a33],xs:sort[a34].del'(max(cons(y, xs)), cons(y, xs))=true x':sort[a33],y:sort[a33].equal_sort[a46](ge(x', y), true_renamed)=false ---------------------------------------- (63) Symbolic evaluation (EQUIVALENT) Could be shown by simple symbolic evaluation. ---------------------------------------- (64) Obligation: Formula: x':sort[a33],y:sort[a33],xs:sort[a34].del'(max(cons(x', cons(y, xs))), cons(x', cons(y, xs)))=true Hypotheses: y:sort[a33],xs:sort[a34].del'(max(cons(y, xs)), cons(y, xs))=true x':sort[a33],y:sort[a33].equal_sort[a46](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[a33],xs:sort[a34],x':sort[a33].del'(max(cons(y, xs)), cons(x', cons(y, xs)))=true Hypotheses: y:sort[a33],xs:sort[a34].del'(max(cons(y, xs)), cons(y, xs))=true x':sort[a33],y:sort[a33].equal_sort[a46](ge(x', y), true_renamed)=false ---------------------------------------- (66) Obligation: Formula: y:sort[a33],xs:sort[a34],x':sort[a33].del'(max(cons(y, xs)), cons(x', cons(y, xs)))=true Hypotheses: y:sort[a33],xs:sort[a34].del'(max(cons(y, xs)), cons(y, xs))=true x':sort[a33],y:sort[a33].equal_sort[a46](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[a33],xs:sort[a34].del'(max(cons(y, xs)), cons(y, xs))=true x':sort[a33],y:sort[a33].equal_sort[a46](ge(x', y), true_renamed)=false y:sort[a33],xs:sort[a34],x':sort[a33].equal_sort[a46](eq(max(cons(y, xs)), x'), true_renamed)=true Formula: y:sort[a33],xs:sort[a34].del'(max(cons(y, xs)), cons(y, xs))=true Hypotheses: y:sort[a33],xs:sort[a34].del'(max(cons(y, xs)), cons(y, xs))=true x':sort[a33],y:sort[a33].equal_sort[a46](ge(x', y), true_renamed)=false y:sort[a33],xs:sort[a34],x':sort[a33].equal_sort[a46](eq(max(cons(y, xs)), x'), true_renamed)=false ---------------------------------------- (68) Complex Obligation (AND) ---------------------------------------- (69) Obligation: Formula: true=true Hypotheses: y:sort[a33],xs:sort[a34].del'(max(cons(y, xs)), cons(y, xs))=true x':sort[a33],y:sort[a33].equal_sort[a46](ge(x', y), true_renamed)=false y:sort[a33],xs:sort[a34],x':sort[a33].equal_sort[a46](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[a33],xs:sort[a34].del'(max(cons(y, xs)), cons(y, xs))=true Hypotheses: y:sort[a33],xs:sort[a34].del'(max(cons(y, xs)), cons(y, xs))=true x':sort[a33],y:sort[a33].equal_sort[a46](ge(x', y), true_renamed)=false y:sort[a33],xs:sort[a34],x':sort[a33].equal_sort[a46](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[a33],xs:sort[a34].del'(max(cons(y, xs)), cons(y, xs))=true ---------------------------------------- (74) YES
SORT(cons(x0, x1)) → IF3(false, cons(x0, x1))
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)
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))
ge(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(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
del'(x3, nil) → false
del'(x4, cons(y1, xs1)) → if2'(eq(x4, y1), x4, y1, xs1)
if2'(true_renamed, x7, y4, xs2) → true
if2'(false_renamed, x8, y5, xs3) → del'(x8, xs3)
max(nil) → 0
max(cons(x, nil)) → x
max(cons(x', cons(y, xs))) → if1(ge(x', y), x', y, xs)
if1(true_renamed, x'', y', xs') → max(cons(x'', xs'))
if1(false_renamed, x2, y'', xs'') → max(cons(y'', xs''))
del(x3, nil) → nil
del(x4, cons(y1, xs1)) → if2(eq(x4, y1), x4, y1, xs1)
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, xs2) → xs2
if2(false_renamed, x8, y5, xs3) → cons(y5, del(x8, xs3))
ge(x9, 0) → true_renamed
ge(0, s(x10)) → false_renamed
ge(s(x11), s(y6)) → ge(x11, y6)
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[a33](0, 0) → true
equal_sort[a33](0, s(v54)) → false
equal_sort[a33](s(v55), 0) → false
equal_sort[a33](s(v55), s(v56)) → equal_sort[a33](v55, v56)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(v57, v58)) → false
equal_sort[a34](cons(v59, v60), nil) → false
equal_sort[a34](cons(v59, v60), cons(v61, v62)) → and(equal_sort[a33](v59, v61), equal_sort[a34](v60, v62))
equal_sort[a46](true_renamed, true_renamed) → true
equal_sort[a46](true_renamed, false_renamed) → false
equal_sort[a46](false_renamed, true_renamed) → false
equal_sort[a46](false_renamed, false_renamed) → true
equal_sort[a63](witness_sort[a63], witness_sort[a63]) → true
del'(x3, nil) → false
del'(x4, cons(y1, xs1)) → if2'(eq(x4, y1), x4, y1, xs1)
if2'(true_renamed, x7, y4, xs2) → true
if2'(false_renamed, x8, y5, xs3) → del'(x8, xs3)
max(nil) → 0
max(cons(x, nil)) → x
max(cons(x', cons(y, xs))) → if1(ge(x', y), x', y, xs)
if1(true_renamed, x'', y', xs') → max(cons(x'', xs'))
if1(false_renamed, x2, y'', xs'') → max(cons(y'', xs''))
del(x3, nil) → nil
del(x4, cons(y1, xs1)) → if2(eq(x4, y1), x4, y1, xs1)
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, xs2) → xs2
if2(false_renamed, x8, y5, xs3) → cons(y5, del(x8, xs3))
ge(x9, 0) → true_renamed
ge(0, s(x10)) → false_renamed
ge(s(x11), s(y6)) → ge(x11, y6)
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[a33](0, 0) → true
equal_sort[a33](0, s(v54)) → false
equal_sort[a33](s(v55), 0) → false
equal_sort[a33](s(v55), s(v56)) → equal_sort[a33](v55, v56)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(v57, v58)) → false
equal_sort[a34](cons(v59, v60), nil) → false
equal_sort[a34](cons(v59, v60), cons(v61, v62)) → and(equal_sort[a33](v59, v61), equal_sort[a34](v60, v62))
equal_sort[a46](true_renamed, true_renamed) → true
equal_sort[a46](true_renamed, false_renamed) → false
equal_sort[a46](false_renamed, true_renamed) → false
equal_sort[a46](false_renamed, false_renamed) → true
equal_sort[a63](witness_sort[a63], witness_sort[a63]) → true
del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
max(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, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true_renamed, x0, x1, x2)
if2(false_renamed, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a46](true_renamed, true_renamed)
equal_sort[a46](true_renamed, false_renamed)
equal_sort[a46](false_renamed, true_renamed)
equal_sort[a46](false_renamed, false_renamed)
equal_sort[a63](witness_sort[a63], witness_sort[a63])
DEL'(x4, cons(y1, xs1)) → IF2'(eq(x4, y1), x4, y1, xs1)
DEL'(x4, cons(y1, xs1)) → EQ(x4, y1)
IF2'(false_renamed, x8, y5, xs3) → DEL'(x8, xs3)
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, x'', y', xs') → MAX(cons(x'', xs'))
IF1(false_renamed, x2, y'', xs'') → MAX(cons(y'', xs''))
DEL(x4, cons(y1, xs1)) → IF2(eq(x4, y1), x4, y1, xs1)
DEL(x4, cons(y1, xs1)) → EQ(x4, y1)
EQ(s(x6), s(y3)) → EQ(x6, y3)
IF2(false_renamed, x8, y5, xs3) → DEL(x8, xs3)
GE(s(x11), s(y6)) → GE(x11, y6)
EQUAL_SORT[A33](s(v55), s(v56)) → EQUAL_SORT[A33](v55, v56)
EQUAL_SORT[A34](cons(v59, v60), cons(v61, v62)) → AND(equal_sort[a33](v59, v61), equal_sort[a34](v60, v62))
EQUAL_SORT[A34](cons(v59, v60), cons(v61, v62)) → EQUAL_SORT[A33](v59, v61)
EQUAL_SORT[A34](cons(v59, v60), cons(v61, v62)) → EQUAL_SORT[A34](v60, v62)
del'(x3, nil) → false
del'(x4, cons(y1, xs1)) → if2'(eq(x4, y1), x4, y1, xs1)
if2'(true_renamed, x7, y4, xs2) → true
if2'(false_renamed, x8, y5, xs3) → del'(x8, xs3)
max(nil) → 0
max(cons(x, nil)) → x
max(cons(x', cons(y, xs))) → if1(ge(x', y), x', y, xs)
if1(true_renamed, x'', y', xs') → max(cons(x'', xs'))
if1(false_renamed, x2, y'', xs'') → max(cons(y'', xs''))
del(x3, nil) → nil
del(x4, cons(y1, xs1)) → if2(eq(x4, y1), x4, y1, xs1)
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, xs2) → xs2
if2(false_renamed, x8, y5, xs3) → cons(y5, del(x8, xs3))
ge(x9, 0) → true_renamed
ge(0, s(x10)) → false_renamed
ge(s(x11), s(y6)) → ge(x11, y6)
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[a33](0, 0) → true
equal_sort[a33](0, s(v54)) → false
equal_sort[a33](s(v55), 0) → false
equal_sort[a33](s(v55), s(v56)) → equal_sort[a33](v55, v56)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(v57, v58)) → false
equal_sort[a34](cons(v59, v60), nil) → false
equal_sort[a34](cons(v59, v60), cons(v61, v62)) → and(equal_sort[a33](v59, v61), equal_sort[a34](v60, v62))
equal_sort[a46](true_renamed, true_renamed) → true
equal_sort[a46](true_renamed, false_renamed) → false
equal_sort[a46](false_renamed, true_renamed) → false
equal_sort[a46](false_renamed, false_renamed) → true
equal_sort[a63](witness_sort[a63], witness_sort[a63]) → true
del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
max(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, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true_renamed, x0, x1, x2)
if2(false_renamed, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a46](true_renamed, true_renamed)
equal_sort[a46](true_renamed, false_renamed)
equal_sort[a46](false_renamed, true_renamed)
equal_sort[a46](false_renamed, false_renamed)
equal_sort[a63](witness_sort[a63], witness_sort[a63])
EQUAL_SORT[A33](s(v55), s(v56)) → EQUAL_SORT[A33](v55, v56)
del'(x3, nil) → false
del'(x4, cons(y1, xs1)) → if2'(eq(x4, y1), x4, y1, xs1)
if2'(true_renamed, x7, y4, xs2) → true
if2'(false_renamed, x8, y5, xs3) → del'(x8, xs3)
max(nil) → 0
max(cons(x, nil)) → x
max(cons(x', cons(y, xs))) → if1(ge(x', y), x', y, xs)
if1(true_renamed, x'', y', xs') → max(cons(x'', xs'))
if1(false_renamed, x2, y'', xs'') → max(cons(y'', xs''))
del(x3, nil) → nil
del(x4, cons(y1, xs1)) → if2(eq(x4, y1), x4, y1, xs1)
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, xs2) → xs2
if2(false_renamed, x8, y5, xs3) → cons(y5, del(x8, xs3))
ge(x9, 0) → true_renamed
ge(0, s(x10)) → false_renamed
ge(s(x11), s(y6)) → ge(x11, y6)
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[a33](0, 0) → true
equal_sort[a33](0, s(v54)) → false
equal_sort[a33](s(v55), 0) → false
equal_sort[a33](s(v55), s(v56)) → equal_sort[a33](v55, v56)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(v57, v58)) → false
equal_sort[a34](cons(v59, v60), nil) → false
equal_sort[a34](cons(v59, v60), cons(v61, v62)) → and(equal_sort[a33](v59, v61), equal_sort[a34](v60, v62))
equal_sort[a46](true_renamed, true_renamed) → true
equal_sort[a46](true_renamed, false_renamed) → false
equal_sort[a46](false_renamed, true_renamed) → false
equal_sort[a46](false_renamed, false_renamed) → true
equal_sort[a63](witness_sort[a63], witness_sort[a63]) → true
del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
max(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, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true_renamed, x0, x1, x2)
if2(false_renamed, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a46](true_renamed, true_renamed)
equal_sort[a46](true_renamed, false_renamed)
equal_sort[a46](false_renamed, true_renamed)
equal_sort[a46](false_renamed, false_renamed)
equal_sort[a63](witness_sort[a63], witness_sort[a63])
EQUAL_SORT[A33](s(v55), s(v56)) → EQUAL_SORT[A33](v55, v56)
del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
max(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, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true_renamed, x0, x1, x2)
if2(false_renamed, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a46](true_renamed, true_renamed)
equal_sort[a46](true_renamed, false_renamed)
equal_sort[a46](false_renamed, true_renamed)
equal_sort[a46](false_renamed, false_renamed)
equal_sort[a63](witness_sort[a63], witness_sort[a63])
del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
max(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, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true_renamed, x0, x1, x2)
if2(false_renamed, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a46](true_renamed, true_renamed)
equal_sort[a46](true_renamed, false_renamed)
equal_sort[a46](false_renamed, true_renamed)
equal_sort[a46](false_renamed, false_renamed)
equal_sort[a63](witness_sort[a63], witness_sort[a63])
EQUAL_SORT[A33](s(v55), s(v56)) → EQUAL_SORT[A33](v55, v56)
From the DPs we obtained the following set of size-change graphs:
EQUAL_SORT[A34](cons(v59, v60), cons(v61, v62)) → EQUAL_SORT[A34](v60, v62)
del'(x3, nil) → false
del'(x4, cons(y1, xs1)) → if2'(eq(x4, y1), x4, y1, xs1)
if2'(true_renamed, x7, y4, xs2) → true
if2'(false_renamed, x8, y5, xs3) → del'(x8, xs3)
max(nil) → 0
max(cons(x, nil)) → x
max(cons(x', cons(y, xs))) → if1(ge(x', y), x', y, xs)
if1(true_renamed, x'', y', xs') → max(cons(x'', xs'))
if1(false_renamed, x2, y'', xs'') → max(cons(y'', xs''))
del(x3, nil) → nil
del(x4, cons(y1, xs1)) → if2(eq(x4, y1), x4, y1, xs1)
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, xs2) → xs2
if2(false_renamed, x8, y5, xs3) → cons(y5, del(x8, xs3))
ge(x9, 0) → true_renamed
ge(0, s(x10)) → false_renamed
ge(s(x11), s(y6)) → ge(x11, y6)
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[a33](0, 0) → true
equal_sort[a33](0, s(v54)) → false
equal_sort[a33](s(v55), 0) → false
equal_sort[a33](s(v55), s(v56)) → equal_sort[a33](v55, v56)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(v57, v58)) → false
equal_sort[a34](cons(v59, v60), nil) → false
equal_sort[a34](cons(v59, v60), cons(v61, v62)) → and(equal_sort[a33](v59, v61), equal_sort[a34](v60, v62))
equal_sort[a46](true_renamed, true_renamed) → true
equal_sort[a46](true_renamed, false_renamed) → false
equal_sort[a46](false_renamed, true_renamed) → false
equal_sort[a46](false_renamed, false_renamed) → true
equal_sort[a63](witness_sort[a63], witness_sort[a63]) → true
del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
max(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, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true_renamed, x0, x1, x2)
if2(false_renamed, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a46](true_renamed, true_renamed)
equal_sort[a46](true_renamed, false_renamed)
equal_sort[a46](false_renamed, true_renamed)
equal_sort[a46](false_renamed, false_renamed)
equal_sort[a63](witness_sort[a63], witness_sort[a63])
EQUAL_SORT[A34](cons(v59, v60), cons(v61, v62)) → EQUAL_SORT[A34](v60, v62)
del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
max(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, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true_renamed, x0, x1, x2)
if2(false_renamed, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a46](true_renamed, true_renamed)
equal_sort[a46](true_renamed, false_renamed)
equal_sort[a46](false_renamed, true_renamed)
equal_sort[a46](false_renamed, false_renamed)
equal_sort[a63](witness_sort[a63], witness_sort[a63])
del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
max(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, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true_renamed, x0, x1, x2)
if2(false_renamed, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a46](true_renamed, true_renamed)
equal_sort[a46](true_renamed, false_renamed)
equal_sort[a46](false_renamed, true_renamed)
equal_sort[a46](false_renamed, false_renamed)
equal_sort[a63](witness_sort[a63], witness_sort[a63])
EQUAL_SORT[A34](cons(v59, v60), cons(v61, v62)) → EQUAL_SORT[A34](v60, v62)
From the DPs we obtained the following set of size-change graphs:
GE(s(x11), s(y6)) → GE(x11, y6)
del'(x3, nil) → false
del'(x4, cons(y1, xs1)) → if2'(eq(x4, y1), x4, y1, xs1)
if2'(true_renamed, x7, y4, xs2) → true
if2'(false_renamed, x8, y5, xs3) → del'(x8, xs3)
max(nil) → 0
max(cons(x, nil)) → x
max(cons(x', cons(y, xs))) → if1(ge(x', y), x', y, xs)
if1(true_renamed, x'', y', xs') → max(cons(x'', xs'))
if1(false_renamed, x2, y'', xs'') → max(cons(y'', xs''))
del(x3, nil) → nil
del(x4, cons(y1, xs1)) → if2(eq(x4, y1), x4, y1, xs1)
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, xs2) → xs2
if2(false_renamed, x8, y5, xs3) → cons(y5, del(x8, xs3))
ge(x9, 0) → true_renamed
ge(0, s(x10)) → false_renamed
ge(s(x11), s(y6)) → ge(x11, y6)
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[a33](0, 0) → true
equal_sort[a33](0, s(v54)) → false
equal_sort[a33](s(v55), 0) → false
equal_sort[a33](s(v55), s(v56)) → equal_sort[a33](v55, v56)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(v57, v58)) → false
equal_sort[a34](cons(v59, v60), nil) → false
equal_sort[a34](cons(v59, v60), cons(v61, v62)) → and(equal_sort[a33](v59, v61), equal_sort[a34](v60, v62))
equal_sort[a46](true_renamed, true_renamed) → true
equal_sort[a46](true_renamed, false_renamed) → false
equal_sort[a46](false_renamed, true_renamed) → false
equal_sort[a46](false_renamed, false_renamed) → true
equal_sort[a63](witness_sort[a63], witness_sort[a63]) → true
del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
max(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, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true_renamed, x0, x1, x2)
if2(false_renamed, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a46](true_renamed, true_renamed)
equal_sort[a46](true_renamed, false_renamed)
equal_sort[a46](false_renamed, true_renamed)
equal_sort[a46](false_renamed, false_renamed)
equal_sort[a63](witness_sort[a63], witness_sort[a63])
GE(s(x11), s(y6)) → GE(x11, y6)
del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
max(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, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true_renamed, x0, x1, x2)
if2(false_renamed, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a46](true_renamed, true_renamed)
equal_sort[a46](true_renamed, false_renamed)
equal_sort[a46](false_renamed, true_renamed)
equal_sort[a46](false_renamed, false_renamed)
equal_sort[a63](witness_sort[a63], witness_sort[a63])
del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
max(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, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true_renamed, x0, x1, x2)
if2(false_renamed, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a46](true_renamed, true_renamed)
equal_sort[a46](true_renamed, false_renamed)
equal_sort[a46](false_renamed, true_renamed)
equal_sort[a46](false_renamed, false_renamed)
equal_sort[a63](witness_sort[a63], witness_sort[a63])
GE(s(x11), s(y6)) → GE(x11, y6)
From the DPs we obtained the following set of size-change graphs:
EQ(s(x6), s(y3)) → EQ(x6, y3)
del'(x3, nil) → false
del'(x4, cons(y1, xs1)) → if2'(eq(x4, y1), x4, y1, xs1)
if2'(true_renamed, x7, y4, xs2) → true
if2'(false_renamed, x8, y5, xs3) → del'(x8, xs3)
max(nil) → 0
max(cons(x, nil)) → x
max(cons(x', cons(y, xs))) → if1(ge(x', y), x', y, xs)
if1(true_renamed, x'', y', xs') → max(cons(x'', xs'))
if1(false_renamed, x2, y'', xs'') → max(cons(y'', xs''))
del(x3, nil) → nil
del(x4, cons(y1, xs1)) → if2(eq(x4, y1), x4, y1, xs1)
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, xs2) → xs2
if2(false_renamed, x8, y5, xs3) → cons(y5, del(x8, xs3))
ge(x9, 0) → true_renamed
ge(0, s(x10)) → false_renamed
ge(s(x11), s(y6)) → ge(x11, y6)
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[a33](0, 0) → true
equal_sort[a33](0, s(v54)) → false
equal_sort[a33](s(v55), 0) → false
equal_sort[a33](s(v55), s(v56)) → equal_sort[a33](v55, v56)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(v57, v58)) → false
equal_sort[a34](cons(v59, v60), nil) → false
equal_sort[a34](cons(v59, v60), cons(v61, v62)) → and(equal_sort[a33](v59, v61), equal_sort[a34](v60, v62))
equal_sort[a46](true_renamed, true_renamed) → true
equal_sort[a46](true_renamed, false_renamed) → false
equal_sort[a46](false_renamed, true_renamed) → false
equal_sort[a46](false_renamed, false_renamed) → true
equal_sort[a63](witness_sort[a63], witness_sort[a63]) → true
del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
max(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, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true_renamed, x0, x1, x2)
if2(false_renamed, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a46](true_renamed, true_renamed)
equal_sort[a46](true_renamed, false_renamed)
equal_sort[a46](false_renamed, true_renamed)
equal_sort[a46](false_renamed, false_renamed)
equal_sort[a63](witness_sort[a63], witness_sort[a63])
EQ(s(x6), s(y3)) → EQ(x6, y3)
del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
max(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, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true_renamed, x0, x1, x2)
if2(false_renamed, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a46](true_renamed, true_renamed)
equal_sort[a46](true_renamed, false_renamed)
equal_sort[a46](false_renamed, true_renamed)
equal_sort[a46](false_renamed, false_renamed)
equal_sort[a63](witness_sort[a63], witness_sort[a63])
del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
max(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, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true_renamed, x0, x1, x2)
if2(false_renamed, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a46](true_renamed, true_renamed)
equal_sort[a46](true_renamed, false_renamed)
equal_sort[a46](false_renamed, true_renamed)
equal_sort[a46](false_renamed, false_renamed)
equal_sort[a63](witness_sort[a63], witness_sort[a63])
EQ(s(x6), s(y3)) → EQ(x6, y3)
From the DPs we obtained the following set of size-change graphs:
IF2(false_renamed, x8, y5, xs3) → DEL(x8, xs3)
DEL(x4, cons(y1, xs1)) → IF2(eq(x4, y1), x4, y1, xs1)
del'(x3, nil) → false
del'(x4, cons(y1, xs1)) → if2'(eq(x4, y1), x4, y1, xs1)
if2'(true_renamed, x7, y4, xs2) → true
if2'(false_renamed, x8, y5, xs3) → del'(x8, xs3)
max(nil) → 0
max(cons(x, nil)) → x
max(cons(x', cons(y, xs))) → if1(ge(x', y), x', y, xs)
if1(true_renamed, x'', y', xs') → max(cons(x'', xs'))
if1(false_renamed, x2, y'', xs'') → max(cons(y'', xs''))
del(x3, nil) → nil
del(x4, cons(y1, xs1)) → if2(eq(x4, y1), x4, y1, xs1)
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, xs2) → xs2
if2(false_renamed, x8, y5, xs3) → cons(y5, del(x8, xs3))
ge(x9, 0) → true_renamed
ge(0, s(x10)) → false_renamed
ge(s(x11), s(y6)) → ge(x11, y6)
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[a33](0, 0) → true
equal_sort[a33](0, s(v54)) → false
equal_sort[a33](s(v55), 0) → false
equal_sort[a33](s(v55), s(v56)) → equal_sort[a33](v55, v56)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(v57, v58)) → false
equal_sort[a34](cons(v59, v60), nil) → false
equal_sort[a34](cons(v59, v60), cons(v61, v62)) → and(equal_sort[a33](v59, v61), equal_sort[a34](v60, v62))
equal_sort[a46](true_renamed, true_renamed) → true
equal_sort[a46](true_renamed, false_renamed) → false
equal_sort[a46](false_renamed, true_renamed) → false
equal_sort[a46](false_renamed, false_renamed) → true
equal_sort[a63](witness_sort[a63], witness_sort[a63]) → true
del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
max(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, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true_renamed, x0, x1, x2)
if2(false_renamed, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a46](true_renamed, true_renamed)
equal_sort[a46](true_renamed, false_renamed)
equal_sort[a46](false_renamed, true_renamed)
equal_sort[a46](false_renamed, false_renamed)
equal_sort[a63](witness_sort[a63], witness_sort[a63])
IF2(false_renamed, x8, y5, xs3) → DEL(x8, xs3)
DEL(x4, cons(y1, xs1)) → IF2(eq(x4, y1), x4, y1, xs1)
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, nil)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
max(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, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true_renamed, x0, x1, x2)
if2(false_renamed, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a46](true_renamed, true_renamed)
equal_sort[a46](true_renamed, false_renamed)
equal_sort[a46](false_renamed, true_renamed)
equal_sort[a46](false_renamed, false_renamed)
equal_sort[a63](witness_sort[a63], witness_sort[a63])
del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
max(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, nil)
del(x0, cons(x1, x2))
if2(true_renamed, x0, x1, x2)
if2(false_renamed, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a46](true_renamed, true_renamed)
equal_sort[a46](true_renamed, false_renamed)
equal_sort[a46](false_renamed, true_renamed)
equal_sort[a46](false_renamed, false_renamed)
equal_sort[a63](witness_sort[a63], witness_sort[a63])
IF2(false_renamed, x8, y5, xs3) → DEL(x8, xs3)
DEL(x4, cons(y1, xs1)) → IF2(eq(x4, y1), x4, y1, xs1)
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, x'', y', xs') → MAX(cons(x'', xs'))
MAX(cons(x', cons(y, xs))) → IF1(ge(x', y), x', y, xs)
IF1(false_renamed, x2, y'', xs'') → MAX(cons(y'', xs''))
del'(x3, nil) → false
del'(x4, cons(y1, xs1)) → if2'(eq(x4, y1), x4, y1, xs1)
if2'(true_renamed, x7, y4, xs2) → true
if2'(false_renamed, x8, y5, xs3) → del'(x8, xs3)
max(nil) → 0
max(cons(x, nil)) → x
max(cons(x', cons(y, xs))) → if1(ge(x', y), x', y, xs)
if1(true_renamed, x'', y', xs') → max(cons(x'', xs'))
if1(false_renamed, x2, y'', xs'') → max(cons(y'', xs''))
del(x3, nil) → nil
del(x4, cons(y1, xs1)) → if2(eq(x4, y1), x4, y1, xs1)
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, xs2) → xs2
if2(false_renamed, x8, y5, xs3) → cons(y5, del(x8, xs3))
ge(x9, 0) → true_renamed
ge(0, s(x10)) → false_renamed
ge(s(x11), s(y6)) → ge(x11, y6)
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[a33](0, 0) → true
equal_sort[a33](0, s(v54)) → false
equal_sort[a33](s(v55), 0) → false
equal_sort[a33](s(v55), s(v56)) → equal_sort[a33](v55, v56)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(v57, v58)) → false
equal_sort[a34](cons(v59, v60), nil) → false
equal_sort[a34](cons(v59, v60), cons(v61, v62)) → and(equal_sort[a33](v59, v61), equal_sort[a34](v60, v62))
equal_sort[a46](true_renamed, true_renamed) → true
equal_sort[a46](true_renamed, false_renamed) → false
equal_sort[a46](false_renamed, true_renamed) → false
equal_sort[a46](false_renamed, false_renamed) → true
equal_sort[a63](witness_sort[a63], witness_sort[a63]) → true
del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
max(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, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true_renamed, x0, x1, x2)
if2(false_renamed, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a46](true_renamed, true_renamed)
equal_sort[a46](true_renamed, false_renamed)
equal_sort[a46](false_renamed, true_renamed)
equal_sort[a46](false_renamed, false_renamed)
equal_sort[a63](witness_sort[a63], witness_sort[a63])
IF1(true_renamed, x'', y', xs') → MAX(cons(x'', xs'))
MAX(cons(x', cons(y, xs))) → IF1(ge(x', y), x', y, xs)
IF1(false_renamed, x2, y'', xs'') → MAX(cons(y'', xs''))
ge(x9, 0) → true_renamed
ge(0, s(x10)) → false_renamed
ge(s(x11), s(y6)) → ge(x11, y6)
del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
max(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, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true_renamed, x0, x1, x2)
if2(false_renamed, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a46](true_renamed, true_renamed)
equal_sort[a46](true_renamed, false_renamed)
equal_sort[a46](false_renamed, true_renamed)
equal_sort[a46](false_renamed, false_renamed)
equal_sort[a63](witness_sort[a63], witness_sort[a63])
del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
max(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, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true_renamed, x0, x1, x2)
if2(false_renamed, x0, x1, x2)
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[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a46](true_renamed, true_renamed)
equal_sort[a46](true_renamed, false_renamed)
equal_sort[a46](false_renamed, true_renamed)
equal_sort[a46](false_renamed, false_renamed)
equal_sort[a63](witness_sort[a63], witness_sort[a63])
IF1(true_renamed, x'', y', xs') → MAX(cons(x'', xs'))
MAX(cons(x', cons(y, xs))) → IF1(ge(x', y), x', y, xs)
IF1(false_renamed, x2, y'', xs'') → MAX(cons(y'', xs''))
ge(x9, 0) → true_renamed
ge(0, s(x10)) → false_renamed
ge(s(x11), s(y6)) → ge(x11, y6)
ge(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, x'', y', xs') → MAX(cons(x'', xs'))
MAX(cons(x', cons(y, xs))) → IF1(ge(x', y), x', y, xs)
IF1(false_renamed, x2, y'', xs'') → MAX(cons(y'', xs''))
trivial
dummyConstant=1
IF1_1=3
cons_1=2
ge(x9, 0) → true_renamed
ge(0, s(x10)) → false_renamed
ge(s(x11), s(y6)) → ge(x11, y6)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
IF2'(false_renamed, x8, y5, xs3) → DEL'(x8, xs3)
DEL'(x4, cons(y1, xs1)) → IF2'(eq(x4, y1), x4, y1, xs1)
del'(x3, nil) → false
del'(x4, cons(y1, xs1)) → if2'(eq(x4, y1), x4, y1, xs1)
if2'(true_renamed, x7, y4, xs2) → true
if2'(false_renamed, x8, y5, xs3) → del'(x8, xs3)
max(nil) → 0
max(cons(x, nil)) → x
max(cons(x', cons(y, xs))) → if1(ge(x', y), x', y, xs)
if1(true_renamed, x'', y', xs') → max(cons(x'', xs'))
if1(false_renamed, x2, y'', xs'') → max(cons(y'', xs''))
del(x3, nil) → nil
del(x4, cons(y1, xs1)) → if2(eq(x4, y1), x4, y1, xs1)
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, xs2) → xs2
if2(false_renamed, x8, y5, xs3) → cons(y5, del(x8, xs3))
ge(x9, 0) → true_renamed
ge(0, s(x10)) → false_renamed
ge(s(x11), s(y6)) → ge(x11, y6)
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[a33](0, 0) → true
equal_sort[a33](0, s(v54)) → false
equal_sort[a33](s(v55), 0) → false
equal_sort[a33](s(v55), s(v56)) → equal_sort[a33](v55, v56)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(v57, v58)) → false
equal_sort[a34](cons(v59, v60), nil) → false
equal_sort[a34](cons(v59, v60), cons(v61, v62)) → and(equal_sort[a33](v59, v61), equal_sort[a34](v60, v62))
equal_sort[a46](true_renamed, true_renamed) → true
equal_sort[a46](true_renamed, false_renamed) → false
equal_sort[a46](false_renamed, true_renamed) → false
equal_sort[a46](false_renamed, false_renamed) → true
equal_sort[a63](witness_sort[a63], witness_sort[a63]) → true
del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
max(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, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true_renamed, x0, x1, x2)
if2(false_renamed, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a46](true_renamed, true_renamed)
equal_sort[a46](true_renamed, false_renamed)
equal_sort[a46](false_renamed, true_renamed)
equal_sort[a46](false_renamed, false_renamed)
equal_sort[a63](witness_sort[a63], witness_sort[a63])
IF2'(false_renamed, x8, y5, xs3) → DEL'(x8, xs3)
DEL'(x4, cons(y1, xs1)) → IF2'(eq(x4, y1), x4, y1, xs1)
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, nil)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
max(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, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true_renamed, x0, x1, x2)
if2(false_renamed, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a46](true_renamed, true_renamed)
equal_sort[a46](true_renamed, false_renamed)
equal_sort[a46](false_renamed, true_renamed)
equal_sort[a46](false_renamed, false_renamed)
equal_sort[a63](witness_sort[a63], witness_sort[a63])
del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true_renamed, x0, x1, x2)
if2'(false_renamed, x0, x1, x2)
max(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, nil)
del(x0, cons(x1, x2))
if2(true_renamed, x0, x1, x2)
if2(false_renamed, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a46](true_renamed, true_renamed)
equal_sort[a46](true_renamed, false_renamed)
equal_sort[a46](false_renamed, true_renamed)
equal_sort[a46](false_renamed, false_renamed)
equal_sort[a63](witness_sort[a63], witness_sort[a63])
IF2'(false_renamed, x8, y5, xs3) → DEL'(x8, xs3)
DEL'(x4, cons(y1, xs1)) → IF2'(eq(x4, y1), x4, y1, xs1)
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: