From 6d44c638512eb736c41551c5887b4475a14935bf Mon Sep 17 00:00:00 2001 From: Norbert Preining Date: Thu, 15 Sep 2022 03:15:34 +0000 Subject: CTAN sync 202209150315 --- .../contrib/stex/doc/packages/stex-proofs.tex | 425 +++++++++++++++------ 1 file changed, 299 insertions(+), 126 deletions(-) (limited to 'macros/latex/contrib/stex/doc/packages/stex-proofs.tex') diff --git a/macros/latex/contrib/stex/doc/packages/stex-proofs.tex b/macros/latex/contrib/stex/doc/packages/stex-proofs.tex index d06db1282f..9e6e44f5ca 100644 --- a/macros/latex/contrib/stex/doc/packages/stex-proofs.tex +++ b/macros/latex/contrib/stex/doc/packages/stex-proofs.tex @@ -1,100 +1,308 @@ +\begin{sfragment}{Proofs} + The \pkg{stex-proof} package supplies macros and environment that allow to annotate the structure of mathematical proofs in \sTeX document. This structure can be used by MKM systems for added-value services, either directly from the \sTeX sources, or after translation. -We will go over the general intuition by way of a running example: +Its central component is the |sproof|-environment, whose body consists +of: +\begin{itemize} + \item \emph{subproofs} via the |subproof|-environment, + \item \emph{proof steps} via the |\spfstep|, |\eqstep| + |\assumption|, and |\conclude| macros, and + \item \emph{comments}, via normal text without special markup. +\end{itemize} + +|sproof|, |subproof| and the various proof step macros take the following +optional arguments: +\begin{itemize} + \item[|id|] (\meta{string}) for referencing, + \item[|method|] (\meta{string}) the proof method (e.g. contradiction, induction,...) + \item[|term|] (\meta{token list}) the (ideally semantically-marked up) + proposition that is derived/proven by this proof/subproof/proof step. +\end{itemize} +Additionally, they take one mandatory argument for the document text +to be annotated, or (in the case of the environments) +as an introductory description of the proof itself. Since +the latter often contains the |term| to be derived +as text, alternatively to providing it as +an optional argument, the mandatory argument can use the +|\yield|-macro to mark it up in the text. + +The |sproof| and |subproof| environments additionally take +two optional arguments: +\begin{itemize} + \item[|for|] the symbol identifier/name corresponding to the |sassertion| + to be proven. This too subsumes |\yield| and the |term|-argument. + \item[|hide|] In the pdf, this only shows the mandatory argument text + and hides the body of the environment. In the HTML (as served by \mmt), + the bodies of all |proof| and |subproof| environments are \emph{collapsible}, + and |hide| collapses the body by default. +\end{itemize} + +\begin{smodule}{sproofs} + \symdef{coprime}[args=2]{#1 \comp\bot #2} + \symdef{realroot}[args=1]{\sqrt{#1}} + \symdecl{irrational}[args=1] + \symdecl{rational}[args=1] + \symdef{eq}[args=2]{#1 \comp= #2} + \symdef{ratfrac}[args=2,prec=1]{\frac{#1}{#2}} + \symdef{intpow}[args=2,prec=-1]{{#1}^{#2}} + \symdef{ratpow}[args=2]{{#1}^{#2}} + \symdef{inset}[args=ai]{#1\comp\in#2}{##1\comp,##2} + \symdef{Int}{\comp{\mathbb Z}} + \symdef{PosInt}{\comp{{\mathbb Z}^+}} + \symdef{inttimes}[args=2]{#1 #2} + \symdef{divides}[args=2]{#1\comp\|#2} + + \vardef{vara}{\comp a} + \vardef{varb}{\comp b} + \vardef{varc}{\comp c} + + \def\contradiction{} \begin{latexcode} -\begin{sproof}[id=simple-proof] + \begin{sassertion}[type=theorem,name=sqrt2irr] + \conclusion{\irrational{$\arg{\realroot{2}}$ is \comp{irrational}}}. +\end{sassertion} + +\begin{sproof}[for=sqrt2irr,method=contradiction]{By contradiction} + \assumption{Assume \yield{\rational{$\arg{\realroot{2}}$ is + \comp{rational}}}} + \begin{subproof}[method=straightforward]{Then + \yield{$\eq{\ratfrac{\intpow{\vara}{2}}{\intpow{\varb}2}}{2}$ + for some $\inset{\vara,\varb}\PosInt$ with + \coprime{$\arg{\vara},\arg{\varb}$ \comp{coprime}}}} + \assumption{By assumption, \yield{there are + $\inset{\vara,\varb}\PosInt $ with + $\realroot{2}=\ratfrac{\vara}{\varb}$}} + \spfstep{wlog, we can assume \coprime{$\arg{\vara},\arg{\varb}$ + to be \comp{coprime}}} + % a comment: + If not, reduce the fraction until numerator and denominator + are coprime, and let the resulting components be + $\vara $ and $\varb $ + \spfstep{Then \yield{$\eq{\intpow{\ratfrac{\vara}{\varb}}2}2$}} + \eqstep{\ratfrac{\intpow{\vara}2}{\intpow{\varb}2}} + \end{subproof} + \begin{subproof}[term=\divides{2}{\vara},method=straightforward]{ + Then $\vara $ is even} + \spfstep{Multiplying the equation by $\intpow{\varb}2$ yields + $\yield{\eq{\intpow{\vara}2}{\inttimes{2}{\intpow{\varb}2}}}$} + \spfstep[term=\divides{2}{\intpow{\vara}2}]{Hence + $\intpow{\vara}2$ is even} + \conclude[term=\divides{2}{\vara}]{Hence $\vara $ is even as well} + % another comment: + Hint: Think about the prime factorizations of $\vara $ and + $\intpow{\vara}2$ + \end{subproof} + \begin{subproof}[term=\divides{2}{\varb},method=straightforward,]{ + Then $\varb $ is also even} + \spfstep{Since $\vara $ is even, we have \yield{some $\varc $ + such that $\eq{\inttimes{2}{\varc}}{\vara}$}} + \spfstep{Plugging into the above, we get + \yield{$\eq{\intpow{\inttimes{2}{\vara}}2} + {\inttimes{2}{\intpow{\varb}2}}$}} + \eqstep{\inttimes{4}{\intpow{\vara}2}} + \spfstep{Dividing both sides by $2$ yields + \yield{$\eq{\intpow{\varb}2}{\inttimes{2}{\intpow{\vara}2}}$}} + \spfstep[term=\divides{2}{\intpow{\varb}2}]{Hence + $\intpow{\varb}2$ is even} + \conclude[term=\divides{2}{\varb}]{Hence $\varb $ is even} + % one more comment: + By the same argument as above + \end{subproof} + \conclude[term=\contradiction]{Contradiction to $\vara,\varb $ being + \symname{coprime}.} +\end{sproof} +\end{latexcode} + +which will produce: + +\begin{mdframed} +\begin{sassertion}[type=theorem,name=sqrt2irr] + \conclusion{\irrational{$\arg{\realroot2}$ is \comp{irrational}}}. +\end{sassertion} + +\begin{sproof}[for=sqrt2irr,method=contradiction]{By contradiction} + \assumption{Assume \yield{\rational{$\arg{\realroot2}$ is \comp{rational}}}} + \begin{subproof}[method=straightforward]% + {Then \yield{$\eq{\ratfrac{\intpow \vara2}{\intpow \varb2}}{2}$ for some $\inset{\vara,\varb}\PosInt$ with \coprime{$\arg \vara,\arg \varb$ \comp{coprime}}}} + \assumption{By assumption, \yield{there are $\inset{\vara,\varb}\PosInt$ with $\realroot2=\ratfrac\vara\varb$}} + \spfstep{wlog, we can assume \coprime{$\arg{\vara},\arg{\varb}$ to be \comp{coprime}}} + If not, reduce the fraction until numerator and denominator are + coprime, and let the resulting components be $\vara$ and $\varb$ + \spfstep{Then \yield{$\eq{\intpow{\ratfrac\vara\varb}2}2$}} + \eqstep{\ratfrac{\intpow\vara2}{\intpow\varb2}} + \end{subproof} + \begin{subproof}[term=\divides{2}{\vara},method=straightforward]{Then $\vara$ is even} + \spfstep{Multiplying the equation by $\intpow\varb2$ yields $\yield{\eq{\intpow\vara2}{\inttimes2{\intpow\varb2}}}$} + \spfstep[term=\divides{2}{\intpow\vara2}]{Hence $\intpow\vara2$ is even} + \conclude[term=\divides{2}{\vara}]{Hence $\vara$ is even as well} + Hint: Think about the prime factorizations of $\vara$ and $\intpow\vara2$ + \end{subproof} + \begin{subproof}[term=\divides{2}{\varb},method=straightforward]{Then $\varb$ is also even} + \spfstep{Since $\vara$ is even, we have \yield{some $\varc$ such that $\eq{\inttimes2\varc}{\vara}$}} + \spfstep{Plugging into the above, we get \yield{$\eq{\intpow{\inttimes2\vara}2}{\inttimes2{\intpow\varb2}}$}} + \eqstep{\inttimes4{\intpow\vara2}} + \spfstep{Dividing both sides by $2$ yields \yield{$\eq{\intpow\varb2}{\inttimes2{\intpow\vara2}}$}} + \spfstep[term=\divides{2}{\intpow\varb2}]{Hence $\intpow\varb2$ is even} + \conclude[term=\divides{2}{\varb}]{Hence $\varb$ is even} + By the same argument as above + \end{subproof} + \conclude[term=\contradiction]{Contradiction to $\vara,\varb$ being \symname{coprime}.} +\end{sproof} +\end{mdframed} + +If we mark all subproofs with |hide|, we will obtain the following +instead: + +\begin{mdframed} + \begin{sassertion}[type=theorem,name=sqrt2irr] + \conclusion{\irrational{$\arg{\realroot2}$ is \comp{irrational}}}. + \end{sassertion} + + \begin{sproof}[for=sqrt2irr,method=contradiction]{By contradiction} + \assumption{Assume \yield{\rational{$\arg{\realroot2}$ is \comp{rational}}}} + \begin{subproof}[hide,method=straightforward]% + {Then \yield{$\eq{\ratfrac{\intpow \vara2}{\intpow \varb2}}{2}$ for some $\inset{\vara,\varb}\PosInt$ with \coprime{$\arg \vara,\arg \varb$ \comp{coprime}}}} + \assumption{By assumption, \yield{there are $\inset{\vara,\varb}\PosInt$ with $\realroot2=\ratfrac\vara\varb$}} + \spfstep{wlog, we can assume \coprime{$\arg{\vara},\arg{\varb}$ to be \comp{coprime}}} + If not, reduce the fraction until numerator and denominator are + coprime, and let the resulting components be $\vara$ and $\varb$ + \spfstep{Then \yield{$\eq{\intpow{\ratfrac\vara\varb}2}2$}} + \eqstep{\ratfrac{\intpow\vara2}{\intpow\varb2}} + \end{subproof} + \begin{subproof}[hide,term=\divides{2}{\vara},method=straightforward]{Then $\vara$ is even} + \spfstep{Multiplying the equation by $\intpow\varb2$ yields $\yield{\eq{\intpow\vara2}{\inttimes2{\intpow\varb2}}}$} + \spfstep[term=\divides{2}{\intpow\vara2}]{Hence $\intpow\vara2$ is even} + \conclude[term=\divides{2}{\vara}]{Hence $\vara$ is even as well} + Hint: Think about the prime factorizations of $\vara$ and $\intpow\vara2$ + \end{subproof} + \begin{subproof}[hide,term=\divides{2}{\varb},method=straightforward,]{Then $\varb$ is also even} + \spfstep{Since $\vara$ is even, we have \yield{some $\varc$ such that $\eq{\inttimes2\varc}{\vara}$}} + \spfstep{Plugging into the above, we get \yield{$\eq{\intpow{\inttimes2\vara}2}{\inttimes2{\intpow\varb2}}$}} + \eqstep{\inttimes4{\intpow\vara2}} + \spfstep{Dividing both sides by $2$ yields \yield{$\eq{\intpow\varb2}{\inttimes2{\intpow\vara2}}$}} + \spfstep[term=\divides{2}{\intpow\varb2}]{Hence $\intpow\varb2$ is even} + \conclude[term=\divides{2}{\varb}]{Hence $\varb$ is even} + By the same argument as above + \end{subproof} + \conclude[term=\contradiction]{Contradiction to $\vara,\varb$ being \symname{coprime}.} + \end{sproof} + \end{mdframed} + + However, the hidden subproofs will still be shown in the HTML, + only in an expandable section which is collapsed by default. + + +The above style of writing proofs is usually called \emph{structured proofs}. +They have a huge advantage over the traditional purely prosaic style, +in that (as the name suggests) the actual \emph{structure} of the proof +is made explicit, which almost always makes it considerably more +comprehensible. We, among many others, encourage the general use of +structured proofs. + +Alas, most proofs are not written in this style, and we would +do users a disservice by insisting on this style. For that reason, +the |spfblock| environment turns all subproofs and proof step +macros into presentationally neutral \emph{inline} annotations, +as in the induction step of the following example: + +\begin{latexcode} +\begin{sproof}[id=simple-proof,method=induction] {We prove that $\sum_{i=1}^n{2i-1}=n^{2}$ by induction over $n$} - \begin{spfcases}{For the induction we have to consider three cases:} - \begin{spfcase}{$n=1$} - \begin{spfstep}[type=inline] then we compute $1=1^2$\end{spfstep} - \end{spfcase} - \begin{spfcase}{$n=2$} - \begin{spfcomment}[type=inline] + For the induction we have to consider three cases: % <- a comment + \begin{subproof}{$n=1$} + \spfstep*{then we compute $1=1^2$} + \end{subproof} + \begin{subproof}{$n=2$} This case is not really necessary, but we do it for the fun of it (and to get more intuition). - \end{spfcomment} - \begin{spfstep}[type=inline] We compute $1+3=2^{2}=4$.\end{spfstep} - \end{spfcase} - \begin{spfcase}{$n>1$} - \begin{spfstep}[type=assumption,id=ind-hyp] + \spfstep*{We compute $1+3=2^{2}=4$.} + \end{subproof} + \begin{subproof}{$n>1$}\begin{spfblock} + \assumption[id=ind-hyp]{ Now, we assume that the assertion is true for a certain $k\geq 1$, - i.e. $\sum_{i=1}^k{(2i-1)}=k^{2}$. - \end{spfstep} - \begin{spfcomment} + i.e. \yield{$\sum_{i=1}^k{(2i-1)}=k^{2}$}. + } + We have to show that we can derive the assertion for $n=k+1$ from this assumption, i.e. $\sum_{i=1}^{k+1}{(2i-1)}=(k+1)^{2}$. - \end{spfcomment} - \begin{spfstep} - We obtain $\sum_{i=1}^{k+1}{2i-1}=\sum_{i=1}^k{2i-1}+2(k+1)-1$ - \spfjust[method=arith:split-sum]{by splitting the sum}. - \end{spfstep} - \begin{spfstep} - Thus we have $\sum_{i=1}^{k+1}{(2i-1)}=k^2+2k+1$ - \spfjust[method=fertilize]{by inductive hypothesis}. - \end{spfstep} - \begin{spfstep}[type=conclusion] - We can \spfjust[method=simplify]{simplify} the right-hand side to + + \spfstep{ + We obtain $\yield{\sum_{i=1}^{k+1}{2i-1}= + \sum_{i=1}^k{2i-1}+2(k+1)-1}$ + \spfjust{by \splitsum{\comp{splitting the sum} + \arg*{$\sum_{i=1}^{k+1}{(2i-1)}=(k+1)^{2}$}}}. + } + \spfstep{ + Thus we have $\yield{\sum_{i=1}^{k+1}{(2i-1)}=k^2+2k+1}$ + \spfjust{by \symname{induction-hypothesis}}. + } + \conclude{ + We can \spfjust{\simplification{\comp{simplify} the right-hand side + \arg*{k^2+2k+1}}} to ${k+1}^2$, which proves the assertion. - \end{spfstep} - \end{spfcase} - \begin{spfstep}[type=conclusion] + } + \end{spfblock}\end{subproof} + \conclude{ We have considered all the cases, so we have proven the assertion. - \end{spfstep} - \end{spfcases} + } \end{sproof} \end{latexcode} + +\symdecl{splitsum}[args=1] +\symdecl{inducthypothesis}[name=induction-hypothesis] +\symdecl{simplification}[args=1] + This yields the following result: \begin{mdframed} - \begin{sproof}[id=simple-proof] - {We prove that $\sum_{i=1}^n{2i-1}=n^{2}$ by induction over $n$} - \begin{spfcases}{For the induction we have to consider the following cases:} - \begin{spfcase}{$n=1$} - \begin{spfstep}[type=inline] then we compute $1=1^2$\end{spfstep} - \end{spfcase} - \begin{spfcase}{$n=2$} - \begin{spfcomment}[type=inline] - This case is not really necessary, but we do it for the fun - of it (and to get more intuition). - \end{spfcomment} - \begin{spfstep}[type=inline] - We compute $1+3=2^{2}=4$ - \end{spfstep} - \end{spfcase} - \begin{spfcase}{$n>1$} - \begin{spfstep}[type=hypothesis,id=ind-hyp] - Now, we assume that the assertion is true for a certain $k\geq 1$, i.e. - $\sum_{i=1}^k{(2i-1)}=k^{2}$. - \end{spfstep} - \begin{spfcomment} - We have to show that we can derive the assertion for $n=k+1$ from this - assumption, i.e. $\sum_{i=1}^{k+1}{(2i-1)}=(k+1)^{2}$. - \end{spfcomment} - \begin{spfstep}[id=splitit] - We obtain $\sum_{i=1}^{k+1}{(2i-1)}=\sum_{i=1}^k{(2i-1)}+2(k+1)-1$ - \spfjust[method=arith:split-sum]{by splitting the sum}. - \end{spfstep} - \begin{spfstep}[id=byindhyp] - Thus we have $\sum_{i=1}^{k+1}{(2i-1)}=k^2+2k+1$ - \spfjust[method=fertilize]{by \premise[ind-hyp]{inductive hypothesis}}. - \end{spfstep} - \begin{spfstep}[type=conclusion] - We can \spfjust[method=simplify-eq]{simplify the \justarg[rhs]{right-hand side}} to - $(k+1)^2$, which proves the assertion. - \end{spfstep} - \end{spfcase} - \begin{spfstep}[type=conclusion] - We have considered all the cases, so we have proven the assertion. - \end{spfstep} - \end{spfcases} -\end{sproof} + \begin{sproof}[id=simple-proof,method=induction] + {We prove that $\sum_{i=1}^n{2i-1}=n^{2}$ by induction over $n$} + For the induction we have to consider three cases: % <- a comment + \begin{subproof}{$n=1$} + \spfstep*{then we compute $1=1^2$} + \end{subproof} + \begin{subproof}{$n=2$} + This case is not really necessary, but we do it for the + fun of it (and to get more intuition). + \spfstep*{We compute $1+3=2^{2}=4$.} + \end{subproof} + \begin{subproof}{$n>1$}\begin{spfblock} + \assumption[id=ind-hyp]{ + Now, we assume that the assertion is true for a certain $k\geq 1$, + i.e. \yield{$\sum_{i=1}^k{(2i-1)}=k^{2}$}. + } + + We have to show that we can derive the assertion for $n=k+1$ from + this assumption, i.e. $\sum_{i=1}^{k+1}{(2i-1)}=(k+1)^{2}$. + + \spfstep{ + We obtain $\yield{\sum_{i=1}^{k+1}{2i-1}=\sum_{i=1}^k{2i-1}+2(k+1)-1}$ + \spfjust{by \splitsum{\comp{splitting the sum}\arg*{$\sum_{i=1}^{k+1}{(2i-1)}=(k+1)^{2}$}}}. + } + \spfstep{ + Thus we have $\yield{\sum_{i=1}^{k+1}{(2i-1)}=k^2+2k+1}$ + \spfjust{by \symname{induction-hypothesis}}. + } + \conclude{ + We can \spfjust{\simplification{\comp{simplify} the right-hand side + \arg*{k^2+2k+1}}} to + ${k+1}^2$, which proves the assertion. + } + \end{spfblock}\end{subproof} + \conclude{ + We have considered all the cases, so we have proven the assertion. + } + \end{sproof} \end{mdframed} +\end{smodule} + \begin{environment}{sproof} The |sproof| environment is the main container for proofs. It takes an optional |KeyVal| argument that allows to specify the |id| (identifier) and |for| (for which assertion is @@ -114,78 +322,39 @@ This yields the following result: the proof. \end{function} -\begin{environment}{spfstep} - Regular proof steps are marked up with the |step| environment, which takes an optional +\begin{function}{\spfstep} + Regular proof steps are marked up with the |\spfstep| macro, which takes an optional |KeyVal| argument for annotations. A proof step usually contains a local assertion (the text of the step) together with some kind of evidence that this can be derived from already established assertions. -\end{environment} +\end{function} + +\begin{function}{\yield} + See above +\end{function} \begin{function}{\spfjust} This evidence is marked up with the |\spfjust| macro in the \pkg{stex-proofs} package. This environment totally invisible to the formatted result; it wraps the text - in the proof step that corresponds to the evidence. The environment takes an optional - |KeyVal| argument, which can have the |method| key, whose value is the name of a proof - method (this will only need to mean something to the application that consumes the - semantic annotations). Furthermore, the justification can contain ``premises'' - (specifications to assertions that were used justify the step) and ``arguments'' - (other information taken into account by the proof method). + in the proof step that corresponds to the evidence (ideally, a + semantically marked-up term). \end{function} -\begin{function}{\premise} - The |\premise| macro allows to mark up part of the text as reference to an assertion - that is used in the argumentation. In the running example we have used the |\premise| - macro to identify the inductive hypothesis. +\begin{function}{\assumption} + The |\assumption| macro allows to mark up a (justified) assumption. \end{function} \begin{function}{\justarg} - The |\justarg| macro is very similar to |\premise| with the difference that it is used - to mark up arguments to the proof method. Therefore the content of the first argument - is interpreted as a mathematical object rather than as an identifier as in the case of - |\premise|. In our example, we specified that the simplification should take place on - the right hand side of the equation. Other examples include proof methods that - instantiate. Here we would indicate the substituted object in a |\justarg| macro. \end{function} -Note that both |\premise| and |\justarg| can be used with an empty second argument to -mark up premises and arguments that are not explicitly mentioned in the text. - \begin{environment}{subproof} - The |spfcases| environment is used to mark up a subproof. This environment takes an + The |subproof| environment is used to mark up a subproof. This environment takes an optional |KeyVal| argument for semantic annotations and a second argument that allows to specify an introductory comment (just like in the |proof| environment). The |method| key can be used to give the name of the proof method executed to make this subproof. \end{environment} -\begin{environment}{spfcases} - The |spfcases| environment is used to mark up a proof by cases. Technically it is a - variant of the |subproof| where the |method| is |by-cases|. Its contents are |spfcase| - environments that mark up the cases one by one. -\end{environment} - -\begin{environment}{spfcase} - The content of a |spfcases| environment are a sequence of case proofs marked up in the - |spfcase| environment, which takes an optional |KeyVal| argument for semantic - annotations. The second argument is used to specify the the description of the case - under consideration. The content of a |spfcase| environment is the same as that of a - |sproof|, i.e. |spfstep|s, |spfcomment|s, and |spfcases| environments. -\end{environment} - -\begin{function}{\spfcasesketch} - |\spfcasesketch| is a variant of the |spfcase| environment that takes the same - arguments, but instead of the |spfstep|s in the body uses a third argument for a proof - sketch. -\end{function} - -\begin{environment}{spfcomment} - The |spfcomment| environment is much like a |step|, only that it does not have an - object-level assertion of its own. Rather than asserting some fact that is relevant - for the proof, it is used to explain where the proof is going, what we are attempting - to to, or what we have achieved so far. As such, it cannot be the target of a - |\premise|. -\end{environment} - \begin{function}{\sproofend} Traditionally, the end of a mathematical proof is marked with a little box at the end of the last line of the proof (if there is space and on the end of the next line if there @@ -205,10 +374,14 @@ in most cases, this is desirable to make the proof structure explicit, but somet wastes space (especially, if a proof ends in a case analysis which will supply its own proof end marker). To suppress it locally, just set |proofend={}| in them or use use |\sProofEndSymbol{}|. +\end{sfragment} %%% Local Variables: %%% mode: latex %%% TeX-master: "../stex-manual" %%% End: -% LocalWords: hypothesis,id geq splitit arith:split-sum byindhyp rhs proofend +% LocalWords: hypothesis,id geq splitit arith:split-sum byindhyp rhs proofend eqstep +% LocalWords: sproofs coprime ratfrac 2,prec intpow ratpow inttimes varb varc sqrt2irr +% LocalWords: theorem,name sqrt2irr,method wlog hide,method hide,term spfblock splitsum +% LocalWords: simple-proof,method inducthypothesis -- cgit v1.2.3