equal
deleted
inserted
replaced
1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{CTLind}% |
3 \def\isabellecontext{CTLind}% |
|
4 \isamarkupfalse% |
4 % |
5 % |
5 \isadelimtheory |
6 \isadelimtheory |
6 % |
7 % |
7 \endisadelimtheory |
8 \endisadelimtheory |
8 % |
9 % |
9 \isatagtheory |
10 \isatagtheory |
10 \isamarkupfalse% |
|
11 % |
11 % |
12 \endisatagtheory |
12 \endisatagtheory |
13 {\isafoldtheory}% |
13 {\isafoldtheory}% |
14 % |
14 % |
15 \isadelimtheory |
15 \isadelimtheory |
135 \isacommand{apply}\isamarkupfalse% |
135 \isacommand{apply}\isamarkupfalse% |
136 {\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequoteopen}wf{\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}{\isachardoublequoteclose}{\isacharparenright}\isanewline |
136 {\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequoteopen}wf{\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}{\isachardoublequoteclose}{\isacharparenright}\isanewline |
137 \ \isacommand{apply}\isamarkupfalse% |
137 \ \isacommand{apply}\isamarkupfalse% |
138 {\isacharparenleft}erule{\isacharunderscore}tac\ a\ {\isacharequal}\ t\ \isakeyword{in}\ wf{\isacharunderscore}induct{\isacharparenright}\isanewline |
138 {\isacharparenleft}erule{\isacharunderscore}tac\ a\ {\isacharequal}\ t\ \isakeyword{in}\ wf{\isacharunderscore}induct{\isacharparenright}\isanewline |
139 \ \isacommand{apply}\isamarkupfalse% |
139 \ \isacommand{apply}\isamarkupfalse% |
140 {\isacharparenleft}clarsimp{\isacharparenright}\isamarkupfalse% |
140 {\isacharparenleft}clarsimp{\isacharparenright}% |
141 % |
|
142 \begin{isamarkuptxt}% |
141 \begin{isamarkuptxt}% |
143 \noindent |
142 \noindent |
144 \begin{isabelle}% |
143 \begin{isabelle}% |
145 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ {\isasymlbrakk}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharsemicolon}\isanewline |
144 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ {\isasymlbrakk}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharsemicolon}\isanewline |
146 \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ }{\isasymforall}y{\isachardot}\ {\isacharparenleft}t{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymnotin}\ A\ {\isasymlongrightarrow}\isanewline |
145 \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ }{\isasymforall}y{\isachardot}\ {\isacharparenleft}t{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymnotin}\ A\ {\isasymlongrightarrow}\isanewline |
237 \isadelimtheory |
236 \isadelimtheory |
238 % |
237 % |
239 \endisadelimtheory |
238 \endisadelimtheory |
240 % |
239 % |
241 \isatagtheory |
240 \isatagtheory |
242 \isamarkupfalse% |
|
243 % |
241 % |
244 \endisatagtheory |
242 \endisatagtheory |
245 {\isafoldtheory}% |
243 {\isafoldtheory}% |
246 % |
244 % |
247 \isadelimtheory |
245 \isadelimtheory |