Keenan & Comrie (1977) [KC77]

Noun Phrase Accessibility and Universal Grammar. Linguistic Inquiry 8(1): 63–99.

Formalizes the three Hierarchy Constraints (HCs) and the derived Primary Relativization Constraint (PRC) from [KC77], verified against a subset of the paper's Table 1 data (pp. 76-79).

Architecture

This file derives K&C's typological theorems directly from Fragments.{Lang}.relMarkers : List Marker, the per-language data layer encoding actual linguistic markers (particles, pronouns, verbal suffixes). No intermediate KCProfile/StrategyEntry schema — predicates and aggregations are stated over List Marker directly, projecting through Marker.{positions, bearsCaseMarking, rcPosition} as needed.

The Fragment files cite [KC79] (the per-language exemplification appendix originally intended for publication with K&C 1977 — Language 55(2): 333–351) inline where its sentence-level examples back the descriptive marker data.

Hierarchy Constraints

The paper proposes three constraints on how languages form relative clauses, building on the Accessibility Hierarchy (AH):

SU > DO > IO > OBL > GEN > OCOMP

• HC₁ (p. 67): A language must be able to relativize subjects.
• HC₂ (Continuity) (p. 67): Any RC-forming strategy must apply to a continuous segment of the AH.
• HC₃ (Cut-off) (p. 67): Strategies that apply at one point may cease at any lower point.

From HC₁ + HC₂, the Primary Relativization Constraint (p. 68) follows: if a language's primary strategy (one that covers subjects) can apply to a low position N, it can apply to all positions above N. Non-primary strategies need not satisfy this — they may cover a continuous segment that excludes subjects (e.g., the +case strategy covering IO–OCOMP but not SU–DO in Welsh and Arabic, p. 70 + Table 1 p. 76).

Multi-Strategy Profiles

The paper's key empirical contribution is showing that languages typically have multiple relativization strategies, each covering a different contiguous segment of the AH. The ±case distinction (whether the relative element bears case marking) is the primary parameter distinguishing strategies.

Sample

Seventeen of the paper's Table 1 languages plus Yoruba (post-1977) cover the key patterns: gap-to-resumptive split (Welsh, Hebrew, Arabic, Toba Batak; prenominal and reaching OCOMP in Mandarin; below a participial cut-off in Turkish), multi-strategy with prenominal RCs (Korean, Finnish, Japanese, German), single-strategy (Malagasy, Basque, French, Russian), subject-only with voice-mediated promotion (Malagasy, Tagalog), correlative (Hindi), and per-position strategy split with serial-verb-mediated obliques (Yoruba). Every AH position from SU to GEN is attested as a primary cut-off (each_upper_cutoff_attested).

def KeenanComrie1977.SatisfiesHC1 (markers : List RelativeClause.Marker) : Prop

HC₁: a language can relativize subjects iff some marker covers SU.

Equations

• KeenanComrie1977.SatisfiesHC1 markers = ∃ m ∈ markers, m.Covers RelativeClause.AHPosition.subject

@[instance_reducible]

instance KeenanComrie1977.instDecidableSatisfiesHC1 (markers : List RelativeClause.Marker) : Decidable (SatisfiesHC1 markers)

Equations

• KeenanComrie1977.instDecidableSatisfiesHC1 markers = id inferInstance

def KeenanComrie1977.SatisfiesHC2 (markers : List RelativeClause.Marker) : Prop

HC₂: every marker covers a contiguous segment of the AH.

Equations

• KeenanComrie1977.SatisfiesHC2 markers = ∀ m ∈ markers, m.IsContinuous

@[instance_reducible]

instance KeenanComrie1977.instDecidableSatisfiesHC2 (markers : List RelativeClause.Marker) : Decidable (SatisfiesHC2 markers)

Equations

• KeenanComrie1977.instDecidableSatisfiesHC2 markers = id inferInstance

def KeenanComrie1977.SatisfiesPRC (markers : List RelativeClause.Marker) : Prop

PRC: every primary marker is upward-closed on the AH. If marker m is primary and covers position pos, then m covers every position above pos. This is the paper's Primary Relativization Constraint (p. 68), which follows from HC₂ for primary strategies (see prc_from_hc2 below for the general derivation).

Equations

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

@[instance_reducible]

instance KeenanComrie1977.instDecidableSatisfiesPRC (markers : List RelativeClause.Marker) : Decidable (SatisfiesPRC markers)

Equations

• KeenanComrie1977.instDecidableSatisfiesPRC markers = id inferInstance

def KeenanComrie1977.lowestCovered (markers : List RelativeClause.Marker) : RelativeClause.AHPosition

The lowest AH position covered by any marker in the list (i.e., the deepest the language can reach). Returns .subject if even SU is uncovered (vacuously, since HC₁ would be violated).

Equations

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

Per-language abbrevs over Fragment marker lists. The original 17-language sample from the paper plus Yoruba (added later via [Awo78] + [KC79]).

@[reducible, inline]

abbrev KeenanComrie1977.english : List RelativeClause.Marker

Equations

• KeenanComrie1977.english = English.relMarkers

@[reducible, inline]

abbrev KeenanComrie1977.welsh : List RelativeClause.Marker

Equations

• KeenanComrie1977.welsh = Welsh.relMarkers

@[reducible, inline]

abbrev KeenanComrie1977.arabic : List RelativeClause.Marker

Equations

• KeenanComrie1977.arabic = [Arabic.ModernStandard.relAlladhi, Arabic.ModernStandard.relResumptive]

@[reducible, inline]

abbrev KeenanComrie1977.hebrew : List RelativeClause.Marker

Equations

• KeenanComrie1977.hebrew = Hebrew.relMarkers

@[reducible, inline]

abbrev KeenanComrie1977.tobaBatak : List RelativeClause.Marker

Equations

• KeenanComrie1977.tobaBatak = TobaBatak.relMarkers

@[reducible, inline]

abbrev KeenanComrie1977.korean : List RelativeClause.Marker

Equations

• KeenanComrie1977.korean = Korean.relMarkers

@[reducible, inline]

abbrev KeenanComrie1977.finnish : List RelativeClause.Marker

Equations

• KeenanComrie1977.finnish = Finnish.relMarkers

@[reducible, inline]

abbrev KeenanComrie1977.malagasy : List RelativeClause.Marker

Equations

• KeenanComrie1977.malagasy = Malagasy.relMarkers

@[reducible, inline]

abbrev KeenanComrie1977.mandarin : List RelativeClause.Marker

K&C's "Chinese (spoken Pekingese)" (Table 1 pp. 76-79).

Equations

• KeenanComrie1977.mandarin = Mandarin.relMarkers

@[reducible, inline]

abbrev KeenanComrie1977.basque : List RelativeClause.Marker

Equations

• KeenanComrie1977.basque = Basque.relMarkers

@[reducible, inline]

abbrev KeenanComrie1977.french : List RelativeClause.Marker

Equations

• KeenanComrie1977.french = French.relMarkers

@[reducible, inline]

abbrev KeenanComrie1977.german : List RelativeClause.Marker

Equations

• KeenanComrie1977.german = German.relMarkers

@[reducible, inline]

abbrev KeenanComrie1977.hindi : List RelativeClause.Marker

Table 1's "Hindi".

Equations

• KeenanComrie1977.hindi = HindiUrdu.relMarkers

@[reducible, inline]

abbrev KeenanComrie1977.japanese : List RelativeClause.Marker

Equations

• KeenanComrie1977.japanese = Japanese.relMarkers

@[reducible, inline]

abbrev KeenanComrie1977.russian : List RelativeClause.Marker

Equations

• KeenanComrie1977.russian = Russian.relMarkers

@[reducible, inline]

abbrev KeenanComrie1977.tagalog : List RelativeClause.Marker

Equations

• KeenanComrie1977.tagalog = Tagalog.relMarkers

@[reducible, inline]

abbrev KeenanComrie1977.turkish : List RelativeClause.Marker

Equations

• KeenanComrie1977.turkish = Turkish.relMarkers

@[reducible, inline]

abbrev KeenanComrie1977.yoruba : List RelativeClause.Marker

Equations

• KeenanComrie1977.yoruba = Yoruba.relMarkers

def KeenanComrie1977.originalSample : List (List RelativeClause.Marker)

The 17-language sub-sample from the original paper Table 1 (pp. 76-79).

Equations

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

def KeenanComrie1977.allSamples : List (List RelativeClause.Marker)

The original 17-language sample plus Yoruba (the only post-1977 addition; refutes one of the paper's implicit ±case generalizations — see yoruba_refutes_minus_case_covers_subjects below).

Equations

• KeenanComrie1977.allSamples = KeenanComrie1977.originalSample ++ [KeenanComrie1977.yoruba]

theorem KeenanComrie1977.sample_size : allSamples.length = 18

theorem KeenanComrie1977.hc1_verified (markers : List RelativeClause.Marker) : markers ∈ allSamples → SatisfiesHC1 markers

HC₁ holds: every language in the sample can relativize subjects.

theorem KeenanComrie1977.hc2_verified (markers : List RelativeClause.Marker) : markers ∈ allSamples → SatisfiesHC2 markers

HC₂ holds: every marker in every sampled language covers a contiguous AH segment.

theorem KeenanComrie1977.prc_verified (markers : List RelativeClause.Marker) : markers ∈ allSamples → SatisfiesPRC markers

PRC holds: every primary marker satisfies upward closure on the AH.

theorem KeenanComrie1977.every_language_has_primary (markers : List RelativeClause.Marker) : markers ∈ allSamples → ∃ m ∈ markers, m.IsPrimary

Restating HC₁ in terms of Marker.IsPrimary: every language has at least one primary marker.

theorem KeenanComrie1977.isUpperSet_of_satisfiesPRC {markers : List RelativeClause.Marker} (h : SatisfiesPRC markers) {m : RelativeClause.Marker} (hm : m ∈ markers) (hp : m.IsPrimary) : IsUpperSet {p : RelativeClause.AHPosition | m.Covers p}

The PRC is order upward-closure: in any PRC-satisfying language, a primary marker's coverage is an IsUpperSet on the AHPosition scale order. Keenan & Comrie's Primary Relativization Constraint is the order-theoretic "upper set" property — the same IsUpperSet that Core.Order.Markedness uses for differential-marking cutoffs — rather than a bespoke rank predicate.

theorem KeenanComrie1977.minus_case_covers_subjects_in_original_sample (markers : List RelativeClause.Marker) : markers ∈ originalSample → ∀ m ∈ markers, m.bearsCaseMarking = false → m.Covers RelativeClause.AHPosition.subject

In the original 17-language sub-sample, every -case marker covers subjects. The -case (gap/deletion) strategy is always primary when present in those languages.

REFUTED by Yoruba — see yoruba_refutes_minus_case_covers_subjects below: Yoruba has gap markers for DO and OBL that do not cover SU because subject relativization independently uses pronoun retention (ó, per [Awo78] §6.19).

theorem KeenanComrie1977.yoruba_refutes_minus_case_covers_subjects : ∃ m ∈ yoruba, m.bearsCaseMarking = false ∧ ¬m.Covers RelativeClause.AHPosition.subject

[KC79] effectively documents Yoruba as a refutation of the gap-implies-subject correlation. Yoruba's IO/OBL relativization is mediated by serial-verb DO recasting (K&C 1979 p. 349), producing -case markers that do not cover SU. SU relativization independently uses pronoun retention (ó, K&C 1979 p. 350 analyzes as verb agreement; descriptive surface form per [Awo78] §6.19).

theorem KeenanComrie1977.most_have_multiple_strategies : (List.filter (fun (x : List RelativeClause.Marker) => decide (x.length > 1)) allSamples).length ≥ 5

Most languages in the sample use more than one marker, with markers covering different segments.

theorem KeenanComrie1977.plus_case_secondary_excludes_su (markers : List RelativeClause.Marker) : markers ∈ allSamples → ∀ m ∈ markers, m.bearsCaseMarking = true → ¬m.IsPrimary → ¬m.Covers RelativeClause.AHPosition.subject

+case markers that are non-primary (don't cover SU) never cover SU in our sample. This reflects the typological generalization that pronoun retention is used for lower, not higher, AH positions. Holds across all 18 languages including Yoruba.

theorem KeenanComrie1977.each_upper_cutoff_attested (p : RelativeClause.AHPosition) : p ∈ [RelativeClause.AHPosition.subject, RelativeClause.AHPosition.directObject, RelativeClause.AHPosition.indirectObject, RelativeClause.AHPosition.oblique, RelativeClause.AHPosition.genitive] → ∃ markers ∈ allSamples, ∃ m ∈ markers, m.IsPrimary ∧ lowestCovered [m] = p

Every AH position from SU down to GEN is attested in the sample as the cut-off of some primary marker — the paper's §1.3 justification of HC₃ (each point on the AH is a possible cut-off point). The paper's OCOMP-cutoff witnesses (Czech, Slovenian, Urhobo) are not in the encoded sample.

theorem KeenanComrie1977.toba_batak_do_gap (m : RelativeClause.Marker) : m ∈ tobaBatak → ¬m.Covers RelativeClause.AHPosition.directObject

Toba Batak has a genuine gap at DO: neither marker can relativize direct objects. This is consistent with the HCs because each individual marker is contiguous — the gap exists between markers, not within one. The paper notes this explicitly (p. 68-69: "direct objects cannot be relativized using this or any other strategy in Toba").

theorem KeenanComrie1977.toba_batak_hc2 : SatisfiesHC2 tobaBatak

Despite the DO gap, Toba Batak satisfies HC₂: both individual markers are contiguous (SU alone; IO–GEN alone).

theorem KeenanComrie1977.english_full_coverage : List.map (fun (x : RelativeClause.Marker) => x.positions.length) english = [2, 4]

English (Table 1 p. 76): -case that/∅ covers SU/DO (2 positions); +case who/whom covers IO/OBL/GEN/OCOMP (4 positions).

theorem KeenanComrie1977.welsh_strategy_split : welsh.length = 2 ∧ List.map (fun (m : RelativeClause.Marker) => decide (m.Covers RelativeClause.AHPosition.subject)) welsh = [true, false] ∧ List.map (fun (m : RelativeClause.Marker) => decide (m.Covers RelativeClause.AHPosition.directObject)) welsh = [true, false] ∧ List.map (fun (m : RelativeClause.Marker) => decide (m.Covers RelativeClause.AHPosition.indirectObject)) welsh = [false, true] ∧ List.map (fun (m : RelativeClause.Marker) => decide (m.Covers RelativeClause.AHPosition.objComparison)) welsh = [false, true]

Welsh (Table 1 p. 76; paper §1.3.2 p. 70): markers split at DO/IO. -case (particle a) covers SU/DO; +case (particle y + resumptive) covers IO/OBL/GEN/OCOMP.

theorem KeenanComrie1977.arabic_primary_su_only : List.map (fun (m : RelativeClause.Marker) => decide (m.Covers RelativeClause.AHPosition.subject)) arabic = [true, false] ∧ List.map (fun (m : RelativeClause.Marker) => decide (m.Covers RelativeClause.AHPosition.directObject)) arabic = [false, true]

Arabic (MSA) (Table 1 p. 76): the relative pronoun alladhī/allatii used alone (-case strategy) covers SU only; alladhī/allatii with a resumptive pronoun (+case strategy) covers DO–OCOMP.

theorem KeenanComrie1977.malagasy_su_only : malagasy.length = 1 ∧ List.map (fun (m : RelativeClause.Marker) => decide (m.Covers RelativeClause.AHPosition.subject)) malagasy = [true] ∧ List.map (fun (m : RelativeClause.Marker) => decide (m.Covers RelativeClause.AHPosition.directObject)) malagasy = [false]

Malagasy (Table 1 p. 78; paper §1.3.1 p. 69-70): single marker, SU only.

theorem KeenanComrie1977.korean_primary_su_to_obl : List.map (fun (m : RelativeClause.Marker) => decide (m.Covers RelativeClause.AHPosition.subject)) korean = [true, false] ∧ List.map (fun (m : RelativeClause.Marker) => decide (m.Covers RelativeClause.AHPosition.oblique)) korean = [true, false] ∧ List.map (fun (m : RelativeClause.Marker) => decide (m.Covers RelativeClause.AHPosition.genitive)) korean = [false, true]

Korean (Table 1 p. 78; paper §1.3.4 p. 74): -case adnominal verb suffix covers SU/DO/IO/OBL but not GEN; +case genitive marker covers GEN only.

theorem KeenanComrie1977.mandarin_retention_reaches_ocomp : List.map (fun (m : RelativeClause.Marker) => decide (m.Covers RelativeClause.AHPosition.subject)) mandarin = [true, false] ∧ List.map (fun (m : RelativeClause.Marker) => decide (m.Covers RelativeClause.AHPosition.directObject)) mandarin = [true, true] ∧ lowestCovered mandarin = RelativeClause.AHPosition.objComparison

Mandarin — K&C's "Chinese (spoken Pekingese)" (Table 1 pp. 76-79): -case gap covers SU/DO; +case retention covers DO–OCOMP. The two strategies overlap at DO (retention optional there, Table 2), and retention reaches the hierarchy floor despite the prenominal RC.

theorem KeenanComrie1977.basque_cutoff_at_io : basque.length = 1 ∧ lowestCovered basque = RelativeClause.AHPosition.indirectObject

Basque (Table 1 p. 76; §1.3.3 p. 72): single -case strategy covering SU/DO/IO — the sample's witness that IO is a possible primary cut-off.

theorem KeenanComrie1977.french_single_strategy_to_gen : french.length = 1 ∧ lowestCovered french = RelativeClause.AHPosition.genitive

French (Table 1 p. 76): the single +case relative pronoun system covers SU–GEN (OCOMP blank).

theorem KeenanComrie1977.german_participial_su_only : List.map (fun (m : RelativeClause.Marker) => decide (m.Covers RelativeClause.AHPosition.subject)) german = [true, true] ∧ List.map (fun (x : RelativeClause.Marker) => x.positions.length) german = [5, 1]

German (Table 1 p. 77; §1.1 exx. (1)-(2), §1.3.1 p. 70): the +case relative pronoun covers SU–GEN; the -case participial strategy covers SU only.

theorem KeenanComrie1977.hindi_both_strategies_primary (m : RelativeClause.Marker) : m ∈ hindi → m.IsPrimary ∧ lowestCovered [m] = RelativeClause.AHPosition.genitive

Hindi (Table 1 p. 77): both +case strategies (postnominal jo, the correlative coded "internal" there) are primary and cover SU–GEN; OCOMP is treated as an oblique.

theorem KeenanComrie1977.japanese_gap_to_gen : lowestCovered japanese = RelativeClause.AHPosition.genitive ∧ List.map (fun (m : RelativeClause.Marker) => decide (m.Covers RelativeClause.AHPosition.genitive)) japanese = [true, true]

Japanese (Table 1 p. 77): the -case gap strategy reaches GEN (OBL and GEN only for some NPs); retention appears only at GEN.

theorem KeenanComrie1977.russian_single_strategy_to_gen : russian.length = 1 ∧ lowestCovered russian = RelativeClause.AHPosition.genitive

Russian (Table 1 p. 78): the single declining relative pronoun kotoryj covers SU–GEN (OCOMP blank).

theorem KeenanComrie1977.tagalog_su_only (m : RelativeClause.Marker) : m ∈ tagalog → m.positions = [RelativeClause.AHPosition.subject]

Tagalog (Table 1 p. 79; §1.3.1 p. 70): two -case strategies (postnominal and prenominal linker), each covering SU only.

theorem KeenanComrie1977.turkish_retention_below_participles : lowestCovered turkish = RelativeClause.AHPosition.objComparison ∧ List.map (fun (m : RelativeClause.Marker) => decide (m.Covers RelativeClause.AHPosition.oblique)) turkish = [true, false] ∧ List.map (fun (m : RelativeClause.Marker) => decide (m.Covers RelativeClause.AHPosition.genitive)) turkish = [false, true]

Turkish (Table 1 p. 79): -case participles cover SU–OBL; +case retention covers GEN and (marginally) OCOMP — the Korean pattern plus retention below the participial cut-off.

theorem KeenanComrie1977.finnish_plus_case_is_primary : List.map (fun (x : RelativeClause.Marker) => x.bearsCaseMarking) finnish = [true, false] ∧ List.map (fun (m : RelativeClause.Marker) => decide m.IsPrimary) finnish = [true, true]

Finnish (Table 1 p. 76; paper §1.3.2 p. 70-71): the +case marker joka is the broader/primary one (covers SU–GEN); the -case participial marker also covers SU but is narrower (SU/DO only).

theorem KeenanComrie1977.yoruba_strategy_breakdown : yoruba.length = 4 ∧ List.map (fun (x : RelativeClause.Marker) => x.bearsCaseMarking) yoruba = [false, false, false, true] ∧ List.map (fun (m : RelativeClause.Marker) => decide m.IsPrimary) yoruba = [true, false, false, false]

Yoruba: 4 per-position markers. relTiSubject (-case, primary, only SU); relTiObject (-case, NOT primary, only DO); relTiOblique (-case, NOT primary, IO/OBL); relTiGenitive (+case, NOT primary, GEN only). All 4 individually contiguous on the AH, so HC₂ holds.

HC₂ ("any RC-forming strategy must apply to a continuous segment of the AH") is a paper-anchored claim. The contiguity machinery (contiguousOnAH, AHPosition.rank) lives in Typology/RelativeClause/Basic.lean because it mirrors Features/Case/Basic.lean's IsValidInventory and is genuinely framework-agnostic. The specific contiguous-segment witnesses below exemplify HC₂ on the AH and are part of [KC77]'s core argumentation.

theorem KeenanComrie1977.full_ah_contiguous : RelativeClause.contiguousOnAH RelativeClause.AHPosition.all = true

The full hierarchy [SU, DO, IO, OBL, GEN, OCOMP] is contiguous.

theorem KeenanComrie1977.singleton_contiguous : RelativeClause.contiguousOnAH [RelativeClause.AHPosition.subject] = true

A single position is trivially contiguous.

theorem KeenanComrie1977.su_do_contiguous : RelativeClause.contiguousOnAH [RelativeClause.AHPosition.subject, RelativeClause.AHPosition.directObject] = true

[SU, DO] is contiguous.

theorem KeenanComrie1977.io_obl_gen_contiguous : RelativeClause.contiguousOnAH [RelativeClause.AHPosition.indirectObject, RelativeClause.AHPosition.oblique, RelativeClause.AHPosition.genitive] = true

[IO, OBL, GEN] is contiguous (a non-primary segment).

theorem KeenanComrie1977.su_do_obl_not_contiguous : RelativeClause.contiguousOnAH [RelativeClause.AHPosition.subject, RelativeClause.AHPosition.directObject, RelativeClause.AHPosition.oblique] = false

[SU, DO, OBL] is NOT contiguous (skips IO at rank 4).

The PRC is the paper's main derivation: it follows from HC₁ + HC₂ rather than being an independent stipulation. The general proof lives here (paper content), not in Typology/RelativeClause/Basic.lean (substrate).

theorem KeenanComrie1977.prc_from_hc2 (positions : List RelativeClause.AHPosition) (h_contig : RelativeClause.contiguousOnAH positions = true) (h_su : (positions.any fun (x : RelativeClause.AHPosition) => x == RelativeClause.AHPosition.subject) = true) (p above : RelativeClause.AHPosition) (hp : (positions.any fun (x : RelativeClause.AHPosition) => x == p) = true) (habove : above.rank > p.rank) : (positions.any fun (x : RelativeClause.AHPosition) => x == above) = true

Primary Relativization Constraint (general proof).

If a list of AH positions is contiguous (HC₂) and contains .subject (i.e., the strategy is primary), then the list is upward-closed: for any covered position p, all positions above p on the AH are also covered.

This proves that the PRC is a logical consequence of HC₂ + being primary, not an independent constraint — the paper's core derivation ([KC77] p. 68: "PRC₂ follows directly from HC₂ and the definition of primary").

theorem KeenanComrie1977.prc_all_primary_segments : have segs := [[RelativeClause.AHPosition.subject], [RelativeClause.AHPosition.subject, RelativeClause.AHPosition.directObject], [RelativeClause.AHPosition.subject, RelativeClause.AHPosition.directObject, RelativeClause.AHPosition.indirectObject], [RelativeClause.AHPosition.subject, RelativeClause.AHPosition.directObject, RelativeClause.AHPosition.indirectObject, RelativeClause.AHPosition.oblique], [RelativeClause.AHPosition.subject, RelativeClause.AHPosition.directObject, RelativeClause.AHPosition.indirectObject, RelativeClause.AHPosition.oblique, RelativeClause.AHPosition.genitive], [RelativeClause.AHPosition.subject, RelativeClause.AHPosition.directObject, RelativeClause.AHPosition.indirectObject, RelativeClause.AHPosition.oblique, RelativeClause.AHPosition.genitive, RelativeClause.AHPosition.objComparison]]; (segs.all fun (seg : List RelativeClause.AHPosition) => (RelativeClause.contiguousOnAH seg && seg.any fun (x : RelativeClause.AHPosition) => x == RelativeClause.AHPosition.subject) && seg.all fun (p : RelativeClause.AHPosition) => RelativeClause.AHPosition.all.all fun (above : RelativeClause.AHPosition) => if above.rank > p.rank then seg.any fun (x : RelativeClause.AHPosition) => x == above else true) = true

All 6 canonical primary strategy segments are upward-closed. These are the only possible contiguous segments containing .subject.