Difference between ⫾ (U+2AFE) and ⫿ (U+2AFF) in the context of Dijkstra's Guarded Command Language?

Continuing https://tex.stackexchange.com/questions/435986/how-to-draw-the-box-of-dijkstras-guarded-command-language, what is the difference in the intended usage of ⫾ (Dijkstra choice, U+2AFE) and ⫿ (n-ary Dijkstra choice, U+2AFF) in the context of the Guarded Command Language (GCL) of Dijkstra? In other words, when do you use ⫾ and when ⫿ for typesetting GCL programs?

Related:

-
http://latex.org/forum/viewtopic.php?t=32939

-
Barbara's take on GCL

Non-deterministic guarded choice is an associative-commutative binary operator. My guess is that the character ⫾ U+2AFE is intended to be used as an infix binary operator and the character ⫿ U+2AFF, which is larger and described as “n-ary”, is intended to be used as a prefix operator which is typeset larger, in prefix position, and typically with a subscript and sometimes a superscript to indicate the range over which the operation is carried out.

$$⫿_{i=1}^n c_i \rightarrow a_i \qquad = \qquad \mathsf{if}\; c_1 \rightarrow a_1 ⫾ \cdots ⫾ c_n \rightarrow a_n \;\mathsf{fi}$$

Typeset with inline math: $⫿_{i=1}^n c_i \rightarrow a_i = \mathsf{if}\; c_1 \rightarrow a_1 ⫾ \cdots ⫾ c_n \rightarrow a_n \;\mathsf{fi}$

It's the same relationship as between $+$ (binary) and $\sum$ (n-ary), or between $\times$ (binary) and $\prod$ (n-ary) ($\prod$ is sometimes a different product such as $\cdot$). For binary operators other than the two classics addition and multiplication, the n-ary version is the same glyph, just bigger.

StackExchange Computer Science Q#115967, answer score: 3