4.7.3.5 Computed Processing Instruction Constructors

Norm / rule (2|3)
fs:item-sequence-to-untypedAtomic-PI( [[ Expr ]]_Expr )
    This function takes a single argument (of type item*), but
    [[ Expr ]]_Expr could result in a sequence of comma-separated
    ExprSingles, which would then constitute multiple args.
    Put [[ Expr ]]_Expr in parentheses to ensure a single arg.

Norm / rule (2|3)
fn:data( [[ Expr1 ]]_Expr )
    Ditto the above. Add parentheses to ensure a single arg.

DEv / rule 3 / premise 3
"xs:NCName(Value1); =>"
    Delete semicolon.

DEv / rule (2|3|4) / premise 3
"dynEnv |- xs:NCName(Value1) => NCName1"
    I don't think you need dynEnv for this.  Change to:
        NCName1 = xs:NCName(Value1)

DEv / rule (2|3|4)
    These three rules differ only in premise 2. Couldn't you combine them
    into one rule, with:
        statEnv |- Value1 matches (xs:NCName|xs:string|xdt:untypedAtomic)
    as its premise 2?