0 QTRS
↳1 Overlay + Local Confluence (⇔, 0 ms)
↳2 QTRS
↳3 DependencyPairsProof (⇔, 0 ms)
↳4 QDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 QDP
↳10 QReductionProof (⇔, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 QDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 QDP
↳17 QReductionProof (⇔, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 QDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 QDP
↳24 QReductionProof (⇔, 0 ms)
↳25 QDP
↳26 QDPSizeChangeProof (⇔, 0 ms)
↳27 YES
↳28 QDP
↳29 UsableRulesProof (⇔, 0 ms)
↳30 QDP
↳31 QReductionProof (⇔, 0 ms)
↳32 QDP
↳33 QDPSizeChangeProof (⇔, 0 ms)
↳34 YES
↳35 QDP
↳36 UsableRulesProof (⇔, 0 ms)
↳37 QDP
↳38 QReductionProof (⇔, 0 ms)
↳39 QDP
↳40 TransformationProof (⇔, 0 ms)
↳41 QDP
↳42 TransformationProof (⇔, 0 ms)
↳43 QDP
↳44 Induction-Processor (⇒, 11 ms)
↳45 AND
↳46 QDP
↳47 UsableRulesProof (⇔, 0 ms)
↳48 QDP
↳49 QReductionProof (⇔, 0 ms)
↳50 QDP
↳51 Induction-Processor (⇒, 1 ms)
↳52 AND
↳53 QDP
↳54 PisEmptyProof (⇔, 0 ms)
↳55 YES
↳56 QTRS
↳57 QTRSRRRProof (⇔, 25 ms)
↳58 QTRS
↳59 QTRSRRRProof (⇔, 0 ms)
↳60 QTRS
↳61 RisEmptyProof (⇔, 0 ms)
↳62 YES
↳63 QTRS
↳64 QTRSRRRProof (⇔, 30 ms)
↳65 QTRS
↳66 RisEmptyProof (⇔, 0 ms)
↳67 YES
qsort(nil) → nil
qsort(cons(x, xs)) → append(qsort(filterlow(x, cons(x, xs))), cons(x, qsort(filterhigh(x, cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
qsort(nil) → nil
qsort(cons(x, xs)) → append(qsort(filterlow(x, cons(x, xs))), cons(x, qsort(filterhigh(x, cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
QSORT(cons(x, xs)) → APPEND(qsort(filterlow(x, cons(x, xs))), cons(x, qsort(filterhigh(x, cons(x, xs)))))
QSORT(cons(x, xs)) → QSORT(filterlow(x, cons(x, xs)))
QSORT(cons(x, xs)) → FILTERLOW(x, cons(x, xs))
QSORT(cons(x, xs)) → QSORT(filterhigh(x, cons(x, xs)))
QSORT(cons(x, xs)) → FILTERHIGH(x, cons(x, xs))
FILTERLOW(n, cons(x, xs)) → IF1(ge(n, x), n, x, xs)
FILTERLOW(n, cons(x, xs)) → GE(n, x)
IF1(true, n, x, xs) → FILTERLOW(n, xs)
IF1(false, n, x, xs) → FILTERLOW(n, xs)
FILTERHIGH(n, cons(x, xs)) → IF2(ge(x, n), n, x, xs)
FILTERHIGH(n, cons(x, xs)) → GE(x, n)
IF2(true, n, x, xs) → FILTERHIGH(n, xs)
IF2(false, n, x, xs) → FILTERHIGH(n, xs)
GE(s(x), s(y)) → GE(x, y)
APPEND(cons(x, xs), ys) → APPEND(xs, ys)
qsort(nil) → nil
qsort(cons(x, xs)) → append(qsort(filterlow(x, cons(x, xs))), cons(x, qsort(filterhigh(x, cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
APPEND(cons(x, xs), ys) → APPEND(xs, ys)
qsort(nil) → nil
qsort(cons(x, xs)) → append(qsort(filterlow(x, cons(x, xs))), cons(x, qsort(filterhigh(x, cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
APPEND(cons(x, xs), ys) → APPEND(xs, ys)
qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
APPEND(cons(x, xs), ys) → APPEND(xs, ys)
From the DPs we obtained the following set of size-change graphs:
GE(s(x), s(y)) → GE(x, y)
qsort(nil) → nil
qsort(cons(x, xs)) → append(qsort(filterlow(x, cons(x, xs))), cons(x, qsort(filterhigh(x, cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
GE(s(x), s(y)) → GE(x, y)
qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
GE(s(x), s(y)) → GE(x, y)
From the DPs we obtained the following set of size-change graphs:
IF2(true, n, x, xs) → FILTERHIGH(n, xs)
FILTERHIGH(n, cons(x, xs)) → IF2(ge(x, n), n, x, xs)
IF2(false, n, x, xs) → FILTERHIGH(n, xs)
qsort(nil) → nil
qsort(cons(x, xs)) → append(qsort(filterlow(x, cons(x, xs))), cons(x, qsort(filterhigh(x, cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
IF2(true, n, x, xs) → FILTERHIGH(n, xs)
FILTERHIGH(n, cons(x, xs)) → IF2(ge(x, n), n, x, xs)
IF2(false, n, x, xs) → FILTERHIGH(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
append(nil, ys)
append(cons(x0, x1), ys)
IF2(true, n, x, xs) → FILTERHIGH(n, xs)
FILTERHIGH(n, cons(x, xs)) → IF2(ge(x, n), n, x, xs)
IF2(false, n, x, xs) → FILTERHIGH(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
From the DPs we obtained the following set of size-change graphs:
IF1(true, n, x, xs) → FILTERLOW(n, xs)
FILTERLOW(n, cons(x, xs)) → IF1(ge(n, x), n, x, xs)
IF1(false, n, x, xs) → FILTERLOW(n, xs)
qsort(nil) → nil
qsort(cons(x, xs)) → append(qsort(filterlow(x, cons(x, xs))), cons(x, qsort(filterhigh(x, cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
IF1(true, n, x, xs) → FILTERLOW(n, xs)
FILTERLOW(n, cons(x, xs)) → IF1(ge(n, x), n, x, xs)
IF1(false, n, x, xs) → FILTERLOW(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
append(nil, ys)
append(cons(x0, x1), ys)
IF1(true, n, x, xs) → FILTERLOW(n, xs)
FILTERLOW(n, cons(x, xs)) → IF1(ge(n, x), n, x, xs)
IF1(false, n, x, xs) → FILTERLOW(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
From the DPs we obtained the following set of size-change graphs:
QSORT(cons(x, xs)) → QSORT(filterhigh(x, cons(x, xs)))
QSORT(cons(x, xs)) → QSORT(filterlow(x, cons(x, xs)))
qsort(nil) → nil
qsort(cons(x, xs)) → append(qsort(filterlow(x, cons(x, xs))), cons(x, qsort(filterhigh(x, cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
QSORT(cons(x, xs)) → QSORT(filterhigh(x, cons(x, xs)))
QSORT(cons(x, xs)) → QSORT(filterlow(x, cons(x, xs)))
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
qsort(nil)
qsort(cons(x0, x1))
append(nil, ys)
append(cons(x0, x1), ys)
QSORT(cons(x, xs)) → QSORT(filterhigh(x, cons(x, xs)))
QSORT(cons(x, xs)) → QSORT(filterlow(x, cons(x, xs)))
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
QSORT(cons(x, xs)) → QSORT(if2(ge(x, x), x, x, xs)) → QSORT(cons(x, xs)) → QSORT(if2(ge(x, x), x, x, xs))
QSORT(cons(x, xs)) → QSORT(filterlow(x, cons(x, xs)))
QSORT(cons(x, xs)) → QSORT(if2(ge(x, x), x, x, xs))
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
QSORT(cons(x, xs)) → QSORT(if1(ge(x, x), x, x, xs)) → QSORT(cons(x, xs)) → QSORT(if1(ge(x, x), x, x, xs))
QSORT(cons(x, xs)) → QSORT(if2(ge(x, x), x, x, xs))
QSORT(cons(x, xs)) → QSORT(if1(ge(x, x), x, x, xs))
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
POL(0) = 1
POL(QSORT(x1)) = x1
POL(cons(x1, x2)) = 1 + x2
POL(false_renamed) = 1
POL(filterhigh(x1, x2)) = x2
POL(filterlow(x1, x2)) = x2
POL(ge(x1, x2)) = 1
POL(if1(x1, x2, x3, x4)) = 1 + x4
POL(if2(x1, x2, x3, x4)) = x1 + x4
POL(nil) = 0
POL(s(x1)) = x1
POL(true_renamed) = 1
proof of internal # AProVE Commit ID: 3a20a6ef7432c3f292db1a8838479c42bf5e3b22 root 20240618 unpublished Partial correctness of the following Program [x, v21, v22, v23, v24, v25, v26, v27, v28, v29, n1, x5, xs2, n2, x6, x8, xs5, n3, n5, x1, x2, x3, y, n'', n4, x7, xs4, n, x'', n', x4] equal_bool(true, false) -> false equal_bool(false, true) -> false equal_bool(true, true) -> true equal_bool(false, false) -> true true and x -> x false and x -> false true or x -> true false or x -> x not(false) -> true not(true) -> false isa_true(true) -> true isa_true(false) -> false isa_false(true) -> false isa_false(false) -> true equal_sort[a0](0, 0) -> true equal_sort[a0](0, s(v21)) -> false equal_sort[a0](s(v22), 0) -> false equal_sort[a0](s(v22), s(v23)) -> equal_sort[a0](v22, v23) equal_sort[a2](cons(v24, v25), cons(v26, v27)) -> equal_sort[a0](v24, v26) and equal_sort[a2](v25, v27) equal_sort[a2](cons(v24, v25), nil) -> false equal_sort[a2](nil, cons(v28, v29)) -> false equal_sort[a2](nil, nil) -> true equal_sort[a33](true_renamed, true_renamed) -> true equal_sort[a33](true_renamed, false_renamed) -> false equal_sort[a33](false_renamed, true_renamed) -> false equal_sort[a33](false_renamed, false_renamed) -> true equal_sort[a57](witness_sort[a57], witness_sort[a57]) -> true if2'(true_renamed, n1, x5, xs2) -> true if2'(false_renamed, n2, x6, nil) -> false if2'(false_renamed, n2, x6, cons(x8, xs5)) -> if2'(ge(x8, n2), n2, x8, xs5) filterhigh'(n3, nil) -> false equal_sort[a33](ge(x8, n5), true_renamed) -> true | filterhigh'(n5, cons(x8, xs5)) -> true equal_sort[a33](ge(x8, n5), true_renamed) -> false | filterhigh'(n5, cons(x8, xs5)) -> filterhigh'(n5, xs5) ge(x1, 0) -> true_renamed ge(0, s(x2)) -> false_renamed ge(s(x3), s(y)) -> ge(x3, y) filterlow(n'', nil) -> nil equal_sort[a33](ge(n4, x7), true_renamed) -> true | filterlow(n4, cons(x7, xs4)) -> filterlow(n4, xs4) equal_sort[a33](ge(n4, x7), true_renamed) -> false | filterlow(n4, cons(x7, xs4)) -> cons(x7, filterlow(n4, xs4)) filterhigh(n3, nil) -> nil equal_sort[a33](ge(x8, n5), true_renamed) -> true | filterhigh(n5, cons(x8, xs5)) -> filterhigh(n5, xs5) equal_sort[a33](ge(x8, n5), true_renamed) -> false | filterhigh(n5, cons(x8, xs5)) -> cons(x8, filterhigh(n5, xs5)) if1(true_renamed, n, x'', nil) -> nil if1(true_renamed, n, x'', cons(x7, xs4)) -> if1(ge(n, x7), n, x7, xs4) if1(false_renamed, n', x4, nil) -> cons(x4, nil) if1(false_renamed, n', x4, cons(x7, xs4)) -> cons(x4, if1(ge(n', x7), n', x7, xs4)) if2(true_renamed, n1, x5, nil) -> nil if2(true_renamed, n1, x5, cons(x8, xs5)) -> if2(ge(x8, n1), n1, x8, xs5) if2(false_renamed, n2, x6, nil) -> cons(x6, nil) if2(false_renamed, n2, x6, cons(x8, xs5)) -> cons(x6, if2(ge(x8, n2), n2, x8, xs5)) using the following formula: x:sort[a0],xs:sort[a2].if2'(ge(x, x), x, x, xs)=true could be successfully shown: (0) Formula (1) Induction by data structure [EQUIVALENT, 0 ms] (2) AND (3) Formula (4) Symbolic evaluation [EQUIVALENT, 0 ms] (5) YES (6) Formula (7) Symbolic evaluation [EQUIVALENT, 0 ms] (8) Formula (9) Case Analysis [EQUIVALENT, 0 ms] (10) AND (11) Formula (12) Inverse Substitution [SOUND, 0 ms] (13) Formula (14) Induction by data structure [SOUND, 0 ms] (15) AND (16) Formula (17) Symbolic evaluation [EQUIVALENT, 0 ms] (18) YES (19) Formula (20) Symbolic evaluation under hypothesis [EQUIVALENT, 0 ms] (21) YES (22) Formula (23) Inverse Substitution [SOUND, 0 ms] (24) Formula (25) Induction by data structure [SOUND, 0 ms] (26) AND (27) Formula (28) Symbolic evaluation [EQUIVALENT, 0 ms] (29) YES (30) Formula (31) Symbolic evaluation under hypothesis [EQUIVALENT, 0 ms] (32) YES ---------------------------------------- (0) Obligation: Formula: x:sort[a0],xs:sort[a2].if2'(ge(x, x), x, x, xs)=true There are no hypotheses. ---------------------------------------- (1) Induction by data structure (EQUIVALENT) Induction by data structure sort[a0] generates the following cases: 1. Base Case: Formula: xs:sort[a2].if2'(ge(0, 0), 0, 0, xs)=true There are no hypotheses. 1. Step Case: Formula: n:sort[a0],xs:sort[a2].if2'(ge(s(n), s(n)), s(n), s(n), xs)=true Hypotheses: n:sort[a0],!xs:sort[a2].if2'(ge(n, n), n, n, xs)=true ---------------------------------------- (2) Complex Obligation (AND) ---------------------------------------- (3) Obligation: Formula: xs:sort[a2].if2'(ge(0, 0), 0, 0, xs)=true There are no hypotheses. ---------------------------------------- (4) Symbolic evaluation (EQUIVALENT) Could be reduced to the following new obligation by simple symbolic evaluation: True ---------------------------------------- (5) YES ---------------------------------------- (6) Obligation: Formula: n:sort[a0],xs:sort[a2].if2'(ge(s(n), s(n)), s(n), s(n), xs)=true Hypotheses: n:sort[a0],!xs:sort[a2].if2'(ge(n, n), n, n, xs)=true ---------------------------------------- (7) Symbolic evaluation (EQUIVALENT) Could be shown by simple symbolic evaluation. ---------------------------------------- (8) Obligation: Formula: n:sort[a0],xs:sort[a2].if2'(ge(n, n), s(n), s(n), xs)=true Hypotheses: n:sort[a0],!xs:sort[a2].if2'(ge(n, n), n, n, xs)=true ---------------------------------------- (9) Case Analysis (EQUIVALENT) Case analysis leads to the following new obligations: Formula: n:sort[a0],x_1:sort[a0],x_2:sort[a2].if2'(ge(n, n), s(n), s(n), cons(x_1, x_2))=true Hypotheses: n:sort[a0],!xs:sort[a2].if2'(ge(n, n), n, n, xs)=true Formula: n:sort[a0].if2'(ge(n, n), s(n), s(n), nil)=true Hypotheses: n:sort[a0],!xs:sort[a2].if2'(ge(n, n), n, n, xs)=true ---------------------------------------- (10) Complex Obligation (AND) ---------------------------------------- (11) Obligation: Formula: n:sort[a0],x_1:sort[a0],x_2:sort[a2].if2'(ge(n, n), s(n), s(n), cons(x_1, x_2))=true Hypotheses: n:sort[a0],!xs:sort[a2].if2'(ge(n, n), n, n, xs)=true ---------------------------------------- (12) Inverse Substitution (SOUND) The formula could be generalised by inverse substitution to: n:sort[a0],n':sort[a0],x_1:sort[a0],x_2:sort[a2].if2'(ge(n, n), n', n', cons(x_1, x_2))=true Inverse substitution used: [s(n)/n'] ---------------------------------------- (13) Obligation: Formula: n:sort[a0],n':sort[a0],x_1:sort[a0],x_2:sort[a2].if2'(ge(n, n), n', n', cons(x_1, x_2))=true Hypotheses: n:sort[a0],!xs:sort[a2].if2'(ge(n, n), n, n, xs)=true ---------------------------------------- (14) Induction by data structure (SOUND) Induction by data structure sort[a0] generates the following cases: 1. Base Case: Formula: n':sort[a0],x_1:sort[a0],x_2:sort[a2].if2'(ge(0, 0), n', n', cons(x_1, x_2))=true There are no hypotheses. 1. Step Case: Formula: n'':sort[a0],n':sort[a0],x_1:sort[a0],x_2:sort[a2].if2'(ge(s(n''), s(n'')), n', n', cons(x_1, x_2))=true Hypotheses: n'':sort[a0],!n':sort[a0],!x_1:sort[a0],!x_2:sort[a2].if2'(ge(n'', n''), n', n', cons(x_1, x_2))=true ---------------------------------------- (15) Complex Obligation (AND) ---------------------------------------- (16) Obligation: Formula: n':sort[a0],x_1:sort[a0],x_2:sort[a2].if2'(ge(0, 0), n', n', cons(x_1, x_2))=true There are no hypotheses. ---------------------------------------- (17) Symbolic evaluation (EQUIVALENT) Could be reduced to the following new obligation by simple symbolic evaluation: True ---------------------------------------- (18) YES ---------------------------------------- (19) Obligation: Formula: n'':sort[a0],n':sort[a0],x_1:sort[a0],x_2:sort[a2].if2'(ge(s(n''), s(n'')), n', n', cons(x_1, x_2))=true Hypotheses: n'':sort[a0],!n':sort[a0],!x_1:sort[a0],!x_2:sort[a2].if2'(ge(n'', n''), n', n', cons(x_1, x_2))=true ---------------------------------------- (20) Symbolic evaluation under hypothesis (EQUIVALENT) Could be shown using symbolic evaluation under hypothesis, by using the following hypotheses: n'':sort[a0],!n':sort[a0],!x_1:sort[a0],!x_2:sort[a2].if2'(ge(n'', n''), n', n', cons(x_1, x_2))=true ---------------------------------------- (21) YES ---------------------------------------- (22) Obligation: Formula: n:sort[a0].if2'(ge(n, n), s(n), s(n), nil)=true Hypotheses: n:sort[a0],!xs:sort[a2].if2'(ge(n, n), n, n, xs)=true ---------------------------------------- (23) Inverse Substitution (SOUND) The formula could be generalised by inverse substitution to: n:sort[a0],n':sort[a0].if2'(ge(n, n), n', n', nil)=true Inverse substitution used: [s(n)/n'] ---------------------------------------- (24) Obligation: Formula: n:sort[a0],n':sort[a0].if2'(ge(n, n), n', n', nil)=true Hypotheses: n:sort[a0],!xs:sort[a2].if2'(ge(n, n), n, n, xs)=true ---------------------------------------- (25) Induction by data structure (SOUND) Induction by data structure sort[a0] generates the following cases: 1. Base Case: Formula: n':sort[a0].if2'(ge(0, 0), n', n', nil)=true There are no hypotheses. 1. Step Case: Formula: n'':sort[a0],n':sort[a0].if2'(ge(s(n''), s(n'')), n', n', nil)=true Hypotheses: n'':sort[a0],!n':sort[a0].if2'(ge(n'', n''), n', n', nil)=true ---------------------------------------- (26) Complex Obligation (AND) ---------------------------------------- (27) Obligation: Formula: n':sort[a0].if2'(ge(0, 0), n', n', nil)=true There are no hypotheses. ---------------------------------------- (28) Symbolic evaluation (EQUIVALENT) Could be reduced to the following new obligation by simple symbolic evaluation: True ---------------------------------------- (29) YES ---------------------------------------- (30) Obligation: Formula: n'':sort[a0],n':sort[a0].if2'(ge(s(n''), s(n'')), n', n', nil)=true Hypotheses: n'':sort[a0],!n':sort[a0].if2'(ge(n'', n''), n', n', nil)=true ---------------------------------------- (31) Symbolic evaluation under hypothesis (EQUIVALENT) Could be shown using symbolic evaluation under hypothesis, by using the following hypotheses: n'':sort[a0],!n':sort[a0].if2'(ge(n'', n''), n', n', nil)=true ---------------------------------------- (32) YES
QSORT(cons(x, xs)) → QSORT(if1(ge(x, x), x, x, xs))
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
QSORT(cons(x, xs)) → QSORT(if1(ge(x, x), x, x, xs))
ge(x, 0) → true
ge(s(x), s(y)) → ge(x, y)
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
ge(0, s(x)) → false
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
QSORT(cons(x, xs)) → QSORT(if1(ge(x, x), x, x, xs))
ge(x, 0) → true
ge(s(x), s(y)) → ge(x, y)
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
ge(0, s(x)) → false
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
POL(0) = 1
POL(QSORT(x1)) = x1
POL(cons(x1, x2)) = 1 + x2
POL(false_renamed) = 1
POL(filterlow(x1, x2)) = x2
POL(ge(x1, x2)) = 1
POL(if1(x1, x2, x3, x4)) = x1 + x4
POL(nil) = 0
POL(s(x1)) = x1
POL(true_renamed) = 1
proof of internal # AProVE Commit ID: 3a20a6ef7432c3f292db1a8838479c42bf5e3b22 root 20240618 unpublished Partial correctness of the following Program [x, v13, v14, v15, v16, v17, v18, v19, v20, v21, n, x1, xs', n'', x3, x2, xs'', n1, n', x', x'', y, x4] equal_bool(true, false) -> false equal_bool(false, true) -> false equal_bool(true, true) -> true equal_bool(false, false) -> true true and x -> x false and x -> false true or x -> true false or x -> x not(false) -> true not(true) -> false isa_true(true) -> true isa_true(false) -> false isa_false(true) -> false isa_false(false) -> true equal_sort[a0](0, 0) -> true equal_sort[a0](0, s(v13)) -> false equal_sort[a0](s(v14), 0) -> false equal_sort[a0](s(v14), s(v15)) -> equal_sort[a0](v14, v15) equal_sort[a5](cons(v16, v17), cons(v18, v19)) -> equal_sort[a0](v16, v18) and equal_sort[a5](v17, v19) equal_sort[a5](cons(v16, v17), nil) -> false equal_sort[a5](nil, cons(v20, v21)) -> false equal_sort[a5](nil, nil) -> true equal_sort[a18](true_renamed, true_renamed) -> true equal_sort[a18](true_renamed, false_renamed) -> false equal_sort[a18](false_renamed, true_renamed) -> false equal_sort[a18](false_renamed, false_renamed) -> true equal_sort[a37](witness_sort[a37], witness_sort[a37]) -> true if1'(true_renamed, n, x1, xs') -> true if1'(false_renamed, n'', x3, cons(x2, xs'')) -> if1'(ge(n'', x2), n'', x2, xs'') if1'(false_renamed, n'', x3, nil) -> false filterlow'(n1, nil) -> false equal_sort[a18](ge(n', x2), true_renamed) -> true | filterlow'(n', cons(x2, xs'')) -> true equal_sort[a18](ge(n', x2), true_renamed) -> false | filterlow'(n', cons(x2, xs'')) -> filterlow'(n', xs'') ge(x', 0) -> true_renamed ge(s(x''), s(y)) -> ge(x'', y) ge(0, s(x4)) -> false_renamed filterlow(n1, nil) -> nil equal_sort[a18](ge(n', x2), true_renamed) -> true | filterlow(n', cons(x2, xs'')) -> filterlow(n', xs'') equal_sort[a18](ge(n', x2), true_renamed) -> false | filterlow(n', cons(x2, xs'')) -> cons(x2, filterlow(n', xs'')) if1(true_renamed, n, x1, cons(x2, xs'')) -> if1(ge(n, x2), n, x2, xs'') if1(true_renamed, n, x1, nil) -> nil if1(false_renamed, n'', x3, cons(x2, xs'')) -> cons(x3, if1(ge(n'', x2), n'', x2, xs'')) if1(false_renamed, n'', x3, nil) -> cons(x3, nil) using the following formula: x:sort[a0],xs:sort[a5].if1'(ge(x, x), x, x, xs)=true could be successfully shown: (0) Formula (1) Induction by data structure [EQUIVALENT, 0 ms] (2) AND (3) Formula (4) Symbolic evaluation [EQUIVALENT, 0 ms] (5) YES (6) Formula (7) Symbolic evaluation [EQUIVALENT, 0 ms] (8) Formula (9) Case Analysis [EQUIVALENT, 0 ms] (10) AND (11) Formula (12) Inverse Substitution [SOUND, 0 ms] (13) Formula (14) Induction by data structure [SOUND, 0 ms] (15) AND (16) Formula (17) Symbolic evaluation [EQUIVALENT, 0 ms] (18) YES (19) Formula (20) Symbolic evaluation under hypothesis [EQUIVALENT, 0 ms] (21) YES (22) Formula (23) Inverse Substitution [SOUND, 0 ms] (24) Formula (25) Induction by data structure [SOUND, 0 ms] (26) AND (27) Formula (28) Symbolic evaluation [EQUIVALENT, 0 ms] (29) YES (30) Formula (31) Symbolic evaluation under hypothesis [EQUIVALENT, 0 ms] (32) YES ---------------------------------------- (0) Obligation: Formula: x:sort[a0],xs:sort[a5].if1'(ge(x, x), x, x, xs)=true There are no hypotheses. ---------------------------------------- (1) Induction by data structure (EQUIVALENT) Induction by data structure sort[a0] generates the following cases: 1. Base Case: Formula: xs:sort[a5].if1'(ge(0, 0), 0, 0, xs)=true There are no hypotheses. 1. Step Case: Formula: n:sort[a0],xs:sort[a5].if1'(ge(s(n), s(n)), s(n), s(n), xs)=true Hypotheses: n:sort[a0],!xs:sort[a5].if1'(ge(n, n), n, n, xs)=true ---------------------------------------- (2) Complex Obligation (AND) ---------------------------------------- (3) Obligation: Formula: xs:sort[a5].if1'(ge(0, 0), 0, 0, xs)=true There are no hypotheses. ---------------------------------------- (4) Symbolic evaluation (EQUIVALENT) Could be reduced to the following new obligation by simple symbolic evaluation: True ---------------------------------------- (5) YES ---------------------------------------- (6) Obligation: Formula: n:sort[a0],xs:sort[a5].if1'(ge(s(n), s(n)), s(n), s(n), xs)=true Hypotheses: n:sort[a0],!xs:sort[a5].if1'(ge(n, n), n, n, xs)=true ---------------------------------------- (7) Symbolic evaluation (EQUIVALENT) Could be shown by simple symbolic evaluation. ---------------------------------------- (8) Obligation: Formula: n:sort[a0],xs:sort[a5].if1'(ge(n, n), s(n), s(n), xs)=true Hypotheses: n:sort[a0],!xs:sort[a5].if1'(ge(n, n), n, n, xs)=true ---------------------------------------- (9) Case Analysis (EQUIVALENT) Case analysis leads to the following new obligations: Formula: n:sort[a0],x_1:sort[a0],x_2:sort[a5].if1'(ge(n, n), s(n), s(n), cons(x_1, x_2))=true Hypotheses: n:sort[a0],!xs:sort[a5].if1'(ge(n, n), n, n, xs)=true Formula: n:sort[a0].if1'(ge(n, n), s(n), s(n), nil)=true Hypotheses: n:sort[a0],!xs:sort[a5].if1'(ge(n, n), n, n, xs)=true ---------------------------------------- (10) Complex Obligation (AND) ---------------------------------------- (11) Obligation: Formula: n:sort[a0],x_1:sort[a0],x_2:sort[a5].if1'(ge(n, n), s(n), s(n), cons(x_1, x_2))=true Hypotheses: n:sort[a0],!xs:sort[a5].if1'(ge(n, n), n, n, xs)=true ---------------------------------------- (12) Inverse Substitution (SOUND) The formula could be generalised by inverse substitution to: n:sort[a0],n':sort[a0],x_1:sort[a0],x_2:sort[a5].if1'(ge(n, n), n', n', cons(x_1, x_2))=true Inverse substitution used: [s(n)/n'] ---------------------------------------- (13) Obligation: Formula: n:sort[a0],n':sort[a0],x_1:sort[a0],x_2:sort[a5].if1'(ge(n, n), n', n', cons(x_1, x_2))=true Hypotheses: n:sort[a0],!xs:sort[a5].if1'(ge(n, n), n, n, xs)=true ---------------------------------------- (14) Induction by data structure (SOUND) Induction by data structure sort[a0] generates the following cases: 1. Base Case: Formula: n':sort[a0],x_1:sort[a0],x_2:sort[a5].if1'(ge(0, 0), n', n', cons(x_1, x_2))=true There are no hypotheses. 1. Step Case: Formula: n'':sort[a0],n':sort[a0],x_1:sort[a0],x_2:sort[a5].if1'(ge(s(n''), s(n'')), n', n', cons(x_1, x_2))=true Hypotheses: n'':sort[a0],!n':sort[a0],!x_1:sort[a0],!x_2:sort[a5].if1'(ge(n'', n''), n', n', cons(x_1, x_2))=true ---------------------------------------- (15) Complex Obligation (AND) ---------------------------------------- (16) Obligation: Formula: n':sort[a0],x_1:sort[a0],x_2:sort[a5].if1'(ge(0, 0), n', n', cons(x_1, x_2))=true There are no hypotheses. ---------------------------------------- (17) Symbolic evaluation (EQUIVALENT) Could be reduced to the following new obligation by simple symbolic evaluation: True ---------------------------------------- (18) YES ---------------------------------------- (19) Obligation: Formula: n'':sort[a0],n':sort[a0],x_1:sort[a0],x_2:sort[a5].if1'(ge(s(n''), s(n'')), n', n', cons(x_1, x_2))=true Hypotheses: n'':sort[a0],!n':sort[a0],!x_1:sort[a0],!x_2:sort[a5].if1'(ge(n'', n''), n', n', cons(x_1, x_2))=true ---------------------------------------- (20) Symbolic evaluation under hypothesis (EQUIVALENT) Could be shown using symbolic evaluation under hypothesis, by using the following hypotheses: n'':sort[a0],!n':sort[a0],!x_1:sort[a0],!x_2:sort[a5].if1'(ge(n'', n''), n', n', cons(x_1, x_2))=true ---------------------------------------- (21) YES ---------------------------------------- (22) Obligation: Formula: n:sort[a0].if1'(ge(n, n), s(n), s(n), nil)=true Hypotheses: n:sort[a0],!xs:sort[a5].if1'(ge(n, n), n, n, xs)=true ---------------------------------------- (23) Inverse Substitution (SOUND) The formula could be generalised by inverse substitution to: n:sort[a0],n':sort[a0].if1'(ge(n, n), n', n', nil)=true Inverse substitution used: [s(n)/n'] ---------------------------------------- (24) Obligation: Formula: n:sort[a0],n':sort[a0].if1'(ge(n, n), n', n', nil)=true Hypotheses: n:sort[a0],!xs:sort[a5].if1'(ge(n, n), n, n, xs)=true ---------------------------------------- (25) Induction by data structure (SOUND) Induction by data structure sort[a0] generates the following cases: 1. Base Case: Formula: n':sort[a0].if1'(ge(0, 0), n', n', nil)=true There are no hypotheses. 1. Step Case: Formula: n'':sort[a0],n':sort[a0].if1'(ge(s(n''), s(n'')), n', n', nil)=true Hypotheses: n'':sort[a0],!n':sort[a0].if1'(ge(n'', n''), n', n', nil)=true ---------------------------------------- (26) Complex Obligation (AND) ---------------------------------------- (27) Obligation: Formula: n':sort[a0].if1'(ge(0, 0), n', n', nil)=true There are no hypotheses. ---------------------------------------- (28) Symbolic evaluation (EQUIVALENT) Could be reduced to the following new obligation by simple symbolic evaluation: True ---------------------------------------- (29) YES ---------------------------------------- (30) Obligation: Formula: n'':sort[a0],n':sort[a0].if1'(ge(s(n''), s(n'')), n', n', nil)=true Hypotheses: n'':sort[a0],!n':sort[a0].if1'(ge(n'', n''), n', n', nil)=true ---------------------------------------- (31) Symbolic evaluation under hypothesis (EQUIVALENT) Could be shown using symbolic evaluation under hypothesis, by using the following hypotheses: n'':sort[a0],!n':sort[a0].if1'(ge(n'', n''), n', n', nil)=true ---------------------------------------- (32) YES
ge(x, 0) → true
ge(s(x), s(y)) → ge(x, y)
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
ge(0, s(x)) → false
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
if1'(true_renamed, n, x1, xs') → true
filterlow'(n', cons(x2, xs'')) → if1'(ge(n', x2), n', x2, xs'')
if1'(false_renamed, n'', x3, xs1) → filterlow'(n'', xs1)
filterlow'(n1, nil) → false
ge(x', 0) → true_renamed
ge(s(x''), s(y)) → ge(x'', y)
if1(true_renamed, n, x1, xs') → filterlow(n, xs')
filterlow(n', cons(x2, xs'')) → if1(ge(n', x2), n', x2, xs'')
if1(false_renamed, n'', x3, xs1) → cons(x3, filterlow(n'', xs1))
filterlow(n1, nil) → nil
ge(0, s(x4)) → false_renamed
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(v13)) → false
equal_sort[a0](s(v14), 0) → false
equal_sort[a0](s(v14), s(v15)) → equal_sort[a0](v14, v15)
equal_sort[a5](cons(v16, v17), cons(v18, v19)) → and(equal_sort[a0](v16, v18), equal_sort[a5](v17, v19))
equal_sort[a5](cons(v16, v17), nil) → false
equal_sort[a5](nil, cons(v20, v21)) → false
equal_sort[a5](nil, nil) → true
equal_sort[a18](true_renamed, true_renamed) → true
equal_sort[a18](true_renamed, false_renamed) → false
equal_sort[a18](false_renamed, true_renamed) → false
equal_sort[a18](false_renamed, false_renamed) → true
equal_sort[a37](witness_sort[a37], witness_sort[a37]) → true
[if1'4, filterlow'2] > [truerenamed, ge2, false, if14, filterlow2, not1] > [true, witnesssort[a37]] > and2
[if1'4, filterlow'2] > [truerenamed, ge2, false, if14, filterlow2, not1] > cons2 > and2
[if1'4, filterlow'2] > [truerenamed, ge2, false, if14, filterlow2, not1] > nil > and2
0 > [true, witnesssort[a37]] > and2
s1 > falserenamed > [truerenamed, ge2, false, if14, filterlow2, not1] > [true, witnesssort[a37]] > and2
s1 > falserenamed > [truerenamed, ge2, false, if14, filterlow2, not1] > cons2 > and2
s1 > falserenamed > [truerenamed, ge2, false, if14, filterlow2, not1] > nil > and2
s1 > equalsort[a0]2 > [truerenamed, ge2, false, if14, filterlow2, not1] > [true, witnesssort[a37]] > and2
s1 > equalsort[a0]2 > [truerenamed, ge2, false, if14, filterlow2, not1] > cons2 > and2
s1 > equalsort[a0]2 > [truerenamed, ge2, false, if14, filterlow2, not1] > nil > and2
equalbool2 > and2
or2 > [true, witnesssort[a37]] > and2
isafalse1 > [truerenamed, ge2, false, if14, filterlow2, not1] > [true, witnesssort[a37]] > and2
isafalse1 > [truerenamed, ge2, false, if14, filterlow2, not1] > cons2 > and2
isafalse1 > [truerenamed, ge2, false, if14, filterlow2, not1] > nil > and2
equalsort[a5]2 > equalsort[a0]2 > [truerenamed, ge2, false, if14, filterlow2, not1] > [true, witnesssort[a37]] > and2
equalsort[a5]2 > equalsort[a0]2 > [truerenamed, ge2, false, if14, filterlow2, not1] > cons2 > and2
equalsort[a5]2 > equalsort[a0]2 > [truerenamed, ge2, false, if14, filterlow2, not1] > nil > and2
equalsort[a18]2 > [true, witnesssort[a37]] > and2
equalsort[a37]2 > [true, witnesssort[a37]] > and2
if1'4: [4,2,3,1]
truerenamed: multiset
true: multiset
filterlow'2: [2,1]
cons2: multiset
ge2: [2,1]
falserenamed: multiset
nil: multiset
false: multiset
0: multiset
s1: [1]
if14: [4,2,1,3]
filterlow2: [2,1]
equalbool2: multiset
and2: multiset
or2: multiset
not1: multiset
isafalse1: multiset
equalsort[a0]2: [1,2]
equalsort[a5]2: multiset
equalsort[a18]2: multiset
equalsort[a37]2: multiset
witnesssort[a37]: multiset
if1'(true_renamed, n, x1, xs') → true
filterlow'(n', cons(x2, xs'')) → if1'(ge(n', x2), n', x2, xs'')
if1'(false_renamed, n'', x3, xs1) → filterlow'(n'', xs1)
filterlow'(n1, nil) → false
ge(x', 0) → true_renamed
ge(s(x''), s(y)) → ge(x'', y)
if1(true_renamed, n, x1, xs') → filterlow(n, xs')
filterlow(n', cons(x2, xs'')) → if1(ge(n', x2), n', x2, xs'')
if1(false_renamed, n'', x3, xs1) → cons(x3, filterlow(n'', xs1))
filterlow(n1, nil) → nil
ge(0, s(x4)) → false_renamed
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_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(v13)) → false
equal_sort[a0](s(v14), 0) → false
equal_sort[a0](s(v14), s(v15)) → equal_sort[a0](v14, v15)
equal_sort[a5](cons(v16, v17), cons(v18, v19)) → and(equal_sort[a0](v16, v18), equal_sort[a5](v17, v19))
equal_sort[a5](cons(v16, v17), nil) → false
equal_sort[a5](nil, cons(v20, v21)) → false
equal_sort[a5](nil, nil) → true
equal_sort[a18](true_renamed, true_renamed) → true
equal_sort[a18](true_renamed, false_renamed) → false
equal_sort[a18](false_renamed, true_renamed) → false
equal_sort[a18](false_renamed, false_renamed) → true
equal_sort[a37](witness_sort[a37], witness_sort[a37]) → true
isa_true(true) → true
isa_true(false) → false
isatrue1 > false > true
true=1
false=1
isa_true_1=0
isa_true(true) → true
isa_true(false) → false
if2'(true_renamed, n1, x5, xs2) → true
if2'(false_renamed, n2, x6, xs3) → filterhigh'(n2, xs3)
filterhigh'(n3, nil) → false
filterhigh'(n5, cons(x8, xs5)) → if2'(ge(x8, n5), n5, x8, xs5)
if1(true_renamed, n, x'', xs'') → filterlow(n, xs'')
ge(x1, 0) → true_renamed
ge(0, s(x2)) → false_renamed
ge(s(x3), s(y)) → ge(x3, y)
if1(false_renamed, n', x4, xs1) → cons(x4, filterlow(n', xs1))
filterlow(n'', nil) → nil
if2(true_renamed, n1, x5, xs2) → filterhigh(n1, xs2)
if2(false_renamed, n2, x6, xs3) → cons(x6, filterhigh(n2, xs3))
filterhigh(n3, nil) → nil
filterlow(n4, cons(x7, xs4)) → if1(ge(n4, x7), n4, x7, xs4)
filterhigh(n5, cons(x8, xs5)) → if2(ge(x8, n5), n5, x8, xs5)
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(v21)) → false
equal_sort[a0](s(v22), 0) → false
equal_sort[a0](s(v22), s(v23)) → equal_sort[a0](v22, v23)
equal_sort[a2](cons(v24, v25), cons(v26, v27)) → and(equal_sort[a0](v24, v26), equal_sort[a2](v25, v27))
equal_sort[a2](cons(v24, v25), nil) → false
equal_sort[a2](nil, cons(v28, v29)) → false
equal_sort[a2](nil, nil) → true
equal_sort[a33](true_renamed, true_renamed) → true
equal_sort[a33](true_renamed, false_renamed) → false
equal_sort[a33](false_renamed, true_renamed) → false
equal_sort[a33](false_renamed, false_renamed) → true
equal_sort[a57](witness_sort[a57], witness_sort[a57]) → true
[if2'4, filterhigh'2] > [ge2, if24, filterhigh2] > [cons2, and2]
nil > [truerenamed, true, false, equalsort[a57]2] > [if14, filterlow2] > [ge2, if24, filterhigh2] > [cons2, and2]
0 > [truerenamed, true, false, equalsort[a57]2] > [if14, filterlow2] > [ge2, if24, filterhigh2] > [cons2, and2]
0 > falserenamed > [ge2, if24, filterhigh2] > [cons2, and2]
s1 > [ge2, if24, filterhigh2] > [cons2, and2]
equalbool2 > [truerenamed, true, false, equalsort[a57]2] > [if14, filterlow2] > [ge2, if24, filterhigh2] > [cons2, and2]
or2 > [cons2, and2]
not1 > [cons2, and2]
isatrue1 > [cons2, and2]
isafalse1 > [cons2, and2]
[equalsort[a0]2, equalsort[a2]2] > [truerenamed, true, false, equalsort[a57]2] > [if14, filterlow2] > [ge2, if24, filterhigh2] > [cons2, and2]
equalsort[a33]2 > [truerenamed, true, false, equalsort[a57]2] > [if14, filterlow2] > [ge2, if24, filterhigh2] > [cons2, and2]
witnesssort[a57] > [cons2, and2]
if2'4: [2,4,1,3]
truerenamed: multiset
true: multiset
falserenamed: multiset
filterhigh'2: [1,2]
nil: multiset
false: multiset
cons2: multiset
ge2: [1,2]
if14: [2,4,3,1]
filterlow2: [1,2]
0: multiset
s1: [1]
if24: [4,2,1,3]
filterhigh2: [2,1]
equalbool2: [1,2]
and2: multiset
or2: multiset
not1: [1]
isatrue1: [1]
isafalse1: [1]
equalsort[a0]2: [2,1]
equalsort[a2]2: [2,1]
equalsort[a33]2: [1,2]
equalsort[a57]2: multiset
witnesssort[a57]: multiset
if2'(true_renamed, n1, x5, xs2) → true
if2'(false_renamed, n2, x6, xs3) → filterhigh'(n2, xs3)
filterhigh'(n3, nil) → false
filterhigh'(n5, cons(x8, xs5)) → if2'(ge(x8, n5), n5, x8, xs5)
if1(true_renamed, n, x'', xs'') → filterlow(n, xs'')
ge(x1, 0) → true_renamed
ge(0, s(x2)) → false_renamed
ge(s(x3), s(y)) → ge(x3, y)
if1(false_renamed, n', x4, xs1) → cons(x4, filterlow(n', xs1))
filterlow(n'', nil) → nil
if2(true_renamed, n1, x5, xs2) → filterhigh(n1, xs2)
if2(false_renamed, n2, x6, xs3) → cons(x6, filterhigh(n2, xs3))
filterhigh(n3, nil) → nil
filterlow(n4, cons(x7, xs4)) → if1(ge(n4, x7), n4, x7, xs4)
filterhigh(n5, cons(x8, xs5)) → if2(ge(x8, n5), n5, x8, xs5)
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(v21)) → false
equal_sort[a0](s(v22), 0) → false
equal_sort[a0](s(v22), s(v23)) → equal_sort[a0](v22, v23)
equal_sort[a2](cons(v24, v25), cons(v26, v27)) → and(equal_sort[a0](v24, v26), equal_sort[a2](v25, v27))
equal_sort[a2](cons(v24, v25), nil) → false
equal_sort[a2](nil, cons(v28, v29)) → false
equal_sort[a2](nil, nil) → true
equal_sort[a33](true_renamed, true_renamed) → true
equal_sort[a33](true_renamed, false_renamed) → false
equal_sort[a33](false_renamed, true_renamed) → false
equal_sort[a33](false_renamed, false_renamed) → true
equal_sort[a57](witness_sort[a57], witness_sort[a57]) → true