equal
deleted
inserted
replaced
57 \isamarkupfalse% |
57 \isamarkupfalse% |
58 % |
58 % |
59 \begin{isamarkuptext}% |
59 \begin{isamarkuptext}% |
60 \noindent |
60 \noindent |
61 This time everything works fine. Now \isa{f{\isachardot}simps} contains precisely |
61 This time everything works fine. Now \isa{f{\isachardot}simps} contains precisely |
62 the stated recursion equation for \isa{{\isacharquery}{\isacharquery}{\isachardot}f}, which has been stored as a |
62 the stated recursion equation for \isa{f}, which has been turned into a |
63 simplification rule. Thus we can automatically prove results such as this one:% |
63 simplification rule. Thus we can automatically prove results such as this one:% |
64 \end{isamarkuptext}% |
64 \end{isamarkuptext}% |
65 \isamarkuptrue% |
65 \isamarkuptrue% |
66 \isacommand{theorem}\ {\isachardoublequote}f{\isacharparenleft}{\isadigit{1}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ f{\isacharparenleft}{\isadigit{1}}{\isacharcomma}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline |
66 \isacommand{theorem}\ {\isachardoublequote}f{\isacharparenleft}{\isadigit{1}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ f{\isacharparenleft}{\isadigit{1}}{\isacharcomma}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline |
67 \isamarkupfalse% |
67 \isamarkupfalse% |