cycle1: [guard1,2] Po -enum< P1 >elim- P2

cycle2: [guard2,1] Po -enum< P3 -enum< P4 -enum< P5 >elim- P6

Similarly guard2,1 may specify if the problem set (P3, P4, P5 or P6) is empty then control is transferred to cycle1. In other words if cycle2 produces no solutions then M_sis should switch to cycle1. If P6 is non-empty then M_sis halts.