

\input menv
\input stuki

\newdimen\conspace\conspace=2pt
\newdimen\spspace\spspace=4pt
\def\con#1{\vskip\conspace\item{}#1\vskip\conspace}
\def\conp#1#2{\vskip\conspace\item{#1}#2\vskip\conspace}

\newcount\spsw\spsw=0
\def\var(#1:#2){\ifodd\spsw{$\times $}\else{\global\spsw=1}\fi
            {\baselineskip 9pt\vtop{\hbox{#1}\hbox{$#2$}}}}
\def\sp#1{\vskip\spspace\global\spsw=0\item{}$#1=$}
\def\edef{\mathrel{\mathop=^{{\fiverm def}}}}

\font\kiscimf=cmbx10
\font\kiemf=cmssqi8
\newcount\tetelc\tetelc=0
\newcount\altetelc\altetelc=0
\newcount\alaltetelc\alaltetelc=0
\def\tetel#1{\advance\tetelc by 1 \altetelc = 0 \alaltetelc = 0
             \vskip 2mm
             \leftline{{\kiscimf\number \tetelc .\enskip #1}}
             \vskip 1.2 mm}

\def\altetel#1{\advance\altetelc by 1 \alaltetelc = 0
               \vskip 1.2mm
               \leftline{{\kiscimf\number\tetelc .\number\altetelc .\enskip #1}}
               \vskip 1.2mm}

\def\alaltetel#1{\advance\alaltetelc by 1
                 \vskip .8mm
                 \leftline{{\kiscimf\number\tetelc .\number\altetelc .\number\alaltetelc .\enskip #1}}
                 \vskip 1.2mm}


% ---- [m..n] u { m - 1 } ----
\def\mn{ [ m .. n ] \cup \{ m - 1 \} }

\cim{M\'atrixt\"ukr\"oz\'es a mell\'ek\'atl\'ora}
\bigskip\noindent

{\bf A feladat specifik\'aci\'oja:}
\bigskip\noindent
Legyen $\M: vekt(\N,vekt(\N,\R))$ \'es 
\hfill\break
${\M}^\prime=\{m\in \M | \forall j \in 
                                   [m.lob..m.hib]:m_j.lob=m.lob \land m_j.hib=m.hib\}$

\sp{A}\var(${\M^\prime}$:m)
\sp{B}\var(${\M^\prime}$:{m^\prime})
\medskip

\con{$Q:\bigl(m=m^\prime \bigr)$}
\con{$R:\bigl(\forall i \in [m.lob..m.hib]: \forall j \in [m.lob..m.hib]: 
\nl
m^\prime_{ij} = m_{(m.hib-(j-m.lob))(m.hib-(i-m.lob))} \land
\nl
        \land\ m^\prime.lob=m.lob \land m^\prime.hib=m.hib
 \bigr)$}
\medskip

Keress\"uk a megold\'ast ad\'o programot {\bf ciklus} form\'aban, ahol

\con{$P:\bigl(k\in [m.lob..m.hib+1]\land 
\nl
   \land\ \forall i \in [k..m.hib]: \forall j \in [m.lob..m.lob+(m.hib-k)]:
\nl 
m^\prime_{ij} = m_{(m.hib-(j-m.lob))(m.hib-(i-m.lob))} \land
\nl
   \land\ \forall (i,j) \in [m.lob..m.hib]\times[m.lob..m.hib]\setminus
\nl
\setminus[k..m.hib]\times[m.lob..m.lob+(m.hib-k)]:
\nl
 m^\prime_{ij} = m_{ij} \land 
        \land\ m^\prime.lob=m.lob \land m^\prime.hib=m.hib
	\bigr)$}
\bigskip

\itemitem{1.}$Q\not\Rightarrow P$, de $Q\Rightarrow P^{k\leftarrow m.hib+1}$.
\nl
Innen ad\'odik, hogy
\nl
$Q\Rightarrow\lf(k:=m.hib+1,\ P)$
\itemitem{2.} A ciklus levezet\'esi szab\'alya m\'asodik felt\'etele:
\hfill\break
$P\land\neg\pi \Rightarrow R$
\hfill\break
teljes\"ul, ha $\neg\pi:\ (k\le m.lob)$.
\nl
Ez\'ert $\pi:\ (k> m.lob)$ alkalmas v\'alaszt\'as.
\itemitem{3.} A ciklus levezet\'esi szab\'alya harmadik felt\'etele:
\hfill\break
$P\land\pi \Rightarrow t > 0$
\hfill\break
teljes\"ul, ha $t:\ k-m.lob$
\hfill\break
a $\pi$ v\'alaszt\'asa miatt.
\itemitem{4.} \'es 5. Bel\'athat\'o, hogy
\hfill\break
$P\land k> m.lob \Rightarrow \lf(S^1_0,\ P^{k\leftarrow k-1})$
\hfill\break
eset\'en a $(S^1_0;k:=k-1)$ program alkalmas ciklusmag.
%\hfill\break
\vfill\eject
Legyen
\con{$\overline P:\bigl(k\in [m.lob..m.hib+1]\land k> m.lob \land l\in [m.lob-1..m.lob+(m.hib-(k-1)] \land
\nl
   \land\ \forall i \in [k..m.hib]: \forall j \in [m.lob..m.lob+(m.hib-k)]:
\nl 
m^\prime_{ij} = m_{(m.hib-(j-m.lob))(m.hib-(i-m.lob))} \land
\nl
   \land\ \forall i \in [m.lob..l]:
\nl
 (m^\prime_{k-1i} = m_{(m.hib-(i-m.lob))(m.hib-((k-1)-m.lob)} \land
\nl
\land\ m^\prime_{(m.hib-(i-m.lob))(m.hib-((k-1)-m.lob)} = m_{k-1i}) \land
\nl
   \land\ \forall (i,j) \in ([m.lob..m.hib]\times[m.lob..m.hib]\setminus
\nl
\setminus([k..m.hib]\times[m.lob..m.lob+(m.hib-k)]\cup 
\{k-1\}\times[m.lob..l]\cup
\nl
\cup [m.hib-(l-m.lob)..m.hib]\times\{m.hib-(k-1-m.lob)\})):
\nl
 m^\prime_{ij} = m_{ij} \land 
\nl
        \land\ m^\prime.lob=m.lob \land m^\prime.hib=m.hib
\bigr)$}
\nl
Ekkor
\nl
$P\land k> m.lob \Rightarrow \overline P^{l\leftarrow m.lob-1}$
\nl
$\overline P\land \neg\overline\pi \Rightarrow P^{k\leftarrow k-1}$ teljes\"ul, ha
\nl
$\neg\overline\pi:\ l\ge m.lob+(m.hib-(k-1)$, teh\'at $\overline\pi: l<m.lob+(m.hib-(k-1)$ alkalmas v\'alaszt\'as.
\nl
$\overline P\land \overline\pi \Rightarrow \overline t > 0$ teljes\"ul, ha $\overline t:\ m.lob+(m.hib-(k-1)-l$.
\nl
L\'athat\'o, hogy
\nl
$\overline P\land \overline\pi \Rightarrow 
\nl
\bigl(k\in [m.lob..m.hib+1]\land k> m.lob \land l+1\in [m.lob-1..m.lob+(m.hib-(k-1)] \land
\nl
   \land\ \forall i \in [k..m.hib]: \forall j \in [m.lob..m.lob+(m.hib-k)]:
\nl 
m^\prime_{ij} = m_{(m.hib-(j-m.lob))(m.hib-(i-m.lob))} \land
\nl
   \land\ \forall i \in [m.lob..l]:
\nl
 (m^\prime_{k-1i} = m_{(m.hib-(i-m.lob))(m.hib-((k-1)-m.lob)} \land
\nl
\land\ m^\prime_{(m.hib-(i-m.lob))(m.hib-((k-1)-m.lob)} = m_{k-1i}) \land
\nl
\land\ m^\prime_{(k-1)(l+1)}=m_{(k-1)(l+1)}\land
\nl
\land\ m^\prime_{(m.hib-((l+1)-m.lob))(m.hib-((k-1)-m.lob))}=m_{(m.hib-((l+1)-m.lob))(m.hib-((k-1)-m.lob))}\land
\nl
   \land\ \forall (i,j) \in ([m.lob..m.hib]\times[m.lob..m.hib]\setminus
\nl
\setminus([k..m.hib]\times[m.lob..m.lob+(m.hib-k)]\cup 
\{k-1\}\times[m.lob..(l+1)]\cup
\nl
\cup [m.hib-((l+1)-m.lob)..m.hib]\times\{m.hib-(k-1-m.lob)\})):
\nl
 m^\prime_{ij} = m_{ij} \land 
\nl
        \land\ m^\prime.lob=m.lob \land m^\prime.hib=m.hib
\bigr)$
\nl
%Ez\'ert
%\nl
%$\overline P\land \overline\pi \Rightarrow 
%\nl
%{\overline P^{l\leftarrow l+1}}^{m_{k-1,l+1},m_{(m.hib-(l+1-m.lob)),(m.hib-(k-1-m.lob}\leftarrow m_{(m.hib-(l+1-m.lob)),(m.hib-(k-1-m.lob},m_{k-1,l+1}}$ 
%\nl
Teh\'at
\nl
$\overline P\land \overline\pi \Rightarrow \lf(\overline{S}^1_0,\ \overline{P}^{l\leftarrow l+1})$
\nl
teljes\"ul, ha
\nl
 $\overline{S}^1_0:\ m_{k-1,l+1},m_{(m.hib-(l+1-m.lob)),(m.hib-(k-1-m.lob}:=
\nl
 m_{(m.hib-(l+1-m.lob)),(m.hib-(k-1-m.lob},m_{k-1,l+1}$
\bigskip

Egy lehets\'eges megold\'as teh\'at a k\"ovetkez\H o program:

\bigskip
\centerline{
\loopindent=90
\STRUC 320pt :
     \Stm $k:=m.hib+1$;
     \Rule
     \WHILE \Stm $k> m.lob$; DO
        \Stm $l:=m.lob-1$;
        \Rule
        {
        \WHILE \Stm $l < m.lob+(m.hib-(k-1)$; DO
           \Stm $m_{(k-1)(l+1)},m_{(m.hib-((l+1)-m.lob))(m.hib-((k-1)-m.lob))}:=$;
           \Stm $\ m_{(m.hib-((l+1)-m.lob))(m.hib-((k-1)-m.lob))},m_{(k-1)(l+1)}$;
         \Rule
           \Stm $l:=l+1 $;
        \ENDDO
         }
        \Rule
        \Stm $ k := k-1$;
     \ENDDO
\END. }


\end
