Function necessary 

pub fn necessary(
    graph: &[NQuin],
    world: u64,
    prop: u64,
    accesses: u64,
    holds: u64,
) -> bool

□φ (necessary) — ALL worlds accessible from world satisfy prop. Vacuously true when no worlds are accessible (standard modal semantics).