Characterizing and proving operational termination of deterministic conditional term rewriting systems