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

(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'(minus, app'(app'(minus, x), y)), z) → app'(app'(minus, x), app'(app'(plus, y), z))
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'(plus, 0), y) → y
app'(app'(plus, app'(s, x)), y) → app'(s, app'(app'(plus, x), y))
app'(app'(app, nil), k) → k
app'(app'(app, l), nil) → l
app'(app'(app, app'(app'(cons, x), l)), k) → app'(app'(cons, x), app'(app'(app, l), k))
app'(sum, app'(app'(cons, x), nil)) → app'(app'(cons, x), nil)
app'(sum, app'(app'(cons, x), app'(app'(cons, y), l))) → app'(sum, app'(app'(cons, app'(app'(plus, x), y)), l))
app'(sum, app'(app'(app, l), app'(app'(cons, x), app'(app'(cons, y), k)))) → app'(sum, app'(app'(app, l), app'(sum, app'(app'(cons, x), app'(app'(cons, y), k)))))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(cons, x), xs)) → app'(app'(cons, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(cons, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(cons, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

Q is empty.

(1) DependencyPairsProof (EQUIVALENT transformation)

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

(2) 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'(minus, app'(app'(minus, x), y)), z) → APP'(app'(minus, x), app'(app'(plus, y), z))
APP'(app'(minus, app'(app'(minus, x), y)), z) → APP'(app'(plus, y), z)
APP'(app'(minus, app'(app'(minus, x), y)), z) → APP'(plus, y)
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'(plus, app'(s, x)), y) → APP'(s, app'(app'(plus, x), y))
APP'(app'(plus, app'(s, x)), y) → APP'(app'(plus, x), y)
APP'(app'(plus, app'(s, x)), y) → APP'(plus, x)
APP'(app'(app, app'(app'(cons, x), l)), k) → APP'(app'(cons, x), app'(app'(app, l), k))
APP'(app'(app, app'(app'(cons, x), l)), k) → APP'(app'(app, l), k)
APP'(app'(app, app'(app'(cons, x), l)), k) → APP'(app, l)
APP'(sum, app'(app'(cons, x), app'(app'(cons, y), l))) → APP'(sum, app'(app'(cons, app'(app'(plus, x), y)), l))
APP'(sum, app'(app'(cons, x), app'(app'(cons, y), l))) → APP'(app'(cons, app'(app'(plus, x), y)), l)
APP'(sum, app'(app'(cons, x), app'(app'(cons, y), l))) → APP'(cons, app'(app'(plus, x), y))
APP'(sum, app'(app'(cons, x), app'(app'(cons, y), l))) → APP'(app'(plus, x), y)
APP'(sum, app'(app'(cons, x), app'(app'(cons, y), l))) → APP'(plus, x)
APP'(sum, app'(app'(app, l), app'(app'(cons, x), app'(app'(cons, y), k)))) → APP'(sum, app'(app'(app, l), app'(sum, app'(app'(cons, x), app'(app'(cons, y), k)))))
APP'(sum, app'(app'(app, l), app'(app'(cons, x), app'(app'(cons, y), k)))) → APP'(app'(app, l), app'(sum, app'(app'(cons, x), app'(app'(cons, y), k))))
APP'(sum, app'(app'(app, l), app'(app'(cons, x), app'(app'(cons, y), k)))) → APP'(sum, app'(app'(cons, x), app'(app'(cons, y), k)))
APP'(app'(map, f), app'(app'(cons, x), xs)) → APP'(app'(cons, app'(f, x)), app'(app'(map, f), xs))
APP'(app'(map, f), app'(app'(cons, x), xs)) → APP'(cons, app'(f, x))
APP'(app'(map, f), app'(app'(cons, x), xs)) → APP'(f, x)
APP'(app'(map, f), app'(app'(cons, x), xs)) → APP'(app'(map, f), xs)
APP'(app'(filter, f), app'(app'(cons, x), xs)) → APP'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
APP'(app'(filter, f), app'(app'(cons, x), xs)) → APP'(app'(app'(filter2, app'(f, x)), f), x)
APP'(app'(filter, f), app'(app'(cons, x), xs)) → APP'(app'(filter2, app'(f, x)), f)
APP'(app'(filter, f), app'(app'(cons, x), xs)) → APP'(filter2, app'(f, x))
APP'(app'(filter, f), app'(app'(cons, x), xs)) → APP'(f, x)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(cons, x), app'(app'(filter, f), xs))
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(cons, 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'(minus, app'(app'(minus, x), y)), z) → app'(app'(minus, x), app'(app'(plus, y), z))
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'(plus, 0), y) → y
app'(app'(plus, app'(s, x)), y) → app'(s, app'(app'(plus, x), y))
app'(app'(app, nil), k) → k
app'(app'(app, l), nil) → l
app'(app'(app, app'(app'(cons, x), l)), k) → app'(app'(cons, x), app'(app'(app, l), k))
app'(sum, app'(app'(cons, x), nil)) → app'(app'(cons, x), nil)
app'(sum, app'(app'(cons, x), app'(app'(cons, y), l))) → app'(sum, app'(app'(cons, app'(app'(plus, x), y)), l))
app'(sum, app'(app'(app, l), app'(app'(cons, x), app'(app'(cons, y), k)))) → app'(sum, app'(app'(app, l), app'(sum, app'(app'(cons, x), app'(app'(cons, y), k)))))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(cons, x), xs)) → app'(app'(cons, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(cons, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(cons, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

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

(3) DependencyGraphProof (EQUIVALENT transformation)

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

(4) Complex Obligation (AND)

(5) Obligation:

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

APP'(app'(app, app'(app'(cons, x), l)), k) → APP'(app'(app, l), k)

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'(minus, app'(app'(minus, x), y)), z) → app'(app'(minus, x), app'(app'(plus, y), z))
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'(plus, 0), y) → y
app'(app'(plus, app'(s, x)), y) → app'(s, app'(app'(plus, x), y))
app'(app'(app, nil), k) → k
app'(app'(app, l), nil) → l
app'(app'(app, app'(app'(cons, x), l)), k) → app'(app'(cons, x), app'(app'(app, l), k))
app'(sum, app'(app'(cons, x), nil)) → app'(app'(cons, x), nil)
app'(sum, app'(app'(cons, x), app'(app'(cons, y), l))) → app'(sum, app'(app'(cons, app'(app'(plus, x), y)), l))
app'(sum, app'(app'(app, l), app'(app'(cons, x), app'(app'(cons, y), k)))) → app'(sum, app'(app'(app, l), app'(sum, app'(app'(cons, x), app'(app'(cons, y), k)))))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(cons, x), xs)) → app'(app'(cons, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(cons, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(cons, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

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

(6) Obligation:

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

APP'(app'(plus, app'(s, x)), y) → APP'(app'(plus, 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'(minus, app'(app'(minus, x), y)), z) → app'(app'(minus, x), app'(app'(plus, y), z))
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'(plus, 0), y) → y
app'(app'(plus, app'(s, x)), y) → app'(s, app'(app'(plus, x), y))
app'(app'(app, nil), k) → k
app'(app'(app, l), nil) → l
app'(app'(app, app'(app'(cons, x), l)), k) → app'(app'(cons, x), app'(app'(app, l), k))
app'(sum, app'(app'(cons, x), nil)) → app'(app'(cons, x), nil)
app'(sum, app'(app'(cons, x), app'(app'(cons, y), l))) → app'(sum, app'(app'(cons, app'(app'(plus, x), y)), l))
app'(sum, app'(app'(app, l), app'(app'(cons, x), app'(app'(cons, y), k)))) → app'(sum, app'(app'(app, l), app'(sum, app'(app'(cons, x), app'(app'(cons, y), k)))))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(cons, x), xs)) → app'(app'(cons, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(cons, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(cons, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

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

(7) Obligation:

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

APP'(sum, app'(app'(cons, x), app'(app'(cons, y), l))) → APP'(sum, app'(app'(cons, app'(app'(plus, x), y)), l))

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'(minus, app'(app'(minus, x), y)), z) → app'(app'(minus, x), app'(app'(plus, y), z))
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'(plus, 0), y) → y
app'(app'(plus, app'(s, x)), y) → app'(s, app'(app'(plus, x), y))
app'(app'(app, nil), k) → k
app'(app'(app, l), nil) → l
app'(app'(app, app'(app'(cons, x), l)), k) → app'(app'(cons, x), app'(app'(app, l), k))
app'(sum, app'(app'(cons, x), nil)) → app'(app'(cons, x), nil)
app'(sum, app'(app'(cons, x), app'(app'(cons, y), l))) → app'(sum, app'(app'(cons, app'(app'(plus, x), y)), l))
app'(sum, app'(app'(app, l), app'(app'(cons, x), app'(app'(cons, y), k)))) → app'(sum, app'(app'(app, l), app'(sum, app'(app'(cons, x), app'(app'(cons, y), k)))))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(cons, x), xs)) → app'(app'(cons, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(cons, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(cons, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

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

(8) Obligation:

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

APP'(sum, app'(app'(app, l), app'(app'(cons, x), app'(app'(cons, y), k)))) → APP'(sum, app'(app'(app, l), app'(sum, app'(app'(cons, x), app'(app'(cons, y), k)))))

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'(minus, app'(app'(minus, x), y)), z) → app'(app'(minus, x), app'(app'(plus, y), z))
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'(plus, 0), y) → y
app'(app'(plus, app'(s, x)), y) → app'(s, app'(app'(plus, x), y))
app'(app'(app, nil), k) → k
app'(app'(app, l), nil) → l
app'(app'(app, app'(app'(cons, x), l)), k) → app'(app'(cons, x), app'(app'(app, l), k))
app'(sum, app'(app'(cons, x), nil)) → app'(app'(cons, x), nil)
app'(sum, app'(app'(cons, x), app'(app'(cons, y), l))) → app'(sum, app'(app'(cons, app'(app'(plus, x), y)), l))
app'(sum, app'(app'(app, l), app'(app'(cons, x), app'(app'(cons, y), k)))) → app'(sum, app'(app'(app, l), app'(sum, app'(app'(cons, x), app'(app'(cons, y), k)))))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(cons, x), xs)) → app'(app'(cons, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(cons, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(cons, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

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

(9) Obligation:

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

APP'(app'(minus, app'(app'(minus, x), y)), z) → APP'(app'(minus, x), app'(app'(plus, y), z))
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'(minus, app'(app'(minus, x), y)), z) → app'(app'(minus, x), app'(app'(plus, y), z))
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'(plus, 0), y) → y
app'(app'(plus, app'(s, x)), y) → app'(s, app'(app'(plus, x), y))
app'(app'(app, nil), k) → k
app'(app'(app, l), nil) → l
app'(app'(app, app'(app'(cons, x), l)), k) → app'(app'(cons, x), app'(app'(app, l), k))
app'(sum, app'(app'(cons, x), nil)) → app'(app'(cons, x), nil)
app'(sum, app'(app'(cons, x), app'(app'(cons, y), l))) → app'(sum, app'(app'(cons, app'(app'(plus, x), y)), l))
app'(sum, app'(app'(app, l), app'(app'(cons, x), app'(app'(cons, y), k)))) → app'(sum, app'(app'(app, l), app'(sum, app'(app'(cons, x), app'(app'(cons, y), k)))))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(cons, x), xs)) → app'(app'(cons, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(cons, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(cons, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

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

(10) 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'(minus, app'(app'(minus, x), y)), z) → app'(app'(minus, x), app'(app'(plus, y), z))
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'(plus, 0), y) → y
app'(app'(plus, app'(s, x)), y) → app'(s, app'(app'(plus, x), y))
app'(app'(app, nil), k) → k
app'(app'(app, l), nil) → l
app'(app'(app, app'(app'(cons, x), l)), k) → app'(app'(cons, x), app'(app'(app, l), k))
app'(sum, app'(app'(cons, x), nil)) → app'(app'(cons, x), nil)
app'(sum, app'(app'(cons, x), app'(app'(cons, y), l))) → app'(sum, app'(app'(cons, app'(app'(plus, x), y)), l))
app'(sum, app'(app'(app, l), app'(app'(cons, x), app'(app'(cons, y), k)))) → app'(sum, app'(app'(app, l), app'(sum, app'(app'(cons, x), app'(app'(cons, y), k)))))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(cons, x), xs)) → app'(app'(cons, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(cons, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(cons, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

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

(11) Obligation:

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

APP'(app'(map, f), app'(app'(cons, x), xs)) → APP'(app'(map, f), xs)
APP'(app'(map, f), app'(app'(cons, x), xs)) → APP'(f, x)
APP'(app'(filter, f), app'(app'(cons, 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'(cons, 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'(minus, app'(app'(minus, x), y)), z) → app'(app'(minus, x), app'(app'(plus, y), z))
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'(plus, 0), y) → y
app'(app'(plus, app'(s, x)), y) → app'(s, app'(app'(plus, x), y))
app'(app'(app, nil), k) → k
app'(app'(app, l), nil) → l
app'(app'(app, app'(app'(cons, x), l)), k) → app'(app'(cons, x), app'(app'(app, l), k))
app'(sum, app'(app'(cons, x), nil)) → app'(app'(cons, x), nil)
app'(sum, app'(app'(cons, x), app'(app'(cons, y), l))) → app'(sum, app'(app'(cons, app'(app'(plus, x), y)), l))
app'(sum, app'(app'(app, l), app'(app'(cons, x), app'(app'(cons, y), k)))) → app'(sum, app'(app'(app, l), app'(sum, app'(app'(cons, x), app'(app'(cons, y), k)))))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(cons, x), xs)) → app'(app'(cons, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(cons, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(cons, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

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