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 Induction-Processor (⇐)
↳34 AND
↳35 QDP
↳36 PisEmptyProof (⇔)
↳37 TRUE
↳38 QTRS
↳39 Overlay + Local Confluence (⇔)
↳40 QTRS
↳41 DependencyPairsProof (⇔)
↳42 QDP
↳43 DependencyGraphProof (⇔)
↳44 AND
↳45 QDP
↳46 UsableRulesProof (⇔)
↳47 QDP
↳48 QReductionProof (⇔)
↳49 QDP
↳50 QDPSizeChangeProof (⇔)
↳51 TRUE
↳52 QDP
↳53 UsableRulesProof (⇔)
↳54 QDP
↳55 QReductionProof (⇔)
↳56 QDP
↳57 QDPSizeChangeProof (⇔)
↳58 TRUE
↳59 QDP
↳60 UsableRulesProof (⇔)
↳61 QDP
↳62 QReductionProof (⇔)
↳63 QDP
↳64 QDPSizeChangeProof (⇔)
↳65 TRUE
↳66 QDP
↳67 UsableRulesProof (⇔)
↳68 QDP
↳69 QReductionProof (⇔)
↳70 QDP
↳71 QDPSizeChangeProof (⇔)
↳72 TRUE
↳73 QDP
↳74 UsableRulesProof (⇔)
↳75 QDP
↳76 QReductionProof (⇔)
↳77 QDP
↳78 QDPSizeChangeProof (⇔)
↳79 TRUE
↳80 QDP
↳81 UsableRulesProof (⇔)
↳82 QDP
↳83 QReductionProof (⇔)
↳84 QDP
↳85 QDPSizeChangeProof (⇔)
↳86 TRUE
last(nil) → 0
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))
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)
reverse(nil) → nil
reverse(cons(x, xs)) → cons(last(cons(x, xs)), reverse(del(last(cons(x, xs)), cons(x, xs))))
last(nil) → 0
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))
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)
reverse(nil) → nil
reverse(cons(x, xs)) → cons(last(cons(x, xs)), reverse(del(last(cons(x, xs)), cons(x, xs))))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
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))
reverse(nil)
reverse(cons(x0, x1))
LAST(cons(x, cons(y, xs))) → LAST(cons(y, xs))
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)
REVERSE(cons(x, xs)) → LAST(cons(x, xs))
REVERSE(cons(x, xs)) → REVERSE(del(last(cons(x, xs)), cons(x, xs)))
REVERSE(cons(x, xs)) → DEL(last(cons(x, xs)), cons(x, xs))
last(nil) → 0
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))
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)
reverse(nil) → nil
reverse(cons(x, xs)) → cons(last(cons(x, xs)), reverse(del(last(cons(x, xs)), cons(x, xs))))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
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))
reverse(nil)
reverse(cons(x0, x1))
EQ(s(x), s(y)) → EQ(x, y)
last(nil) → 0
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))
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)
reverse(nil) → nil
reverse(cons(x, xs)) → cons(last(cons(x, xs)), reverse(del(last(cons(x, xs)), cons(x, xs))))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
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))
reverse(nil)
reverse(cons(x0, x1))
EQ(s(x), s(y)) → EQ(x, y)
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
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))
reverse(nil)
reverse(cons(x0, x1))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
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))
reverse(nil)
reverse(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)
last(nil) → 0
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))
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)
reverse(nil) → nil
reverse(cons(x, xs)) → cons(last(cons(x, xs)), reverse(del(last(cons(x, xs)), cons(x, xs))))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
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))
reverse(nil)
reverse(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)
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
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))
reverse(nil)
reverse(cons(x0, x1))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
reverse(nil)
reverse(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:
LAST(cons(x, cons(y, xs))) → LAST(cons(y, xs))
last(nil) → 0
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))
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)
reverse(nil) → nil
reverse(cons(x, xs)) → cons(last(cons(x, xs)), reverse(del(last(cons(x, xs)), cons(x, xs))))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
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))
reverse(nil)
reverse(cons(x0, x1))
LAST(cons(x, cons(y, xs))) → LAST(cons(y, xs))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
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))
reverse(nil)
reverse(cons(x0, x1))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
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))
reverse(nil)
reverse(cons(x0, x1))
LAST(cons(x, cons(y, xs))) → LAST(cons(y, xs))
From the DPs we obtained the following set of size-change graphs:
REVERSE(cons(x, xs)) → REVERSE(del(last(cons(x, xs)), cons(x, xs)))
last(nil) → 0
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))
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)
reverse(nil) → nil
reverse(cons(x, xs)) → cons(last(cons(x, xs)), reverse(del(last(cons(x, xs)), cons(x, xs))))
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
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))
reverse(nil)
reverse(cons(x0, x1))
REVERSE(cons(x, xs)) → REVERSE(del(last(cons(x, xs)), cons(x, xs)))
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, 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)
if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))
del(x, nil) → nil
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
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))
reverse(nil)
reverse(cons(x0, x1))
reverse(nil)
reverse(cons(x0, x1))
REVERSE(cons(x, xs)) → REVERSE(del(last(cons(x, xs)), cons(x, xs)))
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, 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)
if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))
del(x, nil) → nil
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
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) = 2
POL(REVERSE(x1)) = x1
POL(cons(x1, x2)) = 1 + x1 + 2·x2
POL(del(x1, x2)) = x2
POL(eq(x1, x2)) = 2·x2
POL(false) = 1
POL(if(x1, x2, x3, x4)) = 1 + x3 + 2·x4
POL(last(x1)) = 3 + 2·x1
POL(nil) = 0
POL(s(x1)) = 1 + x1
POL(true) = 2
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, 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)
if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))
del(x, nil) → nil
last(nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
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))
del'(x16, cons(y11, xs7)) → if'(eq(x16, y11), x16, y11, xs7)
if'(true, x59, y44, xs28) → true
if'(false, x68, y51, xs33) → del'(x68, xs33)
del'(x77, nil) → false
last(cons(x, nil)) → x
last(cons(x7, cons(y4, xs2))) → last(cons(y4, xs2))
del(x16, cons(y11, xs7)) → if(eq(x16, y11), x16, y11, xs7)
eq(0, 0) → true
eq(0, s(y24)) → false
eq(s(x41), 0) → false
eq(s(x50), s(y37)) → eq(x50, y37)
if(true, x59, y44, xs28) → xs28
if(false, x68, y51, xs33) → cons(y51, del(x68, xs33))
del(x77, nil) → nil
last(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(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a24](nil, nil) → true
equal_sort[a24](nil, cons(x0, x1)) → false
equal_sort[a24](cons(x0, x1), nil) → false
equal_sort[a24](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a24](x0, x2), equal_sort[a24](x1, x3))
equal_sort[a42](witness_sort[a42], witness_sort[a42]) → true
del'(x16, cons(y11, xs7)) → if'(eq(x16, y11), x16, y11, xs7)
if'(true, x59, y44, xs28) → true
if'(false, x68, y51, xs33) → del'(x68, xs33)
del'(x77, nil) → false
last(cons(x, nil)) → x
last(cons(x7, cons(y4, xs2))) → last(cons(y4, xs2))
del(x16, cons(y11, xs7)) → if(eq(x16, y11), x16, y11, xs7)
eq(0, 0) → true
eq(0, s(y24)) → false
eq(s(x41), 0) → false
eq(s(x50), s(y37)) → eq(x50, y37)
if(true, x59, y44, xs28) → xs28
if(false, x68, y51, xs33) → cons(y51, del(x68, xs33))
del(x77, nil) → nil
last(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(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a24](nil, nil) → true
equal_sort[a24](nil, cons(x0, x1)) → false
equal_sort[a24](cons(x0, x1), nil) → false
equal_sort[a24](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a24](x0, x2), equal_sort[a24](x1, x3))
equal_sort[a42](witness_sort[a42], witness_sort[a42]) → true
del'(x0, cons(x1, x2))
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, nil)
last(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[a24](nil, nil)
equal_sort[a24](nil, cons(x0, x1))
equal_sort[a24](cons(x0, x1), nil)
equal_sort[a24](cons(x0, x1), cons(x2, x3))
equal_sort[a42](witness_sort[a42], witness_sort[a42])
DEL'(x16, cons(y11, xs7)) → IF'(eq(x16, y11), x16, y11, xs7)
DEL'(x16, cons(y11, xs7)) → EQ(x16, y11)
IF'(false, x68, y51, xs33) → DEL'(x68, xs33)
LAST(cons(x7, cons(y4, xs2))) → LAST(cons(y4, xs2))
DEL(x16, cons(y11, xs7)) → IF(eq(x16, y11), x16, y11, xs7)
DEL(x16, cons(y11, xs7)) → EQ(x16, y11)
EQ(s(x50), s(y37)) → EQ(x50, y37)
IF(false, x68, y51, xs33) → DEL(x68, xs33)
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
EQUAL_SORT[A24](cons(x0, x1), cons(x2, x3)) → AND(equal_sort[a24](x0, x2), equal_sort[a24](x1, x3))
EQUAL_SORT[A24](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A24](x0, x2)
EQUAL_SORT[A24](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A24](x1, x3)
del'(x16, cons(y11, xs7)) → if'(eq(x16, y11), x16, y11, xs7)
if'(true, x59, y44, xs28) → true
if'(false, x68, y51, xs33) → del'(x68, xs33)
del'(x77, nil) → false
last(cons(x, nil)) → x
last(cons(x7, cons(y4, xs2))) → last(cons(y4, xs2))
del(x16, cons(y11, xs7)) → if(eq(x16, y11), x16, y11, xs7)
eq(0, 0) → true
eq(0, s(y24)) → false
eq(s(x41), 0) → false
eq(s(x50), s(y37)) → eq(x50, y37)
if(true, x59, y44, xs28) → xs28
if(false, x68, y51, xs33) → cons(y51, del(x68, xs33))
del(x77, nil) → nil
last(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(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a24](nil, nil) → true
equal_sort[a24](nil, cons(x0, x1)) → false
equal_sort[a24](cons(x0, x1), nil) → false
equal_sort[a24](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a24](x0, x2), equal_sort[a24](x1, x3))
equal_sort[a42](witness_sort[a42], witness_sort[a42]) → true
del'(x0, cons(x1, x2))
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, nil)
last(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[a24](nil, nil)
equal_sort[a24](nil, cons(x0, x1))
equal_sort[a24](cons(x0, x1), nil)
equal_sort[a24](cons(x0, x1), cons(x2, x3))
equal_sort[a42](witness_sort[a42], witness_sort[a42])
EQUAL_SORT[A24](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A24](x1, x3)
EQUAL_SORT[A24](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A24](x0, x2)
del'(x16, cons(y11, xs7)) → if'(eq(x16, y11), x16, y11, xs7)
if'(true, x59, y44, xs28) → true
if'(false, x68, y51, xs33) → del'(x68, xs33)
del'(x77, nil) → false
last(cons(x, nil)) → x
last(cons(x7, cons(y4, xs2))) → last(cons(y4, xs2))
del(x16, cons(y11, xs7)) → if(eq(x16, y11), x16, y11, xs7)
eq(0, 0) → true
eq(0, s(y24)) → false
eq(s(x41), 0) → false
eq(s(x50), s(y37)) → eq(x50, y37)
if(true, x59, y44, xs28) → xs28
if(false, x68, y51, xs33) → cons(y51, del(x68, xs33))
del(x77, nil) → nil
last(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(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a24](nil, nil) → true
equal_sort[a24](nil, cons(x0, x1)) → false
equal_sort[a24](cons(x0, x1), nil) → false
equal_sort[a24](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a24](x0, x2), equal_sort[a24](x1, x3))
equal_sort[a42](witness_sort[a42], witness_sort[a42]) → true
del'(x0, cons(x1, x2))
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, nil)
last(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[a24](nil, nil)
equal_sort[a24](nil, cons(x0, x1))
equal_sort[a24](cons(x0, x1), nil)
equal_sort[a24](cons(x0, x1), cons(x2, x3))
equal_sort[a42](witness_sort[a42], witness_sort[a42])
EQUAL_SORT[A24](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A24](x1, x3)
EQUAL_SORT[A24](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A24](x0, x2)
del'(x0, cons(x1, x2))
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, nil)
last(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[a24](nil, nil)
equal_sort[a24](nil, cons(x0, x1))
equal_sort[a24](cons(x0, x1), nil)
equal_sort[a24](cons(x0, x1), cons(x2, x3))
equal_sort[a42](witness_sort[a42], witness_sort[a42])
del'(x0, cons(x1, x2))
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, nil)
last(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[a24](nil, nil)
equal_sort[a24](nil, cons(x0, x1))
equal_sort[a24](cons(x0, x1), nil)
equal_sort[a24](cons(x0, x1), cons(x2, x3))
equal_sort[a42](witness_sort[a42], witness_sort[a42])
EQUAL_SORT[A24](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A24](x1, x3)
EQUAL_SORT[A24](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A24](x0, x2)
From the DPs we obtained the following set of size-change graphs:
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
del'(x16, cons(y11, xs7)) → if'(eq(x16, y11), x16, y11, xs7)
if'(true, x59, y44, xs28) → true
if'(false, x68, y51, xs33) → del'(x68, xs33)
del'(x77, nil) → false
last(cons(x, nil)) → x
last(cons(x7, cons(y4, xs2))) → last(cons(y4, xs2))
del(x16, cons(y11, xs7)) → if(eq(x16, y11), x16, y11, xs7)
eq(0, 0) → true
eq(0, s(y24)) → false
eq(s(x41), 0) → false
eq(s(x50), s(y37)) → eq(x50, y37)
if(true, x59, y44, xs28) → xs28
if(false, x68, y51, xs33) → cons(y51, del(x68, xs33))
del(x77, nil) → nil
last(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(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a24](nil, nil) → true
equal_sort[a24](nil, cons(x0, x1)) → false
equal_sort[a24](cons(x0, x1), nil) → false
equal_sort[a24](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a24](x0, x2), equal_sort[a24](x1, x3))
equal_sort[a42](witness_sort[a42], witness_sort[a42]) → true
del'(x0, cons(x1, x2))
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, nil)
last(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[a24](nil, nil)
equal_sort[a24](nil, cons(x0, x1))
equal_sort[a24](cons(x0, x1), nil)
equal_sort[a24](cons(x0, x1), cons(x2, x3))
equal_sort[a42](witness_sort[a42], witness_sort[a42])
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
del'(x0, cons(x1, x2))
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, nil)
last(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[a24](nil, nil)
equal_sort[a24](nil, cons(x0, x1))
equal_sort[a24](cons(x0, x1), nil)
equal_sort[a24](cons(x0, x1), cons(x2, x3))
equal_sort[a42](witness_sort[a42], witness_sort[a42])
del'(x0, cons(x1, x2))
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, nil)
last(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[a24](nil, nil)
equal_sort[a24](nil, cons(x0, x1))
equal_sort[a24](cons(x0, x1), nil)
equal_sort[a24](cons(x0, x1), cons(x2, x3))
equal_sort[a42](witness_sort[a42], witness_sort[a42])
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
From the DPs we obtained the following set of size-change graphs:
EQ(s(x50), s(y37)) → EQ(x50, y37)
del'(x16, cons(y11, xs7)) → if'(eq(x16, y11), x16, y11, xs7)
if'(true, x59, y44, xs28) → true
if'(false, x68, y51, xs33) → del'(x68, xs33)
del'(x77, nil) → false
last(cons(x, nil)) → x
last(cons(x7, cons(y4, xs2))) → last(cons(y4, xs2))
del(x16, cons(y11, xs7)) → if(eq(x16, y11), x16, y11, xs7)
eq(0, 0) → true
eq(0, s(y24)) → false
eq(s(x41), 0) → false
eq(s(x50), s(y37)) → eq(x50, y37)
if(true, x59, y44, xs28) → xs28
if(false, x68, y51, xs33) → cons(y51, del(x68, xs33))
del(x77, nil) → nil
last(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(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a24](nil, nil) → true
equal_sort[a24](nil, cons(x0, x1)) → false
equal_sort[a24](cons(x0, x1), nil) → false
equal_sort[a24](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a24](x0, x2), equal_sort[a24](x1, x3))
equal_sort[a42](witness_sort[a42], witness_sort[a42]) → true
del'(x0, cons(x1, x2))
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, nil)
last(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[a24](nil, nil)
equal_sort[a24](nil, cons(x0, x1))
equal_sort[a24](cons(x0, x1), nil)
equal_sort[a24](cons(x0, x1), cons(x2, x3))
equal_sort[a42](witness_sort[a42], witness_sort[a42])
EQ(s(x50), s(y37)) → EQ(x50, y37)
del'(x0, cons(x1, x2))
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, nil)
last(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[a24](nil, nil)
equal_sort[a24](nil, cons(x0, x1))
equal_sort[a24](cons(x0, x1), nil)
equal_sort[a24](cons(x0, x1), cons(x2, x3))
equal_sort[a42](witness_sort[a42], witness_sort[a42])
del'(x0, cons(x1, x2))
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, nil)
last(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[a24](nil, nil)
equal_sort[a24](nil, cons(x0, x1))
equal_sort[a24](cons(x0, x1), nil)
equal_sort[a24](cons(x0, x1), cons(x2, x3))
equal_sort[a42](witness_sort[a42], witness_sort[a42])
EQ(s(x50), s(y37)) → EQ(x50, y37)
From the DPs we obtained the following set of size-change graphs:
IF(false, x68, y51, xs33) → DEL(x68, xs33)
DEL(x16, cons(y11, xs7)) → IF(eq(x16, y11), x16, y11, xs7)
del'(x16, cons(y11, xs7)) → if'(eq(x16, y11), x16, y11, xs7)
if'(true, x59, y44, xs28) → true
if'(false, x68, y51, xs33) → del'(x68, xs33)
del'(x77, nil) → false
last(cons(x, nil)) → x
last(cons(x7, cons(y4, xs2))) → last(cons(y4, xs2))
del(x16, cons(y11, xs7)) → if(eq(x16, y11), x16, y11, xs7)
eq(0, 0) → true
eq(0, s(y24)) → false
eq(s(x41), 0) → false
eq(s(x50), s(y37)) → eq(x50, y37)
if(true, x59, y44, xs28) → xs28
if(false, x68, y51, xs33) → cons(y51, del(x68, xs33))
del(x77, nil) → nil
last(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(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a24](nil, nil) → true
equal_sort[a24](nil, cons(x0, x1)) → false
equal_sort[a24](cons(x0, x1), nil) → false
equal_sort[a24](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a24](x0, x2), equal_sort[a24](x1, x3))
equal_sort[a42](witness_sort[a42], witness_sort[a42]) → true
del'(x0, cons(x1, x2))
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, nil)
last(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[a24](nil, nil)
equal_sort[a24](nil, cons(x0, x1))
equal_sort[a24](cons(x0, x1), nil)
equal_sort[a24](cons(x0, x1), cons(x2, x3))
equal_sort[a42](witness_sort[a42], witness_sort[a42])
IF(false, x68, y51, xs33) → DEL(x68, xs33)
DEL(x16, cons(y11, xs7)) → IF(eq(x16, y11), x16, y11, xs7)
eq(0, 0) → true
eq(0, s(y24)) → false
eq(s(x41), 0) → false
eq(s(x50), s(y37)) → eq(x50, y37)
del'(x0, cons(x1, x2))
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, nil)
last(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[a24](nil, nil)
equal_sort[a24](nil, cons(x0, x1))
equal_sort[a24](cons(x0, x1), nil)
equal_sort[a24](cons(x0, x1), cons(x2, x3))
equal_sort[a42](witness_sort[a42], witness_sort[a42])
del'(x0, cons(x1, x2))
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, nil)
last(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[a24](nil, nil)
equal_sort[a24](nil, cons(x0, x1))
equal_sort[a24](cons(x0, x1), nil)
equal_sort[a24](cons(x0, x1), cons(x2, x3))
equal_sort[a42](witness_sort[a42], witness_sort[a42])
IF(false, x68, y51, xs33) → DEL(x68, xs33)
DEL(x16, cons(y11, xs7)) → IF(eq(x16, y11), x16, y11, xs7)
eq(0, 0) → true
eq(0, s(y24)) → false
eq(s(x41), 0) → false
eq(s(x50), s(y37)) → eq(x50, y37)
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:
LAST(cons(x7, cons(y4, xs2))) → LAST(cons(y4, xs2))
del'(x16, cons(y11, xs7)) → if'(eq(x16, y11), x16, y11, xs7)
if'(true, x59, y44, xs28) → true
if'(false, x68, y51, xs33) → del'(x68, xs33)
del'(x77, nil) → false
last(cons(x, nil)) → x
last(cons(x7, cons(y4, xs2))) → last(cons(y4, xs2))
del(x16, cons(y11, xs7)) → if(eq(x16, y11), x16, y11, xs7)
eq(0, 0) → true
eq(0, s(y24)) → false
eq(s(x41), 0) → false
eq(s(x50), s(y37)) → eq(x50, y37)
if(true, x59, y44, xs28) → xs28
if(false, x68, y51, xs33) → cons(y51, del(x68, xs33))
del(x77, nil) → nil
last(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(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a24](nil, nil) → true
equal_sort[a24](nil, cons(x0, x1)) → false
equal_sort[a24](cons(x0, x1), nil) → false
equal_sort[a24](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a24](x0, x2), equal_sort[a24](x1, x3))
equal_sort[a42](witness_sort[a42], witness_sort[a42]) → true
del'(x0, cons(x1, x2))
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, nil)
last(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[a24](nil, nil)
equal_sort[a24](nil, cons(x0, x1))
equal_sort[a24](cons(x0, x1), nil)
equal_sort[a24](cons(x0, x1), cons(x2, x3))
equal_sort[a42](witness_sort[a42], witness_sort[a42])
LAST(cons(x7, cons(y4, xs2))) → LAST(cons(y4, xs2))
del'(x0, cons(x1, x2))
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, nil)
last(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[a24](nil, nil)
equal_sort[a24](nil, cons(x0, x1))
equal_sort[a24](cons(x0, x1), nil)
equal_sort[a24](cons(x0, x1), cons(x2, x3))
equal_sort[a42](witness_sort[a42], witness_sort[a42])
del'(x0, cons(x1, x2))
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, nil)
last(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[a24](nil, nil)
equal_sort[a24](nil, cons(x0, x1))
equal_sort[a24](cons(x0, x1), nil)
equal_sort[a24](cons(x0, x1), cons(x2, x3))
equal_sort[a42](witness_sort[a42], witness_sort[a42])
LAST(cons(x7, cons(y4, xs2))) → LAST(cons(y4, xs2))
From the DPs we obtained the following set of size-change graphs:
IF'(false, x68, y51, xs33) → DEL'(x68, xs33)
DEL'(x16, cons(y11, xs7)) → IF'(eq(x16, y11), x16, y11, xs7)
del'(x16, cons(y11, xs7)) → if'(eq(x16, y11), x16, y11, xs7)
if'(true, x59, y44, xs28) → true
if'(false, x68, y51, xs33) → del'(x68, xs33)
del'(x77, nil) → false
last(cons(x, nil)) → x
last(cons(x7, cons(y4, xs2))) → last(cons(y4, xs2))
del(x16, cons(y11, xs7)) → if(eq(x16, y11), x16, y11, xs7)
eq(0, 0) → true
eq(0, s(y24)) → false
eq(s(x41), 0) → false
eq(s(x50), s(y37)) → eq(x50, y37)
if(true, x59, y44, xs28) → xs28
if(false, x68, y51, xs33) → cons(y51, del(x68, xs33))
del(x77, nil) → nil
last(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(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a24](nil, nil) → true
equal_sort[a24](nil, cons(x0, x1)) → false
equal_sort[a24](cons(x0, x1), nil) → false
equal_sort[a24](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a24](x0, x2), equal_sort[a24](x1, x3))
equal_sort[a42](witness_sort[a42], witness_sort[a42]) → true
del'(x0, cons(x1, x2))
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, nil)
last(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[a24](nil, nil)
equal_sort[a24](nil, cons(x0, x1))
equal_sort[a24](cons(x0, x1), nil)
equal_sort[a24](cons(x0, x1), cons(x2, x3))
equal_sort[a42](witness_sort[a42], witness_sort[a42])
IF'(false, x68, y51, xs33) → DEL'(x68, xs33)
DEL'(x16, cons(y11, xs7)) → IF'(eq(x16, y11), x16, y11, xs7)
eq(0, 0) → true
eq(0, s(y24)) → false
eq(s(x41), 0) → false
eq(s(x50), s(y37)) → eq(x50, y37)
del'(x0, cons(x1, x2))
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, nil)
last(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[a24](nil, nil)
equal_sort[a24](nil, cons(x0, x1))
equal_sort[a24](cons(x0, x1), nil)
equal_sort[a24](cons(x0, x1), cons(x2, x3))
equal_sort[a42](witness_sort[a42], witness_sort[a42])
del'(x0, cons(x1, x2))
if'(true, x0, x1, x2)
if'(false, x0, x1, x2)
del'(x0, nil)
last(cons(x0, nil))
last(cons(x0, cons(x1, x2)))
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
del(x0, nil)
last(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[a24](nil, nil)
equal_sort[a24](nil, cons(x0, x1))
equal_sort[a24](cons(x0, x1), nil)
equal_sort[a24](cons(x0, x1), cons(x2, x3))
equal_sort[a42](witness_sort[a42], witness_sort[a42])
IF'(false, x68, y51, xs33) → DEL'(x68, xs33)
DEL'(x16, cons(y11, xs7)) → IF'(eq(x16, y11), x16, y11, xs7)
eq(0, 0) → true
eq(0, s(y24)) → false
eq(s(x41), 0) → false
eq(s(x50), s(y37)) → eq(x50, y37)
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: