1.1 --- a/doc-src/TutorialI/CTL/document/PDL.tex	Mon Oct 09 09:33:45 2000 +0200
     1.2 +++ b/doc-src/TutorialI/CTL/document/PDL.tex	Mon Oct 09 10:18:21 2000 +0200
     1.3 @@ -173,7 +173,24 @@
     1.4  \isacommand{theorem}\ {\isachardoublequote}mc\ f\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ f{\isacharbraceright}{\isachardoublequote}\isanewline
     1.5  \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline
     1.6  \isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}EF{\isacharunderscore}lemma{\isacharparenright}\isanewline
     1.7 -\isacommand{done}\end{isabellebody}%
     1.8 +\isacommand{done}%
     1.9 +\begin{isamarkuptext}%
    1.10 +\begin{exercise}
    1.11 +\isa{AX} has a dual operator \isa{EN}\footnote{We cannot use the customary \isa{EX}
    1.12 +as that is the ASCII equivalent of \isa{{\isasymexists}}}
    1.13 +(``there exists a next state such that'') with the intended semantics
    1.14 +\begin{isabelle}%
    1.15 +\ \ \ \ \ s\ {\isasymTurnstile}\ EN\ f\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymTurnstile}\ f{\isacharparenright}%
    1.16 +\end{isabelle}
    1.17 +Fortunately, \isa{EN\ f} can already be expressed as a PDL formula. How?
    1.18 +
    1.19 +Show that the semantics for \isa{EF} satisfies the following recursion equation:
    1.20 +\begin{isabelle}%
    1.21 +\ \ \ \ \ s\ {\isasymTurnstile}\ EF\ f\ {\isacharequal}\ {\isacharparenleft}s\ {\isasymTurnstile}\ f\ {\isasymor}\ s\ {\isasymTurnstile}\ EN\ {\isacharparenleft}EF\ f{\isacharparenright}{\isacharparenright}%
    1.22 +\end{isabelle}
    1.23 +\end{exercise}%
    1.24 +\end{isamarkuptext}%
    1.25 +\end{isabellebody}%
    1.26  %%% Local Variables:
    1.27  %%% mode: latex
    1.28  %%% TeX-master: "root"