0.00/0.46 MAYBE 0.00/0.46 0.00/0.46 Problem: 0.00/0.47 ssp'(xs, v) -> ys <= subseteq_m(ys, xs) = tt(), sum(ys) = v 0.00/0.47 subseteq_m(nil(), ys) -> tt() 0.00/0.47 subseteq_m(cons(x, xs), ys) -> z <= del(x, ys) = some(ws), subseteq_m(xs, ws) = z 0.00/0.47 del(x, nil()) -> none() 0.00/0.47 del(x, cons(x, ys)) -> some(ys) 0.00/0.47 del(x, cons(y, ys)) -> some(cons(y, zs)) <= del(x, ys) = some(zs) 0.00/0.47 sum(nil()) -> 0() 0.00/0.47 add(x, 0()) -> x 0.00/0.47 add(x, s(y)) -> s(z) <= add(x, y) = z 0.00/0.47 0.00/0.47 Proof: 0.00/0.47 ConCon could not decide confluence of the system. 0.00/0.47 \cite{GNG13}, Theorem 9 does not apply. 0.00/0.47 0.00/0.47 EOF