equal
deleted
inserted
replaced
63 Thus we can automatically prove results such as this one:% |
63 Thus we can automatically prove results such as this one:% |
64 \end{isamarkuptext}% |
64 \end{isamarkuptext}% |
65 \isamarkuptrue% |
65 \isamarkuptrue% |
66 \isacommand{theorem}\ {\isachardoublequote}qs{\isacharbrackleft}{\isadigit{2}}{\isacharcomma}{\isadigit{3}}{\isacharcomma}{\isadigit{0}}{\isacharbrackright}\ {\isacharequal}\ qs{\isacharbrackleft}{\isadigit{3}}{\isacharcomma}{\isadigit{0}}{\isacharcomma}{\isadigit{2}}{\isacharbrackright}{\isachardoublequote}\isanewline |
66 \isacommand{theorem}\ {\isachardoublequote}qs{\isacharbrackleft}{\isadigit{2}}{\isacharcomma}{\isadigit{3}}{\isacharcomma}{\isadigit{0}}{\isacharbrackright}\ {\isacharequal}\ qs{\isacharbrackleft}{\isadigit{3}}{\isacharcomma}{\isadigit{0}}{\isacharcomma}{\isadigit{2}}{\isacharbrackright}{\isachardoublequote}\isanewline |
67 \isamarkupfalse% |
67 \isamarkupfalse% |
68 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline |
|
69 \isamarkupfalse% |
68 \isamarkupfalse% |
70 \isacommand{done}\isamarkupfalse% |
69 \isamarkupfalse% |
71 % |
70 % |
72 \begin{isamarkuptext}% |
71 \begin{isamarkuptext}% |
73 \noindent |
72 \noindent |
74 More exciting theorems require induction, which is discussed below. |
73 More exciting theorems require induction, which is discussed below. |
75 |
74 |