(0) Obligation:

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

app(app(app(if, true), xs), ys) → xs
app(app(app(if, false), xs), ys) → ys
app(app(lt, app(s, x)), app(s, y)) → app(app(lt, x), y)
app(app(lt, 0), app(s, y)) → true
app(app(lt, y), 0) → false
app(app(eq, x), x) → true
app(app(eq, app(s, x)), 0) → false
app(app(eq, 0), app(s, x)) → false
app(app(merge, xs), nil) → xs
app(app(merge, nil), ys) → ys
app(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → app(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys))))
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(mult, 0), x) → 0
app(app(mult, app(s, x)), y) → app(app(plus, y), app(app(mult, x), y))
app(app(plus, 0), x) → 0
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
list1app(app(map, app(mult, app(s, app(s, 0)))), hamming)
list2app(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming)
list3app(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming)
hammingapp(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3)))

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(app(if, true), xs), ys) → xs
app(app(app(if, false), xs), ys) → ys
app(app(lt, app(s, x)), app(s, y)) → app(app(lt, x), y)
app(app(lt, 0), app(s, y)) → true
app(app(lt, y), 0) → false
app(app(eq, x), x) → true
app(app(eq, app(s, x)), 0) → false
app(app(eq, 0), app(s, x)) → false
app(app(merge, xs), nil) → xs
app(app(merge, nil), ys) → ys
app(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → app(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys))))
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(mult, 0), x) → 0
app(app(mult, app(s, x)), y) → app(app(plus, y), app(app(mult, x), y))
app(app(plus, 0), x) → 0
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
list1app(app(map, app(mult, app(s, app(s, 0)))), hamming)
list2app(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming)
list3app(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming)
hammingapp(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3)))

The set Q consists of the following terms:

app(app(app(if, true), x0), x1)
app(app(app(if, false), x0), x1)
app(app(lt, app(s, x0)), app(s, x1))
app(app(lt, 0), app(s, x0))
app(app(lt, x0), 0)
app(app(eq, x0), x0)
app(app(eq, app(s, x0)), 0)
app(app(eq, 0), app(s, x0))
app(app(merge, x0), nil)
app(app(merge, nil), x0)
app(app(merge, app(app(cons, x0), x1)), app(app(cons, x2), x3))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(mult, 0), x0)
app(app(mult, app(s, x0)), x1)
app(app(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
list1
list2
list3
hamming

(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(lt, app(s, x)), app(s, y)) → APP(app(lt, x), y)
APP(app(lt, app(s, x)), app(s, y)) → APP(lt, x)
APP(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → APP(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys))))
APP(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → APP(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys))))
APP(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → APP(if, app(app(lt, x), y))
APP(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → APP(app(lt, x), y)
APP(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → APP(lt, x)
APP(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → APP(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))
APP(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → APP(app(merge, xs), app(app(cons, y), ys))
APP(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → APP(merge, xs)
APP(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → APP(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys)))
APP(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → APP(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys)))
APP(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → APP(if, app(app(eq, x), y))
APP(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → APP(app(eq, x), y)
APP(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → APP(eq, x)
APP(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → APP(app(cons, x), app(app(merge, xs), ys))
APP(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → APP(app(merge, xs), ys)
APP(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → APP(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys))
APP(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → APP(app(merge, app(app(cons, x), xs)), ys)
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(mult, app(s, x)), y) → APP(app(plus, y), app(app(mult, x), y))
APP(app(mult, app(s, x)), y) → APP(plus, y)
APP(app(mult, app(s, x)), y) → APP(app(mult, x), y)
APP(app(mult, app(s, x)), y) → APP(mult, 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)
LIST1APP(app(map, app(mult, app(s, app(s, 0)))), hamming)
LIST1APP(map, app(mult, app(s, app(s, 0))))
LIST1APP(mult, app(s, app(s, 0)))
LIST1APP(s, app(s, 0))
LIST1APP(s, 0)
LIST1HAMMING
LIST2APP(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming)
LIST2APP(map, app(mult, app(s, app(s, app(s, 0)))))
LIST2APP(mult, app(s, app(s, app(s, 0))))
LIST2APP(s, app(s, app(s, 0)))
LIST2APP(s, app(s, 0))
LIST2APP(s, 0)
LIST2HAMMING
LIST3APP(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming)
LIST3APP(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0)))))))
LIST3APP(mult, app(s, app(s, app(s, app(s, app(s, 0))))))
LIST3APP(s, app(s, app(s, app(s, app(s, 0)))))
LIST3APP(s, app(s, app(s, app(s, 0))))
LIST3APP(s, app(s, app(s, 0)))
LIST3APP(s, app(s, 0))
LIST3APP(s, 0)
LIST3HAMMING
HAMMINGAPP(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3)))
HAMMINGAPP(cons, app(s, 0))
HAMMINGAPP(s, 0)
HAMMINGAPP(app(merge, list1), app(app(merge, list2), list3))
HAMMINGAPP(merge, list1)
HAMMINGLIST1
HAMMINGAPP(app(merge, list2), list3)
HAMMINGAPP(merge, list2)
HAMMINGLIST2
HAMMINGLIST3

The TRS R consists of the following rules:

app(app(app(if, true), xs), ys) → xs
app(app(app(if, false), xs), ys) → ys
app(app(lt, app(s, x)), app(s, y)) → app(app(lt, x), y)
app(app(lt, 0), app(s, y)) → true
app(app(lt, y), 0) → false
app(app(eq, x), x) → true
app(app(eq, app(s, x)), 0) → false
app(app(eq, 0), app(s, x)) → false
app(app(merge, xs), nil) → xs
app(app(merge, nil), ys) → ys
app(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → app(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys))))
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(mult, 0), x) → 0
app(app(mult, app(s, x)), y) → app(app(plus, y), app(app(mult, x), y))
app(app(plus, 0), x) → 0
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
list1app(app(map, app(mult, app(s, app(s, 0)))), hamming)
list2app(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming)
list3app(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming)
hammingapp(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3)))

The set Q consists of the following terms:

app(app(app(if, true), x0), x1)
app(app(app(if, false), x0), x1)
app(app(lt, app(s, x0)), app(s, x1))
app(app(lt, 0), app(s, x0))
app(app(lt, x0), 0)
app(app(eq, x0), x0)
app(app(eq, app(s, x0)), 0)
app(app(eq, 0), app(s, x0))
app(app(merge, x0), nil)
app(app(merge, nil), x0)
app(app(merge, app(app(cons, x0), x1)), app(app(cons, x2), x3))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(mult, 0), x0)
app(app(mult, app(s, x0)), x1)
app(app(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
list1
list2
list3
hamming

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) 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(app(if, true), xs), ys) → xs
app(app(app(if, false), xs), ys) → ys
app(app(lt, app(s, x)), app(s, y)) → app(app(lt, x), y)
app(app(lt, 0), app(s, y)) → true
app(app(lt, y), 0) → false
app(app(eq, x), x) → true
app(app(eq, app(s, x)), 0) → false
app(app(eq, 0), app(s, x)) → false
app(app(merge, xs), nil) → xs
app(app(merge, nil), ys) → ys
app(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → app(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys))))
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(mult, 0), x) → 0
app(app(mult, app(s, x)), y) → app(app(plus, y), app(app(mult, x), y))
app(app(plus, 0), x) → 0
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
list1app(app(map, app(mult, app(s, app(s, 0)))), hamming)
list2app(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming)
list3app(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming)
hammingapp(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3)))

The set Q consists of the following terms:

app(app(app(if, true), x0), x1)
app(app(app(if, false), x0), x1)
app(app(lt, app(s, x0)), app(s, x1))
app(app(lt, 0), app(s, x0))
app(app(lt, x0), 0)
app(app(eq, x0), x0)
app(app(eq, app(s, x0)), 0)
app(app(eq, 0), app(s, x0))
app(app(merge, x0), nil)
app(app(merge, nil), x0)
app(app(merge, app(app(cons, x0), x1)), app(app(cons, x2), x3))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(mult, 0), x0)
app(app(mult, app(s, x0)), x1)
app(app(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
list1
list2
list3
hamming

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

(8) 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)

Recursive path order with status [RPO].
Precedence:
s1 > plus11

Status:
plus11: multiset
s1: multiset

The following usable rules [FROCOS05] were oriented: none

(9) Obligation:

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

app(app(app(if, true), xs), ys) → xs
app(app(app(if, false), xs), ys) → ys
app(app(lt, app(s, x)), app(s, y)) → app(app(lt, x), y)
app(app(lt, 0), app(s, y)) → true
app(app(lt, y), 0) → false
app(app(eq, x), x) → true
app(app(eq, app(s, x)), 0) → false
app(app(eq, 0), app(s, x)) → false
app(app(merge, xs), nil) → xs
app(app(merge, nil), ys) → ys
app(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → app(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys))))
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(mult, 0), x) → 0
app(app(mult, app(s, x)), y) → app(app(plus, y), app(app(mult, x), y))
app(app(plus, 0), x) → 0
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
list1app(app(map, app(mult, app(s, app(s, 0)))), hamming)
list2app(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming)
list3app(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming)
hammingapp(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3)))

The set Q consists of the following terms:

app(app(app(if, true), x0), x1)
app(app(app(if, false), x0), x1)
app(app(lt, app(s, x0)), app(s, x1))
app(app(lt, 0), app(s, x0))
app(app(lt, x0), 0)
app(app(eq, x0), x0)
app(app(eq, app(s, x0)), 0)
app(app(eq, 0), app(s, x0))
app(app(merge, x0), nil)
app(app(merge, nil), x0)
app(app(merge, app(app(cons, x0), x1)), app(app(cons, x2), x3))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(mult, 0), x0)
app(app(mult, app(s, x0)), x1)
app(app(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
list1
list2
list3
hamming

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

(10) PisEmptyProof (EQUIVALENT transformation)

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

(11) TRUE

(12) Obligation:

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

APP(app(mult, app(s, x)), y) → APP(app(mult, x), y)

The TRS R consists of the following rules:

app(app(app(if, true), xs), ys) → xs
app(app(app(if, false), xs), ys) → ys
app(app(lt, app(s, x)), app(s, y)) → app(app(lt, x), y)
app(app(lt, 0), app(s, y)) → true
app(app(lt, y), 0) → false
app(app(eq, x), x) → true
app(app(eq, app(s, x)), 0) → false
app(app(eq, 0), app(s, x)) → false
app(app(merge, xs), nil) → xs
app(app(merge, nil), ys) → ys
app(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → app(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys))))
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(mult, 0), x) → 0
app(app(mult, app(s, x)), y) → app(app(plus, y), app(app(mult, x), y))
app(app(plus, 0), x) → 0
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
list1app(app(map, app(mult, app(s, app(s, 0)))), hamming)
list2app(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming)
list3app(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming)
hammingapp(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3)))

The set Q consists of the following terms:

app(app(app(if, true), x0), x1)
app(app(app(if, false), x0), x1)
app(app(lt, app(s, x0)), app(s, x1))
app(app(lt, 0), app(s, x0))
app(app(lt, x0), 0)
app(app(eq, x0), x0)
app(app(eq, app(s, x0)), 0)
app(app(eq, 0), app(s, x0))
app(app(merge, x0), nil)
app(app(merge, nil), x0)
app(app(merge, app(app(cons, x0), x1)), app(app(cons, x2), x3))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(mult, 0), x0)
app(app(mult, app(s, x0)), x1)
app(app(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
list1
list2
list3
hamming

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

(13) 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

mult1(s(x), y) → mult1(x, y)

The a-transformed usable rules are
none


The following pairs can be oriented strictly and are deleted.


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

Recursive path order with status [RPO].
Precedence:
s1 > mult11

Status:
s1: multiset
mult11: multiset

The following usable rules [FROCOS05] were oriented: none

(14) Obligation:

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

app(app(app(if, true), xs), ys) → xs
app(app(app(if, false), xs), ys) → ys
app(app(lt, app(s, x)), app(s, y)) → app(app(lt, x), y)
app(app(lt, 0), app(s, y)) → true
app(app(lt, y), 0) → false
app(app(eq, x), x) → true
app(app(eq, app(s, x)), 0) → false
app(app(eq, 0), app(s, x)) → false
app(app(merge, xs), nil) → xs
app(app(merge, nil), ys) → ys
app(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → app(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys))))
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(mult, 0), x) → 0
app(app(mult, app(s, x)), y) → app(app(plus, y), app(app(mult, x), y))
app(app(plus, 0), x) → 0
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
list1app(app(map, app(mult, app(s, app(s, 0)))), hamming)
list2app(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming)
list3app(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming)
hammingapp(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3)))

The set Q consists of the following terms:

app(app(app(if, true), x0), x1)
app(app(app(if, false), x0), x1)
app(app(lt, app(s, x0)), app(s, x1))
app(app(lt, 0), app(s, x0))
app(app(lt, x0), 0)
app(app(eq, x0), x0)
app(app(eq, app(s, x0)), 0)
app(app(eq, 0), app(s, x0))
app(app(merge, x0), nil)
app(app(merge, nil), x0)
app(app(merge, app(app(cons, x0), x1)), app(app(cons, x2), x3))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(mult, 0), x0)
app(app(mult, app(s, x0)), x1)
app(app(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
list1
list2
list3
hamming

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

(15) PisEmptyProof (EQUIVALENT transformation)

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

(16) TRUE

(17) Obligation:

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

APP(app(lt, app(s, x)), app(s, y)) → APP(app(lt, x), y)

The TRS R consists of the following rules:

app(app(app(if, true), xs), ys) → xs
app(app(app(if, false), xs), ys) → ys
app(app(lt, app(s, x)), app(s, y)) → app(app(lt, x), y)
app(app(lt, 0), app(s, y)) → true
app(app(lt, y), 0) → false
app(app(eq, x), x) → true
app(app(eq, app(s, x)), 0) → false
app(app(eq, 0), app(s, x)) → false
app(app(merge, xs), nil) → xs
app(app(merge, nil), ys) → ys
app(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → app(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys))))
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(mult, 0), x) → 0
app(app(mult, app(s, x)), y) → app(app(plus, y), app(app(mult, x), y))
app(app(plus, 0), x) → 0
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
list1app(app(map, app(mult, app(s, app(s, 0)))), hamming)
list2app(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming)
list3app(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming)
hammingapp(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3)))

The set Q consists of the following terms:

app(app(app(if, true), x0), x1)
app(app(app(if, false), x0), x1)
app(app(lt, app(s, x0)), app(s, x1))
app(app(lt, 0), app(s, x0))
app(app(lt, x0), 0)
app(app(eq, x0), x0)
app(app(eq, app(s, x0)), 0)
app(app(eq, 0), app(s, x0))
app(app(merge, x0), nil)
app(app(merge, nil), x0)
app(app(merge, app(app(cons, x0), x1)), app(app(cons, x2), x3))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(mult, 0), x0)
app(app(mult, app(s, x0)), x1)
app(app(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
list1
list2
list3
hamming

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

(18) 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

lt1(s(x), s(y)) → lt1(x, y)

The a-transformed usable rules are
none


The following pairs can be oriented strictly and are deleted.


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

Recursive path order with status [RPO].
Precedence:
s1 > lt11

Status:
s1: multiset
lt11: multiset

The following usable rules [FROCOS05] were oriented: none

(19) Obligation:

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

app(app(app(if, true), xs), ys) → xs
app(app(app(if, false), xs), ys) → ys
app(app(lt, app(s, x)), app(s, y)) → app(app(lt, x), y)
app(app(lt, 0), app(s, y)) → true
app(app(lt, y), 0) → false
app(app(eq, x), x) → true
app(app(eq, app(s, x)), 0) → false
app(app(eq, 0), app(s, x)) → false
app(app(merge, xs), nil) → xs
app(app(merge, nil), ys) → ys
app(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → app(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys))))
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(mult, 0), x) → 0
app(app(mult, app(s, x)), y) → app(app(plus, y), app(app(mult, x), y))
app(app(plus, 0), x) → 0
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
list1app(app(map, app(mult, app(s, app(s, 0)))), hamming)
list2app(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming)
list3app(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming)
hammingapp(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3)))

The set Q consists of the following terms:

app(app(app(if, true), x0), x1)
app(app(app(if, false), x0), x1)
app(app(lt, app(s, x0)), app(s, x1))
app(app(lt, 0), app(s, x0))
app(app(lt, x0), 0)
app(app(eq, x0), x0)
app(app(eq, app(s, x0)), 0)
app(app(eq, 0), app(s, x0))
app(app(merge, x0), nil)
app(app(merge, nil), x0)
app(app(merge, app(app(cons, x0), x1)), app(app(cons, x2), x3))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(mult, 0), x0)
app(app(mult, app(s, x0)), x1)
app(app(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
list1
list2
list3
hamming

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

(20) PisEmptyProof (EQUIVALENT transformation)

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

(21) TRUE

(22) Obligation:

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

APP(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → APP(app(merge, xs), ys)
APP(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → APP(app(merge, xs), app(app(cons, y), ys))
APP(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → APP(app(merge, app(app(cons, x), xs)), ys)

The TRS R consists of the following rules:

app(app(app(if, true), xs), ys) → xs
app(app(app(if, false), xs), ys) → ys
app(app(lt, app(s, x)), app(s, y)) → app(app(lt, x), y)
app(app(lt, 0), app(s, y)) → true
app(app(lt, y), 0) → false
app(app(eq, x), x) → true
app(app(eq, app(s, x)), 0) → false
app(app(eq, 0), app(s, x)) → false
app(app(merge, xs), nil) → xs
app(app(merge, nil), ys) → ys
app(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → app(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys))))
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(mult, 0), x) → 0
app(app(mult, app(s, x)), y) → app(app(plus, y), app(app(mult, x), y))
app(app(plus, 0), x) → 0
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
list1app(app(map, app(mult, app(s, app(s, 0)))), hamming)
list2app(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming)
list3app(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming)
hammingapp(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3)))

The set Q consists of the following terms:

app(app(app(if, true), x0), x1)
app(app(app(if, false), x0), x1)
app(app(lt, app(s, x0)), app(s, x1))
app(app(lt, 0), app(s, x0))
app(app(lt, x0), 0)
app(app(eq, x0), x0)
app(app(eq, app(s, x0)), 0)
app(app(eq, 0), app(s, x0))
app(app(merge, x0), nil)
app(app(merge, nil), x0)
app(app(merge, app(app(cons, x0), x1)), app(app(cons, x2), x3))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(mult, 0), x0)
app(app(mult, app(s, x0)), x1)
app(app(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
list1
list2
list3
hamming

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

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

merge1(cons(x, xs), cons(y, ys)) → merge1(xs, ys)
merge1(cons(x, xs), cons(y, ys)) → merge1(xs, cons(y, ys))
merge1(cons(x, xs), cons(y, ys)) → merge1(cons(x, xs), ys)

The a-transformed usable rules are
none


The following pairs can be oriented strictly and are deleted.


APP(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → APP(app(merge, xs), ys)
APP(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → APP(app(merge, xs), app(app(cons, y), ys))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
merge1(x1, x2)  =  x1
cons(x1, x2)  =  cons(x2)

Recursive path order with status [RPO].
Precedence:
trivial

Status:
cons1: multiset

The following usable rules [FROCOS05] were oriented: none

(24) Obligation:

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

APP(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → APP(app(merge, app(app(cons, x), xs)), ys)

The TRS R consists of the following rules:

app(app(app(if, true), xs), ys) → xs
app(app(app(if, false), xs), ys) → ys
app(app(lt, app(s, x)), app(s, y)) → app(app(lt, x), y)
app(app(lt, 0), app(s, y)) → true
app(app(lt, y), 0) → false
app(app(eq, x), x) → true
app(app(eq, app(s, x)), 0) → false
app(app(eq, 0), app(s, x)) → false
app(app(merge, xs), nil) → xs
app(app(merge, nil), ys) → ys
app(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → app(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys))))
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(mult, 0), x) → 0
app(app(mult, app(s, x)), y) → app(app(plus, y), app(app(mult, x), y))
app(app(plus, 0), x) → 0
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
list1app(app(map, app(mult, app(s, app(s, 0)))), hamming)
list2app(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming)
list3app(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming)
hammingapp(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3)))

The set Q consists of the following terms:

app(app(app(if, true), x0), x1)
app(app(app(if, false), x0), x1)
app(app(lt, app(s, x0)), app(s, x1))
app(app(lt, 0), app(s, x0))
app(app(lt, x0), 0)
app(app(eq, x0), x0)
app(app(eq, app(s, x0)), 0)
app(app(eq, 0), app(s, x0))
app(app(merge, x0), nil)
app(app(merge, nil), x0)
app(app(merge, app(app(cons, x0), x1)), app(app(cons, x2), x3))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(mult, 0), x0)
app(app(mult, app(s, x0)), x1)
app(app(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
list1
list2
list3
hamming

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

(25) 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

merge1(cons(x, xs), cons(y, ys)) → merge1(cons(x, xs), ys)

The a-transformed usable rules are
none


The following pairs can be oriented strictly and are deleted.


APP(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → APP(app(merge, app(app(cons, x), xs)), ys)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
merge1(x1, x2)  =  merge1(x2)
cons(x1, x2)  =  cons(x2)

Recursive path order with status [RPO].
Precedence:
cons1 > merge11

Status:
cons1: multiset
merge11: multiset

The following usable rules [FROCOS05] were oriented: none

(26) Obligation:

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

app(app(app(if, true), xs), ys) → xs
app(app(app(if, false), xs), ys) → ys
app(app(lt, app(s, x)), app(s, y)) → app(app(lt, x), y)
app(app(lt, 0), app(s, y)) → true
app(app(lt, y), 0) → false
app(app(eq, x), x) → true
app(app(eq, app(s, x)), 0) → false
app(app(eq, 0), app(s, x)) → false
app(app(merge, xs), nil) → xs
app(app(merge, nil), ys) → ys
app(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → app(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys))))
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(mult, 0), x) → 0
app(app(mult, app(s, x)), y) → app(app(plus, y), app(app(mult, x), y))
app(app(plus, 0), x) → 0
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
list1app(app(map, app(mult, app(s, app(s, 0)))), hamming)
list2app(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming)
list3app(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming)
hammingapp(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3)))

The set Q consists of the following terms:

app(app(app(if, true), x0), x1)
app(app(app(if, false), x0), x1)
app(app(lt, app(s, x0)), app(s, x1))
app(app(lt, 0), app(s, x0))
app(app(lt, x0), 0)
app(app(eq, x0), x0)
app(app(eq, app(s, x0)), 0)
app(app(eq, 0), app(s, x0))
app(app(merge, x0), nil)
app(app(merge, nil), x0)
app(app(merge, app(app(cons, x0), x1)), app(app(cons, x2), x3))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(mult, 0), x0)
app(app(mult, app(s, x0)), x1)
app(app(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
list1
list2
list3
hamming

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

(27) PisEmptyProof (EQUIVALENT transformation)

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

(28) TRUE

(29) 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)

The TRS R consists of the following rules:

app(app(app(if, true), xs), ys) → xs
app(app(app(if, false), xs), ys) → ys
app(app(lt, app(s, x)), app(s, y)) → app(app(lt, x), y)
app(app(lt, 0), app(s, y)) → true
app(app(lt, y), 0) → false
app(app(eq, x), x) → true
app(app(eq, app(s, x)), 0) → false
app(app(eq, 0), app(s, x)) → false
app(app(merge, xs), nil) → xs
app(app(merge, nil), ys) → ys
app(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → app(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys))))
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(mult, 0), x) → 0
app(app(mult, app(s, x)), y) → app(app(plus, y), app(app(mult, x), y))
app(app(plus, 0), x) → 0
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
list1app(app(map, app(mult, app(s, app(s, 0)))), hamming)
list2app(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming)
list3app(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming)
hammingapp(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3)))

The set Q consists of the following terms:

app(app(app(if, true), x0), x1)
app(app(app(if, false), x0), x1)
app(app(lt, app(s, x0)), app(s, x1))
app(app(lt, 0), app(s, x0))
app(app(lt, x0), 0)
app(app(eq, x0), x0)
app(app(eq, app(s, x0)), 0)
app(app(eq, 0), app(s, x0))
app(app(merge, x0), nil)
app(app(merge, nil), x0)
app(app(merge, app(app(cons, x0), x1)), app(app(cons, x2), x3))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(mult, 0), x0)
app(app(mult, app(s, x0)), x1)
app(app(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
list1
list2
list3
hamming

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

(30) 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)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
APP(x1, x2)  =  APP(x2)
app(x1, x2)  =  app(x1, x2)
map  =  map
cons  =  cons

Recursive path order with status [RPO].
Precedence:
app2 > map > APP1
cons > map > APP1

Status:
APP1: multiset
cons: multiset
map: multiset
app2: multiset

The following usable rules [FROCOS05] were oriented: none

(31) Obligation:

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

app(app(app(if, true), xs), ys) → xs
app(app(app(if, false), xs), ys) → ys
app(app(lt, app(s, x)), app(s, y)) → app(app(lt, x), y)
app(app(lt, 0), app(s, y)) → true
app(app(lt, y), 0) → false
app(app(eq, x), x) → true
app(app(eq, app(s, x)), 0) → false
app(app(eq, 0), app(s, x)) → false
app(app(merge, xs), nil) → xs
app(app(merge, nil), ys) → ys
app(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → app(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys))))
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(mult, 0), x) → 0
app(app(mult, app(s, x)), y) → app(app(plus, y), app(app(mult, x), y))
app(app(plus, 0), x) → 0
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
list1app(app(map, app(mult, app(s, app(s, 0)))), hamming)
list2app(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming)
list3app(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming)
hammingapp(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3)))

The set Q consists of the following terms:

app(app(app(if, true), x0), x1)
app(app(app(if, false), x0), x1)
app(app(lt, app(s, x0)), app(s, x1))
app(app(lt, 0), app(s, x0))
app(app(lt, x0), 0)
app(app(eq, x0), x0)
app(app(eq, app(s, x0)), 0)
app(app(eq, 0), app(s, x0))
app(app(merge, x0), nil)
app(app(merge, nil), x0)
app(app(merge, app(app(cons, x0), x1)), app(app(cons, x2), x3))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(mult, 0), x0)
app(app(mult, app(s, x0)), x1)
app(app(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
list1
list2
list3
hamming

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

(32) PisEmptyProof (EQUIVALENT transformation)

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

(33) TRUE

(34) Obligation:

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

LIST1HAMMING
HAMMINGLIST1
HAMMINGLIST2
LIST2HAMMING
HAMMINGLIST3
LIST3HAMMING

The TRS R consists of the following rules:

app(app(app(if, true), xs), ys) → xs
app(app(app(if, false), xs), ys) → ys
app(app(lt, app(s, x)), app(s, y)) → app(app(lt, x), y)
app(app(lt, 0), app(s, y)) → true
app(app(lt, y), 0) → false
app(app(eq, x), x) → true
app(app(eq, app(s, x)), 0) → false
app(app(eq, 0), app(s, x)) → false
app(app(merge, xs), nil) → xs
app(app(merge, nil), ys) → ys
app(app(merge, app(app(cons, x), xs)), app(app(cons, y), ys)) → app(app(app(if, app(app(lt, x), y)), app(app(cons, x), app(app(merge, xs), app(app(cons, y), ys)))), app(app(app(if, app(app(eq, x), y)), app(app(cons, x), app(app(merge, xs), ys))), app(app(cons, y), app(app(merge, app(app(cons, x), xs)), ys))))
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(mult, 0), x) → 0
app(app(mult, app(s, x)), y) → app(app(plus, y), app(app(mult, x), y))
app(app(plus, 0), x) → 0
app(app(plus, app(s, x)), y) → app(s, app(app(plus, x), y))
list1app(app(map, app(mult, app(s, app(s, 0)))), hamming)
list2app(app(map, app(mult, app(s, app(s, app(s, 0))))), hamming)
list3app(app(map, app(mult, app(s, app(s, app(s, app(s, app(s, 0))))))), hamming)
hammingapp(app(cons, app(s, 0)), app(app(merge, list1), app(app(merge, list2), list3)))

The set Q consists of the following terms:

app(app(app(if, true), x0), x1)
app(app(app(if, false), x0), x1)
app(app(lt, app(s, x0)), app(s, x1))
app(app(lt, 0), app(s, x0))
app(app(lt, x0), 0)
app(app(eq, x0), x0)
app(app(eq, app(s, x0)), 0)
app(app(eq, 0), app(s, x0))
app(app(merge, x0), nil)
app(app(merge, nil), x0)
app(app(merge, app(app(cons, x0), x1)), app(app(cons, x2), x3))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(mult, 0), x0)
app(app(mult, app(s, x0)), x1)
app(app(plus, 0), x0)
app(app(plus, app(s, x0)), x1)
list1
list2
list3
hamming

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