Syllables

The syllable σ is the level above the mora in the prosodic hierarchy, a headed moraic constituent (Hayes 1989; Hyman 1985). A non-moraic onset sits over a moraic spine whose head is the nucleus, the sonority peak (Clements 1990). The nucleus mora is mandatory and initial, so a σ has at least one mora, and tail carries any further nuclear morae (long vowels) and a moraic coda. Weight is mora-based, so the moraic structure is the carrier; Selkirk's (1982) rival onset-rime theory is a re-representation (toOnsetRime) that agrees with it on weight. The file also defines the prosodic constituents, the prosodic tree, and the Layeredness relation by which each constituent licenses its daughters.

Main definitions

• Syllable — a headed moraic σ: onset, a nucleus head mora, and a tail of morae.
• Syllable.morae / nucleusMora / nucleusSegments / weight / moraCount / pnatMoraCount.
• Syllable.IsHeavy / IsLight — the weight inventory (sonority/SSP well-formedness is a syllabification follow-up).
• Syllable.ofCV / ofVowel / ofLongVowel / mk' — smart constructors (a non-empty nucleus is required; a long vowel is two morae on one melody).
• Syllable.yield / toOnsetRime — re-representations; toOnsetRime_weight is the weight-correspondence between the moraic and onset-rime theories.
• Syllable.Weight — Nat (the mora count), with .light/.heavy/.superheavy.
• Level, Constituent.level — the levels of the prosodic hierarchy, linearly ordered σ < f < ω < φ < ι, and the level of a node.
• Constituent, Tree — the prosodic constituents and the prosodic tree over them.
• Constituent.Licenses — Layeredness: a node dominates only its own level or below.

References

• [Hay89]
• [Hym85]
• [Cle90]
• [Sel80]
• [Sel82]
• [Sel96]
• [NV86]
• [McCP93]
• [Dol20]
• [IM03]

Syllables

structure Prosody.Syllable : Type

A syllable σ is a headed moraic constituent ([Hay89]) with a non-moraic onset, a nucleus head mora (the sonority peak; mandatory, so σ has at least one mora and the head is initial by construction), and a tail of further morae (long-vowel morae and a moraic coda).

• onset : List Phonology.Segment

  The non-moraic onset melody.

• head : Mora

  The nucleus mora — the sonority peak; mandatory, so σ has ≥ 1 mora.

• tail : List Mora

  The further morae are long-vowel morae and a moraic coda.

def Prosody.instDecidableEqSyllable.decEq (x✝ x✝¹ : Syllable) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Prosody.instDecidableEqSyllable : DecidableEq Syllable

Equations

• Prosody.instDecidableEqSyllable = Prosody.instDecidableEqSyllable.decEq

@[reducible, inline]

abbrev Prosody.Syllable.Weight : Type

Syllable weight is just the mora count — there is no separate weight type. .light (1μ), .heavy (2μ), .superheavy (3μ) name the common values for readable weight profiles in metrical and accentual computations.

Equations

• Prosody.Syllable.Weight = ℕ

@[reducible, inline]

abbrev Prosody.Syllable.Weight.light : Weight

Equations

• Prosody.Syllable.Weight.light = 1

@[reducible, inline]

abbrev Prosody.Syllable.Weight.heavy : Weight

Equations

• Prosody.Syllable.Weight.heavy = 2

@[reducible, inline]

abbrev Prosody.Syllable.Weight.superheavy : Weight

Equations

• Prosody.Syllable.Weight.superheavy = 3

def Prosody.Syllable.morae (σ : Syllable) : List Mora

The moraic spine, nucleus (peak) first.

Equations

• σ.morae = σ.head :: σ.tail

@[reducible, inline]

abbrev Prosody.Syllable.nucleusMora (σ : Syllable) : Mora

The nucleus — the head mora (the sonority peak).

Equations

• σ.nucleusMora = σ.head

def Prosody.Syllable.nucleusSegments (σ : Syllable) : List Phonology.Segment

The nucleus segment(s).

Equations

• σ.nucleusSegments = σ.head.dominates

def Prosody.Syllable.moraCount (σ : Syllable) : ℕ

The number of morae — the syllable's weight.

Equations

• σ.moraCount = σ.morae.length

@[reducible, inline]

abbrev Prosody.Syllable.weight (σ : Syllable) : Weight

The syllable's weight (= its mora count).

Equations

• σ.weight = σ.moraCount

theorem Prosody.Syllable.moraCount_pos (σ : Syllable) : 0 < σ.moraCount

A syllable has at least its nucleus mora.

def Prosody.Syllable.pnatMoraCount (σ : Syllable) : ℕ+

The mora count as a positive natural is the weight a Tone.Registered word reads.

Equations

• σ.pnatMoraCount = ⟨σ.moraCount, ⋯⟩

def Prosody.Syllable.IsHeavy (σ : Syllable) : Prop

A syllable is heavy when it has at least two morae.

Equations

• σ.IsHeavy = (Prosody.Syllable.Weight.heavy ≤ σ.weight)

def Prosody.Syllable.IsLight (σ : Syllable) : Prop

A syllable is light when it has exactly one mora.

Equations

• σ.IsLight = (σ.weight = Prosody.Syllable.Weight.light)

@[instance_reducible]

instance Prosody.Syllable.instDecidableIsHeavy (σ : Syllable) : Decidable σ.IsHeavy

Equations

• σ.instDecidableIsHeavy = id inferInstance

@[instance_reducible]

instance Prosody.Syllable.instDecidableIsLight (σ : Syllable) : Decidable σ.IsLight

Equations

• σ.instDecidableIsLight = id inferInstance

def Prosody.Syllable.mk' (onset : List Phonology.Segment) (nucleus : Mora) (coda : List Mora := []) : Syllable

Build a syllable from an explicit nucleus mora (+ optional further/coda morae).

Equations

• Prosody.Syllable.mk' onset nucleus coda = { onset := onset, head := nucleus, tail := coda }

def Prosody.Syllable.ofMorae (onset : List Phonology.Segment) (ms : List Mora) (h : ms ≠ [] := by simp) : Syllable

Build a syllable from an onset and a non-empty mora spine (nucleus = first mora).

Equations

• Prosody.Syllable.ofMorae onset ms h = { onset := onset, head := ms.head h, tail := ms.tail }

def Prosody.Syllable.ofCV (onset nucleus coda : List Phonology.Segment) (wbp : Bool := true) (hn : nucleus ≠ [] := by simp) : Syllable

Build a syllable from a segmental onset–nucleus–coda string. Each nucleus segment projects a mora (the first is the nucleus head). Under Weight by Position ([Hay89]) the first coda segment projects its own mora and any further coda segments ride it, so the syllable stays at most bimoraic; without it the coda rides the last nucleus mora. A non-empty nucleus is required.

Equations

• One or more equations did not get rendered due to their size.
• Prosody.Syllable.ofCV onset [] coda wbp h = ⋯.elim
• Prosody.Syllable.ofCV onset (n₀ :: ns) (c :: cs) true x = { onset := onset, head := Prosody.Mora.of n₀, tail := List.map Prosody.Mora.of ns ++ [(Prosody.Mora.of c).attach cs] }

def Prosody.Syllable.ofVowel (onset : List Phonology.Segment) (v : Phonology.Segment) : Syllable

The open syllable of an onset and a short vowel has one mora.

Equations

• Prosody.Syllable.ofVowel onset v = { onset := onset, head := Prosody.Mora.of v, tail := [] }

def Prosody.Syllable.ofLongVowel (onset : List Phonology.Segment) (v : Phonology.Segment) : Syllable

The open syllable of an onset and a long vowel has two morae dominating the same melody ([Hay89]).

Equations

• Prosody.Syllable.ofLongVowel onset v = { onset := onset, head := Prosody.Mora.of v, tail := [Prosody.Mora.of v] }

@[simp]

theorem Prosody.Syllable.moraCount_ofVowel (onset : List Phonology.Segment) (v : Phonology.Segment) : (ofVowel onset v).moraCount = 1

@[simp]

theorem Prosody.Syllable.moraCount_ofLongVowel (onset : List Phonology.Segment) (v : Phonology.Segment) : (ofLongVowel onset v).moraCount = 2

def Prosody.Syllable.yield (σ : Syllable) : List Phonology.Segment

The segment string, or yield, of a syllable is its onset followed by the moraic melody.

Equations

• σ.yield = σ.onset ++ List.flatMap (fun (x : Prosody.Mora) => x.dominates) σ.morae

Onset-rime re-representation

structure Prosody.OnsetRime : Type

The onset-rime structure of [Sel82] is a rival theory of σ structure, an onset over a rime, here a re-representation of the canonical moraic Syllable.

• onset : List Phonology.Segment

  The non-moraic onset melody.

• rime : List Mora

  The rime is the moraic spine.

@[instance_reducible]

instance Prosody.instDecidableEqOnsetRime : DecidableEq OnsetRime

Equations

• Prosody.instDecidableEqOnsetRime = Prosody.instDecidableEqOnsetRime.decEq

def Prosody.instDecidableEqOnsetRime.decEq (x✝ x✝¹ : OnsetRime) : Decidable (x✝ = x✝¹)

Equations

• Prosody.instDecidableEqOnsetRime.decEq { onset := a, rime := a_1 } { onset := b, rime := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Prosody.Syllable.toOnsetRime (σ : Syllable) : OnsetRime

Passing from σ to onset-rime structure, the rime is the moraic spine ([Sel82]).

Equations

• σ.toOnsetRime = { onset := σ.onset, rime := σ.morae }

theorem Prosody.Syllable.toOnsetRime_weight (σ : Syllable) : σ.toOnsetRime.rime.length = σ.moraCount

By weight correspondence, the onset-rime rime's mora count equals σ's weight, so the moraic and onset-rime theories agree on weight ([Sel82]; [Hay89]).

Yield

@[reducible, inline]

abbrev Prosody.Yield : Type

A yield is the terminal σ-weight string of a prosodic structure, the unparsed input or the leaves of a prosodic Tree. Unlike the prosodic word ω (an IsWord tree), which is a headed constituent, a yield is just the weight profile, with no head and no constituency.

Equations

• Prosody.Yield = List Prosody.Syllable.Weight

def Prosody.Yield.ofSyllables (σs : List Syllable) : Yield

The weight profile of fully-moraified syllables — the σ → yield bridge.

Equations

• Prosody.Yield.ofSyllables σs = List.map Prosody.Syllable.weight σs

def Prosody.Yield.moraCount (y : Yield) : ℕ

Total mora count (each weight is a mora count).

Equations

• y.moraCount = List.sum y

@[reducible, inline]

abbrev Prosody.Yield.satisfiesMinWord (y : Yield) (minMorae : ℕ := 2) : Prop

The minimal-word size constraint of [McCP93] asks for at least minMorae morae (default 2, the moraic-trochee minimum), the moraic size floor on a prosodic word. Whether an ω must structurally contain a foot is a separate, non-presupposed matter (footless languages have ω directly over σ, [Dol20]).

Equations

• y.satisfiesMinWord minMorae = (minMorae ≤ y.moraCount)

The prosodic-tree carrier

The recursive prosodic constituent ([IM03]): the Core ordered rose tree RoseTree labeled by prosodic-level Constituents — the violable OT candidate carrier for ω/φ/… structures, including the ill-formed ones (a footless ω, a stray under φ) that IsWord rules out. Its OT constraints are OptimalityTheory.Constraint Tree values, defined alongside IsWord. Homed here because Constituent.weight/.syl need Syllable.Weight; it inherits DecidableEq/map from RoseTree.

inductive Prosody.Level : Type

The levels of the prosodic hierarchy ([Sel80]; [NV86]), linearly ordered σ < f < ω < φ < ι.

• syl : Level
• ft : Level
• om : Level
• ph : Level
• iota : Level

@[instance_reducible]

instance Prosody.instDecidableEqLevel : DecidableEq Level

Equations

• Prosody.instDecidableEqLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Prosody.instReprLevel.repr : Level → ℕ → Std.Format

Equations

• Prosody.instReprLevel.repr Prosody.Level.syl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Prosody.Level.syl")).group prec✝
• Prosody.instReprLevel.repr Prosody.Level.ft prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Prosody.Level.ft")).group prec✝
• Prosody.instReprLevel.repr Prosody.Level.om prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Prosody.Level.om")).group prec✝
• Prosody.instReprLevel.repr Prosody.Level.ph prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Prosody.Level.ph")).group prec✝
• Prosody.instReprLevel.repr Prosody.Level.iota prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Prosody.Level.iota")).group prec✝

@[instance_reducible]

instance Prosody.instReprLevel : Repr Level

Equations

• Prosody.instReprLevel = { reprPrec := Prosody.instReprLevel.repr }

def Prosody.Level.toNat : Level → ℕ

The rank of a level, σ lowest.

Equations

• Prosody.Level.syl.toNat = 0
• Prosody.Level.ft.toNat = 1
• Prosody.Level.om.toNat = 2
• Prosody.Level.ph.toNat = 3
• Prosody.Level.iota.toNat = 4

theorem Prosody.Level.toNat_injective : Function.Injective toNat

@[instance_reducible]

instance Prosody.Level.instLinearOrder : LinearOrder Level

Equations

• Prosody.Level.instLinearOrder = LinearOrder.lift' Prosody.Level.toNat Prosody.Level.toNat_injective

inductive Prosody.Constituent : Type

In a prosodic node the level is the constructor. A σ carries its mora weight and isHead, and every non-root level carries isHead (whether it heads its parent). Constructor defaults match the former smart constructors, so node literals are unchanged; illegal nodes (a weight on a foot, a head on the ι root) are unrepresentable.

• syl (weight : Syllable.Weight := 0) (isHead : Bool := false) : Constituent

  A syllable of the given weight, optionally the head of its foot.

• ft (isHead : Bool := false) : Constituent

  A foot, optionally the head foot of its word.

• om (isHead : Bool := false) : Constituent

  A prosodic word ω, optionally the head word of its phrase.

• ph (isHead : Bool := false) : Constituent

  A phonological phrase φ, optionally the head phrase of its intonational phrase.

• iota : Constituent

  An intonational phrase ι — the root of the utterance-level hierarchy, headless.

@[instance_reducible]

instance Prosody.instDecidableEqConstituent : DecidableEq Constituent

Equations

• Prosody.instDecidableEqConstituent = Prosody.instDecidableEqConstituent.decEq

def Prosody.instDecidableEqConstituent.decEq (x✝ x✝¹ : Constituent) : Decidable (x✝ = x✝¹)

Equations

• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.syl a a_1) (Prosody.Constituent.syl b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.syl weight isHead) (Prosody.Constituent.ft isHead_1) = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.syl weight isHead) (Prosody.Constituent.om isHead_1) = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.syl weight isHead) (Prosody.Constituent.ph isHead_1) = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.syl weight isHead) Prosody.Constituent.iota = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.ft isHead) (Prosody.Constituent.syl weight isHead_1) = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.ft a) (Prosody.Constituent.ft b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.ft isHead) (Prosody.Constituent.om isHead_1) = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.ft isHead) (Prosody.Constituent.ph isHead_1) = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.ft isHead) Prosody.Constituent.iota = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.om isHead) (Prosody.Constituent.syl weight isHead_1) = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.om isHead) (Prosody.Constituent.ft isHead_1) = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.om a) (Prosody.Constituent.om b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.om isHead) (Prosody.Constituent.ph isHead_1) = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.om isHead) Prosody.Constituent.iota = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.ph isHead) (Prosody.Constituent.syl weight isHead_1) = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.ph isHead) (Prosody.Constituent.ft isHead_1) = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.ph isHead) (Prosody.Constituent.om isHead_1) = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.ph a) (Prosody.Constituent.ph b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.ph isHead) Prosody.Constituent.iota = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq Prosody.Constituent.iota (Prosody.Constituent.syl weight isHead) = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq Prosody.Constituent.iota (Prosody.Constituent.ft isHead) = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq Prosody.Constituent.iota (Prosody.Constituent.om isHead) = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq Prosody.Constituent.iota (Prosody.Constituent.ph isHead) = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq Prosody.Constituent.iota Prosody.Constituent.iota = isTrue ⋯

@[instance_reducible]

instance Prosody.instReprConstituent : Repr Constituent

Equations

• Prosody.instReprConstituent = { reprPrec := Prosody.instReprConstituent.repr }

def Prosody.instReprConstituent.repr : Constituent → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Prosody.instReprConstituent.repr Prosody.Constituent.iota prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Prosody.Constituent.iota")).group prec✝

def Prosody.Constituent.isHead : Constituent → Bool

Whether a node heads its parent (a σ heads its foot, a foot heads its word, an ω its phrase, a φ its intonational phrase); false for the ι root.

Equations

• (Prosody.Constituent.syl weight h).isHead = h
• (Prosody.Constituent.ft h).isHead = h
• (Prosody.Constituent.om h).isHead = h
• (Prosody.Constituent.ph h).isHead = h
• Prosody.Constituent.iota.isHead = false

def Prosody.Constituent.weight? : Constituent → Option Syllable.Weight

The mora weight of a σ node; none for non-σ nodes.

Equations

• (Prosody.Constituent.syl w isHead).weight? = some w
• x✝.weight? = none

def Prosody.Constituent.level : Constituent → Level

The level of a node, the constructor without its weight and head mark.

Equations

• (Prosody.Constituent.syl weight h).level = Prosody.Level.syl
• (Prosody.Constituent.ft h).level = Prosody.Level.ft
• (Prosody.Constituent.om h).level = Prosody.Level.om
• (Prosody.Constituent.ph h).level = Prosody.Level.ph
• Prosody.Constituent.iota.level = Prosody.Level.iota

def Prosody.Constituent.Licenses : Constituent → List Constituent → Prop

Under Layeredness ([Sel96]) a node dominates only nodes of its own level or below: σ is the terminal, a foot a non-empty string of σs (foot recursion, contested, is excluded with it), and ω, φ and ι dominate anything at or below their level. Recursion at ω, φ and ι and level skipping, a σ or a foot directly under a φ, are thereby admitted: Nonrecursivity and Exhaustivity are the violable constraints noRec and parseInto. Licenses a ks says that a may dominate daughters labelled ks.

Equations

• (Prosody.Constituent.syl weight isHead).Licenses x✝ = (x✝ = [])
• (Prosody.Constituent.ft isHead).Licenses x✝ = (x✝ ≠ [] ∧ ∀ k ∈ x✝, k.level = Prosody.Level.syl)
• x✝¹.Licenses x✝ = ∀ k ∈ x✝, k.level ≤ x✝¹.level

@[instance_reducible]

instance Prosody.Constituent.instDecidableLicenses (a : Constituent) (ks : List Constituent) : Decidable (a.Licenses ks)

Equations

• (Prosody.Constituent.syl weight isHead).instDecidableLicenses x✝ = Prosody.Constituent.instDecidableLicenses._aux_1 weight isHead x✝
• (Prosody.Constituent.ft isHead).instDecidableLicenses x✝ = { decide := decide (x✝ ≠ []) && decide (∀ k ∈ x✝, k.level = Prosody.Level.syl), reflects_decide := ⋯ }
• (Prosody.Constituent.om isHead).instDecidableLicenses x✝ = Prosody.Constituent.instDecidableLicenses._aux_4 isHead x✝
• (Prosody.Constituent.ph isHead).instDecidableLicenses x✝ = Prosody.Constituent.instDecidableLicenses._aux_6 isHead x✝
• Prosody.Constituent.iota.instDecidableLicenses x✝ = Prosody.Constituent.instDecidableLicenses._aux_8 x✝

@[reducible, inline]

abbrev Prosody.Tree : Type

A prosodic tree is an ordered rose tree labelled by Constituents. Ordered children give No-Tangling by construction.

Equations

• Prosody.Tree = RoseTree Prosody.Constituent

@[reducible, inline]

abbrev Prosody.Tree.σ (w : Syllable.Weight := 0) (h : Bool := false) : Tree

A σ-leaf is the metrical terminal, a syllable of weight w with head mark h.

Equations

• Prosody.Tree.σ w h = RoseTree.node (Prosody.Constituent.syl w h) []

@[reducible, inline]

abbrev Prosody.Tree.ft (h : Bool) (cs : List Tree) : Tree

A foot node over cs, optionally the head foot of its word.

Equations

• Prosody.Tree.ft h cs = RoseTree.node (Prosody.Constituent.ft h) cs

@[reducible, inline]

abbrev Prosody.Tree.om (cs : List Tree) : Tree

A prosodic-word (ω) node over cs.

Equations

• Prosody.Tree.om cs = RoseTree.node Prosody.Constituent.om cs

@[reducible, inline]

abbrev Prosody.Tree.ph (cs : List Tree) : Tree

A phonological-phrase (φ) node over cs.

Equations

• Prosody.Tree.ph cs = RoseTree.node Prosody.Constituent.ph cs

theorem Prosody.Tree.recLeafBranch {motive : Tree → Prop} (leaf : ∀ (a : Constituent), a.level = Level.syl → motive (RoseTree.node a [])) (branch : ∀ (a : Constituent) (cs : List Tree), ¬(a.level = Level.syl ∧ cs = []) → (∀ c ∈ cs, motive c) → motive (RoseTree.node a cs)) (t : Tree) : motive t

Leaf/branch induction on a prosodic tree. A σ-leaf is a base case; every other node — a foot, word, phrase, or degenerate/ill-formed node — is a branch, carrying the induction hypothesis over its children and the fact that it is not a σ-leaf. This is what lets proofs reduce the σ-leaf if the reader equations carry (via ite_eq_left ⟨ha, rfl⟩ or ite_eq_right hne) instead of splitting it.