% -*- coding: iso-8859-2 -*-
\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{1. feladatsor, 13. feladat}
\newcommand{\trans}{\text{trans}}
\begin{document}
\noindent
\emph{Feladat:} Adott a $t$ négyzetes mátrix.  Tükrözzük (transzponáljuk) a főátlójára helyben (azaz az eredmény
$t$-ben keletkezzen)!

\emph{Használt mátrixtípus:}\\
$\M = \vect(\Z, \vect(\Z,\Z))$, invariánsa: $I(x) = (\forall i\in[x.lob,x.hib]: x_i.lob = x.lob \es x_i.hib = x.hib)$

\emph{Jelölés (feltéve, hogy $t$ és $t'$ $\M$ típusú, $k\in [t.lob, t.hib], l\in[t.lob, k]$):}
\[
\begin{array}{rcl}
t=\trans(t', k, l) & \ekv &
\begin{array}{l}
\text{i.) }t'.hib=t.hib \es t'.lob=t.lob \\
\text{ii.) }\forall i\in[t.lob, k-1]:\forall j\in[t.lob, k-1]: {t_i}_j={t'_j}_i \\
\text{iii.) }\forall j\in[t.lob, l-1]:{t_k}_j={t'_j}_k \es {t_j}_k = {t'_k}_j \\
\text{iv.) }\forall j\in[l, k]:{t_k}_j={t'_k}_j \es {t_j}_k = {t'_j}_k \\
\text{v.) }\forall i\in[k+1, t.hib]:\forall j\in[t.lob, k]: {t_i}_j={t'_i}_j \\
\text{vi.) }\forall i\in[t.lob, k]:\forall j\in[k+1, t.hib]: {t_i}_j={t'_i}_j \\
\text{vii.) }\forall i\in[k+1, t.hib]:\forall j\in[k+1, t.hib]: {t_i}_j={t'_i}_j
\end{array}
\end{array}
\]

\emph{Specifikáció:}\\
$A = \alatt{\M}{t}$\\
$B = \alatt{\M}{t'}$\\
$Q = (t=t')$\\
$R = (t=\trans(t', t.hib, t.hib))$

\emph{Megoldás:}\\
$A' = \alatt{\M}{t} \times \alatt{\Z}{k} \times \alatt{\Z}{l}$\\
$P  = (k\in [t.lob,t.hib] \es t=\trans(t', k, k))$\\
\cklegy: $Q'=(k=t.lob)$ \\
\cklketto: $\nem\pi = (k=t.hib)$ \\
\bigskip 3. \fbox{$P \es \pi \kov t^*>0$}: $t^*:=t.hib-k$ \\
\bigskip 4. \fbox{$P \es \pi \es t^*=t_0 \kov \lf(S_0, P \es t^*<t_0)$}: egy szekvenciával, aminek első fele egy újabb ciklus:\\
$Q_b = (P \es \pi \es t^*=t_0) = (t^*=t_0 \es k\in [t.lob,t.hib-1] \es t=\trans(t', k, k))$\\
$R_b = (k\in [t.lob,t.hib-1] \es t=\trans(t', k+1, k+1) \es t^*=t_0)$\\
$P_b = (k\in [t.lob,t.hib-1] \es l\in[t.lob, k+1] \es t=\trans(t', k+1, l) \es t^*=t_0)$\\
$Q'_b = (k\in [t.lob,t.hib-1] \es l=t.lob \es t=\trans(t', k+1, t.lob) \es t^*=t_0)$\\
$\pi_b = (l \ne k+1)$\\
$t^*_b = (t.hib - l)$\\
$Q''_b = (k\in [t.lob,t.hib-1] \es l\in[t.lob, k] \es t=\trans(t', k+1, l+1) \es t^*=t_0 \es t^*_b={t^*_b}_0)$\\
\begin{stuki}[13cm]
  \stm{k:=t.lob}
  \begin{WHILE}{5}{\stm{k \ne t.hib}}
    \stm{l:=t.lob}
    \begin{WHILE}{2}{\stm{l \ne k+1}}
      \stm{{t_l}_k,{t_k}_l:={t_k}_l,{t_l}_k}
      \stm{l:=l+1}
    \end{WHILE}
    \stm{k:=k+1}
  \end{WHILE}
\end{stuki}
\begin{textblock}{3}(11.5,-2.59)
$Q$
\vspace{0.2cm}\\$Q'$
\vspace{0.2cm}\\$Q_b$
\vspace{0.2cm}\\$Q'_b$
\vspace{0.2cm}\\$P_b \es \pi_b \es t^*_b = {t^*_b}_0$
\vspace{0.2cm}\\$Q''_b$
\vspace{0.2cm}\\$R_b$
\vspace{0.2cm}\\$R$
\end{textblock}
\end{document}