Skip to content
Snippets Groups Projects
Commit 08bfb781 authored by Eric Giovannini's avatar Eric Giovannini
Browse files

small changes in adequacy proof

parent 44f3ca04
No related branches found
No related tags found
No related merge requests found
......@@ -657,11 +657,11 @@ Then weak bisimilarity is defined by the rules
{\tnow\, x_? \bisimdelay \tnow\, y_? }
\inferrule*[]
{d_1 \Da x_? \and x_? \bisim_{X + 1} y'_?}
{\tlater\, d_1 \bisimdelay \tnow\, y'_? }
{d_1 \Da x_? \and x_? \bisim_{X + 1} y_?}
{\tlater\, d_1 \bisimdelay \tnow\, y_? }
\inferrule*[]
{d_2 \Da y_? \and x_? \bisim_{X + 1} y'_?}
{d_2 \Da y_? \and x_? \bisim_{X + 1} y_?}
{\tnow\, x_? \bisimdelay \tlater\, d_2}
\inferrule*[]
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment