Termination w.r.t. Q proof of Applicative_first_order_05

Termination w.r.t. Q of the given QTRS could be proven:

0 QTRS

↳1 Overlay + Local Confluence (⇔, 0 ms)

↳2 QTRS

↳3 DependencyPairsProof (⇔, 116 ms)

↳4 QDP

↳5 DependencyGraphProof (⇔, 0 ms)

↳6 AND

    ↳7 QDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 QDP

        ↳10 ATransformationProof (⇔, 0 ms)

        ↳11 QDP

        ↳12 QReductionProof (⇔, 0 ms)

        ↳13 QDP

        ↳14 QDPSizeChangeProof (⇔, 0 ms)

        ↳15 YES

    ↳16 QDP

        ↳17 UsableRulesProof (⇔, 0 ms)

        ↳18 QDP

        ↳19 ATransformationProof (⇔, 0 ms)

        ↳20 QDP

        ↳21 QReductionProof (⇔, 0 ms)

        ↳22 QDP

        ↳23 QDPSizeChangeProof (⇔, 0 ms)

        ↳24 YES

    ↳25 QDP

        ↳26 UsableRulesProof (⇔, 0 ms)

        ↳27 QDP

        ↳28 ATransformationProof (⇔, 0 ms)

        ↳29 QDP

        ↳30 QReductionProof (⇔, 0 ms)

        ↳31 QDP

        ↳32 QDPSizeChangeProof (⇔, 0 ms)

        ↳33 YES

    ↳34 QDP

        ↳35 UsableRulesProof (⇔, 0 ms)

        ↳36 QDP

        ↳37 ATransformationProof (⇔, 0 ms)

        ↳38 QDP

        ↳39 QReductionProof (⇔, 0 ms)

        ↳40 QDP

        ↳41 QDPSizeChangeProof (⇔, 0 ms)

        ↳42 YES

    ↳43 QDP

        ↳44 UsableRulesProof (⇔, 0 ms)

        ↳45 QDP

        ↳46 ATransformationProof (⇔, 0 ms)

        ↳47 QDP

        ↳48 QReductionProof (⇔, 0 ms)

        ↳49 QDP

        ↳50 QDPOrderProof (⇔, 8 ms)

        ↳51 QDP

        ↳52 UsableRulesProof (⇔, 0 ms)

        ↳53 QDP

        ↳54 QReductionProof (⇔, 0 ms)

        ↳55 QDP

        ↳56 QDPOrderProof (⇔, 0 ms)

        ↳57 QDP

        ↳58 PisEmptyProof (⇔, 0 ms)

        ↳59 YES

    ↳60 QDP

        ↳61 UsableRulesProof (⇔, 0 ms)

        ↳62 QDP

        ↳63 ATransformationProof (⇔, 0 ms)

        ↳64 QDP

        ↳65 QReductionProof (⇔, 0 ms)

        ↳66 QDP

        ↳67 QDPSizeChangeProof (⇔, 0 ms)

        ↳68 YES

    ↳69 QDP

        ↳70 UsableRulesProof (⇔, 0 ms)

        ↳71 QDP

        ↳72 ATransformationProof (⇔, 0 ms)

        ↳73 QDP

        ↳74 QReductionProof (⇔, 0 ms)

        ↳75 QDP

        ↳76 QDPOrderProof (⇔, 0 ms)

        ↳77 QDP

        ↳78 PisEmptyProof (⇔, 0 ms)

        ↳79 YES

    ↳80 QDP

        ↳81 QDPSizeChangeProof (⇔, 0 ms)

        ↳82 YES

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

app'(app'(minus, x), 0) → x
app'(app'(minus, app'(s, x)), app'(s, y)) → app'(app'(minus, x), y)
app'(app'(quot, 0), app'(s, y)) → 0
app'(app'(quot, app'(s, x)), app'(s, y)) → app'(s, app'(app'(quot, app'(app'(minus, x), y)), app'(s, y)))
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(app'(low, n), nil) → nil
app'(app'(low, n), app'(app'(add, m), x)) → app'(app'(app'(if_low, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(if_low, true), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(low, n), x))
app'(app'(app'(if_low, false), n), app'(app'(add, m), x)) → app'(app'(low, n), x)
app'(app'(high, n), nil) → nil
app'(app'(high, n), app'(app'(add, m), x)) → app'(app'(app'(if_high, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(if_high, true), n), app'(app'(add, m), x)) → app'(app'(high, n), x)
app'(app'(app'(if_high, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(high, n), x))
app'(quicksort, nil) → nil
app'(quicksort, app'(app'(add, n), x)) → app'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

Q is empty.

(1) Overlay + Local Confluence (EQUIVALENT transformation)

The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.

(2) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

app'(app'(minus, x), 0) → x
app'(app'(minus, app'(s, x)), app'(s, y)) → app'(app'(minus, x), y)
app'(app'(quot, 0), app'(s, y)) → 0
app'(app'(quot, app'(s, x)), app'(s, y)) → app'(s, app'(app'(quot, app'(app'(minus, x), y)), app'(s, y)))
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(app'(low, n), nil) → nil
app'(app'(low, n), app'(app'(add, m), x)) → app'(app'(app'(if_low, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(if_low, true), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(low, n), x))
app'(app'(app'(if_low, false), n), app'(app'(add, m), x)) → app'(app'(low, n), x)
app'(app'(high, n), nil) → nil
app'(app'(high, n), app'(app'(add, m), x)) → app'(app'(app'(if_high, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(if_high, true), n), app'(app'(add, m), x)) → app'(app'(high, n), x)
app'(app'(app'(if_high, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(high, n), x))
app'(quicksort, nil) → nil
app'(quicksort, app'(app'(add, n), x)) → app'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(minus, x0), 0)
app'(app'(minus, app'(s, x0)), app'(s, x1))
app'(app'(quot, 0), app'(s, x0))
app'(app'(quot, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(app'(low, x0), nil)
app'(app'(low, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, false), x0), app'(app'(add, x1), x2))
app'(app'(high, x0), nil)
app'(app'(high, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, false), x0), app'(app'(add, x1), x2))
app'(quicksort, nil)
app'(quicksort, app'(app'(add, x0), x1))
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(4) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(minus, app'(s, x)), app'(s, y)) → APP'(app'(minus, x), y)
APP'(app'(minus, app'(s, x)), app'(s, y)) → APP'(minus, x)
APP'(app'(quot, app'(s, x)), app'(s, y)) → APP'(s, app'(app'(quot, app'(app'(minus, x), y)), app'(s, y)))
APP'(app'(quot, app'(s, x)), app'(s, y)) → APP'(app'(quot, app'(app'(minus, x), y)), app'(s, y))
APP'(app'(quot, app'(s, x)), app'(s, y)) → APP'(quot, app'(app'(minus, x), y))
APP'(app'(quot, app'(s, x)), app'(s, y)) → APP'(app'(minus, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) → APP'(minus, x)
APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(app'(le, x), y)
APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(le, x)
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(add, n), app'(app'(app, x), y))
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(app, x), y)
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app, x)
APP'(app'(low, n), app'(app'(add, m), x)) → APP'(app'(app'(if_low, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(low, n), app'(app'(add, m), x)) → APP'(app'(if_low, app'(app'(le, m), n)), n)
APP'(app'(low, n), app'(app'(add, m), x)) → APP'(if_low, app'(app'(le, m), n))
APP'(app'(low, n), app'(app'(add, m), x)) → APP'(app'(le, m), n)
APP'(app'(low, n), app'(app'(add, m), x)) → APP'(le, m)
APP'(app'(app'(if_low, true), n), app'(app'(add, m), x)) → APP'(app'(add, m), app'(app'(low, n), x))
APP'(app'(app'(if_low, true), n), app'(app'(add, m), x)) → APP'(app'(low, n), x)
APP'(app'(app'(if_low, true), n), app'(app'(add, m), x)) → APP'(low, n)
APP'(app'(app'(if_low, false), n), app'(app'(add, m), x)) → APP'(app'(low, n), x)
APP'(app'(app'(if_low, false), n), app'(app'(add, m), x)) → APP'(low, n)
APP'(app'(high, n), app'(app'(add, m), x)) → APP'(app'(app'(if_high, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(high, n), app'(app'(add, m), x)) → APP'(app'(if_high, app'(app'(le, m), n)), n)
APP'(app'(high, n), app'(app'(add, m), x)) → APP'(if_high, app'(app'(le, m), n))
APP'(app'(high, n), app'(app'(add, m), x)) → APP'(app'(le, m), n)
APP'(app'(high, n), app'(app'(add, m), x)) → APP'(le, m)
APP'(app'(app'(if_high, true), n), app'(app'(add, m), x)) → APP'(app'(high, n), x)
APP'(app'(app'(if_high, true), n), app'(app'(add, m), x)) → APP'(high, n)
APP'(app'(app'(if_high, false), n), app'(app'(add, m), x)) → APP'(app'(add, m), app'(app'(high, n), x))
APP'(app'(app'(if_high, false), n), app'(app'(add, m), x)) → APP'(app'(high, n), x)
APP'(app'(app'(if_high, false), n), app'(app'(add, m), x)) → APP'(high, n)
APP'(quicksort, app'(app'(add, n), x)) → APP'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))
APP'(quicksort, app'(app'(add, n), x)) → APP'(app, app'(quicksort, app'(app'(low, n), x)))
APP'(quicksort, app'(app'(add, n), x)) → APP'(quicksort, app'(app'(low, n), x))
APP'(quicksort, app'(app'(add, n), x)) → APP'(app'(low, n), x)
APP'(quicksort, app'(app'(add, n), x)) → APP'(low, n)
APP'(quicksort, app'(app'(add, n), x)) → APP'(app'(add, n), app'(quicksort, app'(app'(high, n), x)))
APP'(quicksort, app'(app'(add, n), x)) → APP'(quicksort, app'(app'(high, n), x))
APP'(quicksort, app'(app'(add, n), x)) → APP'(app'(high, n), x)
APP'(quicksort, app'(app'(add, n), x)) → APP'(high, n)
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(add, app'(f, x)), app'(app'(map, f), xs))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(add, app'(f, x))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(map, f), xs)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(filter2, app'(f, x)), f), x)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(filter2, app'(f, x)), f)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(filter2, app'(f, x))
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(add, x), app'(app'(filter, f), xs))
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(add, x)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(filter, f), xs)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(filter, f)
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(app'(filter, f), xs)
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(filter, f)

The TRS R consists of the following rules:

app'(app'(minus, x), 0) → x
app'(app'(minus, app'(s, x)), app'(s, y)) → app'(app'(minus, x), y)
app'(app'(quot, 0), app'(s, y)) → 0
app'(app'(quot, app'(s, x)), app'(s, y)) → app'(s, app'(app'(quot, app'(app'(minus, x), y)), app'(s, y)))
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(app'(low, n), nil) → nil
app'(app'(low, n), app'(app'(add, m), x)) → app'(app'(app'(if_low, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(if_low, true), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(low, n), x))
app'(app'(app'(if_low, false), n), app'(app'(add, m), x)) → app'(app'(low, n), x)
app'(app'(high, n), nil) → nil
app'(app'(high, n), app'(app'(add, m), x)) → app'(app'(app'(if_high, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(if_high, true), n), app'(app'(add, m), x)) → app'(app'(high, n), x)
app'(app'(app'(if_high, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(high, n), x))
app'(quicksort, nil) → nil
app'(quicksort, app'(app'(add, n), x)) → app'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(minus, x0), 0)
app'(app'(minus, app'(s, x0)), app'(s, x1))
app'(app'(quot, 0), app'(s, x0))
app'(app'(quot, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(app'(low, x0), nil)
app'(app'(low, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, false), x0), app'(app'(add, x1), x2))
app'(app'(high, x0), nil)
app'(app'(high, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, false), x0), app'(app'(add, x1), x2))
app'(quicksort, nil)
app'(quicksort, app'(app'(add, x0), x1))
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 8 SCCs with 38 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(app, x), y)

The TRS R consists of the following rules:

app'(app'(minus, x), 0) → x
app'(app'(minus, app'(s, x)), app'(s, y)) → app'(app'(minus, x), y)
app'(app'(quot, 0), app'(s, y)) → 0
app'(app'(quot, app'(s, x)), app'(s, y)) → app'(s, app'(app'(quot, app'(app'(minus, x), y)), app'(s, y)))
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(app'(low, n), nil) → nil
app'(app'(low, n), app'(app'(add, m), x)) → app'(app'(app'(if_low, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(if_low, true), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(low, n), x))
app'(app'(app'(if_low, false), n), app'(app'(add, m), x)) → app'(app'(low, n), x)
app'(app'(high, n), nil) → nil
app'(app'(high, n), app'(app'(add, m), x)) → app'(app'(app'(if_high, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(if_high, true), n), app'(app'(add, m), x)) → app'(app'(high, n), x)
app'(app'(app'(if_high, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(high, n), x))
app'(quicksort, nil) → nil
app'(quicksort, app'(app'(add, n), x)) → app'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(minus, x0), 0)
app'(app'(minus, app'(s, x0)), app'(s, x1))
app'(app'(quot, 0), app'(s, x0))
app'(app'(quot, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(app'(low, x0), nil)
app'(app'(low, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, false), x0), app'(app'(add, x1), x2))
app'(app'(high, x0), nil)
app'(app'(high, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, false), x0), app'(app'(add, x1), x2))
app'(quicksort, nil)
app'(quicksort, app'(app'(add, x0), x1))
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.

(8) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(9) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(app, x), y)

R is empty.
The set Q consists of the following terms:

app'(app'(minus, x0), 0)
app'(app'(minus, app'(s, x0)), app'(s, x1))
app'(app'(quot, 0), app'(s, x0))
app'(app'(quot, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(app'(low, x0), nil)
app'(app'(low, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, false), x0), app'(app'(add, x1), x2))
app'(app'(high, x0), nil)
app'(app'(high, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, false), x0), app'(app'(add, x1), x2))
app'(quicksort, nil)
app'(quicksort, app'(app'(add, x0), x1))
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.

(10) ATransformationProof (EQUIVALENT transformation)

We have applied the A-Transformation [FROCOS05] to get from an applicative problem to a standard problem.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

app1(add(n, x), y) → app1(x, y)

R is empty.
The set Q consists of the following terms:

minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
quicksort(nil)
quicksort(add(x0, x1))
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.

(12) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
quicksort(nil)
quicksort(add(x0, x1))
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

(13) Obligation:

Q DP problem:
The TRS P consists of the following rules:

app1(add(n, x), y) → app1(x, y)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(14) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

app1(add(n, x), y) → app1(x, y)
The graph contains the following edges 1 > 1, 2 >= 2

(15) YES

(16) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(app'(le, x), y)

The TRS R consists of the following rules:

app'(app'(minus, x), 0) → x
app'(app'(minus, app'(s, x)), app'(s, y)) → app'(app'(minus, x), y)
app'(app'(quot, 0), app'(s, y)) → 0
app'(app'(quot, app'(s, x)), app'(s, y)) → app'(s, app'(app'(quot, app'(app'(minus, x), y)), app'(s, y)))
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(app'(low, n), nil) → nil
app'(app'(low, n), app'(app'(add, m), x)) → app'(app'(app'(if_low, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(if_low, true), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(low, n), x))
app'(app'(app'(if_low, false), n), app'(app'(add, m), x)) → app'(app'(low, n), x)
app'(app'(high, n), nil) → nil
app'(app'(high, n), app'(app'(add, m), x)) → app'(app'(app'(if_high, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(if_high, true), n), app'(app'(add, m), x)) → app'(app'(high, n), x)
app'(app'(app'(if_high, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(high, n), x))
app'(quicksort, nil) → nil
app'(quicksort, app'(app'(add, n), x)) → app'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(minus, x0), 0)
app'(app'(minus, app'(s, x0)), app'(s, x1))
app'(app'(quot, 0), app'(s, x0))
app'(app'(quot, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(app'(low, x0), nil)
app'(app'(low, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, false), x0), app'(app'(add, x1), x2))
app'(app'(high, x0), nil)
app'(app'(high, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, false), x0), app'(app'(add, x1), x2))
app'(quicksort, nil)
app'(quicksort, app'(app'(add, x0), x1))
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.

(17) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(app'(le, x), y)

R is empty.
The set Q consists of the following terms:

app'(app'(minus, x0), 0)
app'(app'(minus, app'(s, x0)), app'(s, x1))
app'(app'(quot, 0), app'(s, x0))
app'(app'(quot, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(app'(low, x0), nil)
app'(app'(low, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, false), x0), app'(app'(add, x1), x2))
app'(app'(high, x0), nil)
app'(app'(high, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, false), x0), app'(app'(add, x1), x2))
app'(quicksort, nil)
app'(quicksort, app'(app'(add, x0), x1))
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.

(19) ATransformationProof (EQUIVALENT transformation)

We have applied the A-Transformation [FROCOS05] to get from an applicative problem to a standard problem.

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

le1(s(x), s(y)) → le1(x, y)

R is empty.
The set Q consists of the following terms:

minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
quicksort(nil)
quicksort(add(x0, x1))
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.

(21) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
quicksort(nil)
quicksort(add(x0, x1))
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

(22) Obligation:

Q DP problem:
The TRS P consists of the following rules:

le1(s(x), s(y)) → le1(x, y)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(23) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

le1(s(x), s(y)) → le1(x, y)
The graph contains the following edges 1 > 1, 2 > 2

(24) YES

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(high, n), app'(app'(add, m), x)) → APP'(app'(app'(if_high, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app'(if_high, true), n), app'(app'(add, m), x)) → APP'(app'(high, n), x)
APP'(app'(app'(if_high, false), n), app'(app'(add, m), x)) → APP'(app'(high, n), x)

The TRS R consists of the following rules:

app'(app'(minus, x), 0) → x
app'(app'(minus, app'(s, x)), app'(s, y)) → app'(app'(minus, x), y)
app'(app'(quot, 0), app'(s, y)) → 0
app'(app'(quot, app'(s, x)), app'(s, y)) → app'(s, app'(app'(quot, app'(app'(minus, x), y)), app'(s, y)))
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(app'(low, n), nil) → nil
app'(app'(low, n), app'(app'(add, m), x)) → app'(app'(app'(if_low, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(if_low, true), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(low, n), x))
app'(app'(app'(if_low, false), n), app'(app'(add, m), x)) → app'(app'(low, n), x)
app'(app'(high, n), nil) → nil
app'(app'(high, n), app'(app'(add, m), x)) → app'(app'(app'(if_high, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(if_high, true), n), app'(app'(add, m), x)) → app'(app'(high, n), x)
app'(app'(app'(if_high, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(high, n), x))
app'(quicksort, nil) → nil
app'(quicksort, app'(app'(add, n), x)) → app'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(minus, x0), 0)
app'(app'(minus, app'(s, x0)), app'(s, x1))
app'(app'(quot, 0), app'(s, x0))
app'(app'(quot, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(app'(low, x0), nil)
app'(app'(low, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, false), x0), app'(app'(add, x1), x2))
app'(app'(high, x0), nil)
app'(app'(high, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, false), x0), app'(app'(add, x1), x2))
app'(quicksort, nil)
app'(quicksort, app'(app'(add, x0), x1))
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.

(26) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(27) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(high, n), app'(app'(add, m), x)) → APP'(app'(app'(if_high, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app'(if_high, true), n), app'(app'(add, m), x)) → APP'(app'(high, n), x)
APP'(app'(app'(if_high, false), n), app'(app'(add, m), x)) → APP'(app'(high, n), x)

The TRS R consists of the following rules:

app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)

The set Q consists of the following terms:

app'(app'(minus, x0), 0)
app'(app'(minus, app'(s, x0)), app'(s, x1))
app'(app'(quot, 0), app'(s, x0))
app'(app'(quot, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(app'(low, x0), nil)
app'(app'(low, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, false), x0), app'(app'(add, x1), x2))
app'(app'(high, x0), nil)
app'(app'(high, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, false), x0), app'(app'(add, x1), x2))
app'(quicksort, nil)
app'(quicksort, app'(app'(add, x0), x1))
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.

(28) ATransformationProof (EQUIVALENT transformation)

We have applied the A-Transformation [FROCOS05] to get from an applicative problem to a standard problem.

(29) Obligation:

Q DP problem:
The TRS P consists of the following rules:

high1(n, add(m, x)) → if_high1(le(m, n), n, add(m, x))
if_high1(true, n, add(m, x)) → high1(n, x)
if_high1(false, n, add(m, x)) → high1(n, x)

The TRS R consists of the following rules:

le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)

The set Q consists of the following terms:

minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
quicksort(nil)
quicksort(add(x0, x1))
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.

(30) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
quicksort(nil)
quicksort(add(x0, x1))
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

(31) Obligation:

Q DP problem:
The TRS P consists of the following rules:

high1(n, add(m, x)) → if_high1(le(m, n), n, add(m, x))
if_high1(true, n, add(m, x)) → high1(n, x)
if_high1(false, n, add(m, x)) → high1(n, x)

The TRS R consists of the following rules:

le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

(32) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

high1(n, add(m, x)) → if_high1(le(m, n), n, add(m, x))
The graph contains the following edges 1 >= 2, 2 >= 3
if_high1(true, n, add(m, x)) → high1(n, x)
The graph contains the following edges 2 >= 1, 3 > 2
if_high1(false, n, add(m, x)) → high1(n, x)
The graph contains the following edges 2 >= 1, 3 > 2

(33) YES

(34) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(low, n), app'(app'(add, m), x)) → APP'(app'(app'(if_low, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app'(if_low, true), n), app'(app'(add, m), x)) → APP'(app'(low, n), x)
APP'(app'(app'(if_low, false), n), app'(app'(add, m), x)) → APP'(app'(low, n), x)

The TRS R consists of the following rules:

app'(app'(minus, x), 0) → x
app'(app'(minus, app'(s, x)), app'(s, y)) → app'(app'(minus, x), y)
app'(app'(quot, 0), app'(s, y)) → 0
app'(app'(quot, app'(s, x)), app'(s, y)) → app'(s, app'(app'(quot, app'(app'(minus, x), y)), app'(s, y)))
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(app'(low, n), nil) → nil
app'(app'(low, n), app'(app'(add, m), x)) → app'(app'(app'(if_low, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(if_low, true), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(low, n), x))
app'(app'(app'(if_low, false), n), app'(app'(add, m), x)) → app'(app'(low, n), x)
app'(app'(high, n), nil) → nil
app'(app'(high, n), app'(app'(add, m), x)) → app'(app'(app'(if_high, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(if_high, true), n), app'(app'(add, m), x)) → app'(app'(high, n), x)
app'(app'(app'(if_high, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(high, n), x))
app'(quicksort, nil) → nil
app'(quicksort, app'(app'(add, n), x)) → app'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(minus, x0), 0)
app'(app'(minus, app'(s, x0)), app'(s, x1))
app'(app'(quot, 0), app'(s, x0))
app'(app'(quot, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(app'(low, x0), nil)
app'(app'(low, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, false), x0), app'(app'(add, x1), x2))
app'(app'(high, x0), nil)
app'(app'(high, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, false), x0), app'(app'(add, x1), x2))
app'(quicksort, nil)
app'(quicksort, app'(app'(add, x0), x1))
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.

(35) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(36) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(low, n), app'(app'(add, m), x)) → APP'(app'(app'(if_low, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app'(if_low, true), n), app'(app'(add, m), x)) → APP'(app'(low, n), x)
APP'(app'(app'(if_low, false), n), app'(app'(add, m), x)) → APP'(app'(low, n), x)

The TRS R consists of the following rules:

app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)

The set Q consists of the following terms:

app'(app'(minus, x0), 0)
app'(app'(minus, app'(s, x0)), app'(s, x1))
app'(app'(quot, 0), app'(s, x0))
app'(app'(quot, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(app'(low, x0), nil)
app'(app'(low, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, false), x0), app'(app'(add, x1), x2))
app'(app'(high, x0), nil)
app'(app'(high, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, false), x0), app'(app'(add, x1), x2))
app'(quicksort, nil)
app'(quicksort, app'(app'(add, x0), x1))
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.

(37) ATransformationProof (EQUIVALENT transformation)

We have applied the A-Transformation [FROCOS05] to get from an applicative problem to a standard problem.

(38) Obligation:

Q DP problem:
The TRS P consists of the following rules:

low1(n, add(m, x)) → if_low1(le(m, n), n, add(m, x))
if_low1(true, n, add(m, x)) → low1(n, x)
if_low1(false, n, add(m, x)) → low1(n, x)

The TRS R consists of the following rules:

le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)

The set Q consists of the following terms:

minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
quicksort(nil)
quicksort(add(x0, x1))
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.

(39) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
quicksort(nil)
quicksort(add(x0, x1))
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

(40) Obligation:

Q DP problem:
The TRS P consists of the following rules:

low1(n, add(m, x)) → if_low1(le(m, n), n, add(m, x))
if_low1(true, n, add(m, x)) → low1(n, x)
if_low1(false, n, add(m, x)) → low1(n, x)

The TRS R consists of the following rules:

le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

(41) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

low1(n, add(m, x)) → if_low1(le(m, n), n, add(m, x))
The graph contains the following edges 1 >= 2, 2 >= 3
if_low1(true, n, add(m, x)) → low1(n, x)
The graph contains the following edges 2 >= 1, 3 > 2
if_low1(false, n, add(m, x)) → low1(n, x)
The graph contains the following edges 2 >= 1, 3 > 2

(42) YES

(43) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APP'(quicksort, app'(app'(add, n), x)) → APP'(quicksort, app'(app'(high, n), x))
APP'(quicksort, app'(app'(add, n), x)) → APP'(quicksort, app'(app'(low, n), x))

The TRS R consists of the following rules:

app'(app'(minus, x), 0) → x
app'(app'(minus, app'(s, x)), app'(s, y)) → app'(app'(minus, x), y)
app'(app'(quot, 0), app'(s, y)) → 0
app'(app'(quot, app'(s, x)), app'(s, y)) → app'(s, app'(app'(quot, app'(app'(minus, x), y)), app'(s, y)))
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(app'(low, n), nil) → nil
app'(app'(low, n), app'(app'(add, m), x)) → app'(app'(app'(if_low, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(if_low, true), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(low, n), x))
app'(app'(app'(if_low, false), n), app'(app'(add, m), x)) → app'(app'(low, n), x)
app'(app'(high, n), nil) → nil
app'(app'(high, n), app'(app'(add, m), x)) → app'(app'(app'(if_high, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(if_high, true), n), app'(app'(add, m), x)) → app'(app'(high, n), x)
app'(app'(app'(if_high, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(high, n), x))
app'(quicksort, nil) → nil
app'(quicksort, app'(app'(add, n), x)) → app'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(minus, x0), 0)
app'(app'(minus, app'(s, x0)), app'(s, x1))
app'(app'(quot, 0), app'(s, x0))
app'(app'(quot, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(app'(low, x0), nil)
app'(app'(low, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, false), x0), app'(app'(add, x1), x2))
app'(app'(high, x0), nil)
app'(app'(high, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, false), x0), app'(app'(add, x1), x2))
app'(quicksort, nil)
app'(quicksort, app'(app'(add, x0), x1))
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.

(44) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(45) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APP'(quicksort, app'(app'(add, n), x)) → APP'(quicksort, app'(app'(high, n), x))
APP'(quicksort, app'(app'(add, n), x)) → APP'(quicksort, app'(app'(low, n), x))

The TRS R consists of the following rules:

app'(app'(low, n), nil) → nil
app'(app'(low, n), app'(app'(add, m), x)) → app'(app'(app'(if_low, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(if_low, false), n), app'(app'(add, m), x)) → app'(app'(low, n), x)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app'(if_low, true), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(low, n), x))
app'(app'(high, n), nil) → nil
app'(app'(high, n), app'(app'(add, m), x)) → app'(app'(app'(if_high, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(if_high, true), n), app'(app'(add, m), x)) → app'(app'(high, n), x)
app'(app'(app'(if_high, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(high, n), x))

The set Q consists of the following terms:

app'(app'(minus, x0), 0)
app'(app'(minus, app'(s, x0)), app'(s, x1))
app'(app'(quot, 0), app'(s, x0))
app'(app'(quot, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(app'(low, x0), nil)
app'(app'(low, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, false), x0), app'(app'(add, x1), x2))
app'(app'(high, x0), nil)
app'(app'(high, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, false), x0), app'(app'(add, x1), x2))
app'(quicksort, nil)
app'(quicksort, app'(app'(add, x0), x1))
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.

(46) ATransformationProof (EQUIVALENT transformation)

We have applied the A-Transformation [FROCOS05] to get from an applicative problem to a standard problem.

(47) Obligation:

Q DP problem:
The TRS P consists of the following rules:

quicksort1(add(n, x)) → quicksort1(high(n, x))
quicksort1(add(n, x)) → quicksort1(low(n, x))

The TRS R consists of the following rules:

low(n, nil) → nil
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
if_low(false, n, add(m, x)) → low(n, x)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
if_low(true, n, add(m, x)) → add(m, low(n, x))
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → high(n, x)
if_high(false, n, add(m, x)) → add(m, high(n, x))

The set Q consists of the following terms:

minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
quicksort(nil)
quicksort(add(x0, x1))
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.

(48) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
quicksort(nil)
quicksort(add(x0, x1))
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

(49) Obligation:

Q DP problem:
The TRS P consists of the following rules:

quicksort1(add(n, x)) → quicksort1(high(n, x))
quicksort1(add(n, x)) → quicksort1(low(n, x))

The TRS R consists of the following rules:

low(n, nil) → nil
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
if_low(false, n, add(m, x)) → low(n, x)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
if_low(true, n, add(m, x)) → add(m, low(n, x))
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → high(n, x)
if_high(false, n, add(m, x)) → add(m, high(n, x))

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))

We have to consider all minimal (P,Q,R)-chains.

(50) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

quicksort1(add(n, x)) → quicksort1(low(n, x))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( quicksort1(x₁) ) = max{0, 2x₁ - 1}

POL( high(x₁, x₂) ) = x₂ + 2

POL( nil ) = 0

POL( add(x₁, x₂) ) = x₂ + 2

POL( if_high(x₁, ..., x₃) ) = x₃ + 2

POL( le(x₁, x₂) ) = 1

POL( true ) = 1

POL( low(x₁, x₂) ) = x₂

POL( if_low(x₁, ..., x₃) ) = max{0, 2x₁ + x₃ - 2}

POL( false ) = 0

POL( 0 ) = 2

POL( s(x₁) ) = 2x₁

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → high(n, x)
low(n, nil) → nil
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
if_low(false, n, add(m, x)) → low(n, x)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
if_low(true, n, add(m, x)) → add(m, low(n, x))
if_high(false, n, add(m, x)) → add(m, high(n, x))

(51) Obligation:

Q DP problem:
The TRS P consists of the following rules:

quicksort1(add(n, x)) → quicksort1(high(n, x))

The TRS R consists of the following rules:

low(n, nil) → nil
low(n, add(m, x)) → if_low(le(m, n), n, add(m, x))
if_low(false, n, add(m, x)) → low(n, x)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
if_low(true, n, add(m, x)) → add(m, low(n, x))
high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → high(n, x)
if_high(false, n, add(m, x)) → add(m, high(n, x))

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))

We have to consider all minimal (P,Q,R)-chains.

(52) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(53) Obligation:

Q DP problem:
The TRS P consists of the following rules:

quicksort1(add(n, x)) → quicksort1(high(n, x))

The TRS R consists of the following rules:

high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → high(n, x)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
if_high(false, n, add(m, x)) → add(m, high(n, x))

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))

We have to consider all minimal (P,Q,R)-chains.

(54) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))

(55) Obligation:

Q DP problem:
The TRS P consists of the following rules:

quicksort1(add(n, x)) → quicksort1(high(n, x))

The TRS R consists of the following rules:

high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → high(n, x)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
if_high(false, n, add(m, x)) → add(m, high(n, x))

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))

We have to consider all minimal (P,Q,R)-chains.

(56) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

quicksort1(add(n, x)) → quicksort1(high(n, x))

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
quicksort1(x1) = x1
add(x1, x2) = add(x2)
high(x1, x2) = x2
nil = nil
if_high(x1, x2, x3) = x3

Knuth-Bendix order [KBO] with precedence:

trivial

and weight map:

add_1=1
nil=1

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → high(n, x)
if_high(false, n, add(m, x)) → add(m, high(n, x))

(57) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

high(n, nil) → nil
high(n, add(m, x)) → if_high(le(m, n), n, add(m, x))
if_high(true, n, add(m, x)) → high(n, x)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
if_high(false, n, add(m, x)) → add(m, high(n, x))

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))

We have to consider all minimal (P,Q,R)-chains.

(58) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(59) YES

(60) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(minus, app'(s, x)), app'(s, y)) → APP'(app'(minus, x), y)

The TRS R consists of the following rules:

app'(app'(minus, x), 0) → x
app'(app'(minus, app'(s, x)), app'(s, y)) → app'(app'(minus, x), y)
app'(app'(quot, 0), app'(s, y)) → 0
app'(app'(quot, app'(s, x)), app'(s, y)) → app'(s, app'(app'(quot, app'(app'(minus, x), y)), app'(s, y)))
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(app'(low, n), nil) → nil
app'(app'(low, n), app'(app'(add, m), x)) → app'(app'(app'(if_low, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(if_low, true), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(low, n), x))
app'(app'(app'(if_low, false), n), app'(app'(add, m), x)) → app'(app'(low, n), x)
app'(app'(high, n), nil) → nil
app'(app'(high, n), app'(app'(add, m), x)) → app'(app'(app'(if_high, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(if_high, true), n), app'(app'(add, m), x)) → app'(app'(high, n), x)
app'(app'(app'(if_high, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(high, n), x))
app'(quicksort, nil) → nil
app'(quicksort, app'(app'(add, n), x)) → app'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(minus, x0), 0)
app'(app'(minus, app'(s, x0)), app'(s, x1))
app'(app'(quot, 0), app'(s, x0))
app'(app'(quot, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(app'(low, x0), nil)
app'(app'(low, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, false), x0), app'(app'(add, x1), x2))
app'(app'(high, x0), nil)
app'(app'(high, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, false), x0), app'(app'(add, x1), x2))
app'(quicksort, nil)
app'(quicksort, app'(app'(add, x0), x1))
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.

(61) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(62) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(minus, app'(s, x)), app'(s, y)) → APP'(app'(minus, x), y)

R is empty.
The set Q consists of the following terms:

app'(app'(minus, x0), 0)
app'(app'(minus, app'(s, x0)), app'(s, x1))
app'(app'(quot, 0), app'(s, x0))
app'(app'(quot, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(app'(low, x0), nil)
app'(app'(low, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, false), x0), app'(app'(add, x1), x2))
app'(app'(high, x0), nil)
app'(app'(high, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, false), x0), app'(app'(add, x1), x2))
app'(quicksort, nil)
app'(quicksort, app'(app'(add, x0), x1))
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.

(63) ATransformationProof (EQUIVALENT transformation)

We have applied the A-Transformation [FROCOS05] to get from an applicative problem to a standard problem.

(64) Obligation:

Q DP problem:
The TRS P consists of the following rules:

minus1(s(x), s(y)) → minus1(x, y)

R is empty.
The set Q consists of the following terms:

minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
quicksort(nil)
quicksort(add(x0, x1))
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.

(65) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
quicksort(nil)
quicksort(add(x0, x1))
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

(66) Obligation:

Q DP problem:
The TRS P consists of the following rules:

minus1(s(x), s(y)) → minus1(x, y)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(67) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

minus1(s(x), s(y)) → minus1(x, y)
The graph contains the following edges 1 > 1, 2 > 2

(68) YES

(69) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(quot, app'(s, x)), app'(s, y)) → APP'(app'(quot, app'(app'(minus, x), y)), app'(s, y))

The TRS R consists of the following rules:

app'(app'(minus, x), 0) → x
app'(app'(minus, app'(s, x)), app'(s, y)) → app'(app'(minus, x), y)
app'(app'(quot, 0), app'(s, y)) → 0
app'(app'(quot, app'(s, x)), app'(s, y)) → app'(s, app'(app'(quot, app'(app'(minus, x), y)), app'(s, y)))
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(app'(low, n), nil) → nil
app'(app'(low, n), app'(app'(add, m), x)) → app'(app'(app'(if_low, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(if_low, true), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(low, n), x))
app'(app'(app'(if_low, false), n), app'(app'(add, m), x)) → app'(app'(low, n), x)
app'(app'(high, n), nil) → nil
app'(app'(high, n), app'(app'(add, m), x)) → app'(app'(app'(if_high, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(if_high, true), n), app'(app'(add, m), x)) → app'(app'(high, n), x)
app'(app'(app'(if_high, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(high, n), x))
app'(quicksort, nil) → nil
app'(quicksort, app'(app'(add, n), x)) → app'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(minus, x0), 0)
app'(app'(minus, app'(s, x0)), app'(s, x1))
app'(app'(quot, 0), app'(s, x0))
app'(app'(quot, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(app'(low, x0), nil)
app'(app'(low, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, false), x0), app'(app'(add, x1), x2))
app'(app'(high, x0), nil)
app'(app'(high, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, false), x0), app'(app'(add, x1), x2))
app'(quicksort, nil)
app'(quicksort, app'(app'(add, x0), x1))
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.

(70) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(71) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(quot, app'(s, x)), app'(s, y)) → APP'(app'(quot, app'(app'(minus, x), y)), app'(s, y))

The TRS R consists of the following rules:

app'(app'(minus, x), 0) → x
app'(app'(minus, app'(s, x)), app'(s, y)) → app'(app'(minus, x), y)

The set Q consists of the following terms:

app'(app'(minus, x0), 0)
app'(app'(minus, app'(s, x0)), app'(s, x1))
app'(app'(quot, 0), app'(s, x0))
app'(app'(quot, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(app'(low, x0), nil)
app'(app'(low, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, false), x0), app'(app'(add, x1), x2))
app'(app'(high, x0), nil)
app'(app'(high, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, false), x0), app'(app'(add, x1), x2))
app'(quicksort, nil)
app'(quicksort, app'(app'(add, x0), x1))
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.

(72) ATransformationProof (EQUIVALENT transformation)

We have applied the A-Transformation [FROCOS05] to get from an applicative problem to a standard problem.

(73) Obligation:

Q DP problem:
The TRS P consists of the following rules:

quot1(s(x), s(y)) → quot1(minus(x, y), s(y))

The TRS R consists of the following rules:

minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)

The set Q consists of the following terms:

minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
quicksort(nil)
quicksort(add(x0, x1))
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.

(74) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
low(x0, nil)
low(x0, add(x1, x2))
if_low(true, x0, add(x1, x2))
if_low(false, x0, add(x1, x2))
high(x0, nil)
high(x0, add(x1, x2))
if_high(true, x0, add(x1, x2))
if_high(false, x0, add(x1, x2))
quicksort(nil)
quicksort(add(x0, x1))
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

(75) Obligation:

Q DP problem:
The TRS P consists of the following rules:

quot1(s(x), s(y)) → quot1(minus(x, y), s(y))

The TRS R consists of the following rules:

minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)

The set Q consists of the following terms:

minus(x0, 0)
minus(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

(76) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

quot1(s(x), s(y)) → quot1(minus(x, y), s(y))

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
quot1(x1, x2) = x1
s(x1) = s(x1)
minus(x1, x2) = x1

Knuth-Bendix order [KBO] with precedence:

trivial

and weight map:

s_1=1
dummyConstant=1

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)

(77) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)

The set Q consists of the following terms:

minus(x0, 0)
minus(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

(78) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(79) YES

(80) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(map, f), xs)
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(filter, f), xs)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(app'(filter, f), xs)

The TRS R consists of the following rules:

app'(app'(minus, x), 0) → x
app'(app'(minus, app'(s, x)), app'(s, y)) → app'(app'(minus, x), y)
app'(app'(quot, 0), app'(s, y)) → 0
app'(app'(quot, app'(s, x)), app'(s, y)) → app'(s, app'(app'(quot, app'(app'(minus, x), y)), app'(s, y)))
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(app'(low, n), nil) → nil
app'(app'(low, n), app'(app'(add, m), x)) → app'(app'(app'(if_low, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(if_low, true), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(low, n), x))
app'(app'(app'(if_low, false), n), app'(app'(add, m), x)) → app'(app'(low, n), x)
app'(app'(high, n), nil) → nil
app'(app'(high, n), app'(app'(add, m), x)) → app'(app'(app'(if_high, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(if_high, true), n), app'(app'(add, m), x)) → app'(app'(high, n), x)
app'(app'(app'(if_high, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(high, n), x))
app'(quicksort, nil) → nil
app'(quicksort, app'(app'(add, n), x)) → app'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(minus, x0), 0)
app'(app'(minus, app'(s, x0)), app'(s, x1))
app'(app'(quot, 0), app'(s, x0))
app'(app'(quot, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(app'(low, x0), nil)
app'(app'(low, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_low, false), x0), app'(app'(add, x1), x2))
app'(app'(high, x0), nil)
app'(app'(high, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_high, false), x0), app'(app'(add, x1), x2))
app'(quicksort, nil)
app'(quicksort, app'(app'(add, x0), x1))
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.

(81) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(f, x)
The graph contains the following edges 1 > 1, 2 > 2
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(f, x)
The graph contains the following edges 1 > 1, 2 > 2
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(map, f), xs)
The graph contains the following edges 1 >= 1, 2 > 2
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
The graph contains the following edges 2 > 2
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(filter, f), xs)
The graph contains the following edges 2 >= 2
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(app'(filter, f), xs)
The graph contains the following edges 2 >= 2