equal
deleted
inserted
replaced
298 \end{isabelle} |
298 \end{isabelle} |
299 Note that \isa{EU} is not definable in terms of the other operators! |
299 Note that \isa{EU} is not definable in terms of the other operators! |
300 |
300 |
301 Model checking \isa{EU} is again a least fixed point construction: |
301 Model checking \isa{EU} is again a least fixed point construction: |
302 \begin{isabelle}% |
302 \begin{isabelle}% |
303 \ \ \ \ \ mc{\isacharparenleft}EU\ f\ g{\isacharparenright}\ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ g\ {\isasymunion}\ mc\ f\ {\isasyminter}\ {\isacharparenleft}M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isacharparenright}% |
303 \ \ \ \ \ mc{\isacharparenleft}EU\ f\ g{\isacharparenright}\ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ g\ {\isasymunion}\ mc\ f\ {\isasyminter}\ {\isacharparenleft}M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isacharparenright}% |
304 \end{isabelle} |
304 \end{isabelle} |
305 |
305 |
306 \begin{exercise} |
306 \begin{exercise} |
307 Extend the datatype of formulae by the above until operator |
307 Extend the datatype of formulae by the above until operator |
308 and prove the equivalence between semantics and model checking, i.e.\ that |
308 and prove the equivalence between semantics and model checking, i.e.\ that |