\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{2. feladatsor, 5. feladat}
\begin{document}
\noindent
\emph{Feladat:} Adjunk meg egy az $n$ és $2n$ természetes számok közé eső
prímszámot!

\emph{Specifikáció:}\\
$A = \alatt{\N}{n} \times \alatt{\N}{p}$\\
$B = \alatt{\N}{n'}$\\
$Q = ( n=n' \es \exists j\in [n..2n]: \text{prím}(j))$\\
$R = ( Q \es p\in [n..2n] \es \text{prím}(p))$

A lineáris keresés 1. változatának specifikációja hasonló.  Lássuk,
hogy az alábbi átnevezések után milyen különbségek maradnak!

\begin{tabular}{ccc}
feladat &  & lin. ker. 1.0 \\
\hline
$n$ & \knyil & $m$ \\
$p$ & \knyil & $i$ \\
$\text{prím}(i)$ & \knyil & $\beta(i)$
\end{tabular}

Különbség, hogy az előfeltételünk szigorúbb, hiszen a $j$ futóindexnek
nem csupán $n$ fölött, hanem $2n$ alatt kell lennie.  (Megjegyezzük,
hogy a specifikáció előfeltétele az általánosságot nem szorítja meg,
ugyanis minden $n$ természetes szám esetén létezik egy prím $n$ és
$2n$ között. (Csebisev-tétel))

A lin. ker. 1 utófeltételének behelyettesítés utáni alakja:\\
$R' = (Q \es p\ge n \es \text{prím}(p) \es \forall j\in[n..p-1]:\nem\text{prím}(j))$

Ez az utófeltétel biztosítja az $R$ feltételt a Csebisev-tétel miatt.
Hiszen, ha $p$-nek olyannak kell lennie, hogy $p-1$-ig ne legyen prím
$n$-től, és $p$ prím, akkor p biztosan $2n$-nél kisebb.  Ugyanakkor az
$R$ nem követeli meg, hogy $p-1$-ig minden szám $n$-től kezdve
összetett legyen, ezért a két feltétel között egyenlőség nem, csupán
következés áll fenn ($R'\kov R$).

Az olyan visszavezetést, ahol a programozási tétel előfeltételénél
a kitűzött feladat előfeltétele erősebb vagy/és az utófeltétele gyengébb,
\emph{általánosított visszavezetés}nek nevezzük.

\begin{stuki}
  \stm{p:=n}
  \begin{WHILE}{1}{\stm{\nem\text{prím}(p)}}
    \stm{p:=p+1}
  \end{WHILE}
\end{stuki}

\end{document}