CCS semantics via proved transition systems and rewriting logic