In the Java Language Specification version 11, section 4.10.2, how do I read Uₖ θ?

Question

(I'm aware of a previous question in this area but you'll notice that the root of the original poster's issue was never resolved. My question, like theirs, is notational in nature.)

In the Java Language Specification, version 11 (but interestingly no longer in JLS 17, probably because it's hard to understand), it says, in part, in section 4.10.2:

Given a generic type declaration C<F₁,…,Fₙ> (n > 0), the direct supertypes of the parameterized type C<T₁,…,Tₙ>, where Tᵢ (1 ≤ i ≤ n) is a type, are all of the following:

D<U₁ θ,…,Uₖ θ>, where D<U₁,…,Uₖ> is a generic type which is a direct supertype of the generic type C<F₁,…,Fₙ> and θ is the substitution [F₁:=T₁,…,Fₙ:=Tₙ].

Here are (possibly incorrect!) assumptions I am making:

• θ means, loosely, "substitute formal type parameters with actual type arguments" because of the meta-notation in section 1.3.
• C<F₁,…,Fₙ> represents, say, public interface Collection<E> extends Iterable<E> (n = 1), and C<T₁,…,Tₙ> represents, say, public class MyStringCollection implements Collection<String> (so Tₙ = T₁). Here, F₁ is the E in Collection<E>, and T₁ is String.
  • (I'm guessing that the author(s) chose C as a symbol because they're talking about a Class declaration.)
• D is a direct supertype of the raw type C, so, say, Iterable. (I'm also guessing that the author(s) chose D as a symbol because they're talking about a type that is derived from C, so the "next symbol after C" is D.)
• k is unbounded, but I'm assuming it is supposed to be 1 ≤ k ≤ n, and the fact that its bounds are left unmentioned makes me think my hypothesis is correct
• Uₖ is the replacement-by-θ of Tₙ (my possibly incorrect hypothesis only! This is my question!), i.e. the result of applying θ to Fₖ, so since n is 1 (Collection takes exactly n = 1 type parameter E), then k is also 1, so we apply θ to F₁, which according to the definition of θ yields T₁, which is String, so therefore D<U₁> is Iterable<String>.
  • (Quick sanity check: can a reference of type Iterable<String> be assigned a reference of type Collection<String>? Yes it can.)
  • (I'm also guessing that the author(s) chose U as a symbol because they're talking about a type that is derived from T, so the "next symbol after T" is U.)

My main question: Is my hypothesis of how to read the notation construction "Uₖ θ" correct? Does "Uₖ θ" mean "find Fₖ and apply θ to it"? If so, in what section can I find the justification—referring to the specification only—for this hypothesis?

My sub-question: if my hypothesis is correct, where can I find the meta-notation that defines notations such as "Uₖ θ", where " " appears to mean "apply the substitution function that follows to the k^th occurrence of the thing that came before, on the k^th occurrence of an element of the domain of the substitution function"?

(Such a meta-notation is not delineated in the specification itself (others, such as θ are, quite explicitly, which is greatly appreciated), and a quick search of conventional meta-notations didn't yield such a convention.)