McCarthy (1981): the Classical Arabic verb

[McC81] (A Prosodic Theory of Nonconcatenative Morphology, LI 12.3) analyzes the Classical Arabic verb as three morphemes on separate autosegmental tiers — a consonantal root, a vocalic melody, and affixal material — associated to a prosodic (CV-skeletal) template. The language-particular apparatus is small (his (26)): the template schema (14a) with rule (14b), the affixes ʔ, t, n, st, the Eighth Binyan Flop (19), and the Erasure rule (24); everything else is the universal association conventions — one-to-one left-to-right, then spreading of the element on the immediate left.

This file implements the conventions as a derivational pipeline (assemble) over the substrate Morphology.TemplateMatch and proves that the pipeline generates the perfective active of all fifteen triliteral binyanim and the perfective passive of the nine that have one, matching Table 1 (p. 385) for the citation root ktb. Gemination falls out as one-to-many association: automatic spreading in IX and XI, Erasure plus reassociation in II, V, and XII, and final-radical spreading for biradical roots (samam, not *sasam — his (33)). Binyan XIII differs from XII only in which tier reassociates after Erasure, a genuine choice point (his (30)), so it is given representationally.

Main declarations

• binyanTemplates — the eight canonical perfective patterns (13a–h).
• SatisfiesSchema — the template schema (14a).
• assemble — affix placement + left-to-right association + spreading + optional Erasure, then vocalism association per rule (41).
• Binyan, perfMatch — the fifteen triliteral binyanim and their derived matches.
• perfectiveActiveParadigm — the binyan paradigm of a root as a substrate Paradigm.

Main results

• templates_satisfy_schema, rule14b_eliminates_cvcvcvc — the template inventory is exactly the schema's output.
• perfective_active_matches_table1, perfective_passive_matches_table1 — the pipeline reproduces Table 1.
• formII_geminates_medial_radical, biradical_geminates_final_radical — gemination as one-to-many association, and why *sasam is underivable.
• geminate_roots_are_biradical — the OCP argument: surface geminate verbs come from OCP-clean biradicals.
• quinqueliteral_strands_final_consonant — maġnaṭ (his (38)).

Roots

def McCarthy1981.ktb : Morphology.ConsonantalRoot String

The citation root ktb "write".

Equations

• McCarthy1981.ktb = { segments := ["k", "t", "b"] }

def McCarthy1981.sm : Morphology.ConsonantalRoot String

The biradical root sm "poison" (surface samam, sammam).

Equations

• McCarthy1981.sm = { segments := ["s", "m"] }

def McCarthy1981.qlq : Morphology.ConsonantalRoot String

The root qlq, with identical first and third radicals — unremarkable for the OCP, which constrains adjacent elements only.

Equations

• McCarthy1981.qlq = { segments := ["q", "l", "q"] }

Templates ((13) and the schema (14a))

def McCarthy1981.cvcvc : Morphology.CVTemplate

CVCVC (13a): binyan I.

Equations

• McCarthy1981.cvcvc = { slots := [Morphology.CVSlot.C, Morphology.CVSlot.V, Morphology.CVSlot.C, Morphology.CVSlot.V, Morphology.CVSlot.C] }

def McCarthy1981.cvccvc : Morphology.CVTemplate

CVCCVC (13b): binyanim II and IV.

Equations

• McCarthy1981.cvccvc = { slots := [Morphology.CVSlot.C, Morphology.CVSlot.V, Morphology.CVSlot.C, Morphology.CVSlot.C, Morphology.CVSlot.V, Morphology.CVSlot.C] }

def McCarthy1981.cvvcvc : Morphology.CVTemplate

CVVCVC (13c): binyan III.

Equations

• McCarthy1981.cvvcvc = { slots := [Morphology.CVSlot.C, Morphology.CVSlot.V, Morphology.CVSlot.V, Morphology.CVSlot.C, Morphology.CVSlot.V, Morphology.CVSlot.C] }

def McCarthy1981.cvcvccvc : Morphology.CVTemplate

CVCVCCVC (13d): binyan V.

Equations

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

def McCarthy1981.cvcvvcvc : Morphology.CVTemplate

CVCVVCVC (13e): binyan VI.

Equations

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

def McCarthy1981.ccvcvc : Morphology.CVTemplate

CCVCVC (13f): binyanim VII, VIII, IX.

Equations

• McCarthy1981.ccvcvc = { slots := [Morphology.CVSlot.C, Morphology.CVSlot.C, Morphology.CVSlot.V, Morphology.CVSlot.C, Morphology.CVSlot.V, Morphology.CVSlot.C] }

def McCarthy1981.ccvccvc : Morphology.CVTemplate

CCVCCVC (13g): binyanim X and XII–XV.

Equations

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

def McCarthy1981.ccvvcvc : Morphology.CVTemplate

CCVVCVC (13h): binyan XI.

Equations

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

def McCarthy1981.binyanTemplates : List Morphology.CVTemplate

The canonical perfective patterns (13a–h).

Equations

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

def McCarthy1981.SatisfiesSchema (t : Morphology.CVTemplate) : Prop

The prosodic-template schema (14a): [({C,CV}) CV ([+seg]) CVC]. A template is generated by choosing the optional first expansion (C or CV), the optional [+seg] element (realized C or V), and the fixed CV and CVC.

Equations

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

@[implicit_reducible]

instance McCarthy1981.instDecidablePredCVTemplateSatisfiesSchema : DecidablePred SatisfiesSchema

Equations

• McCarthy1981.instDecidablePredCVTemplateSatisfiesSchema x✝ = McCarthy1981.instDecidablePredCVTemplateSatisfiesSchema._aux_1 x✝

theorem McCarthy1981.templates_satisfy_schema (t : Morphology.CVTemplate) : t ∈ binyanTemplates → SatisfiesSchema t

Every canonical pattern of (13) is generated by the schema (14a).

theorem McCarthy1981.rule14b_eliminates_cvcvcvc : SatisfiesSchema { slots := [Morphology.CVSlot.C, Morphology.CVSlot.V, Morphology.CVSlot.C, Morphology.CVSlot.V, Morphology.CVSlot.C, Morphology.CVSlot.V, Morphology.CVSlot.C] } ∧ [Morphology.CVSlot.C, Morphology.CVSlot.V, Morphology.CVSlot.C, Morphology.CVSlot.V, Morphology.CVSlot.C, Morphology.CVSlot.V, Morphology.CVSlot.C].eraseIdx 3 = cvccvc.slots

The schema also generates the unattested CVCVCVC — two light syllables followed by CVC — which rule (14b), V → ∅ / [CVC _ CVC], eliminates: deleting the offending V yields the attested CVCCVC.

The association conventions as a pipeline

Conventions (i) and (iii) (his §2.2, after Clements and Ford): melodic elements associate one-to-one left-to-right with the listed slots; each leftover slot receives the melody of the element on its immediate left. Rule (41) associates the final element of a plural vocalism with the final V-slot before the conventions run. Affixal material associates before the root tier (p. 389), so affixes claim their slots first.

def McCarthy1981.associateLR (src : Morphology.AssocSource) (n : ℕ) (slots : List ℕ) : List Morphology.Association

One-to-one left-to-right association of an n-element melody with the listed slots; leftover slots spread the final element. Leftover melodic elements stay unassociated and receive no realization (his (38)).

Equations

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

def McCarthy1981.vocalismAssocs (n : ℕ) (vs : List ℕ) : List Morphology.Association

Vocalism association: rule (41) anchors the final melodic element to the final V-slot; the remaining elements associate left-to-right with the remaining V-slots and the last of them spreads.

Equations

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

def McCarthy1981.eraseRespread (t : Morphology.CVTemplate) (assocs : List Morphology.Association) : List Morphology.Association

The Erasure rule (24), generalized per his (28)–(29): remove the root association at the pre-final C-slot (the C before the final VC), then reassociate that slot from the root association nearest on its left. For a geminate-root input the respread reinstates the erased line, so Erasure is vacuous there (his (34)).

Equations

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

def McCarthy1981.assemble (t : Morphology.CVTemplate) (affixSegs : List String) (affixSlots : List ℕ) (erase : Bool) (voc : List String) (r : Morphology.ConsonantalRoot String) : Morphology.TemplateMatch String

Assemble a match: the affix claims affixSlots, the root associates left-to-right with the remaining C-slots (spreading onto leftovers), Erasure applies if erase, and the vocalism associates with the V-slots per rule (41).

Equations

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

The fifteen triliteral binyanim

inductive McCarthy1981.Binyan : Type

The triliteral binyanim of Table 1.

• I : Binyan
• II : Binyan
• III : Binyan
• IV : Binyan
• V : Binyan
• VI : Binyan
• VII : Binyan
• VIII : Binyan
• IX : Binyan
• X : Binyan
• XI : Binyan
• XII : Binyan
• XIII : Binyan
• XIV : Binyan
• XV : Binyan

@[implicit_reducible]

instance McCarthy1981.instDecidableEqBinyan : DecidableEq Binyan

Equations

• McCarthy1981.instDecidableEqBinyan x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance McCarthy1981.instReprBinyan : Repr Binyan

Equations

• McCarthy1981.instReprBinyan = { reprPrec := McCarthy1981.instReprBinyan.repr }

def McCarthy1981.instReprBinyan.repr : Binyan → ℕ → Std.Format

Equations

• McCarthy1981.instReprBinyan.repr McCarthy1981.Binyan.I prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "McCarthy1981.Binyan.I")).group prec✝
• McCarthy1981.instReprBinyan.repr McCarthy1981.Binyan.II prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "McCarthy1981.Binyan.II")).group prec✝
• McCarthy1981.instReprBinyan.repr McCarthy1981.Binyan.III prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "McCarthy1981.Binyan.III")).group prec✝
• McCarthy1981.instReprBinyan.repr McCarthy1981.Binyan.IV prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "McCarthy1981.Binyan.IV")).group prec✝
• McCarthy1981.instReprBinyan.repr McCarthy1981.Binyan.V prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "McCarthy1981.Binyan.V")).group prec✝
• McCarthy1981.instReprBinyan.repr McCarthy1981.Binyan.VI prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "McCarthy1981.Binyan.VI")).group prec✝
• McCarthy1981.instReprBinyan.repr McCarthy1981.Binyan.VII prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "McCarthy1981.Binyan.VII")).group prec✝
• McCarthy1981.instReprBinyan.repr McCarthy1981.Binyan.VIII prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "McCarthy1981.Binyan.VIII")).group prec✝
• McCarthy1981.instReprBinyan.repr McCarthy1981.Binyan.IX prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "McCarthy1981.Binyan.IX")).group prec✝
• McCarthy1981.instReprBinyan.repr McCarthy1981.Binyan.X prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "McCarthy1981.Binyan.X")).group prec✝
• McCarthy1981.instReprBinyan.repr McCarthy1981.Binyan.XI prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "McCarthy1981.Binyan.XI")).group prec✝
• McCarthy1981.instReprBinyan.repr McCarthy1981.Binyan.XII prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "McCarthy1981.Binyan.XII")).group prec✝
• McCarthy1981.instReprBinyan.repr McCarthy1981.Binyan.XIII prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "McCarthy1981.Binyan.XIII")).group prec✝
• McCarthy1981.instReprBinyan.repr McCarthy1981.Binyan.XIV prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "McCarthy1981.Binyan.XIV")).group prec✝
• McCarthy1981.instReprBinyan.repr McCarthy1981.Binyan.XV prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "McCarthy1981.Binyan.XV")).group prec✝

@[implicit_reducible]

instance McCarthy1981.instFintypeBinyan : Fintype Binyan

Equations

• McCarthy1981.instFintypeBinyan = { elems := { val := ↑McCarthy1981.Binyan.enumList, nodup := McCarthy1981.Binyan.enumList_nodup }, complete := McCarthy1981.instFintypeBinyan._proof_1 }

def McCarthy1981.formXIII (voc : List String) (r : Morphology.ConsonantalRoot String) : Morphology.TemplateMatch String

Binyan XIII (ktawwab): after Erasure on CCVCCVC, reassociation may come from the infixed w-tier rather than the root tier — the choice point distinguishing XIII from XII (his (30)). Given representationally: the affix w is doubly linked, the root associates around it.

Equations

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

def McCarthy1981.perfMatch (voc : List String) (r : Morphology.ConsonantalRoot String) : Binyan → Morphology.TemplateMatch String

The derived match of a binyan: its template, affixal material with the paper's placements — first C-slot(s) for ʔ, t, n, st ((16), (18)), second C-slot for the VIII reflexive after the Flop (19), medial and final slots for the rare XII–XV affixes (27) — and Erasure for II, V, and XII.

Equations

• McCarthy1981.perfMatch voc r McCarthy1981.Binyan.I = McCarthy1981.assemble McCarthy1981.cvcvc [] [] false voc r
• McCarthy1981.perfMatch voc r McCarthy1981.Binyan.II = McCarthy1981.assemble McCarthy1981.cvccvc [] [] true voc r
• McCarthy1981.perfMatch voc r McCarthy1981.Binyan.III = McCarthy1981.assemble McCarthy1981.cvvcvc [] [] false voc r
• McCarthy1981.perfMatch voc r McCarthy1981.Binyan.IV = McCarthy1981.assemble McCarthy1981.cvccvc ["ʔ"] [0] false voc r
• McCarthy1981.perfMatch voc r McCarthy1981.Binyan.V = McCarthy1981.assemble McCarthy1981.cvcvccvc ["t"] [0] true voc r
• McCarthy1981.perfMatch voc r McCarthy1981.Binyan.VI = McCarthy1981.assemble McCarthy1981.cvcvvcvc ["t"] [0] false voc r
• McCarthy1981.perfMatch voc r McCarthy1981.Binyan.VII = McCarthy1981.assemble McCarthy1981.ccvcvc ["n"] [0] false voc r
• McCarthy1981.perfMatch voc r McCarthy1981.Binyan.VIII = McCarthy1981.assemble McCarthy1981.ccvcvc ["t"] [1] false voc r
• McCarthy1981.perfMatch voc r McCarthy1981.Binyan.IX = McCarthy1981.assemble McCarthy1981.ccvcvc [] [] false voc r
• McCarthy1981.perfMatch voc r McCarthy1981.Binyan.X = McCarthy1981.assemble McCarthy1981.ccvccvc ["s", "t"] [0, 1] false voc r
• McCarthy1981.perfMatch voc r McCarthy1981.Binyan.XI = McCarthy1981.assemble McCarthy1981.ccvvcvc [] [] false voc r
• McCarthy1981.perfMatch voc r McCarthy1981.Binyan.XII = McCarthy1981.assemble McCarthy1981.ccvccvc ["w"] [3] true voc r
• McCarthy1981.perfMatch voc r McCarthy1981.Binyan.XIII = McCarthy1981.formXIII voc r
• McCarthy1981.perfMatch voc r McCarthy1981.Binyan.XIV = McCarthy1981.assemble McCarthy1981.ccvccvc ["n"] [3] false voc r
• McCarthy1981.perfMatch voc r McCarthy1981.Binyan.XV = McCarthy1981.assemble McCarthy1981.ccvccvc ["n", "y"] [3, 6] false voc r

def McCarthy1981.activeVoc : List String

The perfective active vocalism: the single melody a, spreading over every V-slot (his (39)/(40a)).

Equations

• McCarthy1981.activeVoc = ["a"]

def McCarthy1981.passiveVoc : List String

The perfective passive vocalism u–i: i anchors to the final V-slot by rule (41), u spreads over the rest (his (39)/(40b)).

Equations

• McCarthy1981.passiveVoc = ["u", "i"]

Table 1: the perfective forms of ktb

def McCarthy1981.table1Active : Binyan → List String

The perfective active column of Table 1 for ktb.

Equations

• McCarthy1981.table1Active McCarthy1981.Binyan.I = ["k", "a", "t", "a", "b"]
• McCarthy1981.table1Active McCarthy1981.Binyan.II = ["k", "a", "t", "t", "a", "b"]
• McCarthy1981.table1Active McCarthy1981.Binyan.III = ["k", "a", "a", "t", "a", "b"]
• McCarthy1981.table1Active McCarthy1981.Binyan.IV = ["ʔ", "a", "k", "t", "a", "b"]
• McCarthy1981.table1Active McCarthy1981.Binyan.V = ["t", "a", "k", "a", "t", "t", "a", "b"]
• McCarthy1981.table1Active McCarthy1981.Binyan.VI = ["t", "a", "k", "a", "a", "t", "a", "b"]
• McCarthy1981.table1Active McCarthy1981.Binyan.VII = ["n", "k", "a", "t", "a", "b"]
• McCarthy1981.table1Active McCarthy1981.Binyan.VIII = ["k", "t", "a", "t", "a", "b"]
• McCarthy1981.table1Active McCarthy1981.Binyan.IX = ["k", "t", "a", "b", "a", "b"]
• McCarthy1981.table1Active McCarthy1981.Binyan.X = ["s", "t", "a", "k", "t", "a", "b"]
• McCarthy1981.table1Active McCarthy1981.Binyan.XI = ["k", "t", "a", "a", "b", "a", "b"]
• McCarthy1981.table1Active McCarthy1981.Binyan.XII = ["k", "t", "a", "w", "t", "a", "b"]
• McCarthy1981.table1Active McCarthy1981.Binyan.XIII = ["k", "t", "a", "w", "w", "a", "b"]
• McCarthy1981.table1Active McCarthy1981.Binyan.XIV = ["k", "t", "a", "n", "b", "a", "b"]
• McCarthy1981.table1Active McCarthy1981.Binyan.XV = ["k", "t", "a", "n", "b", "a", "y"]

theorem McCarthy1981.perfective_active_matches_table1 (b : Binyan) : (perfMatch activeVoc ktb b).spellout = table1Active b

The pipeline derives the entire perfective active column of Table 1.

def McCarthy1981.table1Passive : List (Binyan × List String)

The binyanim with a perfective passive in Table 1 (the gaps are regularly intransitive or stative binyanim), with their forms for ktb.

Equations

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

theorem McCarthy1981.perfective_passive_matches_table1 (p : Binyan × List String) : p ∈ table1Passive → (perfMatch passiveVoc ktb p.1).spellout = p.2

Swapping in the u–i vocalism derives the perfective passive column — the voice contrast is a vocalism morpheme, nothing else changes.

theorem McCarthy1981.perfMatch_ordered_on_root (b : Binyan) : (perfMatch activeVoc ktb b).OrderedOn Morphology.AssocSource.root

Every derived match associates its root tier without crossing lines.

Gemination as one-to-many association

def McCarthy1981.rootLinkCount (m : Morphology.TemplateMatch String) (i : ℕ) : ℕ

The number of association lines from root element i.

Equations

• McCarthy1981.rootLinkCount m i = (List.filter (fun (a : Morphology.Association) => a.source == Morphology.AssocSource.root && a.melodyIndex == i) m.associations).length

theorem McCarthy1981.formII_geminates_medial_radical : rootLinkCount (perfMatch activeVoc ktb Binyan.II) 1 = 2 ∧ rootLinkCount (perfMatch activeVoc ktb Binyan.II) 0 = 1 ∧ rootLinkCount (perfMatch activeVoc ktb Binyan.II) 2 = 1

Binyan II gemination (kattab, his (17)): the medial radical is doubly linked — Erasure removes the final radical's medial line and reassociation respreads the medial radical — while the outer radicals stay single.

theorem McCarthy1981.biradical_geminates_final_radical : (perfMatch activeVoc sm Binyan.I).spellout = ["s", "a", "m", "a", "m"] ∧ rootLinkCount (perfMatch activeVoc sm Binyan.I) 1 = 2 ∧ rootLinkCount (perfMatch activeVoc sm Binyan.I) 0 = 1

Biradical sm in binyan I surfaces as samam (his (33)): left-to-right association reaches the second radical before the leftover slot, so only the final radical geminates — *sasam, with a geminated first radical, is underivable from the conventions.

theorem McCarthy1981.biradical_formII_sammam : (perfMatch activeVoc sm Binyan.II).spellout = ["s", "a", "m", "m", "a", "m"]

Biradical sm in binyan II surfaces as sammam (his (34)): Erasure applies but reassociation reinstates the erased line, so its effect is automatically reversed.

The OCP argument (pp. 395–397)

Surface geminate verbs (samam) come from OCP-clean biradicals plus spreading, so the root inventory needs no roots with adjacent identical radicals; qlq-type roots, identical only at a distance, are unconstrained. The OCP also excludes quadriliteral *ddrj — and indeed no QI verbs of the type *dadraj occur.

theorem McCarthy1981.attested_roots_ocp_clean : sm.IsOCPClean ∧ qlq.IsOCPClean

The biradical sm and the first-third-identical qlq are OCP-clean.

theorem McCarthy1981.geminate_roots_are_biradical : ¬{ segments := ["s", "m", "m"] }.IsOCPClean ∧ ¬{ segments := ["d", "d", "r", "j"] }.IsOCPClean

Hypothetical smm and ddrj, with adjacent identical radicals, violate the root-level OCP — the shapes the theory correctly excludes from the lexicon.

Stranding (his (38))

theorem McCarthy1981.quinqueliteral_strands_final_consonant : (assemble cvccvc [] [] false activeVoc { segments := ["m", "ġ", "n", "ṭ", "š"] }).spellout = ["m", "a", "ġ", "n", "a", "ṭ"]

The denominal quinqueliteral root mġnṭš on the QI template CVCCVC: left-to-right association exhausts the C-slots at the fourth radical, the final š remains unassociated and unrealized — maġnaṭ, with loss at the right edge, exactly as attested.

The binyan paradigm as a cell-realization map

def McCarthy1981.binyanList : List Binyan

The binyanim in Table 1 order.

Equations

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

def McCarthy1981.perfectiveActiveParadigm (r : Morphology.ConsonantalRoot String) : Morphology.Paradigm 15 (List String)

The perfective active paradigm of a root: the substrate Paradigm over the fifteen binyan cells, realized by the association pipeline. The root is the lexeme index; each cell contributes its template, affix, and Erasure setting.

Equations

• McCarthy1981.perfectiveActiveParadigm r i = (McCarthy1981.perfMatch McCarthy1981.activeVoc r (McCarthy1981.binyanList.getD (↑i) McCarthy1981.Binyan.I)).spellout

theorem McCarthy1981.perfectiveActiveParadigm_ktb (i : Fin 15) : perfectiveActiveParadigm ktb i = table1Active (binyanList.getD (↑i) Binyan.I)

The paradigm of ktb reads off Table 1 cell by cell.