diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst
index b4c15c8f31..2413b638f6 100644
--- a/document/core/appendix/properties.rst
+++ b/document/core/appendix/properties.rst
@@ -513,10 +513,10 @@ where :math:`\val_1 \gg^+_S \val_2` denotes the transitive closure of the follow
 .. index:: table type, table instance, limits, function address
 .. _valid-tableinst:
 
-:ref:`Table Instances <syntax-tableinst>` :math:`\{ \TITYPE~(\limits~t), \TIELEM~\reff^\ast \}`
-...............................................................................................
+:ref:`Table Instances <syntax-tableinst>` :math:`\{ \TITYPE~\idxtype~\limits~t, \TIELEM~\reff^\ast \}`
+......................................................................................................
 
-* The :ref:`table type <syntax-tabletype>` :math:`\limits~t` must be :ref:`valid <valid-tabletype>` under the empty :ref:`context <context>`.
+* The :ref:`table type <syntax-tabletype>` :math:`\idxtype~\limits~t` must be :ref:`valid <valid-tabletype>` under the empty :ref:`context <context>`.
 
 * The length of :math:`\reff^\ast` must equal :math:`\limits.\LMIN`.
 
@@ -526,11 +526,11 @@ where :math:`\val_1 \gg^+_S \val_2` denotes the transitive closure of the follow
 
   * The :ref:`reference type <syntax-reftype>` :math:`t'_i` must :ref:`match <match-reftype>` the :ref:`reference type <syntax-reftype>` :math:`t`.
 
-* Then the table instance is valid with :ref:`table type <syntax-tabletype>` :math:`\limits~t`.
+* Then the table instance is valid with :ref:`table type <syntax-tabletype>` :math:`\idxtype~\limits~t`.
 
 .. math::
    \frac{
-     \vdashtabletype \limits~t \ok
+     \vdashtabletype \idxtype~\limits~t \ok
      \qquad
      n = \limits.\LMIN
      \qquad
@@ -538,37 +538,37 @@ where :math:`\val_1 \gg^+_S \val_2` denotes the transitive closure of the follow
      \qquad
      (\vdashreftypematch t' \matchesvaltype t)^n
    }{
-     S \vdashtableinst \{ \TITYPE~(\limits~t), \TIELEM~\reff^n \} : \limits~t
+     S \vdashtableinst \{ \TITYPE~\idxtype~\limits~t, \TIELEM~\reff^n \} : \idxtype~\limits~t
    }
 
 
 .. index:: memory type, memory instance, limits, byte
 .. _valid-meminst:
 
-:ref:`Memory Instances <syntax-meminst>` :math:`\{ \MITYPE~\limits, \MIDATA~b^\ast \}`
-......................................................................................
+:ref:`Memory Instances <syntax-meminst>` :math:`\{ \MITYPE~\idxtype~\limits, \MIDATA~b^\ast \}`
+...............................................................................................
 
-* The :ref:`memory type <syntax-memtype>` :math:`\limits` must be :ref:`valid <valid-memtype>` under the empty :ref:`context <context>`.
+* The :ref:`memory type <syntax-memtype>` :math:`\idxtype~\limits` must be :ref:`valid <valid-memtype>` under the empty :ref:`context <context>`.
 
 * The length of :math:`b^\ast` must equal :math:`\limits.\LMIN` multiplied by the :ref:`page size <page-size>` :math:`64\,\F{Ki}`.
 
-* Then the memory instance is valid with :ref:`memory type <syntax-memtype>` :math:`\limits`.
+* Then the memory instance is valid with :ref:`memory type <syntax-memtype>` :math:`\idxtype~\limits`.
 
 .. math::
    \frac{
-     \vdashmemtype \limits \ok
+     \vdashmemtype \idxtype~\limits \ok
      \qquad
      n = \limits.\LMIN \cdot 64\,\F{Ki}
    }{
-     S \vdashmeminst \{ \MITYPE~\limits, \MIDATA~b^n \} : \limits
+     S \vdashmeminst \{ \MITYPE~\idxtype~\limits, \MIDATA~b^n \} : \idxtype~\limits
    }
 
 
 .. index:: global type, global instance, value, mutability
 .. _valid-globalinst:
 
-:ref:`Global Instances <syntax-globalinst>` :math:`\{ \GITYPE~(\mut~t), \GIVALUE~\val \}`
-.........................................................................................
+:ref:`Global Instances <syntax-globalinst>` :math:`\{ \GITYPE~\mut~t, \GIVALUE~\val \}`
+.......................................................................................
 
 * The :ref:`global type <syntax-globaltype>` :math:`\mut~t` must be :ref:`valid <valid-globaltype>` under the empty :ref:`context <context>`.
 
@@ -586,7 +586,7 @@ where :math:`\val_1 \gg^+_S \val_2` denotes the transitive closure of the follow
      \qquad
      \vdashvaltypematch t' \matchesvaltype t
    }{
-     S \vdashglobalinst \{ \GITYPE~(\mut~t), \GIVALUE~\val \} : \mut~t
+     S \vdashglobalinst \{ \GITYPE~\mut~t, \GIVALUE~\val \} : \mut~t
    }
 
 
diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst
index 9b00db7ea4..e47bdb576a 100644
--- a/document/core/valid/instructions.rst
+++ b/document/core/valid/instructions.rst
@@ -1366,6 +1366,8 @@ Table Instructions
 
 * The table :math:`C.\CTABLES[x]` must be defined in the context.
 
+* Let :math:`\X{it}~\limits~t` be the :ref:`table type <syntax-tabletype>` :math:`C.\CTABLES[x]`.
+
 * Then the instruction is valid with type :math:`[] \to [\X{it}]`.
 
 .. math::
@@ -2413,7 +2415,7 @@ Control Instructions
 
 * The :ref:`expansion <aux-expand-deftype>` of :math:`C.\CTYPES[y]` must be a :ref:`function type <syntax-functype>` :math:`\TFUNC~[t_1^\ast] \toF [t_2^\ast]`.
 
-* Then the instruction is valid with type :math:`[t_1^\ast~\I32] \to [t_2^\ast]`.
+* Then the instruction is valid with type :math:`[t_1^\ast~\X{it}] \to [t_2^\ast]`.
 
 .. math::
    \frac{
@@ -2504,7 +2506,7 @@ Control Instructions
 
 * The :ref:`result type <syntax-resulttype>` :math:`[t_2^\ast]` must :ref:`match <match-resulttype>` :math:`C.\CRETURN`.
 
-* Then the instruction is valid with type :math:`[t_3^\ast~t_1^\ast~\I32] \to [t_4^\ast]`, for any sequences of :ref:`value types <syntax-valtype>` :math:`t_3^\ast` and :math:`t_4^\ast`.
+* Then the instruction is valid with type :math:`[t_3^\ast~t_1^\ast~\X{it}] \to [t_4^\ast]`, for any sequences of :ref:`value types <syntax-valtype>` :math:`t_3^\ast` and :math:`t_4^\ast`.
 
 .. math::
    \frac{
@@ -2518,7 +2520,7 @@ Control Instructions
      \qquad
      C \vdashinstrtype [t_3^\ast~t_1^\ast~\I32] \to [t_4^\ast] \ok
    }{
-     C \vdashinstr \RETURNCALLINDIRECT~x~y : [t_3^\ast~t_1^\ast~\I32] \to [t_4^\ast]
+     C \vdashinstr \RETURNCALLINDIRECT~x~y : [t_3^\ast~t_1^\ast~\X{it}] \to [t_4^\ast]
    }
 
 .. note::
diff --git a/document/core/valid/matching.rst b/document/core/valid/matching.rst
index af9c161edf..c4dda45b45 100644
--- a/document/core/valid/matching.rst
+++ b/document/core/valid/matching.rst
@@ -502,7 +502,9 @@ Limits
 Table Types
 ~~~~~~~~~~~
 
-A :ref:`table type <syntax-tabletype>` :math:`(\limits_1~\reftype_1)` matches :math:`(\limits_2~\reftype_2)` if and only if:
+A :ref:`table type <syntax-tabletype>` :math:`(\idxtype_1~\limits_1~\reftype_1)` matches :math:`(\idxtype_2~\limits_2~\reftype_2)` if and only if:
+
+* Index types :math:`\idxtype_1` and :math:`\idxtype_2` are the same.
 
 * Limits :math:`\limits_1` :ref:`match <match-limits>` :math:`\limits_2`.
 
@@ -511,13 +513,15 @@ A :ref:`table type <syntax-tabletype>` :math:`(\limits_1~\reftype_1)` matches :m
 .. math::
    ~\\[-1ex]
    \frac{
+     C \vdashnumtypematch \idxtype_1 \matchesnumtype \idxtype_2
+     \qquad
      C \vdashlimitsmatch \limits_1 \matcheslimits \limits_2
      \qquad
      C \vdashreftypematch \reftype_1 \matchesreftype \reftype_2
      \qquad
      C \vdashreftypematch \reftype_2 \matchesreftype \reftype_1
    }{
-     C \vdashtabletypematch \limits_1~\reftype_1 \matchestabletype \limits_2~\reftype_2
+     C \vdashtabletypematch \idxtype_1~\limits_1~\reftype_1 \matchestabletype \idxtype_2~\limits_2~\reftype_2
    }
 
 
@@ -527,7 +531,9 @@ A :ref:`table type <syntax-tabletype>` :math:`(\limits_1~\reftype_1)` matches :m
 Memory Types
 ~~~~~~~~~~~~
 
-A :ref:`memory type <syntax-memtype>` :math:`\limits_1` matches :math:`\limits_2` if and only if:
+A :ref:`memory type <syntax-memtype>` :math:`(\idxtype_1~\limits_1)` matches :math:`(\idxtype_2~\limits_2)` if and only if:
+
+* Index types :math:`\idxtype_1` and :math:`\idxtype_2` are the same.
 
 * Limits :math:`\limits_1` :ref:`match <match-limits>` :math:`\limits_2`.
 
@@ -535,6 +541,8 @@ A :ref:`memory type <syntax-memtype>` :math:`\limits_1` matches :math:`\limits_2
 .. math::
    ~\\[-1ex]
    \frac{
+     C \vdashnumtypematch \idxtype_1 \matchesnumtype \idxtype_2
+     \qquad
      C \vdashlimitsmatch \limits_1 \matcheslimits \limits_2
    }{
      C \vdashmemtypematch \limits_1 \matchesmemtype \limits_2