Changeset 142 for docs

Legend:

Unmodified

Added

Removed

• docs/trunk/omega-test-slides/omega-test.tex

  r141	r142
  489	489	\begin{frame}[fragile]
  490	490	\frametitle{Integers}
  491	\includegraphics[width=100mm]{Omega-Test-Number-Line.png}
  492
  493	$\neg \exists x: a\beta \leq abx \leq b\alpha \implies b\alpha - a\beta \leq ab - a - b$
  494
  495	Using $A \implies B = \lnot B \implies \lnot A$:
  496
  491	\only<1>{ \begin{center} \includegraphics[width=100mm]{Omega-Test-Number-Line.png} \end{center} }
  492	\only<1-2>{ \begin{align*}
  493	% I can explain it without this equation, and I think it's easier that way:
  494	%\only<1>{\neg \exists x: a\beta \leq abx \leq b\alpha &\implies b\alpha - a\beta \leq ab - a - b \\ }
  495	\only<1-2>{ b\alpha - a\beta > ab - a - b &\implies \exists x: a\beta \leq abx \leq b\alpha \\ }
  496	\only<2>{ b\alpha - a\beta \geq ab - a - b + 1 &\implies \ldots \\
  497	b\alpha - a\beta \geq (a - 1)(b - 1) &\implies \ldots }
  498	\end{align*} }
  497	499	\note{$A \implies B$
  498	500
  …	…
  503	505	$\lnot B \implies \lnot A$ (by definition)
  504	506	}
  505
  506	$b\alpha - a\beta > ab - a - b \implies \exists x: a\beta \leq abx \leq b\alpha$
  507
  508	$b\alpha - a\beta \geq ab - a - b + 1 \implies \ldots$
  509
  510	$b\alpha - a\beta \geq (a - 1)(b - 1) \implies \ldots$
  511
  512	Term this constraint $C_D$. $\operatorname{hasIntSol}(C_D) \implies \exists x: a\beta \leq abx \leq b\alpha$.
  513	Therefore $\operatorname{hasIntSol}(C_R) \land \operatorname{hasIntSol}(C_D) \implies \operatorname{hasIntSol}(C)$
  514
  515	N.B. $a = 1 \vee b = 1 \implies b\alpha - a\beta \geq 0 \implies b\alpha \geq a\beta$
  516
  507	\only<2>
  508	{
  509	\begin{itemize}
  510	\item Term this constraint $C_D$ (the dark shadow). $C_D$ has an integer solution $\implies \exists x: a\beta \leq abx \leq b\alpha$
  511	\item If both $C_R$ and $C_D$ have an integer solution, so does $C$
  512	\item N.B. $a = 1 \vee b = 1 \implies b\alpha - a\beta \geq 0 \implies b\alpha \geq a\beta$
  513	\end{itemize}
  514	}
  517	515
  518	516	\end{frame}

Note: See TracChangeset for help on using the changeset viewer.