Lab for Automated Reasoning and Analysis LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

sav08:proof_of_first_lecture01_example [2008/02/19 14:16]
vkuncak
sav08:proof_of_first_lecture01_example [2015/04/21 17:30] (current)
Line 21: Line 21:
 By translating Java code into math, we obtain the following mathematical definition of $f$: By translating Java code into math, we obtain the following mathematical definition of $f$:
  
-\[+\begin{equation*}
     f(x,y) = \left\{\begin{array}{rl}     f(x,y) = \left\{\begin{array}{rl}
 0, & \mbox{ if } y = 0 \\ 0, & \mbox{ if } y = 0 \\
Line 27: Line 27:
 x + f(x,y-1), & \mbox{ if } y > 0, \mbox{ and } y=2k+1 \mbox{ for some } k \\ x + f(x,y-1), & \mbox{ if } y > 0, \mbox{ and } y=2k+1 \mbox{ for some } k \\
 \end{array}\right. \end{array}\right.
-\]+\end{equation*}
  
 By induction on $y$ we then prove $f(x,y) = x \cdot y$. By induction on $y$ we then prove $f(x,y) = x \cdot y$.
Line 34: Line 34:
      * Goal: show that it holds for $y$ where $y > 0$.       * Goal: show that it holds for $y$ where $y > 0$. 
      * **Case 1**: $y = 2k$. Note $k < y$. By definition and I.H.      * **Case 1**: $y = 2k$. Note $k < y$. By definition and I.H.
-\[+\begin{equation*}
    ​f(x,​y) = f(x,2k) = 2 f(x,k) = 2 (x k) = x (2 k) = x y    ​f(x,​y) = f(x,2k) = 2 f(x,k) = 2 (x k) = x (2 k) = x y
-\]+\end{equation*}
   *   *
-     * **Case 2**: $y = 2k+1$. Note $y-1 < y$ and $k < y$. By definition and I.H. +     * **Case 2**: $y = 2k+1$. Note $y-1 < y$. By definition and I.H. 
-\[ +\begin{equation*} 
-   ​f(x,​y) = f(x,2k+1) = x + f(x,2k) = x + 2 f(x,k) = x + 2 (x k) = x (2 k + 1) = x y +   ​f(x,​y) = f(x,2k+1) = x + f(x,2k) = x + x \cdot (2k) = x (2 k + 1) = x y 
-\]+\end{equation*}
 This completes the proof. This completes the proof.
  
 
sav08/proof_of_first_lecture01_example.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice