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 QTRSRRRProof (⇔)
↳40 QTRS
↳41 RisEmptyProof (⇔)
↳42 TRUE
↳43 RisEmptyProof (⇔)
↳44 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
s1 > eq2
s1 > equalsort[a0]2
not1 > [del'2, if'4, false, nil, 0, equalsort[a24]2] > true
not1 > [del'2, if'4, false, nil, 0, equalsort[a24]2] > [del2, if4] > [cons2, last1, and2] > eq2
isafalse1 > [del'2, if'4, false, nil, 0, equalsort[a24]2] > true
isafalse1 > [del'2, if'4, false, nil, 0, equalsort[a24]2] > [del2, if4] > [cons2, last1, and2] > eq2
equalsort[a42]2 > true
witnesssort[a42]: multiset
if4: [2,4,3,1]
eq2: [2,1]
if'4: [2,4,3,1]
last1: [1]
true: multiset
or2: [2,1]
equalsort[a42]2: multiset
and2: multiset
del2: [1,2]
0: multiset
del'2: [1,2]
equalbool2: [1,2]
equalsort[a0]2: [1,2]
cons2: [1,2]
equalsort[a24]2: multiset
not1: multiset
isafalse1: [1]
false: multiset
s1: [1]
nil: multiset
isatrue1: [1]
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