"In some cases, ellipses may be used in inference rules to handle an
arbitrary number of judgments."
    s/may be/are/

    To only talk about an arbitrary number of *judgments* gives a limited
    view of the role of ellipses. An ellipsis can also be used *within* a
    judgment to match an arbitrary number of syntactic objects (usually,
    items in some kind of list construct).

    For instance, consider 4.1.5 / Norm / rule 1. The three ellipses there
    are not about expanding the number of judgments in the rule; every
    different "version" of the rule has four judgments.  Instead, two of
    the judgments have a varying number of patterns.

    Ellipses are also used in a different sense in
        7.1.5 / STA / rule 1
        7.1.6 / STA / rule 1

"some of the patterns may have indices as subscript."
    s/subscript/subscripts/

    It's not clear what you mean by indices/index. E.g., in
        Expr1, ..., Exprn
    the '1' and 'n' are both subscripts, but are they both indices? Or is
    only the 'n' an index?  If the latter, it might be more
    self-explanatory to use a term like "symbolic subscript" or
    "non-numeric subscript", e.g. "some of the patterns may have symbolic
    subscripts".

"the number of judgment"
    s/judgment/judgments/

"for any number of expressions, from Expr1 to Exprn,"
    Delete "from".

"an unbounded number of rules, the first of which has 1 judgment"

    Actually, the first has 4 judgments, the second has 5, etc.
    You could say:
        the first of which has 1 judgment of the form
        'StatEnv |- Expri: Type', the second of which has 2, etc.

    You should probably note that in some cases, an ellipsis can generate
    (must be allowed to generate) zero judgments, or zero patterns. E.g.,
        5.11 / Notation 2 / rule 1
        4.7.1 / Norm / rule 4

    However, in about 10 places, the 2006-06 CR pulls out the "zero"
    version of a rule-with-ellipses and redundantly presents it as a
    separate rule (e.g., 4.1.5 / STA / rule (1|2)).  The Revision Log
    (G.3) doesn't mention these changes, so I'm left to wonder why. It
    seems like a waste of time and attention.

    (Whenever I see such a pair of rules, I immediately wonder, "Is the
    n=0 rule just a degenerate version of the n>0 rule, or does it
    actually require something special?", and I start picking through the
    rules to see which it is. It seems pointless to make readers do that
    when it *is* just a degenerate version of a general rule.)

"When ellipses are used, the value for the index always ranges from 1 to
an arbitrary number n."
    Usually, but not always. Here are some other examples:
        0 to n-1 (4.7.3.1 / Notation / rule 2)
        1 to n+1 (4.12.2 / STA / rule 1 / conclusion)
        1 to m   (5.11 / Notation 2 / rule 1)
        2 to n   (5.11 / Notation 3 / rule 2 / premise 2)
        2 to k   (5.11 / Notation 3 / rule 4 / premise 2)
        1 to k   (5.11 / Notation 3 / rule 4 / conclusion)
    The first example also demonstrates that within a single ellipsis,
    the subscripts-that-vary within a given judgment need not all have the
    same value.