283
edits
Pipe-calculus: Difference between revisions
→Equational theory
KalmanKeri (talk | contribs) |
KalmanKeri (talk | contribs) |
||
| Line 199: | Line 199: | ||
\def\fail{\textbf{fail}} | \def\fail{\textbf{fail}} | ||
\def\pipe{\rhd} | \def\pipe{\rhd} | ||
\def\eq{ = ~} | \def\eq{ = ~} | ||
</math>Sequential composition is associative with left neutral element <math>\succeed</math> and left absorbing element <math>\fail</math>. | </math>Sequential composition is associative with left neutral element <math>\succeed</math> and left absorbing element <math>\fail</math>. | ||
| Line 206: | Line 205: | ||
\begin{align} | \begin{align} | ||
(s \seq t) \seq u \eq & s \seq (t \seq u) \\ | (s \seq t) \seq u \eq & s \seq (t \seq u) \\ | ||
\succeed \seq | \succeed \seq t \eq & t \\ | ||
\fail \seq | \fail \seq t \eq & \fail \\ | ||
\end{align} | \end{align} | ||
</math> | </math> | ||
| Line 218: | Line 217: | ||
s \alt t \eq & t \alt s \\ | s \alt t \eq & t \alt s \\ | ||
s \alt s \eq & s \\ | s \alt s \eq & s \\ | ||
\succeed \alt | \succeed \alt t \eq & \succeed \\ | ||
\fail \alt | \fail \alt t \eq & t \\ | ||
\end{align} | \end{align} | ||
</math> | </math> | ||
| Line 231: | Line 230: | ||
</math> | </math> | ||
Pipe | Pipe has left neutral element <math>\fail</math> and right absorbing element <math>\succeed</math>. | ||
<math> | <math> | ||
\begin{align} | \begin{align} | ||
\fail \pipe t \eq & t \\ | |||
s \pipe \ | s \pipe \succeed \eq & \succeed \\ | ||
\end{align} | \end{align} | ||
</math> | </math> | ||