关于Java语言规范11版第4.10.2节Uₖ θ符号解读及规范依据的技术问询

我知道之前已经有相关问题被提出，但原提问者的核心困惑并没有得到解决。和那个问题类似，我的疑问也属于对规范中符号的解读范畴。

在《Java语言规范》11版中（有意思的是，JLS 17版里已经删掉了这部分内容，可能是因为它确实不太好理解），第4.10.2节有这么一段内容：给定泛型类型声明C<F₁,…,Fₙ>（n>0），参数化类型C<T₁,…,Tₙ>（其中Tᵢ（1≤i≤n）为类型）的直接超类型包含以下所有类型：D<U₁ θ,…,Uₖ θ>，其中D<U₁,…,Uₖ>是泛型类型C<F₁,…,Fₙ>的直接超类型，θ为替换操作[F₁:=T₁,…,Fₙ:=Tₙ]。

我做出了以下（可能有误的）假设：

• θ大致表示“用实际类型参数替换形式类型参数”，这个是根据第1.3节里的元符号定义来的。
• C<F₁,…,Fₙ>可以举个例子，比如public interface Collection<E> extends Iterable<E>（这里n=1），C<T₁,…,Tₙ>对应的例子就是public class MyStringCollection implements Collection<String>（所以Tₙ=T₁）。这里的F₁就是Collection<E>里的E，T₁是String。我猜作者选符号C是因为它代表Class（类）声明。
• D是原始类型C的直接超类型，比如Iterable。我还猜作者选符号D是因为它指代C派生而来的类型，也就是C之后的下一个符号用D。
• k没有设定边界，但我假设它的范围是1≤k≤n，规范里没提边界这件事，反而让我觉得这个假设是成立的。
• Uₖ是通过θ替换得到的结果（这只是我可能错的假设，也是我的核心疑问！），也就是对Fₖ应用θ后的结果。所以当n=1（Collection只接受1个类型参数E）时，k也为1，对F₁应用θ后，根据θ的定义得到T₁也就是String，所以D<U₁>就是Iterable<String>。（快速验证：Iterable<String>类型的引用能不能赋值给Collection<String>类型的引用？答案是可以的。）我还猜作者选符号U是因为它指代由T派生的类型，也就是T之后的下一个符号用U。

主问题 #

我对符号构造Uₖ θ的解读假设是否正确？Uₖ θ是不是表示“找到Fₖ并对其应用θ”？如果正确的话，我能在规范的哪一节找到支持这个假设的依据（只参考规范内容）？

子问题 #

如果我的假设是正确的，哪里能找到定义Uₖ θ这类符号的元符号规范？其中ₖ似乎表示“对前面事物的第k次出现应用后续的替换函数，针对替换函数域中元素的第k次出现”？（这类元符号在规范里没有明确说明，而其他符号比如θ是有明确定义的，这点做得很好；我快速查了常规元符号也没找到这类约定。）

内容的提问来源于stack exchange，提问作者Laird Nelson