0 QTRS
↳1 Overlay + Local Confluence (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔)
↳9 QDP
↳10 QReductionProof (⇔)
↳11 QDP
↳12 QDPSizeChangeProof (⇔)
↳13 TRUE
↳14 QDP
↳15 UsableRulesProof (⇔)
↳16 QDP
↳17 QReductionProof (⇔)
↳18 QDP
↳19 QDPSizeChangeProof (⇔)
↳20 TRUE
↳21 QDP
↳22 UsableRulesProof (⇔)
↳23 QDP
↳24 QReductionProof (⇔)
↳25 QDP
↳26 QDPSizeChangeProof (⇔)
↳27 TRUE
↳28 QDP
↳29 UsableRulesProof (⇔)
↳30 QDP
↳31 QReductionProof (⇔)
↳32 QDP
↳33 Rewriting (⇔)
↳34 QDP
↳35 Rewriting (⇔)
↳36 QDP
↳37 Rewriting (⇔)
↳38 QDP
↳39 UsableRulesProof (⇔)
↳40 QDP
↳41 QReductionProof (⇔)
↳42 QDP
↳43 Induction-Processor (⇐)
↳44 AND
↳45 QDP
↳46 PisEmptyProof (⇔)
↳47 TRUE
↳48 QTRS
↳49 Overlay + Local Confluence (⇔)
↳50 QTRS
↳51 DependencyPairsProof (⇔)
↳52 QDP
↳53 DependencyGraphProof (⇔)
↳54 AND
↳55 QDP
↳56 UsableRulesProof (⇔)
↳57 QDP
↳58 QReductionProof (⇔)
↳59 QDP
↳60 QDPSizeChangeProof (⇔)
↳61 TRUE
↳62 QDP
↳63 UsableRulesProof (⇔)
↳64 QDP
↳65 QReductionProof (⇔)
↳66 QDP
↳67 QDPSizeChangeProof (⇔)
↳68 TRUE
↳69 QDP
↳70 UsableRulesProof (⇔)
↳71 QDP
↳72 QReductionProof (⇔)
↳73 QDP
↳74 QDPSizeChangeProof (⇔)
↳75 TRUE
↳76 QDP
↳77 UsableRulesProof (⇔)
↳78 QDP
↳79 QReductionProof (⇔)
↳80 QDP
↳81 QDPSizeChangeProof (⇔)
↳82 TRUE
↳83 QDP
↳84 UsableRulesProof (⇔)
↳85 QDP
↳86 QReductionProof (⇔)
↳87 QDP
↳88 QDPSizeChangeProof (⇔)
↳89 TRUE
double(0) → 0
double(s(x)) → s(s(double(x)))
del(x, nil) → nil
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)
if(true, x, y, xs) → xs
if(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)
first(nil) → 0
first(cons(x, xs)) → x
doublelist(nil) → nil
doublelist(cons(x, xs)) → cons(double(x), doublelist(del(first(cons(x, xs)), cons(x, xs))))
double(0) → 0
double(s(x)) → s(s(double(x)))
del(x, nil) → nil
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)
if(true, x, y, xs) → xs
if(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)
first(nil) → 0
first(cons(x, xs)) → x
doublelist(nil) → nil
doublelist(cons(x, xs)) → cons(double(x), doublelist(del(first(cons(x, xs)), cons(x, xs))))
double(0)
double(s(x0))
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
doublelist(nil)
doublelist(cons(x0, x1))
DOUBLE(s(x)) → DOUBLE(x)
DEL(x, cons(y, xs)) → IF(eq(x, y), x, y, xs)
DEL(x, cons(y, xs)) → EQ(x, y)
IF(false, x, y, xs) → DEL(x, xs)
EQ(s(x), s(y)) → EQ(x, y)
DOUBLELIST(cons(x, xs)) → DOUBLE(x)
DOUBLELIST(cons(x, xs)) → DOUBLELIST(del(first(cons(x, xs)), cons(x, xs)))
DOUBLELIST(cons(x, xs)) → DEL(first(cons(x, xs)), cons(x, xs))
DOUBLELIST(cons(x, xs)) → FIRST(cons(x, xs))
double(0) → 0
double(s(x)) → s(s(double(x)))
del(x, nil) → nil
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)
if(true, x, y, xs) → xs
if(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)
first(nil) → 0
first(cons(x, xs)) → x
doublelist(nil) → nil
doublelist(cons(x, xs)) → cons(double(x), doublelist(del(first(cons(x, xs)), cons(x, xs))))
double(0)
double(s(x0))
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
doublelist(nil)
doublelist(cons(x0, x1))
EQ(s(x), s(y)) → EQ(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
del(x, nil) → nil
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)
if(true, x, y, xs) → xs
if(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)
first(nil) → 0
first(cons(x, xs)) → x
doublelist(nil) → nil
doublelist(cons(x, xs)) → cons(double(x), doublelist(del(first(cons(x, xs)), cons(x, xs))))
double(0)
double(s(x0))
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
doublelist(nil)
doublelist(cons(x0, x1))
EQ(s(x), s(y)) → EQ(x, y)
double(0)
double(s(x0))
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
doublelist(nil)
doublelist(cons(x0, x1))
double(0)
double(s(x0))
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
doublelist(nil)
doublelist(cons(x0, x1))
EQ(s(x), s(y)) → EQ(x, y)
From the DPs we obtained the following set of size-change graphs:
IF(false, x, y, xs) → DEL(x, xs)
DEL(x, cons(y, xs)) → IF(eq(x, y), x, y, xs)
double(0) → 0
double(s(x)) → s(s(double(x)))
del(x, nil) → nil
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)
if(true, x, y, xs) → xs
if(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)
first(nil) → 0
first(cons(x, xs)) → x
doublelist(nil) → nil
doublelist(cons(x, xs)) → cons(double(x), doublelist(del(first(cons(x, xs)), cons(x, xs))))
double(0)
double(s(x0))
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
doublelist(nil)
doublelist(cons(x0, x1))
IF(false, x, y, xs) → DEL(x, xs)
DEL(x, cons(y, xs)) → IF(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)
double(0)
double(s(x0))
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
doublelist(nil)
doublelist(cons(x0, x1))
double(0)
double(s(x0))
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
first(nil)
first(cons(x0, x1))
doublelist(nil)
doublelist(cons(x0, x1))
IF(false, x, y, xs) → DEL(x, xs)
DEL(x, cons(y, xs)) → IF(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:
DOUBLE(s(x)) → DOUBLE(x)
double(0) → 0
double(s(x)) → s(s(double(x)))
del(x, nil) → nil
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)
if(true, x, y, xs) → xs
if(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)
first(nil) → 0
first(cons(x, xs)) → x
doublelist(nil) → nil
doublelist(cons(x, xs)) → cons(double(x), doublelist(del(first(cons(x, xs)), cons(x, xs))))
double(0)
double(s(x0))
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
doublelist(nil)
doublelist(cons(x0, x1))
DOUBLE(s(x)) → DOUBLE(x)
double(0)
double(s(x0))
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
doublelist(nil)
doublelist(cons(x0, x1))
double(0)
double(s(x0))
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
doublelist(nil)
doublelist(cons(x0, x1))
DOUBLE(s(x)) → DOUBLE(x)
From the DPs we obtained the following set of size-change graphs:
DOUBLELIST(cons(x, xs)) → DOUBLELIST(del(first(cons(x, xs)), cons(x, xs)))
double(0) → 0
double(s(x)) → s(s(double(x)))
del(x, nil) → nil
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)
if(true, x, y, xs) → xs
if(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)
first(nil) → 0
first(cons(x, xs)) → x
doublelist(nil) → nil
doublelist(cons(x, xs)) → cons(double(x), doublelist(del(first(cons(x, xs)), cons(x, xs))))
double(0)
double(s(x0))
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
doublelist(nil)
doublelist(cons(x0, x1))
DOUBLELIST(cons(x, xs)) → DOUBLELIST(del(first(cons(x, xs)), cons(x, xs)))
first(cons(x, xs)) → x
del(x, cons(y, xs)) → if(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)
if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))
del(x, nil) → nil
double(0)
double(s(x0))
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
doublelist(nil)
doublelist(cons(x0, x1))
double(0)
double(s(x0))
doublelist(nil)
doublelist(cons(x0, x1))
DOUBLELIST(cons(x, xs)) → DOUBLELIST(del(first(cons(x, xs)), cons(x, xs)))
first(cons(x, xs)) → x
del(x, cons(y, xs)) → if(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)
if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))
del(x, nil) → nil
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
DOUBLELIST(cons(x, xs)) → DOUBLELIST(if(eq(first(cons(x, xs)), x), first(cons(x, xs)), x, xs))
DOUBLELIST(cons(x, xs)) → DOUBLELIST(if(eq(first(cons(x, xs)), x), first(cons(x, xs)), x, xs))
first(cons(x, xs)) → x
del(x, cons(y, xs)) → if(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)
if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))
del(x, nil) → nil
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
DOUBLELIST(cons(x, xs)) → DOUBLELIST(if(eq(x, x), first(cons(x, xs)), x, xs))
DOUBLELIST(cons(x, xs)) → DOUBLELIST(if(eq(x, x), first(cons(x, xs)), x, xs))
first(cons(x, xs)) → x
del(x, cons(y, xs)) → if(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)
if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))
del(x, nil) → nil
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
DOUBLELIST(cons(x, xs)) → DOUBLELIST(if(eq(x, x), x, x, xs))
DOUBLELIST(cons(x, xs)) → DOUBLELIST(if(eq(x, x), x, x, xs))
first(cons(x, xs)) → x
del(x, cons(y, xs)) → if(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)
if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))
del(x, nil) → nil
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
DOUBLELIST(cons(x, xs)) → DOUBLELIST(if(eq(x, x), x, x, xs))
eq(0, 0) → true
eq(s(x), s(y)) → eq(x, y)
if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)
del(x, nil) → nil
eq(0, s(y)) → false
eq(s(x), 0) → false
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
first(nil)
first(cons(x0, x1))
DOUBLELIST(cons(x, xs)) → DOUBLELIST(if(eq(x, x), x, x, xs))
eq(0, 0) → true
eq(s(x), s(y)) → eq(x, y)
if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)
del(x, nil) → nil
eq(0, s(y)) → false
eq(s(x), 0) → false
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
POL(0) = 0
POL(DOUBLELIST(x1)) = x1
POL(cons(x1, x2)) = 1 + x2
POL(del(x1, x2)) = x2
POL(eq(x1, x2)) = 0
POL(false) = 0
POL(if(x1, x2, x3, x4)) = 1 + x4
POL(nil) = 0
POL(s(x1)) = 0
POL(true) = 0
eq(0, 0) → true
eq(s(x), s(y)) → eq(x, y)
if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)
del(x, nil) → nil
eq(0, s(y)) → false
eq(s(x), 0) → false
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if'(true, x11, y9, xs4) → true
if'(false, x18, y15, xs8) → del'(x18, xs8)
del'(x25, cons(y21, xs12)) → if'(eq(x25, y21), x25, y21, xs12)
del'(x32, nil) → false
eq(0, 0) → true
eq(s(x4), s(y3)) → eq(x4, y3)
if(true, x11, y9, xs4) → xs4
if(false, x18, y15, xs8) → cons(y15, del(x18, xs8))
del(x25, cons(y21, xs12)) → if(eq(x25, y21), x25, y21, xs12)
del(x32, nil) → nil
eq(0, s(y32)) → false
eq(s(x45), 0) → false
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[a4](nil, nil) → true
equal_sort[a4](nil, cons(x0, x1)) → false
equal_sort[a4](cons(x0, x1), nil) → false
equal_sort[a4](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a4](x0, x2), equal_sort[a4](x1, x3))
equal_sort[a19](0, 0) → true
equal_sort[a19](0, s(x0)) → false
equal_sort[a19](s(x0), 0) → false
equal_sort[a19](s(x0), s(x1)) → equal_sort[a19](x0, x1)
equal_sort[a37](witness_sort[a37], witness_sort[a37]) → true
if'(true, x11, y9, xs4) → true
if'(false, x18, y15, xs8) → del'(x18, xs8)
del'(x25, cons(y21, xs12)) → if'(eq(x25, y21), x25, y21, xs12)
del'(x32, nil) → false
eq(0, 0) → true
eq(s(x4), s(y3)) → eq(x4, y3)
if(true, x11, y9, xs4) → xs4
if(false, x18, y15, xs8) → cons(y15, del(x18, xs8))
del(x25, cons(y21, xs12)) → if(eq(x25, y21), x25, y21, xs12)
del(x32, nil) → nil
eq(0, s(y32)) → false
eq(s(x45), 0) → false
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[a4](nil, nil) → true
equal_sort[a4](nil, cons(x0, x1)) → false
equal_sort[a4](cons(x0, x1), nil) → false
equal_sort[a4](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a4](x0, x2), equal_sort[a4](x1, x3))
equal_sort[a19](0, 0) → true
equal_sort[a19](0, s(x0)) → false
equal_sort[a19](s(x0), 0) → false
equal_sort[a19](s(x0), s(x1)) → equal_sort[a19](x0, x1)
equal_sort[a37](witness_sort[a37], witness_sort[a37]) → true
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, cons(x1, x2))
del'(x0, nil)
eq(0, 0)
eq(s(x0), s(x1))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, cons(x1, x2))
del(x0, nil)
eq(0, s(x0))
eq(s(x0), 0)
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[a4](nil, nil)
equal_sort[a4](nil, cons(x0, x1))
equal_sort[a4](cons(x0, x1), nil)
equal_sort[a4](cons(x0, x1), cons(x2, x3))
equal_sort[a19](0, 0)
equal_sort[a19](0, s(x0))
equal_sort[a19](s(x0), 0)
equal_sort[a19](s(x0), s(x1))
equal_sort[a37](witness_sort[a37], witness_sort[a37])
IF'(false, x18, y15, xs8) → DEL'(x18, xs8)
DEL'(x25, cons(y21, xs12)) → IF'(eq(x25, y21), x25, y21, xs12)
DEL'(x25, cons(y21, xs12)) → EQ(x25, y21)
EQ(s(x4), s(y3)) → EQ(x4, y3)
IF(false, x18, y15, xs8) → DEL(x18, xs8)
DEL(x25, cons(y21, xs12)) → IF(eq(x25, y21), x25, y21, xs12)
DEL(x25, cons(y21, xs12)) → EQ(x25, y21)
EQUAL_SORT[A4](cons(x0, x1), cons(x2, x3)) → AND(equal_sort[a4](x0, x2), equal_sort[a4](x1, x3))
EQUAL_SORT[A4](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A4](x0, x2)
EQUAL_SORT[A4](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A4](x1, x3)
EQUAL_SORT[A19](s(x0), s(x1)) → EQUAL_SORT[A19](x0, x1)
if'(true, x11, y9, xs4) → true
if'(false, x18, y15, xs8) → del'(x18, xs8)
del'(x25, cons(y21, xs12)) → if'(eq(x25, y21), x25, y21, xs12)
del'(x32, nil) → false
eq(0, 0) → true
eq(s(x4), s(y3)) → eq(x4, y3)
if(true, x11, y9, xs4) → xs4
if(false, x18, y15, xs8) → cons(y15, del(x18, xs8))
del(x25, cons(y21, xs12)) → if(eq(x25, y21), x25, y21, xs12)
del(x32, nil) → nil
eq(0, s(y32)) → false
eq(s(x45), 0) → false
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[a4](nil, nil) → true
equal_sort[a4](nil, cons(x0, x1)) → false
equal_sort[a4](cons(x0, x1), nil) → false
equal_sort[a4](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a4](x0, x2), equal_sort[a4](x1, x3))
equal_sort[a19](0, 0) → true
equal_sort[a19](0, s(x0)) → false
equal_sort[a19](s(x0), 0) → false
equal_sort[a19](s(x0), s(x1)) → equal_sort[a19](x0, x1)
equal_sort[a37](witness_sort[a37], witness_sort[a37]) → true
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, cons(x1, x2))
del'(x0, nil)
eq(0, 0)
eq(s(x0), s(x1))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, cons(x1, x2))
del(x0, nil)
eq(0, s(x0))
eq(s(x0), 0)
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[a4](nil, nil)
equal_sort[a4](nil, cons(x0, x1))
equal_sort[a4](cons(x0, x1), nil)
equal_sort[a4](cons(x0, x1), cons(x2, x3))
equal_sort[a19](0, 0)
equal_sort[a19](0, s(x0))
equal_sort[a19](s(x0), 0)
equal_sort[a19](s(x0), s(x1))
equal_sort[a37](witness_sort[a37], witness_sort[a37])
EQUAL_SORT[A19](s(x0), s(x1)) → EQUAL_SORT[A19](x0, x1)
if'(true, x11, y9, xs4) → true
if'(false, x18, y15, xs8) → del'(x18, xs8)
del'(x25, cons(y21, xs12)) → if'(eq(x25, y21), x25, y21, xs12)
del'(x32, nil) → false
eq(0, 0) → true
eq(s(x4), s(y3)) → eq(x4, y3)
if(true, x11, y9, xs4) → xs4
if(false, x18, y15, xs8) → cons(y15, del(x18, xs8))
del(x25, cons(y21, xs12)) → if(eq(x25, y21), x25, y21, xs12)
del(x32, nil) → nil
eq(0, s(y32)) → false
eq(s(x45), 0) → false
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[a4](nil, nil) → true
equal_sort[a4](nil, cons(x0, x1)) → false
equal_sort[a4](cons(x0, x1), nil) → false
equal_sort[a4](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a4](x0, x2), equal_sort[a4](x1, x3))
equal_sort[a19](0, 0) → true
equal_sort[a19](0, s(x0)) → false
equal_sort[a19](s(x0), 0) → false
equal_sort[a19](s(x0), s(x1)) → equal_sort[a19](x0, x1)
equal_sort[a37](witness_sort[a37], witness_sort[a37]) → true
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, cons(x1, x2))
del'(x0, nil)
eq(0, 0)
eq(s(x0), s(x1))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, cons(x1, x2))
del(x0, nil)
eq(0, s(x0))
eq(s(x0), 0)
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[a4](nil, nil)
equal_sort[a4](nil, cons(x0, x1))
equal_sort[a4](cons(x0, x1), nil)
equal_sort[a4](cons(x0, x1), cons(x2, x3))
equal_sort[a19](0, 0)
equal_sort[a19](0, s(x0))
equal_sort[a19](s(x0), 0)
equal_sort[a19](s(x0), s(x1))
equal_sort[a37](witness_sort[a37], witness_sort[a37])
EQUAL_SORT[A19](s(x0), s(x1)) → EQUAL_SORT[A19](x0, x1)
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, cons(x1, x2))
del'(x0, nil)
eq(0, 0)
eq(s(x0), s(x1))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, cons(x1, x2))
del(x0, nil)
eq(0, s(x0))
eq(s(x0), 0)
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[a4](nil, nil)
equal_sort[a4](nil, cons(x0, x1))
equal_sort[a4](cons(x0, x1), nil)
equal_sort[a4](cons(x0, x1), cons(x2, x3))
equal_sort[a19](0, 0)
equal_sort[a19](0, s(x0))
equal_sort[a19](s(x0), 0)
equal_sort[a19](s(x0), s(x1))
equal_sort[a37](witness_sort[a37], witness_sort[a37])
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, cons(x1, x2))
del'(x0, nil)
eq(0, 0)
eq(s(x0), s(x1))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, cons(x1, x2))
del(x0, nil)
eq(0, s(x0))
eq(s(x0), 0)
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[a4](nil, nil)
equal_sort[a4](nil, cons(x0, x1))
equal_sort[a4](cons(x0, x1), nil)
equal_sort[a4](cons(x0, x1), cons(x2, x3))
equal_sort[a19](0, 0)
equal_sort[a19](0, s(x0))
equal_sort[a19](s(x0), 0)
equal_sort[a19](s(x0), s(x1))
equal_sort[a37](witness_sort[a37], witness_sort[a37])
EQUAL_SORT[A19](s(x0), s(x1)) → EQUAL_SORT[A19](x0, x1)
From the DPs we obtained the following set of size-change graphs:
EQUAL_SORT[A4](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A4](x1, x3)
EQUAL_SORT[A4](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A4](x0, x2)
if'(true, x11, y9, xs4) → true
if'(false, x18, y15, xs8) → del'(x18, xs8)
del'(x25, cons(y21, xs12)) → if'(eq(x25, y21), x25, y21, xs12)
del'(x32, nil) → false
eq(0, 0) → true
eq(s(x4), s(y3)) → eq(x4, y3)
if(true, x11, y9, xs4) → xs4
if(false, x18, y15, xs8) → cons(y15, del(x18, xs8))
del(x25, cons(y21, xs12)) → if(eq(x25, y21), x25, y21, xs12)
del(x32, nil) → nil
eq(0, s(y32)) → false
eq(s(x45), 0) → false
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[a4](nil, nil) → true
equal_sort[a4](nil, cons(x0, x1)) → false
equal_sort[a4](cons(x0, x1), nil) → false
equal_sort[a4](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a4](x0, x2), equal_sort[a4](x1, x3))
equal_sort[a19](0, 0) → true
equal_sort[a19](0, s(x0)) → false
equal_sort[a19](s(x0), 0) → false
equal_sort[a19](s(x0), s(x1)) → equal_sort[a19](x0, x1)
equal_sort[a37](witness_sort[a37], witness_sort[a37]) → true
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, cons(x1, x2))
del'(x0, nil)
eq(0, 0)
eq(s(x0), s(x1))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, cons(x1, x2))
del(x0, nil)
eq(0, s(x0))
eq(s(x0), 0)
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[a4](nil, nil)
equal_sort[a4](nil, cons(x0, x1))
equal_sort[a4](cons(x0, x1), nil)
equal_sort[a4](cons(x0, x1), cons(x2, x3))
equal_sort[a19](0, 0)
equal_sort[a19](0, s(x0))
equal_sort[a19](s(x0), 0)
equal_sort[a19](s(x0), s(x1))
equal_sort[a37](witness_sort[a37], witness_sort[a37])
EQUAL_SORT[A4](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A4](x1, x3)
EQUAL_SORT[A4](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A4](x0, x2)
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, cons(x1, x2))
del'(x0, nil)
eq(0, 0)
eq(s(x0), s(x1))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, cons(x1, x2))
del(x0, nil)
eq(0, s(x0))
eq(s(x0), 0)
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[a4](nil, nil)
equal_sort[a4](nil, cons(x0, x1))
equal_sort[a4](cons(x0, x1), nil)
equal_sort[a4](cons(x0, x1), cons(x2, x3))
equal_sort[a19](0, 0)
equal_sort[a19](0, s(x0))
equal_sort[a19](s(x0), 0)
equal_sort[a19](s(x0), s(x1))
equal_sort[a37](witness_sort[a37], witness_sort[a37])
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, cons(x1, x2))
del'(x0, nil)
eq(0, 0)
eq(s(x0), s(x1))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, cons(x1, x2))
del(x0, nil)
eq(0, s(x0))
eq(s(x0), 0)
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[a4](nil, nil)
equal_sort[a4](nil, cons(x0, x1))
equal_sort[a4](cons(x0, x1), nil)
equal_sort[a4](cons(x0, x1), cons(x2, x3))
equal_sort[a19](0, 0)
equal_sort[a19](0, s(x0))
equal_sort[a19](s(x0), 0)
equal_sort[a19](s(x0), s(x1))
equal_sort[a37](witness_sort[a37], witness_sort[a37])
EQUAL_SORT[A4](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A4](x1, x3)
EQUAL_SORT[A4](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A4](x0, x2)
From the DPs we obtained the following set of size-change graphs:
EQ(s(x4), s(y3)) → EQ(x4, y3)
if'(true, x11, y9, xs4) → true
if'(false, x18, y15, xs8) → del'(x18, xs8)
del'(x25, cons(y21, xs12)) → if'(eq(x25, y21), x25, y21, xs12)
del'(x32, nil) → false
eq(0, 0) → true
eq(s(x4), s(y3)) → eq(x4, y3)
if(true, x11, y9, xs4) → xs4
if(false, x18, y15, xs8) → cons(y15, del(x18, xs8))
del(x25, cons(y21, xs12)) → if(eq(x25, y21), x25, y21, xs12)
del(x32, nil) → nil
eq(0, s(y32)) → false
eq(s(x45), 0) → false
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[a4](nil, nil) → true
equal_sort[a4](nil, cons(x0, x1)) → false
equal_sort[a4](cons(x0, x1), nil) → false
equal_sort[a4](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a4](x0, x2), equal_sort[a4](x1, x3))
equal_sort[a19](0, 0) → true
equal_sort[a19](0, s(x0)) → false
equal_sort[a19](s(x0), 0) → false
equal_sort[a19](s(x0), s(x1)) → equal_sort[a19](x0, x1)
equal_sort[a37](witness_sort[a37], witness_sort[a37]) → true
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, cons(x1, x2))
del'(x0, nil)
eq(0, 0)
eq(s(x0), s(x1))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, cons(x1, x2))
del(x0, nil)
eq(0, s(x0))
eq(s(x0), 0)
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[a4](nil, nil)
equal_sort[a4](nil, cons(x0, x1))
equal_sort[a4](cons(x0, x1), nil)
equal_sort[a4](cons(x0, x1), cons(x2, x3))
equal_sort[a19](0, 0)
equal_sort[a19](0, s(x0))
equal_sort[a19](s(x0), 0)
equal_sort[a19](s(x0), s(x1))
equal_sort[a37](witness_sort[a37], witness_sort[a37])
EQ(s(x4), s(y3)) → EQ(x4, y3)
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, cons(x1, x2))
del'(x0, nil)
eq(0, 0)
eq(s(x0), s(x1))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, cons(x1, x2))
del(x0, nil)
eq(0, s(x0))
eq(s(x0), 0)
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[a4](nil, nil)
equal_sort[a4](nil, cons(x0, x1))
equal_sort[a4](cons(x0, x1), nil)
equal_sort[a4](cons(x0, x1), cons(x2, x3))
equal_sort[a19](0, 0)
equal_sort[a19](0, s(x0))
equal_sort[a19](s(x0), 0)
equal_sort[a19](s(x0), s(x1))
equal_sort[a37](witness_sort[a37], witness_sort[a37])
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, cons(x1, x2))
del'(x0, nil)
eq(0, 0)
eq(s(x0), s(x1))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, cons(x1, x2))
del(x0, nil)
eq(0, s(x0))
eq(s(x0), 0)
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[a4](nil, nil)
equal_sort[a4](nil, cons(x0, x1))
equal_sort[a4](cons(x0, x1), nil)
equal_sort[a4](cons(x0, x1), cons(x2, x3))
equal_sort[a19](0, 0)
equal_sort[a19](0, s(x0))
equal_sort[a19](s(x0), 0)
equal_sort[a19](s(x0), s(x1))
equal_sort[a37](witness_sort[a37], witness_sort[a37])
EQ(s(x4), s(y3)) → EQ(x4, y3)
From the DPs we obtained the following set of size-change graphs:
DEL(x25, cons(y21, xs12)) → IF(eq(x25, y21), x25, y21, xs12)
IF(false, x18, y15, xs8) → DEL(x18, xs8)
if'(true, x11, y9, xs4) → true
if'(false, x18, y15, xs8) → del'(x18, xs8)
del'(x25, cons(y21, xs12)) → if'(eq(x25, y21), x25, y21, xs12)
del'(x32, nil) → false
eq(0, 0) → true
eq(s(x4), s(y3)) → eq(x4, y3)
if(true, x11, y9, xs4) → xs4
if(false, x18, y15, xs8) → cons(y15, del(x18, xs8))
del(x25, cons(y21, xs12)) → if(eq(x25, y21), x25, y21, xs12)
del(x32, nil) → nil
eq(0, s(y32)) → false
eq(s(x45), 0) → false
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[a4](nil, nil) → true
equal_sort[a4](nil, cons(x0, x1)) → false
equal_sort[a4](cons(x0, x1), nil) → false
equal_sort[a4](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a4](x0, x2), equal_sort[a4](x1, x3))
equal_sort[a19](0, 0) → true
equal_sort[a19](0, s(x0)) → false
equal_sort[a19](s(x0), 0) → false
equal_sort[a19](s(x0), s(x1)) → equal_sort[a19](x0, x1)
equal_sort[a37](witness_sort[a37], witness_sort[a37]) → true
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, cons(x1, x2))
del'(x0, nil)
eq(0, 0)
eq(s(x0), s(x1))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, cons(x1, x2))
del(x0, nil)
eq(0, s(x0))
eq(s(x0), 0)
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[a4](nil, nil)
equal_sort[a4](nil, cons(x0, x1))
equal_sort[a4](cons(x0, x1), nil)
equal_sort[a4](cons(x0, x1), cons(x2, x3))
equal_sort[a19](0, 0)
equal_sort[a19](0, s(x0))
equal_sort[a19](s(x0), 0)
equal_sort[a19](s(x0), s(x1))
equal_sort[a37](witness_sort[a37], witness_sort[a37])
DEL(x25, cons(y21, xs12)) → IF(eq(x25, y21), x25, y21, xs12)
IF(false, x18, y15, xs8) → DEL(x18, xs8)
eq(0, 0) → true
eq(s(x4), s(y3)) → eq(x4, y3)
eq(0, s(y32)) → false
eq(s(x45), 0) → false
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, cons(x1, x2))
del'(x0, nil)
eq(0, 0)
eq(s(x0), s(x1))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, cons(x1, x2))
del(x0, nil)
eq(0, s(x0))
eq(s(x0), 0)
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[a4](nil, nil)
equal_sort[a4](nil, cons(x0, x1))
equal_sort[a4](cons(x0, x1), nil)
equal_sort[a4](cons(x0, x1), cons(x2, x3))
equal_sort[a19](0, 0)
equal_sort[a19](0, s(x0))
equal_sort[a19](s(x0), 0)
equal_sort[a19](s(x0), s(x1))
equal_sort[a37](witness_sort[a37], witness_sort[a37])
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, cons(x1, x2))
del'(x0, nil)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, cons(x1, x2))
del(x0, nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a4](nil, nil)
equal_sort[a4](nil, cons(x0, x1))
equal_sort[a4](cons(x0, x1), nil)
equal_sort[a4](cons(x0, x1), cons(x2, x3))
equal_sort[a19](0, 0)
equal_sort[a19](0, s(x0))
equal_sort[a19](s(x0), 0)
equal_sort[a19](s(x0), s(x1))
equal_sort[a37](witness_sort[a37], witness_sort[a37])
DEL(x25, cons(y21, xs12)) → IF(eq(x25, y21), x25, y21, xs12)
IF(false, x18, y15, xs8) → DEL(x18, xs8)
eq(0, 0) → true
eq(s(x4), s(y3)) → eq(x4, y3)
eq(0, s(y32)) → false
eq(s(x45), 0) → false
eq(0, 0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
From the DPs we obtained the following set of size-change graphs:
DEL'(x25, cons(y21, xs12)) → IF'(eq(x25, y21), x25, y21, xs12)
IF'(false, x18, y15, xs8) → DEL'(x18, xs8)
if'(true, x11, y9, xs4) → true
if'(false, x18, y15, xs8) → del'(x18, xs8)
del'(x25, cons(y21, xs12)) → if'(eq(x25, y21), x25, y21, xs12)
del'(x32, nil) → false
eq(0, 0) → true
eq(s(x4), s(y3)) → eq(x4, y3)
if(true, x11, y9, xs4) → xs4
if(false, x18, y15, xs8) → cons(y15, del(x18, xs8))
del(x25, cons(y21, xs12)) → if(eq(x25, y21), x25, y21, xs12)
del(x32, nil) → nil
eq(0, s(y32)) → false
eq(s(x45), 0) → false
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[a4](nil, nil) → true
equal_sort[a4](nil, cons(x0, x1)) → false
equal_sort[a4](cons(x0, x1), nil) → false
equal_sort[a4](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a4](x0, x2), equal_sort[a4](x1, x3))
equal_sort[a19](0, 0) → true
equal_sort[a19](0, s(x0)) → false
equal_sort[a19](s(x0), 0) → false
equal_sort[a19](s(x0), s(x1)) → equal_sort[a19](x0, x1)
equal_sort[a37](witness_sort[a37], witness_sort[a37]) → true
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, cons(x1, x2))
del'(x0, nil)
eq(0, 0)
eq(s(x0), s(x1))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, cons(x1, x2))
del(x0, nil)
eq(0, s(x0))
eq(s(x0), 0)
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[a4](nil, nil)
equal_sort[a4](nil, cons(x0, x1))
equal_sort[a4](cons(x0, x1), nil)
equal_sort[a4](cons(x0, x1), cons(x2, x3))
equal_sort[a19](0, 0)
equal_sort[a19](0, s(x0))
equal_sort[a19](s(x0), 0)
equal_sort[a19](s(x0), s(x1))
equal_sort[a37](witness_sort[a37], witness_sort[a37])
DEL'(x25, cons(y21, xs12)) → IF'(eq(x25, y21), x25, y21, xs12)
IF'(false, x18, y15, xs8) → DEL'(x18, xs8)
eq(0, 0) → true
eq(s(x4), s(y3)) → eq(x4, y3)
eq(0, s(y32)) → false
eq(s(x45), 0) → false
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, cons(x1, x2))
del'(x0, nil)
eq(0, 0)
eq(s(x0), s(x1))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, cons(x1, x2))
del(x0, nil)
eq(0, s(x0))
eq(s(x0), 0)
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[a4](nil, nil)
equal_sort[a4](nil, cons(x0, x1))
equal_sort[a4](cons(x0, x1), nil)
equal_sort[a4](cons(x0, x1), cons(x2, x3))
equal_sort[a19](0, 0)
equal_sort[a19](0, s(x0))
equal_sort[a19](s(x0), 0)
equal_sort[a19](s(x0), s(x1))
equal_sort[a37](witness_sort[a37], witness_sort[a37])
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, cons(x1, x2))
del'(x0, nil)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, cons(x1, x2))
del(x0, nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a4](nil, nil)
equal_sort[a4](nil, cons(x0, x1))
equal_sort[a4](cons(x0, x1), nil)
equal_sort[a4](cons(x0, x1), cons(x2, x3))
equal_sort[a19](0, 0)
equal_sort[a19](0, s(x0))
equal_sort[a19](s(x0), 0)
equal_sort[a19](s(x0), s(x1))
equal_sort[a37](witness_sort[a37], witness_sort[a37])
DEL'(x25, cons(y21, xs12)) → IF'(eq(x25, y21), x25, y21, xs12)
IF'(false, x18, y15, xs8) → DEL'(x18, xs8)
eq(0, 0) → true
eq(s(x4), s(y3)) → eq(x4, y3)
eq(0, s(y32)) → false
eq(s(x45), 0) → false
eq(0, 0)
eq(s(x0), s(x1))
eq(0, s(x0))
eq(s(x0), 0)
From the DPs we obtained the following set of size-change graphs: