Function always_globally 

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

AG φ — EVERY state reachable from start (including start) satisfies the invariant inv. Zero-heap BFS.