equal
deleted
inserted
replaced
101 conclusion, but not \isa{y}. Thus our induction statement is too |
101 conclusion, but not \isa{y}. Thus our induction statement is too |
102 weak. Fortunately, it can easily be strengthened: |
102 weak. Fortunately, it can easily be strengthened: |
103 transfer the additional premise \isa{{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}} into the conclusion:% |
103 transfer the additional premise \isa{{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}} into the conclusion:% |
104 \end{isamarkuptxt}% |
104 \end{isamarkuptxt}% |
105 \isamarkuptrue% |
105 \isamarkuptrue% |
106 \isanewline |
|
107 \isamarkupfalse% |
106 \isamarkupfalse% |
108 \isacommand{lemma}\ rtc{\isacharunderscore}trans{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline |
107 \isacommand{lemma}\ rtc{\isacharunderscore}trans{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline |
109 \ \ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isamarkupfalse% |
108 \ \ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isamarkupfalse% |
110 % |
109 % |
111 \begin{isamarkuptxt}% |
110 \begin{isamarkuptxt}% |
209 \isamarkupfalse% |
208 \isamarkupfalse% |
210 \isamarkupfalse% |
209 \isamarkupfalse% |
211 \isamarkupfalse% |
210 \isamarkupfalse% |
212 \isamarkupfalse% |
211 \isamarkupfalse% |
213 \isamarkupfalse% |
212 \isamarkupfalse% |
214 \isanewline |
|
215 \isamarkupfalse% |
213 \isamarkupfalse% |
216 \end{isabellebody}% |
214 \end{isabellebody}% |
217 %%% Local Variables: |
215 %%% Local Variables: |
218 %%% mode: latex |
216 %%% mode: latex |
219 %%% TeX-master: "root" |
217 %%% TeX-master: "root" |