fact: Definition mm2_bounded (P : list mm2_instr) (k: nat) (x: mm2_state) : Prop := exists (L: list mm2_state), (length L <= k) /\ (forall (y: mm2_state), P // x ↠ y -> In y L).
imports: List Relations.Relation_Operators