Siptár and Törkenczy (2000): The Phonology of Hungarian

This file formalizes the analysis of vowel harmony in chapter 6 of [ST00] and runs it on the derivations the chapter gives. A stem is a sequence of vocalic nodes with the unary place features COR, LAB and DOR of [CH95b] either prelinked to nodes or floating on the morpheme, and a suffix vowel is a node carrying a linked LAB or placeless, with its aperture. Four rules apply in order: Link DOR and Link Place associate a floating feature, unboundedly, to every node it may reach; Spread DOR and Spread Place extend an anchored feature to the adjacent node, iterating left to right; and a node still placeless is coronal by default. Throughout, DOR may join any node without COR, COR only a placeless node, and LAB any node without DOR that is not low (MayLink, linkDor, linkPlace, spreadDor, spreadPlace, derive). The rules only add association lines and never put COR and DOR on one node (links_subset_derive, derive_sound). The eleven stem representations of the chapter's Table 18 with the four suffixes of its (2) yield the forty-four suffixed forms of its (13) to (23) (derivations), transparency, antiharmony and opacity following from the prelinking alone, and the vacillating stem of section 3.2.3.1 has two representations deriving its two forms (dzsungel_vacillates). The surface generalization of section 3.2, that the last harmonic vowel governs suffix backness through the transparent neutral vowels, is the Fragment's palatalHarmony; it agrees with the derivations on the regular stems and is silent or wrong exactly on the neutral, antiharmonic and opaque stems the analysis handles by prelinking (sourceValue_agrees, sourceValue_viz, sourceValue_hid, sourceValue_kodex).

Implementation notes

• Words are the substrate's Form with vocalic nodes for the backbone, place features for the tier and the stem and suffix as sponsors, and the rules act on its Candidates; a rule inserts association lines, and the derivation composes the rules in the chapter's order. Default COR is read at the surface, a placeless node counting as coronal. Where the chapter has COR and LAB spread together onto one node, COR spreads first and LAB joins it.
• A word is a stem and one suffix; the chapter's stems have at most two vowels and its suffixes one, and a prelinked feature is one tier element per node it is linked to. Apertures are read from the vowel letters and matter only through the constraint against a low labial node; long vowels are not distinguished.
• The forms are rows of Data/Forms/SiptarTorkenczy2000.json; a derivation is compared with the suffixed form's segments after the stem's, since three of the chapter's forms shorten the stem vowel.

References

• [ST00]
• [CH95b]
• [RW11]

inductive SiptarTorkenczy2000.Place : Type

The unary place features of the vowels, (1) of the chapter.

• cor : Place
• lab : Place
• dor : Place

@[instance_reducible]

instance SiptarTorkenczy2000.instDecidableEqPlace : DecidableEq Place

Equations

• SiptarTorkenczy2000.instDecidableEqPlace x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance SiptarTorkenczy2000.instFintypePlace : Fintype Place

Equations

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

structure SiptarTorkenczy2000.VNode : Type

A vocalic node with its aperture features.

• open1 : Bool
• open2 : Bool

@[instance_reducible]

instance SiptarTorkenczy2000.instDecidableEqVNode : DecidableEq VNode

Equations

• SiptarTorkenczy2000.instDecidableEqVNode = SiptarTorkenczy2000.instDecidableEqVNode.decEq

def SiptarTorkenczy2000.instDecidableEqVNode.decEq (x✝ x✝¹ : VNode) : Decidable (x✝ = x✝¹)

Equations

• SiptarTorkenczy2000.instDecidableEqVNode.decEq { open1 := a, open2 := a_1 } { open1 := b, open2 := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def SiptarTorkenczy2000.VNode.ofLetter (l : String) : VNode

The aperture of the vowel a letter writes. The high vowels are closed on both features, the mid vowels and é open on the second, and the low vowels and e open on both.

Equations

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

inductive SiptarTorkenczy2000.Morph : Type

The sponsors of a word's material.

• stem : Morph
• suffix : Morph

@[instance_reducible]

instance SiptarTorkenczy2000.instDecidableEqMorph : DecidableEq Morph

Equations

• SiptarTorkenczy2000.instDecidableEqMorph x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[reducible, inline]

abbrev SiptarTorkenczy2000.Word : Type

A phonological word is an autosegmental form over vocalic nodes and place features.

Equations

• SiptarTorkenczy2000.Word = Autosegmental.Form SiptarTorkenczy2000.VNode SiptarTorkenczy2000.Place SiptarTorkenczy2000.Morph

The rules

def SiptarTorkenczy2000.places {w : Word} (c : Autosegmental.Candidate w) (i : Fin w.lower.length) : List Place

The place features linked to the i-th node.

Equations

• SiptarTorkenczy2000.places c i = c.tierValues i

def SiptarTorkenczy2000.isLow {w : Word} (i : Fin w.lower.length) : Bool

Whether the i-th node is low.

Equations

• SiptarTorkenczy2000.isLow i = w.lower[i].value.open1

def SiptarTorkenczy2000.valueAt {w : Word} (k : Fin w.upper.length) : Place

The value of the k-th tier element.

Equations

• SiptarTorkenczy2000.valueAt k = w.upper[k].value

def SiptarTorkenczy2000.MayLink {w : Word} (c : Autosegmental.Candidate w) (p : Place) (i : Fin w.lower.length) : Prop

Where a place feature may associate, principles (7c) and (7d) under constraints (6a) and (6b): DOR to any node without COR, COR to a placeless node, LAB to a node without DOR that is not low.

Equations

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

@[instance_reducible]

instance SiptarTorkenczy2000.instDecidableMayLink {w : Word} (c : Autosegmental.Candidate w) (p : Place) (i : Fin w.lower.length) : Decidable (MayLink c p i)

Equations

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

def SiptarTorkenczy2000.linkAll {w : Word} (c : Autosegmental.Candidate w) (k : Fin w.upper.length) (p : Place) : Autosegmental.Candidate w

Associate tier element k, bearing p, to every node it may link to.

Equations

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

def SiptarTorkenczy2000.floating {w : Word} (c : Autosegmental.Candidate w) (p : Place) : List (Fin w.upper.length)

The floating tier elements bearing p.

Equations

• SiptarTorkenczy2000.floating c p = List.filter (fun (k : Fin w.upper.length) => decide (c.IsFloating k ∧ SiptarTorkenczy2000.valueAt k = p)) (List.finRange w.upper.length)

def SiptarTorkenczy2000.linkDor {w : Word} (c : Autosegmental.Candidate w) : Autosegmental.Candidate w

By Link DOR (3b), every floating DOR associates to every node without COR.

Equations

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

def SiptarTorkenczy2000.linkPlace {w : Word} (c : Autosegmental.Candidate w) : Autosegmental.Candidate w

By Link Place (3a), every floating place feature associates to every node it may link to.

Equations

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

def SiptarTorkenczy2000.anchored {w : Word} (c : Autosegmental.Candidate w) (p : Place) (i : Fin w.lower.length) : Option (Fin w.upper.length)

The tier element bearing p anchored on node i.

Equations

• SiptarTorkenczy2000.anchored c p i = List.find? (fun (k : Fin w.upper.length) => decide (SiptarTorkenczy2000.valueAt k = p)) (c.linksTo i)

def SiptarTorkenczy2000.spreadAt {w : Word} (c : Autosegmental.Candidate w) (p : Place) (i : Fin w.lower.length) : Autosegmental.Candidate w

Spread p from node i to the next node when it is anchored on i and may link there.

Equations

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

def SiptarTorkenczy2000.spreadDor {w : Word} (c : Autosegmental.Candidate w) : Autosegmental.Candidate w

By Spread DOR (4b), iterating left to right, an anchored DOR extends to the next node.

Equations

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

def SiptarTorkenczy2000.spreadPlace {w : Word} (c : Autosegmental.Candidate w) : Autosegmental.Candidate w

By Spread Place (4a), iterating left to right, an anchored COR extends to the next node when it is placeless, and an anchored LAB when it bears no DOR and is not low.

Equations

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

def SiptarTorkenczy2000.derive {w : Word} (c : Autosegmental.Candidate w) : Autosegmental.Candidate w

The derivation applies the linking rules, the DOR rule first, and then the spreading rules.

Equations

• SiptarTorkenczy2000.derive c = SiptarTorkenczy2000.spreadPlace (SiptarTorkenczy2000.spreadDor (SiptarTorkenczy2000.linkPlace (SiptarTorkenczy2000.linkDor c)))

inductive SiptarTorkenczy2000.Quality : Type

A node surfaces back with DOR, front rounded with LAB alone, and front unrounded with COR or, by Default COR (5), when placeless.

• back : Quality
• frontRounded : Quality
• frontUnrounded : Quality

@[instance_reducible]

instance SiptarTorkenczy2000.instDecidableEqQuality : DecidableEq Quality

Equations

• SiptarTorkenczy2000.instDecidableEqQuality x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def SiptarTorkenczy2000.quality (ps : List Place) : Quality

The quality of a place specification.

Equations

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

Structural properties

def SiptarTorkenczy2000.Sound {w : Word} (g : Autosegmental.Candidate w) : Prop

By constraint (6a), no node bears both COR and DOR.

Equations

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

theorem SiptarTorkenczy2000.mem_places_insertLink {w : Word} {c : Autosegmental.Candidate w} {p : Place} {k : Fin w.upper.length} {i j : Fin w.lower.length} : p ∈ places (c.insertLink k i) j ↔ p ∈ places c j ∨ j = i ∧ valueAt k = p

theorem SiptarTorkenczy2000.Sound.insertLink {w : Word} {c : Autosegmental.Candidate w} {p : Place} {k : Fin w.upper.length} {i : Fin w.lower.length} (hs : Sound c) (hv : valueAt k = p) (hm : MayLink c p i) : Sound (c.insertLink k i)

Inserting a line admitted by MayLink keeps the form sound.

structure SiptarTorkenczy2000.Preserves {w : Word} (f g : Autosegmental.Candidate w) : Prop

Every rule preserves the association lines and soundness.

• subset : f.links ⊆ g.links
• sound : Sound f → Sound g

theorem SiptarTorkenczy2000.Preserves.refl {w : Word} {c : Autosegmental.Candidate w} : Preserves c c

theorem SiptarTorkenczy2000.Preserves.trans {w : Word} {c g h : Autosegmental.Candidate w} (h₁ : Preserves c g) (h₂ : Preserves g h) : Preserves c h

theorem SiptarTorkenczy2000.Preserves.insertLink {w : Word} {c : Autosegmental.Candidate w} {p : Place} {k : Fin w.upper.length} {i : Fin w.lower.length} (hv : valueAt k = p) (hm : MayLink c p i) : Preserves c (c.insertLink k i)

theorem SiptarTorkenczy2000.preserves_linkAll {w : Word} {c : Autosegmental.Candidate w} {k : Fin w.upper.length} {p : Place} (hv : valueAt k = p) : Preserves c (linkAll c k p)

theorem SiptarTorkenczy2000.preserves_linkDor {w : Word} {c : Autosegmental.Candidate w} : Preserves c (linkDor c)

theorem SiptarTorkenczy2000.preserves_linkPlace {w : Word} {c : Autosegmental.Candidate w} : Preserves c (linkPlace c)

theorem SiptarTorkenczy2000.preserves_spreadAt {w : Word} {c : Autosegmental.Candidate w} (p : Place) (i : Fin w.lower.length) : Preserves c (spreadAt c p i)

theorem SiptarTorkenczy2000.preserves_spreadDor {w : Word} {c : Autosegmental.Candidate w} : Preserves c (spreadDor c)

theorem SiptarTorkenczy2000.preserves_spreadPlace {w : Word} {c : Autosegmental.Candidate w} : Preserves c (spreadPlace c)

theorem SiptarTorkenczy2000.preserves_derive {w : Word} {c : Autosegmental.Candidate w} : Preserves c (derive c)

theorem SiptarTorkenczy2000.links_subset_derive {w : Word} {c : Autosegmental.Candidate w} : c.links ⊆ (derive c).links

The rules only add association lines.

theorem SiptarTorkenczy2000.derive_sound {w : Word} {c : Autosegmental.Candidate w} (hs : Sound c) : Sound (derive c)

The rules never put COR and DOR on one node.

Stems and suffixes

structure SiptarTorkenczy2000.Stem : Type

A stem's underlying representation in Table 18 gives for each vowel its aperture and the place features prelinked to it, and the floating place features of the morpheme.

• nodes : List (VNode × List Place)
• floating : List Place

def SiptarTorkenczy2000.Stem.ofRow (row : Data.Forms.Form Forms.Cell) (linked : List (List Place)) (floating : List Place) : Stem

The representation of a stem row whose vowels bear the given prelinked features.

Equations

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

inductive SiptarTorkenczy2000.Suffix : Type

Of the suffixes of the derivations, (2), the possessive ü/u and the ablative ö/o carry a linked LAB, and the dative e/a, the allative ö/o/e and the inessive e/a are placeless.

• poss : Suffix
• abl : Suffix
• dat : Suffix
• all : Suffix
• iness : Suffix

@[instance_reducible]

instance SiptarTorkenczy2000.instDecidableEqSuffix : DecidableEq Suffix

Equations

• SiptarTorkenczy2000.instDecidableEqSuffix x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def SiptarTorkenczy2000.Suffix.node : Suffix → VNode

The suffix vowel's aperture.

Equations

• SiptarTorkenczy2000.Suffix.poss.node = { open1 := false, open2 := false }
• SiptarTorkenczy2000.Suffix.abl.node = { open1 := false, open2 := true }
• SiptarTorkenczy2000.Suffix.all.node = { open1 := false, open2 := true }
• SiptarTorkenczy2000.Suffix.dat.node = { open1 := true, open2 := true }
• SiptarTorkenczy2000.Suffix.iness.node = { open1 := true, open2 := true }

def SiptarTorkenczy2000.Suffix.hasLab : Suffix → Bool

Whether the suffix vowel carries a linked LAB.

Equations

• SiptarTorkenczy2000.Suffix.poss.hasLab = true
• SiptarTorkenczy2000.Suffix.abl.hasLab = true
• SiptarTorkenczy2000.Suffix.dat.hasLab = false
• SiptarTorkenczy2000.Suffix.all.hasLab = false
• SiptarTorkenczy2000.Suffix.iness.hasLab = false

def SiptarTorkenczy2000.Suffix.segments : Suffix → Quality → Option (List String)

The segments of a suffix at a harmonic quality, none where that quality cannot arise.

Equations

• SiptarTorkenczy2000.Suffix.poss.segments SiptarTorkenczy2000.Quality.back = some ["u", "n", "k"]
• SiptarTorkenczy2000.Suffix.poss.segments SiptarTorkenczy2000.Quality.frontRounded = some ["ü", "n", "k"]
• SiptarTorkenczy2000.Suffix.abl.segments SiptarTorkenczy2000.Quality.back = some ["t", "ó", "l"]
• SiptarTorkenczy2000.Suffix.abl.segments SiptarTorkenczy2000.Quality.frontRounded = some ["t", "ő", "l"]
• SiptarTorkenczy2000.Suffix.dat.segments SiptarTorkenczy2000.Quality.back = some ["n", "a", "k"]
• SiptarTorkenczy2000.Suffix.dat.segments SiptarTorkenczy2000.Quality.frontUnrounded = some ["n", "e", "k"]
• SiptarTorkenczy2000.Suffix.all.segments SiptarTorkenczy2000.Quality.back = some ["h", "o", "z"]
• SiptarTorkenczy2000.Suffix.all.segments SiptarTorkenczy2000.Quality.frontRounded = some ["h", "ö", "z"]
• SiptarTorkenczy2000.Suffix.all.segments SiptarTorkenczy2000.Quality.frontUnrounded = some ["h", "e", "z"]
• SiptarTorkenczy2000.Suffix.iness.segments SiptarTorkenczy2000.Quality.back = some ["b", "a", "n"]
• SiptarTorkenczy2000.Suffix.iness.segments SiptarTorkenczy2000.Quality.frontUnrounded = some ["b", "e", "n"]
• x✝¹.segments x✝ = none

def SiptarTorkenczy2000.word (s : Stem) (x : Suffix) : Word

The word of a stem and a suffix concatenates the stem's melody, its floating features and then its prelinked features over its nodes, with the suffix's melody, a LAB over the suffix node when the suffix has one.

Equations

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

def SiptarTorkenczy2000.suffixSlot (s : Stem) (x : Suffix) : Fin (word s x).lower.length

The slot of the suffix node, the last node of the word.

Equations

• SiptarTorkenczy2000.suffixSlot s x = ⟨s.nodes.length, ⋯⟩

def SiptarTorkenczy2000.derived (s : Stem) (x : Suffix) : Option (List String)

The suffix segments the derivation yields.

Equations

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

def SiptarTorkenczy2000.Stem.isBack (s : Stem) : Bool

Whether the derivation gives a stem back suffixes.

Equations

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

The representations of Table 18

def SiptarTorkenczy2000.Stem.haz : Stem

The pure DOR stem ház 'house' has a floating DOR (8a).

Equations

• SiptarTorkenczy2000.Stem.haz = SiptarTorkenczy2000.Stem.ofRow SiptarTorkenczy2000.Forms.haz [[]] [SiptarTorkenczy2000.Place.dor]

def SiptarTorkenczy2000.Stem.tuz : Stem

The pure LAB stem tűz 'fire' has a floating LAB (8b).

Equations

• SiptarTorkenczy2000.Stem.tuz = SiptarTorkenczy2000.Stem.ofRow SiptarTorkenczy2000.Forms.tuz [[]] [SiptarTorkenczy2000.Place.lab]

def SiptarTorkenczy2000.Stem.viz : Stem

The pure COR stem víz 'water' has a floating COR (8c).

Equations

• SiptarTorkenczy2000.Stem.viz = SiptarTorkenczy2000.Stem.ofRow SiptarTorkenczy2000.Forms.viz [[]] [SiptarTorkenczy2000.Place.cor]

def SiptarTorkenczy2000.Stem.piros : Stem

The COR + DOR stem piros 'red' has a linked COR and a floating DOR (9a).

Equations

• SiptarTorkenczy2000.Stem.piros = SiptarTorkenczy2000.Stem.ofRow SiptarTorkenczy2000.Forms.piros [[SiptarTorkenczy2000.Place.cor], []] [SiptarTorkenczy2000.Place.dor]

def SiptarTorkenczy2000.Stem.nuansz : Stem

The LAB + DOR stem nüansz 'nuance' has both features linked (10a).

Equations

• SiptarTorkenczy2000.Stem.nuansz = SiptarTorkenczy2000.Stem.ofRow SiptarTorkenczy2000.Forms.nuansz [[SiptarTorkenczy2000.Place.lab], [SiptarTorkenczy2000.Place.dor]] []

def SiptarTorkenczy2000.Stem.oreg : Stem

The LAB + COR stem öreg 'old' has both features linked (10b).

Equations

• SiptarTorkenczy2000.Stem.oreg = SiptarTorkenczy2000.Stem.ofRow SiptarTorkenczy2000.Forms.oreg [[SiptarTorkenczy2000.Place.lab], [SiptarTorkenczy2000.Place.cor]] []

def SiptarTorkenczy2000.Stem.szemolcs : Stem

The COR + LAB stem szemölcs 'wart' has a floating COR and a linked LAB (11a).

Equations

• SiptarTorkenczy2000.Stem.szemolcs = SiptarTorkenczy2000.Stem.ofRow SiptarTorkenczy2000.Forms.szemolcs [[], [SiptarTorkenczy2000.Place.lab]] [SiptarTorkenczy2000.Place.cor]

def SiptarTorkenczy2000.Stem.sofor : Stem

The DOR + LAB stem sofőr 'driver' has a linked DOR and a labial vowel exceptionally also coronal, which keeps DOR from spreading onto it (11b).

Equations

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

def SiptarTorkenczy2000.Stem.papir : Stem

The transparent DOR + COR stem papír 'paper' has a floating DOR and a linked COR (12a).

Equations

• SiptarTorkenczy2000.Stem.papir = SiptarTorkenczy2000.Stem.ofRow SiptarTorkenczy2000.Forms.papir [[], [SiptarTorkenczy2000.Place.cor]] [SiptarTorkenczy2000.Place.dor]

def SiptarTorkenczy2000.Stem.hid : Stem

The antiharmonic DOR + COR stem híd 'bridge' has a linked COR and a floating DOR with no node in the stem to link to (12b).

Equations

• SiptarTorkenczy2000.Stem.hid = SiptarTorkenczy2000.Stem.ofRow SiptarTorkenczy2000.Forms.hid [[SiptarTorkenczy2000.Place.cor]] [SiptarTorkenczy2000.Place.dor]

def SiptarTorkenczy2000.Stem.kodex : Stem

The opaque DOR + COR stem kódex 'codex' has both features linked (12c).

Equations

• SiptarTorkenczy2000.Stem.kodex = SiptarTorkenczy2000.Stem.ofRow SiptarTorkenczy2000.Forms.kodex [[SiptarTorkenczy2000.Place.dor], [SiptarTorkenczy2000.Place.cor]] []

def SiptarTorkenczy2000.Stem.dzsungelTransparent : Stem

The vacillating stem dzsungel 'jungle' represented like papír.

Equations

• SiptarTorkenczy2000.Stem.dzsungelTransparent = SiptarTorkenczy2000.Stem.ofRow SiptarTorkenczy2000.Forms.dzsungel [[], [SiptarTorkenczy2000.Place.cor]] [SiptarTorkenczy2000.Place.dor]

def SiptarTorkenczy2000.Stem.dzsungelOpaque : Stem

The vacillating stem dzsungel 'jungle' represented like kódex.

Equations

• SiptarTorkenczy2000.Stem.dzsungelOpaque = SiptarTorkenczy2000.Stem.ofRow SiptarTorkenczy2000.Forms.dzsungel [[SiptarTorkenczy2000.Place.dor], [SiptarTorkenczy2000.Place.cor]] []

def SiptarTorkenczy2000.stems : List (Data.Forms.Form Forms.Cell × Stem)

The stems of Table 18, each with the row of its base form.

Equations

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

def SiptarTorkenczy2000.suffixes : List (String × Suffix)

The suffixes of the derivations, by the names of the relations in the data.

Equations

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

theorem SiptarTorkenczy2000.derivations (rel : Data.Forms.FormRelation (Data.Forms.Form Forms.Cell)) : rel ∈ Forms.relations → rel.form ≠ Forms.dzsungel → ∃ s ∈ List.lookup rel.form stems, ∃ x ∈ List.lookup rel.relation suffixes, derived s x = some (List.drop rel.form.segments.length rel.target.segments)

Every derivation of (13) to (23), each a relation of the data from a stem of Table 18 other than the vacillating dzsungel, yields the attested suffix, so transparency, antiharmony and opacity follow from the prelinking of Table 18 by the same rules.

theorem SiptarTorkenczy2000.dzsungel_vacillates : derived Stem.dzsungelTransparent Suffix.iness = some (List.drop Forms.dzsungel.segments.length Forms.dzsungelban.segments) ∧ derived Stem.dzsungelOpaque Suffix.iness = some (List.drop Forms.dzsungel.segments.length Forms.dzsungelben.segments)

The vacillating stem of section 3.2.3.1 derives its back form from the transparent representation and its front form from the opaque one.

The surface generalization of section 3.2

The Fragment's palatal harmony system reads the backness of the last harmonic vowel through the transparent neutral vowels.

def SiptarTorkenczy2000.regular : List (Data.Forms.Form Forms.Cell × Stem)

The stems whose harmonic vowels govern their suffixes as section 3.2 describes, all but the pure COR víz, the antiharmonic híd and the opaque kódex.

Equations

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

theorem SiptarTorkenczy2000.sourceValue_agrees (t : Data.Forms.Form Forms.Cell × Stem) : t ∈ regular → Hungarian.palatalHarmony.searchCopy.sourceValue (Hungarian.vowelsOf t.1.segments) = some t.2.isBack

On the regular stems the surface generalization and the derivations agree.

theorem SiptarTorkenczy2000.sourceValue_viz : Hungarian.palatalHarmony.searchCopy.sourceValue (Hungarian.vowelsOf Forms.viz.segments) = none ∧ Stem.viz.isBack = false

A pure COR stem has no harmonic vowel to read, and its floating COR derives front suffixes.

theorem SiptarTorkenczy2000.sourceValue_hid : Hungarian.palatalHarmony.searchCopy.sourceValue (Hungarian.vowelsOf Forms.hid.segments) = none ∧ Stem.hid.isBack = true

An antiharmonic stem has no harmonic vowel to read either; its floating DOR derives back suffixes.

theorem SiptarTorkenczy2000.sourceValue_kodex : Hungarian.palatalHarmony.searchCopy.sourceValue (Hungarian.vowelsOf Forms.kodex.segments) = some true ∧ Stem.kodex.isBack = false

An opaque stem's last harmonic vowel is back, yet its linked DOR cannot reach the suffix and its linked COR derives front suffixes.