equal
deleted
inserted
replaced
92 these lemmas:% |
92 these lemmas:% |
93 \end{isamarkuptext}% |
93 \end{isamarkuptext}% |
94 \isamarkuptrue% |
94 \isamarkuptrue% |
95 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}gcd\ {\isacharparenleft}m{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ m{\isachardoublequote}\isanewline |
95 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}gcd\ {\isacharparenleft}m{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ m{\isachardoublequote}\isanewline |
96 \isamarkupfalse% |
96 \isamarkupfalse% |
97 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline |
|
98 \isamarkupfalse% |
97 \isamarkupfalse% |
99 \isacommand{done}\isanewline |
98 \isanewline |
100 \isanewline |
99 \isanewline |
101 \isamarkupfalse% |
100 \isamarkupfalse% |
102 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ gcd{\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ gcd{\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isachardoublequote}\isanewline |
101 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ gcd{\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ gcd{\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isachardoublequote}\isanewline |
103 \isamarkupfalse% |
102 \isamarkupfalse% |
104 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline |
|
105 \isamarkupfalse% |
103 \isamarkupfalse% |
106 \isacommand{done}\isamarkupfalse% |
104 \isamarkupfalse% |
107 % |
105 % |
108 \begin{isamarkuptext}% |
106 \begin{isamarkuptext}% |
109 \noindent |
107 \noindent |
110 Simplification terminates for these proofs because the condition of the \isa{if} simplifies to \isa{True} or \isa{False}. |
108 Simplification terminates for these proofs because the condition of the \isa{if} simplifies to \isa{True} or \isa{False}. |
111 Now we can disable the original simplification rule:% |
109 Now we can disable the original simplification rule:% |