\documentclass[a4paper]{article}
\usepackage{progm}
\analpacks
\analoldal{1. feladatsor, 24-25. feladat}
\newcommand{\db}{\text{db}}
\newcommand{\szj}{\text{szj}}
\renewcommand{\div}{\mathop{\text{ div }}}
\begin{document}
\noindent
\emph{Feladat:} Határozzuk meg az $x$ természetes szám decimális alakja számjegyeinek számát!

\emph{Feladat:} Határozzuk meg az $x$ természetes szám decimális alakja számjegyeinek összegét!

\emph{Specifikáció:}\\
$A = \alatt{\N}{x} \times \alatt{\N}{s} \times \alatt{\N}{d}$\\
$B = \alatt{\N}{x'}$\\
$Q = ( x=x' )$\\
$R = ( Q \es s = \sum\limits_{i=1}^{\db(x)} \szj(x,i) \es d = \db(x))$

Ahol a db függvény megadja egy természetes szám számjegyeinek a
számát, míg az szj függvény megadja egy természetes szám számjegyei
közül hátulról számolva az $i$-ediket.

Formálisan:\\
$\db:\N\to\N, db(x):=\lfloor\log_{10}(x)\rfloor+1$ \\
$\szj:\N\times\N\to[0..9], \D_\szj:=\{(x,i)\in\N\times\N\mathop{|} i\le \db(x)\}, \szj(x,i):=(x \div 10^{i-1}) \bmod 10$ 

Látható, hogy a két feladatot egyszerre úgy oldjuk meg, hogy az $s$
változóba számoljuk ki a számjegyek összegét, a $d$-be pedig a
számjegyek számát.

\emph{Megoldás:}\\
$P = ( Q \es d\in[0,\db(x)] \es y=(x\div 10^d) \es s=\sum\limits_{i=1}^d \szj(x,i))$

\cklegy\\
$Q' = (Q \es d=s=0 \es y=x)$

\cklketto\\
$\nem\pi = (d=\db(x))$, de vegyük észre, hogy $(P \es d=\db(x)) \ekv (P \es y=x\div10^{\db(x)}=0)$, így $\nem\pi=(y=0)$ is jó.

\cklharom\\
Az előző pont észrevételével: $t:=y$.

\cklnegyot\\
$P\es\pi\es y=t_0 = (Q \es d\in[0,\db(x)-1] \es 0\ne y=(x\div 10^d) \es s=\sum\limits_{i=1}^d \szj(x,i) \es y=t_0) \kovkerdes$ \\
$\kovkerdes \lf(y,s,d:=y \div 10, s+(y \bmod 10), d+1, P \es y<t_0) = $ \\
$ = ( Q \es d+1\in[0,\db(x)] \es y\div 10=(x\div 10(10^d)) \es s+(y\bmod 10)=\sum\limits_{i=1}^{d+1} \szj(x,i) \es y\div 10<t_0) \surd$

A következés a db és szj definiciójából és egyszerű behelyettesítésekből adódik.

\begin{stuki}
  \stm{d,s,y:=0,0,x}
  \begin{WHILE}{1}{\stm{y \ne 0}}
    \stm{y,s,d:=y\div 10, s+(y\bmod 10), d+1}
  \end{WHILE}
\end{stuki}
\begin{textblock}{1}(2.4,-1.27)
$Q$
\vspace{0.2cm}\\$Q'$
\vspace{0.85cm}\\$R$
\end{textblock}
\begin{textblock}{1}(10.4,-0.57)
$P \es \pi$
\vspace{0.2cm}\\$P$
\end{textblock}

\end{document}