diff --git a/README.md b/README.md
index 439884a..1219fe4 100644
--- a/README.md
+++ b/README.md
@@ -6,7 +6,7 @@ A collection of examples of using PSL for functional and formal verification of
 
 This is a project with the purpose to get a current state of PSL implementation in GHDL. It probably will find unsupported PSL features, incorrect implemented features or simple bugs like GHDL crashs.
 
-It is also intended for experiments with PSL when learning the language. You can play around with the examples, as they are pretty simple. You can comment out failing assertions if you want to have a sucessful proof os simulation if you want. You can change them to see what happens. Have fun!
+It is also intended for experiments with PSL when learning the language. You can play around with the examples, as they are pretty simple. You can comment out failing assertions if you want to have a successful proof or simulation if you want. You can change them to see what happens. Have fun!
 
 
 The next two lists will grow during further development
@@ -22,6 +22,7 @@ The next two lists will grow during further development
 * implication operator
 * next operator
 * next[n] operator
+* next_a[i to j] operator
 * next_event operator
 * next_event[n] operator
 * until operator
@@ -31,10 +32,9 @@ The next two lists will grow during further development
 
 ## PSL features not yet supported by GHDL:
 
-* next_a[i:j] operator
-* next_e[i:j] operator
-* next_event_a[i:j] operator
-* next_event_e[i:j] operator
+* next_e[i to j] operator
+* next_event_a[i to j] operator
+* next_event_e[i to j] operator
 
 ## PSL features supported by GHDL but with wrong behaviour
 
diff --git a/formal/psl_next_a.sby b/formal/psl_next_a.sby
new file mode 100644
index 0000000..5e3e8e4
--- /dev/null
+++ b/formal/psl_next_a.sby
@@ -0,0 +1,18 @@
+[tasks]
+prove
+
+[options]
+depth 25
+prove: mode bmc
+
+[engines]
+prove: smtbmc z3
+
+[script]
+prove: ghdl --std=08 pkg.vhd sequencer.vhd psl_next_a.vhd -e psl_next_a
+prep -top psl_next_a
+
+[files]
+../src/pkg.vhd
+../src/sequencer.vhd
+../src/psl_next_a.vhd
diff --git a/formal/tests.mk b/formal/tests.mk
index 270d563..2d9b166 100644
--- a/formal/tests.mk
+++ b/formal/tests.mk
@@ -3,6 +3,7 @@ psl_always \
 psl_never \
 psl_next \
 psl_next_3 \
+psl_next_a \
 psl_next_event \
 psl_next_event_4 \
 psl_until \
diff --git a/src/psl_next_a.vhd b/src/psl_next_a.vhd
new file mode 100644
index 0000000..745c5a0
--- /dev/null
+++ b/src/psl_next_a.vhd
@@ -0,0 +1,49 @@
+library ieee;
+  use ieee.std_logic_1164.all;
+
+use work.pkg.all;
+
+
+entity psl_next_a is
+  port (
+    clk : in std_logic
+  );
+end entity psl_next_a;
+
+
+architecture psl of psl_next_a is
+
+  signal a, b : std_logic;
+  signal c, d : std_logic;
+  signal e, f : std_logic;
+
+begin
+
+
+  --                              01234567890
+  SEQ_A : sequencer generic map ("__-_-______") port map (clk, a);
+  SEQ_B : sequencer generic map ("_____-_-___") port map (clk, b);
+
+  --                              01234567890
+  SEQ_C : sequencer generic map ("__-_-______") port map (clk, c);
+  SEQ_D : sequencer generic map ("_____-_____") port map (clk, d);
+
+  --                              01234567890
+  SEQ_E : sequencer generic map ("__-_-______") port map (clk, e);
+  SEQ_F : sequencer generic map ("_____-----_") port map (clk, f);
+
+
+  -- All is sensitive to rising edge of clk
+  default clock is rising_edge(clk);
+
+  -- This assertion doesn't hold at cycle 6
+  NEXT_0_a : assert always (a -> next_a[3 to 5] (b));
+
+  -- This assertion doesn't hold at cycle 6
+  NEXT_1_a : assert always (c -> next_a[3 to 5] (d));
+
+  -- This assertion holds
+  NEXT_2_a : assert always (e -> next_a[3 to 5] (f));
+
+
+end architecture psl;