and([
  always(or([not a1, next(x1)])),
  always(or([not x1, sometime(a2)])),
  always(or([not a2, next(x2)])),
  always(or([not x2, sometime(a3)])),
  always(or([not a3, next(x3)])),
  always(or([not x3, sometime(a4)])),
  always(or([not a4, next(x4)])),
  always(or([not x4, sometime(a1)])),

  or([x1]),
  always(or([not x1, sometime(x2)])),
  always(or([not x2, a1, a2, a3, a4])),

  or([y1]),
  always(or([not y1, sometime(y2)])),
  always(or([not y3, not a1])),
  always(or([not y2, y3])),
  always(or([not y2, y4])),
  always(or([not y4, next(y3)])),
  always(or([not y4, next(y4)]))
]).