\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{2. feladatsor, 13. feladat}
\begin{document}
\noindent
\emph{Feladat:} Keressünk az $[a..b]$ intervallumban ikerprímeket!
Feltehetjük, hogy $a>2$.

\emph{Specifikáció:}\\
$A = \alatt{\N}{a} \times \alatt{\N}{b} \times \alatt{\L}{l} \times \alatt{\N}{p}$\\
$B = \alatt{\N}{a'} \times \alatt{\N}{b'}$\\
$Q = ( a=a' \es b=b' \es a\le b-1 \es a> 2)$\\
$R = ( Q \es l=(\exists i\in[a..b-2]: (\text{prím}(i) \es \text{prím}(i+2))) \es 
l\nyil (p\in[a..b-2]\es \text{prím}(p) \es \text{prím}(p+2)))$

Ha az utófeltétel második alakját vesszük figyelembe, akkor 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
  $\text{prím}(i)\es \text{prím}(i+2)$ & \knyil & $\beta(i)$ \\
  $p$ & \knyil & $i$ & \\
  $a$ & \knyil & $m$ & \\
  $b-2$ & \knyil & $n$ &
\end{tabular}

A visszavezetés általánosított, hiszen az előfeltétel az intervallumok
tekintetében szigorúbb a feladatban, míg az utófeltétel gyengébb a
feladatban, mint a tételben (mi nem követeljük meg, hogy az első
ikerprímet találja meg a program).

\begin{stuki}
  \stm{p,l:=a-1,\hamis}
  \begin{WHILE}{2}{\stm{\nem l \es p \ne b-2}}
    \stm{l:=\text{prím}(p+1)\es\text{prím}(p+3)}
    \stm{p:=p+1}
  \end{WHILE}
\end{stuki}

A megoldásban szereplő $l:=\text{prím}(p+1)\es\text{prím}(p+3)$
értékadást egy új feladatként is megfogalmazhatjuk: állapítsuk meg egy
$p$ számról, hogy ő maga és a nála kettővel nagyobb szám prím-e!  Ez a
feladat az eredeti állapottér egy alterén specifikálható:

$A' = \alatt{\L}{l} \times \alatt{\N}{p}$\\
$B' = \alatt{\N}{p'}$\\
$Q' = ( p=p' \es p> 2)$\\
$R' = ( Q \es l=(\forall i\in[2..p-1]: (\nem(i|p) \es \nem(i|(p+2)))))
= ( Q \es \nem l=(\exists i\in[2..p-1]: (i|p \vagy i|(p+2))))$

Ez visszavezethető a lin. ker. 2.8-ra.  A visszavezetés az alteres
visszavezetés mindkét esetével összeegyeztethető (hiszen az
intervallum kezdetét konstanssal helyettesítettük, ugyanakkor a tétel
$i$ eredménykomponensét nem használtuk a specifikációban).  A
visszavezetés általános is, mivel mi a $2$ konstanssal, mint
intervallum elejével és a $p-1\ge2$ kifejezéssel, mint intervallum
végével az üres intervallum feldolgozását kizártuk az előfeltételben,
így az szigorúbb a tétel előfeltételénél.

\begin{tabular}{cccr}
  feladat &  & lin. ker. 2.8 \\
  \hline
  $i|p \vagy i|(p+2)$ & \knyil & $\beta(i)$ \\
  $\nem l$ & \knyil & $l$ \\
  $2$ & \knyil & $m$ \\
  $p-1$ & \knyil & $n$ 
\end{tabular}

\begin{textblock}{1}(0,0)
\begin{stuki*}[6cm]{l:=\text{prím}(p) \es \text{prím}(p+2)}
  \stm{i,l:=1,\igaz}
  \begin{WHILE}{2}{\stm{l \es i \ne p-1}}
    \stm{l:=\nem(i+1)|p \es \nem(i+1)|(p+2)}
    \stm{i:=i+1}
  \end{WHILE}
\end{stuki*}
\end{textblock}

\begin{textblock}{1}(5,-1.5)
\begin{stuki}
  \stm{p,l:=a-1,\hamis}
  \begin{WHILE}{5}{\stm{\nem l \es p \ne b-2}}
    \stm{i,l:=1,\igaz}
    \begin{WHILE}{2}{\stm{l \es i \ne p-1}}
      \stm{l:=\nem(i+1)|(p+1) \es \nem(i+1)|(p+3)}
      \stm{i:=i+1}
    \end{WHILE}
    \stm{p:=p+1}
  \end{WHILE}
\end{stuki}
\end{textblock}



\end{document}