Function all_finally 

pub fn all_finally(
    graph: &[NQuin],
    start: u64,
    prop: u64,
    next: u64,
    holds: u64,
) -> bool

AF φ — on ALL paths from start, prop eventually holds. Least-fixpoint labelling: a state is AF if it satisfies prop, or it has ≥1 successor and ALL successors are AF (a prop-free cycle or prop-free deadlock falsifies it). Bounded + zero-heap.