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

0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 AND
  ↳5 QDP
    ↳6 QDPOrderProof (⇔)
    ↳7 QDP
    ↳8 PisEmptyProof (⇔)
    ↳9 TRUE
  ↳10 QDP
    ↳11 QDPOrderProof (⇔)
    ↳12 QDP
    ↳13 PisEmptyProof (⇔)
    ↳14 TRUE
  ↳15 QDP
    ↳16 QDPOrderProof (⇔)
    ↳17 QDP
    ↳18 PisEmptyProof (⇔)
    ↳19 TRUE
  ↳20 QDP
  ↳21 QDP
    ↳22 QDPOrderProof (⇔)
    ↳23 QDP
    ↳24 QDPOrderProof (⇔)
    ↳25 QDP
    ↳26 PisEmptyProof (⇔)
    ↳27 TRUE
  ↳28 QDP
    ↳29 QDPOrderProof (⇔)
    ↳30 QDP
    ↳31 PisEmptyProof (⇔)
    ↳32 TRUE
  ↳33 QDP
    ↳34 QDPOrderProof (⇔)
    ↳35 QDP
    ↳36 DependencyGraphProof (⇔)
    ↳37 TRUE

(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) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04]. Here, we combined the reduction pair processor with the A-transformation [FROCOS05] which results in the following intermediate Q-DP Problem.
The a-transformed P is

app1(cons(x, l), k) → app1(l, k)

The a-transformed usable rules are
none


The following pairs can be oriented strictly and are deleted.


APP'(app'(app, app'(app'(cons, x), l)), k) → APP'(app'(app, l), k)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
app1(x1, x2)  =  app1(x1)
cons(x1, x2)  =  cons(x1, x2)

Lexicographic Path Order [LPO].
Precedence:
cons2 > app11

The following usable rules [FROCOS05] were oriented: none

(7) Obligation:

Q DP problem:
P is empty.
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) PisEmptyProof (EQUIVALENT transformation)

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

(9) TRUE

(10) 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.

(11) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04]. Here, we combined the reduction pair processor with the A-transformation [FROCOS05] which results in the following intermediate Q-DP Problem.
The a-transformed P is

plus1(s(x), y) → plus1(x, y)

The a-transformed usable rules are
none


The following pairs can be oriented strictly and are deleted.


APP'(app'(plus, app'(s, x)), y) → APP'(app'(plus, x), y)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
plus1(x1, x2)  =  plus1(x1)
s(x1)  =  s(x1)

Lexicographic Path Order [LPO].
Precedence:
s1 > plus11

The following usable rules [FROCOS05] were oriented: none

(12) Obligation:

Q DP problem:
P is empty.
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.

(13) PisEmptyProof (EQUIVALENT transformation)

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

(14) TRUE

(15) 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.

(16) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04]. Here, we combined the reduction pair processor with the A-transformation [FROCOS05] which results in the following intermediate Q-DP Problem.
The a-transformed P is

sum1(cons(x, cons(y, l))) → sum1(cons(plus(x, y), l))

The a-transformed usable rules are

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


The following pairs can be oriented strictly and are deleted.


APP'(sum, app'(app'(cons, x), app'(app'(cons, y), l))) → APP'(sum, app'(app'(cons, app'(app'(plus, x), y)), l))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
sum1(x1)  =  sum1(x1)
cons(x1, x2)  =  cons(x2)
plus(x1, x2)  =  plus(x1, x2)
0  =  0
s(x1)  =  s

Lexicographic Path Order [LPO].
Precedence:
sum11 > cons1
plus2 > s

The following usable rules [FROCOS05] were oriented:

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

(17) Obligation:

Q DP problem:
P is empty.
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.

(18) PisEmptyProof (EQUIVALENT transformation)

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

(19) TRUE

(20) 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.

(21) 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.

(22) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04]. Here, we combined the reduction pair processor with the A-transformation [FROCOS05] which results in the following intermediate Q-DP Problem.
The a-transformed P is

minus1(minus(x, y), z) → minus1(x, plus(y, z))
minus1(s(x), s(y)) → minus1(x, y)

The a-transformed usable rules are

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


The following pairs can be oriented strictly and are deleted.


APP'(app'(minus, app'(app'(minus, x), y)), z) → APP'(app'(minus, x), app'(app'(plus, y), z))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
minus1(x1, x2)  =  minus1(x1, x2)
minus(x1, x2)  =  minus(x1)
plus(x1, x2)  =  x2
s(x1)  =  x1
0  =  0

Lexicographic Path Order [LPO].
Precedence:
trivial

The following usable rules [FROCOS05] were oriented:

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

(23) 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'(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.

(24) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04]. Here, we combined the reduction pair processor with the A-transformation [FROCOS05] which results in the following intermediate Q-DP Problem.
The a-transformed P is

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

The a-transformed usable rules are
none


The following pairs can be oriented strictly and are deleted.


APP'(app'(minus, app'(s, x)), app'(s, y)) → APP'(app'(minus, x), y)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
minus1(x1, x2)  =  minus1(x2)
s(x1)  =  s(x1)

Lexicographic Path Order [LPO].
Precedence:
s1 > minus11

The following usable rules [FROCOS05] were oriented: none

(25) Obligation:

Q DP problem:
P is empty.
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.

(26) PisEmptyProof (EQUIVALENT transformation)

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

(27) TRUE

(28) 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.

(29) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04]. Here, we combined the reduction pair processor with the A-transformation [FROCOS05] which results in the following intermediate Q-DP Problem.
The a-transformed P is

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

The a-transformed usable rules are

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


The following pairs can be oriented strictly and are deleted.


APP'(app'(quot, app'(s, x)), app'(s, y)) → APP'(app'(quot, app'(app'(minus, x), y)), app'(s, y))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
quot1(x1, x2)  =  quot1(x1)
s(x1)  =  s(x1)
minus(x1, x2)  =  x1
0  =  0
plus(x1, x2)  =  plus(x1, x2)

Lexicographic Path Order [LPO].
Precedence:
quot11 > s1
plus2 > s1

The following usable rules [FROCOS05] were oriented:

app'(app'(minus, x), 0) → x
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)
app'(app'(plus, 0), y) → y
app'(app'(plus, app'(s, x)), y) → app'(s, app'(app'(plus, x), y))

(30) Obligation:

Q DP problem:
P is empty.
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.

(31) PisEmptyProof (EQUIVALENT transformation)

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

(32) TRUE

(33) 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.

(34) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


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'(filter, f), app'(app'(cons, x), xs)) → APP'(f, x)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
APP'(x1, x2)  =  x2
app'(x1, x2)  =  app'(x1, x2)
map  =  map
cons  =  cons
filter  =  filter
filter2  =  filter2
true  =  true
false  =  false
minus  =  minus
0  =  0
plus  =  plus
s  =  s
quot  =  quot
app  =  app
nil  =  nil
sum  =  sum

Lexicographic Path Order [LPO].
Precedence:
map > nil > cons > app'2
filter > nil > cons > app'2
filter2 > cons > app'2
false > app'2
plus > app'2
quot > s > minus > app'2
quot > s > 0
app > sum > cons > app'2

The following usable rules [FROCOS05] were oriented: none

(35) Obligation:

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

APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(filter, f), xs)
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.

(36) DependencyGraphProof (EQUIVALENT transformation)

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

(37) TRUE