283
edits
Pipe-calculus: Difference between revisions
→Normal forms
KalmanKeri (talk | contribs) |
KalmanKeri (talk | contribs) |
||
| Line 262: | Line 262: | ||
<math> | <math> | ||
\def\seq{\mathrel{;}} | \def\seq{\mathrel{;}} | ||
\def\alt{\mid} | \def\alt{\mid} | ||
\def\pipe{\rhd} | \def\pipe{\rhd} | ||
\def\in{\,?} | \def\in{\,?} | ||
| Line 274: | Line 272: | ||
(s \seq t) \seq u \rew & s \seq (t \seq u) \\ | (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 \\ | ||
\ | \top \seq s \rew & s \\ | ||
\ | \bot \seq s \rew & \bot \\ | ||
\\ | \\ | ||
(s \alt t) \alt u \rew & s \alt (t \alt u) \\ | (s \alt t) \alt u \rew & s \alt (t \alt u) \\ | ||
a^+ . s \alt a^+ \seq t \rew & a^+ . (s \alt t) \\ | a^+ . s \alt a^+ \seq t \rew & a^+ . (s \alt t) \\ | ||
a^- . s \alt a^- \seq t \rew & a^- . (s \alt t) \\ | a^- . s \alt a^- \seq t \rew & a^- . (s \alt t) \\ | ||
\ | \bot \alt s \rew & s \\ | ||
s \alt \ | s \alt \bot \rew & s \\ | ||
\ | \top \alt s \rew & \top \\ | ||
s \alt \ | s \alt \top \rew & \top \\ | ||
\end{alignat} | \end{alignat} | ||
</math> | </math> | ||
| Line 300: | Line 298: | ||
s \alt t \pipe u \rew & (s \pipe u) \alt (t \pipe u) \\ | s \alt t \pipe u \rew & (s \pipe u) \alt (t \pipe u) \\ | ||
s \pipe t \alt u \rew & (s \pipe t) \alt (s \pipe u) \\ | s \pipe t \alt u \rew & (s \pipe t) \alt (s \pipe u) \\ | ||
\ | \bot \pipe t \rew & t \\ | ||
s \pipe \ | s \pipe \top \rew & \top \\ | ||
s \pipe t \rew & \ | s \pipe t \rew & \bot & \\ | ||
\end{alignat} | \end{alignat} | ||
</math> | </math> | ||