equal
deleted
inserted
replaced
495 $(r_1 + r_2) \cdot r_3 \longrightarrow (r_1 \cdot r_3) + (r_2 \cdot r_3)$, |
495 $(r_1 + r_2) \cdot r_3 \longrightarrow (r_1 \cdot r_3) + (r_2 \cdot r_3)$, |
496 |
496 |
497 |
497 |
498 |
498 |
499 |
499 |
500 \section{The NTIMES Constructor, and the Size Bound and Correctness Proof for it} |
500 \section{The NTIMES Constructor, and the Size Bound and Correctness Proof for it} |
501 The NTIMES construct has the following closed form: |
501 The NTIMES construct has the following closed form: |
502 \begin{verbatim} |
502 \begin{verbatim} |
503 "rders_simp (RNTIMES r0 (Suc n)) (c#s) = |
503 "rders_simp (RNTIMES r0 (Suc n)) (c#s) = |
504 rsimp ( RALTS ( (map (optermsimp r0 ) (nupdates s r0 [Some ([c], n)]) ) ))" |
504 rsimp ( RALTS ( (map (optermsimp r0 ) (nupdates s r0 [Some ([c], n)]) ) ))" |
505 \end{verbatim} |
505 \end{verbatim} |