begin

@ N1 (  (<>true)
      & (<><>true)
      & ([][]<->N1)
      & ([] (   (<>true)
              & (down x1 . []-x1)
              & (down x1 . [][]-x1)
              & (down x1 . [][]<->x1)
            )
        )
     )
end