diff --git a/spec.html b/spec.html
index 6569d451f5..6a6c7e4a90 100644
--- a/spec.html
+++ b/spec.html
@@ -4808,27 +4808,12 @@ Runtime Semantics: MV
The MV of StringNumericLiteral ::: StrWhiteSpace? StrNumericLiteral StrWhiteSpace? is the MV of |StrNumericLiteral|, no matter whether white space is present or not.
-
- The MV of StrNumericLiteral ::: StrDecimalLiteral is the MV of |StrDecimalLiteral|.
-
-
- The MV of StrNumericLiteral ::: NonDecimalIntegerLiteral is the MV of |NonDecimalIntegerLiteral|.
-
-
- The MV of StrDecimalLiteral ::: StrUnsignedDecimalLiteral is the MV of |StrUnsignedDecimalLiteral|.
-
-
- The MV of StrDecimalLiteral ::: `+` StrUnsignedDecimalLiteral is the MV of |StrUnsignedDecimalLiteral|.
-
The MV of StrDecimalLiteral ::: `-` StrUnsignedDecimalLiteral is the negative of the MV of |StrUnsignedDecimalLiteral|. (Note that if the MV of |StrUnsignedDecimalLiteral| is 0, the negative of this MV is also 0. The rounding rule described below handles the conversion of this signless mathematical zero to a floating-point *+0* or *-0* as appropriate.)
The MV of StrUnsignedDecimalLiteral ::: `Infinity` is 10ℝ10000ℝ (a value so large that it will round to *+∞*).
-
- The MV of StrUnsignedDecimalLiteral ::: DecimalDigits `.` is the MV of |DecimalDigits|.
-
The MV of StrUnsignedDecimalLiteral ::: DecimalDigits `.` DecimalDigits is the MV of the first |DecimalDigits| plus (the MV of the second |DecimalDigits| times 10ℝ-ℝ_n_), where _n_ is the mathematical value of the number of code points in the second |DecimalDigits|.
@@ -4844,9 +4829,6 @@ Runtime Semantics: MV
The MV of StrUnsignedDecimalLiteral ::: `.` DecimalDigits ExponentPart is the MV of |DecimalDigits| times 10ℝ_e_ -ℝ _n_, where _n_ is the mathematical value of the number of code points in |DecimalDigits| and _e_ is the MV of |ExponentPart|.
-
- The MV of StrUnsignedDecimalLiteral ::: DecimalDigits is the MV of |DecimalDigits|.
-
The MV of StrUnsignedDecimalLiteral ::: DecimalDigits ExponentPart is the MV of |DecimalDigits| times 10ℝ_e_, where _e_ is the MV of |ExponentPart|.
@@ -11460,12 +11442,6 @@ Static Semantics: SV
The SV of StringLiteral :: `'` `'` is the empty code unit sequence.
-
- The SV of StringLiteral :: `"` DoubleStringCharacters `"` is the SV of |DoubleStringCharacters|.
-
-
- The SV of StringLiteral :: `'` SingleStringCharacters `'` is the SV of |SingleStringCharacters|.
-
The SV of DoubleStringCharacters :: DoubleStringCharacter is a sequence of up to two code units that is the SV of |DoubleStringCharacter|.
@@ -11487,9 +11463,6 @@ Static Semantics: SV
The SV of DoubleStringCharacter :: <PS> is the code unit 0x2029 (PARAGRAPH SEPARATOR).
-
- The SV of DoubleStringCharacter :: `\` EscapeSequence is the SV of |EscapeSequence|.
-
The SV of DoubleStringCharacter :: LineContinuation is the empty code unit sequence.
@@ -11502,24 +11475,12 @@ Static Semantics: SV
The SV of SingleStringCharacter :: <PS> is the code unit 0x2029 (PARAGRAPH SEPARATOR).
-
- The SV of SingleStringCharacter :: `\` EscapeSequence is the SV of |EscapeSequence|.
-
The SV of SingleStringCharacter :: LineContinuation is the empty code unit sequence.
-
- The SV of EscapeSequence :: CharacterEscapeSequence is the SV of |CharacterEscapeSequence|.
-
The SV of EscapeSequence :: `0` is the code unit 0x0000 (NULL).
-
- The SV of EscapeSequence :: HexEscapeSequence is the SV of |HexEscapeSequence|.
-
-
- The SV of EscapeSequence :: UnicodeEscapeSequence is the SV of |UnicodeEscapeSequence|.
-
The SV of CharacterEscapeSequence :: SingleEscapeCharacter is the code unit whose value is determined by the |SingleEscapeCharacter| according to .
@@ -11671,18 +11632,12 @@ Static Semantics: SV
- -
- The SV of CharacterEscapeSequence :: NonEscapeCharacter is the SV of |NonEscapeCharacter|.
-
-
The SV of NonEscapeCharacter :: SourceCharacter but not one of EscapeCharacter or LineTerminator is the UTF16Encoding of the code point value of |SourceCharacter|.
-
The SV of HexEscapeSequence :: `x` HexDigit HexDigit is the code unit whose value is (16ℝ times the MV of the first |HexDigit|) plus the MV of the second |HexDigit|.
- -
- The SV of UnicodeEscapeSequence :: `u` Hex4Digits is the SV of |Hex4Digits|.
-
-
The SV of Hex4Digits :: HexDigit HexDigit HexDigit HexDigit is the code unit whose value is the MV of |Hex4Digits|.
@@ -11849,21 +11804,6 @@ Static Semantics: TV and TRV
-
The TV and TRV of TemplateTail :: `}` ``` is the empty code unit sequence.
- -
- The TV of NoSubstitutionTemplate :: ``` TemplateCharacters ``` is the TV of |TemplateCharacters|.
-
- -
- The TV of TemplateHead :: ``` TemplateCharacters `${` is the TV of |TemplateCharacters|.
-
- -
- The TV of TemplateMiddle :: `}` TemplateCharacters `${` is the TV of |TemplateCharacters|.
-
- -
- The TV of TemplateTail :: `}` TemplateCharacters ``` is the TV of |TemplateCharacters|.
-
- -
- The TV of TemplateCharacters :: TemplateCharacter is the TV of |TemplateCharacter|.
-
-
The TV of TemplateCharacters :: TemplateCharacter TemplateCharacters is *undefined* if either the TV of |TemplateCharacter| is *undefined* or the TV of |TemplateCharacters| is *undefined*. Otherwise, it is a sequence consisting of the code units of the TV of |TemplateCharacter| followed by the code units of the TV of |TemplateCharacters|.
@@ -11879,30 +11819,9 @@ Static Semantics: TV and TRV
-
The TV of TemplateCharacter :: `\` NotEscapeSequence is *undefined*.
- -
- The TV of TemplateCharacter :: LineContinuation is the TV of |LineContinuation|.
-
- -
- The TV of TemplateCharacter :: LineTerminatorSequence is the TRV of |LineTerminatorSequence|.
-
-
The TV of LineContinuation :: `\` LineTerminatorSequence is the empty code unit sequence.
- -
- The TRV of NoSubstitutionTemplate :: ``` TemplateCharacters ``` is the TRV of |TemplateCharacters|.
-
- -
- The TRV of TemplateHead :: ``` TemplateCharacters `${` is the TRV of |TemplateCharacters|.
-
- -
- The TRV of TemplateMiddle :: `}` TemplateCharacters `${` is the TRV of |TemplateCharacters|.
-
- -
- The TRV of TemplateTail :: `}` TemplateCharacters ``` is the TRV of |TemplateCharacters|.
-
- -
- The TRV of TemplateCharacters :: TemplateCharacter is the TRV of |TemplateCharacter|.
-
-
The TRV of TemplateCharacters :: TemplateCharacter TemplateCharacters is a sequence consisting of the code units of the TRV of |TemplateCharacter| followed by the code units of the TRV of |TemplateCharacters|.
@@ -11918,24 +11837,9 @@ Static Semantics: TV and TRV
-
The TRV of TemplateCharacter :: `\` NotEscapeSequence is the sequence consisting of the code unit 0x005C (REVERSE SOLIDUS) followed by the code units of TRV of |NotEscapeSequence|.
- -
- The TRV of TemplateCharacter :: LineContinuation is the TRV of |LineContinuation|.
-
- -
- The TRV of TemplateCharacter :: LineTerminatorSequence is the TRV of |LineTerminatorSequence|.
-
- -
- The TRV of EscapeSequence :: CharacterEscapeSequence is the TRV of |CharacterEscapeSequence|.
-
-
The TRV of EscapeSequence :: `0` is the code unit 0x0030 (DIGIT ZERO).
- -
- The TRV of EscapeSequence :: HexEscapeSequence is the TRV of |HexEscapeSequence|.
-
- -
- The TRV of EscapeSequence :: UnicodeEscapeSequence is the TRV of |UnicodeEscapeSequence|.
-
-
The TRV of NotEscapeSequence :: `0` DecimalDigit is the sequence consisting of the code unit 0x0030 (DIGIT ZERO) followed by the code units of the TRV of |DecimalDigit|.
@@ -11969,9 +11873,6 @@ Static Semantics: TV and TRV
-
The TRV of DecimalDigit :: one of `0` `1` `2` `3` `4` `5` `6` `7` `8` `9` is the UTF16Encoding of the single code point matched by this production.
- -
- The TRV of CharacterEscapeSequence :: SingleEscapeCharacter is the TRV of |SingleEscapeCharacter|.
-
-
The TRV of CharacterEscapeSequence :: NonEscapeCharacter is the SV of |NonEscapeCharacter|.
@@ -11990,9 +11891,6 @@ Static Semantics: TV and TRV
-
The TRV of Hex4Digits :: HexDigit HexDigit HexDigit HexDigit is the sequence consisting of the TRV of the first |HexDigit| followed by the TRV of the second |HexDigit| followed by the TRV of the third |HexDigit| followed by the TRV of the fourth |HexDigit|.
- -
- The TRV of HexDigits :: HexDigit is the TRV of |HexDigit|.
-
-
The TRV of HexDigits :: HexDigits HexDigit is the sequence consisting of TRV of |HexDigits| followed by TRV of |HexDigit|.
@@ -31357,18 +31255,6 @@ Static Semantics: CharacterValue
1. Let _cp_ be UTF16DecodeSurrogatePair(_lead_, _trail_).
1. Return the code point value of _cp_.
- RegExpUnicodeEscapeSequence :: `u` LeadSurrogate
-
- 1. Return the CharacterValue of |LeadSurrogate|.
-
- RegExpUnicodeEscapeSequence :: `u` TrailSurrogate
-
- 1. Return the CharacterValue of |TrailSurrogate|.
-
- RegExpUnicodeEscapeSequence :: `u` NonSurrogate
-
- 1. Return the CharacterValue of |NonSurrogate|.
-
RegExpUnicodeEscapeSequence :: `u` Hex4Digits
1. Return the Number value for the MV of |Hex4Digits|.