fact: Definition filter2s (pmod : positive) (ps : (states * states) * states) (s : state) := let (pstates, nstates) := ps in let (states1, states2) := pstates in if (in_states s states1 || in_states s states2)%bool then ps else match pmod with xH => ((s::states1,states2), s::nstates) | xO _ => ((states1,s::states2), s::nstates) | xI _ => ((s::states1,s::states2), s::nstates) end.
imports: ZArith List