More work on solution soundness, cleanup description of bisimilarity/cyclicity.