equal
deleted
inserted
replaced
96 \ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}% |
96 \ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}% |
97 \begin{isamarkuptxt}% |
97 \begin{isamarkuptxt}% |
98 \noindent |
98 \noindent |
99 Simplification leaves us with the following first subgoal |
99 Simplification leaves us with the following first subgoal |
100 \begin{isabelle}% |
100 \begin{isabelle}% |
101 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A% |
101 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}s{\isachardot}\ s\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A% |
102 \end{isabelle} |
102 \end{isabelle} |
103 which is proved by \isa{lfp}-induction:% |
103 which is proved by \isa{lfp}-induction:% |
104 \end{isamarkuptxt}% |
104 \end{isamarkuptxt}% |
105 \ \isacommand{apply}{\isacharparenleft}erule\ lfp{\isacharunderscore}induct{\isacharparenright}\isanewline |
105 \ \isacommand{apply}{\isacharparenleft}erule\ lfp{\isacharunderscore}induct{\isacharparenright}\isanewline |
106 \ \ \isacommand{apply}{\isacharparenleft}rule\ mono{\isacharunderscore}ef{\isacharparenright}\isanewline |
106 \ \ \isacommand{apply}{\isacharparenleft}rule\ mono{\isacharunderscore}ef{\isacharparenright}\isanewline |