equal
deleted
inserted
replaced
119 The \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}} modifier of the \isa{rule{\isacharunderscore}format} directive means |
119 The \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}} modifier of the \isa{rule{\isacharunderscore}format} directive means |
120 that the assumption is left unchanged---otherwise the \isa{{\isasymforall}p} is turned |
120 that the assumption is left unchanged---otherwise the \isa{{\isasymforall}p} is turned |
121 into a \isa{{\isasymAnd}p}, which would complicate matters below. As it is, |
121 into a \isa{{\isasymAnd}p}, which would complicate matters below. As it is, |
122 \isa{Avoid{\isacharunderscore}in{\isacharunderscore}lfp} is now |
122 \isa{Avoid{\isacharunderscore}in{\isacharunderscore}lfp} is now |
123 \begin{isabelle}% |
123 \begin{isabelle}% |
124 \ \ \ \ \ {\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ Avoid\ s\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}% |
124 \ \ \ \ \ {\isasymlbrakk}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharsemicolon}\ t\ {\isasymin}\ Avoid\ s\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}% |
125 \end{isabelle} |
125 \end{isabelle} |
126 The main theorem is simply the corollary where \isa{t\ {\isacharequal}\ s}, |
126 The main theorem is simply the corollary where \isa{t\ {\isacharequal}\ s}, |
127 in which case the assumption \isa{t\ {\isasymin}\ Avoid\ s\ A} is trivially true |
127 in which case the assumption \isa{t\ {\isasymin}\ Avoid\ s\ A} is trivially true |
128 by the first \isa{Avoid}-rule). Isabelle confirms this:% |
128 by the first \isa{Avoid}-rule). Isabelle confirms this:% |
129 \end{isamarkuptext}% |
129 \end{isamarkuptext}% |