equal
deleted
inserted
replaced
397 defined as the datatype |
397 defined as the datatype |
398 |
398 |
399 \begin{center} |
399 \begin{center} |
400 \begin{tabular}{rcll} |
400 \begin{tabular}{rcll} |
401 @{text "o"} & $::=$ & @{term "Inc R"} & increment register $R$ by one\\ |
401 @{text "o"} & $::=$ & @{term "Inc R"} & increment register $R$ by one\\ |
402 & $\mid$ & @{term "Dec R o"} & if content of $R$ is non-zero, then decrement it by one\\ |
402 & $\mid$ & @{term "Dec R n"} & if content of $R$ is non-zero, then decrement it by one\\ |
403 & & & otherwise jump to opcode $o$ |
403 & & & otherwise jump to opcode $o$\\ |
404 & $\mid$ & @{term "Goto o"} & jump to opcode $o$ |
404 & $\mid$ & @{term "Goto n"} & jump to opcode $o$ |
405 \end{tabular} |
405 \end{tabular} |
406 \end{center} |
406 \end{center} |
407 *} |
407 *} |
408 |
408 |
409 |
409 |