29.07/8.41	YES
29.07/8.41	
29.07/8.41	Problem:
29.07/8.41	fstsplit(0(), x) -> nil()
29.07/8.41	fstsplit(s(n), nil()) -> nil()
29.07/8.41	fstsplit(s(n), cons(h, t)) -> cons(h, fstsplit(n, t))
29.07/8.41	sndsplit(0(), x) -> x
29.07/8.41	sndsplit(s(n), nil()) -> nil()
29.07/8.41	sndsplit(s(n), cons(h, t)) -> sndsplit(n, t)
29.07/8.41	empty(nil()) -> true()
29.07/8.41	empty(cons(h, t)) -> false()
29.07/8.41	leq(0(), m) -> true()
29.07/8.41	leq(s(n), 0()) -> false()
29.07/8.41	leq(s(n), s(m)) -> leq(n, m)
29.07/8.41	length(nil()) -> 0()
29.07/8.41	length(cons(h, t)) -> s(length(t))
29.07/8.41	app(nil(), x) -> x
29.07/8.41	app(cons(h, t), x) -> cons(h, app(t, x))
29.07/8.41	map_f(pid, nil()) -> nil()
29.07/8.41	map_f(pid, cons(h, t)) -> app(f(pid, h), map_f(pid, t))
29.07/8.41	process(store, m) -> process(app(map_f(self(), nil()), sndsplit(m, store)), m) <= leq(m, length(store)) = true(), empty(fstsplit(m, store)) = false()
29.07/8.41	process(store, m) -> process(sndsplit(m, app(map_f(self(), nil()), store)), m) <= leq(m, length(store)) = false(), empty(fstsplit(m, app(map_f(self(), nil()), store))) = false()
29.07/8.41	
29.07/8.41	Proof:
29.07/8.41	This system is confluent.
29.07/8.41	By \cite{SMI95}, Corollary 4.7 or 5.3.
29.07/8.41	This system is oriented.
29.07/8.41	This system is of type 3 or smaller.
29.07/8.41	This system is right-stable.
29.07/8.41	This system is properly oriented.
29.07/8.41	This is an overlay system.
29.07/8.41	This system is left-linear.
29.07/8.41	All 2 critical pairs are trivial or infeasible.
29.07/8.41	CP: process(app(map_f(self(), nil()), sndsplit(z, x')), z) = process(sndsplit(z, app(map_f(self(), nil()), x')), z) <= leq(z, length(x')) = false(), empty(fstsplit(z, app(map_f(self(), nil()), x'))) = false(), leq(z, length(x')) = true(), empty(fstsplit(z, x')) = false():
29.07/8.41	This critical pair is infeasible.
29.07/8.41	This critical pair is conditional.
29.07/8.41	This critical pair has some non-trivial conditions.
29.07/8.41	usabel rules
29.07/8.41	growing approximation
29.07/8.41	fstsplit(s(n), cons(h, t)) -> cons(y, fstsplit(z, x'))
29.07/8.41	map_f(pid, nil()) -> nil()
29.07/8.41	app(cons(h, t), x) -> cons(y', app(z', x))
29.07/8.41	fstsplit(s(n), nil()) -> nil()
29.07/8.41	empty(nil()) -> true()
29.07/8.41	empty(cons(h, t)) -> false()
29.07/8.41	fstsplit(0(), x) -> nil()
29.07/8.41	app(nil(), x) -> x
29.07/8.41	'\Sigma(empty(fstsplit(z, app(map_f(self(), nil()), x')))) \cap (->^*_R)[\Sigma(REN(false()))]' is empty.
29.07/8.41	CP: process(sndsplit(z, app(map_f(self(), nil()), x')), z) = process(app(map_f(self(), nil()), sndsplit(z, x')), z) <= leq(z, length(x')) = true(), empty(fstsplit(z, x')) = false(), leq(z, length(x')) = false(), empty(fstsplit(z, app(map_f(self(), nil()), x'))) = false():
29.07/8.41	This critical pair is infeasible.
29.07/8.41	This critical pair is conditional.
29.07/8.41	This critical pair has some non-trivial conditions.
29.07/8.41	usabel rules
29.07/8.41	growing approximation
29.07/8.41	fstsplit(s(n), cons(h, t)) -> cons(y, fstsplit(z, x'))
29.07/8.41	map_f(pid, nil()) -> nil()
29.07/8.41	app(cons(h, t), x) -> cons(y', app(z', x))
29.07/8.41	fstsplit(s(n), nil()) -> nil()
29.07/8.41	empty(nil()) -> true()
29.07/8.41	empty(cons(h, t)) -> false()
29.07/8.41	fstsplit(0(), x) -> nil()
29.07/8.41	app(nil(), x) -> x
29.41/8.42	'\Sigma(empty(fstsplit(z, app(map_f(self(), nil()), x')))) \cap (->^*_R)[\Sigma(REN(false()))]' is empty.
29.41/8.42	
31.12/8.91	EOF