At step 11 of the definition of extmul (below image), there is an expression $\text{imul}_{t_2 \times N}(k_1^*, k_2^*)$.
First solution
I guess it should be $\text{imul}_{|t_2|} (k_1^*, k_2^*)$.
The underscored argument of $\text{imul}$, which is $t_2 \times N$ is typed wrong. From the definition of $\text{imul}$, its argument should be an integer.
Here, from line 12, $k^*$ should be a sequence of length $N$ with its elements typed $t_2$. So I think the argument should be $|t_2|$.
Same problem occurs in the definition of extadd (below image).
I think the expression $\text{iadd}_N(j_1, j_2)^*$ at step 6 should be $\text{iadd}_{|t_2|} (j_1, j_2)^*$ instead, and fixed the document.
Second solution
Another solution (which I'm not so sure of) could be using the lane-wise applying notation.
With this notation, $\text{lanes}_{t_2 \times N}^{-1}(\text{imul}_{t_2 \times N} (k_1^*, k_2^*))$ from extmul can be replaced by $\text{mul}_{t_2 \times N} (k_1^*, k_2^*)$, and $\text{lanes}_{t_2 \times N}^{-1}(\text{iadd}_N(j_1, j_2)^*)$ from extadd by $\text{add}_{t_2 \times N}(j_1, j_2)^*$.
I'm not sure about the second solution nor which one is better, so I applied the first one to the document for now.
At step 11 of the definition of extmul (below image), there is an expression $
\text{imul}_{t_2 \times N}(k_1^*, k_2^*)$.First solution
I guess it should be $
Here, from line 12, $
I think the expression $
\text{imul}_{|t_2|} (k_1^*, k_2^*)$. The underscored argument of $\text{imul}$, which is $t_2 \times N$ is typed wrong. From the definition of $\text{imul}$, its argument should be an integer.k^*$ should be a sequence of length $N$ with its elements typed $t_2$. So I think the argument should be $|t_2|$. Same problem occurs in the definition of extadd (below image).\text{iadd}_N(j_1, j_2)^*$ at step 6 should be $\text{iadd}_{|t_2|} (j_1, j_2)^*$ instead, and fixed the document.Second solution
Another solution (which I'm not so sure of) could be using the lane-wise applying notation.
With this notation, $
\text{lanes}_{t_2 \times N}^{-1}(\text{imul}_{t_2 \times N} (k_1^*, k_2^*))$ from extmul can be replaced by $\text{mul}_{t_2 \times N} (k_1^*, k_2^*)$, and $\text{lanes}_{t_2 \times N}^{-1}(\text{iadd}_N(j_1, j_2)^*)$ from extadd by $\text{add}_{t_2 \times N}(j_1, j_2)^*$.I'm not sure about the second solution nor which one is better, so I applied the first one to the document for now.