\newcommand{\reds}[0]{\stackrel{*}{\Longrightarrow}}
\newcommand{\red}[0]{\Longrightarrow}