Editing

2 files changed, 6 insertions, 6 deletions

diff --git a/docs/spec/inferred.html b/docs/spec/inferred.html
index ef7bb6e1..433a65c5 100644
--- a/docs/spec/inferred.html
+++ b/docs/spec/inferred.html
@@ -477,9 +477,9 @@
 <p>When implementing, there is no need to implement invertable Under specially: it can be handled as part of the structural and computation cases.</p>
 <h3 id="mathematical-definition-of-structural-under">Mathematical definition of structural Under</h3>
 <p>In general, structural Under requires information from the original right argument to be computed. Here we will define the <em>structural inverse of</em> structural function <code><span class='Function'>𝔾</span></code> <em>on</em> <code><span class='Value'>v</span></code> <em>into</em> <code><span class='Value'>𝕩</span></code>, where <code><span class='Value'>𝕩</span></code> gives this information. The value <code><span class='Value'>𝕨</span><span class='Function'>𝔽</span><span class='Modifier2'>⌾</span><span class='Function'>𝔾</span><span class='Value'>𝕩</span></code> is then the structural inverse of <code><span class='Function'>𝔾</span></code> on <code><span class='Value'>𝕨</span><span class='Function'>𝔽</span><span class='Modifier2'>○</span><span class='Function'>𝔾</span><span class='Value'>𝕩</span></code> into <code><span class='Value'>𝕩</span></code>.</p>
-<p>We define a <em>structure</em> to be either the value <code><span class='Nothing'>·</span></code> or an array of structures (substitute <code><span class='Number'>0</span></code> or any other specific value for <code><span class='Nothing'>·</span></code> if you'd like structures to be a subset of BQN arrays; the value is irrelevant). A given structure <code><span class='Value'>s</span></code> is a <em>captures</em> a BQN value or structure <code><span class='Value'>𝕩</span></code> if it is <code><span class='Nothing'>·</span></code>, or if <code><span class='Value'>s</span></code> and <code><span class='Value'>𝕩</span></code> are arrays of the same shape, and each element of <code><span class='Value'>s</span></code> captures the corresponding element of <code><span class='Value'>𝕩</span></code>. Thus a structure shares some or all of the structural information in arrays it captures, but none of the data.</p>
+<p>We define a <em>structure</em> to be either the value <code><span class='Nothing'>·</span></code> or an array of structures (substitute <code><span class='Number'>0</span></code> or any other specific value for <code><span class='Nothing'>·</span></code> if you'd like structures to be a subset of BQN arrays; the value is irrelevant). A given structure <code><span class='Value'>s</span></code> <em>captures</em> a BQN value or structure <code><span class='Value'>𝕩</span></code> if it is <code><span class='Nothing'>·</span></code>, or if <code><span class='Value'>s</span></code> and <code><span class='Value'>𝕩</span></code> are arrays of the same shape, and each element of <code><span class='Value'>s</span></code> captures the corresponding element of <code><span class='Value'>𝕩</span></code>. Thus a structure shares some or all of the structural information in arrays it captures, but none of the data.</p>
 <p>A <em>structure transformation</em> consists of an initial structure <code><span class='Value'>s</span></code> and a result structure <code><span class='Value'>t</span></code>, as well as a relation between the two: each instance of <code><span class='Nothing'>·</span></code> in <code><span class='Value'>t</span></code> is assigned the location of an instance of <code><span class='Nothing'>·</span></code> in <code><span class='Value'>s</span></code>. If <code><span class='Value'>s</span></code> captures a value <code><span class='Value'>𝕩</span></code>, we say that the structural transformation captures <code><span class='Value'>𝕩</span></code> as well. Given such a value <code><span class='Value'>𝕩</span></code>, the transformation is applied to <code><span class='Value'>𝕩</span></code> by replacing each <code><span class='Nothing'>·</span></code> in <code><span class='Value'>t</span></code> with the corresponding value from <code><span class='Value'>𝕩</span></code>, found by taking the same location in <code><span class='Value'>𝕩</span></code> as the one in <code><span class='Value'>s</span></code> given by the transformation.</p>
-<p>Given a structure transformation <code><span class='Function'>G</span></code> and values <code><span class='Value'>𝕩</span></code> and <code><span class='Value'>v</span></code>, the <em>structural inverse</em> <code><span class='Value'>z</span></code> of <code><span class='Function'>G</span></code> on <code><span class='Value'>v</span></code> into <code><span class='Value'>𝕩</span></code>, if it exists, is the value such that <code><span class='Value'>v</span><span class='Function'>≡G</span> <span class='Value'>z</span></code>, and <code><span class='Value'>𝕩</span> <span class='Function'>≡</span><span class='Modifier2'>○</span><span class='Function'>F</span> <span class='Value'>z</span></code> for every structure transformation <code><span class='Function'>F</span></code> as possible given the previous constraint. If <code><span class='Function'>G</span></code> has initial structure <code><span class='Value'>s</span></code> and final structure <code><span class='Value'>t</span></code>, we know that <code><span class='Value'>s</span></code> captures <code><span class='Value'>𝕩</span></code> and <code><span class='Value'>z</span></code> (it's required in order to apply <code><span class='Function'>G</span></code> at all) while <code><span class='Value'>t</span></code> captures <code><span class='Value'>v</span></code>. For each instance of <code><span class='Nothing'>·</span></code> in <code><span class='Value'>s</span></code>, there are three possibilities:</p>
+<p>Given values <code><span class='Value'>𝕩</span></code> and <code><span class='Value'>v</span></code> and a structure transformation <code><span class='Function'>G</span></code> capturing <code><span class='Value'>𝕩</span></code>, the <em>structural inverse</em> <code><span class='Value'>z</span></code> of <code><span class='Function'>G</span></code> on <code><span class='Value'>v</span></code> into <code><span class='Value'>𝕩</span></code>, if it exists, is the value such that <code><span class='Value'>v</span><span class='Function'>≡G</span> <span class='Value'>z</span></code>, and <code><span class='Value'>𝕩</span> <span class='Function'>≡</span><span class='Modifier2'>○</span><span class='Function'>F</span> <span class='Value'>z</span></code> for every structure transformation <code><span class='Function'>F</span></code> possible given the previous constraint. If <code><span class='Function'>G</span></code> has initial structure <code><span class='Value'>s</span></code> and final structure <code><span class='Value'>t</span></code>, we know that <code><span class='Value'>s</span></code> captures <code><span class='Value'>𝕩</span></code> and <code><span class='Value'>z</span></code> (it's required in order to apply <code><span class='Function'>G</span></code> at all) while <code><span class='Value'>t</span></code> captures <code><span class='Value'>v</span></code>. For each instance of <code><span class='Nothing'>·</span></code> in <code><span class='Value'>s</span></code>, there are three possibilities:</p>
 <ul>
 <li>No result location in <code><span class='Value'>t</span></code> is assigned this location. This component of <code><span class='Value'>z</span></code> must match <code><span class='Value'>𝕩</span></code>, or <code><span class='Value'>z</span></code> could be improved without breaking any constraints by replacing it.</li>
 <li>Exactly one result location is assigned this location. The requirement <code><span class='Value'>v</span><span class='Function'>≡G</span> <span class='Value'>z</span></code> implies <code><span class='Value'>z</span></code>'s value here is exactly <code><span class='Value'>v</span></code>'s value at that result location.</li>
@@ -489,7 +489,7 @@
 <p>A <em>structural function decomposition</em> is a possibly infinite family of structure transformations such that any possible BQN value is captured by at most one of these transformations. It can be applied to any value: if some transformation captures the value, then apply that transformation, and otherwise give an error. A function is a <em>structural function</em> if there is a structural function decomposition that matches it: that is, for any input either both functions give an error or the results match.</p>
 <p>For a structural function <code><span class='Function'>𝔾</span></code>, the <em>structural inverse</em> of <code><span class='Function'>𝔾</span></code> on <code><span class='Value'>v</span></code> into <code><span class='Value'>𝕩</span></code> is the inverse of <code><span class='Function'>G</span></code> on <code><span class='Value'>v</span></code> into <code><span class='Value'>𝕩</span></code>, where <code><span class='Function'>G</span></code> is the structure transformation that captures <code><span class='Value'>𝕩</span></code> from some structural function decomposition <code><span class='Function'>Gd</span></code> matching <code><span class='Function'>𝔾</span></code>. If no decomposition has an initial structural matching <code><span class='Value'>𝕩</span></code> then the structural inverse does not exist.</p>
 <h4 id="well-definedness">Well-definedness</h4>
-<p>In order to show that the structural inverse of a structural function is well-defined, we must show that it does not depend on the choice of structural function decomposition. That is, for a given <code><span class='Value'>𝕩</span></code>, if <code><span class='Function'>G</span></code> and <code><span class='Function'>H</span></code> are structure transformations from different decompositions of <code><span class='Function'>𝔾</span></code> both capturing <code><span class='Value'>𝕩</span></code>, then the structural inverse of <code><span class='Function'>G</span></code> on <code><span class='Value'>v</span></code> into <code><span class='Value'>𝕩</span></code> matches that of <code><span class='Function'>H</span></code> on <code><span class='Value'>v</span></code> into <code><span class='Value'>𝕩</span></code>. Call these inverses <code><span class='Value'>y</span></code> and <code><span class='Value'>z</span></code>. Now begin by supposing that <code><span class='Function'>H</span></code> captures <code><span class='Value'>y</span></code> and <code><span class='Function'>G</span></code> captures <code><span class='Value'>z</span></code>; we will show this later. From the definition of a structural inverse, <code><span class='Value'>v</span><span class='Function'>≡G</span> <span class='Value'>y</span></code>, so that <code><span class='Value'>v</span><span class='Function'>≡𝔾</span> <span class='Value'>y</span></code>, and because <code><span class='Function'>H</span></code> captures <code><span class='Value'>y</span></code> we know that <code><span class='Function'>𝔾</span> <span class='Value'>y</span></code> is <code><span class='Function'>H</span> <span class='Value'>y</span></code>, so we have <code><span class='Value'>v</span><span class='Function'>≡H</span> <span class='Value'>y</span></code> as well. Let <code><span class='Function'>S</span> <span class='Value'>w</span></code> indicate the set of all functions <code><span class='Function'>F</span></code> such that <code><span class='Value'>w</span> <span class='Function'>≡</span><span class='Modifier2'>○</span><span class='Function'>F</span> <span class='Value'>𝕩</span></code> (this is not a BQN value, both because it is a set and because it's usually infinite): from the definition of <code><span class='Value'>z</span></code> we know that <code><span class='Function'>S</span> <span class='Value'>z</span></code> is a strict superset of <code><span class='Function'>S</span> <span class='Value'>w</span></code> for any <code><span class='Value'>w</span></code> other than <code><span class='Value'>z</span></code> with <code><span class='Value'>v</span><span class='Function'>≡H</span> <span class='Value'>w</span></code>. It follows that either <code><span class='Value'>y</span><span class='Function'>≡</span><span class='Value'>z</span></code> or <code><span class='Function'>S</span> <span class='Value'>y</span></code> is a strict subset of <code><span class='Function'>S</span> <span class='Value'>z</span></code>. By symmetry the same relation holds exchanging <code><span class='Value'>y</span></code> and <code><span class='Value'>z</span></code>, but it's not possible for <code><span class='Function'>S</span> <span class='Value'>y</span></code> to be a strict subset of <code><span class='Function'>S</span> <span class='Value'>z</span></code> and vice-versa. The only remaining possibility is that <code><span class='Value'>y</span><span class='Function'>≡</span><span class='Value'>z</span></code>.</p>
+<p>In order to show that the structural inverse of a structural function is well-defined, we must show that it does not depend on the choice of structural function decomposition. That is, for a given <code><span class='Value'>𝕩</span></code>, if <code><span class='Function'>G</span></code> and <code><span class='Function'>H</span></code> are structure transformations from different decompositions of <code><span class='Function'>𝔾</span></code> both capturing <code><span class='Value'>𝕩</span></code>, then the structural inverse of <code><span class='Function'>G</span></code> on <code><span class='Value'>v</span></code> into <code><span class='Value'>𝕩</span></code> matches that of <code><span class='Function'>H</span></code> on <code><span class='Value'>v</span></code> into <code><span class='Value'>𝕩</span></code>. Call these inverses <code><span class='Value'>y</span></code> and <code><span class='Value'>z</span></code>. Now begin by supposing that <code><span class='Function'>H</span></code> captures <code><span class='Value'>y</span></code> and <code><span class='Function'>G</span></code> captures <code><span class='Value'>z</span></code>; we will show this later. From the definition of a structural inverse, <code><span class='Value'>v</span><span class='Function'>≡G</span> <span class='Value'>y</span></code>, so that <code><span class='Value'>v</span><span class='Function'>≡𝔾</span> <span class='Value'>y</span></code>, and because <code><span class='Function'>H</span></code> captures <code><span class='Value'>y</span></code> we know that <code><span class='Function'>𝔾</span> <span class='Value'>y</span></code> is <code><span class='Function'>H</span> <span class='Value'>y</span></code>, so we have <code><span class='Value'>v</span><span class='Function'>≡H</span> <span class='Value'>y</span></code> as well. Let <code><span class='Function'>S</span> <span class='Value'>w</span></code> indicate the set of all structure transformations <code><span class='Function'>F</span></code> such that <code><span class='Value'>w</span> <span class='Function'>≡</span><span class='Modifier2'>○</span><span class='Function'>F</span> <span class='Value'>𝕩</span></code> (this is not a BQN value, both because it is a set and because it's usually infinite): from the definition of <code><span class='Value'>z</span></code> we know that <code><span class='Function'>S</span> <span class='Value'>z</span></code> is a strict superset of <code><span class='Function'>S</span> <span class='Value'>w</span></code> for any <code><span class='Value'>w</span></code> other than <code><span class='Value'>z</span></code> with <code><span class='Value'>v</span><span class='Function'>≡H</span> <span class='Value'>w</span></code>. It follows that either <code><span class='Value'>y</span><span class='Function'>≡</span><span class='Value'>z</span></code> or <code><span class='Function'>S</span> <span class='Value'>y</span></code> is a strict subset of <code><span class='Function'>S</span> <span class='Value'>z</span></code>. By symmetry the same relation holds exchanging <code><span class='Value'>y</span></code> and <code><span class='Value'>z</span></code>, but it's not possible for <code><span class='Function'>S</span> <span class='Value'>y</span></code> to be a strict subset of <code><span class='Function'>S</span> <span class='Value'>z</span></code> and vice-versa. The only remaining possibility is that <code><span class='Value'>y</span><span class='Function'>≡</span><span class='Value'>z</span></code>.</p>
 <p>We now need to show that <code><span class='Function'>H</span></code> captures <code><span class='Value'>y</span></code> (the proof that <code><span class='Function'>G</span></code> captures <code><span class='Value'>z</span></code> is of course the same as <code><span class='Function'>H</span></code> and <code><span class='Function'>G</span></code> are symmetric). To do this we must show that any array in the initial structure of <code><span class='Function'>H</span></code> corresponds to a matching array in <code><span class='Value'>y</span></code>. For convenience, we will call the initial structures of the two transformations <code><span class='Value'>iG</span></code> and <code><span class='Value'>iH</span></code>, and the final structures <code><span class='Value'>fG</span></code> and <code><span class='Value'>fH</span></code>, and use the notation <code><span class='Value'>p</span><span class='Function'>⊑</span><span class='Value'>a</span></code> to indicate the value of array <code><span class='Value'>a</span></code> at position <code><span class='Value'>p</span></code>. Choose the position of an array in <code><span class='Function'>H</span></code>, and assume by induction that each array containing it already has the desired property; this implies that this position exists in <code><span class='Value'>y</span></code> as well although we know nothing about its contents. <code><span class='Function'>G</span></code> captures <code><span class='Value'>y</span></code>, so <code><span class='Value'>iG</span></code> is <code><span class='Nothing'>·</span></code> at this position or some parent position; call this position in <code><span class='Value'>iG</span></code> <code><span class='Value'>p</span></code>. There are now two cases: either <code><span class='Function'>G</span></code> makes use of this <code><span class='Value'>p</span></code>—at least one position in <code><span class='Value'>fG</span></code> corresponds to it—or it doesn't. If it doesn't, then the contents of <code><span class='Value'>y</span></code> at <code><span class='Value'>p</span></code> are the same as those of <code><span class='Value'>𝕩</span></code>. Since <code><span class='Function'>H</span></code> captures <code><span class='Value'>𝕩</span></code>, <code><span class='Value'>iH</span></code> matches <code><span class='Value'>𝕩</span></code> and hence <code><span class='Value'>y</span></code> as well at <code><span class='Value'>p</span></code>. If it does, then let <code><span class='Value'>s</span></code> be a position in <code><span class='Value'>fG</span></code> that corresponds to <code><span class='Value'>p</span></code> (if there are multiple possibilities, choose one). From <code><span class='Value'>v</span><span class='Function'>≡G</span> <span class='Value'>y</span></code>, we know that <code><span class='Value'>s</span><span class='Function'>⊑</span><span class='Value'>v</span></code> matches <code><span class='Value'>p</span><span class='Function'>⊑</span><span class='Value'>y</span></code>. We know that <code><span class='Value'>fH</span></code> captures <code><span class='Value'>v</span></code>, so that <code><span class='Value'>s</span><span class='Function'>⊑</span><span class='Value'>fH</span></code> captures <code><span class='Value'>s</span><span class='Function'>⊑</span><span class='Value'>v</span></code>, or <code><span class='Value'>p</span><span class='Function'>⊑</span><span class='Value'>y</span></code>. But we can show that the value of <code><span class='Value'>s</span><span class='Function'>⊑</span><span class='Value'>fH</span></code> is the same as <code><span class='Value'>p</span><span class='Function'>⊑</span><span class='Value'>iH</span></code>, which would prove that <code><span class='Function'>H</span></code> captures <code><span class='Value'>y</span></code> at <code><span class='Value'>p</span></code>. To show this, construct an array <code><span class='Value'>xp</span></code> by replacing the value of <code><span class='Value'>𝕩</span></code> at <code><span class='Value'>p</span></code> with <code><span class='Value'>p</span><span class='Function'>⊑</span><span class='Value'>iH</span></code> (to be more careful in our handling of types, we might replace every <code><span class='Nothing'>·</span></code> with some value that never appears in <code><span class='Value'>𝕩</span></code>). Both <code><span class='Function'>H</span></code> and <code><span class='Function'>G</span></code> capture <code><span class='Value'>xp</span></code>: clearly they capture it outside <code><span class='Value'>p</span></code>, while at <code><span class='Value'>p</span></code> itself, <code><span class='Value'>iG</span></code> is <code><span class='Nothing'>·</span></code> and <code><span class='Value'>iH</span></code> is equal to <code><span class='Value'>p</span><span class='Function'>⊑</span><span class='Value'>xp</span></code>. Now <code><span class='Paren'>(</span><span class='Function'>H</span> <span class='Value'>xp</span><span class='Paren'>)</span><span class='Function'>≡</span><span class='Paren'>(</span><span class='Function'>G</span> <span class='Value'>xp</span><span class='Paren'>)</span></code> because both functions match <code><span class='Function'>𝔾</span></code> on their domains. Therefore <code><span class='Value'>s</span><span class='Function'>⊑H</span> <span class='Value'>xp</span></code> matches <code><span class='Value'>s</span><span class='Function'>⊑G</span> <span class='Value'>xp</span></code>, which by the definition of <code><span class='Value'>s</span></code> matches <code><span class='Value'>p</span><span class='Function'>⊑</span><span class='Value'>xp</span></code>, which matches <code><span class='Value'>p</span><span class='Function'>⊑</span><span class='Value'>iH</span></code>. But <code><span class='Value'>s</span><span class='Function'>⊑H</span> <span class='Value'>xp</span></code> comes from replacing each atom in <code><span class='Value'>s</span><span class='Function'>⊑</span><span class='Value'>fH</span></code> with an atom in <code><span class='Value'>xp</span></code> that's captured by a <code><span class='Nothing'>·</span></code> in <code><span class='Value'>iH</span></code>. Because it matches <code><span class='Value'>p</span><span class='Function'>⊑</span><span class='Value'>iH</span></code>, every atom in <code><span class='Value'>s</span><span class='Function'>⊑H</span> <span class='Value'>xp</span></code> is <code><span class='Nothing'>·</span></code>, but the only instances of <code><span class='Nothing'>·</span></code> in <code><span class='Value'>xp</span></code> come from our inserted copy of <code><span class='Value'>p</span><span class='Function'>⊑</span><span class='Value'>iH</span></code> and each is immediately captured by the corresponding <code><span class='Nothing'>·</span></code> in <code><span class='Value'>iH</span></code>. It follows that <code><span class='Value'>s</span><span class='Function'>⊑H</span> <span class='Value'>xp</span></code>, and consequently <code><span class='Value'>s</span><span class='Function'>⊑</span><span class='Value'>fH</span></code>, is exactly <code><span class='Value'>p</span><span class='Function'>⊑</span><span class='Value'>iH</span></code>, completing the proof.</p>
 <h3 id="required-structural-inverses">Required structural inverses</h3>
 <p>The following primitive functions be fully supported by structural Under. Each manipulates its right argument structurally.</p>
diff --git a/spec/inferred.md b/spec/inferred.md
index 0fe24442..d83461c7 100644
--- a/spec/inferred.md
+++ b/spec/inferred.md
@@ -180,11 +180,11 @@ When implementing, there is no need to implement invertable Under specially: it
 
 In general, structural Under requires information from the original right argument to be computed. Here we will define the *structural inverse of* structural function `𝔾` *on* `v` *into* `𝕩`, where `𝕩` gives this information. The value `𝕨𝔽⌾𝔾𝕩` is then the structural inverse of `𝔾` on `𝕨𝔽○𝔾𝕩` into `𝕩`.
 
-We define a *structure* to be either the value `·` or an array of structures (substitute `0` or any other specific value for `·` if you'd like structures to be a subset of BQN arrays; the value is irrelevant). A given structure `s` is a *captures* a BQN value or structure `𝕩` if it is `·`, or if `s` and `𝕩` are arrays of the same shape, and each element of `s` captures the corresponding element of `𝕩`. Thus a structure shares some or all of the structural information in arrays it captures, but none of the data.
+We define a *structure* to be either the value `·` or an array of structures (substitute `0` or any other specific value for `·` if you'd like structures to be a subset of BQN arrays; the value is irrelevant). A given structure `s` *captures* a BQN value or structure `𝕩` if it is `·`, or if `s` and `𝕩` are arrays of the same shape, and each element of `s` captures the corresponding element of `𝕩`. Thus a structure shares some or all of the structural information in arrays it captures, but none of the data.
 
 A *structure transformation* consists of an initial structure `s` and a result structure `t`, as well as a relation between the two: each instance of `·` in `t` is assigned the location of an instance of `·` in `s`. If `s` captures a value `𝕩`, we say that the structural transformation captures `𝕩` as well. Given such a value `𝕩`, the transformation is applied to `𝕩` by replacing each `·` in `t` with the corresponding value from `𝕩`, found by taking the same location in `𝕩` as the one in `s` given by the transformation.
 
-Given a structure transformation `G` and values `𝕩` and `v`, the *structural inverse* `z` of `G` on `v` into `𝕩`, if it exists, is the value such that `v≡G z`, and `𝕩 ≡○F z` for every structure transformation `F` as possible given the previous constraint. If `G` has initial structure `s` and final structure `t`, we know that `s` captures `𝕩` and `z` (it's required in order to apply `G` at all) while `t` captures `v`. For each instance of `·` in `s`, there are three possibilities:
+Given values `𝕩` and `v` and a structure transformation `G` capturing `𝕩`, the *structural inverse* `z` of `G` on `v` into `𝕩`, if it exists, is the value such that `v≡G z`, and `𝕩 ≡○F z` for every structure transformation `F` possible given the previous constraint. If `G` has initial structure `s` and final structure `t`, we know that `s` captures `𝕩` and `z` (it's required in order to apply `G` at all) while `t` captures `v`. For each instance of `·` in `s`, there are three possibilities:
 - No result location in `t` is assigned this location. This component of `z` must match `𝕩`, or `z` could be improved without breaking any constraints by replacing it.
 - Exactly one result location is assigned this location. The requirement `v≡G z` implies `z`'s value here is exactly `v`'s value at that result location.
 - More than one result location is assigned this location. Now `z`'s value there must match `v`'s value at each of these result leaves. If `v` has different values at the different leaves, there is no inverse.
@@ -196,7 +196,7 @@ For a structural function `𝔾`, the *structural inverse* of `𝔾` on `v` into
 
 #### Well-definedness
 
-In order to show that the structural inverse of a structural function is well-defined, we must show that it does not depend on the choice of structural function decomposition. That is, for a given `𝕩`, if `G` and `H` are structure transformations from different decompositions of `𝔾` both capturing `𝕩`, then the structural inverse of `G` on `v` into `𝕩` matches that of `H` on `v` into `𝕩`. Call these inverses `y` and `z`. Now begin by supposing that `H` captures `y` and `G` captures `z`; we will show this later. From the definition of a structural inverse, `v≡G y`, so that `v≡𝔾 y`, and because `H` captures `y` we know that `𝔾 y` is `H y`, so we have `v≡H y` as well. Let `S w` indicate the set of all functions `F` such that `w ≡○F 𝕩` (this is not a BQN value, both because it is a set and because it's usually infinite): from the definition of `z` we know that `S z` is a strict superset of `S w` for any `w` other than `z` with `v≡H w`. It follows that either `y≡z` or `S y` is a strict subset of `S z`. By symmetry the same relation holds exchanging `y` and `z`, but it's not possible for `S y` to be a strict subset of `S z` and vice-versa. The only remaining possibility is that `y≡z`.
+In order to show that the structural inverse of a structural function is well-defined, we must show that it does not depend on the choice of structural function decomposition. That is, for a given `𝕩`, if `G` and `H` are structure transformations from different decompositions of `𝔾` both capturing `𝕩`, then the structural inverse of `G` on `v` into `𝕩` matches that of `H` on `v` into `𝕩`. Call these inverses `y` and `z`. Now begin by supposing that `H` captures `y` and `G` captures `z`; we will show this later. From the definition of a structural inverse, `v≡G y`, so that `v≡𝔾 y`, and because `H` captures `y` we know that `𝔾 y` is `H y`, so we have `v≡H y` as well. Let `S w` indicate the set of all structure transformations `F` such that `w ≡○F 𝕩` (this is not a BQN value, both because it is a set and because it's usually infinite): from the definition of `z` we know that `S z` is a strict superset of `S w` for any `w` other than `z` with `v≡H w`. It follows that either `y≡z` or `S y` is a strict subset of `S z`. By symmetry the same relation holds exchanging `y` and `z`, but it's not possible for `S y` to be a strict subset of `S z` and vice-versa. The only remaining possibility is that `y≡z`.
 
 We now need to show that `H` captures `y` (the proof that `G` captures `z` is of course the same as `H` and `G` are symmetric). To do this we must show that any array in the initial structure of `H` corresponds to a matching array in `y`. For convenience, we will call the initial structures of the two transformations `iG` and `iH`, and the final structures `fG` and `fH`, and use the notation `p⊑a` to indicate the value of array `a` at position `p`. Choose the position of an array in `H`, and assume by induction that each array containing it already has the desired property; this implies that this position exists in `y` as well although we know nothing about its contents. `G` captures `y`, so `iG` is `·` at this position or some parent position; call this position in `iG` `p`. There are now two cases: either `G` makes use of this `p`—at least one position in `fG` corresponds to it—or it doesn't. If it doesn't, then the contents of `y` at `p` are the same as those of `𝕩`. Since `H` captures `𝕩`, `iH` matches `𝕩` and hence `y` as well at `p`. If it does, then let `s` be a position in `fG` that corresponds to `p` (if there are multiple possibilities, choose one). From `v≡G y`, we know that `s⊑v` matches `p⊑y`. We know that `fH` captures `v`, so that `s⊑fH` captures `s⊑v`, or `p⊑y`. But we can show that the value of `s⊑fH` is the same as `p⊑iH`, which would prove that `H` captures `y` at `p`. To show this, construct an array `xp` by replacing the value of `𝕩` at `p` with `p⊑iH` (to be more careful in our handling of types, we might replace every `·` with some value that never appears in `𝕩`). Both `H` and `G` capture `xp`: clearly they capture it outside `p`, while at `p` itself, `iG` is `·` and `iH` is equal to `p⊑xp`. Now `(H xp)≡(G xp)` because both functions match `𝔾` on their domains. Therefore `s⊑H xp` matches `s⊑G xp`, which by the definition of `s` matches `p⊑xp`, which matches `p⊑iH`. But `s⊑H xp` comes from replacing each atom in `s⊑fH` with an atom in `xp` that's captured by a `·` in `iH`. Because it matches `p⊑iH`, every atom in `s⊑H xp` is `·`, but the only instances of `·` in `xp` come from our inserted copy of `p⊑iH` and each is immediately captured by the corresponding `·` in `iH`. It follows that `s⊑H xp`, and consequently `s⊑fH`, is exactly `p⊑iH`, completing the proof.