1.1 --- a/src/Doc/isac/mlehnfeld/presentation.tex Mon Sep 16 12:27:20 2013 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,469 +0,0 @@
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 -