\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{2. feladatsor, 33. feladat}
\begin{document}
\noindent
\emph{Feladat:} Keressük meg az $f$ függvény egy olyan értékét, amely
egyenlő a közvetlen szomszédai átlagával!

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

A lineáris keresés 2.8 specifikációja hasonló.  Lássuk,
hogy az alábbi átnevezés után milyen különbségek maradnak:

\begin{tabular}{ccc}
feladat &  & lin. ker. 2.8 \\
\hline
$m+1$ & \knyil & $m$ \\
$n-1$ & \knyil & $n$ \\
$f(i)=\frac{f(i-1)+f(i+1)}{2}$ & \knyil & $\beta(i)$
\end{tabular}

A visszavezetés általánosított, hiszen nem követeljük meg, hogy az
első ilyen speciális tulajdonságú elemet találjuk meg.

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

\end{document}
