283
edits
Pipe-calculus: Difference between revisions
→Normal form
KalmanKeri (talk | contribs) |
KalmanKeri (talk | contribs) |
||
| Line 204: | Line 204: | ||
\def\eq{ = ~} | \def\eq{ = ~} | ||
\def\rule{ ::= ~} | \def\rule{ ::= ~} | ||
\def\rew{\Rightarrow} | \def\rew{\Rightarrow~} | ||
</math> | </math> | ||
<math> | <math> | ||
\begin{alignat}{1} | \begin{alignat}{1} | ||
(s \seq t) \seq u \rew & s \seq | (s \seq t) \seq u \rew & s \seq t \seq u \\ | ||
(s \alt t) \seq u \rew & s \seq u \alt t \seq u \\ | (s \alt t) \seq u \rew & s \seq u \alt t \seq u \\ | ||
\succeed \seq s \rew & s \\ | \succeed \seq s \rew & s \\ | ||
\fail \seq s \rew & \fail \\ | \fail \seq s \rew & \fail \\ | ||
\\ | |||
(s \alt t) \alt u \rew & s \alt t \alt u \\ | |||
s \alt s \rew & s \\ | |||
\neg a \alt \neg a \rew & \neg a \\ | |||
\pos a \seq s \alt \pos a \seq t \rew & \pos a \seq (s \alt t) \\ | |||
\neg a \seq s \alt \neg a \seq t \rew & \neg a \seq (s \alt t) \\ | |||
\fail \alt s \rew & s \\ | |||
s \alt \fail \rew & s \\ | |||
\succeed \alt s \rew & \succeed \\ | |||
s \alt \succeed \rew & \succeed \\ | |||
\end{alignat} | \end{alignat} | ||
</math> | </math> | ||