Floating autosegmental forms

A form is a two-tier autosegmental representation in position coordinates: an upper tier of autosegments over a lower tier of slots, each element sponsored by a morpheme, and a finite set of association lines between positions of the two tiers. Forms concatenate by juxtaposing the tiers and shifting the right factor's lines, and they form a monoid. A form is a computable presentation of a graph-theoretic representation, Form.toAR, and its concatenation is the tensor there, so the No-Crossing Constraint on its lines is Axiom 5 on the graph.

A candidate of a form records the autosegments deleted so far and the current surface lines, the state of a serial optimality-theoretic derivation. GEN acts on candidates and never on the form, so faithfulness constraints compare the surface lines with the form's lines. An autosegment that is neither deleted nor linked on the surface is floating.

Main definitions

• Sponsored α M: a tier element with the morpheme that sponsors it.
• Form S T M: a representation with slots in S, autosegments in T, and sponsors in M; Form.concat and Form.empty make the forms a monoid.
• Form.toAR: the representation a form presents, through AR.ofWords.
• Form.IsTautomorphemic: a line whose autosegment and slot share a sponsor.
• Candidate u: the surface state of a derivation from the form u; Candidate.input is the faithful candidate, and Candidate.gen the one-step GEN.

Main results

• Form.noCrossing_toAR_iff: the presented representation obeys the NCC iff the lines are non-crossing.
• Form.toARConcatIso, Form.clsHom: presenting a concatenation gives the tensor, so presentation is a monoid hom into the representations up to isomorphism.
• Form.isNonCrossing_links_concat: concatenation preserves the No-Crossing Constraint.
• Candidate.isNonCrossing_links_of_mem_gen: GEN is closed on the No-Crossing Constraint.

Implementation notes

Positions are elements of Fin over the tier lengths, so a candidate shares its form's tiers by type and every line is in bounds. Numerals for positions of a concrete form need a NeZero instance for its tier lengths, which a study supplies by decide. The readings of the surface are List.finRange filters, which reduce under kernel decide, because Finset.sort does not unfold structurally. Form.toAR needs the three label types in one universe, as TwoTier does.

References

• [Gol76]
• [Pul86]
• [Wol07]
• [McCMS12]
• [McPL26]
• [Lie83]
• [LK26]
• [Zim17]
• [JH15]
• [Jar16b]

structure Autosegmental.Sponsored (α : Type u_1) (M : Type u_2) : Type (max u_1 u_2)

A Sponsored α M is a tier element of type α together with the morpheme of type M that sponsors it. On the upper tier the element is an autosegment, on the lower tier a slot.

• value : α

  The autosegment or slot.

• morpheme : M

  The sponsoring morpheme.

def Autosegmental.instDecidableEqSponsored.decEq {α✝ : Type u_1} {M✝ : Type u_2} [DecidableEq α✝] [DecidableEq M✝] (x✝ x✝¹ : Sponsored α✝ M✝) : Decidable (x✝ = x✝¹)

Equations

• Autosegmental.instDecidableEqSponsored.decEq { value := a, morpheme := a_1 } { value := b, morpheme := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Autosegmental.instDecidableEqSponsored {α✝ : Type u_1} {M✝ : Type u_2} [DecidableEq α✝] [DecidableEq M✝] : DecidableEq (Sponsored α✝ M✝)

Equations

• Autosegmental.instDecidableEqSponsored = Autosegmental.instDecidableEqSponsored.decEq

def Autosegmental.instReprSponsored.repr {α✝ : Type u_1} {M✝ : Type u_2} [Repr α✝] [Repr M✝] : Sponsored α✝ M✝ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Autosegmental.instReprSponsored {α✝ : Type u_1} {M✝ : Type u_2} [Repr α✝] [Repr M✝] : Repr (Sponsored α✝ M✝)

Equations

• Autosegmental.instReprSponsored = { reprPrec := Autosegmental.instReprSponsored.repr }

structure Autosegmental.Form (S : Type u_1) (T : Type u_2) (M : Type u_3) : Type (max (max u_1 u_2) u_3)

A Form S T M is a two-tier autosegmental representation with slots in S, autosegments in T, and sponsors in M. Its association lines run from positions of the upper tier to positions of the lower tier.

• upper : List (Sponsored T M)

  The upper tier, of autosegments in tier order.

• lower : List (Sponsored S M)

  The lower tier, of slots in tier order.

• links : Finset (Fin self.upper.length × Fin self.lower.length)

  The association lines, each from an autosegment to a slot.

@[instance_reducible]

instance Autosegmental.Form.instDecidableEq {S : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq S] [DecidableEq T] [DecidableEq M] : DecidableEq (Form S T M)

Forms are compared tier by tier and then on their lines, which live over the same positions once the tiers agree.

Equations

• One or more equations did not get rendered due to their size.

theorem Autosegmental.Form.ext {S : Type u_1} {T : Type u_2} {M : Type u_3} {f g : Form S T M} (hu : f.upper = g.upper) (hl : f.lower = g.lower) (h : ∀ (p : Fin f.upper.length × Fin f.lower.length), p ∈ f.links ↔ ((finCongr ⋯) p.1, (finCongr ⋯) p.2) ∈ g.links) : f = g

Two forms are equal when their tiers agree and their lines correspond across the resulting identification of positions.

Morphemes

def Autosegmental.Form.morphemes {S : Type u_1} {T : Type u_2} {M : Type u_3} (f : Form S T M) [DecidableEq M] : Finset M

morphemes f is the set of morphemes sponsoring an element of either tier.

Equations

• f.morphemes = (List.map Autosegmental.Sponsored.morpheme f.lower).toFinset ∪ (List.map Autosegmental.Sponsored.morpheme f.upper).toFinset

def Autosegmental.Form.lowerOfMorpheme {S : Type u_1} {T : Type u_2} {M : Type u_3} (f : Form S T M) [DecidableEq M] (m : M) : List (Fin f.lower.length)

lowerOfMorpheme f m lists the slots sponsored by m in tier order.

Equations

• f.lowerOfMorpheme m = List.filter (fun (i : Fin f.lower.length) => decide (f.lower[i].morpheme = m)) (List.finRange f.lower.length)

@[simp]

theorem Autosegmental.Form.mem_lowerOfMorpheme {S : Type u_1} {T : Type u_2} {M : Type u_3} (f : Form S T M) [DecidableEq M] {m : M} {i : Fin f.lower.length} : i ∈ f.lowerOfMorpheme m ↔ f.lower[i].morpheme = m

def Autosegmental.Form.IsTautomorphemic {S : Type u_1} {T : Type u_2} {M : Type u_3} (f : Form S T M) (l : Fin f.upper.length × Fin f.lower.length) : Prop

A line is tautomorphemic when its autosegment and its slot have the same sponsor. Such lines are the ones *TAUTDOCK penalises.

Equations

• f.IsTautomorphemic l = (f.upper[l.1].morpheme = f.lower[l.2].morpheme)

@[instance_reducible]

instance Autosegmental.Form.instDecidableIsTautomorphemicOfDecidableEq {S : Type u_1} {T : Type u_2} {M : Type u_3} (f : Form S T M) [DecidableEq M] (l : Fin f.upper.length × Fin f.lower.length) : Decidable (f.IsTautomorphemic l)

Equations

• f.instDecidableIsTautomorphemicOfDecidableEq l = Autosegmental.Form.instDecidableIsTautomorphemicOfDecidableEq._aux_1 f l

Concatenation

Concatenation juxtaposes the tiers and shifts the right factor's lines past the left factor's tiers, so the forms are a monoid with the empty form as unit.

def Autosegmental.Form.castAppend {α : Type u_4} (a b : List α) : Fin a.length ↪ Fin (a ++ b).length

The positions of a as the left block of a ++ b.

Equations

• Autosegmental.Form.castAppend a b = { toFun := fun (i : Fin a.length) => ⟨↑i, ⋯⟩, inj' := ⋯ }

def Autosegmental.Form.natAddAppend {α : Type u_4} (a b : List α) : Fin b.length ↪ Fin (a ++ b).length

The positions of b as the right block of a ++ b.

Equations

• Autosegmental.Form.natAddAppend a b = { toFun := fun (i : Fin b.length) => ⟨a.length + ↑i, ⋯⟩, inj' := ⋯ }

@[simp]

theorem Autosegmental.Form.val_castAppend {α : Type u_4} {a b : List α} (i : Fin a.length) : ↑((castAppend a b) i) = ↑i

@[simp]

theorem Autosegmental.Form.val_natAddAppend {α : Type u_4} {a b : List α} (i : Fin b.length) : ↑((natAddAppend a b) i) = a.length + ↑i

def Autosegmental.Form.concat {S : Type u_1} {T : Type u_2} {M : Type u_3} (f g : Form S T M) : Form S T M

concat f g juxtaposes the tiers of f and g and shifts the lines of g past the tiers of f.

Equations

• One or more equations did not get rendered due to their size.

def Autosegmental.Form.empty {S : Type u_1} {T : Type u_2} {M : Type u_3} : Form S T M

The empty form has empty tiers and no lines.

Equations

• Autosegmental.Form.empty = { upper := [], lower := [], links := ∅ }

@[simp]

theorem Autosegmental.Form.concat_upper {S : Type u_1} {T : Type u_2} {M : Type u_3} (f g : Form S T M) : (f.concat g).upper = f.upper ++ g.upper

@[simp]

theorem Autosegmental.Form.concat_lower {S : Type u_1} {T : Type u_2} {M : Type u_3} (f g : Form S T M) : (f.concat g).lower = f.lower ++ g.lower

@[simp]

theorem Autosegmental.Form.empty_upper {S : Type u_1} {T : Type u_2} {M : Type u_3} : empty.upper = []

@[simp]

theorem Autosegmental.Form.empty_lower {S : Type u_1} {T : Type u_2} {M : Type u_3} : empty.lower = []

@[simp]

theorem Autosegmental.Form.empty_links {S : Type u_1} {T : Type u_2} {M : Type u_3} : empty.links = ∅

theorem Autosegmental.Form.mem_links_concat {S : Type u_1} {T : Type u_2} {M : Type u_3} {f g : Form S T M} {p : Fin (f.concat g).upper.length × Fin (f.concat g).lower.length} : p ∈ (f.concat g).links ↔ (∃ q ∈ f.links, ↑q.1 = ↑p.1 ∧ ↑q.2 = ↑p.2) ∨ ∃ q ∈ g.links, f.upper.length + ↑q.1 = ↑p.1 ∧ f.lower.length + ↑q.2 = ↑p.2

A line of a concatenation is a line of the left factor, or a line of the right factor shifted past the left factor's tiers.

theorem Autosegmental.Form.concat_assoc {S : Type u_1} {T : Type u_2} {M : Type u_3} (f g h : Form S T M) : (f.concat g).concat h = f.concat (g.concat h)

theorem Autosegmental.Form.empty_concat {S : Type u_1} {T : Type u_2} {M : Type u_3} (f : Form S T M) : empty.concat f = f

theorem Autosegmental.Form.concat_empty {S : Type u_1} {T : Type u_2} {M : Type u_3} (f : Form S T M) : f.concat empty = f

@[instance_reducible]

instance Autosegmental.Form.instMonoid {S : Type u_1} {T : Type u_2} {M : Type u_3} : Monoid (Form S T M)

Forms are a monoid under concatenation, with the empty form as unit.

Equations

• Autosegmental.Form.instMonoid = { one := Autosegmental.Form.empty, mul := Autosegmental.Form.concat, mul_assoc := ⋯, one_mul := ⋯, mul_one := ⋯, npow_zero := ⋯, npow_succ := ⋯ }

@[simp]

theorem Autosegmental.Form.mul_eq_concat {S : Type u_1} {T : Type u_2} {M : Type u_3} (f g : Form S T M) : f * g = f.concat g

@[simp]

theorem Autosegmental.Form.one_eq_empty {S : Type u_1} {T : Type u_2} {M : Type u_3} : 1 = empty

The presented representation

A form presents the two-tier representation AR.ofWords builds from its tiers and its lines in ℕ coordinates.

def Autosegmental.Form.lines {S : Type u_1} {T : Type u_2} {M : Type u_3} (f : Form S T M) : Finset (ℕ × ℕ)

The lines of a form in ℕ coordinates.

Equations

• f.lines = Finset.map (Fin.valEmbedding.prodMap Fin.valEmbedding) f.links

@[simp]

theorem Autosegmental.Form.mem_lines {S : Type u_1} {T : Type u_2} {M : Type u_3} {f : Form S T M} {p : ℕ × ℕ} : p ∈ f.lines ↔ ∃ q ∈ f.links, ↑q.1 = p.1 ∧ ↑q.2 = p.2

theorem Autosegmental.Form.lt_of_mem_lines {S : Type u_1} {T : Type u_2} {M : Type u_3} (f : Form S T M) {p : ℕ × ℕ} (h : p ∈ f.lines) : p.1 < f.upper.length ∧ p.2 < f.lower.length

theorem Autosegmental.Form.isNonCrossing_lines_iff {S : Type u_1} {T : Type u_2} {M : Type u_3} (f : Form S T M) : IsNonCrossing f.lines ↔ IsNonCrossing f.links

def Autosegmental.Form.toAR {S T M : Type u} (f : Form S T M) : TieredAR Bool (TwoTier (Sponsored T M) (Sponsored S M))

The representation a form presents, with the sponsors on its labels.

Equations

• f.toAR = Autosegmental.AR.ofWords f.upper f.lower fun (p q : ℕ) => (p, q) ∈ f.lines

instance Autosegmental.Form.instFiniteVSigmaBoolTwoTierSponsoredObjGraphAndIsTierOrderedArcsTierFstNoInternalAssocEdgesToAR {S T M : Type u} (f : Form S T M) : Finite f.toAR.obj.V

@[simp]

theorem Autosegmental.Form.tierWord_toAR_true {S T M : Type u} (f : Form S T M) : AR.tierWord true = f.upper

@[simp]

theorem Autosegmental.Form.tierWord_toAR_false {S T M : Type u} (f : Form S T M) : AR.tierWord false = f.lower

@[simp]

theorem Autosegmental.Form.tierLength_toAR_true {S T M : Type u} (f : Form S T M) : AR.tierLength f.toAR true = f.upper.length

@[simp]

theorem Autosegmental.Form.tierLength_toAR_false {S T M : Type u} (f : Form S T M) : AR.tierLength f.toAR false = f.lower.length

@[simp]

theorem Autosegmental.Form.link_toAR {S T M : Type u} (f : Form S T M) {p q : ℕ} : AR.link f.toAR true false p q ↔ (p, q) ∈ f.lines

theorem Autosegmental.Form.noCrossing_toAR_iff {S T M : Type u} (f : Form S T M) : NoCrossing f.toAR.obj.edges f.toAR.obj.arcs ↔ IsNonCrossing f.links

The presented representation obeys the NCC iff the lines are non-crossing.

noncomputable def Autosegmental.Form.toARConcatIso {S T M : Type u} (f g : Form S T M) : (f.concat g).toAR.obj.Iso (CategoryTheory.MonoidalCategoryStruct.tensorObj f.toAR g.toAR).obj

A concatenation presents the tensor of the presented representations.

Equations

• f.toARConcatIso g = Autosegmental.AR.fullIsoOfReaderEq ⋯ ⋯

theorem Autosegmental.Form.isNonCrossing_links_concat {S T M : Type u} (f g : Form S T M) (h₁ : IsNonCrossing f.links) (h₂ : IsNonCrossing g.links) : IsNonCrossing (f.concat g).links

Concatenation preserves the No-Crossing Constraint, as concatenation of representations does ([Jar16b] Theorem 4).

noncomputable def Autosegmental.Form.toAREmptyIso {S T M : Type u} : empty.toAR.obj.Iso (CategoryTheory.MonoidalCategoryStruct.tensorUnit (TieredAR Bool (TwoTier (Sponsored T M) (Sponsored S M)))).obj

The empty form presents the unit.

Equations

• Autosegmental.Form.toAREmptyIso = Autosegmental.AR.fullIsoOfReaderEq ⋯ ⋯

noncomputable def Autosegmental.Form.clsHom {S T M : Type u} : Form S T M →* CategoryTheory.Skeleton (PrecAR Bool (TwoTier (Sponsored T M) (Sponsored S M)))

Presentation is a monoid hom from forms to representations up to isomorphism, so the strict monoid of forms models concatenation of representations.

Equations

• Autosegmental.Form.clsHom = { toFun := fun (f : Autosegmental.Form S T M) => Autosegmental.AR.cls f.toAR, map_one' := ⋯, map_mul' := ⋯ }

structure Autosegmental.Candidate {S : Type u_1} {T : Type u_2} {M : Type u_3} (u : Form S T M) : Type

A Candidate u is the surface state of a derivation from the form u, recording the autosegments deleted so far and the current surface lines. The faithful candidate is Candidate.input u, and GEN edits candidates while u stays fixed.

• deleted : Finset (Fin u.upper.length)

  The autosegments deleted on the surface.

• links : Finset (Fin u.upper.length × Fin u.lower.length)

  The surface association lines.

@[instance_reducible]

instance Autosegmental.instDecidableEqCandidate {S✝ : Type u_1} {T✝ : Type u_2} {M✝ : Type u_3} {u✝ : Form S✝ T✝ M✝} [DecidableEq S✝] [DecidableEq T✝] [DecidableEq M✝] : DecidableEq (Candidate u✝)

Equations

• Autosegmental.instDecidableEqCandidate = Autosegmental.instDecidableEqCandidate.decEq

def Autosegmental.instDecidableEqCandidate.decEq {S✝ : Type u_1} {T✝ : Type u_2} {M✝ : Type u_3} {u✝ : Form S✝ T✝ M✝} [DecidableEq S✝] [DecidableEq T✝] [DecidableEq M✝] (x✝ x✝¹ : Candidate u✝) : Decidable (x✝ = x✝¹)

Equations

• Autosegmental.instDecidableEqCandidate.decEq { deleted := a, links := a_1 } { deleted := b, links := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Autosegmental.Candidate.input {S : Type u_1} {T : Type u_2} {M : Type u_3} (u : Form S T M) : Candidate u

input u is the faithful candidate of u, with nothing deleted and the form's lines as its surface lines.

Equations

• Autosegmental.Candidate.input u = { deleted := ∅, links := u.links }

@[simp]

theorem Autosegmental.Candidate.input_deleted {S : Type u_1} {T : Type u_2} {M : Type u_3} (u : Form S T M) : (input u).deleted = ∅

@[simp]

theorem Autosegmental.Candidate.input_links {S : Type u_1} {T : Type u_2} {M : Type u_3} (u : Form S T M) : (input u).links = u.links

Surface predicates

def Autosegmental.Candidate.IsLinked {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} (c : Candidate u) (k : Fin u.upper.length) : Prop

Autosegment k is linked when it bears a surface line.

Equations

• c.IsLinked k = ∃ l ∈ c.links, l.1 = k

def Autosegmental.Candidate.IsLinkedLower {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} (c : Candidate u) (i : Fin u.lower.length) : Prop

Slot i is linked when it bears a surface line.

Equations

• c.IsLinkedLower i = ∃ l ∈ c.links, l.2 = i

def Autosegmental.Candidate.IsFloating {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} (c : Candidate u) (k : Fin u.upper.length) : Prop

Autosegment k is floating when it is not deleted and bears no surface line.

Equations

• c.IsFloating k = (k ∉ c.deleted ∧ ¬c.IsLinked k)

def Autosegmental.Candidate.insertedLinks {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} (c : Candidate u) : Finset (Fin u.upper.length × Fin u.lower.length)

insertedLinks c is the set of surface lines absent from the form, which GEN has inserted and DEP counts.

Equations

• c.insertedLinks = c.links \ u.links

def Autosegmental.Candidate.deletedLinks {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} (c : Candidate u) : Finset (Fin u.upper.length × Fin u.lower.length)

deletedLinks c is the set of the form's lines absent from the surface, which GEN has deleted and MAX counts.

Equations

• c.deletedLinks = u.links \ c.links

@[instance_reducible]

instance Autosegmental.Candidate.instDecidableIsLinked {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} (c : Candidate u) {k : Fin u.upper.length} : Decidable (c.IsLinked k)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Autosegmental.Candidate.instDecidableIsLinkedLower {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} (c : Candidate u) {i : Fin u.lower.length} : Decidable (c.IsLinkedLower i)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Autosegmental.Candidate.instDecidableIsFloating {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} (c : Candidate u) {k : Fin u.upper.length} : Decidable (c.IsFloating k)

Equations

• c.instDecidableIsFloating = { decide := decide (k ∉ c.deleted) && decide ¬c.IsLinked k, reflects_decide := ⋯ }

theorem Autosegmental.Candidate.isLinked_iff {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} {c : Candidate u} {k : Fin u.upper.length} : c.IsLinked k ↔ ∃ (i : Fin u.lower.length), (k, i) ∈ c.links

theorem Autosegmental.Candidate.isLinkedLower_iff {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} {c : Candidate u} {i : Fin u.lower.length} : c.IsLinkedLower i ↔ ∃ (k : Fin u.upper.length), (k, i) ∈ c.links

@[simp]

theorem Autosegmental.Candidate.mem_insertedLinks {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} {c : Candidate u} {l : Fin u.upper.length × Fin u.lower.length} : l ∈ c.insertedLinks ↔ l ∈ c.links ∧ l ∉ u.links

@[simp]

theorem Autosegmental.Candidate.mem_deletedLinks {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} {c : Candidate u} {l : Fin u.upper.length × Fin u.lower.length} : l ∈ c.deletedLinks ↔ l ∈ u.links ∧ l ∉ c.links

@[simp]

theorem Autosegmental.Candidate.insertedLinks_input {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} : (input u).insertedLinks = ∅

The faithful candidate has no inserted line.

@[simp]

theorem Autosegmental.Candidate.deletedLinks_input {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} : (input u).deletedLinks = ∅

The faithful candidate has no deleted line.

Reading the surface

The readings of the surface are lists over List.finRange in tier order, which reduce under kernel decide.

def Autosegmental.Candidate.linksTo {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} (c : Candidate u) (i : Fin u.lower.length) : List (Fin u.upper.length)

linksTo c i lists the autosegments linked to slot i on the surface, in tier order.

Equations

• c.linksTo i = List.filter (fun (k : Fin u.upper.length) => decide ((k, i) ∈ c.links)) (List.finRange u.upper.length)

def Autosegmental.Candidate.tierValues {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} (c : Candidate u) (i : Fin u.lower.length) : List T

tierValues c i lists the values of the autosegments linked to slot i on the surface, in tier order.

Equations

• c.tierValues i = List.map (fun (k : Fin u.upper.length) => u.upper[k].value) (c.linksTo i)

def Autosegmental.Candidate.alive {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} (c : Candidate u) : List (Fin u.upper.length)

alive c lists the undeleted autosegments in tier order.

Equations

• c.alive = List.filter (fun (x : Fin u.upper.length) => decide (x ∉ c.deleted)) (List.finRange u.upper.length)

@[simp]

theorem Autosegmental.Candidate.mem_linksTo {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} {c : Candidate u} {k : Fin u.upper.length} {i : Fin u.lower.length} : k ∈ c.linksTo i ↔ (k, i) ∈ c.links

theorem Autosegmental.Candidate.nodup_linksTo {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} (c : Candidate u) (i : Fin u.lower.length) : (c.linksTo i).Nodup

@[simp]

theorem Autosegmental.Candidate.mem_tierValues {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} {c : Candidate u} {i : Fin u.lower.length} {t : T} : t ∈ c.tierValues i ↔ ∃ (k : Fin u.upper.length), (k, i) ∈ c.links ∧ u.upper[k].value = t

@[simp]

theorem Autosegmental.Candidate.mem_alive {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} {c : Candidate u} {k : Fin u.upper.length} : k ∈ c.alive ↔ k ∉ c.deleted

The atomic GEN operations

def Autosegmental.Candidate.deleteTierElem {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} (c : Candidate u) (k : Fin u.upper.length) : Candidate u

deleteTierElem c k deletes autosegment k on the surface, together with every surface line it bears.

Equations

• c.deleteTierElem k = { deleted := insert k c.deleted, links := {x ∈ c.links | x.1 ≠ k} }

@[simp]

theorem Autosegmental.Candidate.deleteTierElem_links {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} (c : Candidate u) (k : Fin u.upper.length) : (c.deleteTierElem k).links = {x ∈ c.links | x.1 ≠ k}

@[simp]

theorem Autosegmental.Candidate.deleteTierElem_deleted {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} (c : Candidate u) (k : Fin u.upper.length) : (c.deleteTierElem k).deleted = insert k c.deleted

def Autosegmental.Candidate.insertLink {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} (c : Candidate u) (k : Fin u.upper.length) (i : Fin u.lower.length) : Candidate u

insertLink c k i inserts the surface line from autosegment k to slot i.

Equations

• c.insertLink k i = { deleted := c.deleted, links := insert (k, i) c.links }

@[simp]

theorem Autosegmental.Candidate.insertLink_deleted {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} (c : Candidate u) (k : Fin u.upper.length) (i : Fin u.lower.length) : (c.insertLink k i).deleted = c.deleted

@[simp]

theorem Autosegmental.Candidate.insertLink_links {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} (c : Candidate u) (k : Fin u.upper.length) (i : Fin u.lower.length) : (c.insertLink k i).links = insert (k, i) c.links

def Autosegmental.Candidate.deleteLink {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} (c : Candidate u) (k : Fin u.upper.length) (i : Fin u.lower.length) : Candidate u

deleteLink c k i deletes the surface line from autosegment k to slot i.

Equations

• c.deleteLink k i = { deleted := c.deleted, links := c.links.erase (k, i) }

@[simp]

theorem Autosegmental.Candidate.deleteLink_deleted {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} (c : Candidate u) (k : Fin u.upper.length) (i : Fin u.lower.length) : (c.deleteLink k i).deleted = c.deleted

@[simp]

theorem Autosegmental.Candidate.deleteLink_links {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} (c : Candidate u) (k : Fin u.upper.length) (i : Fin u.lower.length) : (c.deleteLink k i).links = c.links.erase (k, i)

@[simp]

theorem Autosegmental.Candidate.isLinked_deleteTierElem {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} {c : Candidate u} {k j : Fin u.upper.length} : (c.deleteTierElem k).IsLinked j ↔ j ≠ k ∧ c.IsLinked j

@[simp]

theorem Autosegmental.Candidate.isLinked_insertLink {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} {c : Candidate u} {k j : Fin u.upper.length} {i : Fin u.lower.length} : (c.insertLink k i).IsLinked j ↔ j = k ∨ c.IsLinked j

@[simp]

theorem Autosegmental.Candidate.isLinkedLower_insertLink {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} {c : Candidate u} {k : Fin u.upper.length} {i i' : Fin u.lower.length} : (c.insertLink k i).IsLinkedLower i' ↔ i' = i ∨ c.IsLinkedLower i'

@[simp]

theorem Autosegmental.Candidate.isFloating_deleteTierElem {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} {c : Candidate u} {k j : Fin u.upper.length} : (c.deleteTierElem k).IsFloating j ↔ j ≠ k ∧ c.IsFloating j

@[simp]

theorem Autosegmental.Candidate.isFloating_insertLink {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} {c : Candidate u} {k j : Fin u.upper.length} {i : Fin u.lower.length} : (c.insertLink k i).IsFloating j ↔ j ≠ k ∧ c.IsFloating j

theorem Autosegmental.Candidate.links_deleteTierElem_subset {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} {c : Candidate u} {k : Fin u.upper.length} : (c.deleteTierElem k).links ⊆ c.links

theorem Autosegmental.Candidate.links_subset_insertLink {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} {c : Candidate u} {k : Fin u.upper.length} {i : Fin u.lower.length} : c.links ⊆ (c.insertLink k i).links

One-step GEN

def Autosegmental.Candidate.gen {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} [DecidableEq S] [DecidableEq T] [DecidableEq M] (c : Candidate u) : Finset (Candidate u)

gen c is the one-step GEN of harmonic serialism. It contains c itself, the deletion of each undeleted autosegment, and each line from a floating autosegment to a slot that crosses no surface line; insert-and-associate and shift are omitted.

Equations

• One or more equations did not get rendered due to their size.

theorem Autosegmental.Candidate.mem_gen {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} {c : Candidate u} [DecidableEq S] [DecidableEq T] [DecidableEq M] {c' : Candidate u} : c' ∈ c.gen ↔ c' = c ∨ (∃ k ∉ c.deleted, c' = c.deleteTierElem k) ∨ ∃ (k : Fin u.upper.length) (i : Fin u.lower.length), c.IsFloating k ∧ ¬IndexCrosses c.links (k, i) ∧ c' = c.insertLink k i

@[simp]

theorem Autosegmental.Candidate.self_mem_gen {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} {c : Candidate u} [DecidableEq S] [DecidableEq T] [DecidableEq M] : c ∈ c.gen

theorem Autosegmental.Candidate.deleteTierElem_mem_gen {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} {c : Candidate u} {k : Fin u.upper.length} [DecidableEq S] [DecidableEq T] [DecidableEq M] (hd : k ∉ c.deleted) : c.deleteTierElem k ∈ c.gen

theorem Autosegmental.Candidate.insertLink_mem_gen {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} {c : Candidate u} {k : Fin u.upper.length} {i : Fin u.lower.length} [DecidableEq S] [DecidableEq T] [DecidableEq M] (hk : c.IsFloating k) (hx : ¬IndexCrosses c.links (k, i)) : c.insertLink k i ∈ c.gen

theorem Autosegmental.Candidate.deleted_subset_of_mem_gen {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} {c : Candidate u} [DecidableEq S] [DecidableEq T] [DecidableEq M] {c' : Candidate u} (hc : c' ∈ c.gen) : c.deleted ⊆ c'.deleted

GEN never resurrects a deleted autosegment.

theorem Autosegmental.Candidate.isNonCrossing_links_of_mem_gen {S : Type u_1} {T : Type u_2} {M : Type u_3} {u : Form S T M} {c : Candidate u} [DecidableEq S] [DecidableEq T] [DecidableEq M] {c' : Candidate u} (h : IsNonCrossing c.links) (hc : c' ∈ c.gen) : IsNonCrossing c'.links

GEN is closed on the No-Crossing Constraint, since deletion shrinks the surface lines and each inserted line passed the crossing filter.