0.00/0.46 MAYBE 0.00/0.46 0.00/0.46 Problem: 0.00/0.47 div(z, y) -> x <= mul(x, y) = z, gt(y, 0()) = tt() 0.00/0.47 mul(x, 0()) -> 0() 0.00/0.47 mul(0(), y) -> 0() 0.00/0.47 mul(s(x), s(y)) -> s(z) <= mul(x, s(y)) = w, add(w, y) = z 0.00/0.47 gt(0(), y) -> ff() 0.00/0.47 gt(s(x), 0()) -> tt() 0.00/0.47 gt(s(x), s(y)) -> z <= gt(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{SMI95}, Corollary 4.7 or 5.3 do not apply. 0.00/0.47 0.00/0.48 EOF