Member predicate ControlFlowTree::succ

Holds if succ is a control flow successor for pred, given that pred finishes with completion c.

predicate succ(ControlFlowElement pred, ControlFlowElement succ, Completion c)