16.80/4.87	MAYBE
16.80/4.87	
16.80/4.87	Problem:
16.80/4.87	ssp'(xs, 0()) -> nil()
16.80/4.87	ssp'(cons(y', ws), v) -> cons(y', ys') <= sub(v, y') = w, ssp'(ws, w) = ys'
16.80/4.87	ssp'(cons(x', xs'), v) -> cons(y', ys') <= get(xs') = tp2(y', zs), sub(v, y') = w, ssp'(cons(x', zs), w) = ys'
16.80/4.87	sub(z, 0()) -> z
16.80/4.87	sub(s(v), s(w)) -> z <= sub(v, w) = z
16.80/4.87	get(cons(y, ys)) -> tp2(y, ys)
16.80/4.87	get(cons(x', xs')) -> tp2(y, cons(x', zs)) <= get(xs') = tp2(y, zs)
16.80/4.87	
16.80/4.87	Proof:
16.80/4.87	ConCon could not decide confluence of the system.
16.80/4.87	\cite{ALS94}, Theorem 4.1 does not apply.
16.80/4.87	ConCon could not decide whether all 8 critical pairs are joinable or not.
16.80/4.87	CP: nil() = cons(y', $4) <= get($6) = tp2(y', x'), sub(0(), y') = $5, ssp'(cons($3, x'), $5) = $4:
16.80/4.87	ConCon could not decide infeasibility of this critical pair.
16.80/4.87	
17.33/4.92	EOF