an(1,1)\land\bothF{\tpc 1}\imp \subst{an(2,2)}{x|x'}{y|y} \\
an(2,2)\land\bothF{\tpc 2} \land x > 0 \land x' > 0 \imp an(3,3) \\
an(2,2)\land\bothF{\tpc 2} \land x\ngtr 0 \land x'\ngtr 0 \imp  an(6,6) \\
an(3,3)\land\bothF{\tpc 3} \land x\mod 2=0 \land x'\mod 2=0 \imp an(4,4) \\
an(3,3)\land\bothF{\tpc 3} \land x\mod 2\neq 0 \land x'\mod 2\neq 0 \imp an(5,5) \\
%\models x:=x-1\sep x:=x-1 : \rspec{an(4,4)}{an(2,2)}     \\
an(4,4)\land\bothF{\tpc 4} \imp \subst{an(2,2)}{x|x'}{x-1|x'-1}     \\
%\models x:=x-2\sep x:=x-2 : \rspec{an(5,5)}{an(2,2)}
an(5,5)\land\bothF{\tpc 5}\imp \subst{an(2,2)}{x|x'}{x-2|x'-2}
\end{array}
\end{equation}

All the other VCs have false antecedent or precondition.
For example, one VC is
$an(2,2)\land\bothF{\tpc 2} \land x > 0 \land x' < 0 \imp an(3,6) $
but $an(2,2)$ says $x=x'$ so the antecedent simplifies to false.
The annotation is valid.

To construct a proof of $c0\sep c0:\rspec{true}{x=x'}$
in RHL+ we use the normal form in (<ref>),
i.e., $\spc 1; d0$ where

\[ d0: \quad \keyw{do}
\begin{array}[t]{l}
\tpc 1 \gcto x:=y; \spc 2 \\
\gcsep \tpc 2 \land x > 0 \gcto \spc 3 \\
\gcsep \tpc 2 \land x \ngtr 0 \gcto \spc 6  \\
\gcsep \tpc 3 \land x\mod 2=0 \gcto \spc 4 \\
\gcsep \tpc 3 \land x\mod 2\neq 0 \gcto \spc 5 \\
\gcsep \tpc 4 \gcto \lassg{}{x}{x-1}; \spc 2 \\
\gcsep \tpc 5 \gcto \lassg{}{x}{x-2}; \spc 2
\quad \keyw{od}
\end{array}
\]

We will use rule rDo instantiated with $\Q,\Lrel,\R:=\S,\mathit{false},\mathit{false}$,
with the following as loop invariant.

\[\S: \quad
\begin{array}[t]{l}
(pc=1=pc' \imp true) \land \\
\quant{\land}{i}{2\leq i\leq 6}{pc=i=pc' \imp x=x'} \land \\
1\leq pc \leq 6 \land pc=pc'
\end{array}
\]

Note that $1\leq pc \leq 6 \land pc=pc'$ is equivalent to
$\encode{J}\lor \bothF{\tpc 6}$.

Writing $gcs$ for the body of $d0$,
the side condition of rDo is thus

\[ \S\imp (\leftF{\enab(gcs)} = \rightF{\enab(gcs)})
\lor (\mathit{false} \land \leftF{\enab(gcs)})
\lor (\mathit{false} \land \rightF{\enab(gcs)}) \]

which is valid
by $\leftF{pc}=\rightF{pc}$, i.e., $pc=pc'$, from $\S$.
There are three sets of premises in rDo.  The first set relates a guarded command on the left to $\skipc$ on the right, with a precondition including the left alignment condition which here is $\mathit{false}$, so these premises are immediate using rule rFalse.
The second set of premises is similar, with $\skipc$ on the left, and again precondition $\mathit{false}$.

What remains is the third set of premises, which require us to relate each guarded command in $d0$, on the left, with each guarded command of $d0$ on the right, under precondition $\encode{J}$.
There are $7\times 7$ such premises,
each of the form $d\sep d': \rspec{\leftF{e}\land\rightF{e'}\land\S}{\S}$
for $e\gcto d$ and $e'\gcto d'$ in $d0$.

Here is one case: for the guarded commands
$ \tpc 1 \gcto x:=y; \spc 2$ and
$ \tpc 2 \land x > 0 \gcto \spc 3$ we must show

\[ x:=y;\spc 2 \sep \spc 3 : \rspec{\leftF{\tpc 1}\land\rightF{\tpc 2\land x>0}\land \S}{\S} \]

The precondition has a contradiction:
$\leftF{\tpc 1}$ and $\rightF{\tpc 2}$ contradict the conjunct $pc=pc'$ of $\S$.
So the displayed judgment can be proved using rConseq and rFalse.

In fact all cases where control is at different places in the two programs,
or different branches are being taken, can be proved using rFalse.
Some of those cases contradict $pc=pc'$, as above.
The other cases contradict $x=x'$, for example the case
of $\tpc 2 \land x > 0 \gcto \spc 3$ versus
$\tpc 2 \land x \ngtr 0 \gcto \spc 6$.

What remain are the cases where control is at the same point on both sides and the same branch (of the original program) is being taken.  We consider these in turn.

* $\tpc y \gcto x:=y; \spc 2$.  For this we must show

\begin{equation}\label{eq:A}
x:=y; \spc 2 \mid x:=y; \spc 2 : \rspec{\leftF{\tpc 1}\land\rightF{\tpc 1}\land\S}{\S}
\end{equation}

By a VC in (<ref>) we have
$an(1,1)\land\bothF{\tpc 1}\imp\subst{an(2,2)}{x|x'}{y|y}$
so using rAsgnAsgn and then rConseq we get
$x:=y \sep x':=y : \rspec{an(1,1)\land\bothF{\tpc 1}}{an(2,2)}$.
By rAsgnAsgn and $pc$ not free in $an(2,2)$ we have

\[ \begin{array}{l}
\spc 2 \sep \spc 2 : \rspec{\leftF{2=2}\land\rightF{2=2}\land  an(2,2)  }{\leftF{\tpc 2}\land\rightF{\tpc 2}\land an(2,2)}
\end{array}
\]

hence by rConseq we have

\[ \spc 2 \sep \spc 2 : \rspec{an(2,2)}{\leftF{\tpc 2}\land\rightF{\tpc 2}\land an(2,2)} \]

So by rSeq we have

\[ \begin{array}{l}
x:=y; \spc 2 \sep x:=y; \spc 2 : \rspec{an(1,1)\land\bothF{\tpc 1}}{ \leftF{\tpc 2}\land\rightF{\tpc 2}\land an(2,2)}
\end{array}
\]

so by rConseq and definition of $\S$ we have (<ref>).

* $\tpc 2 \land x > 0 \gcto \spc 3$.
By rAsgnAsgn, using that $pc$ is distinct from $x$ and is not free in $an(3,3)$, we have

\[
\begin{array}{l}
\spc 3 \sep \spc 3 : \rspec{\bothF{3=3 } \land an(3,3) }{ \bothF{\tpc 3} \land an(3,3)}
\end{array}
\]

so by rConseq we have

\[\begin{array}{l}
\spc 3 \sep \spc 3 : \rspec{an(3,3) }{ \bothF{\tpc 3}\land an(3,3)}
\end{array}\]

Using the VC $an(2,2)\land\bothF{\tpc 2} \land \bothF{x>0}\imp an(3,3)$
with rConseq we get

\[\begin{array}{l}
\spc 3 \sep \spc 3 : \rspec{\bothF{x > 0}\land an(2,2)\land\bothF{\tpc 2} }{ \bothF{\tpc 3}\land an(3,3)}
\end{array}\]

From the definition of $\S$ we have
$\bothF{\tpc 2}\land S \imp an(2,2)$ and
$\bothF{\tpc 3}\land an(3,3) \imp \S$
so by rConseq we get what is required:

\[ \spc 3 \sep \spc 3 : \rspec{\bothF{\tpc 2 \land x > 0}\land \S }{\S}
\]

* The remaining five cases are proved similarly; the cases are
$\tpc 2 \land x \ngtr 0 \gcto \spc 6$,
$\tpc 3 \land x\mod 2=0 \gcto \spc 4$,
$\tpc 3 \land x\mod 2\neq 0 \gcto \spc 5$,
$\tpc 4 \gcto \lassg{}{x}{x-1}; \spc 2 $, and
$\tpc 5 \gcto \lassg{}{x}{x-2}; \spc 2  $

Having established the premises and side condition of rule rDo, we infer its conclusion:

\[ d0\sep d0: \rspec{\S}{\S\land\neg\leftF{\enab(gcs)}\land\neg\rightF{\enab(gcs)} } \]

As in the proof for unary correctness of $d0$,
we have that $\enab(gcs)$ is equivalent to $1\leq pc <6$,
so in conjunction with $\S$ we can apply rConseq to get

\[ d0\sep d0: \rspec{\S}{\S\land \bothF{\tpc 6}} \]

Another use of rConseq and the definition of $\S$ yields

\[ d0\sep d0: \rspec{\S}{x=x'} \]

Yet another use of rConseq and definition of $\S$ yields

\[ d0\sep d0: \rspec{\bothF{\tpc 1}}{x=x'} \]

By rAsgnAsgn and rConseq we have
$\spc 1 \sep \spc 1 : \rspec{true}{\leftF{\tpc 1}\land\rightF{\tpc 1}}$.
Hence by rSeq we have

\[ \spc 1; d0 \Sep \spc 1; d0 :  \rspec{true}{x=x'} \]

Now, using the equivalence (<ref>) and rule rRewrite we get

\[ c0^+ \sep c0^+ :  \rspec{true}{x=x'} \]

Next, $pc$ has the ghost property so by rGhost we get

\[ \erase(pc,c0^+) \sep \erase(pc,c0^+) :  \rspec{true}{x=x'} \]

As noted in the unary proof (Sect. <ref>) we have $ \erase(pc,c0^+) \kateq c0$,
so by rRewrite we get

\[ c0 \sep c0 :  \rspec{true}{x=x'} \]

§.§ A conditionally aligned example

\(
\begin{array}{ll}
%% c4: &
%% \lassg{1}{y}{x}; \lassg{2}{z}{24}; \lassg{3}{w}{0};
%%    \lwhilec{4}{y\neq 4}{
%%       \lifc{5}{w \mod 2 = 0}{
%%         \lassg{6}{z}{z*y}; \lassg{7}{y}{y-1} }{\lskipc{8}}; \lassg{9}{w}{w+1} }
%% \\[.3ex]
%% c5: &
%% \lassg{1}{y}{x}; \lassg{2}{z}{16}; \lassg{3}{w}{0};
%%     \lwhilec{4}{y\neq 4}{
%%           \lifc{5}{w \mod 3 = 0}{
%%            \lassg{6}{z}{z*2}; \lassg{7}{y}{y-1}}{\lskipc{8}}; \lassg{9}{w}{w+1} }
%% \\[1ex]
c4: &
\lassg{1}{y}{x}; \lassg{2}{z}{24}; \lassg{3}{w}{0};
\ldogc{4}{
y\neq 4 \gcto
\lifgc{5}{ w \mod 2 = 0 \gcto \lassg{6}{z}{z*y}; \lassg{7}{y}{y-1}
\gcsep w\mod 2 \neq 0 \gcto \lskipc{8}}
; \lassg{9}{w}{w+1} }
\\[.3ex]
c5: &
\lassg{1}{y}{x}; \lassg{2}{z}{16}; \lassg{3}{w}{0};
\ldogc{4}{y\neq 4 \gcto
\lifgc{5}{w \mod 3 = 0 \gcto \lassg{6}{z}{z*2}; \lassg{7}{y}{y-1}
\gcsep w \mod 3 \neq 0 \gcto \lskipc{8}}
; \lassg{9}{w}{w+1} }
\end{array}
\)

Commands c4 and c5 adapted from <cit.>.

We consider two example programs used in prior work to illustrate the conditionally aligned loop rule (our rDo).
We use them to illustrate a non-lockstep alignment automaton
used in an IAM proof and then in the corresponding RHL+ proof.
The two commands are in Fig. <ref>.

Both loops maintain $y\geq 4$ as invariant.
The loop in $c4$ maintains the invariants  $x! \cdot 4! = z \cdot y!$ and
the loop in $c5$ maintains $2^x\cdot 2^4 = z \cdot 2^y$, owing to the respective
initializations of $z=4!=24$ and $z=2^4=16$.
(Postfix $!$ means factorial as usual, and is not to be confused with the prefix abbreviation $\spc n$ for $\lassg{}{pc}{n}$.)
The reader may enjoy to use the proof rules to show

\[ c4 \sep c5 : \rspec{x = x'\land x > 3}{z>z'} \]

using loop alignment conditions $\Lrel := \leftF{ w\mod 2\neq 0 }$ and $\R := \rightF{  w'\mod 3\neq 0 }$
and rule rDo.
But we give an automaton and then verify the program in automaton normal form.
The alignment enables use of annotations with simple predicates, avoiding any reference
to the factorial or exponential functions.

Here is an interesting variation on the example.  Replace the moduli 2 (in $c4$) and 3 (in $c5$) by  variables $u$ and $v$ respectively, that are not modified by the program.
Conjoin to the precondition that $1 < u$ and $1 < v'$.
The proofs in this section go through essentially unchanged.
But the variation goes beyond what can be handled by Churchill et al <cit.>
and similar techniques that are restricted to linear arithmetic in alignment conditions
and in relational invariants.

We prove

\begin{equation}\label{eq:specc4c5}
\aut(c4,0) \sep \aut(c5,0) : \rspec{x = x'\land x > 3}{z>z'}
\end{equation}

using $0$ as final label.

Define $L,R,J$ as follows; recall that
$[i|j]$ is  set of automaton states where control is at $(i,j)$.

\[ \begin{array}{l}
J:\quad [1|1]\lor[2|2]\lor[3|3]\lor([4|4]\land\leftF{ w\mod 2 = 0}\land \rightF{ w'\mod 3 = 0})\lor
\\
L: \quad
([4|4]\land\leftF{ w\mod 2\neq 0})
\lor [5|4]
\lor [8|4]
\lor [9|4]
\\
R: \quad
([4|4]\land\rightF{w'\mod 3\neq 0})
\lor [4|5]
\lor [4|8]
\lor [4|9]
\end{array}
\]

Note that $(L,R,J)$ is live,
because assignments are always enabled and at $(5,5)$ the conditional is total.
It is straightforward but tedious to check that the following
is an inductive $(x=x')$-invariant: $J\lor L\lor R\lor [0|0]$.
So the alignment automaton
$\aprod(\aut(c4,0),\aut(c5,0),L,R,J)$ is manifestly $(x=x')$-adequate.

\(  \begin{array}{ll}
(n,m) & an(n,m) \\\hline
(1,1) & x=x'\land x>3 \qquad\mbox{precondition}\\
(2,2)  & y=y' \land y>3 \\
(3,3)  & \S \\ %y=y' \land y>3 \land z>z'>0 \\
(4,4)  & \S \\
(5,5)  & \S \land y>4 \land w\mod 2 = 0 = w'\mod 3 \\
(6,6)  & \S \land y>4 \land w\mod 2 = 0 = w'\mod 3 \\
(7,7)  & \S \land y>4 \land w\mod 2 = 0 = w'\mod 3 \\
(9,9)  & \S \\
(5,4)  & \S \land w\mod 2 \neq 0 \\
(8,4)  & \S   \\
(9,4)  & \S   \\
(4,5)  & \S \land w'\mod 3\neq 0  \\
(4,8)  & \S    \\
(4,9)  & \S   \\
(0,0) & z>z' \qquad\mbox{postcondition} \\
(\_,\_) & \mathit{false} \quad\mbox{in all other cases}
\end{array}
\)
Annotation for $c4,c5$ example.

Using the predicate

\[ \S: \qquad y=y' \land y>3 \land z>z'>0 \]

we define annotation $an$ in Fig. <ref>.

The automaton has $10^2$ control points $(i,j)$, and thus $10^4$ pairs of control points
for which VCs must hold.
Most are infeasible of course.
For example, consider the VC for $((5,5),(8,8))$.
The automaton only transitions from $(5,5)$ to $(8,8)$ when
$w\mod 2\neq 0$ and $w'\mod 3\neq 0$ but this contradicts $an(5,5)$ so the VC holds vacuously.
As another example, the automaton can transition from $(5,4)$ to $(6,4)$ when $w\mod 2 = 0$,
but this contradicts $an(5,4)$.

Fig. <ref> shows the VCs where the automaton has transitions from states that satisfy the annotation.
They all follow by propositional reasoning and a bit of linear inequality reasoning.
So we have an IAM proof the programs satisfy their spec (<ref>)
in accord with Corollary <ref>.

\(\begin{array}{lll}
((n,n'),(m,m'))\hspace*{-3em} & \qquad \mbox{VC for } ((n,n'),(m,m')) \\\hline

((1,1),(2,2)) &
J\land[1|1]\land x=x'\land x>3 \imp \subst{(y=y'\land y>3)}{y|y'}{x|x'}
\\
((2,2),(3,3)) &
J\land[2|2]\land y=y' \land y>3 \imp \subst{\S}{z|z'}{24|16}
\\
((3,3),(4,4)) &
J\land[3|3]\land \S \imp \subst{\S}{w|w'}{0|0}
\\
((4,4),(5,5)) &
J\land[4|4]\land \S\land y\neq 4 \land y'\neq 4 \imp \S\land y>4\land w\mod 2=0=w'\mod 3
& \mbox{\hspace*{-8em}(proved using $J$)}
\\
((4,4),(0,0)) &
J\land[4|4]\land \S\imp z>z'
\\
((5,5),(6,6)) &
J\land[5|5]\land w\mod 2=0=w'\mod 3 \land\S\land y>4 \imp \S\land y>4\land w\mod 2=0=w'\mod 3
\\
((6,6),(7,7)) &
J\land[6|6]\land w\mod 2=0=w'\mod 3 \land\S\land y>4 \imp
\subst{(\S\land y>4\land w\mod 2=0=w'\mod 3)}{z|z'}{z*y|z'*2}
\\
((7,7),(9,9)) &
J\land[7|7]\land w\mod 2=0=w'\mod 3 \land\S\land y>4 \imp
\subst{\S}{y|y'}{y-1|y'-1}
\\
((9,9),(4,4)) &
J\land[9|9]\land\S \imp \subst{\S}{w|w'}{w+1|w'+1}
\\
((4,4),(5,4)) &
L\land[4|4]\land \S\land y\neq 4 \imp \S \land w\mod 2 \neq 0
\\
((5,4),(8,4)) &
L\land[5|4]\land \S\land w\mod 2\neq 0 \imp \S
\\
((8,4),(9,4)) &
L\land[8|4]\land \S\imp \S
\\
((9,4),(4,4)) &
L\land[9|4]\land \S\imp \S
\\
((4,4),(5,4)) &
R\land[4|4]\land \S\land y'\neq 4 \imp \S \land w'\mod 3 \neq 0
\\
((4,5),(4,8)) &
R\land[4|5]\land \S\land w'\mod 3\neq 0 \imp \S
\\
((4,8),(4,9)) &
R\land[4|8]\land \S\imp \S
\\
((4,9),(4,4)) &
R\land[4|9]\land \S\imp \S
\end{array}
\)

The nontrivial VCs for

For a deductive proof in RHL+,
let $pc$ be a fresh variable, i.e., one distinct from the variables of $c4,c5$ since these are the only variables that occur in the annotation or in the alignment conditions.
Fig. <ref> spells out the $pc$-encoded store relations $\encode{L},\encode{R},\encode{J}$, that express the alignment conditions $L,R,J$ as predicates on $pc$.

\[ \begin{array}{l}
\encode{J}:
\quad
\bothF{\tpc 1}\lor\bothF{\tpc 2}\lor\bothF{\tpc 3}\lor(\bothF{\tpc 4}\land\leftF{ w\mod 2 = 0}\land \rightF{ w'\mod 3 = 0})\lor \bothF{\tpc 5}\lor\bothF{\tpc 6}\lor\bothF{\tpc 7}\lor\bothF{\tpc 9}
\\
\encode{L}:
\quad
(\bothF{\tpc 4}\land\leftF{ w\mod 2\neq 0})
\lor (\bothF{\tpc 5\sep\tpc 4})
\lor (\bothF{\tpc 8\sep\tpc 4})
\lor (\bothF{\tpc 9\sep\tpc 4})
\\
\encode{R}:
\quad
(\bothF{\tpc 4}\land\rightF{ w\mod 3\neq 0})
\lor (\bothF{\tpc 4\sep\tpc 5})
\lor (\bothF{\tpc 4\sep\tpc 8})
\lor (\bothF{\tpc 4\sep\tpc 9})
\end{array}
\]

Store relations $\encode{L},\encode{R},\encode{J}$ for $c4,c5$.

We aim to prove $\rspec{x=x'\land x>3}{z>z'}$ for the normal forms of $c4$ and $c5$,
instantiating rule rDo
with $\Lrel:=\encode{L}$, $\R:=\encode{R}$, and invariant
$\Q$ defined by

\[ \Q: \quad \S\land(\encode{L}\lor\encode{R}\lor\encode{J}\lor\bothF{\tpc 0}) \]

In the unary example of Sect. <ref>,
the invariant $I$ includes a conjunct that constrains the range of $pc$.
In $\Q$ the range on both sides is constrained by
$\encode{L}\lor\encode{R}\lor\encode{J}\lor\bothF{\tpc 0}$.

The normal form of $c4$ is $\spc 1; d4$ where

\[ \graybox{d4:}\quad \keyw{do}
\begin{array}[t]{l}
\tpc 1 \gcto y:=x; \spc 2 \\
\gcsep \tpc 2 \gcto z:=24; \spc 3 \\
\gcsep \tpc 3 \gcto w:=0; \spc 4 \\
\gcsep \tpc 4 \land y\neq 0 \gcto \spc 5 \\
\gcsep \tpc 4 \land y=0 \gcto \spc 0 \\
\gcsep \tpc 5 \land w\mod 2 = 0 \gcto \spc 6 \\
\gcsep \tpc 5 \land w\mod 2 \neq 0 \gcto \spc 8 \\
\gcsep \tpc 6 \gcto z:=z*y; \spc 7 \\
\gcsep \tpc 7 \gcto y:=y-1; \spc 9 \\
\gcsep \tpc 8 \gcto \spc 9 \\
\gcsep \tpc 9 \gcto w:=w+1; \spc 4
\quad \keyw{od}
\end{array}
\]

The normal form of $c5$ is $\spc 1; d5$ where

\[ \graybox{d5:}\quad \keyw{do}
\begin{array}[t]{l}
\tpc 1 \gcto y:=x; \spc 2 \\
\gcsep \tpc 2 \gcto z:=16; \spc 3 \\
\gcsep \tpc 3 \gcto w:=0; \spc 4 \\
\gcsep \tpc 4 \land y\neq 0 \gcto \spc 5 \\
\gcsep \tpc 4 \land y=0 \gcto \spc 0 \\
\gcsep \tpc 5 \land w\mod 3 = 0 \gcto \spc 6 \\
\gcsep \tpc 5 \land w\mod 3 \neq 0 \gcto \spc 8 \\
\gcsep \tpc 6 \gcto z:=z*2; \spc 7 \\
\gcsep \tpc 7 \gcto y:=y-1; \spc 9 \\
\gcsep \tpc 8 \gcto \spc 9 \\
\gcsep \tpc 9 \gcto w:=w+1; \spc 4
\quad \keyw{od}
\end{array}
\]

As an abbreviation, we write $\enab(d4)$ for $\enab$ applied to the body of $d4$,
and likewise for $\enab(d5)$.
The conditions $\enab(d4)$ and $\enab(d5)$ are both equivalent to $1\leq pc\leq 9$.

We aim to instantiate rule rDo by
$\Q:=\Q$, $\Lrel:=\encode{L}$, and $\R:=\encode{R}$.
The side condition of rDo is

\begin{equation}\label{eq:side-c4c5}
\Q \imp (\leftF{\enab(d4)} = \rightF{\enab(d5)})
\lor (\encode{L}\land\leftF{\enab(d4)})
\lor (\encode{R}\land\rightF{\enab(d5)})
\end{equation}

To prove it, distribute in $\Q$ so the antecedent of the side condition has the form

\[ (\S\land\encode{L})\lor(\S\land\encode{R})\lor(\S\land\encode{J})\lor(\S\land\bothF{\tpc 0}) \]

We show each disjunct implies the consequent of the side condition (<ref>).

* $\S\land\encode{L}$ implies $\encode{L}\land\leftF{\enab(d4)}$ using the definition of $\encode{L}$.

* $\S\land\encode{R}$ implies $\encode{R}\land\rightF{\enab(d5)}$ using the definition of $\encode{R}$.

* $\S\land\encode{J}$ implies both $\leftF{\enab(d4)}$ and $\rightF{\enab(d5)}$ are true
so we have $\leftF{\enab(d4)} = \rightF{\enab(d5)}$.

* $\S\land\bothF{\tpc 0}$ implies both $\leftF{\enab(d4)}$ and $\rightF{\enab(d5)}$ are false,
so we have $\leftF{\enab(d4)} = \rightF{\enab(d5)}$.

As for the premises of rDo, note that the normal form bodies in $d4$ and $d5$ each have 11 cases.  So for rDo there are 11 left-only premises, 11 right-only, and 121 joint premises.

Let's do the left-only premises first — selected cases of guarded commands in $d4$.

* for $\tpc 1\gcto y:=x;\spc 2$  we must show

\[ y:=x;\spc 2\sep\skipc : \rspec{\Q\land \leftF{\tpc 1}\land\encode{L}}{\Q} \]

Since $\leftF{\tpc 1}$ contradicts $\encode{L}$, we get the judgment by rConseq and rFalse.

* for $\tpc 4\land y\neq 0\gcto \spc 5$ we must show

\[ \spc 5\sep\skipc : \rspec{\Q\land \leftF{\tpc 4\land y\neq 0}\land\encode{L}}{\Q} \]

By rAsgnSkip we have
\( \spc 5\sep\skipc : \rspec{\subst{\Q}{pc|}{5|}}{\Q} \),
and we complete the proof using rConseq, because
we can prove
$\Q\land \leftF{\tpc 4\land y\neq 0}\land\encode{L} \imp \subst{\Q}{pc|}{5|}$.
To do so, note that $\subst{\Q}{pc|}{5|}$ is equivalent to

\[ (\S\land \subst{\encode{L}}{pc|}{5|})\lor
(\S\land \subst{\encode{R}}{pc|}{5|})\lor
(\S\land \subst{\encode{J}}{pc|}{5|})\lor
(\S\land \subst{\bothF{\tpc 0}}{pc|}{5|}) \]

We show $\S\land \subst{\encode{L}}{pc|}{5|}$ follows from the antecedent
$\Q\land \leftF{\tpc 4\land y\neq 0}\land\encode{L}$.
For $\S$, it is immediate from $\Q$.
Now $\subst{\encode{L}}{pc|}{5|}$ is

\[
(\leftF{5=4}\land\rightF{\tpc 4}\land\leftF{ w\mod 2\neq 0})
\lor (\leftF{5=5}\land\rightF{\tpc 4})
\lor (\leftF{5=8}\land\rightF{\tpc 4})
\lor (\leftF{5=9}\land\rightF{\tpc 4})
\]

And we have that $\leftF{5=5}\land\rightF{\tpc 4}$ follows from
$\Q\land \leftF{\tpc 4}\land\encode{L}$,
because $\encode{L}$ and $\leftF{\tpc 4}$ imply $\rightF{\tpc 4}$.

Turning to the joint premises,
note that the antecedents  include $\lnot\Lrel\land\lnot\R$,
which together with $\encode{L}\lor\encode{R}\lor\encode{J}\lor\bothF{\tpc 0}$ from the invariant
implies $\encode{J}\lor\bothF{\tpc 0}$.

For each $e\gcto c$ in $d4$ and $e'\gcto c'$ in $d5$,
the premise to be established is

\[ c|c':\rspec{ \Q\land\leftF{e}\land\rightF{e'}\land\lnot\encode{L}\land\lnot\encode{R} }
{ \Q }
\]

which by rConseq follows from

\[ c|c':\rspec{ \Q\land\leftF{e}\land\rightF{e'}\land(\encode{J}\lor\bothF{\tpc 0}) }
{ \Q }
\]

which follows by rDisj from

\[ c|c':\rspec{ \Q\land\leftF{e}\land\rightF{e'}\land\bothF{\tpc 0} }
{ \Q }
\]

\begin{equation}\label{eq:c4c5joint}
c|c':\rspec{ \Q\land\leftF{e}\land\rightF{e'}\land\encode{J} }
{ \Q }
\end{equation}

The first of these then follows using rConseq and rFalse because the guards $e$ in $d4$, and $e'$ in $d5$, all contradict $\tpc 0$.
This leaves us with the 121 cases of the form (<ref>).
Many of those cases go by rConseq and rFalse, for example
the case for $\tpc 1 \gcto y:=x; \spc 2$ and $\tpc 2 \gcto z:=16; \spc 3$
has precondition $\leftF{\tpc 1}\land\rightF{\tpc 2}$ for the guards, which contradicts $\encode{J}$.

The remaining cases correspond to the $J$-cases of the VCs in Fig. <ref>.
We consider one case.

* $\tpc 6 \gcto \lassg{}{z}{z*y};\spc 7
\Sep
\tpc 6 \gcto \lassg{}{z}{z*2};\spc 7$.
We must show

\[ \lassg{}{z}{z*y};\spc 7 \Sep \lassg{}{z}{z*2};\spc 7
: \; \rspec{\Q\land\encode{J}\land\bothF{6}}{\Q} \]

We get $\spc 7\sep\spc 7: \rspec{an(7,7)}{an(7,7)\land\bothF{\tpc 7}}$
using rAsgn and rConseq, noting that $an(7,7)$ is independent from $pc$.
By definition of $\Q$ we have
$an(7,7)\land\bothF{\tpc 7} \imp \Q$ so by rConseq we get
$\spc 7\sep\spc 7: \rspec{an(7,7)}{\Q}$.
By rAsgn we get
$\lassg{}{z}{z*y} \sep \lassg{}{z}{z*2}
: \rspec{\subst{an(7,7)}{z|z}{z*y|z*2}}{an(7,7)}$.
By a $pc$-encoded VC we have
$\encode{J}\land\bothF{\tpc 6}\land an(6,6) \imp \subst{an(7,7)}{z|z}{z*y|z*2}$.
So by rConseq we get
$\lassg{}{z}{z*y} \sep \lassg{}{z}{z*2}
: \rspec{\encode{J}\land\bothF{\tpc 6}\land an(6,6)}{an(7,7)}$.
So by rSeq we get
$\lassg{}{z}{z*y};\spc 7 \Sep \lassg{}{z}{z*2};\spc 7
: \; \rspec{\Q\land\encode{J}\land\bothF{6}}{\Q}$.

Once all the premises for rDo are proved, we get its conclusion:
$d4\sep d5: \rspec{\Q}{\Q\land \neg\leftF{\enab(gcs_4)}\land\neg\rightF{\enab(gcs_5)}}$
where $gcs_4$ and $gcs_5$ are the bodies of $d4$ and $d5$.

By steps like those in Sect. <ref>,
we can proceed to get
$\spc 1;d4 \sep \spc 1;d5 : \rspec{x = x'\land x > 3}{z>z'}$
and continue using using rRewrite and rGhost to conclude
the proof of
$ c4 \sep c5 : \rspec{x = x'\land x > 3}{z>z'}$.

§.§ A $\forall\exists$ example: possibilistic noninterference

Consider the example adapted from Unno et al. <cit.>,

\[
\begin{array}{ll@{\;}l}
\graybox{$c1:$}
& \keyw{if}^1 \vhigh \neq 0 \gcto & \lhavc{2}{x}; \\
& & \!\!\!\begin{array}[t]{l}
\keyw{if}^3\ x \geq \vlow \gcto \lskipc{4}
\gcsep\ x < \vlow \gcto \ldogc{4}{\mathit{true}\gcto\lskipc{6}}\ \keyw{fi}
\end{array} \\
& \gcsep \ \ \vhigh = 0 \gcto & \lassg{7}{x}{\vlow};\ \lhavc{8}{b};\ \lskipc{9}; \\
& & \ldogc{10}{b \neq 0 \gcto \lassg{11}{x}{x+1};\ \lhavc{12}{b};\ \lskipc{13}}
\quad\keyw{fi}
%\\ & \keyw{fi}
\end{array}
\]

The program $c1$ satisfies a possibilistic noninterference property expressed
by the judgment

\[c1\sep c1 : \aespec{\leftF{\vlow}=\rightF{\vlow}}{\leftF{x}=\rightF{x}}\]

A proof sketch is provided in Sec. <ref>.  In this section, we
show how the filtered alignment automata for this example is constructed.  In
what follows, we write $x = x'$ to abbreviate $\leftF{x}=\rightF{x}$.
We also abbreviate the test $\vhigh\neq0$ as $h$ and $\vhigh=0$ as $\neg h$.

Product construction

Let $\fin = \fin' = 14$, a label that does not occur in $c1$.  Construct the
filtered alignment product $\aprod(\aut(c1,\fin),\aut(c1,\fin'),L,R,J,K)$ as

\[
\begin{array}{l}
J: \quad \quant{\lor}{i}{i\in\{1\ldots13\}}{[i|i]} \land ([2|2]\imp \bothF{h\sep h})
\land ([7|7]\imp\bothF{\neg h\sep\neg h}) \\
L: \quad \quant{\lor}{i}{i\in\{2\ldots13\}}{[i|1]} \land ([2|1]\imp \bothF{h\sep\neg h})
\land ([7|1]\imp\bothF{\neg h\sep h}) \\
R: \quad \quant{\lor}{i}{i\in\{1\ldots13\}\setminus\{5,6\}}{[\fin|i]} \land
([\fin|2]\imp\bothF{\neg h\sep h}) \land ([\fin|7]\imp\bothF{h\sep\neg h})
\end{array}
\]

The alignment $L, R, J$ capture can be described as follows: if both copies of
$c1$ are to take the same branch of the conditional at label 1, i.e., the
initial states agree on the test $\vhigh\neq 0$, align the executions in
lockstep.  Otherwise, sequentially align.  The left copy of $c1$ is executed
to termination, after which the right copy $c1$ is executed.  Note that $R$
does not include control points $[\fin|5]$ and $[\fin|6]$.  The loop at label
$5$ diverges and so we disallow, through $R$, diverging executions of the
right copy of $c1$.  As we'll see below, the annotation at these points will
be $\mathit{false}$. We define $K$ as follows,

\[
\begin{array}{ll@{\;}l}
K: \quad & & ([3|3]\imp x=x') \land ([9|9]\imp b = b') \land ([13|13]\imp b = b') \\
& \land & ([\fin|3] \imp x=x') \\
& \land & ([\fin|9] \imp x-x'=b') \land ([\fin|13]\imp x-x'=b')
\end{array}
\]

In this example $K$ only constrains choices made by $\lhavc{}{x}$ and
$\lhavc{}{b}$ on the right.  The first line in the definition handles joint
executions.  It ensures that the right execution makes the same choices as the
left does when nondeterministically assigning a value to $x$ and $b$.  The
second line handles the case when the left execution takes the $\vhigh = 0$
branch and the right takes the $\vhigh\neq0$ branch.
The third line handles the case when the left execution takes the $\vhigh\neq0$ branch and
the right takes the $\vhigh=0$ branch.  In this situation the right copy of
$c1$ executes
$\ldogc{10}{b\neq 0\gcto \lassg{11}{x}{x+1};\ \lhavc{12}{b};\ \lskipc{13}}$.
The annotation, defined below, asserts $x-x'=b'$ is an invariant of this loop
and $K$ ensures that nondeterminacy is resolved in a way that will preserve
this invariant.

We define the annotation $an$ of
$\prod(\aut(c1,\fin),\aut(c1,\fin'),L,R,J,K)$ as follows,

\[
\begin{array}{lll}
an(1,1) & = (\vlow = \vlow') \\
an(\fin,\fin') & = (x = x') \\[.5em]
an(2,2) & = (\vlow = \vlow') \\
an(i,i) & = (x = x') & \mbox{for $i \in \{ 3,4,5,6,7,8 \}$ } \\
an(i,i) & = (b = b' \land x = x') & \mbox{for $i \in \{ 9,10,11,12,13 \}$} \\[.5em]
an(i,1) & = (\vlow = \vlow') & \mbox{for $i \in \{2,3,7\}$} \\
an(i,1) & = (\vlow = \vlow' \land x \geq low) & \mbox{for $i \in \{4,5,6,8,9,10,11,12,13,\fin\}$} \\[.5em]
an(\fin,2) & = (\vlow = \vlow' \land x \geq low) \\
an(\fin,i) & = (\vlow = \vlow' \land x \geq low \land x = x') & \mbox{for $i \in \{3,4\}$} \\
an(\fin,5) & = \mathit{false} \\
an(\fin,6) & = \mathit{false} \\
an(\fin,7) & = (\vlow = \vlow' \land x \geq low) \\
an(\fin,8) & = (x \geq low \land x' \geq \vlow') \\
an(\fin,i) & = (x \geq low \land b' = x-x') & \mbox{for $i\in\{9,10,11,13\}$} \\
an(\fin,12) & = (x \geq low \land b' = x-x'+1) \\[.5em]
an(i,j) & = \mathit{false} & \mbox{for all other $i,j$}
\end{array}
\]

We have that
$\hat{an}(i,j) \imp K(i,j) \land (L \lor R \lor J \lor [\fin|\fin'])$ for all
control points of the product $(i,j)$.  Checking this is tedious and we omit
details.  The annotation $an$ is also valid: each of the corresponding VCs
hold.  Hence, the filtered product satisfies the spec
$\spec{\vlow = \vlow'}{x = x'}$.

As an example, consider the corresponding VC for control points
$(\fin,12)$ and $(\fin,13)$, the step that performs nothing on the left and
$\lhavc{12}{b}$ on the right.  We must show (see the right-only VC for havoc in
Fig. <ref>),

\[
\all{v'\in\Z}{\breve{an}(\fin,12) \land R \land \subst{K(\fin,13)}{|b'}{|v'}
\imp \subst{\hat{an}(\fin,13)}{|b'}{|v'}}
\]

We reason as follows.  For any $v' \in \Z$,

\(\begin{array}{lll}
& \breve{an}(\fin,12) \land R \land \subst{K(\fin,13)}{|b'}{|v'} \\
\imp & x \geq \vlow \land b' = x-x' + 1 \land \subst{(x-x' = b')}{|b'}{|v'}
& \hint{by def and weakening} \\
\iff & x \geq \vlow  \land b' = x-x' + 1 \land v' = x-x'
& \hint{substitution} \\
\imp & x \geq \vlow \land v' = x-x'
& \hint{weaken} \\
\imp & x \geq \vlow \land \subst{(b' = x-x')}{|b'}{|v'}
& \hint{substition} \\
\iff & \subst{\hat{an}(\fin,13)}{|b'}{|v'}
& \hint{by def}
\end{array}\)

Validity of all the other VCs is straightforward to prove.

Adequate filtering

We now show that $K$ as defined above is an adequate filtering as in
Def. <ref>.  We must prove that $K$ is left-permissive
and right- and joint-productive with respect to $an$.  For right productivity,
we also need to define a variant function $V$ of type
$(\labs(c1)\union\{\fin\} \times (\Var\to\Z))\to D$ where $(D,\prec)$ is some
well-founded set.

We start by defining an ordering $\cprec$ on control points as follows

\[
\fin' \cprec 12 \cprec 11 \cprec 10 \cprec 13 \cprec 9 \cprec 8 \cprec 7 \cprec 4 \cprec 3 \cprec 2 \cprec 1
\]

Let $D$ be the set of lexically ordered triples of type
$(\{0,1\}, \mathsf{Nat}, \labs(c1)\union\{\fin'\})$, where the last component
is ordered by $\cprec$.  We now define
$V (n',s') \eqdef (\ifc{n'\geq 9}{0}{1}, |s'(b')|, n')$.

The variant is defined this way to account for the following: each right-only
step progresses along the control flow graph, thereby decreasing the third
component with respect to $(\cprec)$ as the ordering.  The order on control
points is defined in a way such that even the step from control point
$(\fin,13)$ to $(\fin,10)$, i.e., when jumping to the head of the loop at
label 10, decreases the variant.  The only step that does not decrease the
third component of the variant is the step from $(\fin,12)$ to $(\fin,13)$
which havocs $b$.  However, $K$ filters executions in a way to ensure that the
value of $b$ is decremented by this step, thus decreasing the second component
of the variant.  There is one issue, however.  The right-only step from
$(\fin,8)$ to $(\fin,9)$ which havocs $b$ does not necessarily decrease the
value of $b$.  Instead, it decreases the first component of the variant.

Now we show that $K$ is an adequate filtering.  Condition (a) of
Def. <ref>, left-permissivity of $K$, follows from $K$
not constraining any of the control points in $L$, thus
$K(m,n) = \mathit{true}$ for any $(m,n) \in L$.

Showing condition (c) of Def. <ref>, joint-productivity
of $K$, is also straightforward.  The three constraints $K$ adds on control
points in $J$ are $K(3,3) = (x = x')$ and $K(9,9) = (b = b')$ and
$K(13,13) = (b = b')$.  Consider the step from control point $(2,2)$ to
$(3,3)$.  We must show,

\[
\hat{an}(2,2) \land J \imp \PRE(\biTranSeg{(2,2),(3,2)})(\EPRE(\biTranSeg{(3,2),(3,3)})(K(3,3)))
\]

Unfolding definitions, this amounts to proving that for chosen value of $x$,
there exists a value of $x'$ such that $x = x'$; this holds.  The other cases
are similar.

Finally, for condition (b) of Def. <ref>,
right-productivity of $K$, we detail a proof of the step from $(\fin,12)$ to
$(\fin,13)$, which performs $\lhavc{12}{b}$ on the right.  We must show

\[
\hat{an}(\fin,12)\land R \imp \EPRE(\biTranSeg{(\fin,12),(\fin,13)})(K(\fin,13) \land \rightF{V(13)\prec V(12)})
\]

Note that this is the only step where the control component of the variant
does not decrease.  Unfolding $\EPRE$, we must show
$\some{v'\in\Z}{\subst{K(\fin,13)}{|b'}{|v'} \land
\rightF{\subst{V(13)}{|b'}{|v'} \prec V(12)}}$.  By the definition of $K$
this is equivalent to
$\some{v'\in\Z}{v' = x-x' \land \rightF{\subst{V(13)}{|b'}{|v'} \prec
V(12)}}$, so by instantiating $v' := x-x'$, it suffices to prove
$\rightF{\subst{V(13)}{|b'}{|x-x'} \prec V(12)}$.  Now, by $an(\fin,12)$ we
have $b' = x-x'+1$.  We show the second component of the variant decreases.
By definition, we have $\subst{V(13)}{|b'}{|x-x'} = (0, |x-x'|, 13)$.
Clearly, this is below $V(12) = (0, |b'|, 12)$ since
$|b'| = |x-x'+1| > |x-x'|$.

Validity of the annotation defined above leads to an IAM style proof of the
possibilistic noninterference step.  We've constructed a filtered product and
have shown that the filter $K$ is adequate in the sense of
Def. <ref>.  Thus, the assumptions of the alignment
completeness theorem for ERHL+, Theorem. <ref>, are met by
$\aprod(\aut(c1,\fin),\aut(c1,\fin'),L,R,J,K)$.  Appealing to the theorem, we
obtain a deductive proof of the judgment
$c1 \sep c1 : \aespec{\leftF{low}=\rightF{low}}{\leftF{x}=\rightF{x}}$ in


# Impact of Nap on Performance in Different Working Memory Tasks Using EEG
111††thanks: This work was supported by the Institute of Information &
Communications Technology Planning & Evaluation (IITP) grant, funded by the
Korea government (MSIT) (No. 2019-0-00079, Artificial Intelligence Graduate
School Program (Korea University)) and was partly supported by the Institute
of Information & communications Technology Planning & Evaluation (IITP) grant,
funded by the Korea government (MSIT) (No. 2021-0-02068, Artificial
Intelligence Innovation Hub).

Gi-Hwan Shin  Dept. of Brain and Cognitive Engineering
Korea University
Seoul, Republic of Korea
<EMAIL_ADDRESS>Young-Seok Kweon  Heon-Gyu Kwak  Dept. of Brain and
Cognitive Engineering
Korea University
Seoul, Republic of Korea
<EMAIL_ADDRESS>Dept. of Artificial Intelligence
Korea University
Seoul, Republic of Korea
<EMAIL_ADDRESS>Ha-Na Jo  Dept. of Artificial Intelligence
Korea University
Seoul, Republic of Korea
<EMAIL_ADDRESS>Seong-Whan Lee  Dept. of Artificial Intelligence
Korea University
Seoul, Republic of Korea
<EMAIL_ADDRESS>
###### Abstract

Electroencephalography (EEG) has been widely used to study the relationship
between naps and working memory, yet the effects of naps on distinct working
memory tasks remain unclear. Here, participants performed word-pair and
visuospatial working memory tasks pre- and post-nap sessions. We found marked
differences in accuracy and reaction time between tasks performed pre- and
post-nap. In order to identify the impact of naps on performance in each
working memory task, we employed clustering to classify participants as high-
or low-performers. Analysis of sleep architecture revealed significant
variations in sleep onset latency and rapid eye movement (REM) proportion. In
addition, the two groups exhibited prominent differences, especially in the
delta power of the Non-REM 3 stage linked to memory. Our results emphasize the
interplay between nap-related neural activity and working memory, underlining
specific EEG markers associated with cognitive performance.

Keywords–working memory, nap, electroencephalogram;

##  I INTRODUCTION

Sleep, a complex neurophysiological process integral to cognitive functioning,
is divided into rapid-eye movement (REM) and non-REM (NREM) sleep, with the
NREM sleep further subdivided into NREM 1 (N1), NREM 2 (N2), and NREM 3 (N3)
stages [1, 2]. The N3 stage is particularly crucial for memory consolidation
[3]. Additionally, the concept of sleep architecture, which includes factors
like total sleep time (TST), sleep onset latency (SOL), wake after sleep onset
(WASO), sleep efficiency (SE), and the relative proportions of N1, N2, N3, and
REM stages, is intricately linked to memory processes [4]. Yet, the
differential impacts of these sleep characteristics on various memory tasks
remain to be fully explored.

Many studies have focused on working memory, a crucial element for complex
cognitive tasks such as reasoning and learning [5, 6]. Using
electroencephalography (EEG), known for its high temporal resolution, has been
instrumental in revealing the intricate working memory processes [7, 8]. The
advantage of EEG in capturing rapid neural activity related to cognition is
particularly evident in spectrogram analysis [9]. This method offers
comprehensive insights into oscillatory brain activity across various
frequency bands, including delta (1-4 Hz), theta (4-8 Hz), alpha (8-13 Hz),
beta (13-25 Hz), and gamma (25-50 Hz), which enhances our understanding of the
neural oscillations associated with different components of working memory
[10, 11]. However, the specific effects of different sleep stages on distinct
working memory tasks remain less understood, marking an area ripe for further
investigation.

In this study, we aimed to identify the effects of a nap on word-pair and
visuospatial working memory tasks. We hypothesized that the impact of the nap
could vary across these tasks, particularly expecting pronounced effects
across various stages of sleep. To investigate this, we grouped participants
using a clustering method based on their performance in working memory tasks,
considering factors like accuracy and reaction time. Our analysis began with a
comparison of sleep architecture between the groups to discern any differences
in sleep patterns and their potential effects on memory tasks. Subsequently,
we conducted spectrogram-based EEG analyses to examine neural activity during
the naps, aiming to correlate these patterns with working memory performance.

Figure 1: Performance of distinct working memory tasks in pre- and post-nap
sessions. For (a), accuracy rate is shown, and for (b), reaction time is
displayed. Black asterisks indicate statistical significance at p$<$0.05.

##  II METHODS

###  II-A Participants and Experimental Setup

Thirty-five participants (14 females, age: 25.4 ± 2.3 years) were recruited
after providing written informed consent. None had neurological or psychiatric
disorders. Following the procedure outlined by Shin et al. [12], participants
underwent three sessions: pre-nap, a 90-minute nap, and post-nap. During the
pre- and post-nap sessions, they completed two working memory tasks: a word-
pairs task [13] and a visuospatial task involving picture and location memory
[14]. The tasks were developed using Psychtoolbox (http://psychtoolbox.org)
[15]. The study received approval from the Institutional Review Board at Korea
University (KUIRB-2021-0155-03).

###  II-B Data Recording and Preprocessing

Data were recorded from 60 EEG and 4 electrooculography (EOG) channels using
64 electrodes and the BrainAmp system (Brain Products GmbH, Germany).
Electrodes were positioned according to the 10-20 system for EEG and placed
near the eyes for EOG. The data were sampled at 1,000 Hz with FCz and Fpz as
the reference and ground. All electrode impedances were maintained below 20
k$\Omega$.

EEG signals were preprocessed using EEGLAB [16] and BCILAB toolboxes [17] for
MATLAB 2018b. Signals were down-sampled to 250 Hz and band-pass filtered
between 1 and 50 Hz [18]. Eye movement artifacts were corrected using
independent component analysis with the EOG signals. A Laplacian spatial
filter was applied to improve the signal-to-noise ratio [19].

Sleep experts labeled the data into five sleep stages (wake, N1, N2, N3, and
REM) using 30-second epochs, following American Academy of Sleep Medicine
standards [20].

###  II-C Data Analysis

####  II-C1 Cognitive performance analysis

To identify the impact of nap on various working memory, participants
undertook tasks pre- and post-nap sessions, with their performance measured in
terms of accuracy and reaction time. Using a clustering method, we divided
participants into high-performers and low-performers for each working memory
task, based on these performance metrics. This approach aimed to highlight
variations in nap effects linked to proficiency in each task.

TABLE I: Sleep Architecture of High- and Low-Performers Based on Performance in Distinct Working Memory Tasks (Mean $\pm$ SD). | Word-pair memory | Picture memory | Location memory
---|---|---|---
| HP | LP |  p-value | HP | LP |  p-value | HP | LP |  p-value
TST (min) | 70.29 $\pm$ 0.75 | 79.64 $\pm$ 1.16 | 0.098 | 77.56 $\pm$ 0.76 | 72.81 $\pm$ 0.71 | 0.461 | 70.10 $\pm$ 0.90 | 79.27 $\pm$ 0.85 | 0.101
SOL (min) | 5.60 $\pm$ 0.14 | 3.21 $\pm$ 0.25 | 0.035 | 5.06 $\pm$ 0.30 | 4.50 $\pm$ 0.14 | 0.671 | 5.15 $\pm$ 0.17 | 3.97 $\pm$ 0.21 | 0.303
WASO (min) | 14.62 $\pm$ 0.69 | 7.64 $\pm$ 1.00 | 0.166 | 7.89 $\pm$ 0.60 | 13.19 $\pm$ 0.63 | 0.351 | 15.25 $\pm$ 0.79 | 7.27 $\pm$ 0.75 | 0.108
SE (%) | 78.10 $\pm$ 0.83 | 88.49 $\pm$ 1.29 | 0.098 | 86.17 $\pm$ 0.85 | 80.90 $\pm$ 0.79 | 0.461 | 77.89 $\pm$ 1.00 | 88.07 $\pm$ 0.94 | 0.101
N1 (% of TST) | 29.95 $\pm$ 0.86 | 25.08 $\pm$ 1.50 | 0.468 | 23.13 $\pm$ 1.13 | 29.69 $\pm$ 0.82 | 0.383 | 30.85 $\pm$ 1.04 | 24.20 $\pm$ 1.10 | 0.316
N2 (% of TST) | 50.61 $\pm$ 0.79 | 58.38 $\pm$ 1.18 | 0.182 | 56.02 $\pm$ 1.40 | 52.93 $\pm$ 0.69 | 0.640 | 50.29 $\pm$ 0.91 | 58.30 $\pm$ 0.91 | 0.164
N3 (% of TST) | 15.92 $\pm$ 0.94 | 10.36 $\pm$ 1.00 | 0.370 | 13.23 $\pm$ 1.59 | 13.86 $\pm$ 0.73 | 0.928 | 16.70 $\pm$ 0.99 | 9.70 $\pm$ 0.95 | 0.253
R (% of TST) | 3.51 $\pm$ 0.32 | 6.18 $\pm$ 0.66 | 0.326 | 7.63 $\pm$ 0.85 | 3.52 $\pm$ 0.29 | 0.175 | 2.16 $\pm$ 0.25 | 7.80 $\pm$ 0.65 | 0.031
Figure 2: Statistical maps illustrating the relative increase and decrease in
spectrogram between high- and low-performers during nap session. For (a) word-
pair memory, (b) picture memory, and (c) location memory, the channels
corresponding to the Regions of Interest (ROIs) were averaged for each of the
five sleep stages, highlighting the frequency differences within the range of
1-50 Hz. The black-bordered regions indicate significant frequencies and ROIs
(p$<$0.05).

####  II-C2 EEG analysis

EEG data were analyzed via spectrograms to capture the neural oscillatory
patterns prevalent across different sleep stages in nap sessions. The analysis
encompassed a frequency range of 1 to 50 Hz. Time-domain signals were
converted into frequency-domain representations, employing a 99 % window
overlap to ensure high temporal resolution [21]. This methodology was
instrumental in identifying dominant frequencies and elucidating their
distribution patterns throughout the various sleep stages. Furthermore, we
categorized the EEG channels into five key regions: frontal, central,
temporal, parietal, and occipital, to investigate a region-specific analysis
of oscillatory patterns [22].

###  II-D Statistical Analysis

To compare the changes in working memory accuracy and reaction time for pre-
nap and post-nap sessions, a paired t-test was applied. In addition, a two-
sample t-test was used to assess the nap’s impact on high- and low-performer
groups by separately analyzing their sleep architecture and EEG data. For all
these statistical evaluations, a significance threshold was set at p$<$0.05.

##  III RESULTS

###  III-A Influence of Nap on Working Memory Performance

We conducted a comparative analysis of performance in distinct working memory
tasks during pre- and post-nap sessions, as depicted in Fig. 1. In accuracy,
there was a significant improvement post-nap in both word-pair and picture
memory tasks, while the location memory task showed a notable decrease. In
reaction time, a significant reduction was observed across all working memory
tasks in the post-nap session.

###  III-B Variations in Sleep Architecture Across Memory Tasks

To elucidate the impact of napping on distinct working memory tasks, we
conducted a statistical analysis of sleep architecture between high- and low-
performers, as detailed in Table<EMAIL_ADDRESS>In the word-pair memory task, high-
performers statistically exhibited a longer SOL compared to low-performers.
Conversely, in the location memory task, low-performers showed a significantly
higher proportion of REM sleep. For the picture memory task, no significant
statistical differences in sleep architecture were observed between the two
groups.

###  III-C EEG Analysis During Nap and Memory Task Performance

In our EEG analysis, as depicted in Fig. 2, we observed varied patterns across
memory tasks and performer groups during the nap. In the word-pair memory
task, low-performers exhibited higher delta power in the parietal region and
increased gamma power in all brain regions during the wake stage, with higher
gamma power in the central region during the REM stage. In contrast, high-
performers demonstrated elevated powers in various frequency bands, excluding
the gamma band, in different brain regions during the REM stage, and higher
powers in delta, theta, and alpha bands during the N1, N2, and N3 stages. For
the picture memory task, the REM stage showed notable differences, with low-
performers exhibiting increased gamma power in the central region, whereas
high-performers had higher powers in other low-frequency bands. In the
location memory task, high-performers displayed elevated theta power in the
central region during the N1 and N2 stages and higher delta and theta powers
across all brain regions in the N3 stage.

##  IV DISCUSSION

In the current study, our research investigated the impact of napping on
distinct working memory tasks using EEG. We observed significant differences
in accuracy and reaction time between pre- and post-nap sessions in
participants. Based on these results, we categorized participants into high-
and low-performer groups and identified significant variations in SOL and the
proportion of REM. Furthermore, an EEG comparison of the two groups across
different working memory tasks revealed distinct variations in neural patterns
across a variety of frequency bands and brain regions. These results highlight
the complex interplay between sleep, neural activity, and working memory
performance, indicating that nap can differentially affect cognitive
processing in diverse brain regions.

This study conducted statistical comparisons to unravel the impacts of nap on
different cognitive performances. The observed improvement in accuracy for
word-pair and picture memory tasks in post-nap sessions suggests the benefits
of nap in memory consolidation [23]. However, the decrease in location memory
observed in post-nap sessions suggests a contrasting effect, indicative of
memory loss or interference [24]. Additionally, we observed a significant
reduction in reaction time across all working memory tasks in post-nap
sessions, highlighting the restorative effects of nap on overall alertness
[25, 26]. These findings emphasize that naps significantly influence the
performance of various working memory tasks.

Our analysis reveals group differences in sleep architecture and its impact on
various working memory tasks. High performers in the word-pair memory task
showed a longer SOL, suggesting a complex interplay between sleep dynamics and
verbal memory processing, though this doesn’t necessarily imply more effective
memory consolidation [27]. Conversely, in the location memory task, the higher
proportion of REM sleep in low-performers questions its role in location
memory consolidation, indicating that increased REM sleep doesn’t uniformly
enhance performance [28]. In the picture memory task, the absence of
significant sleep differences between high- and low-performers points to the
influence of factors beyond sleep architecture, like individual cognitive
strategies or inherent memory abilities [29]. Collectively, these findings
highlight the intricate relationship between sleep architecture and working
memory and suggest that understanding the impact of sleep stages on memory
could aid in addressing cognitive decline [30].

The EEG analysis in our study uncovered distinct neural activity patterns
associated with napping’s effects on various working memory tasks, revealing a
complex interplay among sleep stages, brain activity, and cognitive
performance. In the word-pair memory task, low-performers showed higher delta
power in the parietal region during the wake stage and increased gamma power
in the central region during REM sleep, indicating intense neural processing.
High-performers, however, demonstrated increased delta, theta, and alpha
powers in deeper sleep stages, particularly in the delta band of the N3 stage,
which is closely associated with memory processes. This pattern suggests a
critical role of N3 in memory consolidation [31]. In the picture memory task,
differences in the REM stage were noted, with low-performers showing increased
gamma power in the central region, while high-performers exhibited higher
powers in low-frequency bands [32]. The location memory task showed that high-
performers had elevated theta power in the central region during N1 and N2
stages and higher delta and theta powers in N3 stage across all brain regions
[12]. These findings highlight napping’s impact on different working memory.

The study’s limitation is the non-randomized order of working memory tasks,
potentially affecting the results. Future research plans to implement a
randomized sequence and apply machine learning to better understand how sleep
stages influence cognitive performance, aiming to tailor cognitive enhancement
to individuals [33, 34]. Insights from such studies have the potential to
inform strategies not only for cognitive enhancement but also for addressing
memory deficits associated with dementia.

##  V CONCLUSION

Our research provides insights into how nap affects performance across various
working memory tasks. The observed differences across performance groups
highlight the potential role of nap in cognitive function. The EEG data,
particularly from the NREM stage, reveal distinct neural patterns associated
with various working memory tasks. These EEG characteristics suggest the
neural mechanisms involved in memory processing during sleep. These findings
lay a foundation for future studies, enriching our understanding of the
interplay between sleep and cognitive functions.

## References

  * [1] A. Eban-Rothschild, L. Appelbaum, and L. de Lecea, “Neuronal mechanisms for sleep/wake regulation and modulatory drive,” _Neuropsychopharmacology_ , vol. 43, no. 5, pp. 937–952, 2018.
  * [2] V. Brodbeck _et al._ , “EEG microstates of wakefulness and NREM sleep,” _Neuroimage_ , vol. 62, no. 3, pp. 2129–2139, 2012.
  * [3] H. Zhang, J. Fell, and N. Axmacher, “Electrophysiological mechanisms of human memory consolidation,” _Nat. Commun._ , vol. 9, no. 1, p. 4103, 2018.
  * [4] S. E. Alger, H. Lau, and W. Fishbein, “Delayed onset of a daytime nap facilitates retention of declarative memory,” _PLoS One_ , vol. 5, no. 8, p. e12131, 2010.
  * [5] G.-H. Shin, Y.-S. Kweon, and M. Lee, “Predicting the transition from short-term to long-term memory based on deep neural network,” in _Int. Winter Conf. Brain-Computer Interface (BCI)_ , 2021, pp. 1–5.
  * [6] S. A. Small _et al._ , “Circuit mechanisms underlying memory encoding and retrieval in the long axis of the hippocampal formation,” _Nat. Neurosci._ , vol. 4, no. 4, pp. 442–449, 2001.
  * [7] R. Mane _et al._ , “FBCNet: A multi–view convolutional neural network for brain–computer interface,” _arXiv:2104.01233_ , 2021.
  * [8] J. Kim _et al._ , “Abstract representations of associated emotions in the human brain,” _J. Neurosci._ , vol. 35, no. 14, pp. 5655–5663, 2015.
  * [9] G.-H. Shin, Y.-S. Kweon, and H.-G. Kwak, “Changes in power and information flow in resting-state EEG by working memory process,” in _Int. Winter Conf. Brain-Computer Interface (BCI)_ , 2023, pp. 1–5.
  * [10] F. Ferrarelli _et al._ , “An increase in sleep slow waves predicts better working memory performance in healthy individuals,” _Neuroimage_ , vol. 191, pp. 1–9, 2019.
  * [11] L. Genzel, M. C. Kroes, M. Dresler, and F. P. Battaglia, “Light sleep versus slow wave sleep in memory consolidation: A question of global versus local processes?” _Trends Neurosci._ , vol. 37, no. 1, pp. 10–19, 2014.
  * [12] G.-H. Shin, M. Lee, and S.-W. Lee, “Assessment of unconsciousness for memory consolidation using EEG signals,” in _Conf. Proc. IEEE. Int. Conf. Syst. Man Cybern. (SMC)_ , 2020, pp. 513–519.
  * [13] M. M. Leminen _et al._ , “Enhanced memory consolidation via automatic sound stimulation during non-REM sleep,” _Sleep_ , vol. 40, no. 3, p. zsx003, 2017.
  * [14] J. Ladenbauer _et al._ , “Brain stimulation during an afternoon nap boosts slow oscillatory activity and memory consolidation in older adults,” _Neuroimage_ , vol. 142, pp. 311–323, 2016.
  * [15] S.-H. Lee, M. Lee, and S.-W. Lee, “Neural decoding of imagined speech and visual imagery as intuitive paradigms for BCI communication,” _IEEE Trans. Neural Syst. Rehabil. Eng._ , vol. 28, no. 12, pp. 2647–2659, 2020.
  * [16] A. Delorme and S. Makeig, “EEGLAB: An open source toolbox for analysis of single-trial EEG dynamics including independent component analysis,” _J. Neurosci. Methods_ , vol. 134, no. 1, pp. 9–21, 2004.
  * [17] C. A. Kothe and S. Makeig, “BCILAB: A platform for brain-computer interface development,” _J. Neural Eng._ , vol. 10, no. 5, p. 056014, 2013.
  * [18] S.-H. Lee, M. Lee, J.-H. Jeong, and S.-W. Lee, “Towards an EEG–based intuitive BCI communication system using imagined speech and visual imagery,” in _Conf. Proc. IEEE Int. Conf. Syst. Man Cybern. (SMC)_ , 2019, pp. 4409–4414.
  * [19] H.-I. Suk, S. Fazli, J. Mehnert, K.-R. Müller, “Predicting BCI subject performance using probabilistic spatio–temporal filters,” _PLoS One_ , vol. 9, no. 2, p. e87056, 2014.
  * [20] M. H. Silber _et al._ , “The visual scoring of sleep in adults,” _J. Clin. Sleep Med._ , vol. 3, no. 02, pp. 121–131, 2007.
  * [21] S.-B. Lee _et al._ , “Comparative analysis of features extracted from EEG spatial, spectral and temporal domains for binary and multiclass motor imagery classification,” _Inf. Sci._ , vol. 502, pp. 190–200, 2019.
  * [22] M. Lee, C.-B. Song, G.-H. Shin, and S.-W. Lee, “Possible effect of binaural beat combined with autonomous sensory meridian response for inducing sleep,” _Front. Hum. Neurosci._ , vol. 13, pp. 425–440, 2019.
  * [23] M. P. Walker and R. Stickgold, “Sleep-dependent learning and memory consolidation,” _Neuron_ , vol. 44, no. 1, pp. 121–133, 2004.
  * [24] C. Álvarez-Bueno _et al._ , “Napping and cognitive decline: A systematic review and meta-analysis of observational studies,” _BMC Geriatr._ , vol. 22, no. 1, pp. 1–8, 2022.
  * [25] C. E. Milner and K. A. Cote, “Benefits of napping in healthy adults: Impact of nap length, time of day, age, and experience with napping,” _J. Sleep Res._ , vol. 18, no. 2, pp. 272–281, 2009.
  * [26] B. Rasch and J. Born, “About sleep’s role in memory,” _Physiol. Rev._ , 2013.
  * [27] J. Zhang, L. N. Whitehurst, and S. C. Mednick, “The role of sleep for episodic memory consolidation: Stabilizing or rescuing?” _Neurobiol. Learn. Mem._ , vol. 191, p. 107621, 2022.
  * [28] A. Tilley and J. Empson, “REM sleep and memory consolidation,” _Biol. Psychol._ , vol. 6, no. 4, pp. 293–300, 1978.
  * [29] S. Diekelmann and J. Born, “The memory function of sleep,” _Nat. Rev. Neurosci._ , vol. 11, no. 2, pp. 114–126, 2010.
  * [30] K.-H. Thung _et al._ , “Conversion and time–to–conversion predictions of mild cognitive impairment using low–rank affinity pursuit denoising and matrix completion,” _Med. Image Anal._ , vol. 45, pp. 68–82, 2018.
  * [31] J. Holz _et al._ , “EEG sigma and slow-wave activity during NREM sleep correlate with overnight declarative and procedural memory consolidation,” _J. Sleep Res._ , vol. 21, no. 6, pp. 612–619, 2012.
  * [32] S. Vijayan, K. Q. Lepage, N. J. Kopell, and S. S. Cash, “Frontal beta-theta network during REM sleep,” _eLife_ , vol. 6, p. e18894, 2017.
  * [33] K.-T. Kim, C. Guan, and S.-W. Lee, “A subject–transfer framework based on single–trial EMG analysis using convolutional neural networks,” _IEEE Trans. Neural Syst. Rehabil. Eng._ , vol. 28, no. 1, pp. 94–103, 2019.
  * [34] J.-S. Bang, M.-H. Lee, S. Fazli, C. Guan, and S.-W. Lee, “Spatio–spectral feature representation for motor imagery classification using convolutional neural networks,” _IEEE Trans. Neural. Netw. Learn. Syst._ , vol. 33, no. 7, pp. 3038–3049, 2021.