\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{2. feladatsor, 12. feladat}
\begin{document}
\noindent
\emph{Feladat:} Adjuk meg az $f$ függvény egy $k$-val osztható
értékéhez tartozó argumentumát!

\emph{Specifikáció:}\\
$A = \alatt{\Z}{m} \times \alatt{\Z}{n} \times \alatt{\N}{k} \times \alatt{\L}{l} \times \alatt{\Z}{i}$\\
$B = \alatt{\Z}{m'} \times \alatt{\Z}{n'} \times \alatt{\N}{k}$\\
$Q = ( m=m' \es n=n' \es m\le n+1 \es k=k')$ \\
$R = ( Q \es l=(\exists i\in[m..n]: (k\mid f(i))) \es l\nyil (i\in[m..n]\es k\mid f(i)))$

A specifikáció hasonlít a lin. ker. 2.8 specifikációjához, pár apró
eltéréstől eltekintve.  Ezeket foglalja össze a táblázat:

\begin{tabular}{cccr}
  feladat &  & lin. ker. 2.8 & \\
  \hline
  $k\mid f(i)$ & \knyil & $\beta(i)$ \\
\end{tabular}

A visszavezetés általánosított, hiszen  utófeltétel gyengébb a
feladatban, mint a tételben (mi nem követeljük meg, hogy az első
$k$-val osztható értékhez találjuk meg az argumentumot).

\begin{stuki}
  \stm{i,l:=m-1,\hamis}
  \begin{WHILE}{2}{\stm{\nem l \es i \ne n}}
    \stm{l:=k\mid f(i+1)}
    \stm{i:=i+1}
  \end{WHILE}
\end{stuki}
\end{document}