Word-Order Typology (@cite{dryer-haspelmath-2013} / WALS)

@cite{dryer-1992} @cite{dryer-haspelmath-2013} @cite{gibson-2025} @cite{greenberg-1963}

WALS data from @cite{gibson-2025}: cross-linguistic counts of harmonic vs disharmonic word-order pairings. @cite{dryer-1992} documents that languages overwhelmingly prefer consistent head direction across construction types (the head-direction generalization, @cite{greenberg-1963}).

Data

Three cross-tabulations from WALS:

• Table 1: VO × Adposition order (981 languages)
• Table 2: VO × Subordinator order (456 languages)
• Table 3: VO × Relative clause order (665 languages)

Each table is a 2×2 contingency table: VO/OV × head-initial/head-final for the second construction. Harmonic cells (both HI or both HF) dominate.

Single-Word Exceptions (Table 4)

Some constructions show disharmonic tendencies cross-linguistically: adjective-noun, demonstrative-noun, intensifier-adjective, negator-verb. @cite{gibson-2025} argues these are cases where the dependent is a single word (no recursive subtree), so head direction is irrelevant to DLM.

structure Phenomena.WordOrder.Typology.AlignmentCell : Type

A single cell in a 2×2 alignment table. dir1 is the direction for the first construction (verb-object order), dir2 is the direction for the second construction.

• dir1 : HeadDirection
• dir2 : HeadDirection
• count : Nat

instance Phenomena.WordOrder.Typology.instReprAlignmentCell : Repr AlignmentCell

Equations

• Phenomena.WordOrder.Typology.instReprAlignmentCell = { reprPrec := Phenomena.WordOrder.Typology.instReprAlignmentCell.repr }

def Phenomena.WordOrder.Typology.instReprAlignmentCell.repr : AlignmentCell → Nat → Std.Format

Equations

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

instance Phenomena.WordOrder.Typology.instDecidableEqAlignmentCell : DecidableEq AlignmentCell

Equations

• Phenomena.WordOrder.Typology.instDecidableEqAlignmentCell = Phenomena.WordOrder.Typology.instDecidableEqAlignmentCell.decEq

def Phenomena.WordOrder.Typology.instDecidableEqAlignmentCell.decEq (x✝ x✝¹ : AlignmentCell) : Decidable (x✝ = x✝¹)

Equations

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

def Phenomena.WordOrder.Typology.instBEqAlignmentCell.beq : AlignmentCell → AlignmentCell → Bool

Equations

• Phenomena.WordOrder.Typology.instBEqAlignmentCell.beq { dir1 := a, dir2 := a_1, count := a_2 } { dir1 := b, dir2 := b_1, count := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Phenomena.WordOrder.Typology.instBEqAlignmentCell.beq x✝¹ x✝ = false

instance Phenomena.WordOrder.Typology.instBEqAlignmentCell : BEq AlignmentCell

Equations

• Phenomena.WordOrder.Typology.instBEqAlignmentCell = { beq := Phenomena.WordOrder.Typology.instBEqAlignmentCell.beq }

def Phenomena.WordOrder.Typology.AlignmentCell.isHarmonic (c : AlignmentCell) : Bool

Whether an alignment cell represents a harmonic (consistent-direction) pair.

Equations

• c.isHarmonic = (c.dir1 == c.dir2)

structure Phenomena.WordOrder.Typology.CrossTab : Type

A 2×2 cross-tabulation of two construction types.

• name : String
• construction1 : String
• construction2 : String
• hihi : AlignmentCell
• hihf : AlignmentCell
• hfhi : AlignmentCell
• hfhf : AlignmentCell

instance Phenomena.WordOrder.Typology.instReprCrossTab : Repr CrossTab

Equations

• Phenomena.WordOrder.Typology.instReprCrossTab = { reprPrec := Phenomena.WordOrder.Typology.instReprCrossTab.repr }

def Phenomena.WordOrder.Typology.instReprCrossTab.repr : CrossTab → Nat → Std.Format

Equations

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

def Phenomena.WordOrder.Typology.CrossTab.harmonicCount (t : CrossTab) : Nat

Total count of harmonic (diagonal) cells.

Equations

• t.harmonicCount = t.hihi.count + t.hfhf.count

def Phenomena.WordOrder.Typology.CrossTab.disharmonicCount (t : CrossTab) : Nat

Total count of disharmonic (off-diagonal) cells.

Equations

• t.disharmonicCount = t.hihf.count + t.hfhi.count

def Phenomena.WordOrder.Typology.CrossTab.totalCount (t : CrossTab) : Nat

Total number of languages in the table.

Equations

• t.totalCount = t.harmonicCount + t.disharmonicCount

def Phenomena.WordOrder.Typology.CrossTab.harmonicDominant (t : CrossTab) : Bool

Whether harmonic pairings are the majority.

Equations

• t.harmonicDominant = decide (t.harmonicCount > t.disharmonicCount)

def Phenomena.WordOrder.Typology.voAdposition : CrossTab

Table 1: Verb-Object order × Adposition order (@cite{dryer-haspelmath-2013}, WALS). @cite{gibson-2025} Table 1. 981 languages.

Equations

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

def Phenomena.WordOrder.Typology.voSubordinator : CrossTab

Table 2: Verb-Object order × Subordinator order (@cite{dryer-haspelmath-2013}, WALS). @cite{gibson-2025} Table 2. 456 languages.

Equations

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

def Phenomena.WordOrder.Typology.voRelativeClause : CrossTab

Table 3: Verb-Object order × Relative clause order (@cite{dryer-haspelmath-2013}, WALS). @cite{gibson-2025} Table 3. 665 languages.

Equations

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

def Phenomena.WordOrder.Typology.allTables : List CrossTab

All three cross-tabulations from @cite{gibson-2025}.

Equations

• Phenomena.WordOrder.Typology.allTables = [Phenomena.WordOrder.Typology.voAdposition, Phenomena.WordOrder.Typology.voSubordinator, Phenomena.WordOrder.Typology.voRelativeClause]

theorem Phenomena.WordOrder.Typology.voAdposition_harmonic_dominant : voAdposition.harmonicDominant = true

Table 1: harmonic (926) > disharmonic (55).

theorem Phenomena.WordOrder.Typology.voSubordinator_harmonic_dominant : voSubordinator.harmonicDominant = true

Table 2: harmonic (393) > disharmonic (63).

theorem Phenomena.WordOrder.Typology.voRelativeClause_harmonic_dominant : voRelativeClause.harmonicDominant = true

Table 3: harmonic (547) > disharmonic (118).

theorem Phenomena.WordOrder.Typology.head_direction_generalization : allTables.all CrossTab.harmonicDominant = true

The head-direction generalization: across all three construction pairs, harmonic word-order pairings dominate.

This is the core empirical observation that @cite{gibson-2025} argues DLM explains: consistent head direction keeps recursive spine dependencies local.

theorem Phenomena.WordOrder.Typology.hihi_is_harmonic : voAdposition.hihi.isHarmonic = true

Harmonic cells have matching directions.

theorem Phenomena.WordOrder.Typology.hfhf_is_harmonic : voAdposition.hfhf.isHarmonic = true

theorem Phenomena.WordOrder.Typology.hihf_is_disharmonic : voAdposition.hihf.isHarmonic = false

Disharmonic cells have mismatched directions.

theorem Phenomena.WordOrder.Typology.hfhi_is_disharmonic : voAdposition.hfhi.isHarmonic = false

inductive Phenomena.WordOrder.Typology.SingleWordException : Type

Construction types where disharmonic order is common (Gibson Table 4).

These are cases where the dependent is typically a single word (no recursive subtree), so head direction doesn't affect DLM. Gibson's argument: DLM only cares about direction when subtrees intervene between head and dependent.

Data here is qualitative — WALS counts not provided in Gibson for these. Marked as data TBD for future WALS lookup.

• adjN : SingleWordException
• demN : SingleWordException
• intensAdj : SingleWordException
• negVerb : SingleWordException

def Phenomena.WordOrder.Typology.instReprSingleWordException.repr : SingleWordException → Nat → Std.Format

Equations

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

instance Phenomena.WordOrder.Typology.instReprSingleWordException : Repr SingleWordException

Equations

• Phenomena.WordOrder.Typology.instReprSingleWordException = { reprPrec := Phenomena.WordOrder.Typology.instReprSingleWordException.repr }

instance Phenomena.WordOrder.Typology.instDecidableEqSingleWordException : DecidableEq SingleWordException

Equations

• Phenomena.WordOrder.Typology.instDecidableEqSingleWordException x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.WordOrder.Typology.instBEqSingleWordException.beq : SingleWordException → SingleWordException → Bool

Equations

• Phenomena.WordOrder.Typology.instBEqSingleWordException.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.WordOrder.Typology.instBEqSingleWordException : BEq SingleWordException

Equations

• Phenomena.WordOrder.Typology.instBEqSingleWordException = { beq := Phenomena.WordOrder.Typology.instBEqSingleWordException.beq }

def Phenomena.WordOrder.Typology.singleWordExceptions : List SingleWordException

All single-word exceptions from Gibson Table 4.

Equations

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

def Phenomena.WordOrder.Typology.isSingleWordDependent : SingleWordException → Bool

These exceptions all involve dependents that are typically single words (leaves in the dependency tree), not recursive phrases.

Equations

• Phenomena.WordOrder.Typology.isSingleWordDependent Phenomena.WordOrder.Typology.SingleWordException.adjN = true
• Phenomena.WordOrder.Typology.isSingleWordDependent Phenomena.WordOrder.Typology.SingleWordException.demN = true
• Phenomena.WordOrder.Typology.isSingleWordDependent Phenomena.WordOrder.Typology.SingleWordException.intensAdj = true
• Phenomena.WordOrder.Typology.isSingleWordDependent Phenomena.WordOrder.Typology.SingleWordException.negVerb = true

theorem Phenomena.WordOrder.Typology.all_exceptions_single_word : singleWordExceptions.all isSingleWordDependent = true

theorem Phenomena.WordOrder.Typology.ch81_total : Core.WALS.F81A.allData.length = 1376

Ch 81 total: 1376 languages.

theorem Phenomena.WordOrder.Typology.ch82_total : Core.WALS.F82A.allData.length = 1496

Ch 82 total: 1496 languages.

theorem Phenomena.WordOrder.Typology.ch83_total : Core.WALS.F83A.allData.length = 1518

Ch 83 total: 1518 languages.

inductive Phenomena.WordOrder.Typology.BasicOrder : Type

WALS Ch 81: The six-way classification of basic constituent order.

The "basic" order is determined by the dominant order in pragmatically neutral, declarative clauses with full NP arguments. Languages where no single order clearly dominates (e.g., free word-order languages like Warlpiri, or V2 languages like German where underlying order is debated) are classified as "no dominant order."

Key finding: SOV and SVO together account for >76% of languages; object-initial orders (OVS + OSV) are vanishingly rare. This asymmetry is one of the most robust typological generalizations: subjects overwhelmingly precede objects.

• sov : BasicOrder
• svo : BasicOrder
• vso : BasicOrder
• vos : BasicOrder
• ovs : BasicOrder
• osv : BasicOrder
• noDominant : BasicOrder

instance Phenomena.WordOrder.Typology.instDecidableEqBasicOrder : DecidableEq BasicOrder

Equations

• Phenomena.WordOrder.Typology.instDecidableEqBasicOrder x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.WordOrder.Typology.instBEqBasicOrder : BEq BasicOrder

Equations

• Phenomena.WordOrder.Typology.instBEqBasicOrder = { beq := Phenomena.WordOrder.Typology.instBEqBasicOrder.beq }

def Phenomena.WordOrder.Typology.instBEqBasicOrder.beq : BasicOrder → BasicOrder → Bool

Equations

• Phenomena.WordOrder.Typology.instBEqBasicOrder.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.WordOrder.Typology.instReprBasicOrder.repr : BasicOrder → Nat → Std.Format

Equations

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

instance Phenomena.WordOrder.Typology.instReprBasicOrder : Repr BasicOrder

Equations

• Phenomena.WordOrder.Typology.instReprBasicOrder = { reprPrec := Phenomena.WordOrder.Typology.instReprBasicOrder.repr }

inductive Phenomena.WordOrder.Typology.SVOrder : Type

WALS Ch 82: Binary classification of S-V order.

• sv : SVOrder
• vs : SVOrder
• noDominant : SVOrder

instance Phenomena.WordOrder.Typology.instDecidableEqSVOrder : DecidableEq SVOrder

Equations

• Phenomena.WordOrder.Typology.instDecidableEqSVOrder x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.WordOrder.Typology.instBEqSVOrder : BEq SVOrder

Equations

• Phenomena.WordOrder.Typology.instBEqSVOrder = { beq := Phenomena.WordOrder.Typology.instBEqSVOrder.beq }

def Phenomena.WordOrder.Typology.instBEqSVOrder.beq : SVOrder → SVOrder → Bool

Equations

• Phenomena.WordOrder.Typology.instBEqSVOrder.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.WordOrder.Typology.instReprSVOrder.repr : SVOrder → Nat → Std.Format

Equations

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

instance Phenomena.WordOrder.Typology.instReprSVOrder : Repr SVOrder

Equations

• Phenomena.WordOrder.Typology.instReprSVOrder = { reprPrec := Phenomena.WordOrder.Typology.instReprSVOrder.repr }

inductive Phenomena.WordOrder.Typology.OVOrder : Type

WALS Ch 83: Binary classification of O-V order.

The most theoretically significant binary parameter: whether the object precedes the verb (OV = head-final VP) or follows it (VO = head-initial VP). This single parameter correlates with adposition order, genitive order, relative clause order, and subordinator order — the head-direction generalization formalized in the cross-tabulations above.

• ov : OVOrder
• vo : OVOrder
• noDominant : OVOrder

instance Phenomena.WordOrder.Typology.instDecidableEqOVOrder : DecidableEq OVOrder

Equations

• Phenomena.WordOrder.Typology.instDecidableEqOVOrder x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.WordOrder.Typology.instBEqOVOrder.beq : OVOrder → OVOrder → Bool

Equations

• Phenomena.WordOrder.Typology.instBEqOVOrder.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.WordOrder.Typology.instBEqOVOrder : BEq OVOrder

Equations

• Phenomena.WordOrder.Typology.instBEqOVOrder = { beq := Phenomena.WordOrder.Typology.instBEqOVOrder.beq }

def Phenomena.WordOrder.Typology.instReprOVOrder.repr : OVOrder → Nat → Std.Format

Equations

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

instance Phenomena.WordOrder.Typology.instReprOVOrder : Repr OVOrder

Equations

• Phenomena.WordOrder.Typology.instReprOVOrder = { reprPrec := Phenomena.WordOrder.Typology.instReprOVOrder.repr }

structure Phenomena.WordOrder.Typology.BasicOrderProfile : Type

A language's basic word-order profile across WALS Chapters 81--83.

Pairing a language's 6-way basic order (Ch 81) with its binary S-V (Ch 82) and O-V (Ch 83) classifications enables cross-chapter consistency checks: e.g., an SOV language should have SV order and OV order.

• language : String

  Language name.

• iso : String

  ISO 639-3 code.

• basicOrder : BasicOrder

  Ch 81: basic order of S, O, V.

• svOrder : SVOrder

  Ch 82: order of subject and verb.

• ovOrder : OVOrder

  Ch 83: order of object and verb.

• notes : String

  Notes on the word-order system.

instance Phenomena.WordOrder.Typology.instReprBasicOrderProfile : Repr BasicOrderProfile

Equations

• Phenomena.WordOrder.Typology.instReprBasicOrderProfile = { reprPrec := Phenomena.WordOrder.Typology.instReprBasicOrderProfile.repr }

def Phenomena.WordOrder.Typology.instReprBasicOrderProfile.repr : BasicOrderProfile → Nat → Std.Format

Equations

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

def Phenomena.WordOrder.Typology.japanese : BasicOrderProfile

Japanese: rigid SOV with postpositions, relative clause before noun, genitive before noun. The canonical head-final language.

Equations

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

def Phenomena.WordOrder.Typology.turkish : BasicOrderProfile

Turkish: SOV with postpositions. Relatively free word order for pragmatic effects, but SOV is strongly dominant.

Equations

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

def Phenomena.WordOrder.Typology.hindiUrdu : BasicOrderProfile

Hindi-Urdu: SOV with postpositions. Word order is relatively flexible due to case marking, but SOV is the default neutral order.

Equations

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

def Phenomena.WordOrder.Typology.korean : BasicOrderProfile

Korean: rigid SOV with postpositions, relative clause before noun. Very similar head-final profile to Japanese.

Equations

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

def Phenomena.WordOrder.Typology.quechua : BasicOrderProfile

Quechua (Southern): rigid SOV with postpositions, suffixal morphology. One of the most consistently head-final languages.

Equations

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

def Phenomena.WordOrder.Typology.basque : BasicOrderProfile

Basque: SOV with postpositions. Ergative-absolutive case system. Word order is flexible but SOV is the pragmatically neutral order.

Equations

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

def Phenomena.WordOrder.Typology.english : BasicOrderProfile

English: rigid SVO with prepositions and relative clause after noun. The canonical head-initial language (among non-V-initial types).

Equations

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

def Phenomena.WordOrder.Typology.mandarinChinese : BasicOrderProfile

Mandarin Chinese: SVO with prepositions (mostly). Some constructions are head-final (relative clause before noun, some postpositions), making Mandarin a mixed-headedness language.

Equations

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

def Phenomena.WordOrder.Typology.russian : BasicOrderProfile

Russian: SVO as the pragmatically neutral order, but word order is relatively free due to rich case morphology.

Equations

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

def Phenomena.WordOrder.Typology.swahili : BasicOrderProfile

Swahili: SVO with prepositions. Bantu language with rich verbal agreement that cross-references subject and object.

Equations

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

def Phenomena.WordOrder.Typology.indonesian : BasicOrderProfile

Indonesian: SVO with prepositions. Relatively rigid word order for an Austronesian language.

Equations

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

def Phenomena.WordOrder.Typology.arabicMSA : BasicOrderProfile

Arabic (Modern Standard): VSO as the classical/formal basic order, though SVO is increasingly common in spoken varieties.

Equations

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

def Phenomena.WordOrder.Typology.irish : BasicOrderProfile

Irish: VSO with prepositions, relative clause after noun. Celtic languages are the canonical European VSO family.

Equations

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

def Phenomena.WordOrder.Typology.tagalog : BasicOrderProfile

Tagalog: VSO / VOS (verb-initial with flexible S/O ordering). WALS classifies as VSO based on pragmatically neutral clauses. Philippine-type voice system complicates the S vs O distinction.

Equations

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

def Phenomena.WordOrder.Typology.welsh : BasicOrderProfile

Welsh: VSO with prepositions, relative clause after noun. Another Celtic VSO language.

Equations

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

def Phenomena.WordOrder.Typology.malagasy : BasicOrderProfile

Malagasy: VOS with prepositions. The best-known VOS language, extensively studied in formal syntax.

Equations

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

def Phenomena.WordOrder.Typology.tzotzil : BasicOrderProfile

Tzotzil (Mayan): VOS basic order, common in the Mayan family.

Equations

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

def Phenomena.WordOrder.Typology.hixkaryana : BasicOrderProfile

Hixkaryana (Cariban; Brazil): the first language for which OVS basic order was convincingly demonstrated. This discovery refuted the earlier claim that OVS and OSV orders were unattested.

Equations

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

def Phenomena.WordOrder.Typology.germanV2 : BasicOrderProfile

German: V2 in main clauses, SOV in embedded clauses. WALS classifies as SVO, but many syntacticians analyze the underlying order as SOV with V2 movement. The tension makes "no dominant order" defensible (though WALS itself codes German as SVO).

Equations

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

def Phenomena.WordOrder.Typology.warlpiri : BasicOrderProfile

Warlpiri (Pama-Nyungan; Australia): radically free word order, with all six permutations of S, O, V attested in natural discourse. The canonical non-configurational language.

Equations

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

def Phenomena.WordOrder.Typology.basicOrderProfiles : List BasicOrderProfile

All basic-order language profiles in the sample.

Equations

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

def Phenomena.WordOrder.Typology.countByBasicOrder (langs : List BasicOrderProfile) (o : BasicOrder) : Nat

Count of languages in a profile list with a given basic order.

Equations

• Phenomena.WordOrder.Typology.countByBasicOrder langs o = (List.filter (fun (x : Phenomena.WordOrder.Typology.BasicOrderProfile) => x.basicOrder == o) langs).length

def Phenomena.WordOrder.Typology.countBySVOrder (langs : List BasicOrderProfile) (o : SVOrder) : Nat

Count of languages in a profile list with a given S-V order.

Equations

• Phenomena.WordOrder.Typology.countBySVOrder langs o = (List.filter (fun (x : Phenomena.WordOrder.Typology.BasicOrderProfile) => x.svOrder == o) langs).length

def Phenomena.WordOrder.Typology.countByOVOrder (langs : List BasicOrderProfile) (o : OVOrder) : Nat

Count of languages in a profile list with a given O-V order.

Equations

• Phenomena.WordOrder.Typology.countByOVOrder langs o = (List.filter (fun (x : Phenomena.WordOrder.Typology.BasicOrderProfile) => x.ovOrder == o) langs).length

theorem Phenomena.WordOrder.Typology.sov_most_common : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => x.value == Core.WALS.F81A.BasicWordOrder.sov) Phenomena.WordOrder.Typology.ch81✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => x.value == Core.WALS.F81A.BasicWordOrder.svo) Phenomena.WordOrder.Typology.ch81✝¹).length

Generalization 1: SOV is the most common basic order.

theorem Phenomena.WordOrder.Typology.sov_svo_majority_overall : have sov := (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => x.value == Core.WALS.F81A.BasicWordOrder.sov) Phenomena.WordOrder.Typology.ch81✝).length; have svo := (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => x.value == Core.WALS.F81A.BasicWordOrder.svo) Phenomena.WordOrder.Typology.ch81✝¹).length; (sov + svo) * 4 > Phenomena.WordOrder.Typology.ch81✝².length * 3

Generalization 2: SOV + SVO together exceed 75% of all sampled languages.

theorem Phenomena.WordOrder.Typology.ov_dominant_ch83 : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F83A.ObjectVerbOrder) => x.value == Core.WALS.F83A.ObjectVerbOrder.ov) Phenomena.WordOrder.Typology.ch83✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F83A.ObjectVerbOrder) => x.value == Core.WALS.F83A.ObjectVerbOrder.vo) Phenomena.WordOrder.Typology.ch83✝¹).length

Generalization 3: In Ch 83, OV slightly outnumbers VO.

theorem Phenomena.WordOrder.Typology.subject_first_dominant : have sf := (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => x.value == Core.WALS.F81A.BasicWordOrder.sov) Phenomena.WordOrder.Typology.ch81✝).length + (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => x.value == Core.WALS.F81A.BasicWordOrder.svo) Phenomena.WordOrder.Typology.ch81✝¹).length; have vf := (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => x.value == Core.WALS.F81A.BasicWordOrder.vso) Phenomena.WordOrder.Typology.ch81✝²).length + (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => x.value == Core.WALS.F81A.BasicWordOrder.vos) Phenomena.WordOrder.Typology.ch81✝³).length; sf > vf * 8

Generalization 4: Subject-first orders (SOV + SVO) far outnumber verb-first orders (VSO + VOS).

theorem Phenomena.WordOrder.Typology.object_initial_rare : have oi := (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => x.value == Core.WALS.F81A.BasicWordOrder.ovs) Phenomena.WordOrder.Typology.ch81✝).length + (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => x.value == Core.WALS.F81A.BasicWordOrder.osv) Phenomena.WordOrder.Typology.ch81✝¹).length; oi * 100 < Phenomena.WordOrder.Typology.ch81✝².length * 2

Generalization 5: Object-initial orders (OVS + OSV) are extremely rare — less than 2% of the sample.

theorem Phenomena.WordOrder.Typology.greenberg_universal_1 : have subj_before_obj := (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => x.value == Core.WALS.F81A.BasicWordOrder.sov) Phenomena.WordOrder.Typology.ch81✝).length + (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => x.value == Core.WALS.F81A.BasicWordOrder.svo) Phenomena.WordOrder.Typology.ch81✝¹).length + (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => x.value == Core.WALS.F81A.BasicWordOrder.vso) Phenomena.WordOrder.Typology.ch81✝²).length; have obj_before_subj := (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => x.value == Core.WALS.F81A.BasicWordOrder.vos) Phenomena.WordOrder.Typology.ch81✝³).length + (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => x.value == Core.WALS.F81A.BasicWordOrder.ovs) Phenomena.WordOrder.Typology.ch81✝⁴).length + (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => x.value == Core.WALS.F81A.BasicWordOrder.osv) Phenomena.WordOrder.Typology.ch81✝⁵).length; subj_before_obj > obj_before_subj * 28

Generalization 6 (Greenberg's Universal 1): In declarative sentences with nominal subject and object, the subject almost always precedes the object. SOV + SVO + VSO (subject before object) vastly outnumber VOS + OVS + OSV (object before subject).

theorem Phenomena.WordOrder.Typology.sv_dominant : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F82A.SubjectVerbOrder) => x.value == Core.WALS.F82A.SubjectVerbOrder.sv) Phenomena.WordOrder.Typology.ch82✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F82A.SubjectVerbOrder) => x.value == Core.WALS.F82A.SubjectVerbOrder.vs) Phenomena.WordOrder.Typology.ch82✝¹).length * 5

Generalization 7: SV overwhelmingly dominates VS in Ch 82. SV languages outnumber VS languages by more than 5 to 1.

theorem Phenomena.WordOrder.Typology.sov_implies_sv_and_ov : have sovLangs := List.filter (fun (x : BasicOrderProfile) => x.basicOrder == BasicOrder.sov) basicOrderProfiles; (sovLangs.all fun (p : BasicOrderProfile) => p.svOrder == SVOrder.sv && p.ovOrder == OVOrder.ov) = true

Generalization 8: Cross-chapter consistency — all SOV languages in our sample have OV order (Ch 83) and SV order (Ch 82).

theorem Phenomena.WordOrder.Typology.svo_implies_sv_and_vo : have svoLangs := List.filter (fun (x : BasicOrderProfile) => x.basicOrder == BasicOrder.svo) basicOrderProfiles; (svoLangs.all fun (p : BasicOrderProfile) => p.svOrder == SVOrder.sv && p.ovOrder == OVOrder.vo) = true

Cross-chapter consistency — all SVO languages in our sample have SV order (Ch 82) and VO order (Ch 83).

theorem Phenomena.WordOrder.Typology.vso_implies_vs_and_vo : have vsoLangs := List.filter (fun (x : BasicOrderProfile) => x.basicOrder == BasicOrder.vso) basicOrderProfiles; (vsoLangs.all fun (p : BasicOrderProfile) => p.svOrder == SVOrder.vs && p.ovOrder == OVOrder.vo) = true

Cross-chapter consistency — all VSO languages in our sample have VS order (Ch 82) and VO order (Ch 83).

theorem Phenomena.WordOrder.Typology.vos_implies_vs_and_vo : have vosLangs := List.filter (fun (x : BasicOrderProfile) => x.basicOrder == BasicOrder.vos) basicOrderProfiles; (vosLangs.all fun (p : BasicOrderProfile) => p.svOrder == SVOrder.vs && p.ovOrder == OVOrder.vo) = true

Cross-chapter consistency — all VOS languages in our sample have VS order (Ch 82) and VO order (Ch 83).

theorem Phenomena.WordOrder.Typology.ov_languages_are_sov_or_ovs : have ovLangs := List.filter (fun (x : BasicOrderProfile) => x.ovOrder == OVOrder.ov) basicOrderProfiles; (ovLangs.all fun (p : BasicOrderProfile) => p.basicOrder == BasicOrder.sov || p.basicOrder == BasicOrder.ovs) = true

Generalization 9: All OV languages in our sample have basic order SOV or OVS (the two S-containing OV orders).

theorem Phenomena.WordOrder.Typology.vo_languages_are_svo_vso_or_vos : have voLangs := List.filter (fun (x : BasicOrderProfile) => x.ovOrder == OVOrder.vo) basicOrderProfiles; (voLangs.all fun (p : BasicOrderProfile) => p.basicOrder == BasicOrder.svo || p.basicOrder == BasicOrder.vso || p.basicOrder == BasicOrder.vos) = true

All VO languages in our sample have basic order SVO, VSO, or VOS.

theorem Phenomena.WordOrder.Typology.japanese_is_sov : (japanese.basicOrder == BasicOrder.sov) = true

theorem Phenomena.WordOrder.Typology.turkish_is_sov : (turkish.basicOrder == BasicOrder.sov) = true

theorem Phenomena.WordOrder.Typology.hindiUrdu_is_sov : (hindiUrdu.basicOrder == BasicOrder.sov) = true

theorem Phenomena.WordOrder.Typology.korean_is_sov : (korean.basicOrder == BasicOrder.sov) = true

theorem Phenomena.WordOrder.Typology.quechua_is_sov : (quechua.basicOrder == BasicOrder.sov) = true

theorem Phenomena.WordOrder.Typology.basque_is_sov : (basque.basicOrder == BasicOrder.sov) = true

theorem Phenomena.WordOrder.Typology.english_is_svo : (english.basicOrder == BasicOrder.svo) = true

theorem Phenomena.WordOrder.Typology.mandarin_is_svo : (mandarinChinese.basicOrder == BasicOrder.svo) = true

theorem Phenomena.WordOrder.Typology.russian_is_svo : (russian.basicOrder == BasicOrder.svo) = true

theorem Phenomena.WordOrder.Typology.swahili_is_svo : (swahili.basicOrder == BasicOrder.svo) = true

theorem Phenomena.WordOrder.Typology.indonesian_is_svo : (indonesian.basicOrder == BasicOrder.svo) = true

theorem Phenomena.WordOrder.Typology.arabic_is_vso : (arabicMSA.basicOrder == BasicOrder.vso) = true

theorem Phenomena.WordOrder.Typology.irish_is_vso : (irish.basicOrder == BasicOrder.vso) = true

theorem Phenomena.WordOrder.Typology.tagalog_is_vso : (tagalog.basicOrder == BasicOrder.vso) = true

theorem Phenomena.WordOrder.Typology.welsh_is_vso : (welsh.basicOrder == BasicOrder.vso) = true

theorem Phenomena.WordOrder.Typology.malagasy_is_vos : (malagasy.basicOrder == BasicOrder.vos) = true

theorem Phenomena.WordOrder.Typology.tzotzil_is_vos : (tzotzil.basicOrder == BasicOrder.vos) = true

theorem Phenomena.WordOrder.Typology.hixkaryana_is_ovs : (hixkaryana.basicOrder == BasicOrder.ovs) = true

theorem Phenomena.WordOrder.Typology.germanV2_no_dominant : (germanV2.basicOrder == BasicOrder.noDominant) = true

theorem Phenomena.WordOrder.Typology.warlpiri_no_dominant : (warlpiri.basicOrder == BasicOrder.noDominant) = true

theorem Phenomena.WordOrder.Typology.basic_order_sample_size : basicOrderProfiles.length = 20

Number of languages in our basic-order profile sample.

theorem Phenomena.WordOrder.Typology.sample_sov_count : countByBasicOrder basicOrderProfiles BasicOrder.sov = 6

Distribution of basic orders in our sample.

theorem Phenomena.WordOrder.Typology.sample_svo_count : countByBasicOrder basicOrderProfiles BasicOrder.svo = 5

theorem Phenomena.WordOrder.Typology.sample_vso_count : countByBasicOrder basicOrderProfiles BasicOrder.vso = 4

theorem Phenomena.WordOrder.Typology.sample_vos_count : countByBasicOrder basicOrderProfiles BasicOrder.vos = 2

theorem Phenomena.WordOrder.Typology.sample_ovs_count : countByBasicOrder basicOrderProfiles BasicOrder.ovs = 1

theorem Phenomena.WordOrder.Typology.sample_osv_count : countByBasicOrder basicOrderProfiles BasicOrder.osv = 0

theorem Phenomena.WordOrder.Typology.sample_noDom_count : countByBasicOrder basicOrderProfiles BasicOrder.noDominant = 2

theorem Phenomena.WordOrder.Typology.japanese_order_wals : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => Phenomena.WordOrder.Typology.fromWALS81A✝ x.value) (Core.WALS.F81A.lookup "jpn") = some japanese.basicOrder

For each profile whose language is in WALS Ch 81A, prove its basic order matches the WALS data. Languages not in the WALS sample (Malagasy, Quechua) are excluded — their profiles are ungrounded assertions.

theorem Phenomena.WordOrder.Typology.turkish_order_wals : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => Phenomena.WordOrder.Typology.fromWALS81A✝ x.value) (Core.WALS.F81A.lookup "tur") = some turkish.basicOrder

theorem Phenomena.WordOrder.Typology.hindiUrdu_order_wals : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => Phenomena.WordOrder.Typology.fromWALS81A✝ x.value) (Core.WALS.F81A.lookup "hin") = some hindiUrdu.basicOrder

theorem Phenomena.WordOrder.Typology.korean_order_wals : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => Phenomena.WordOrder.Typology.fromWALS81A✝ x.value) (Core.WALS.F81A.lookup "kor") = some korean.basicOrder

theorem Phenomena.WordOrder.Typology.basque_order_wals : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => Phenomena.WordOrder.Typology.fromWALS81A✝ x.value) (Core.WALS.F81A.lookup "bsq") = some basque.basicOrder

theorem Phenomena.WordOrder.Typology.english_order_wals : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => Phenomena.WordOrder.Typology.fromWALS81A✝ x.value) (Core.WALS.F81A.lookup "eng") = some english.basicOrder

theorem Phenomena.WordOrder.Typology.mandarin_order_wals : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => Phenomena.WordOrder.Typology.fromWALS81A✝ x.value) (Core.WALS.F81A.lookup "mnd") = some mandarinChinese.basicOrder

theorem Phenomena.WordOrder.Typology.russian_order_wals : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => Phenomena.WordOrder.Typology.fromWALS81A✝ x.value) (Core.WALS.F81A.lookup "rus") = some russian.basicOrder

theorem Phenomena.WordOrder.Typology.swahili_order_wals : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => Phenomena.WordOrder.Typology.fromWALS81A✝ x.value) (Core.WALS.F81A.lookup "swa") = some swahili.basicOrder

theorem Phenomena.WordOrder.Typology.indonesian_order_wals : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => Phenomena.WordOrder.Typology.fromWALS81A✝ x.value) (Core.WALS.F81A.lookup "ind") = some indonesian.basicOrder

theorem Phenomena.WordOrder.Typology.arabic_order_wals : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => Phenomena.WordOrder.Typology.fromWALS81A✝ x.value) (Core.WALS.F81A.lookup "ams") = some arabicMSA.basicOrder

theorem Phenomena.WordOrder.Typology.irish_order_wals : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => Phenomena.WordOrder.Typology.fromWALS81A✝ x.value) (Core.WALS.F81A.lookup "iri") = some irish.basicOrder

theorem Phenomena.WordOrder.Typology.tagalog_order_wals : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => Phenomena.WordOrder.Typology.fromWALS81A✝ x.value) (Core.WALS.F81A.lookup "tag") = some tagalog.basicOrder

theorem Phenomena.WordOrder.Typology.welsh_order_wals : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => Phenomena.WordOrder.Typology.fromWALS81A✝ x.value) (Core.WALS.F81A.lookup "wec") = some welsh.basicOrder

theorem Phenomena.WordOrder.Typology.tzotzil_order_wals : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => Phenomena.WordOrder.Typology.fromWALS81A✝ x.value) (Core.WALS.F81A.lookup "tzo") = some tzotzil.basicOrder

theorem Phenomena.WordOrder.Typology.hixkaryana_order_wals : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => Phenomena.WordOrder.Typology.fromWALS81A✝ x.value) (Core.WALS.F81A.lookup "hix") = some hixkaryana.basicOrder

theorem Phenomena.WordOrder.Typology.german_order_wals : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => Phenomena.WordOrder.Typology.fromWALS81A✝ x.value) (Core.WALS.F81A.lookup "ger") = some germanV2.basicOrder

theorem Phenomena.WordOrder.Typology.warlpiri_order_wals : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F81A.BasicWordOrder) => Phenomena.WordOrder.Typology.fromWALS81A✝ x.value) (Core.WALS.F81A.lookup "wrl") = some warlpiri.basicOrder

theorem Phenomena.WordOrder.Typology.japanese_sv_wals : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F82A.SubjectVerbOrder) => Phenomena.WordOrder.Typology.fromWALS82A✝ x.value) (Core.WALS.F82A.lookup "jpn") = some japanese.svOrder

theorem Phenomena.WordOrder.Typology.english_sv_wals : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F82A.SubjectVerbOrder) => Phenomena.WordOrder.Typology.fromWALS82A✝ x.value) (Core.WALS.F82A.lookup "eng") = some english.svOrder

theorem Phenomena.WordOrder.Typology.arabic_sv_wals : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F82A.SubjectVerbOrder) => Phenomena.WordOrder.Typology.fromWALS82A✝ x.value) (Core.WALS.F82A.lookup "ams") = some arabicMSA.svOrder

theorem Phenomena.WordOrder.Typology.hixkaryana_sv_wals : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F82A.SubjectVerbOrder) => Phenomena.WordOrder.Typology.fromWALS82A✝ x.value) (Core.WALS.F82A.lookup "hix") = some hixkaryana.svOrder

theorem Phenomena.WordOrder.Typology.warlpiri_sv_wals : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F82A.SubjectVerbOrder) => Phenomena.WordOrder.Typology.fromWALS82A✝ x.value) (Core.WALS.F82A.lookup "wrl") = some warlpiri.svOrder

theorem Phenomena.WordOrder.Typology.japanese_ov_wals : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F83A.ObjectVerbOrder) => Phenomena.WordOrder.Typology.fromWALS83A✝ x.value) (Core.WALS.F83A.lookup "jpn") = some japanese.ovOrder

theorem Phenomena.WordOrder.Typology.english_ov_wals : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F83A.ObjectVerbOrder) => Phenomena.WordOrder.Typology.fromWALS83A✝ x.value) (Core.WALS.F83A.lookup "eng") = some english.ovOrder

theorem Phenomena.WordOrder.Typology.german_ov_wals : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F83A.ObjectVerbOrder) => Phenomena.WordOrder.Typology.fromWALS83A✝ x.value) (Core.WALS.F83A.lookup "ger") = some germanV2.ovOrder

theorem Phenomena.WordOrder.Typology.warlpiri_ov_wals : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F83A.ObjectVerbOrder) => Phenomena.WordOrder.Typology.fromWALS83A✝ x.value) (Core.WALS.F83A.lookup "wrl") = some warlpiri.ovOrder

theorem Phenomena.WordOrder.Typology.ch84_total : Phenomena.WordOrder.Typology.ch84✝.length = 500

Ch 84 total: 500 languages.

theorem Phenomena.WordOrder.Typology.ch84_count_vox : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F84A.ObjectObliqueVerbOrder) => x.value == Core.WALS.F84A.ObjectObliqueVerbOrder.vox) Phenomena.WordOrder.Typology.ch84✝).length = 210

theorem Phenomena.WordOrder.Typology.ch84_count_xov : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F84A.ObjectObliqueVerbOrder) => x.value == Core.WALS.F84A.ObjectObliqueVerbOrder.xov) Phenomena.WordOrder.Typology.ch84✝).length = 48

theorem Phenomena.WordOrder.Typology.ch84_count_ovx : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F84A.ObjectObliqueVerbOrder) => x.value == Core.WALS.F84A.ObjectObliqueVerbOrder.ovx) Phenomena.WordOrder.Typology.ch84✝).length = 45

theorem Phenomena.WordOrder.Typology.ch84_count_oxv : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F84A.ObjectObliqueVerbOrder) => x.value == Core.WALS.F84A.ObjectObliqueVerbOrder.oxv) Phenomena.WordOrder.Typology.ch84✝).length = 27

theorem Phenomena.WordOrder.Typology.ch84_count_xvo : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F84A.ObjectObliqueVerbOrder) => x.value == Core.WALS.F84A.ObjectObliqueVerbOrder.xvo) Phenomena.WordOrder.Typology.ch84✝).length = 3

theorem Phenomena.WordOrder.Typology.ch84_count_noDominantOrder : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F84A.ObjectObliqueVerbOrder) => x.value == Core.WALS.F84A.ObjectObliqueVerbOrder.noDominantOrder) Phenomena.WordOrder.Typology.ch84✝).length = 167

theorem Phenomena.WordOrder.Typology.english_ch84 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F84A.ObjectObliqueVerbOrder) => x.value) (Core.WALS.F84A.lookup "eng") = some Core.WALS.F84A.ObjectObliqueVerbOrder.vox

theorem Phenomena.WordOrder.Typology.japanese_ch84 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F84A.ObjectObliqueVerbOrder) => x.value) (Core.WALS.F84A.lookup "jpn") = some Core.WALS.F84A.ObjectObliqueVerbOrder.xov

theorem Phenomena.WordOrder.Typology.turkish_ch84 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F84A.ObjectObliqueVerbOrder) => x.value) (Core.WALS.F84A.lookup "tur") = some Core.WALS.F84A.ObjectObliqueVerbOrder.xov

theorem Phenomena.WordOrder.Typology.basque_ch84 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F84A.ObjectObliqueVerbOrder) => x.value) (Core.WALS.F84A.lookup "bsq") = some Core.WALS.F84A.ObjectObliqueVerbOrder.xov

theorem Phenomena.WordOrder.Typology.mandarin_ch84 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F84A.ObjectObliqueVerbOrder) => x.value) (Core.WALS.F84A.lookup "mnd") = some Core.WALS.F84A.ObjectObliqueVerbOrder.xvo

theorem Phenomena.WordOrder.Typology.arabic_ch84 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F84A.ObjectObliqueVerbOrder) => x.value) (Core.WALS.F84A.lookup "ams") = some Core.WALS.F84A.ObjectObliqueVerbOrder.vox

theorem Phenomena.WordOrder.Typology.irish_ch84 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F84A.ObjectObliqueVerbOrder) => x.value) (Core.WALS.F84A.lookup "iri") = some Core.WALS.F84A.ObjectObliqueVerbOrder.vox

theorem Phenomena.WordOrder.Typology.indonesian_ch84 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F84A.ObjectObliqueVerbOrder) => x.value) (Core.WALS.F84A.lookup "ind") = some Core.WALS.F84A.ObjectObliqueVerbOrder.vox

theorem Phenomena.WordOrder.Typology.malagasy_ch84 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F84A.ObjectObliqueVerbOrder) => x.value) (Core.WALS.F84A.lookup "mal") = some Core.WALS.F84A.ObjectObliqueVerbOrder.vox

theorem Phenomena.WordOrder.Typology.tzotzil_ch84 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F84A.ObjectObliqueVerbOrder) => x.value) (Core.WALS.F84A.lookup "tzo") = some Core.WALS.F84A.ObjectObliqueVerbOrder.vox

theorem Phenomena.WordOrder.Typology.hixkaryana_ch84 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F84A.ObjectObliqueVerbOrder) => x.value) (Core.WALS.F84A.lookup "hix") = some Core.WALS.F84A.ObjectObliqueVerbOrder.ovx

theorem Phenomena.WordOrder.Typology.german_ch84 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F84A.ObjectObliqueVerbOrder) => x.value) (Core.WALS.F84A.lookup "ger") = some Core.WALS.F84A.ObjectObliqueVerbOrder.noDominantOrder

theorem Phenomena.WordOrder.Typology.welsh_ch84 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F84A.ObjectObliqueVerbOrder) => x.value) (Core.WALS.F84A.lookup "wel") = some Core.WALS.F84A.ObjectObliqueVerbOrder.vox

theorem Phenomena.WordOrder.Typology.warlpiri_ch84 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F84A.ObjectObliqueVerbOrder) => x.value) (Core.WALS.F84A.lookup "wrl") = some Core.WALS.F84A.ObjectObliqueVerbOrder.noDominantOrder

theorem Phenomena.WordOrder.Typology.ch85_total : Phenomena.WordOrder.Typology.ch85✝.length = 1184

Ch 85 total: 1184 languages.

theorem Phenomena.WordOrder.Typology.ch85_count_postpositions : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F85A.AdpositionNPOrder) => x.value == Core.WALS.F85A.AdpositionNPOrder.postpositions) Phenomena.WordOrder.Typology.ch85✝).length = 577

theorem Phenomena.WordOrder.Typology.ch85_count_prepositions : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F85A.AdpositionNPOrder) => x.value == Core.WALS.F85A.AdpositionNPOrder.prepositions) Phenomena.WordOrder.Typology.ch85✝).length = 511

theorem Phenomena.WordOrder.Typology.ch85_count_inpositions : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F85A.AdpositionNPOrder) => x.value == Core.WALS.F85A.AdpositionNPOrder.inpositions) Phenomena.WordOrder.Typology.ch85✝).length = 8

theorem Phenomena.WordOrder.Typology.ch85_count_noDominantOrder : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F85A.AdpositionNPOrder) => x.value == Core.WALS.F85A.AdpositionNPOrder.noDominantOrder) Phenomena.WordOrder.Typology.ch85✝).length = 58

theorem Phenomena.WordOrder.Typology.ch85_count_noAdpositions : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F85A.AdpositionNPOrder) => x.value == Core.WALS.F85A.AdpositionNPOrder.noAdpositions) Phenomena.WordOrder.Typology.ch85✝).length = 30

theorem Phenomena.WordOrder.Typology.english_ch85 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F85A.AdpositionNPOrder) => x.value) (Core.WALS.F85A.lookup "eng") = some Core.WALS.F85A.AdpositionNPOrder.prepositions

theorem Phenomena.WordOrder.Typology.japanese_ch85 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F85A.AdpositionNPOrder) => x.value) (Core.WALS.F85A.lookup "jpn") = some Core.WALS.F85A.AdpositionNPOrder.postpositions

theorem Phenomena.WordOrder.Typology.turkish_ch85 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F85A.AdpositionNPOrder) => x.value) (Core.WALS.F85A.lookup "tur") = some Core.WALS.F85A.AdpositionNPOrder.postpositions

theorem Phenomena.WordOrder.Typology.hindiUrdu_ch85 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F85A.AdpositionNPOrder) => x.value) (Core.WALS.F85A.lookup "hin") = some Core.WALS.F85A.AdpositionNPOrder.postpositions

theorem Phenomena.WordOrder.Typology.korean_ch85 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F85A.AdpositionNPOrder) => x.value) (Core.WALS.F85A.lookup "kor") = some Core.WALS.F85A.AdpositionNPOrder.postpositions

theorem Phenomena.WordOrder.Typology.basque_ch85 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F85A.AdpositionNPOrder) => x.value) (Core.WALS.F85A.lookup "bsq") = some Core.WALS.F85A.AdpositionNPOrder.postpositions

theorem Phenomena.WordOrder.Typology.mandarin_ch85 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F85A.AdpositionNPOrder) => x.value) (Core.WALS.F85A.lookup "mnd") = some Core.WALS.F85A.AdpositionNPOrder.noDominantOrder

theorem Phenomena.WordOrder.Typology.russian_ch85 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F85A.AdpositionNPOrder) => x.value) (Core.WALS.F85A.lookup "rus") = some Core.WALS.F85A.AdpositionNPOrder.prepositions

theorem Phenomena.WordOrder.Typology.swahili_ch85 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F85A.AdpositionNPOrder) => x.value) (Core.WALS.F85A.lookup "swa") = some Core.WALS.F85A.AdpositionNPOrder.prepositions

theorem Phenomena.WordOrder.Typology.indonesian_ch85 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F85A.AdpositionNPOrder) => x.value) (Core.WALS.F85A.lookup "ind") = some Core.WALS.F85A.AdpositionNPOrder.prepositions

theorem Phenomena.WordOrder.Typology.arabic_ch85 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F85A.AdpositionNPOrder) => x.value) (Core.WALS.F85A.lookup "ams") = some Core.WALS.F85A.AdpositionNPOrder.prepositions

theorem Phenomena.WordOrder.Typology.irish_ch85 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F85A.AdpositionNPOrder) => x.value) (Core.WALS.F85A.lookup "iri") = some Core.WALS.F85A.AdpositionNPOrder.prepositions

theorem Phenomena.WordOrder.Typology.malagasy_ch85 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F85A.AdpositionNPOrder) => x.value) (Core.WALS.F85A.lookup "mal") = some Core.WALS.F85A.AdpositionNPOrder.prepositions

theorem Phenomena.WordOrder.Typology.tzotzil_ch85 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F85A.AdpositionNPOrder) => x.value) (Core.WALS.F85A.lookup "tzo") = some Core.WALS.F85A.AdpositionNPOrder.prepositions

theorem Phenomena.WordOrder.Typology.hixkaryana_ch85 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F85A.AdpositionNPOrder) => x.value) (Core.WALS.F85A.lookup "hix") = some Core.WALS.F85A.AdpositionNPOrder.postpositions

theorem Phenomena.WordOrder.Typology.welsh_ch85 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F85A.AdpositionNPOrder) => x.value) (Core.WALS.F85A.lookup "wel") = some Core.WALS.F85A.AdpositionNPOrder.prepositions

theorem Phenomena.WordOrder.Typology.german_ch85 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F85A.AdpositionNPOrder) => x.value) (Core.WALS.F85A.lookup "ger") = some Core.WALS.F85A.AdpositionNPOrder.prepositions

theorem Phenomena.WordOrder.Typology.ch86_total : Phenomena.WordOrder.Typology.ch86✝.length = 1249

Ch 86 total: 1249 languages.

theorem Phenomena.WordOrder.Typology.ch86_count_genitiveNoun : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F86A.GenitiveNounOrder) => x.value == Core.WALS.F86A.GenitiveNounOrder.genitiveNoun) Phenomena.WordOrder.Typology.ch86✝).length = 685

theorem Phenomena.WordOrder.Typology.ch86_count_nounGenitive : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F86A.GenitiveNounOrder) => x.value == Core.WALS.F86A.GenitiveNounOrder.nounGenitive) Phenomena.WordOrder.Typology.ch86✝).length = 468

theorem Phenomena.WordOrder.Typology.ch86_count_noDominantOrder : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F86A.GenitiveNounOrder) => x.value == Core.WALS.F86A.GenitiveNounOrder.noDominantOrder) Phenomena.WordOrder.Typology.ch86✝).length = 96

theorem Phenomena.WordOrder.Typology.japanese_ch86 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F86A.GenitiveNounOrder) => x.value) (Core.WALS.F86A.lookup "jpn") = some Core.WALS.F86A.GenitiveNounOrder.genitiveNoun

theorem Phenomena.WordOrder.Typology.turkish_ch86 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F86A.GenitiveNounOrder) => x.value) (Core.WALS.F86A.lookup "tur") = some Core.WALS.F86A.GenitiveNounOrder.genitiveNoun

theorem Phenomena.WordOrder.Typology.hindiUrdu_ch86 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F86A.GenitiveNounOrder) => x.value) (Core.WALS.F86A.lookup "hin") = some Core.WALS.F86A.GenitiveNounOrder.genitiveNoun

theorem Phenomena.WordOrder.Typology.korean_ch86 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F86A.GenitiveNounOrder) => x.value) (Core.WALS.F86A.lookup "kor") = some Core.WALS.F86A.GenitiveNounOrder.genitiveNoun

theorem Phenomena.WordOrder.Typology.basque_ch86 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F86A.GenitiveNounOrder) => x.value) (Core.WALS.F86A.lookup "bsq") = some Core.WALS.F86A.GenitiveNounOrder.genitiveNoun

theorem Phenomena.WordOrder.Typology.english_ch86 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F86A.GenitiveNounOrder) => x.value) (Core.WALS.F86A.lookup "eng") = some Core.WALS.F86A.GenitiveNounOrder.noDominantOrder

theorem Phenomena.WordOrder.Typology.mandarin_ch86 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F86A.GenitiveNounOrder) => x.value) (Core.WALS.F86A.lookup "mnd") = some Core.WALS.F86A.GenitiveNounOrder.genitiveNoun

theorem Phenomena.WordOrder.Typology.russian_ch86 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F86A.GenitiveNounOrder) => x.value) (Core.WALS.F86A.lookup "rus") = some Core.WALS.F86A.GenitiveNounOrder.nounGenitive

theorem Phenomena.WordOrder.Typology.swahili_ch86 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F86A.GenitiveNounOrder) => x.value) (Core.WALS.F86A.lookup "swa") = some Core.WALS.F86A.GenitiveNounOrder.nounGenitive

theorem Phenomena.WordOrder.Typology.indonesian_ch86 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F86A.GenitiveNounOrder) => x.value) (Core.WALS.F86A.lookup "ind") = some Core.WALS.F86A.GenitiveNounOrder.nounGenitive

theorem Phenomena.WordOrder.Typology.arabic_ch86 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F86A.GenitiveNounOrder) => x.value) (Core.WALS.F86A.lookup "ams") = some Core.WALS.F86A.GenitiveNounOrder.nounGenitive

theorem Phenomena.WordOrder.Typology.irish_ch86 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F86A.GenitiveNounOrder) => x.value) (Core.WALS.F86A.lookup "iri") = some Core.WALS.F86A.GenitiveNounOrder.nounGenitive

theorem Phenomena.WordOrder.Typology.tagalog_ch86 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F86A.GenitiveNounOrder) => x.value) (Core.WALS.F86A.lookup "tag") = some Core.WALS.F86A.GenitiveNounOrder.nounGenitive

theorem Phenomena.WordOrder.Typology.malagasy_ch86 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F86A.GenitiveNounOrder) => x.value) (Core.WALS.F86A.lookup "mal") = some Core.WALS.F86A.GenitiveNounOrder.nounGenitive

theorem Phenomena.WordOrder.Typology.tzotzil_ch86 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F86A.GenitiveNounOrder) => x.value) (Core.WALS.F86A.lookup "tzo") = some Core.WALS.F86A.GenitiveNounOrder.nounGenitive

theorem Phenomena.WordOrder.Typology.hixkaryana_ch86 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F86A.GenitiveNounOrder) => x.value) (Core.WALS.F86A.lookup "hix") = some Core.WALS.F86A.GenitiveNounOrder.genitiveNoun

theorem Phenomena.WordOrder.Typology.welsh_ch86 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F86A.GenitiveNounOrder) => x.value) (Core.WALS.F86A.lookup "wel") = some Core.WALS.F86A.GenitiveNounOrder.nounGenitive

theorem Phenomena.WordOrder.Typology.german_ch86 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F86A.GenitiveNounOrder) => x.value) (Core.WALS.F86A.lookup "ger") = some Core.WALS.F86A.GenitiveNounOrder.nounGenitive

theorem Phenomena.WordOrder.Typology.ch87_total : Phenomena.WordOrder.Typology.ch87✝.length = 1367

Ch 87 total: 1367 languages.

theorem Phenomena.WordOrder.Typology.ch87_count_adjectiveNoun : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F87A.AdjectiveNounOrder) => x.value == Core.WALS.F87A.AdjectiveNounOrder.adjectiveNoun) Phenomena.WordOrder.Typology.ch87✝).length = 373

theorem Phenomena.WordOrder.Typology.ch87_count_nounAdjective : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F87A.AdjectiveNounOrder) => x.value == Core.WALS.F87A.AdjectiveNounOrder.nounAdjective) Phenomena.WordOrder.Typology.ch87✝).length = 879

theorem Phenomena.WordOrder.Typology.ch87_count_noDominantOrder : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F87A.AdjectiveNounOrder) => x.value == Core.WALS.F87A.AdjectiveNounOrder.noDominantOrder) Phenomena.WordOrder.Typology.ch87✝).length = 110

theorem Phenomena.WordOrder.Typology.ch87_count_onlyIHRC : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F87A.AdjectiveNounOrder) => x.value == Core.WALS.F87A.AdjectiveNounOrder.onlyInternallyHeadedRelativeClauses) Phenomena.WordOrder.Typology.ch87✝).length = 5

theorem Phenomena.WordOrder.Typology.nounAdj_dominant_ch87 : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F87A.AdjectiveNounOrder) => x.value == Core.WALS.F87A.AdjectiveNounOrder.nounAdjective) Phenomena.WordOrder.Typology.ch87✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F87A.AdjectiveNounOrder) => x.value == Core.WALS.F87A.AdjectiveNounOrder.adjectiveNoun) Phenomena.WordOrder.Typology.ch87✝¹).length * 2

theorem Phenomena.WordOrder.Typology.english_ch87 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F87A.AdjectiveNounOrder) => x.value) (Core.WALS.F87A.lookup "eng") = some Core.WALS.F87A.AdjectiveNounOrder.adjectiveNoun

theorem Phenomena.WordOrder.Typology.japanese_ch87 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F87A.AdjectiveNounOrder) => x.value) (Core.WALS.F87A.lookup "jpn") = some Core.WALS.F87A.AdjectiveNounOrder.adjectiveNoun

theorem Phenomena.WordOrder.Typology.turkish_ch87 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F87A.AdjectiveNounOrder) => x.value) (Core.WALS.F87A.lookup "tur") = some Core.WALS.F87A.AdjectiveNounOrder.adjectiveNoun

theorem Phenomena.WordOrder.Typology.hindiUrdu_ch87 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F87A.AdjectiveNounOrder) => x.value) (Core.WALS.F87A.lookup "hin") = some Core.WALS.F87A.AdjectiveNounOrder.adjectiveNoun

theorem Phenomena.WordOrder.Typology.korean_ch87 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F87A.AdjectiveNounOrder) => x.value) (Core.WALS.F87A.lookup "kor") = some Core.WALS.F87A.AdjectiveNounOrder.adjectiveNoun

theorem Phenomena.WordOrder.Typology.basque_ch87 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F87A.AdjectiveNounOrder) => x.value) (Core.WALS.F87A.lookup "bsq") = some Core.WALS.F87A.AdjectiveNounOrder.nounAdjective

theorem Phenomena.WordOrder.Typology.mandarin_ch87 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F87A.AdjectiveNounOrder) => x.value) (Core.WALS.F87A.lookup "mnd") = some Core.WALS.F87A.AdjectiveNounOrder.adjectiveNoun

theorem Phenomena.WordOrder.Typology.russian_ch87 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F87A.AdjectiveNounOrder) => x.value) (Core.WALS.F87A.lookup "rus") = some Core.WALS.F87A.AdjectiveNounOrder.adjectiveNoun

theorem Phenomena.WordOrder.Typology.swahili_ch87 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F87A.AdjectiveNounOrder) => x.value) (Core.WALS.F87A.lookup "swa") = some Core.WALS.F87A.AdjectiveNounOrder.nounAdjective

theorem Phenomena.WordOrder.Typology.indonesian_ch87 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F87A.AdjectiveNounOrder) => x.value) (Core.WALS.F87A.lookup "ind") = some Core.WALS.F87A.AdjectiveNounOrder.nounAdjective

theorem Phenomena.WordOrder.Typology.arabic_ch87 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F87A.AdjectiveNounOrder) => x.value) (Core.WALS.F87A.lookup "ams") = some Core.WALS.F87A.AdjectiveNounOrder.nounAdjective

theorem Phenomena.WordOrder.Typology.irish_ch87 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F87A.AdjectiveNounOrder) => x.value) (Core.WALS.F87A.lookup "iri") = some Core.WALS.F87A.AdjectiveNounOrder.nounAdjective

theorem Phenomena.WordOrder.Typology.tagalog_ch87 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F87A.AdjectiveNounOrder) => x.value) (Core.WALS.F87A.lookup "tag") = some Core.WALS.F87A.AdjectiveNounOrder.noDominantOrder

theorem Phenomena.WordOrder.Typology.malagasy_ch87 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F87A.AdjectiveNounOrder) => x.value) (Core.WALS.F87A.lookup "mal") = some Core.WALS.F87A.AdjectiveNounOrder.nounAdjective

theorem Phenomena.WordOrder.Typology.hixkaryana_ch87 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F87A.AdjectiveNounOrder) => x.value) (Core.WALS.F87A.lookup "hix") = some Core.WALS.F87A.AdjectiveNounOrder.nounAdjective

theorem Phenomena.WordOrder.Typology.warlpiri_ch87 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F87A.AdjectiveNounOrder) => x.value) (Core.WALS.F87A.lookup "wrl") = some Core.WALS.F87A.AdjectiveNounOrder.nounAdjective

theorem Phenomena.WordOrder.Typology.welsh_ch87 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F87A.AdjectiveNounOrder) => x.value) (Core.WALS.F87A.lookup "wel") = some Core.WALS.F87A.AdjectiveNounOrder.nounAdjective

theorem Phenomena.WordOrder.Typology.german_ch87 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F87A.AdjectiveNounOrder) => x.value) (Core.WALS.F87A.lookup "ger") = some Core.WALS.F87A.AdjectiveNounOrder.adjectiveNoun

theorem Phenomena.WordOrder.Typology.ch88_total : Phenomena.WordOrder.Typology.ch88✝.length = 1225

Ch 88 total: 1225 languages.

theorem Phenomena.WordOrder.Typology.ch88_count_demonstrativeNoun : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F88A.DemonstrativeNounOrder) => x.value == Core.WALS.F88A.DemonstrativeNounOrder.demonstrativeNoun) Phenomena.WordOrder.Typology.ch88✝).length = 542

theorem Phenomena.WordOrder.Typology.ch88_count_nounDemonstrative : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F88A.DemonstrativeNounOrder) => x.value == Core.WALS.F88A.DemonstrativeNounOrder.nounDemonstrative) Phenomena.WordOrder.Typology.ch88✝).length = 562

theorem Phenomena.WordOrder.Typology.ch88_count_demonstrativePrefix : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F88A.DemonstrativeNounOrder) => x.value == Core.WALS.F88A.DemonstrativeNounOrder.demonstrativePrefix) Phenomena.WordOrder.Typology.ch88✝).length = 9

theorem Phenomena.WordOrder.Typology.ch88_count_demonstrativeSuffix : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F88A.DemonstrativeNounOrder) => x.value == Core.WALS.F88A.DemonstrativeNounOrder.demonstrativeSuffix) Phenomena.WordOrder.Typology.ch88✝).length = 28

theorem Phenomena.WordOrder.Typology.ch88_count_demonstrativeBeforeAndAfterNoun : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F88A.DemonstrativeNounOrder) => x.value == Core.WALS.F88A.DemonstrativeNounOrder.demonstrativeBeforeAndAfterNoun) Phenomena.WordOrder.Typology.ch88✝).length = 17

theorem Phenomena.WordOrder.Typology.ch88_count_mixed : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F88A.DemonstrativeNounOrder) => x.value == Core.WALS.F88A.DemonstrativeNounOrder.mixed) Phenomena.WordOrder.Typology.ch88✝).length = 67

theorem Phenomena.WordOrder.Typology.demN_roughly_balanced_ch88 : have demN := (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F88A.DemonstrativeNounOrder) => x.value == Core.WALS.F88A.DemonstrativeNounOrder.demonstrativeNoun) Phenomena.WordOrder.Typology.ch88✝).length; have nDem := (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F88A.DemonstrativeNounOrder) => x.value == Core.WALS.F88A.DemonstrativeNounOrder.nounDemonstrative) Phenomena.WordOrder.Typology.ch88✝¹).length; demN * 10 > nDem * 9

theorem Phenomena.WordOrder.Typology.english_ch88 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F88A.DemonstrativeNounOrder) => x.value) (Core.WALS.F88A.lookup "eng") = some Core.WALS.F88A.DemonstrativeNounOrder.demonstrativeNoun

theorem Phenomena.WordOrder.Typology.japanese_ch88 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F88A.DemonstrativeNounOrder) => x.value) (Core.WALS.F88A.lookup "jpn") = some Core.WALS.F88A.DemonstrativeNounOrder.demonstrativeNoun

theorem Phenomena.WordOrder.Typology.turkish_ch88 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F88A.DemonstrativeNounOrder) => x.value) (Core.WALS.F88A.lookup "tur") = some Core.WALS.F88A.DemonstrativeNounOrder.demonstrativeNoun

theorem Phenomena.WordOrder.Typology.hindiUrdu_ch88 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F88A.DemonstrativeNounOrder) => x.value) (Core.WALS.F88A.lookup "hin") = some Core.WALS.F88A.DemonstrativeNounOrder.demonstrativeNoun

theorem Phenomena.WordOrder.Typology.korean_ch88 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F88A.DemonstrativeNounOrder) => x.value) (Core.WALS.F88A.lookup "kor") = some Core.WALS.F88A.DemonstrativeNounOrder.demonstrativeNoun

theorem Phenomena.WordOrder.Typology.basque_ch88 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F88A.DemonstrativeNounOrder) => x.value) (Core.WALS.F88A.lookup "bsq") = some Core.WALS.F88A.DemonstrativeNounOrder.nounDemonstrative

theorem Phenomena.WordOrder.Typology.mandarin_ch88 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F88A.DemonstrativeNounOrder) => x.value) (Core.WALS.F88A.lookup "mnd") = some Core.WALS.F88A.DemonstrativeNounOrder.demonstrativeNoun

theorem Phenomena.WordOrder.Typology.russian_ch88 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F88A.DemonstrativeNounOrder) => x.value) (Core.WALS.F88A.lookup "rus") = some Core.WALS.F88A.DemonstrativeNounOrder.demonstrativeNoun

theorem Phenomena.WordOrder.Typology.swahili_ch88 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F88A.DemonstrativeNounOrder) => x.value) (Core.WALS.F88A.lookup "swa") = some Core.WALS.F88A.DemonstrativeNounOrder.nounDemonstrative

theorem Phenomena.WordOrder.Typology.indonesian_ch88 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F88A.DemonstrativeNounOrder) => x.value) (Core.WALS.F88A.lookup "ind") = some Core.WALS.F88A.DemonstrativeNounOrder.nounDemonstrative

theorem Phenomena.WordOrder.Typology.arabic_ch88 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F88A.DemonstrativeNounOrder) => x.value) (Core.WALS.F88A.lookup "ams") = some Core.WALS.F88A.DemonstrativeNounOrder.demonstrativeNoun

theorem Phenomena.WordOrder.Typology.irish_ch88 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F88A.DemonstrativeNounOrder) => x.value) (Core.WALS.F88A.lookup "iri") = some Core.WALS.F88A.DemonstrativeNounOrder.nounDemonstrative

theorem Phenomena.WordOrder.Typology.tagalog_ch88 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F88A.DemonstrativeNounOrder) => x.value) (Core.WALS.F88A.lookup "tag") = some Core.WALS.F88A.DemonstrativeNounOrder.mixed

theorem Phenomena.WordOrder.Typology.malagasy_ch88 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F88A.DemonstrativeNounOrder) => x.value) (Core.WALS.F88A.lookup "mal") = some Core.WALS.F88A.DemonstrativeNounOrder.demonstrativeBeforeAndAfterNoun

theorem Phenomena.WordOrder.Typology.welsh_ch88 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F88A.DemonstrativeNounOrder) => x.value) (Core.WALS.F88A.lookup "wel") = some Core.WALS.F88A.DemonstrativeNounOrder.nounDemonstrative

theorem Phenomena.WordOrder.Typology.german_ch88 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F88A.DemonstrativeNounOrder) => x.value) (Core.WALS.F88A.lookup "ger") = some Core.WALS.F88A.DemonstrativeNounOrder.demonstrativeNoun

theorem Phenomena.WordOrder.Typology.ch89_total : Phenomena.WordOrder.Typology.ch89✝.length = 1154

Ch 89 total: 1154 languages.

theorem Phenomena.WordOrder.Typology.ch89_count_numeralNoun : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F89A.NumeralNounOrder) => x.value == Core.WALS.F89A.NumeralNounOrder.numeralNoun) Phenomena.WordOrder.Typology.ch89✝).length = 479

theorem Phenomena.WordOrder.Typology.ch89_count_nounNumeral : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F89A.NumeralNounOrder) => x.value == Core.WALS.F89A.NumeralNounOrder.nounNumeral) Phenomena.WordOrder.Typology.ch89✝).length = 608

theorem Phenomena.WordOrder.Typology.ch89_count_noDominantOrder : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F89A.NumeralNounOrder) => x.value == Core.WALS.F89A.NumeralNounOrder.noDominantOrder) Phenomena.WordOrder.Typology.ch89✝).length = 65

theorem Phenomena.WordOrder.Typology.ch89_count_numeralOnlyModifiesVerb : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F89A.NumeralNounOrder) => x.value == Core.WALS.F89A.NumeralNounOrder.numeralOnlyModifiesVerb) Phenomena.WordOrder.Typology.ch89✝).length = 2

theorem Phenomena.WordOrder.Typology.english_ch89 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F89A.NumeralNounOrder) => x.value) (Core.WALS.F89A.lookup "eng") = some Core.WALS.F89A.NumeralNounOrder.numeralNoun

theorem Phenomena.WordOrder.Typology.japanese_ch89 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F89A.NumeralNounOrder) => x.value) (Core.WALS.F89A.lookup "jpn") = some Core.WALS.F89A.NumeralNounOrder.numeralNoun

theorem Phenomena.WordOrder.Typology.turkish_ch89 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F89A.NumeralNounOrder) => x.value) (Core.WALS.F89A.lookup "tur") = some Core.WALS.F89A.NumeralNounOrder.numeralNoun

theorem Phenomena.WordOrder.Typology.hindiUrdu_ch89 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F89A.NumeralNounOrder) => x.value) (Core.WALS.F89A.lookup "hin") = some Core.WALS.F89A.NumeralNounOrder.numeralNoun

theorem Phenomena.WordOrder.Typology.korean_ch89 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F89A.NumeralNounOrder) => x.value) (Core.WALS.F89A.lookup "kor") = some Core.WALS.F89A.NumeralNounOrder.numeralNoun

theorem Phenomena.WordOrder.Typology.basque_ch89 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F89A.NumeralNounOrder) => x.value) (Core.WALS.F89A.lookup "bsq") = some Core.WALS.F89A.NumeralNounOrder.numeralNoun

theorem Phenomena.WordOrder.Typology.mandarin_ch89 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F89A.NumeralNounOrder) => x.value) (Core.WALS.F89A.lookup "mnd") = some Core.WALS.F89A.NumeralNounOrder.numeralNoun

theorem Phenomena.WordOrder.Typology.russian_ch89 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F89A.NumeralNounOrder) => x.value) (Core.WALS.F89A.lookup "rus") = some Core.WALS.F89A.NumeralNounOrder.numeralNoun

theorem Phenomena.WordOrder.Typology.swahili_ch89 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F89A.NumeralNounOrder) => x.value) (Core.WALS.F89A.lookup "swa") = some Core.WALS.F89A.NumeralNounOrder.nounNumeral

theorem Phenomena.WordOrder.Typology.indonesian_ch89 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F89A.NumeralNounOrder) => x.value) (Core.WALS.F89A.lookup "ind") = some Core.WALS.F89A.NumeralNounOrder.numeralNoun

theorem Phenomena.WordOrder.Typology.arabic_ch89 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F89A.NumeralNounOrder) => x.value) (Core.WALS.F89A.lookup "ams") = some Core.WALS.F89A.NumeralNounOrder.numeralNoun

theorem Phenomena.WordOrder.Typology.irish_ch89 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F89A.NumeralNounOrder) => x.value) (Core.WALS.F89A.lookup "iri") = some Core.WALS.F89A.NumeralNounOrder.numeralNoun

theorem Phenomena.WordOrder.Typology.tagalog_ch89 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F89A.NumeralNounOrder) => x.value) (Core.WALS.F89A.lookup "tag") = some Core.WALS.F89A.NumeralNounOrder.numeralNoun

theorem Phenomena.WordOrder.Typology.malagasy_ch89 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F89A.NumeralNounOrder) => x.value) (Core.WALS.F89A.lookup "mal") = some Core.WALS.F89A.NumeralNounOrder.nounNumeral

theorem Phenomena.WordOrder.Typology.hixkaryana_ch89 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F89A.NumeralNounOrder) => x.value) (Core.WALS.F89A.lookup "hix") = some Core.WALS.F89A.NumeralNounOrder.numeralNoun

theorem Phenomena.WordOrder.Typology.welsh_ch89 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F89A.NumeralNounOrder) => x.value) (Core.WALS.F89A.lookup "wel") = some Core.WALS.F89A.NumeralNounOrder.numeralNoun

theorem Phenomena.WordOrder.Typology.german_ch89 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F89A.NumeralNounOrder) => x.value) (Core.WALS.F89A.lookup "ger") = some Core.WALS.F89A.NumeralNounOrder.numeralNoun

theorem Phenomena.WordOrder.Typology.ch90_total : Phenomena.WordOrder.Typology.ch90✝.length = 824

Ch 90 total: 824 languages.

theorem Phenomena.WordOrder.Typology.ch90_count_nounRelClause : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90A.RelClauseNounOrder) => x.value == Core.WALS.F90A.RelClauseNounOrder.nounRelativeClause) Phenomena.WordOrder.Typology.ch90✝).length = 579

theorem Phenomena.WordOrder.Typology.ch90_count_relClauseNoun : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90A.RelClauseNounOrder) => x.value == Core.WALS.F90A.RelClauseNounOrder.relativeClauseNoun) Phenomena.WordOrder.Typology.ch90✝).length = 141

theorem Phenomena.WordOrder.Typology.ch90_count_internallyHeaded : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90A.RelClauseNounOrder) => x.value == Core.WALS.F90A.RelClauseNounOrder.internallyHeaded) Phenomena.WordOrder.Typology.ch90✝).length = 24

theorem Phenomena.WordOrder.Typology.ch90_count_correlative : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90A.RelClauseNounOrder) => x.value == Core.WALS.F90A.RelClauseNounOrder.correlative) Phenomena.WordOrder.Typology.ch90✝).length = 7

theorem Phenomena.WordOrder.Typology.ch90_count_adjoined : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90A.RelClauseNounOrder) => x.value == Core.WALS.F90A.RelClauseNounOrder.adjoined) Phenomena.WordOrder.Typology.ch90✝).length = 8

theorem Phenomena.WordOrder.Typology.ch90_count_doublyHeaded : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90A.RelClauseNounOrder) => x.value == Core.WALS.F90A.RelClauseNounOrder.doublyHeaded) Phenomena.WordOrder.Typology.ch90✝).length = 1

theorem Phenomena.WordOrder.Typology.ch90_count_mixed : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90A.RelClauseNounOrder) => x.value == Core.WALS.F90A.RelClauseNounOrder.mixed) Phenomena.WordOrder.Typology.ch90✝).length = 64

theorem Phenomena.WordOrder.Typology.nounRelCl_dominant_ch90 : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90A.RelClauseNounOrder) => x.value == Core.WALS.F90A.RelClauseNounOrder.nounRelativeClause) Phenomena.WordOrder.Typology.ch90✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90A.RelClauseNounOrder) => x.value == Core.WALS.F90A.RelClauseNounOrder.relativeClauseNoun) Phenomena.WordOrder.Typology.ch90✝¹).length * 4

theorem Phenomena.WordOrder.Typology.english_ch90 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90A.RelClauseNounOrder) => x.value) (Core.WALS.F90A.lookup "eng") = some Core.WALS.F90A.RelClauseNounOrder.nounRelativeClause

theorem Phenomena.WordOrder.Typology.japanese_ch90 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90A.RelClauseNounOrder) => x.value) (Core.WALS.F90A.lookup "jpn") = some Core.WALS.F90A.RelClauseNounOrder.relativeClauseNoun

theorem Phenomena.WordOrder.Typology.turkish_ch90 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90A.RelClauseNounOrder) => x.value) (Core.WALS.F90A.lookup "tur") = some Core.WALS.F90A.RelClauseNounOrder.relativeClauseNoun

theorem Phenomena.WordOrder.Typology.hindiUrdu_ch90 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90A.RelClauseNounOrder) => x.value) (Core.WALS.F90A.lookup "hin") = some Core.WALS.F90A.RelClauseNounOrder.correlative

theorem Phenomena.WordOrder.Typology.korean_ch90 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90A.RelClauseNounOrder) => x.value) (Core.WALS.F90A.lookup "kor") = some Core.WALS.F90A.RelClauseNounOrder.relativeClauseNoun

theorem Phenomena.WordOrder.Typology.basque_ch90 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90A.RelClauseNounOrder) => x.value) (Core.WALS.F90A.lookup "bsq") = some Core.WALS.F90A.RelClauseNounOrder.relativeClauseNoun

theorem Phenomena.WordOrder.Typology.mandarin_ch90 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90A.RelClauseNounOrder) => x.value) (Core.WALS.F90A.lookup "mnd") = some Core.WALS.F90A.RelClauseNounOrder.relativeClauseNoun

theorem Phenomena.WordOrder.Typology.russian_ch90 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90A.RelClauseNounOrder) => x.value) (Core.WALS.F90A.lookup "rus") = some Core.WALS.F90A.RelClauseNounOrder.nounRelativeClause

theorem Phenomena.WordOrder.Typology.swahili_ch90 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90A.RelClauseNounOrder) => x.value) (Core.WALS.F90A.lookup "swa") = some Core.WALS.F90A.RelClauseNounOrder.nounRelativeClause

theorem Phenomena.WordOrder.Typology.indonesian_ch90 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90A.RelClauseNounOrder) => x.value) (Core.WALS.F90A.lookup "ind") = some Core.WALS.F90A.RelClauseNounOrder.nounRelativeClause

theorem Phenomena.WordOrder.Typology.irish_ch90 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90A.RelClauseNounOrder) => x.value) (Core.WALS.F90A.lookup "iri") = some Core.WALS.F90A.RelClauseNounOrder.nounRelativeClause

theorem Phenomena.WordOrder.Typology.tagalog_ch90 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90A.RelClauseNounOrder) => x.value) (Core.WALS.F90A.lookup "tag") = some Core.WALS.F90A.RelClauseNounOrder.nounRelativeClause

theorem Phenomena.WordOrder.Typology.malagasy_ch90 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90A.RelClauseNounOrder) => x.value) (Core.WALS.F90A.lookup "mal") = some Core.WALS.F90A.RelClauseNounOrder.nounRelativeClause

theorem Phenomena.WordOrder.Typology.hixkaryana_ch90 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90A.RelClauseNounOrder) => x.value) (Core.WALS.F90A.lookup "hix") = some Core.WALS.F90A.RelClauseNounOrder.nounRelativeClause

theorem Phenomena.WordOrder.Typology.warlpiri_ch90 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90A.RelClauseNounOrder) => x.value) (Core.WALS.F90A.lookup "wrl") = some Core.WALS.F90A.RelClauseNounOrder.adjoined

theorem Phenomena.WordOrder.Typology.welsh_ch90 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90A.RelClauseNounOrder) => x.value) (Core.WALS.F90A.lookup "wel") = some Core.WALS.F90A.RelClauseNounOrder.nounRelativeClause

theorem Phenomena.WordOrder.Typology.german_ch90 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90A.RelClauseNounOrder) => x.value) (Core.WALS.F90A.lookup "ger") = some Core.WALS.F90A.RelClauseNounOrder.nounRelativeClause

theorem Phenomena.WordOrder.Typology.ch91_total : Phenomena.WordOrder.Typology.ch91✝.length = 481

Ch 91 total: 481 languages.

theorem Phenomena.WordOrder.Typology.ch91_count_degreeWordAdjective : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F91A.OrderOfDegreeWordAndAdjective) => x.value == Core.WALS.F91A.OrderOfDegreeWordAndAdjective.degreeWordAdjective) Phenomena.WordOrder.Typology.ch91✝).length = 227

theorem Phenomena.WordOrder.Typology.ch91_count_adjectiveDegreeWord : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F91A.OrderOfDegreeWordAndAdjective) => x.value == Core.WALS.F91A.OrderOfDegreeWordAndAdjective.adjectiveDegreeWord) Phenomena.WordOrder.Typology.ch91✝).length = 192

theorem Phenomena.WordOrder.Typology.ch91_count_noDominantOrder : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F91A.OrderOfDegreeWordAndAdjective) => x.value == Core.WALS.F91A.OrderOfDegreeWordAndAdjective.noDominantOrder) Phenomena.WordOrder.Typology.ch91✝).length = 62

theorem Phenomena.WordOrder.Typology.english_ch91 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F91A.OrderOfDegreeWordAndAdjective) => x.value) (Core.WALS.F91A.lookup "eng") = some Core.WALS.F91A.OrderOfDegreeWordAndAdjective.degreeWordAdjective

theorem Phenomena.WordOrder.Typology.japanese_ch91 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F91A.OrderOfDegreeWordAndAdjective) => x.value) (Core.WALS.F91A.lookup "jpn") = some Core.WALS.F91A.OrderOfDegreeWordAndAdjective.degreeWordAdjective

theorem Phenomena.WordOrder.Typology.turkish_ch91 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F91A.OrderOfDegreeWordAndAdjective) => x.value) (Core.WALS.F91A.lookup "tur") = some Core.WALS.F91A.OrderOfDegreeWordAndAdjective.degreeWordAdjective

theorem Phenomena.WordOrder.Typology.hindiUrdu_ch91 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F91A.OrderOfDegreeWordAndAdjective) => x.value) (Core.WALS.F91A.lookup "hin") = some Core.WALS.F91A.OrderOfDegreeWordAndAdjective.degreeWordAdjective

theorem Phenomena.WordOrder.Typology.korean_ch91 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F91A.OrderOfDegreeWordAndAdjective) => x.value) (Core.WALS.F91A.lookup "kor") = some Core.WALS.F91A.OrderOfDegreeWordAndAdjective.degreeWordAdjective

theorem Phenomena.WordOrder.Typology.basque_ch91 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F91A.OrderOfDegreeWordAndAdjective) => x.value) (Core.WALS.F91A.lookup "bsq") = some Core.WALS.F91A.OrderOfDegreeWordAndAdjective.degreeWordAdjective

theorem Phenomena.WordOrder.Typology.mandarin_ch91 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F91A.OrderOfDegreeWordAndAdjective) => x.value) (Core.WALS.F91A.lookup "mnd") = some Core.WALS.F91A.OrderOfDegreeWordAndAdjective.degreeWordAdjective

theorem Phenomena.WordOrder.Typology.russian_ch91 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F91A.OrderOfDegreeWordAndAdjective) => x.value) (Core.WALS.F91A.lookup "rus") = some Core.WALS.F91A.OrderOfDegreeWordAndAdjective.degreeWordAdjective

theorem Phenomena.WordOrder.Typology.arabic_ch91 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F91A.OrderOfDegreeWordAndAdjective) => x.value) (Core.WALS.F91A.lookup "ams") = some Core.WALS.F91A.OrderOfDegreeWordAndAdjective.adjectiveDegreeWord

theorem Phenomena.WordOrder.Typology.hixkaryana_ch91 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F91A.OrderOfDegreeWordAndAdjective) => x.value) (Core.WALS.F91A.lookup "hix") = some Core.WALS.F91A.OrderOfDegreeWordAndAdjective.adjectiveDegreeWord

theorem Phenomena.WordOrder.Typology.welsh_ch91 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F91A.OrderOfDegreeWordAndAdjective) => x.value) (Core.WALS.F91A.lookup "wel") = some Core.WALS.F91A.OrderOfDegreeWordAndAdjective.noDominantOrder

theorem Phenomena.WordOrder.Typology.german_ch91 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F91A.OrderOfDegreeWordAndAdjective) => x.value) (Core.WALS.F91A.lookup "ger") = some Core.WALS.F91A.OrderOfDegreeWordAndAdjective.degreeWordAdjective

theorem Phenomena.WordOrder.Typology.indonesian_ch91 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F91A.OrderOfDegreeWordAndAdjective) => x.value) (Core.WALS.F91A.lookup "ind") = some Core.WALS.F91A.OrderOfDegreeWordAndAdjective.degreeWordAdjective

theorem Phenomena.WordOrder.Typology.ch94_total : Phenomena.WordOrder.Typology.ch94✝.length = 659

Ch 94 total: 659 languages.

theorem Phenomena.WordOrder.Typology.ch94_count_initialSubordinatorWord : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause) => x.value == Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause.initialSubordinatorWord) Phenomena.WordOrder.Typology.ch94✝).length = 398

theorem Phenomena.WordOrder.Typology.ch94_count_finalSubordinatorWord : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause) => x.value == Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause.finalSubordinatorWord) Phenomena.WordOrder.Typology.ch94✝).length = 96

theorem Phenomena.WordOrder.Typology.ch94_count_internalSubordinatorWord : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause) => x.value == Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause.internalSubordinatorWord) Phenomena.WordOrder.Typology.ch94✝).length = 8

theorem Phenomena.WordOrder.Typology.ch94_count_subordinatingSuffix : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause) => x.value == Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause.subordinatingSuffix) Phenomena.WordOrder.Typology.ch94✝).length = 64

theorem Phenomena.WordOrder.Typology.ch94_count_mixed : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause) => x.value == Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause.mixed) Phenomena.WordOrder.Typology.ch94✝).length = 93

theorem Phenomena.WordOrder.Typology.initial_subordinator_dominant_ch94 : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause) => x.value == Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause.initialSubordinatorWord) Phenomena.WordOrder.Typology.ch94✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause) => x.value == Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause.finalSubordinatorWord) Phenomena.WordOrder.Typology.ch94✝¹).length * 4

theorem Phenomena.WordOrder.Typology.english_ch94 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause) => x.value) (Core.WALS.F94A.lookup "eng") = some Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause.initialSubordinatorWord

theorem Phenomena.WordOrder.Typology.hindiUrdu_ch94 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause) => x.value) (Core.WALS.F94A.lookup "hin") = some Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause.initialSubordinatorWord

theorem Phenomena.WordOrder.Typology.korean_ch94 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause) => x.value) (Core.WALS.F94A.lookup "kor") = some Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause.finalSubordinatorWord

theorem Phenomena.WordOrder.Typology.russian_ch94 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause) => x.value) (Core.WALS.F94A.lookup "rus") = some Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause.initialSubordinatorWord

theorem Phenomena.WordOrder.Typology.swahili_ch94 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause) => x.value) (Core.WALS.F94A.lookup "swa") = some Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause.initialSubordinatorWord

theorem Phenomena.WordOrder.Typology.indonesian_ch94 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause) => x.value) (Core.WALS.F94A.lookup "ind") = some Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause.initialSubordinatorWord

theorem Phenomena.WordOrder.Typology.arabic_ch94 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause) => x.value) (Core.WALS.F94A.lookup "ams") = some Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause.initialSubordinatorWord

theorem Phenomena.WordOrder.Typology.irish_ch94 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause) => x.value) (Core.WALS.F94A.lookup "iri") = some Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause.initialSubordinatorWord

theorem Phenomena.WordOrder.Typology.tagalog_ch94 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause) => x.value) (Core.WALS.F94A.lookup "tag") = some Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause.initialSubordinatorWord

theorem Phenomena.WordOrder.Typology.malagasy_ch94 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause) => x.value) (Core.WALS.F94A.lookup "mal") = some Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause.initialSubordinatorWord

theorem Phenomena.WordOrder.Typology.tzotzil_ch94 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause) => x.value) (Core.WALS.F94A.lookup "tzo") = some Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause.initialSubordinatorWord

theorem Phenomena.WordOrder.Typology.hixkaryana_ch94 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause) => x.value) (Core.WALS.F94A.lookup "hix") = some Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause.finalSubordinatorWord

theorem Phenomena.WordOrder.Typology.welsh_ch94 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause) => x.value) (Core.WALS.F94A.lookup "wel") = some Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause.initialSubordinatorWord

theorem Phenomena.WordOrder.Typology.german_ch94 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause) => x.value) (Core.WALS.F94A.lookup "ger") = some Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause.initialSubordinatorWord

theorem Phenomena.WordOrder.Typology.turkish_ch94 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause) => x.value) (Core.WALS.F94A.lookup "tur") = some Core.WALS.F94A.OrderOfAdverbialSubordinatorAndClause.mixed

theorem Phenomena.WordOrder.Typology.ch95_total : Phenomena.WordOrder.Typology.ch95✝.length = 1142

Ch 95 total: 1142 languages.

theorem Phenomena.WordOrder.Typology.ch95_count_ovAndPostpositions : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase) => x.value == Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase.ovAndPostpositions) Phenomena.WordOrder.Typology.ch95✝).length = 472

theorem Phenomena.WordOrder.Typology.ch95_count_ovAndPrepositions : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase) => x.value == Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase.ovAndPrepositions) Phenomena.WordOrder.Typology.ch95✝).length = 14

theorem Phenomena.WordOrder.Typology.ch95_count_voAndPostpositions : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase) => x.value == Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase.voAndPostpositions) Phenomena.WordOrder.Typology.ch95✝).length = 42

theorem Phenomena.WordOrder.Typology.ch95_count_voAndPrepositions : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase) => x.value == Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase.voAndPrepositions) Phenomena.WordOrder.Typology.ch95✝).length = 456

theorem Phenomena.WordOrder.Typology.ch95_count_other : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase) => x.value == Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase.other) Phenomena.WordOrder.Typology.ch95✝).length = 158

theorem Phenomena.WordOrder.Typology.ch95_harmonic_dominant : have harmonic := (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase) => x.value == Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase.ovAndPostpositions) Phenomena.WordOrder.Typology.ch95✝).length + (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase) => x.value == Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase.voAndPrepositions) Phenomena.WordOrder.Typology.ch95✝¹).length; have disharmonic := (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase) => x.value == Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase.ovAndPrepositions) Phenomena.WordOrder.Typology.ch95✝²).length + (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase) => x.value == Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase.voAndPostpositions) Phenomena.WordOrder.Typology.ch95✝³).length; harmonic > disharmonic * 16

theorem Phenomena.WordOrder.Typology.english_ch95 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase) => x.value) (Core.WALS.F95A.lookup "eng") = some Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase.voAndPrepositions

theorem Phenomena.WordOrder.Typology.japanese_ch95 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase) => x.value) (Core.WALS.F95A.lookup "jpn") = some Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase.ovAndPostpositions

theorem Phenomena.WordOrder.Typology.turkish_ch95 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase) => x.value) (Core.WALS.F95A.lookup "tur") = some Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase.ovAndPostpositions

theorem Phenomena.WordOrder.Typology.hindiUrdu_ch95 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase) => x.value) (Core.WALS.F95A.lookup "hin") = some Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase.ovAndPostpositions

theorem Phenomena.WordOrder.Typology.korean_ch95 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase) => x.value) (Core.WALS.F95A.lookup "kor") = some Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase.ovAndPostpositions

theorem Phenomena.WordOrder.Typology.basque_ch95 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase) => x.value) (Core.WALS.F95A.lookup "bsq") = some Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase.ovAndPostpositions

theorem Phenomena.WordOrder.Typology.mandarin_ch95 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase) => x.value) (Core.WALS.F95A.lookup "mnd") = some Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase.other

theorem Phenomena.WordOrder.Typology.russian_ch95 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase) => x.value) (Core.WALS.F95A.lookup "rus") = some Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase.voAndPrepositions

theorem Phenomena.WordOrder.Typology.swahili_ch95 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase) => x.value) (Core.WALS.F95A.lookup "swa") = some Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase.voAndPrepositions

theorem Phenomena.WordOrder.Typology.indonesian_ch95 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase) => x.value) (Core.WALS.F95A.lookup "ind") = some Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase.voAndPrepositions

theorem Phenomena.WordOrder.Typology.arabic_ch95 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase) => x.value) (Core.WALS.F95A.lookup "ams") = some Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase.voAndPrepositions

theorem Phenomena.WordOrder.Typology.irish_ch95 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase) => x.value) (Core.WALS.F95A.lookup "iri") = some Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase.voAndPrepositions

theorem Phenomena.WordOrder.Typology.malagasy_ch95 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase) => x.value) (Core.WALS.F95A.lookup "mal") = some Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase.voAndPrepositions

theorem Phenomena.WordOrder.Typology.tzotzil_ch95 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase) => x.value) (Core.WALS.F95A.lookup "tzo") = some Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase.voAndPrepositions

theorem Phenomena.WordOrder.Typology.hixkaryana_ch95 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase) => x.value) (Core.WALS.F95A.lookup "hix") = some Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase.ovAndPostpositions

theorem Phenomena.WordOrder.Typology.german_ch95 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase) => x.value) (Core.WALS.F95A.lookup "ger") = some Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase.other

theorem Phenomena.WordOrder.Typology.warlpiri_ch95 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase) => x.value) (Core.WALS.F95A.lookup "wrl") = some Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase.other

theorem Phenomena.WordOrder.Typology.welsh_ch95 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase) => x.value) (Core.WALS.F95A.lookup "wel") = some Core.WALS.F95A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdpositionAndNounPhrase.voAndPrepositions

theorem Phenomena.WordOrder.Typology.ch96_total : Phenomena.WordOrder.Typology.ch96✝.length = 879

Ch 96 total: 879 languages.

theorem Phenomena.WordOrder.Typology.ch96_count_ovAndReln : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun) => x.value == Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun.ovAndReln) Phenomena.WordOrder.Typology.ch96✝).length = 132

theorem Phenomena.WordOrder.Typology.ch96_count_ovAndNrel : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun) => x.value == Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun.ovAndNrel) Phenomena.WordOrder.Typology.ch96✝).length = 113

theorem Phenomena.WordOrder.Typology.ch96_count_voAndReln : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun) => x.value == Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun.voAndReln) Phenomena.WordOrder.Typology.ch96✝).length = 5

theorem Phenomena.WordOrder.Typology.ch96_count_voAndNrel : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun) => x.value == Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun.voAndNrel) Phenomena.WordOrder.Typology.ch96✝).length = 416

theorem Phenomena.WordOrder.Typology.ch96_count_other : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun) => x.value == Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun.other) Phenomena.WordOrder.Typology.ch96✝).length = 213

theorem Phenomena.WordOrder.Typology.ch96_voNRel_dominant : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun) => x.value == Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun.voAndNrel) Phenomena.WordOrder.Typology.ch96✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun) => x.value == Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun.voAndReln) Phenomena.WordOrder.Typology.ch96✝¹).length * 80

theorem Phenomena.WordOrder.Typology.english_ch96 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun) => x.value) (Core.WALS.F96A.lookup "eng") = some Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun.voAndNrel

theorem Phenomena.WordOrder.Typology.japanese_ch96 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun) => x.value) (Core.WALS.F96A.lookup "jpn") = some Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun.ovAndReln

theorem Phenomena.WordOrder.Typology.turkish_ch96 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun) => x.value) (Core.WALS.F96A.lookup "tur") = some Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun.ovAndReln

theorem Phenomena.WordOrder.Typology.hindiUrdu_ch96 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun) => x.value) (Core.WALS.F96A.lookup "hin") = some Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun.other

theorem Phenomena.WordOrder.Typology.korean_ch96 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun) => x.value) (Core.WALS.F96A.lookup "kor") = some Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun.ovAndReln

theorem Phenomena.WordOrder.Typology.basque_ch96 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun) => x.value) (Core.WALS.F96A.lookup "bsq") = some Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun.ovAndReln

theorem Phenomena.WordOrder.Typology.mandarin_ch96 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun) => x.value) (Core.WALS.F96A.lookup "mnd") = some Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun.voAndReln

theorem Phenomena.WordOrder.Typology.russian_ch96 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun) => x.value) (Core.WALS.F96A.lookup "rus") = some Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun.voAndNrel

theorem Phenomena.WordOrder.Typology.swahili_ch96 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun) => x.value) (Core.WALS.F96A.lookup "swa") = some Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun.voAndNrel

theorem Phenomena.WordOrder.Typology.indonesian_ch96 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun) => x.value) (Core.WALS.F96A.lookup "ind") = some Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun.voAndNrel

theorem Phenomena.WordOrder.Typology.irish_ch96 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun) => x.value) (Core.WALS.F96A.lookup "iri") = some Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun.voAndNrel

theorem Phenomena.WordOrder.Typology.tagalog_ch96 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun) => x.value) (Core.WALS.F96A.lookup "tag") = some Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun.voAndNrel

theorem Phenomena.WordOrder.Typology.malagasy_ch96 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun) => x.value) (Core.WALS.F96A.lookup "mal") = some Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun.voAndNrel

theorem Phenomena.WordOrder.Typology.hixkaryana_ch96 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun) => x.value) (Core.WALS.F96A.lookup "hix") = some Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun.ovAndNrel

theorem Phenomena.WordOrder.Typology.german_ch96 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun) => x.value) (Core.WALS.F96A.lookup "ger") = some Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun.other

theorem Phenomena.WordOrder.Typology.warlpiri_ch96 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun) => x.value) (Core.WALS.F96A.lookup "wrl") = some Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun.other

theorem Phenomena.WordOrder.Typology.welsh_ch96 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun) => x.value) (Core.WALS.F96A.lookup "wel") = some Core.WALS.F96A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfRelativeClauseAndNoun.voAndNrel

theorem Phenomena.WordOrder.Typology.ch97_total : Phenomena.WordOrder.Typology.ch97✝.length = 1316

Ch 97 total: 1316 languages.

theorem Phenomena.WordOrder.Typology.ch97_count_ovAndAdjn : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun) => x.value == Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun.ovAndAdjn) Phenomena.WordOrder.Typology.ch97✝).length = 216

theorem Phenomena.WordOrder.Typology.ch97_count_ovAndNadj : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun) => x.value == Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun.ovAndNadj) Phenomena.WordOrder.Typology.ch97✝).length = 332

theorem Phenomena.WordOrder.Typology.ch97_count_voAndAdjn : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun) => x.value == Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun.voAndAdjn) Phenomena.WordOrder.Typology.ch97✝).length = 114

theorem Phenomena.WordOrder.Typology.ch97_count_voAndNadj : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun) => x.value == Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun.voAndNadj) Phenomena.WordOrder.Typology.ch97✝).length = 456

theorem Phenomena.WordOrder.Typology.ch97_count_other : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun) => x.value == Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun.other) Phenomena.WordOrder.Typology.ch97✝).length = 198

theorem Phenomena.WordOrder.Typology.ch97_ov_split : have ovAdjN := (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun) => x.value == Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun.ovAndAdjn) Phenomena.WordOrder.Typology.ch97✝).length; have ovNAdj := (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun) => x.value == Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun.ovAndNadj) Phenomena.WordOrder.Typology.ch97✝¹).length; ovNAdj > ovAdjN

theorem Phenomena.WordOrder.Typology.english_ch97 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun) => x.value) (Core.WALS.F97A.lookup "eng") = some Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun.voAndAdjn

theorem Phenomena.WordOrder.Typology.japanese_ch97 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun) => x.value) (Core.WALS.F97A.lookup "jpn") = some Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun.ovAndAdjn

theorem Phenomena.WordOrder.Typology.turkish_ch97 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun) => x.value) (Core.WALS.F97A.lookup "tur") = some Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun.ovAndAdjn

theorem Phenomena.WordOrder.Typology.hindiUrdu_ch97 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun) => x.value) (Core.WALS.F97A.lookup "hin") = some Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun.ovAndAdjn

theorem Phenomena.WordOrder.Typology.korean_ch97 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun) => x.value) (Core.WALS.F97A.lookup "kor") = some Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun.ovAndAdjn

theorem Phenomena.WordOrder.Typology.basque_ch97 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun) => x.value) (Core.WALS.F97A.lookup "bsq") = some Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun.ovAndNadj

theorem Phenomena.WordOrder.Typology.mandarin_ch97 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun) => x.value) (Core.WALS.F97A.lookup "mnd") = some Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun.voAndAdjn

theorem Phenomena.WordOrder.Typology.russian_ch97 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun) => x.value) (Core.WALS.F97A.lookup "rus") = some Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun.voAndAdjn

theorem Phenomena.WordOrder.Typology.swahili_ch97 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun) => x.value) (Core.WALS.F97A.lookup "swa") = some Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun.voAndNadj

theorem Phenomena.WordOrder.Typology.indonesian_ch97 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun) => x.value) (Core.WALS.F97A.lookup "ind") = some Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun.voAndNadj

theorem Phenomena.WordOrder.Typology.arabic_ch97 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun) => x.value) (Core.WALS.F97A.lookup "ams") = some Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun.voAndNadj

theorem Phenomena.WordOrder.Typology.irish_ch97 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun) => x.value) (Core.WALS.F97A.lookup "iri") = some Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun.voAndNadj

theorem Phenomena.WordOrder.Typology.tagalog_ch97 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun) => x.value) (Core.WALS.F97A.lookup "tag") = some Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun.other

theorem Phenomena.WordOrder.Typology.malagasy_ch97 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun) => x.value) (Core.WALS.F97A.lookup "mal") = some Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun.voAndNadj

theorem Phenomena.WordOrder.Typology.hixkaryana_ch97 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun) => x.value) (Core.WALS.F97A.lookup "hix") = some Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun.ovAndNadj

theorem Phenomena.WordOrder.Typology.german_ch97 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun) => x.value) (Core.WALS.F97A.lookup "ger") = some Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun.other

theorem Phenomena.WordOrder.Typology.warlpiri_ch97 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun) => x.value) (Core.WALS.F97A.lookup "wrl") = some Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun.other

theorem Phenomena.WordOrder.Typology.welsh_ch97 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun) => x.value) (Core.WALS.F97A.lookup "wel") = some Core.WALS.F97A.RelationshipBetweenTheOrderOfObjectAndVerbAndTheOrderOfAdjectiveAndNoun.voAndNadj

theorem Phenomena.WordOrder.Typology.ch81B_total : Phenomena.WordOrder.Typology.ch81B✝.length = 67

Ch 81B total: 67 languages.

theorem Phenomena.WordOrder.Typology.ch81B_count_sovOrSvo : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F81B.LanguagesWithTwoDominantOrdersOfSubjectObjectAndVerb) => x.value == Core.WALS.F81B.LanguagesWithTwoDominantOrdersOfSubjectObjectAndVerb.sovOrSvo) Phenomena.WordOrder.Typology.ch81B✝).length = 29

theorem Phenomena.WordOrder.Typology.ch81B_count_vsoOrVos : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F81B.LanguagesWithTwoDominantOrdersOfSubjectObjectAndVerb) => x.value == Core.WALS.F81B.LanguagesWithTwoDominantOrdersOfSubjectObjectAndVerb.vsoOrVos) Phenomena.WordOrder.Typology.ch81B✝).length = 14

theorem Phenomena.WordOrder.Typology.ch81B_count_svoOrVso : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F81B.LanguagesWithTwoDominantOrdersOfSubjectObjectAndVerb) => x.value == Core.WALS.F81B.LanguagesWithTwoDominantOrdersOfSubjectObjectAndVerb.svoOrVso) Phenomena.WordOrder.Typology.ch81B✝).length = 13

theorem Phenomena.WordOrder.Typology.ch81B_count_svoOrVos : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F81B.LanguagesWithTwoDominantOrdersOfSubjectObjectAndVerb) => x.value == Core.WALS.F81B.LanguagesWithTwoDominantOrdersOfSubjectObjectAndVerb.svoOrVos) Phenomena.WordOrder.Typology.ch81B✝).length = 8

theorem Phenomena.WordOrder.Typology.ch81B_count_sovOrOvs : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F81B.LanguagesWithTwoDominantOrdersOfSubjectObjectAndVerb) => x.value == Core.WALS.F81B.LanguagesWithTwoDominantOrdersOfSubjectObjectAndVerb.sovOrOvs) Phenomena.WordOrder.Typology.ch81B✝).length = 3

theorem Phenomena.WordOrder.Typology.ch81B_sovOrSvo_most_common : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F81B.LanguagesWithTwoDominantOrdersOfSubjectObjectAndVerb) => x.value == Core.WALS.F81B.LanguagesWithTwoDominantOrdersOfSubjectObjectAndVerb.sovOrSvo) Phenomena.WordOrder.Typology.ch81B✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F81B.LanguagesWithTwoDominantOrdersOfSubjectObjectAndVerb) => x.value == Core.WALS.F81B.LanguagesWithTwoDominantOrdersOfSubjectObjectAndVerb.vsoOrVos) Phenomena.WordOrder.Typology.ch81B✝¹).length

theorem Phenomena.WordOrder.Typology.german_ch81B : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F81B.LanguagesWithTwoDominantOrdersOfSubjectObjectAndVerb) => x.value) (Core.WALS.F81B.lookup "ger") = some Core.WALS.F81B.LanguagesWithTwoDominantOrdersOfSubjectObjectAndVerb.sovOrSvo

theorem Phenomena.WordOrder.Typology.hungarian_ch81B : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F81B.LanguagesWithTwoDominantOrdersOfSubjectObjectAndVerb) => x.value) (Core.WALS.F81B.lookup "hun") = some Core.WALS.F81B.LanguagesWithTwoDominantOrdersOfSubjectObjectAndVerb.sovOrSvo

theorem Phenomena.WordOrder.Typology.ch90B_total : Phenomena.WordOrder.Typology.ch90B✝.length = 191

Ch 90B total: 191 languages.

theorem Phenomena.WordOrder.Typology.ch90B_count_relativeClauseNounDominant : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90B.PrenominalRelativeClauses) => x.value == Core.WALS.F90B.PrenominalRelativeClauses.relativeClauseNounDominant) Phenomena.WordOrder.Typology.ch90B✝).length = 141

theorem Phenomena.WordOrder.Typology.ch90B_count_relnOrNrel : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90B.PrenominalRelativeClauses) => x.value == Core.WALS.F90B.PrenominalRelativeClauses.relnOrNrel) Phenomena.WordOrder.Typology.ch90B✝).length = 29

theorem Phenomena.WordOrder.Typology.ch90B_count_relnOrInternallyHeaded : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90B.PrenominalRelativeClauses) => x.value == Core.WALS.F90B.PrenominalRelativeClauses.relnOrInternallyHeaded) Phenomena.WordOrder.Typology.ch90B✝).length = 15

theorem Phenomena.WordOrder.Typology.ch90B_count_relnOrCorrelative : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90B.PrenominalRelativeClauses) => x.value == Core.WALS.F90B.PrenominalRelativeClauses.relnOrCorrelative) Phenomena.WordOrder.Typology.ch90B✝).length = 5

theorem Phenomena.WordOrder.Typology.ch90B_count_relnOrDoubleHeaded : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90B.PrenominalRelativeClauses) => x.value == Core.WALS.F90B.PrenominalRelativeClauses.relnOrDoubleHeaded) Phenomena.WordOrder.Typology.ch90B✝).length = 1

theorem Phenomena.WordOrder.Typology.ch90B_dominant_relN_majority : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90B.PrenominalRelativeClauses) => x.value == Core.WALS.F90B.PrenominalRelativeClauses.relativeClauseNounDominant) Phenomena.WordOrder.Typology.ch90B✝).length > Phenomena.WordOrder.Typology.ch90B✝¹.length / 2

theorem Phenomena.WordOrder.Typology.japanese_ch90B : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90B.PrenominalRelativeClauses) => x.value) (Core.WALS.F90B.lookup "jpn") = some Core.WALS.F90B.PrenominalRelativeClauses.relativeClauseNounDominant

theorem Phenomena.WordOrder.Typology.korean_ch90B : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90B.PrenominalRelativeClauses) => x.value) (Core.WALS.F90B.lookup "kor") = some Core.WALS.F90B.PrenominalRelativeClauses.relativeClauseNounDominant

theorem Phenomena.WordOrder.Typology.turkish_ch90B : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90B.PrenominalRelativeClauses) => x.value) (Core.WALS.F90B.lookup "tur") = some Core.WALS.F90B.PrenominalRelativeClauses.relativeClauseNounDominant

theorem Phenomena.WordOrder.Typology.mandarin_ch90B : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90B.PrenominalRelativeClauses) => x.value) (Core.WALS.F90B.lookup "mnd") = some Core.WALS.F90B.PrenominalRelativeClauses.relativeClauseNounDominant

theorem Phenomena.WordOrder.Typology.basque_ch90B : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90B.PrenominalRelativeClauses) => x.value) (Core.WALS.F90B.lookup "bsq") = some Core.WALS.F90B.PrenominalRelativeClauses.relativeClauseNounDominant

theorem Phenomena.WordOrder.Typology.hungarian_ch90B : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90B.PrenominalRelativeClauses) => x.value) (Core.WALS.F90B.lookup "hun") = some Core.WALS.F90B.PrenominalRelativeClauses.relnOrNrel

theorem Phenomena.WordOrder.Typology.ch90C_total : Phenomena.WordOrder.Typology.ch90C✝.length = 620

Ch 90C total: 620 languages.

theorem Phenomena.WordOrder.Typology.ch90C_count_nounRelativeClauseDominant : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90C.PostnominalRelativeClauses) => x.value == Core.WALS.F90C.PostnominalRelativeClauses.nounRelativeClauseDominant) Phenomena.WordOrder.Typology.ch90C✝).length = 579

theorem Phenomena.WordOrder.Typology.ch90C_count_nrelOrReln : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90C.PostnominalRelativeClauses) => x.value == Core.WALS.F90C.PostnominalRelativeClauses.nrelOrReln) Phenomena.WordOrder.Typology.ch90C✝).length = 31

theorem Phenomena.WordOrder.Typology.ch90C_count_nrelOrInternallyHeaded : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90C.PostnominalRelativeClauses) => x.value == Core.WALS.F90C.PostnominalRelativeClauses.nrelOrInternallyHeaded) Phenomena.WordOrder.Typology.ch90C✝).length = 8

theorem Phenomena.WordOrder.Typology.ch90C_count_nrelOrCorrelative : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90C.PostnominalRelativeClauses) => x.value == Core.WALS.F90C.PostnominalRelativeClauses.nrelOrCorrelative) Phenomena.WordOrder.Typology.ch90C✝).length = 2

theorem Phenomena.WordOrder.Typology.ch90C_dominant_nRel_majority : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90C.PostnominalRelativeClauses) => x.value == Core.WALS.F90C.PostnominalRelativeClauses.nounRelativeClauseDominant) Phenomena.WordOrder.Typology.ch90C✝).length > Phenomena.WordOrder.Typology.ch90C✝¹.length * 9 / 10

theorem Phenomena.WordOrder.Typology.english_ch90C : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90C.PostnominalRelativeClauses) => x.value) (Core.WALS.F90C.lookup "eng") = some Core.WALS.F90C.PostnominalRelativeClauses.nounRelativeClauseDominant

theorem Phenomena.WordOrder.Typology.russian_ch90C : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90C.PostnominalRelativeClauses) => x.value) (Core.WALS.F90C.lookup "rus") = some Core.WALS.F90C.PostnominalRelativeClauses.nounRelativeClauseDominant

theorem Phenomena.WordOrder.Typology.swahili_ch90C : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90C.PostnominalRelativeClauses) => x.value) (Core.WALS.F90C.lookup "swa") = some Core.WALS.F90C.PostnominalRelativeClauses.nounRelativeClauseDominant

theorem Phenomena.WordOrder.Typology.indonesian_ch90C : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90C.PostnominalRelativeClauses) => x.value) (Core.WALS.F90C.lookup "ind") = some Core.WALS.F90C.PostnominalRelativeClauses.nounRelativeClauseDominant

theorem Phenomena.WordOrder.Typology.irish_ch90C : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90C.PostnominalRelativeClauses) => x.value) (Core.WALS.F90C.lookup "iri") = some Core.WALS.F90C.PostnominalRelativeClauses.nounRelativeClauseDominant

theorem Phenomena.WordOrder.Typology.welsh_ch90C : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90C.PostnominalRelativeClauses) => x.value) (Core.WALS.F90C.lookup "wel") = some Core.WALS.F90C.PostnominalRelativeClauses.nounRelativeClauseDominant

theorem Phenomena.WordOrder.Typology.german_ch90C : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90C.PostnominalRelativeClauses) => x.value) (Core.WALS.F90C.lookup "ger") = some Core.WALS.F90C.PostnominalRelativeClauses.nounRelativeClauseDominant

theorem Phenomena.WordOrder.Typology.hixkaryana_ch90C : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90C.PostnominalRelativeClauses) => x.value) (Core.WALS.F90C.lookup "hix") = some Core.WALS.F90C.PostnominalRelativeClauses.nounRelativeClauseDominant

theorem Phenomena.WordOrder.Typology.tagalog_ch90C : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90C.PostnominalRelativeClauses) => x.value) (Core.WALS.F90C.lookup "tag") = some Core.WALS.F90C.PostnominalRelativeClauses.nounRelativeClauseDominant

theorem Phenomena.WordOrder.Typology.malagasy_ch90C : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90C.PostnominalRelativeClauses) => x.value) (Core.WALS.F90C.lookup "mal") = some Core.WALS.F90C.PostnominalRelativeClauses.nounRelativeClauseDominant

theorem Phenomena.WordOrder.Typology.hungarian_ch90C : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90C.PostnominalRelativeClauses) => x.value) (Core.WALS.F90C.lookup "hun") = some Core.WALS.F90C.PostnominalRelativeClauses.nrelOrReln

theorem Phenomena.WordOrder.Typology.ch90D_total : Phenomena.WordOrder.Typology.ch90D✝.length = 63

Ch 90D total: 63 languages.

theorem Phenomena.WordOrder.Typology.ch90D_count_internallyHeadedRelativeClauseDominant : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90D.InternallyHeadedRelativeClauses) => x.value == Core.WALS.F90D.InternallyHeadedRelativeClauses.internallyHeadedRelativeClauseDominant) Phenomena.WordOrder.Typology.ch90D✝).length = 24

theorem Phenomena.WordOrder.Typology.ch90D_count_internallyHeadedOrReln : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90D.InternallyHeadedRelativeClauses) => x.value == Core.WALS.F90D.InternallyHeadedRelativeClauses.internallyHeadedOrReln) Phenomena.WordOrder.Typology.ch90D✝).length = 15

theorem Phenomena.WordOrder.Typology.ch90D_count_internallyHeadedOrNrel : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90D.InternallyHeadedRelativeClauses) => x.value == Core.WALS.F90D.InternallyHeadedRelativeClauses.internallyHeadedOrNrel) Phenomena.WordOrder.Typology.ch90D✝).length = 8

theorem Phenomena.WordOrder.Typology.ch90D_count_internallyHeadedOrCorrelative : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90D.InternallyHeadedRelativeClauses) => x.value == Core.WALS.F90D.InternallyHeadedRelativeClauses.internallyHeadedOrCorrelative) Phenomena.WordOrder.Typology.ch90D✝).length = 1

theorem Phenomena.WordOrder.Typology.ch90D_count_internallyHeadedOrDoubleHeaded : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90D.InternallyHeadedRelativeClauses) => x.value == Core.WALS.F90D.InternallyHeadedRelativeClauses.internallyHeadedOrDoubleHeaded) Phenomena.WordOrder.Typology.ch90D✝).length = 1

theorem Phenomena.WordOrder.Typology.ch90D_count_internallyHeadedOccursAsNondominantType : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90D.InternallyHeadedRelativeClauses) => x.value == Core.WALS.F90D.InternallyHeadedRelativeClauses.internallyHeadedOccursAsNondominantType) Phenomena.WordOrder.Typology.ch90D✝).length = 10

theorem Phenomena.WordOrder.Typology.ch90D_count_internallyHeadedExists : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90D.InternallyHeadedRelativeClauses) => x.value == Core.WALS.F90D.InternallyHeadedRelativeClauses.internallyHeadedExists) Phenomena.WordOrder.Typology.ch90D✝).length = 4

theorem Phenomena.WordOrder.Typology.japanese_ch90D : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90D.InternallyHeadedRelativeClauses) => x.value) (Core.WALS.F90D.lookup "jpn") = some Core.WALS.F90D.InternallyHeadedRelativeClauses.internallyHeadedOccursAsNondominantType

theorem Phenomena.WordOrder.Typology.korean_ch90D : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90D.InternallyHeadedRelativeClauses) => x.value) (Core.WALS.F90D.lookup "kor") = some Core.WALS.F90D.InternallyHeadedRelativeClauses.internallyHeadedOccursAsNondominantType

theorem Phenomena.WordOrder.Typology.tagalog_ch90D : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90D.InternallyHeadedRelativeClauses) => x.value) (Core.WALS.F90D.lookup "tag") = some Core.WALS.F90D.InternallyHeadedRelativeClauses.internallyHeadedOccursAsNondominantType

theorem Phenomena.WordOrder.Typology.ch90E_total : Phenomena.WordOrder.Typology.ch90E✝.length = 23

Ch 90E total: 23 languages.

theorem Phenomena.WordOrder.Typology.ch90E_count_correlativeRelativeClauseDominant : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90E.CorrelativeRelativeClauses) => x.value == Core.WALS.F90E.CorrelativeRelativeClauses.correlativeRelativeClauseDominant) Phenomena.WordOrder.Typology.ch90E✝).length = 7

theorem Phenomena.WordOrder.Typology.ch90E_count_correlativeOrReln : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90E.CorrelativeRelativeClauses) => x.value == Core.WALS.F90E.CorrelativeRelativeClauses.correlativeOrReln) Phenomena.WordOrder.Typology.ch90E✝).length = 7

theorem Phenomena.WordOrder.Typology.ch90E_count_correlativeOrNrel : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90E.CorrelativeRelativeClauses) => x.value == Core.WALS.F90E.CorrelativeRelativeClauses.correlativeOrNrel) Phenomena.WordOrder.Typology.ch90E✝).length = 2

theorem Phenomena.WordOrder.Typology.ch90E_count_correlativeOrInternallyHeaded : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90E.CorrelativeRelativeClauses) => x.value == Core.WALS.F90E.CorrelativeRelativeClauses.correlativeOrInternallyHeaded) Phenomena.WordOrder.Typology.ch90E✝).length = 1

theorem Phenomena.WordOrder.Typology.ch90E_count_correlativeOrAdjoined : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90E.CorrelativeRelativeClauses) => x.value == Core.WALS.F90E.CorrelativeRelativeClauses.correlativeOrAdjoined) Phenomena.WordOrder.Typology.ch90E✝).length = 2

theorem Phenomena.WordOrder.Typology.ch90E_count_correlativeAsNondominantType : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90E.CorrelativeRelativeClauses) => x.value == Core.WALS.F90E.CorrelativeRelativeClauses.correlativeAsNondominantType) Phenomena.WordOrder.Typology.ch90E✝).length = 3

theorem Phenomena.WordOrder.Typology.ch90E_count_correlativeExists : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90E.CorrelativeRelativeClauses) => x.value == Core.WALS.F90E.CorrelativeRelativeClauses.correlativeExists) Phenomena.WordOrder.Typology.ch90E✝).length = 1

theorem Phenomena.WordOrder.Typology.hindiUrdu_ch90E : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90E.CorrelativeRelativeClauses) => x.value) (Core.WALS.F90E.lookup "hin") = some Core.WALS.F90E.CorrelativeRelativeClauses.correlativeRelativeClauseDominant

theorem Phenomena.WordOrder.Typology.ch90F_total : Phenomena.WordOrder.Typology.ch90F✝.length = 10

Ch 90F total: 10 languages.

theorem Phenomena.WordOrder.Typology.ch90F_count_adjoinedRelativeClauseDominant : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90F.AdjoinedRelativeClauses) => x.value == Core.WALS.F90F.AdjoinedRelativeClauses.adjoinedRelativeClauseDominant) Phenomena.WordOrder.Typology.ch90F✝).length = 8

theorem Phenomena.WordOrder.Typology.ch90F_count_adjoinedOrCorrelative : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90F.AdjoinedRelativeClauses) => x.value == Core.WALS.F90F.AdjoinedRelativeClauses.adjoinedOrCorrelative) Phenomena.WordOrder.Typology.ch90F✝).length = 2

theorem Phenomena.WordOrder.Typology.warlpiri_ch90F : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F90F.AdjoinedRelativeClauses) => x.value) (Core.WALS.F90F.lookup "wrl") = some Core.WALS.F90F.AdjoinedRelativeClauses.adjoinedRelativeClauseDominant

theorem Phenomena.WordOrder.Typology.ch90G_total : Phenomena.WordOrder.Typology.ch90G✝.length = 5

Ch 90G total: 5 languages.

theorem Phenomena.WordOrder.Typology.ch90G_count_doubleHeadedDominant : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90G.DoubleHeadedRelativeClauses) => x.value == Core.WALS.F90G.DoubleHeadedRelativeClauses.doubleHeadedDominant) Phenomena.WordOrder.Typology.ch90G✝).length = 1

theorem Phenomena.WordOrder.Typology.ch90G_count_doubleHeadedOrReln : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90G.DoubleHeadedRelativeClauses) => x.value == Core.WALS.F90G.DoubleHeadedRelativeClauses.doubleHeadedOrReln) Phenomena.WordOrder.Typology.ch90G✝).length = 1

theorem Phenomena.WordOrder.Typology.ch90G_count_doubleHeadedOrInternallyHeaded : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90G.DoubleHeadedRelativeClauses) => x.value == Core.WALS.F90G.DoubleHeadedRelativeClauses.doubleHeadedOrInternallyHeaded) Phenomena.WordOrder.Typology.ch90G✝).length = 1

theorem Phenomena.WordOrder.Typology.ch90G_count_doubleHeadedAsNondominantType : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F90G.DoubleHeadedRelativeClauses) => x.value == Core.WALS.F90G.DoubleHeadedRelativeClauses.doubleHeadedAsNondominantType) Phenomena.WordOrder.Typology.ch90G✝).length = 2

theorem Phenomena.WordOrder.Typology.ch60_total : Phenomena.WordOrder.Typology.ch60✝.length = 138

Ch 60 total: 138 languages.

theorem Phenomena.WordOrder.Typology.ch60_count_weaklyDifferentiated : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses) => x.value == Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses.weaklyDifferentiated) Phenomena.WordOrder.Typology.ch60✝).length = 15

theorem Phenomena.WordOrder.Typology.ch60_count_genitivesAndAdjectivesCollapsed : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses) => x.value == Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses.genitivesAndAdjectivesCollapsed) Phenomena.WordOrder.Typology.ch60✝).length = 8

theorem Phenomena.WordOrder.Typology.ch60_count_genitivesAndRelativeClausesCollapsed : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses) => x.value == Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses.genitivesAndRelativeClausesCollapsed) Phenomena.WordOrder.Typology.ch60✝).length = 2

theorem Phenomena.WordOrder.Typology.ch60_count_adjectivesAndRelativeClausesCollapsed : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses) => x.value == Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses.adjectivesAndRelativeClausesCollapsed) Phenomena.WordOrder.Typology.ch60✝).length = 33

theorem Phenomena.WordOrder.Typology.ch60_count_moderatelyDifferentiatedInOtherWays : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses) => x.value == Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses.moderatelyDifferentiatedInOtherWays) Phenomena.WordOrder.Typology.ch60✝).length = 3

theorem Phenomena.WordOrder.Typology.ch60_count_highlyDifferentiated : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses) => x.value == Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses.highlyDifferentiated) Phenomena.WordOrder.Typology.ch60✝).length = 77

theorem Phenomena.WordOrder.Typology.ch60_highlyDifferentiated_majority : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses) => x.value == Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses.highlyDifferentiated) Phenomena.WordOrder.Typology.ch60✝).length > Phenomena.WordOrder.Typology.ch60✝¹.length / 2

theorem Phenomena.WordOrder.Typology.english_ch60 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses) => x.value) (Core.WALS.F60A.lookup "eng") = some Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses.highlyDifferentiated

theorem Phenomena.WordOrder.Typology.japanese_ch60 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses) => x.value) (Core.WALS.F60A.lookup "jpn") = some Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses.genitivesAndAdjectivesCollapsed

theorem Phenomena.WordOrder.Typology.turkish_ch60 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses) => x.value) (Core.WALS.F60A.lookup "tur") = some Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses.highlyDifferentiated

theorem Phenomena.WordOrder.Typology.hindiUrdu_ch60 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses) => x.value) (Core.WALS.F60A.lookup "hin") = some Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses.highlyDifferentiated

theorem Phenomena.WordOrder.Typology.korean_ch60 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses) => x.value) (Core.WALS.F60A.lookup "kor") = some Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses.highlyDifferentiated

theorem Phenomena.WordOrder.Typology.basque_ch60 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses) => x.value) (Core.WALS.F60A.lookup "bsq") = some Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses.highlyDifferentiated

theorem Phenomena.WordOrder.Typology.mandarin_ch60 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses) => x.value) (Core.WALS.F60A.lookup "mnd") = some Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses.weaklyDifferentiated

theorem Phenomena.WordOrder.Typology.russian_ch60 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses) => x.value) (Core.WALS.F60A.lookup "rus") = some Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses.highlyDifferentiated

theorem Phenomena.WordOrder.Typology.indonesian_ch60 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses) => x.value) (Core.WALS.F60A.lookup "ind") = some Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses.weaklyDifferentiated

theorem Phenomena.WordOrder.Typology.tagalog_ch60 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses) => x.value) (Core.WALS.F60A.lookup "tag") = some Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses.adjectivesAndRelativeClausesCollapsed

theorem Phenomena.WordOrder.Typology.malagasy_ch60 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses) => x.value) (Core.WALS.F60A.lookup "mal") = some Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses.adjectivesAndRelativeClausesCollapsed

theorem Phenomena.WordOrder.Typology.hungarian_ch60 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses) => x.value) (Core.WALS.F60A.lookup "hun") = some Core.WALS.F60A.GenitivesAdjectivesAndRelativeClauses.highlyDifferentiated

theorem Phenomena.WordOrder.Typology.ch61_total : Phenomena.WordOrder.Typology.ch61✝.length = 124

Ch 61 total: 124 languages.

theorem Phenomena.WordOrder.Typology.ch61_count_notWithoutNoun : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F61A.AdjectivesWithoutNouns) => x.value == Core.WALS.F61A.AdjectivesWithoutNouns.notWithoutNoun) Phenomena.WordOrder.Typology.ch61✝).length = 1

theorem Phenomena.WordOrder.Typology.ch61_count_withoutMarking : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F61A.AdjectivesWithoutNouns) => x.value == Core.WALS.F61A.AdjectivesWithoutNouns.withoutMarking) Phenomena.WordOrder.Typology.ch61✝).length = 73

theorem Phenomena.WordOrder.Typology.ch61_count_markedByPrefix : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F61A.AdjectivesWithoutNouns) => x.value == Core.WALS.F61A.AdjectivesWithoutNouns.markedByPrefix) Phenomena.WordOrder.Typology.ch61✝).length = 7

theorem Phenomena.WordOrder.Typology.ch61_count_markedBySuffix : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F61A.AdjectivesWithoutNouns) => x.value == Core.WALS.F61A.AdjectivesWithoutNouns.markedBySuffix) Phenomena.WordOrder.Typology.ch61✝).length = 13

theorem Phenomena.WordOrder.Typology.ch61_count_markedByPrecedingWord : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F61A.AdjectivesWithoutNouns) => x.value == Core.WALS.F61A.AdjectivesWithoutNouns.markedByPrecedingWord) Phenomena.WordOrder.Typology.ch61✝).length = 18

theorem Phenomena.WordOrder.Typology.ch61_count_markedByFollowingWord : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F61A.AdjectivesWithoutNouns) => x.value == Core.WALS.F61A.AdjectivesWithoutNouns.markedByFollowingWord) Phenomena.WordOrder.Typology.ch61✝).length = 7

theorem Phenomena.WordOrder.Typology.ch61_count_markedByMixedOrOtherStrategies : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F61A.AdjectivesWithoutNouns) => x.value == Core.WALS.F61A.AdjectivesWithoutNouns.markedByMixedOrOtherStrategies) Phenomena.WordOrder.Typology.ch61✝).length = 5

theorem Phenomena.WordOrder.Typology.ch61_withoutMarking_majority : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F61A.AdjectivesWithoutNouns) => x.value == Core.WALS.F61A.AdjectivesWithoutNouns.withoutMarking) Phenomena.WordOrder.Typology.ch61✝).length > Phenomena.WordOrder.Typology.ch61✝¹.length / 2

theorem Phenomena.WordOrder.Typology.english_ch61 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F61A.AdjectivesWithoutNouns) => x.value) (Core.WALS.F61A.lookup "eng") = some Core.WALS.F61A.AdjectivesWithoutNouns.markedByFollowingWord

theorem Phenomena.WordOrder.Typology.japanese_ch61 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F61A.AdjectivesWithoutNouns) => x.value) (Core.WALS.F61A.lookup "jpn") = some Core.WALS.F61A.AdjectivesWithoutNouns.markedByMixedOrOtherStrategies

theorem Phenomena.WordOrder.Typology.turkish_ch61 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F61A.AdjectivesWithoutNouns) => x.value) (Core.WALS.F61A.lookup "tur") = some Core.WALS.F61A.AdjectivesWithoutNouns.withoutMarking

theorem Phenomena.WordOrder.Typology.hindiUrdu_ch61 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F61A.AdjectivesWithoutNouns) => x.value) (Core.WALS.F61A.lookup "hin") = some Core.WALS.F61A.AdjectivesWithoutNouns.markedByFollowingWord

theorem Phenomena.WordOrder.Typology.korean_ch61 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F61A.AdjectivesWithoutNouns) => x.value) (Core.WALS.F61A.lookup "kor") = some Core.WALS.F61A.AdjectivesWithoutNouns.markedByFollowingWord

theorem Phenomena.WordOrder.Typology.basque_ch61 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F61A.AdjectivesWithoutNouns) => x.value) (Core.WALS.F61A.lookup "bsq") = some Core.WALS.F61A.AdjectivesWithoutNouns.withoutMarking

theorem Phenomena.WordOrder.Typology.mandarin_ch61 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F61A.AdjectivesWithoutNouns) => x.value) (Core.WALS.F61A.lookup "mnd") = some Core.WALS.F61A.AdjectivesWithoutNouns.markedByFollowingWord

theorem Phenomena.WordOrder.Typology.russian_ch61 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F61A.AdjectivesWithoutNouns) => x.value) (Core.WALS.F61A.lookup "rus") = some Core.WALS.F61A.AdjectivesWithoutNouns.withoutMarking

theorem Phenomena.WordOrder.Typology.swahili_ch61 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F61A.AdjectivesWithoutNouns) => x.value) (Core.WALS.F61A.lookup "swa") = some Core.WALS.F61A.AdjectivesWithoutNouns.withoutMarking

theorem Phenomena.WordOrder.Typology.indonesian_ch61 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F61A.AdjectivesWithoutNouns) => x.value) (Core.WALS.F61A.lookup "ind") = some Core.WALS.F61A.AdjectivesWithoutNouns.markedByPrecedingWord

theorem Phenomena.WordOrder.Typology.irish_ch61 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F61A.AdjectivesWithoutNouns) => x.value) (Core.WALS.F61A.lookup "iri") = some Core.WALS.F61A.AdjectivesWithoutNouns.markedByPrecedingWord

theorem Phenomena.WordOrder.Typology.tagalog_ch61 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F61A.AdjectivesWithoutNouns) => x.value) (Core.WALS.F61A.lookup "tag") = some Core.WALS.F61A.AdjectivesWithoutNouns.withoutMarking

theorem Phenomena.WordOrder.Typology.malagasy_ch61 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F61A.AdjectivesWithoutNouns) => x.value) (Core.WALS.F61A.lookup "mal") = some Core.WALS.F61A.AdjectivesWithoutNouns.markedByPrecedingWord

theorem Phenomena.WordOrder.Typology.hungarian_ch61 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F61A.AdjectivesWithoutNouns) => x.value) (Core.WALS.F61A.lookup "hun") = some Core.WALS.F61A.AdjectivesWithoutNouns.withoutMarking