Paper/Paper.thy
changeset 142 21c7139ffa07
parent 141 4d7a568bd911
child 143 c56f04b6a2f9
equal deleted inserted replaced
141:4d7a568bd911 142:21c7139ffa07
  1158   use the letter @{text l}. An abacus 
  1158   use the letter @{text l}. An abacus 
  1159   program is a list of \emph{instructions} defined by the datatype:
  1159   program is a list of \emph{instructions} defined by the datatype:
  1160 
  1160 
  1161   \begin{center}
  1161   \begin{center}
  1162   \begin{tabular}{rcl@ {\hspace{10mm}}l}
  1162   \begin{tabular}{rcl@ {\hspace{10mm}}l}
  1163   @{text "i"} & $::=$  & @{term "Inc R\<iota>"} & increment register $R$ by one\\
  1163   @{text "i"} & $::=$  & @{term "Inc R\<iota>"} & increment register @{text "R"} by one\\
  1164   & $\mid$ & @{term "Dec R\<iota> l"} & if content of $R$ is non-zero, then decrement it by one\\
  1164   & $\mid$ & @{term "Dec R\<iota> l"} & if content of @{text R} is non-zero, then decrement it by one\\
  1165   & & & otherwise jump to instruction $l$\\
  1165   & & & otherwise jump to instruction @{text l}\\
  1166   & $\mid$ & @{term "Goto l"} & jump to instruction $l$
  1166   & $\mid$ & @{term "Goto l"} & jump to instruction @{text l}
  1167   \end{tabular}
  1167   \end{tabular}
  1168   \end{center}
  1168   \end{center}
  1169 
  1169 
  1170   \noindent
  1170   \noindent
  1171   For example the program clearing the register @{text R} (that is setting
  1171   For example the program clearing the register @{text R} (that is setting