\procedure{$\O{Run5}(\n{state}, \n{tau})$}{
\pcparse \n{state} \pcas \left(\begin{array}{c}\n{U}, \n{u}, \n{V}, \n{ltk}, \n{acc}, \n{k}, \n{ni}, \pclb\n{nr}, \n{kmac}, \n{sid}, \n{mess}\end{array}\right)\\
\pcassert \n{u} = \lit{false} \\
\pcassert \n{acc} = \bot \\
\pcassert \n{mess} = 2 \\
\pcif \O{\n{mac}}(\n{kmac}, \n{zeron}, 4) = \n{tau} \pcthen\\
\pcind \pcreturn \left(\begin{array}{c}\pclb\left(\begin{array}{c}\n{U}, \n{u}, \n{V}, \n{ltk}, \lit{true}, \n{k}, \pclb\n{ni}, \n{nr}, \n{kmac}, \n{sid}, 3\end{array}\right), \pclb\left(\begin{array}{c}\lit{true}\end{array}\right)\end{array}\right)\\
\pcelse\\
\pcind \pcreturn \left(\begin{array}{c}\n{state}, \pclb\left(\begin{array}{c}\lit{false}\end{array}\right)\end{array}\right)\\
}
