\procedure{$\O{Send3}(\n{ctr}, \n{msg})$}{
\pcassert (\n{State}[\n{ctr}] \neq \bot) \\
 \n{state} \gets \n{State}[\n{ctr}]\\
\n{return} \stackrel{\mathsf{\tiny{invoke}}}{\gets} \O{Run3}(\n{state}, \n{msg}) \pccomment{Pkg: Prot} \\
\pcparse \n{return} \pcas \left(\begin{array}{c}\n{state}, \n{msg}_\n{}\end{array}\right)\\
 \n{State}[\n{ctr}] \gets \n{state}\\
 \pcreturn \n{msg}_\n{}\\
}
