equal
deleted
inserted
replaced
104 \ \isadigit{1}{\isachardot}\ {\isasymAnd}s{\isachardot}\ s\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A |
104 \ \isadigit{1}{\isachardot}\ {\isasymAnd}s{\isachardot}\ s\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A |
105 \end{isabelle} |
105 \end{isabelle} |
106 which is proved by @{term lfp}-induction: |
106 which is proved by @{term lfp}-induction: |
107 *} |
107 *} |
108 |
108 |
109 apply(erule Lfp.induct) |
109 apply(erule lfp_induct) |
110 apply(rule mono_ef) |
110 apply(rule mono_ef) |
111 apply(simp) |
111 apply(simp) |
112 (*pr(latex xsymbols symbols);*) |
112 (*pr(latex xsymbols symbols);*) |
113 txt{*\noindent |
113 txt{*\noindent |
114 Having disposed of the monotonicity subgoal, |
114 Having disposed of the monotonicity subgoal, |