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