Function expand 

pub fn expand(set: &[Belief], belief: Belief, out: &mut [Belief]) -> usize

AGM expansion K + φ: add belief if absent. Writes the result into out, returns its length (no deductive closure beyond the explicit literals — a finite base model).