Function exists_globally 

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

EG φ — SOME path from start on which the invariant prop holds forever. Greatest-fixpoint labelling (Emerson-Clarke): keep a prop-state alive while it retains a successor that is also alive; EG holds iff start survives. Bounded + zero-heap.