Unary and Reverse-Unary Native Insertion

Abstract

Gap masses identify native unary insertion minima in both ordered orientations.

Words and masks use the original ordered source schedule: the first source is inserted and the second is the base. The degree is the minimum number of maximal nonempty first-source runs over all actual masks, with infinity for an invalid output. Neither source roles nor minimum semantics are exchanged when passing to the reverse-unary case.

The inserted-unary gap, degree and spectrum arguments use Hughes arXiv v2, Section 11, Theorem 9: https://arxiv.org/abs/2608.27755v2. The reverse-unary and universal minimum-mask exchange statements are separate arguments.

Definition 1.1 (Occupied extra gaps).

$$\forall e\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\mathrm{occupied}\left(e\right)=\mathrm{countPositive}\left(e\right)$$

Formalization. D5/S1/Words/HughesUnaryInsertion.occupied (✓ std3).

Source. Repository-derived.

Commentary.

Count strictly positive extra masses; a positive original gap with zero extra mass is unoccupied. Both outer gaps are included in this count.

Definition 1.2 (Occupied internal extra gaps).

$$\forall e\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\mathrm{internalOccupied}\left(e\right)=\mathrm{occupied}\left(\mathrm{dropLast}\left(\mathrm{tail}\left(e\right)\right)\right)$$

Formalization. D5/S1/Words/HughesUnaryInsertion.internalOccupied (✓ std3).

Source. Repository-derived.

Commentary.

Discard the initial and terminal gap before counting. For zero or one non-a occurrences there are no internal gaps.

Definition 1.3 (Actual native shuffles).

$$\forall alpha\in \mathrm{Type}\left(\right),\forall u\in \mathrm{List}\left(alpha\right),\forall v\in \mathrm{List}\left(alpha\right),\forall w\in \mathrm{List}\left(alpha\right),w\in \mathrm{Sh}\left(u,v\right)\iff \left(\exists M\in \mathrm{List}\left(Side\right),\mathrm{ValidMask}\left(u,v,w,M\right)\right)$$

Formalization. D5/S1/Words/HughesUnaryInsertion.Sh (✓ std3).

Source. Repository-derived.

Commentary.

Membership means an actual positional mask evaluates to the word and consumes both original sources. No separate ordinary-shuffle identification is used.

Definition 1.4 (Attained natural degrees).

$$\forall alpha\in \mathrm{Type}\left(\right),\forall u\in \mathrm{List}\left(alpha\right),\forall v\in \mathrm{List}\left(alpha\right),\forall r\in \mathrm{Nat}\left(\right),r\in \mathrm{spectrum}\left(u,v\right)\iff \left(\exists w\in \mathrm{List}\left(alpha\right),w\in \mathrm{Sh}\left(u,v\right)\wedge \mathrm{degree}\left(u,v,w\right)=r\right)$$

Formalization. D5/S1/Words/HughesUnaryInsertion.spectrum (✓ std3).

Source. Repository-derived.

Commentary.

A natural value occurs only through an actual shuffle output with that native minimum; infinity contributes no natural spectrum value.

Theorem 1.5 (Inserted-unary unique gap masses).

$$\forall alpha\in \mathrm{Type}\left(\right),\forall a\in alpha,\forall m\in \mathrm{Nat}\left(\right),\forall cs\in \mathrm{List}\left(alpha\right),\forall h\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\forall w\in \mathrm{List}\left(alpha\right),\left(\left(\forall c\in alpha,c\in cs\Rightarrow c\ne a\right)\wedge \mathrm{length}\left(h\right)=\mathrm{length}\left(cs\right)+1\right)\Rightarrow \left(w\in \mathrm{Sh}\left(\mathrm{replicate}\left(m,a\right),\mathrm{gap}\left(a,cs,h\right)\right)\iff \left(\exists e\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\left(\mathrm{length}\left(e\right)=\mathrm{length}\left(h\right)\wedge \left(\mathrm{sum}\left(e\right)=m\wedge w=\mathrm{gap}\left(a,cs,\mathrm{zipWith}\left(add,h,e\right)\right)\right)\right)\wedge \left(\forall f\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\left(\mathrm{length}\left(f\right)=\mathrm{length}\left(h\right)\wedge \left(\mathrm{sum}\left(f\right)=m\wedge w=\mathrm{gap}\left(a,cs,\mathrm{zipWith}\left(add,h,f\right)\right)\right)\right)\Rightarrow f=e\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/HughesUnaryInsertion.inserted_gap_iff (✓ std3). ∎

Citation. Charles E. Hughes (2026). Undecidability of Adjacent Equality for Insertion, Shuffle, and Crossover Language Operations. URL: https://arxiv.org/abs/2608.27755v1.

Commentary.

Non-a occurrences are forced to the base source. Every output has a unique nonnegative extra vector of total inserted length, and every such vector has a full native mask. Repeated separator letters remain indexed occurrences.

Theorem 1.6 (Reverse-unary unique gap masses).

$$\forall alpha\in \mathrm{Type}\left(\right),\forall a\in alpha,\forall m\in \mathrm{Nat}\left(\right),\forall cs\in \mathrm{List}\left(alpha\right),\forall h\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\forall w\in \mathrm{List}\left(alpha\right),\left(\left(\forall c\in alpha,c\in cs\Rightarrow c\ne a\right)\wedge \mathrm{length}\left(h\right)=\mathrm{length}\left(cs\right)+1\right)\Rightarrow \left(w\in \mathrm{Sh}\left(\mathrm{gap}\left(a,cs,h\right),\mathrm{replicate}\left(m,a\right)\right)\iff \left(\exists e\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\left(\mathrm{length}\left(e\right)=\mathrm{length}\left(h\right)\wedge \left(\mathrm{sum}\left(e\right)=m\wedge w=\mathrm{gap}\left(a,cs,\mathrm{zipWith}\left(add,h,e\right)\right)\right)\right)\wedge \left(\forall f\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\left(\mathrm{length}\left(f\right)=\mathrm{length}\left(h\right)\wedge \left(\mathrm{sum}\left(f\right)=m\wedge w=\mathrm{gap}\left(a,cs,\mathrm{zipWith}\left(add,h,f\right)\right)\right)\right)\Rightarrow f=e\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/HughesUnaryInsertion.reverse_gap_iff (✓ std3). ∎

Source. Repository-derived.

Commentary.

Here non-a occurrences are forced to the inserted source. The same concatenation description retains all base mass, including both outer gaps.

Theorem 1.7 (Inserted-unary minimum and attainment).

$$\forall alpha\in \mathrm{Type}\left(\right),\forall a\in alpha,\forall m\in \mathrm{Nat}\left(\right),\forall cs\in \mathrm{List}\left(alpha\right),\forall h\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\forall e\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\left(\left(\forall c\in alpha,c\in cs\Rightarrow c\ne a\right)\wedge \left(\mathrm{length}\left(h\right)=\mathrm{length}\left(cs\right)+1\wedge \left(\mathrm{length}\left(e\right)=\mathrm{length}\left(h\right)\wedge \mathrm{sum}\left(e\right)=m\right)\right)\right)\Rightarrow \left(\mathrm{IsMinimumMask}\left(\mathrm{replicate}\left(m,a\right),\mathrm{gap}\left(a,cs,h\right),\mathrm{gap}\left(a,cs,\mathrm{zipWith}\left(add,h,e\right)\right),\mathrm{grouped}\left(second,cs,h,e\right),\mathrm{occupied}\left(e\right)\right)\wedge \mathrm{degree}\left(\mathrm{replicate}\left(m,a\right),\mathrm{gap}\left(a,cs,h\right),\mathrm{gap}\left(a,cs,\mathrm{zipWith}\left(add,h,e\right)\right)\right)=\mathrm{occupied}\left(e\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/HughesUnaryInsertion.inserted_degree (✓ std3). ∎

Citation. Charles E. Hughes (2026). Undecidability of Adjacent Equality for Insertion, Shuffle, and Crossover Language Operations. URL: https://arxiv.org/abs/2608.27755v1.

Commentary.

Each occupied gap needs an inserted run because non-a letters separate gaps. The grouped mask puts each gap’s inserted letters together, reaches exactly that number of runs, and preserves both projections. This formalizes the occupied-gap proof of Hughes arXiv v2, Theorem 9, for arbitrary alphabets. For positive inserted length its convention agrees with native U-run degree; when that length is zero the native count is zero.

Theorem 1.8 (Reverse-unary internal minimum and attainment).

$$\forall alpha\in \mathrm{Type}\left(\right),\forall a\in alpha,\forall m\in \mathrm{Nat}\left(\right),\forall cs\in \mathrm{List}\left(alpha\right),\forall h\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\forall e\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\left(\left(\left(\forall c\in alpha,c\in cs\Rightarrow c\ne a\right)\wedge \left(\mathrm{length}\left(h\right)=\mathrm{length}\left(cs\right)+1\wedge \left(\mathrm{length}\left(e\right)=\mathrm{length}\left(h\right)\wedge \mathrm{sum}\left(e\right)=m\right)\right)\right)\wedge cs\ne nil\right)\Rightarrow \left(\mathrm{IsMinimumMask}\left(\mathrm{gap}\left(a,cs,h\right),\mathrm{replicate}\left(m,a\right),\mathrm{gap}\left(a,cs,\mathrm{zipWith}\left(add,h,e\right)\right),\mathrm{grouped}\left(first,cs,h,e\right),1+\mathrm{internalOccupied}\left(e\right)\right)\wedge \mathrm{degree}\left(\mathrm{gap}\left(a,cs,h\right),\mathrm{replicate}\left(m,a\right),\mathrm{gap}\left(a,cs,\mathrm{zipWith}\left(add,h,e\right)\right)\right)=1+\mathrm{internalOccupied}\left(e\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/HughesUnaryInsertion.reverse_degree (✓ std3). ∎

Source. Repository-derived.

Commentary.

With at least one non-a occurrence, every occupied internal gap separates forced inserted-source groups. The grouped construction places outer base material outside those groups, so the count is one plus occupied internal gaps. Original a copies in every gap remain part of the inserted projection.

Theorem 1.9 (Reverse-unary boundary cases).

$$\forall alpha\in \mathrm{Type}\left(\right),\forall a\in alpha,\forall m\in \mathrm{Nat}\left(\right),\forall cs\in \mathrm{List}\left(alpha\right),\forall h\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\forall e\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\left(\left(\left(\forall c\in alpha,c\in cs\Rightarrow c\ne a\right)\wedge \left(\mathrm{length}\left(h\right)=\mathrm{length}\left(cs\right)+1\wedge \left(\mathrm{length}\left(e\right)=\mathrm{length}\left(h\right)\wedge \mathrm{sum}\left(e\right)=m\right)\right)\right)\wedge \mathrm{gap}\left(a,cs,h\right)\ne nil\right)\Rightarrow \mathrm{degree}\left(\mathrm{gap}\left(a,cs,h\right),\mathrm{replicate}\left(m,a\right),\mathrm{gap}\left(a,cs,\mathrm{zipWith}\left(add,h,e\right)\right)\right)=\mathrm{ite}\left(cs=nil,1,1+\mathrm{internalOccupied}\left(e\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/HughesUnaryInsertion.reverse_degree_all (✓ std3). ∎

Source. Repository-derived.

Commentary.

For no non-a occurrences, nonemptiness of the inserted source forces a positive unary length and the degree is one. With a single non-a occurrence there are no internal gaps, again giving degree one regardless of both outer extra masses. Both statements use the same actual source projections.

Theorem 1.10 (Every-mask inserted lower bound).

$$\forall alpha\in \mathrm{Type}\left(\right),\forall a\in alpha,\forall cs\in \mathrm{List}\left(alpha\right),\forall h\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\forall e\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\forall w\in \mathrm{List}\left(alpha\right),\forall M\in \mathrm{List}\left(Side\right),\mathrm{Trace}\left(a,second,cs,h,e,w,M\right)\Rightarrow \mathrm{occupied}\left(e\right)\le \mathrm{rho}\left(M\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/HughesUnaryInsertion.inserted_trace_lower (✓ std3). ∎

Source. Repository-derived.

Commentary.

Non-a base occurrences separate the label lists of successive gaps. Each positive first-source count contributes at least one maximal U-run.

Theorem 1.11 (Every-mask reverse lower bound).

$$\forall alpha\in \mathrm{Type}\left(\right),\forall a\in alpha,\forall cs\in \mathrm{List}\left(alpha\right),\forall h\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\forall e\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\forall w\in \mathrm{List}\left(alpha\right),\forall M\in \mathrm{List}\left(Side\right),\left(\mathrm{Trace}\left(a,first,cs,h,e,w,M\right)\wedge cs\ne nil\right)\Rightarrow 1+\mathrm{internalOccupied}\left(e\right)\le \mathrm{rho}\left(M\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/HughesUnaryInsertion.reverse_trace_lower (✓ std3). ∎

Source. Repository-derived.

Commentary.

The first non-a occurrence forces an initial U-group. Every positive internal base count forces a further separator; exterior counts add none.

Theorem 1.12 (Full inserted-unary spectrum).

$$\forall alpha\in \mathrm{Type}\left(\right),\forall a\in alpha,\forall m\in \mathrm{Nat}\left(\right),\forall cs\in \mathrm{List}\left(alpha\right),\forall h\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\left(\left(\forall c\in alpha,c\in cs\Rightarrow c\ne a\right)\wedge \left(\mathrm{length}\left(h\right)=\mathrm{length}\left(cs\right)+1\wedge 1\le m\right)\right)\Rightarrow \left(\forall r\in \mathrm{Nat}\left(\right),r\in \mathrm{spectrum}\left(\mathrm{replicate}\left(m,a\right),\mathrm{gap}\left(a,cs,h\right)\right)\iff \left(1\le r\wedge r\le \min \left(m,\mathrm{length}\left(cs\right)+1\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/HughesUnaryInsertion.inserted_spectrum (✓ std3). ∎

Citation. Charles E. Hughes (2026). Undecidability of Adjacent Equality for Insertion, Shuffle, and Crossover Language Operations. URL: https://arxiv.org/abs/2608.27755v1.

Commentary.

The spectrum is every integer from one to min(m, length(cs)+1), for m>0. Support is bounded by both total mass and gap count. To attain r, put one unit in r-1 gaps, the remaining positive mass in one gap, and zero elsewhere.

Theorem 1.13 (Full reverse-unary spectrum).

$$\forall alpha\in \mathrm{Type}\left(\right),\forall a\in alpha,\forall m\in \mathrm{Nat}\left(\right),\forall cs\in \mathrm{List}\left(alpha\right),\forall h\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\left(\left(\forall c\in alpha,c\in cs\Rightarrow c\ne a\right)\wedge \left(\mathrm{length}\left(h\right)=\mathrm{length}\left(cs\right)+1\wedge \mathrm{gap}\left(a,cs,h\right)\ne nil\right)\right)\Rightarrow \left(\forall r\in \mathrm{Nat}\left(\right),r\in \mathrm{spectrum}\left(\mathrm{gap}\left(a,cs,h\right),\mathrm{replicate}\left(m,a\right)\right)\iff \left(1\le r\wedge r\le 1+\min \left(m,\mathrm{NatSub}\left(\mathrm{length}\left(cs\right),1\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/HughesUnaryInsertion.reverse_spectrum (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a nonempty inserted source the spectrum is every integer from one to 1+min(n, length(cs)-1), with truncated subtraction. Put one unit in each chosen internal gap and all remaining mass at an exterior end. For no non-a occurrences the only value is one.

Definition 1.14 (Equality in every inserted gap).

$$\forall alpha\in \mathrm{Type}\left(\right),\forall a\in alpha,\forall cs\in \mathrm{List}\left(alpha\right),\forall h\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\forall e\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\forall w\in \mathrm{List}\left(alpha\right),\forall M\in \mathrm{List}\left(Side\right),\mathrm{InsertedTight}\left(a,cs,h,e,w,M\right):\mathrm{Prop}\left(\right)$$

Formalization. D5/S1/Words/HughesUnaryInsertion.InsertedTight (✓ std3).

Source. Repository-derived.

Commentary.

This positional trace requires rho(b)=1 in each gap whose inserted count is positive, and rho(b)=0 otherwise. All non-a occurrences have label V. Thus each occupied indexed gap has exactly one whole U-run.

Definition 1.15 (Internal and terminal equality).

$$\forall alpha\in \mathrm{Type}\left(\right),\forall a\in alpha,\forall cs\in \mathrm{List}\left(alpha\right),\forall h\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\forall e\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\forall w\in \mathrm{List}\left(alpha\right),\forall M\in \mathrm{List}\left(Side\right),\mathrm{ReverseTailTight}\left(a,cs,h,e,w,M\right):\mathrm{Prop}\left(\right)$$

Formalization. D5/S1/Words/HughesUnaryInsertion.ReverseTailTight (✓ std3).

Source. Repository-derived.

Commentary.

An internal label gap has the form U^x V^e U^z, with all its base mass e in that single V-block. The terminal gap has form U^x V^y. The internal restart cost is one exactly when e>0, and the terminal restart cost is zero.

Definition 1.16 (Full reverse minimum structure).

$$\forall alpha\in \mathrm{Type}\left(\right),\forall a\in alpha,\forall cs\in \mathrm{List}\left(alpha\right),\forall h\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\forall e\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\forall w\in \mathrm{List}\left(alpha\right),\forall M\in \mathrm{List}\left(Side\right),\mathrm{ReverseTight}\left(a,cs,h,e,w,M\right):\mathrm{Prop}\left(\right)$$

Formalization. D5/S1/Words/HughesUnaryInsertion.ReverseTight (✓ std3).

Source. Repository-derived.

Commentary.

The initial gap is V^x U^y followed by its forced non-a U occurrence, and the remaining trace has the internal and terminal forms above. Every U segment attaches to a bounding non-a occurrence; there is no additional all-a U-run. Outer base material is retained in its actual position.

Theorem 1.17 (Every inserted-unary minimum mask).

$$\forall alpha\in \mathrm{Type}\left(\right),\forall a\in alpha,\forall m\in \mathrm{Nat}\left(\right),\forall cs\in \mathrm{List}\left(alpha\right),\forall h\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\forall e\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\forall w\in \mathrm{List}\left(alpha\right),\forall M\in \mathrm{List}\left(Side\right),\forall r\in \mathrm{Nat}\left(\right),\left(\left(\left(\forall c\in alpha,c\in cs\Rightarrow c\ne a\right)\wedge \left(\mathrm{length}\left(h\right)=\mathrm{length}\left(cs\right)+1\wedge \left(\mathrm{length}\left(e\right)=\mathrm{length}\left(h\right)\wedge \mathrm{sum}\left(e\right)=m\right)\right)\right)\wedge \left(w=\mathrm{gap}\left(a,cs,\mathrm{zipWith}\left(add,h,e\right)\right)\wedge \mathrm{IsMinimumMask}\left(\mathrm{replicate}\left(m,a\right),\mathrm{gap}\left(a,cs,h\right),w,M,r\right)\right)\right)\Rightarrow \mathrm{InsertedTight}\left(a,cs,h,e,w,M\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/HughesUnaryInsertion.inserted_minimum_shape (✓ std3). ∎

Source. Repository-derived.

Commentary.

Comparison with the grouped attaining mask forces equality in each individual gap lower bound, for every minimum mask of the output.

Theorem 1.18 (Every reverse-unary minimum mask).

$$\forall alpha\in \mathrm{Type}\left(\right),\forall a\in alpha,\forall m\in \mathrm{Nat}\left(\right),\forall cs\in \mathrm{List}\left(alpha\right),\forall h\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\forall e\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\forall w\in \mathrm{List}\left(alpha\right),\forall M\in \mathrm{List}\left(Side\right),\forall r\in \mathrm{Nat}\left(\right),\left(\left(\left(\left(\forall c\in alpha,c\in cs\Rightarrow c\ne a\right)\wedge \left(\mathrm{length}\left(h\right)=\mathrm{length}\left(cs\right)+1\wedge \left(\mathrm{length}\left(e\right)=\mathrm{length}\left(h\right)\wedge \mathrm{sum}\left(e\right)=m\right)\right)\right)\wedge cs\ne nil\right)\wedge \left(w=\mathrm{gap}\left(a,cs,\mathrm{zipWith}\left(add,h,e\right)\right)\wedge \mathrm{IsMinimumMask}\left(\mathrm{gap}\left(a,cs,h\right),\mathrm{replicate}\left(m,a\right),w,M,r\right)\right)\right)\Rightarrow \mathrm{ReverseTight}\left(a,cs,h,e,w,M\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/HughesUnaryInsertion.reverse_minimum_shape (✓ std3). ∎

Source. Repository-derived.

Commentary.

With at least one non-a occurrence, equality forces the initial cost one and every internal and terminal cost to be tight. The binary label classification proves the displayed pure-block forms for every minimum mask.

Theorem 1.19 (Spectra of arbitrary actual source words).

$$\forall alpha\in \mathrm{Type}\left(\right),\forall a\in alpha,\forall m\in \mathrm{Nat}\left(\right),\forall n\in \mathrm{Nat}\left(\right),\forall u\in \mathrm{List}\left(alpha\right),\forall v\in \mathrm{List}\left(alpha\right),\left(u\ne nil\wedge \left(v\ne nil\wedge \left(1\le m\wedge 1\le n\right)\right)\right)\Rightarrow \left(\left(\forall r\in \mathrm{Nat}\left(\right),r\in \mathrm{spectrum}\left(\mathrm{replicate}\left(m,a\right),v\right)\iff \left(1\le r\wedge r\le \min \left(m,\mathrm{length}\left(\mathrm{spine}\left(a,v\right)\right)+1\right)\right)\right)\wedge \left(\forall r\in \mathrm{Nat}\left(\right),r\in \mathrm{spectrum}\left(u,\mathrm{replicate}\left(n,a\right)\right)\iff \left(1\le r\wedge r\le 1+\min \left(n,\mathrm{length}\left(\mathrm{spine}\left(a,u\right)\right)-1\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/HughesUnaryInsertion.spectra (✓ std3). ∎

Source. Repository-derived.

Commentary.

For arbitrary nonempty u,v and positive m,n, let s_a(x) be the number of non-a occurrences of the actual word x, counting repetitions. Then D(a^m,v)={r: 1<=r<=min(m,s_a(v)+1)} and D(u,a^n)={r: 1<=r<=1+min(n,s_a(u)-1)}. The occurrence count is recovered from the canonical presentation of each actual source word.

References

• Truth anchor: D5/S1/Words/HughesUnaryInsertion.InsertedTight
• Truth anchor: D5/S1/Words/HughesUnaryInsertion.ReverseTailTight
• Truth anchor: D5/S1/Words/HughesUnaryInsertion.ReverseTight
• Truth anchor: D5/S1/Words/HughesUnaryInsertion.Sh
• Truth anchor: D5/S1/Words/HughesUnaryInsertion.inserted_degree
• Truth anchor: D5/S1/Words/HughesUnaryInsertion.inserted_gap_iff
• Truth anchor: D5/S1/Words/HughesUnaryInsertion.inserted_minimum_shape
• Truth anchor: D5/S1/Words/HughesUnaryInsertion.inserted_spectrum
• Truth anchor: D5/S1/Words/HughesUnaryInsertion.inserted_trace_lower
• Truth anchor: D5/S1/Words/HughesUnaryInsertion.internalOccupied
• Truth anchor: D5/S1/Words/HughesUnaryInsertion.occupied
• Truth anchor: D5/S1/Words/HughesUnaryInsertion.reverse_degree
• Truth anchor: D5/S1/Words/HughesUnaryInsertion.reverse_degree_all
• Truth anchor: D5/S1/Words/HughesUnaryInsertion.reverse_gap_iff
• Truth anchor: D5/S1/Words/HughesUnaryInsertion.reverse_minimum_shape
• Truth anchor: D5/S1/Words/HughesUnaryInsertion.reverse_spectrum
• Truth anchor: D5/S1/Words/HughesUnaryInsertion.reverse_trace_lower
• Truth anchor: D5/S1/Words/HughesUnaryInsertion.spectra
• Truth anchor: D5/S1/Words/HughesUnaryInsertion.spectrum
• Dependency: D5/S1/Words/UnaryGapWords