B.2 Mapping of Overloaded Internal Functions

STA
"The following static typing rules apply generically to all the fs:
special functions."
    This should be conveyed by the inference rules too. I.e., add
        expanded-QName = (FS-URI,String)
        String in {"plus","minus","times","idiv","div", ...}
    (directly or indirectly) to each rule.  (leftover from Bug 1580)

STA / rule 1
    The top set of premises is only satisfied if every Typei is a union of
    the same number (m) of OptAtomicTypes, which is not what you want.
    You could fix this by making the m's distinct:
        ... OptAtomicType<sub>m<sub>1</sub>,1</sub>
        ... OptAtomicType<sub>m<sub>n</sub>,1</sub>
    But then what would you do in the second set of premises?
    If you want the rule to consider all possible combinations of argument
    types, you probably need a recursive rule, e.g.

        Typei = (OptAtomicType1 | ... | OptAtomicTypem)
        statEnv |- expanded-QName(Type1, ..., OptAtomicType1, ..., Typen) :
            Type1'
        ...
        statEnv |- expanded-QName(Type1, ..., OptAtomicTypem, ..., Typen) :
            Typem'
        -----------------------------------------------
        statEnv |- expanded-QName(Type1, ..., Typen) : (Type1' |...| Typem')

    If you concede that the only possibilities are n=1 or n=2, you could
    split this rule into three simpler rules.

STA / rule (2|3|4|5|6|7) / conclusion
HTML source:
<em><a href="#id-expanded-qnames"><em>expanded-QName</em></a></em>
    Remove outer <em></em>.

STA / rule (4|5|6|8|9)
"AtomicType"
    AtomicType is a SequenceType, not a Formal Type. Instead,
    you probably mean AtomicTypeName, which *is* a Formal Type.

STA / rule 7
    The rule needs a premise: Type1 = empty

Notation 2 / rule (1|2)
"AtomicType"
    As above, change to AtomicTypeName.