vault backup: 2025-04-14 17:40:00
This commit is contained in:
parent
5f6df56152
commit
322de74d50
1 changed files with 10 additions and 5 deletions
|
@ -159,14 +159,19 @@ What if we restrict on b?
|
||||||
|
|
||||||

|

|
||||||
|
|
||||||
|
##### Example 1:
|
||||||
|
as $a$ is not in $\{b, \bar{b}\}$, we will see the transitions:
|
||||||
|
$$
|
||||||
|
\frac{\frac{\frac{a.A' \xrightarrow{a} A' \quad A \triangleq a.A'}{A \xrightarrow{a} A'}}
|
||||||
|
{{A \mid B \xrightarrow{a} A' \mid B}}a \not \in \{b, \bar{b}\}}{{(A \mid B) \setminus b \xrightarrow{a} (A' \mid B) \setminus b}}
|
||||||
|
$$
|
||||||
|
|
||||||
|
Split in separate peaces for improved readability:
|
||||||
$$\frac{a.A' \xrightarrow{a} A' \quad A \triangleq a.A'}{A \xrightarrow{a} A'}
|
$$\frac{a.A' \xrightarrow{a} A' \quad A \triangleq a.A'}{A \xrightarrow{a} A'}
|
||||||
\quad
|
\quad
|
||||||
\frac{A \xrightarrow{a} A'}{A \mid B \xrightarrow{a} A' \mid B}
|
\frac{A \xrightarrow{a} A'}{A \mid B \xrightarrow{a} A' \mid B}
|
||||||
\quad
|
\quad
|
||||||
\frac{A \mid B \xrightarrow{a} A' \mid B \quad a \notin \{b, \bar{b}\}}{(A \mid B) \setminus b \xrightarrow{a} (A' \mid B) \setminus b}$$
|
\frac{A \mid B \xrightarrow{a} A' \mid B \quad a \notin \{b, \bar{b}\}}{(A \mid B) \setminus b \xrightarrow{a} (A' \mid B) \setminus b}$$
|
||||||
$$
|
|
||||||
|
|
||||||
|
##### Example 2:
|
||||||
|
as $b$ is in
|
||||||
|
|
||||||
$$
|
|
Loading…
Add table
Add a link
Reference in a new issue