2.36/2.24 MAYBE 2.36/2.24 2.36/2.24 Problem: 2.36/2.24 ssp'(xs, 0()) -> nil() 2.36/2.24 ssp'(cons(y', ws), v) -> cons(y', ys') <= sub(v, y') = w, ssp'(ws, w) = ys' 2.36/2.24 ssp'(cons(x', xs'), v) -> cons(y', ys') <= get(xs') = tp2(y', zs), sub(v, y') = w, ssp'(cons(x', zs), w) = ys' 2.36/2.24 sub(z, 0()) -> z 2.36/2.24 sub(s(v), s(w)) -> z <= sub(v, w) = z 2.36/2.24 get(cons(y, ys)) -> tp2(y, ys) 2.36/2.24 get(cons(x', xs')) -> tp2(y, cons(x', zs)) <= get(xs') = tp2(y, zs) 2.36/2.24 2.36/2.24 Proof: 2.36/2.24 ConCon could not decide confluence of the system. 2.36/2.24 \cite{GNG13}, Theorem 9 does not apply. 2.36/2.24 2.36/2.24 EOF