(COMMENT
Merge two lists into one (append with strange order).
Always append the first element of the longer list to the result.
Do this as often as the sum of the length of both lists determines.
)
(VAR x y z ys zs c l)
(RULES
app(x, y) -> helpa(0, plus(length(x), length(y)), x, y)

plus(x, 0) -> x
plus(x, s(y)) -> s(plus(x, y))

length(nil) -> 0
length(cons(x, y)) -> s(length(y))

helpa(c, l, ys, zs) -> if(ge(c, l), c, l, ys, zs)

ge(x, 0) -> true
ge(0, s(x)) -> false
ge(s(x), s(y)) -> ge(x, y)

if(true, c, l, ys, zs) -> nil
if(false, c, l, ys, zs) -> helpb(c, l, greater(ys, zs), smaller(ys, zs))

greater(ys, zs) -> helpc(ge(length(ys), length(zs)), ys, zs)
smaller(ys, zs) -> helpc(ge(length(ys), length(zs)), zs, ys)
helpc(true, ys, zs) -> ys
helpc(false, ys, zs) -> zs

helpb(c, l, cons(y, ys), zs) -> cons(y, helpa(s(c), l, ys, zs)) 
)