equal
deleted
inserted
replaced
608 |
608 |
609 \begin{tikzpicture}[scale=0.7] |
609 \begin{tikzpicture}[scale=0.7] |
610 \node [anchor=base] at (2.2,0.1) {\small$\Rightarrow$}; |
610 \node [anchor=base] at (2.2,0.1) {\small$\Rightarrow$}; |
611 \node [anchor=base] at (5.6,0.1) {\small$\Rightarrow$}; |
611 \node [anchor=base] at (5.6,0.1) {\small$\Rightarrow$}; |
612 \node [anchor=base] at (10.5,0.1) {\small$\Rightarrow$}; |
612 \node [anchor=base] at (10.5,0.1) {\small$\Rightarrow$}; |
613 \node [anchor=base] at (2.2,-0.6) {\small$\overbrace{@{term "tcopy_init"}}^{}$}; |
613 \node [anchor=base] at (2.2,-0.6) {\small$\overbrace{@{term "tcopy_begin"}}^{}$}; |
614 \node [anchor=base] at (5.6,-0.6) {\small$\overbrace{@{term "tcopy_loop"}}^{}$}; |
614 \node [anchor=base] at (5.6,-0.6) {\small$\overbrace{@{term "tcopy_loop"}}^{}$}; |
615 \node [anchor=base] at (10.5,-0.6) {\small$\overbrace{@{term "tcopy_end"}}^{}$}; |
615 \node [anchor=base] at (10.5,-0.6) {\small$\overbrace{@{term "tcopy_end"}}^{}$}; |
616 |
616 |
617 |
617 |
618 \begin{scope}[shift={(0.5,0)}] |
618 \begin{scope}[shift={(0.5,0)}] |