1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-isac/mlehnfeld/presentation.tex Tue Sep 17 09:50:52 2013 +0200
1.3 @@ -0,0 +1,469 @@
1.4 +% $Header: /cvsroot/latex-beamer/latex-beamer/solutions/conference-talks/conference-ornate-20min.en.tex,v 1.7 2007/01/28 20:48:23 tantau Exp $
1.5 +
1.6 +\documentclass{beamer}
1.7 +
1.8 +% This file is a solution template for:
1.9 +
1.10 +% - Talk at a conference/colloquium.
1.11 +% - Talk length is about 20min.
1.12 +% - Style is ornate.
1.13 +
1.14 +
1.15 +
1.16 +% Copyright 2004 by Till Tantau <tantau@users.sourceforge.net>.
1.17 +%
1.18 +% In principle, this file can be redistributed and/or modified under
1.19 +% the terms of the GNU Public License, version 2.
1.20 +%
1.21 +% However, this file is supposed to be a template to be modified
1.22 +% for your own needs. For this reason, if you use this file as a
1.23 +% template and not specifically distribute it as part of a another
1.24 +% package/program, I grant the extra permission to freely copy and
1.25 +% modify this file as you see fit and even to delete this copyright
1.26 +% notice.
1.27 +
1.28 +
1.29 +\mode<presentation>
1.30 +{
1.31 + \usetheme{Hannover}
1.32 + % or ...
1.33 +
1.34 + \setbeamercovered{transparent}
1.35 + % or whatever (possibly just delete it)
1.36 +}
1.37 +
1.38 +%\usepackage{setspace} %for "\begin{onehalfspace}"
1.39 +\usepackage[english]{babel}
1.40 +% or whatever
1.41 +
1.42 +\usepackage[utf8]{inputenc}
1.43 +% or whatever
1.44 +
1.45 +\usepackage{times}
1.46 +\usepackage[T1]{fontenc}
1.47 +% Or whatever. Note that the encoding and the font should match. If T1
1.48 +% does not look nice, try deleting the line with the fontenc.
1.49 +
1.50 +\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
1.51 +\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
1.52 +
1.53 +\title[\isac: Computation \& Deduction] % (optional, use only with long paper titles)
1.54 +{Integrating Computation and Deduction\\
1.55 + in the \isac-System}
1.56 +
1.57 +\subtitle{Projektpraktikum: Introducing Isabelle's Contexts}
1.58 +
1.59 +\author[Lehnfeld] % (optional, use only with lots of authors)
1.60 +{Mathias~Lehnfeld}
1.61 +% - Give the names in the same order as the appear in the paper.
1.62 +% - Use the \inst{?} command only if the authors have different
1.63 +% affiliation.
1.64 +
1.65 +\institute % (optional, but mostly needed)
1.66 +{
1.67 + Vienna University of Technology\\
1.68 + Institute of Computer Languages
1.69 +}
1.70 +% - Use the \inst command only if there are several affiliations.
1.71 +% - Keep it simple, no one is interested in your street address.
1.72 +
1.73 +% \date[CFP 2003] % (optional, should be abbreviation of conference name)
1.74 +% {Conference on Fabulous Presentations, 2003}
1.75 +% - Either use conference name or its abbreviation.
1.76 +% - Not really informative to the audience, more for people (including
1.77 +% yourself) who are reading the slides online
1.78 +
1.79 +% \subject{Theoretical Computer Science}
1.80 +% This is only inserted into the PDF information catalog. Can be left
1.81 +% out.
1.82 +
1.83 +
1.84 +
1.85 +% If you have a file called "university-logo-filename.xxx", where xxx
1.86 +% is a graphic format that can be processed by latex or pdflatex,
1.87 +% resp., then you can add a logo as follows:
1.88 +
1.89 +% \pgfdeclareimage[height=0.5cm]{university-logo}{university-logo-filename}
1.90 +% \logo{\pgfuseimage{university-logo}}
1.91 +
1.92 +
1.93 +
1.94 +% Delete this, if you do not want the table of contents to pop up at
1.95 +% the beginning of each subsection:
1.96 +\AtBeginSubsection[]
1.97 +{
1.98 + \begin{frame}<beamer>{Outline}
1.99 + \tableofcontents[currentsection,currentsubsection]
1.100 + \end{frame}
1.101 +}
1.102 +
1.103 +
1.104 +% If you wish to uncover everything in a step-wise fashion, uncomment
1.105 +% the following command:
1.106 +
1.107 +%\beamerdefaultoverlayspecification{<+->}
1.108 +
1.109 +
1.110 +\begin{document}
1.111 +
1.112 +\begin{frame}
1.113 + \titlepage
1.114 +\end{frame}
1.115 +
1.116 +\begin{frame}{Outline}
1.117 + \tableofcontents
1.118 + % You might wish to add the option [pausesections]
1.119 +\end{frame}
1.120 +
1.121 +
1.122 +% Structuring a talk is a difficult task and the following structure
1.123 +% may not be suitable. Here are some rules that apply for this
1.124 +% solution:
1.125 +
1.126 +% - Exactly two or three sections (other than the summary).
1.127 +% - At *most* three subsections per section.
1.128 +% - Talk about 30s to 2min per frame. So there should be between about
1.129 +% 15 and 30 frames, all told.
1.130 +
1.131 +% - A conference audience is likely to know very little of what you
1.132 +% are going to talk about. So *simplify*!
1.133 +% - In a 20min talk, getting the main ideas across is hard
1.134 +% enough. Leave out details, even if it means being less precise than
1.135 +% you think necessary.
1.136 +% - If you omit details that are vital to the proof/implementation,
1.137 +% just say so once. Everybody will be happy with that.
1.138 +
1.139 +\section[Introduction]{Introduction: Isabelle and \isac}
1.140 +%\subsection[Isabelle \& \isac]{Isabelle and \isac}
1.141 +\begin{frame}
1.142 + \frametitle{Isabelle and \isac}
1.143 +The task of this ``Projektpraktikum'' (6 ECTS) was to
1.144 +\begin{itemize}
1.145 +\item study the concept of ``context'' in the theorem prover \textbf{Isabelle} from TU Munich
1.146 +\item study basic concepts of the math assistant \sisac{} from TU Graz
1.147 +\pause
1.148 +\item redesign \sisac{} with respect to contexts
1.149 + \begin{itemize}
1.150 + \item use contexts for type inference of user input
1.151 + \item handle preconditions of specifications
1.152 + \item clarify the transfer of context data from sub-programs to the calling program
1.153 + \end{itemize}
1.154 +\pause
1.155 +\item introduce contexts to \sisac{} according to the new design
1.156 +\item use the coding standards of Isabelle2011 for new code.
1.157 +\end{itemize}
1.158 +\end{frame}
1.159 +
1.160 +%\subsection[Computation \& Deduction]{Computation and Deduction in a Lucas-Interpreter}
1.161 +\begin{frame}
1.162 + \frametitle{Computation and Deduction in a Lucas-Interpreter}
1.163 + \includegraphics[width=100mm]{overview.pdf}
1.164 +\end{frame}
1.165 +
1.166 +\section[Contributions]{Contributions of the project to \isac}
1.167 +\subsection[Contexts]{Isabelle's Contexts, advantages and use}
1.168 +\begin{frame}
1.169 + \frametitle{Advantages of Isabelle's Contexts}
1.170 +Isabelle's context replaced theories because \dots:
1.171 +\begin{itemize}
1.172 +\item theories are static containers of \textit{all} logical data
1.173 +\item contexts are \textit{dynamic} containers of logical data:
1.174 + \begin{itemize}
1.175 + \item functions for storing and retrieving various logical data
1.176 + \item functions for type inference
1.177 + \item provide data for Isabelle's automated provers
1.178 + \end{itemize}
1.179 +%\item e.g. theories have no direct functions for type inference
1.180 +%\item replace function \texttt{parseNEW}
1.181 +%\item assumptions \& environment $\rightarrow$ context
1.182 +\item allow to conform with scopes for subprograms.
1.183 +\end{itemize}
1.184 +\end{frame}
1.185 +
1.186 +\begin{frame}
1.187 + \frametitle{Isabelle's context mechanism}
1.188 + \texttt{\small{
1.189 + \begin{tabbing}
1.190 +xx\=xx\=in\=\kill
1.191 +%xx\=xx\=xx\=xx\=\kill
1.192 +%datatype Isac\_Ctxt =\\
1.193 +%\>\>Env of term * term\\
1.194 +%\>| Asm of term;\\
1.195 +%\\
1.196 +structure ContextData = \alert{Proof\_Data}\\
1.197 +\>~(\alert{type T} = term list\\
1.198 +\>\>\alert{fun init \_} = []);\\
1.199 +\\
1.200 +%local\\
1.201 +%\>fun insert\_ctxt data = ContextData\alert{.map} (fn xs => distinct (data@xs));\\
1.202 +%in\\
1.203 +%\>fun insert\_assumptions asms = map (fn t => Asm t) asms |> insert\_ctxt;\\
1.204 +%\>fun insert\_environments envs = map (fn t => Env t) envs |> insert\_ctxt;\\
1.205 +%end\\
1.206 +fun insert\_assumptions asms = \\
1.207 +\>\>\>ContextData\alert{.map} (fn xs => distinct (asms@xs));\\
1.208 +\\
1.209 +%local\\
1.210 +%\>fun unpack\_asms (Asm t::ts) = t::(unpack\_asms ts)\\
1.211 +%\>\>| unpack\_asms (Env \_::ts) = unpack\_asms ts\\
1.212 +%\>\>| unpack\_asms [] = [];\\
1.213 +%\>fun unpack\_envs (Env t::ts) = t::(unpack\_envs ts)\\
1.214 +%\>\>| unpack\_envs (Asm \_::ts) = unpack\_envs ts\\
1.215 +%\>\>| unpack\_envs [] = [];\\
1.216 +%in\\
1.217 +%\>fun get\_assumptions ctxt = ContextData.get ctxt |> unpack\_asms;\\
1.218 +%\>fun get\_environments ctxt = ContextData.get ctxt |> unpack\_envs;\\
1.219 +%end
1.220 +fun get\_assumptions ctxt = ContextData\alert{.get} ctxt;\\
1.221 +\\
1.222 +\\
1.223 +val declare\_constraints : \\
1.224 +\>\>\>term -> Proof.context -> Proof.context
1.225 + \end{tabbing}
1.226 + }}
1.227 +\end{frame}
1.228 +
1.229 +\begin{frame}
1.230 + \frametitle{Usage of Contexts}
1.231 + \texttt{\footnotesize{
1.232 + \begin{tabbing}
1.233 +xx\=xx\=xx\=xx\=xx\=\kill
1.234 +fun transfer\_asms\_from\_to from\_ctxt to\_ctxt =\\
1.235 +\> let\\
1.236 +\>\> val to\_vars = get\_assumptions to\_ctxt |> map vars |> flat\\
1.237 +\>\> fun transfer [] to\_ctxt = to\_ctxt\\
1.238 +\>\>\> | transfer (from\_asm::fas) to\_ctxt =\\
1.239 +\>\>\>\>\> if inter op = (vars from\_asm) to\_vars = []\\
1.240 +\>\>\>\>\> then transfer fas to\_ctxt\\
1.241 +\>\>\>\>\> else transfer fas (insert\_assumptions [from\_asm] to\_ctxt)\\
1.242 +\> in transfer (get\_assumptions from\_ctxt) to\_ctxt end\\
1.243 +\\
1.244 +fun parse thy str =\\
1.245 +\>(let val t = (\alert{typ\_a2real} o numbers\_to\_string)\\
1.246 +\>\>\>\>(\alert{Syntax.read\_term\_global thy} str)\\
1.247 +\>\>in SOME (cterm\_of thy t) end)\\
1.248 +\>\>\>handle \_ => NONE;\\
1.249 +\\
1.250 +fun parseNEW ctxt str = \\
1.251 +\>\>\>SOME (\alert{Syntax.read\_term ctxt} str |> numbers\_to\_string)\\
1.252 +\>\>\>handle \_ => NONE;
1.253 + \end{tabbing}
1.254 + }}
1.255 +
1.256 +
1.257 +\end{frame}
1.258 +
1.259 +\subsection[Redesign]{Redesign of \isac{} using contexts}
1.260 +\begin{frame}
1.261 + \frametitle{Redesign of \isac{} using contexts}
1.262 +\begin{center} DEMO \end{center}
1.263 +\end{frame}
1.264 +
1.265 +\begin{frame}
1.266 + \frametitle{Deduction simplifies computation}
1.267 +\small{
1.268 +%\begin{onehalfspace}
1.269 +\begin{tabbing}
1.270 +xxx\=xxx\=\kill
1.271 + \`$\mathit{(some)}\;\mathit{assumptions}$\\
1.272 +$\mathit{solve}\;(\frac{x}{x ^ 2 - 6 * x + 9} - \frac{1}{x ^ 2 - 3 * x} = \frac{1}{x}, x)$\\
1.273 +% \`$x ^ 2 - 6 * x + 9\not=0\land x ^ 2 - 3 * x\not=0$\\
1.274 +%\>$\frac{x}{x ^ 2 - 6 * x + 9} - \frac{1}{x ^ 2 - 3 * x} = \frac{1}{x}$ \\ \\
1.275 +%\>$\frac{x}{x ^ 2 + -1 * (6 * x) + 9} + \frac{-1 * 1}{x ^ 2 + -1 * (3 * x)} = \frac{1}{x}$ \\ \\
1.276 +\>$\frac{3 + -1 * x + x ^ 2}{9 * x + -6 * x ^ 2 + x ^ 3} = \frac{1}{x}$ \\
1.277 + \`$x\not=3\land x\not=0$\\
1.278 +\>$(3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)$ \\
1.279 +\>$\mathit{solve}\;((3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3), x)$ \\
1.280 +%\>\>$(3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)$ \\
1.281 +%\>\>$(3 + -1 * x + x ^ 2) * x - 1 * (9 * x + -6 * x ^ 2 + x ^ 3) = 0$ \\
1.282 +\>\>$(3 + -1 * x + x ^ 2) * x - (9 * x + -6 * x ^ 2 + x ^ 3) = 0$ \\
1.283 +\>\>$-6 * x + 5 * x ^ 2 = 0$ \\
1.284 +\>\>$\mathit{solve}\;(-6 * x + 5 * x ^ 2 = 0, x)$ \\
1.285 +\>\>$[x = 0, x = \frac{6}{5}]$ \\
1.286 + \`$x = 0\land x = \frac{6}{5}$\\
1.287 +\>$[\alert{x = 0}, x = \frac{6}{5}]$ \\
1.288 + \`\alert{$\mathit{Check\_Elementwise}\;\mathit{Assumptions}:x\not=0\land x = 0$}\\
1.289 +\>$[x = \frac{6}{5}]$ \\
1.290 +$[x = \frac{6}{5}]$
1.291 +\end{tabbing}
1.292 +}
1.293 +%\end{onehalfspace}
1.294 +\end{frame}
1.295 +
1.296 +\begin{frame}
1.297 + \frametitle{More ``deduction'', \\less ``computation''}
1.298 +\footnotesize{\tt
1.299 +\begin{tabbing}
1.300 +xx\=xx\=xx\=xx\=xx\=xx\=\kill
1.301 +Script Solve\_root\_equation (e\_e::bool) (v\_v::real) = \\
1.302 +\> (let e\_e = ((Try (Rewrite\_Set norm\_equation False)) \@\@ \\
1.303 +\>\>\> (Try (Rewrite\_Set Test\_simplify False))) e\_e; \\
1.304 +\>\> (L\_L::bool list) = \\
1.305 +\>\>\> (SubProblem (Test', \\
1.306 +\>\>\>\> [linear,univariate,equation,test]\\
1.307 +\>\>\>\> [Test,solve\_linear]) \\
1.308 +\>\>\>\> [BOOL e\_e, REAL v\_v]) \\
1.309 +\> in \alert{Check\_elementwise L\_L \{(v\_v::real). Assumptions\}})\\
1.310 +\end{tabbing}
1.311 +}
1.312 +\small{
1.313 +``Deductive'' part of Lucas-Interpretation relives the ``computational'' part: \alert{one statement becomes obsolete~!}
1.314 +}
1.315 +\end{frame}
1.316 +
1.317 +
1.318 +\begin{frame}
1.319 + \frametitle{Redesign of \isac{} using contexts}
1.320 +Advantages of the redesign:
1.321 +\begin{itemize}
1.322 +\item type inference by \textit{local} contexts\\
1.323 +\pause
1.324 + \alert{now user-input without type constraints~!}
1.325 +\pause
1.326 +\item consistent handling of logical data
1.327 + \begin{itemize}
1.328 + \item preconditions and partiality conditions in contexts
1.329 + \item transfer of context data into subprograms clarified
1.330 + \item transfer of context data from subprograms clarified
1.331 + \end{itemize}
1.332 +\pause
1.333 + \alert{now some statements become obsolete.}\\
1.334 +\end{itemize}
1.335 +\pause
1.336 +Now Lucas-interpretation shifts efforts from ``computation'' further to ``deduction''.
1.337 +\end{frame}
1.338 +
1.339 +
1.340 +
1.341 +\subsection[Code Improvement]{Improvement of functional code}
1.342 +\begin{frame}
1.343 + \frametitle{Improvement of functional code}
1.344 + \begin{itemize}
1.345 + \item \textbf{code conventions}: Isabelle2011 published coding standards first time
1.346 + \item \textbf{combinators}: Isabelle2011 introduced a library containing the following combinators:
1.347 +\\\vspace{0.2cm}
1.348 +\tiny{\tt%
1.349 + val |$>$ : 'a * ('a -$>$ 'b) -$>$ 'b\\
1.350 + val |-$>$ : ('c * 'a) * ('c -$>$ 'a -$>$ 'b) -$>$ 'b\\
1.351 + val |$>>$ : ('a * 'c) * ('a -$>$ 'b) -$>$ 'b * 'c\\
1.352 + val ||$>$ : ('c * 'a) * ('a -$>$ 'b) -$>$ 'c * 'b\\
1.353 + val ||$>>$ : ('c * 'a) * ('a -$>$ 'd * 'b) -$>$ ('c * 'd) * 'b\\
1.354 + val \#$>$ : ('a -$>$ 'b) * ('b -$>$ 'c) -$>$ 'a -$>$ 'c\\
1.355 + val \#-$>$ : ('a -$>$ 'c * 'b) * ('c -$>$ 'b -$>$ 'd) -$>$ 'a -$>$ 'd\\
1.356 + val \#$>>$ : ('a -$>$ 'c * 'b) * ('c -$>$ 'd) -$>$ 'a -$>$ 'd * 'b\\
1.357 + val \#\#$>$ : ('a -$>$ 'c * 'b) * ('b -$>$ 'd) -$>$ 'a -$>$ 'c * 'd\\
1.358 + val \#\#$>>$ : ('a -$>$ 'c * 'b) * ('b -$>$ 'e * 'd) -$>$ 'a -$>$ ('c * 'e) * 'd\\
1.359 +}
1.360 + \end{itemize}
1.361 +\end{frame}
1.362 +
1.363 +\begin{frame}
1.364 + \frametitle{Example with combinators}
1.365 + \texttt{\footnotesize{
1.366 + \begin{tabbing}
1.367 +xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=\kill
1.368 +fun prep\_ori [] \_ \_ = ([], e\_ctxt)\\
1.369 +\>| prep\_ori fmz thy pbt =\\
1.370 +\>\>\>let\\
1.371 +\>\>\>\>val ctxt = ProofContext.init\_global thy \\
1.372 +\>\>\>\>\> |> fold declare\_constraints fmz\\
1.373 +\>\>\>\>val ori = \\
1.374 +\>\>\>\>\> map (add\_field thy pbt o split\_dts o the o parseNEW ctxt) fmz\\
1.375 +\>\>\>\>\>\> |> add\_variants\\
1.376 +\>\>\>\>val maxv = map fst ori |> max\\
1.377 +\>\>\>\>val maxv = if maxv = 0 then 1 else maxv\\
1.378 +\>\>\>\>val oris = coll\_variants ori\\
1.379 +\>\>\>\>\> |> map (replace\_0 maxv |> apfst)\\
1.380 +\>\>\>\>\> |> add\_id\\
1.381 +\>\>\>\>\> |> map flattup\\
1.382 +\>\>\>in (oris, ctxt) end;
1.383 + \end{tabbing}
1.384 + }}
1.385 +\dots which probably can be further polished.
1.386 +\end{frame}
1.387 +
1.388 +%\subsection[Future Development]{Preparation of Future Development}
1.389 +%\begin{frame}
1.390 +% \frametitle{Preparation of Future Development}
1.391 +%
1.392 +%% "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1.393 +%% " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@ " ^
1.394 +%% " (Try (Rewrite_Set Test_simplify False))) e_e; " ^
1.395 +%% " (L_L::bool list) = " ^
1.396 +%% " (SubProblem (Test', " ^
1.397 +%% " [linear,univariate,equation,test]," ^
1.398 +%% " [Test,solve_linear]) " ^
1.399 +%% " [BOOL e_e, REAL v_v]) " ^
1.400 +%% " in Check_elementwise L_L {(v_v::real). Assumptions}) "
1.401 +%\end{frame}
1.402 +%
1.403 +%\begin{frame}
1.404 +% \frametitle{Preparation of Future Development}
1.405 +% \begin{itemize}
1.406 +% \item logical data for Isabelle provers in contexts
1.407 +% \item \isac{} programming language more compact\\
1.408 +% $\rightarrow$ context built automatically
1.409 +% \end{itemize}
1.410 +%\end{frame}
1.411 +
1.412 +
1.413 +\section[Problems]{Problems encountered in the project}
1.414 +\begin{frame}
1.415 + \frametitle{Problems encountered in the project}
1.416 + \begin{itemize}
1.417 + \item new Isabelle release in February 2011: update \sisac{} first
1.418 +\pause
1.419 + \item lines of code (LOC) in Isabelle and \sisac{}\\ \vspace{0.2cm}
1.420 +\textit{
1.421 + \begin{tabular}{lrl}
1.422 + src/ & 1700 & $\,$k LOC\\
1.423 + src/Pure/ & 70 & k LOC\\
1.424 + src/Provers/ & 8 & k LOC\\
1.425 + src/Tools/ & 800 & k LOC\\
1.426 + src/Tools/isac/ & 37 & k LOC\\
1.427 + src/Tools/isac/Knowledge & 16 & k LOC
1.428 + \end{tabular}
1.429 +}
1.430 +\pause
1.431 + \item changes scattered throughout the code ($\rightarrow$ grep)
1.432 +\pause
1.433 + \item documentation of Isabelle very ``technical'' (no API)
1.434 +\pause
1.435 + \item documentation of \sisac{} not up to date
1.436 + \end{itemize}
1.437 +\end{frame}
1.438 +
1.439 +%\begin{frame}
1.440 +% \frametitle{Lines of Code}
1.441 +% \begin{tabular}{lr}
1.442 +% src/ & 1700 k \\
1.443 +% src/Pure/ & 70 k \\
1.444 +% src/Provers/ & 8 k \\
1.445 +% src/Tools/ & 800 k \\
1.446 +% src/Tools/isac/ & 37 k \\
1.447 +% src/Tools/isac/Knowledge & 16 k \\
1.448 +% \end{tabular}
1.449 +%\end{frame}
1.450 +
1.451 +\section{Summary}
1.452 +\begin{frame}
1.453 + \frametitle{Summary}
1.454 +The project succeeded in all goals:
1.455 +\begin{itemize}
1.456 +\item implemented Isabelle's contexts in \sisac{} such that
1.457 +\item user input requires no type constraints anymore
1.458 +\item consistent logical data is prepared for Isabelle's provers
1.459 +\end{itemize}
1.460 +\pause
1.461 +The course of the project was close to the plan:
1.462 +\begin{itemize}
1.463 +\item faster in writing new code
1.464 +\item slower in integrating the code into \sisac
1.465 +\end{itemize}
1.466 +\pause
1.467 +The project provided essential prerequisites for further development of the Lucas-interpreter.
1.468 +\end{frame}
1.469 +
1.470 +\end{document}
1.471 +
1.472 +