equal
deleted
inserted
replaced
139 \noindent |
139 \noindent |
140 In contrast to the analogous proof for \isa{EF}, and just |
140 In contrast to the analogous proof for \isa{EF}, and just |
141 for a change, we do not use fixed point induction. Park-induction, |
141 for a change, we do not use fixed point induction. Park-induction, |
142 named after David Park, is weaker but sufficient for this proof: |
142 named after David Park, is weaker but sufficient for this proof: |
143 \begin{center} |
143 \begin{center} |
144 \isa{f\ S\ {\isasymle}\ S\ {\isasymLongrightarrow}\ lfp\ f\ {\isasymle}\ S} \hfill (\isa{lfp{\isacharunderscore}lowerbound}) |
144 \isa{f\ S\ {\isasymsubseteq}\ S\ {\isasymLongrightarrow}\ lfp\ f\ {\isasymsubseteq}\ S} \hfill (\isa{lfp{\isacharunderscore}lowerbound}) |
145 \end{center} |
145 \end{center} |
146 The instance of the premise \isa{f\ S\ {\isasymle}\ S} is proved pointwise, |
146 The instance of the premise \isa{f\ S\ {\isasymsubseteq}\ S} is proved pointwise, |
147 a decision that \isa{auto} takes for us:% |
147 a decision that \isa{auto} takes for us:% |
148 \end{isamarkuptxt}% |
148 \end{isamarkuptxt}% |
149 \isamarkuptrue% |
149 \isamarkuptrue% |
150 \isacommand{apply}\isamarkupfalse% |
150 \isacommand{apply}\isamarkupfalse% |
151 {\isacharparenleft}rule\ lfp{\isacharunderscore}lowerbound{\isacharparenright}\isanewline |
151 {\isacharparenleft}rule\ lfp{\isacharunderscore}lowerbound{\isacharparenright}\isanewline |