Yolyan & Comer 2026: Phonological Processes as Modal Transductions

[YC26]: total BMRS — the Boolean monadic recursive schemes of [BCJO20], rendered by Subregular.BMRS — is expressively equivalent to the modal μ-calculus on words (Thm. 2), giving an alternative proof that order-preserving BMRS captures the rational functions. Formula/System render the paper's §4 vectorial presentation of [Koz83]'s μ-calculus over word models — a finite system of equations Xⱼ = θⱼ read as the least fixed point of the induced monotone operator (Knaster–Tarski), which by Bekić's theorem is equivalent to nested μ-binders but spares the binder bookkeeping. This file formalizes the constructive core: the translation tr (Def. 6) from vectorial modal formulas to BMRS expressions and its compositionality (eval_tr, Remark 7) — tr φ evaluates to the truth value of φ wherever rule-head calls agree with the recursion variables. Thm. 8 discharges that hypothesis for directed systems by SCC induction (TODO: the directedness machinery); Thm. 2's converse containment runs through MSO (out of scope until an MSO substrate exists).

The paper's two worked examples ground both formalisms: vowel nasalization ((2)–(4), non-recursive) and progressive nasal spreading in Warao ((5)–(7), [osborn-1966]). The modal form N′ = μX.(N ∨ (¬T ∧ ♦X)) recurses under the backward modality ♦ = bdia — a target inherits nasality from its predecessor. Both compute the Fig. 4/5 columns on /naote/ → [nãõte], and the BMRS and modal results agree (warao_agreement); warao_tr_agreement runs Remark 7 end-to-end on the translated program, with the rule-head hypothesis discharged by direct computation — the concrete shape of Thm. 8's induction.

The vectorial modal μ-calculus on words (§4)

Formulas are the negation-free fragment μML꜀₊ — the ambient of Thm. 8 — extended with negated label atoms (nlabel), which keeps negation off recursion variables (so monotonicity is structural) while covering processes like Warao nasal spreading N′ = μX.(N ∨ (¬T ∧ ♦X)).

inductive YolyanComer2026.Formula (α : Type u_2) (n : ℕ) : Type u_2

Quantifier-free modal formulas over labels α and n recursion variables: negation-free apart from class atoms (nlabel), so recursion variables occur only positively. label/nlabel test the current position's symbol against a Finset class (featural predicates like V or N are single atoms; a symbol test is the singleton case). initial/final are the edge tests (the literature's min/max); dia (◇) reads the successor position, bdia (♦) the predecessor.

• tru {α : Type u_2} {n : ℕ} : Formula α n
• fls {α : Type u_2} {n : ℕ} : Formula α n
• initial {α : Type u_2} {n : ℕ} : Formula α n
• final {α : Type u_2} {n : ℕ} : Formula α n
• label {α : Type u_2} {n : ℕ} (s : Finset α) : Formula α n
• nlabel {α : Type u_2} {n : ℕ} (s : Finset α) : Formula α n
• var {α : Type u_2} {n : ℕ} (X : Fin n) : Formula α n
• and {α : Type u_2} {n : ℕ} (φ ψ : Formula α n) : Formula α n
• or {α : Type u_2} {n : ℕ} (φ ψ : Formula α n) : Formula α n
• dia {α : Type u_2} {n : ℕ} (φ : Formula α n) : Formula α n
• bdia {α : Type u_2} {n : ℕ} (φ : Formula α n) : Formula α n

def YolyanComer2026.instDecidableEqFormula.decEq {α✝ : Type u_2} {n✝ : ℕ} [DecidableEq α✝] (x✝ x✝¹ : Formula α✝ n✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance YolyanComer2026.instDecidableEqFormula {α✝ : Type u_2} {n✝ : ℕ} [DecidableEq α✝] : DecidableEq (Formula α✝ n✝)

Equations

• YolyanComer2026.instDecidableEqFormula = YolyanComer2026.instDecidableEqFormula.decEq

def YolyanComer2026.Formula.Realize {α : Type u_1} {n : ℕ} (w : List α) (U : Fin n → Set ℕ) : ℕ → Formula α n → Prop

Satisfaction at a pointed word (w, i) under a valuation U of the recursion variables.

Equations

• YolyanComer2026.Formula.Realize w U x✝ YolyanComer2026.Formula.tru = True
• YolyanComer2026.Formula.Realize w U x✝ YolyanComer2026.Formula.fls = False
• YolyanComer2026.Formula.Realize w U x✝ YolyanComer2026.Formula.initial = (x✝ = 0)
• YolyanComer2026.Formula.Realize w U x✝ YolyanComer2026.Formula.final = (x✝ + 1 = w.length)
• YolyanComer2026.Formula.Realize w U x✝ (YolyanComer2026.Formula.label s) = ∃ a ∈ s, w[x✝]? = some a
• YolyanComer2026.Formula.Realize w U x✝ (YolyanComer2026.Formula.nlabel s) = ∀ a ∈ s, w[x✝]? ≠ some a
• YolyanComer2026.Formula.Realize w U x✝ (YolyanComer2026.Formula.var X) = (x✝ ∈ U X)
• YolyanComer2026.Formula.Realize w U x✝ (φ.and ψ) = (YolyanComer2026.Formula.Realize w U x✝ φ ∧ YolyanComer2026.Formula.Realize w U x✝ ψ)
• YolyanComer2026.Formula.Realize w U x✝ (φ.or ψ) = (YolyanComer2026.Formula.Realize w U x✝ φ ∨ YolyanComer2026.Formula.Realize w U x✝ ψ)
• YolyanComer2026.Formula.Realize w U x✝ φ.dia = ∃ (j : ℕ), Subregular.succ? w x✝ = some j ∧ YolyanComer2026.Formula.Realize w U j φ
• YolyanComer2026.Formula.Realize w U x✝ φ.bdia = ∃ (j : ℕ), Subregular.pred? w x✝ = some j ∧ YolyanComer2026.Formula.Realize w U j φ

@[simp]

theorem YolyanComer2026.Formula.realize_tru {α : Type u_1} {n : ℕ} {w : List α} {U : Fin n → Set ℕ} {i : ℕ} : Realize w U i tru

@[simp]

theorem YolyanComer2026.Formula.realize_fls {α : Type u_1} {n : ℕ} {w : List α} {U : Fin n → Set ℕ} {i : ℕ} : ¬Realize w U i fls

@[simp]

theorem YolyanComer2026.Formula.realize_initial {α : Type u_1} {n : ℕ} {w : List α} {U : Fin n → Set ℕ} {i : ℕ} : Realize w U i initial ↔ i = 0

@[simp]

theorem YolyanComer2026.Formula.realize_final {α : Type u_1} {n : ℕ} {w : List α} {U : Fin n → Set ℕ} {i : ℕ} : Realize w U i final ↔ i + 1 = w.length

@[simp]

theorem YolyanComer2026.Formula.realize_label {α : Type u_1} {n : ℕ} {w : List α} {U : Fin n → Set ℕ} {i : ℕ} {s : Finset α} : Realize w U i (label s) ↔ ∃ a ∈ s, w[i]? = some a

@[simp]

theorem YolyanComer2026.Formula.realize_nlabel {α : Type u_1} {n : ℕ} {w : List α} {U : Fin n → Set ℕ} {i : ℕ} {s : Finset α} : Realize w U i (nlabel s) ↔ ∀ a ∈ s, w[i]? ≠ some a

@[simp]

theorem YolyanComer2026.Formula.realize_var {α : Type u_1} {n : ℕ} {w : List α} {U : Fin n → Set ℕ} {i : ℕ} {X : Fin n} : Realize w U i (var X) ↔ i ∈ U X

@[simp]

theorem YolyanComer2026.Formula.realize_and {α : Type u_1} {n : ℕ} {w : List α} {U : Fin n → Set ℕ} {i : ℕ} {φ ψ : Formula α n} : Realize w U i (φ.and ψ) ↔ Realize w U i φ ∧ Realize w U i ψ

@[simp]

theorem YolyanComer2026.Formula.realize_or {α : Type u_1} {n : ℕ} {w : List α} {U : Fin n → Set ℕ} {i : ℕ} {φ ψ : Formula α n} : Realize w U i (φ.or ψ) ↔ Realize w U i φ ∨ Realize w U i ψ

@[simp]

theorem YolyanComer2026.Formula.realize_dia {α : Type u_1} {n : ℕ} {w : List α} {U : Fin n → Set ℕ} {i : ℕ} {φ : Formula α n} : Realize w U i φ.dia ↔ ∃ (j : ℕ), Subregular.succ? w i = some j ∧ Realize w U j φ

@[simp]

theorem YolyanComer2026.Formula.realize_bdia {α : Type u_1} {n : ℕ} {w : List α} {U : Fin n → Set ℕ} {i : ℕ} {φ : Formula α n} : Realize w U i φ.bdia ↔ ∃ (j : ℕ), Subregular.pred? w i = some j ∧ Realize w U j φ

@[instance_reducible]

instance YolyanComer2026.Formula.instDecidableRealize {α : Type u_1} {n : ℕ} [DecidableEq α] (w : List α) (U : Fin n → Set ℕ) [(X : Fin n) → DecidablePred fun (x : ℕ) => x ∈ U X] (i : ℕ) (φ : Formula α n) : Decidable (Realize w U i φ)

Equations

• YolyanComer2026.Formula.instDecidableRealize w U x✝ YolyanComer2026.Formula.tru = isTrue trivial
• YolyanComer2026.Formula.instDecidableRealize w U x✝ YolyanComer2026.Formula.fls = isFalse not_false
• YolyanComer2026.Formula.instDecidableRealize w U x✝ YolyanComer2026.Formula.initial = YolyanComer2026.Formula.instDecidableRealize._aux_1 w U x✝
• YolyanComer2026.Formula.instDecidableRealize w U x✝ YolyanComer2026.Formula.final = YolyanComer2026.Formula.instDecidableRealize._aux_3 w U x✝
• YolyanComer2026.Formula.instDecidableRealize w U x✝ (YolyanComer2026.Formula.label s) = YolyanComer2026.Formula.instDecidableRealize._aux_5 w U x✝ s
• YolyanComer2026.Formula.instDecidableRealize w U x✝ (YolyanComer2026.Formula.nlabel s) = YolyanComer2026.Formula.instDecidableRealize._aux_7 w U x✝ s
• YolyanComer2026.Formula.instDecidableRealize w U x✝ (YolyanComer2026.Formula.var X) = YolyanComer2026.Formula.instDecidableRealize._aux_9 w U x✝ X
• YolyanComer2026.Formula.instDecidableRealize w U x✝ (φ.and ψ) = instDecidableAnd
• YolyanComer2026.Formula.instDecidableRealize w U x✝ (φ.or ψ) = instDecidableOr
• YolyanComer2026.Formula.instDecidableRealize w U x✝ φ.dia = match h : Subregular.succ? w x✝ with | none => isFalse ⋯ | some j => decidable_of_iff (YolyanComer2026.Formula.Realize w U j φ) ⋯
• YolyanComer2026.Formula.instDecidableRealize w U x✝ φ.bdia = match h : Subregular.pred? w x✝ with | none => isFalse ⋯ | some j => decidable_of_iff (YolyanComer2026.Formula.Realize w U j φ) ⋯

theorem YolyanComer2026.Formula.Realize.mono {α : Type u_1} {n : ℕ} {w : List α} {U V : Fin n → Set ℕ} (hUV : U ≤ V) {φ : Formula α n} {i : ℕ} : Realize w U i φ → Realize w V i φ

Satisfaction is monotone in the valuation: recursion variables occur only positively.

structure YolyanComer2026.System (α : Type u_2) (n : ℕ) : Type u_2

A vectorial formula: a finite system of equations Xⱼ = θⱼ plus a designated variable.

• eqs : Fin n → Formula α n

  The right-hand side of each equation.

• out : Fin n

  The designated variable whose satisfaction is the system's.

def YolyanComer2026.System.op {α : Type u_1} {n : ℕ} (χ : System α n) (w : List α) : (Fin n → Set ℕ) →o Fin n → Set ℕ

The monotone operator a system induces on valuations (the paper's F_w^χ).

Equations

• χ.op w = { toFun := fun (U : Fin n → Set ℕ) (X : Fin n) => {i : ℕ | YolyanComer2026.Formula.Realize w U i (χ.eqs X)}, monotone' := ⋯ }

@[simp]

theorem YolyanComer2026.System.mem_op {α : Type u_1} {n : ℕ} (χ : System α n) (w : List α) {U : Fin n → Set ℕ} {X : Fin n} {i : ℕ} : i ∈ (χ.op w) U X ↔ Formula.Realize w U i (χ.eqs X)

noncomputable def YolyanComer2026.System.sem {α : Type u_1} {n : ℕ} (χ : System α n) (w : List α) : Fin n → Set ℕ

The least-fixed-point valuation (Knaster–Tarski).

Equations

• χ.sem w = OrderHom.lfp (χ.op w)

theorem YolyanComer2026.System.op_sem {α : Type u_1} {n : ℕ} (χ : System α n) (w : List α) : (χ.op w) (χ.sem w) = χ.sem w

sem is a fixed point of the system operator.

theorem YolyanComer2026.System.sem_le {α : Type u_1} {n : ℕ} (χ : System α n) (w : List α) {U : Fin n → Set ℕ} (hU : (χ.op w) U ≤ U) : χ.sem w ≤ U

sem is below every prefixed point.

theorem YolyanComer2026.System.sem_eq_iterate {α : Type u_1} {n : ℕ} (χ : System α n) (w : List α) {k : ℕ} (h : (χ.op w) ((⇑(χ.op w))^[k] ⊥) = (⇑(χ.op w))^[k] ⊥) : χ.sem w = (⇑(χ.op w))^[k] ⊥

Iteration certificate: an iterate of ⊥ fixed by the operator is sem. The computable route to the least fixed point — no continuity needed.

def YolyanComer2026.System.Sat {α : Type u_1} {n : ℕ} (χ : System α n) (w : List α) (i : ℕ) : Prop

w, i ⊨ χ: the designated variable holds at i in the least fixed point.

Equations

• χ.Sat w i = (i ∈ χ.sem w χ.out)

Segments and feature classes

The examples' segments, with the paper's overlapping feature predicates N, V, T as class tests (a nasalized vowel satisfies both V and N — a partition alphabet cannot represent the nasalization output, which is why label atoms are class tests).

inductive YolyanComer2026.Seg : Type

Segments occurring in the paper's examples.

• n : Seg
• a : Seg
• o : Seg
• t : Seg
• e : Seg
• b : Seg

@[instance_reducible]

instance YolyanComer2026.instDecidableEqSeg : DecidableEq Seg

Equations

• YolyanComer2026.instDecidableEqSeg x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def YolyanComer2026.instReprSeg.repr : Seg → ℕ → Std.Format

Equations

• YolyanComer2026.instReprSeg.repr YolyanComer2026.Seg.n prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "YolyanComer2026.Seg.n")).group prec✝
• YolyanComer2026.instReprSeg.repr YolyanComer2026.Seg.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "YolyanComer2026.Seg.a")).group prec✝
• YolyanComer2026.instReprSeg.repr YolyanComer2026.Seg.o prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "YolyanComer2026.Seg.o")).group prec✝
• YolyanComer2026.instReprSeg.repr YolyanComer2026.Seg.t prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "YolyanComer2026.Seg.t")).group prec✝
• YolyanComer2026.instReprSeg.repr YolyanComer2026.Seg.e prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "YolyanComer2026.Seg.e")).group prec✝
• YolyanComer2026.instReprSeg.repr YolyanComer2026.Seg.b prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "YolyanComer2026.Seg.b")).group prec✝

@[instance_reducible]

instance YolyanComer2026.instReprSeg : Repr Seg

Equations

• YolyanComer2026.instReprSeg = { reprPrec := YolyanComer2026.instReprSeg.repr }

def YolyanComer2026.nas : Finset Seg

N: nasal sounds.

Equations

• YolyanComer2026.nas = {YolyanComer2026.Seg.n}

def YolyanComer2026.vow : Finset Seg

V: vowels.

Equations

• YolyanComer2026.vow = {YolyanComer2026.Seg.a, YolyanComer2026.Seg.o, YolyanComer2026.Seg.e}

def YolyanComer2026.stop : Finset Seg

T: voiceless stops (the spreading blocker).

Equations

• YolyanComer2026.stop = {YolyanComer2026.Seg.t}

def YolyanComer2026.naote : List Seg

/naote/, the Fig. 4 input.

Equations

• YolyanComer2026.naote = [YolyanComer2026.Seg.n, YolyanComer2026.Seg.a, YolyanComer2026.Seg.o, YolyanComer2026.Seg.t, YolyanComer2026.Seg.e]

def YolyanComer2026.baen : List Seg

/bæn/, the vowel-nasalization input.

Equations

• YolyanComer2026.baen = [YolyanComer2026.Seg.b, YolyanComer2026.Seg.a, YolyanComer2026.Seg.n]

Vowel nasalization ((2)–(4)): a vowel nasalizes before a nasal

inductive YolyanComer2026.NasHead : Type

Output predicates of the nasalization program.

• V' : NasHead
• N' : NasHead

@[instance_reducible]

instance YolyanComer2026.instDecidableEqNasHead : DecidableEq NasHead

Equations

• YolyanComer2026.instDecidableEqNasHead x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def YolyanComer2026.nasalization : Subregular.BMRS.Program Seg NasHead

(3): V′(x) = V(x); N′(x) = if V(x) then N(s(x)) else N(x).

Equations

• One or more equations did not get rendered due to their size.
• YolyanComer2026.nasalization YolyanComer2026.NasHead.V' = Subregular.BMRS.Expr.label YolyanComer2026.vow YolyanComer2026.x✝

theorem YolyanComer2026.nasalization_columns : List.map (fun (i : ℕ) => Subregular.BMRS.evalFuel nasalization baen 8 i (Subregular.BMRS.Expr.call NasHead.V' YolyanComer2026.x✝)) (List.range 3) = [some false, some true, some false] ∧ List.map (fun (i : ℕ) => Subregular.BMRS.evalFuel nasalization baen 8 i (Subregular.BMRS.Expr.call NasHead.N' YolyanComer2026.x✝)) (List.range 3) = [some false, some true, some true]

Fig. 3: on /bæn/ the output columns are V′ = ⊥⊤⊥ and N′ = ⊥⊤⊤ — [bæ̃n], the æ nasalized by the following n.

def YolyanComer2026.nasalizationChi : System Seg 1

(4): the modal form N′ = (V ∧ ◇N) ∨ N — non-recursive, so no fixed point is involved.

Equations

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

theorem YolyanComer2026.nasalizationChi_sat (i : ℕ) : nasalizationChi.Sat baen i ↔ i = 1 ∨ i = 2

The modal (4) marks exactly positions 1 and 2 of /bæn/ nasal, agreeing with the BMRS N′ column.

Warao nasal spreading ((5)–(7)): nasality spreads rightward until a stop

inductive YolyanComer2026.WHead : Type

The single output predicate of the spreading program.

• N' : WHead

@[instance_reducible]

instance YolyanComer2026.instDecidableEqWHead : DecidableEq WHead

Equations

• YolyanComer2026.instDecidableEqWHead x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def YolyanComer2026.warao : Subregular.BMRS.Program Seg WHead

(6): N′(x) = if N(x) then ⊤ else if T(x) then ⊥ else if min(x) then ⊥ else N′(p(x)) — recursive through the predecessor: spreading is progressive.

Equations

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

theorem YolyanComer2026.warao_column : List.map (fun (i : ℕ) => Subregular.BMRS.evalFuel warao naote 32 i (Subregular.BMRS.Expr.call WHead.N' YolyanComer2026.x✝)) (List.range 5) = [some true, some true, some true, some false, some false]

Fig. 4: on /naote/ the output column is N′ = ⊤⊤⊤⊥⊥ — [nãõte], spreading blocked by the t.

def YolyanComer2026.waraoChi : System Seg 1

(7): the modal form N′ = μX.(N ∨ (¬T ∧ ♦X)).

Equations

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

@[reducible, inline]

abbrev YolyanComer2026.waraoU : Fin 1 → Set ℕ

The least fixed point on /naote/: nasality holds exactly at positions 0, 1, 2.

Equations

• YolyanComer2026.waraoU x✝ = {i : ℕ | i < 3}

theorem YolyanComer2026.warao_op_le : (waraoChi.op naote) waraoU ≤ waraoU

waraoU is a prefixed point of the system operator.

theorem YolyanComer2026.warao_le_sem : waraoU ≤ waraoChi.sem naote

The three nasal positions are in the least fixed point (unfolding op_sem once per step of the spread).

theorem YolyanComer2026.warao_sem : waraoChi.sem naote = waraoU

The modal semantics on /naote/, exactly.

theorem YolyanComer2026.warao_sat {i : ℕ} : waraoChi.Sat naote i ↔ i < 3

Fig. 5: the modal (7) marks exactly positions 0, 1, 2 of /naote/.

theorem YolyanComer2026.warao_agreement (i : ℕ) (hi : i < 5) : Subregular.BMRS.evalFuel warao naote 32 i (Subregular.BMRS.Expr.call WHead.N' YolyanComer2026.x✝) = some true ↔ waraoChi.Sat naote i

Fig. 4/5 agreement: the BMRS program (6) and the modal formula (7) compute the same nasality column on /naote/.

The translation (Def. 6) and its compositionality (Remark 7)

def YolyanComer2026.tr {α : Type u_1} {n : ℕ} : Formula α n → Subregular.BMRS.Expr α (Fin n)

Def. 6: translate a vectorial modal formula into a BMRS expression whose rule heads are the recursion variables. Modalities substitute a moved term into the translated body; class-negated atoms translate by (3.8)-negation (the evident extension of the paper's clauses, which cover positive atoms).

Equations

• YolyanComer2026.tr YolyanComer2026.Formula.tru = Subregular.BMRS.Expr.tru
• YolyanComer2026.tr YolyanComer2026.Formula.fls = Subregular.BMRS.Expr.fls
• YolyanComer2026.tr YolyanComer2026.Formula.initial = Subregular.BMRS.Expr.initial YolyanComer2026.x✝
• YolyanComer2026.tr YolyanComer2026.Formula.final = Subregular.BMRS.Expr.final YolyanComer2026.x✝
• YolyanComer2026.tr (YolyanComer2026.Formula.label s) = Subregular.BMRS.Expr.label s YolyanComer2026.x✝
• YolyanComer2026.tr (YolyanComer2026.Formula.nlabel s) = (Subregular.BMRS.Expr.label s YolyanComer2026.x✝).ite Subregular.BMRS.Expr.fls Subregular.BMRS.Expr.tru
• YolyanComer2026.tr (YolyanComer2026.Formula.var X) = Subregular.BMRS.Expr.call X YolyanComer2026.x✝
• YolyanComer2026.tr (φ.and ψ) = (YolyanComer2026.tr φ).ite (YolyanComer2026.tr ψ) Subregular.BMRS.Expr.fls
• YolyanComer2026.tr (φ.or ψ) = (YolyanComer2026.tr φ).ite Subregular.BMRS.Expr.tru (YolyanComer2026.tr ψ)
• YolyanComer2026.tr φ.dia = (Subregular.BMRS.Expr.final YolyanComer2026.x✝).ite Subregular.BMRS.Expr.fls ((YolyanComer2026.tr φ).subst YolyanComer2026.x✝.succ)
• YolyanComer2026.tr φ.bdia = (Subregular.BMRS.Expr.initial YolyanComer2026.x✝).ite Subregular.BMRS.Expr.fls ((YolyanComer2026.tr φ).subst YolyanComer2026.x✝.pred)

def YolyanComer2026.System.trProgram {α : Type u_1} {n : ℕ} (χ : System α n) : Subregular.BMRS.Program α (Fin n)

The translated program of a system: one rule per recursion variable.

Equations

• χ.trProgram X = YolyanComer2026.tr (χ.eqs X)

theorem YolyanComer2026.eval_tr {α : Type u_1} {n : ℕ} [DecidableEq α] {P : Subregular.BMRS.Program α (Fin n)} {w : List α} {U : Fin n → Set ℕ} [(X : Fin n) → DecidablePred fun (x : ℕ) => x ∈ U X] (hcall : ∀ (X : Fin n), ∀ j < w.length, Subregular.BMRS.Eval P w j (Subregular.BMRS.Expr.call X YolyanComer2026.x✝) (decide (j ∈ U X))) (φ : Formula α n) {i : ℕ} : i < w.length → Subregular.BMRS.Eval P w i (tr φ) (decide (Formula.Realize w U i φ))

Remark 7 (compositionality of the translation): wherever rule-head calls agree with the recursion variables, tr φ evaluates to the truth value of φ. Thm. 8's SCC induction discharges the hypothesis for directed systems.

theorem YolyanComer2026.warao_tr_agreement (i : ℕ) (hi : i < 5) : Subregular.BMRS.Eval waraoChi.trProgram naote i (tr (waraoChi.eqs 0)) (decide (Formula.Realize naote waraoU i (waraoChi.eqs 0)))

Remark 7 run end-to-end on Warao: the translated program agrees with the modal semantics on /naote/ (waraoU = waraoChi.sem naote by warao_sem), the rule-head hypothesis discharged by direct computation — the concrete shape of Thm. 8.