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 QTRSRRRProof (⇔)
↳50 QTRS
↳51 RisEmptyProof (⇔)
↳52 TRUE
↳53 RisEmptyProof (⇔)
↳54 TRUE
↳55 RisEmptyProof (⇔)
↳56 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
nil > false > true > eq2
nil > false > [if4, del2] > [cons2, and2] > [if'4, del'2] > eq2
0 > false > true > eq2
0 > false > [if4, del2] > [cons2, and2] > [if'4, del'2] > eq2
s1 > eq2
equalbool2 > eq2
or2 > eq2
not1 > false > true > eq2
not1 > false > [if4, del2] > [cons2, and2] > [if'4, del'2] > eq2
isatrue1 > false > true > eq2
isatrue1 > false > [if4, del2] > [cons2, and2] > [if'4, del'2] > eq2
isafalse1 > false > true > eq2
isafalse1 > false > [if4, del2] > [cons2, and2] > [if'4, del'2] > eq2
equalsort[a4]2 > false > true > eq2
equalsort[a4]2 > false > [if4, del2] > [cons2, and2] > [if'4, del'2] > eq2
equalsort[a19]2 > eq2
equalsort[a37]2 > true > eq2
witnesssort[a37] > eq2
if4: [4,2,3,1]
eq2: multiset
if'4: [4,2,3,1]
equalsort[a19]2: multiset
true: multiset
or2: multiset
and2: [2,1]
0: multiset
del2: [2,1]
del'2: [2,1]
equalbool2: multiset
cons2: [2,1]
not1: [1]
equalsort[a4]2: multiset
witnesssort[a37]: multiset
isafalse1: multiset
false: multiset
s1: multiset
equalsort[a37]2: multiset
nil: multiset
isatrue1: [1]
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