Function bernstein_independent 

pub fn bernstein_independent(a: &Op, b: &Op) -> bool

Bernstein’s conditions — a and b commute (are independent) iff neither writes a cell the other reads or writes. This is the independence relation of the trace monoid: precisely the pairs whose commutation square is a 2-cell in ProofPoset. (Read–read sharing is fine; reads commute.)