Morphological Typology: Paradigm Complexity

@cite{ackerman-malouf-2013}

Cross-linguistic typological data on morphological paradigm complexity.

LanguageData

LanguageData records summary statistics about a language's inflectional paradigm system: the number of inflection classes (E-complexity), the number of paradigm cells, and information-theoretic measures of paradigm predictability (I-complexity).

@cite{ackerman-malouf-2013} Sample

Ten typologically diverse languages from @cite{ackerman-malouf-2013}, spanning three phyla, four macro-areas, and a range from 2 to 109 inflection classes. The central empirical finding: despite wildly varying E-complexity, I-complexity (average conditional entropy) is uniformly low across all ten languages.

MorphProfile Sample

Eighteen typologically diverse languages with morphological profiles derived from WALS data. Types and WALS lookup helpers are defined in Core.Morphology.MorphProfile; per-language profiles live in Fragments.{Language}.Morph.

structure Phenomena.Morphology.Typology.LanguageData : Type

Summary statistics for a language's morphological paradigm system, as reported in published studies.

Fields correspond to Tables 2--3 of @cite{ackerman-malouf-2013}.

• name : String

  Language name

• family : String

  Language family

• numClasses : ℕ

  Number of inflection classes (E-complexity)

• numCells : ℕ

  Number of paradigm cells

• avgCondEntropy : ℚ

  Average conditional entropy H(Ci|Cj) in bits (I-complexity)

• maxCellEntropy : ℚ

  Maximum cell entropy max H(Ci) in bits

instance Phenomena.Morphology.Typology.instReprLanguageData : Repr LanguageData

Equations

• Phenomena.Morphology.Typology.instReprLanguageData = { reprPrec := Phenomena.Morphology.Typology.instReprLanguageData.repr }

def Phenomena.Morphology.Typology.instReprLanguageData.repr : LanguageData → ℕ → Std.Format

Equations

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

Nilo-Saharan languages

def Phenomena.Morphology.Typology.fur : LanguageData

Fur (Nilo-Saharan, Fur; Sudan). 4 classes, 2 cells.

Equations

• Phenomena.Morphology.Typology.fur = { name := "Fur", family := "Nilo-Saharan", numClasses := 4, numCells := 2, avgCondEntropy := 489 / 1000, maxCellEntropy := 1334 / 1000 }

def Phenomena.Morphology.Typology.ngiti : LanguageData

Ngiti (Nilo-Saharan, Central Sudanic; DRC). 8 classes, 2 cells.

Equations

• Phenomena.Morphology.Typology.ngiti = { name := "Ngiti", family := "Nilo-Saharan", numClasses := 8, numCells := 2, avgCondEntropy := 380 / 1000, maxCellEntropy := 1741 / 1000 }

def Phenomena.Morphology.Typology.nuer : LanguageData

Nuer (Nilo-Saharan, Nilotic; Sudan/South Sudan). 31 classes, 4 cells.

Equations

• Phenomena.Morphology.Typology.nuer = { name := "Nuer", family := "Nilo-Saharan", numClasses := 31, numCells := 4, avgCondEntropy := 513 / 1000, maxCellEntropy := 3224 / 1000 }

Trans-New Guinea languages

def Phenomena.Morphology.Typology.kwerba : LanguageData

Kwerba (Trans-New Guinea; Papua, Indonesia). 2 classes, 2 cells.

Equations

• Phenomena.Morphology.Typology.kwerba = { name := "Kwerba", family := "Trans-New Guinea", numClasses := 2, numCells := 2, avgCondEntropy := 469 / 1000, maxCellEntropy := 529 / 1000 }

Oto-Manguean languages

def Phenomena.Morphology.Typology.chinantec : LanguageData

Chinantec (Oto-Manguean; Oaxaca, Mexico). 62 classes, 4 cells. Comaltepec Chinantec tonal verb paradigms.

Equations

• Phenomena.Morphology.Typology.chinantec = { name := "Chinantec", family := "Oto-Manguean", numClasses := 62, numCells := 4, avgCondEntropy := 426 / 1000, maxCellEntropy := 4266 / 1000 }

def Phenomena.Morphology.Typology.mazatec : LanguageData

Chiquihuitlan Mazatec (Oto-Manguean; Oaxaca, Mexico). 109 classes, 4 cells. The paper's primary case study (section 4).

Equations

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

Uralic languages

def Phenomena.Morphology.Typology.finnish : LanguageData

Finnish (Uralic, Finnic). 51 classes, 8 cells.

Equations

• Phenomena.Morphology.Typology.finnish = { name := "Finnish", family := "Uralic", numClasses := 51, numCells := 8, avgCondEntropy := 209 / 1000, maxCellEntropy := 3803 / 1000 }

Indo-European languages

def Phenomena.Morphology.Typology.german : LanguageData

German (Indo-European, Germanic). 7 classes, 8 cells.

Equations

• Phenomena.Morphology.Typology.german = { name := "German", family := "Indo-European", numClasses := 7, numCells := 8, avgCondEntropy := 45 / 1000, maxCellEntropy := 1906 / 1000 }

def Phenomena.Morphology.Typology.russian : LanguageData

Russian (Indo-European, Slavic). 8 classes, 8 cells.

Equations

• Phenomena.Morphology.Typology.russian = { name := "Russian", family := "Indo-European", numClasses := 8, numCells := 8, avgCondEntropy := 89 / 1000, maxCellEntropy := 2170 / 1000 }

def Phenomena.Morphology.Typology.spanish : LanguageData

Spanish (Indo-European, Romance). 3 classes, 57 cells.

Equations

• Phenomena.Morphology.Typology.spanish = { name := "Spanish", family := "Indo-European", numClasses := 3, numCells := 57, avgCondEntropy := 3 / 1000, maxCellEntropy := 1522 / 1000 }

def Phenomena.Morphology.Typology.ackermanMalouf2013 : List LanguageData

All 10 languages in the @cite{ackerman-malouf-2013} sample (Table 3).

Equations

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

def Phenomena.Morphology.Typology.lcecThreshold : ℚ

The LCEC threshold: all 10 languages fall below 1 bit of average conditional entropy. Even the most complex system (Mazatec, 109 classes) has I-complexity < 1 bit.

Equations

• Phenomena.Morphology.Typology.lcecThreshold = 1

def Phenomena.Morphology.Typology.mazatecRandomBaseline : ℚ

Expected I-complexity under random class assignment for Mazatec (Monte Carlo baseline). The paper reports the mean of 1000 random permutations as ~5.25 bits, far above the observed 0.709 bits.

Equations

• Phenomena.Morphology.Typology.mazatecRandomBaseline = 525 / 100

Morphological Mechanisms: WALS Chapters 20--29

Chapters 20--29 of WALS cover the fundamental mechanisms of inflectional morphology: how formatives are put together (fusion), how many categories a single formative expresses (exponence), how synthetic verb morphology is (inflectional synthesis), where grammatical relations are marked (locus of marking), whether affixes go before or after stems (prefixing vs suffixing), and whether the language has productive reduplication.

Typological classification types are defined in Core.Morphology.MorphProfile.

Sources: @cite{bickel-nichols-2013a} (Ch 20, Fusion) @cite{bickel-nichols-2013b} (Ch 21, Exponence) @cite{bickel-nichols-2013c} (Ch 22, Inflectional Synthesis) @cite{nichols-bickel-2013b} (Ch 23, Locus of Marking in the Clause) @cite{nichols-bickel-2013c} (Ch 24, Locus of Marking in Possessive NPs) @cite{nichols-bickel-2013a} (Ch 25, Locus of Marking: Whole-language Typology) @cite{nichols-bickel-2013d} (Ch 25B, Zero Marking of A and P Arguments) @cite{baerman-brown-2013} (Ch 28, Case Syncretism) @cite{baerman-brown-2013a} (Ch 29, Syncretism in Verbal Person/Number Marking) @cite{dryer-2013-wals} (Ch 26, Prefixing vs. Suffixing) @cite{rubino-2013} (Ch 27, Reduplication)

def Phenomena.Morphology.Typology.toFusion : Core.WALS.F20A.FusionType → Core.Morphology.Fusion

Map WALS 20A fine-grained fusion types to coarse categories. Mixed types are mapped by their non-concatenative component.

Equations

• Phenomena.Morphology.Typology.toFusion Core.WALS.F20A.FusionType.exclusivelyConcatenative = Core.Morphology.Fusion.concatenative
• Phenomena.Morphology.Typology.toFusion Core.WALS.F20A.FusionType.exclusivelyIsolating = Core.Morphology.Fusion.isolating
• Phenomena.Morphology.Typology.toFusion Core.WALS.F20A.FusionType.exclusivelyTonal = Core.Morphology.Fusion.nonlinear
• Phenomena.Morphology.Typology.toFusion Core.WALS.F20A.FusionType.tonalIsolating = Core.Morphology.Fusion.nonlinear
• Phenomena.Morphology.Typology.toFusion Core.WALS.F20A.FusionType.tonalConcatenative = Core.Morphology.Fusion.nonlinear
• Phenomena.Morphology.Typology.toFusion Core.WALS.F20A.FusionType.ablautConcatenative = Core.Morphology.Fusion.nonlinear
• Phenomena.Morphology.Typology.toFusion Core.WALS.F20A.FusionType.isolatingConcatenative = Core.Morphology.Fusion.concatenative

theorem Phenomena.Morphology.Typology.vietnamese_isolating : Core.WALS.F20A.lookup "vie" = some { walsCode := "vie", language := "Vietnamese", iso := "vie", value := Core.WALS.F20A.FusionType.exclusivelyIsolating }

theorem Phenomena.Morphology.Typology.indonesian_isolating : Core.WALS.F20A.lookup "ind" = some { walsCode := "ind", language := "Indonesian", iso := "ind", value := Core.WALS.F20A.FusionType.exclusivelyIsolating }

theorem Phenomena.Morphology.Typology.turkish_concatenative : Core.WALS.F20A.lookup "tur" = some { walsCode := "tur", language := "Turkish", iso := "tur", value := Core.WALS.F20A.FusionType.exclusivelyConcatenative }

theorem Phenomena.Morphology.Typology.finnish_concatenative : Core.WALS.F20A.lookup "fin" = some { walsCode := "fin", language := "Finnish", iso := "fin", value := Core.WALS.F20A.FusionType.exclusivelyConcatenative }

theorem Phenomena.Morphology.Typology.swahili_concatenative : Core.WALS.F20A.lookup "swa" = some { walsCode := "swa", language := "Swahili", iso := "swh", value := Core.WALS.F20A.FusionType.exclusivelyConcatenative }

theorem Phenomena.Morphology.Typology.arabic_ablaut : Core.WALS.F20A.lookup "aeg" = some { walsCode := "aeg", language := "Arabic (Egyptian)", iso := "arz", value := Core.WALS.F20A.FusionType.ablautConcatenative }

theorem Phenomena.Morphology.Typology.hebrew_ablaut : Core.WALS.F20A.lookup "heb" = some { walsCode := "heb", language := "Hebrew (Modern)", iso := "heb", value := Core.WALS.F20A.FusionType.ablautConcatenative }

theorem Phenomena.Morphology.Typology.russian_concatenative : Core.WALS.F20A.lookup "rus" = some { walsCode := "rus", language := "Russian", iso := "rus", value := Core.WALS.F20A.FusionType.exclusivelyConcatenative }

theorem Phenomena.Morphology.Typology.german_concatenative : Core.WALS.F20A.lookup "ger" = some { walsCode := "ger", language := "German", iso := "deu", value := Core.WALS.F20A.FusionType.exclusivelyConcatenative }

theorem Phenomena.Morphology.Typology.mandarin_isoConcatenative : Core.WALS.F20A.lookup "mnd" = some { walsCode := "mnd", language := "Mandarin", iso := "cmn", value := Core.WALS.F20A.FusionType.isolatingConcatenative }

theorem Phenomena.Morphology.Typology.thai_isoConcatenative : Core.WALS.F20A.lookup "tha" = some { walsCode := "tha", language := "Thai", iso := "tha", value := Core.WALS.F20A.FusionType.isolatingConcatenative }

structure Phenomena.Morphology.Typology.WALSCount : Type

A single row in a WALS distribution table: a label and a language count.

• label : String
• count : ℕ

instance Phenomena.Morphology.Typology.instReprWALSCount : Repr WALSCount

Equations

• Phenomena.Morphology.Typology.instReprWALSCount = { reprPrec := Phenomena.Morphology.Typology.instReprWALSCount.repr }

def Phenomena.Morphology.Typology.instReprWALSCount.repr : WALSCount → ℕ → Std.Format

Equations

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

def Phenomena.Morphology.Typology.instDecidableEqWALSCount.decEq (x✝ x✝¹ : WALSCount) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Morphology.Typology.instDecidableEqWALSCount : DecidableEq WALSCount

Equations

• Phenomena.Morphology.Typology.instDecidableEqWALSCount = Phenomena.Morphology.Typology.instDecidableEqWALSCount.decEq

def Phenomena.Morphology.Typology.instBEqWALSCount.beq : WALSCount → WALSCount → Bool

Equations

• Phenomena.Morphology.Typology.instBEqWALSCount.beq { label := a, count := a_1 } { label := b, count := b_1 } = (a == b && a_1 == b_1)
• Phenomena.Morphology.Typology.instBEqWALSCount.beq x✝¹ x✝ = false

instance Phenomena.Morphology.Typology.instBEqWALSCount : BEq WALSCount

Equations

• Phenomena.Morphology.Typology.instBEqWALSCount = { beq := Phenomena.Morphology.Typology.instBEqWALSCount.beq }

def Phenomena.Morphology.Typology.ch20Distribution : List WALSCount

WALS Chapter 20 distribution, derived from F20A data (@cite{bickel-nichols-2013a}).

Equations

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

theorem Phenomena.Morphology.Typology.ch20_total : List.foldl (fun (acc : ℕ) (c : WALSCount) => acc + c.count) 0 ch20Distribution = 165

Ch 20 total: 165 languages (derived from F20A data).

def Phenomena.Morphology.Typology.toExponence : Core.WALS.F21A.ExponenceType → Core.Morphology.Exponence

Map WALS 21A fine-grained exponence types to coarse categories. All polyexponential subtypes (case+number, case+referentiality, case+TAM) map to .polyexponential.

Equations

• Phenomena.Morphology.Typology.toExponence Core.WALS.F21A.ExponenceType.monoexponentialCase = Core.Morphology.Exponence.monoexponential
• Phenomena.Morphology.Typology.toExponence Core.WALS.F21A.ExponenceType.caseNumber = Core.Morphology.Exponence.polyexponential
• Phenomena.Morphology.Typology.toExponence Core.WALS.F21A.ExponenceType.caseReferentiality = Core.Morphology.Exponence.polyexponential
• Phenomena.Morphology.Typology.toExponence Core.WALS.F21A.ExponenceType.caseTam = Core.Morphology.Exponence.polyexponential
• Phenomena.Morphology.Typology.toExponence Core.WALS.F21A.ExponenceType.noCase = Core.Morphology.Exponence.noCase

theorem Phenomena.Morphology.Typology.turkish_monoexp : Core.WALS.F21A.lookup "tur" = some { walsCode := "tur", language := "Turkish", iso := "tur", value := Core.WALS.F21A.ExponenceType.monoexponentialCase }

theorem Phenomena.Morphology.Typology.finnish_caseNumber : Core.WALS.F21A.lookup "fin" = some { walsCode := "fin", language := "Finnish", iso := "fin", value := Core.WALS.F21A.ExponenceType.caseNumber }

theorem Phenomena.Morphology.Typology.german_caseNumber : Core.WALS.F21A.lookup "ger" = some { walsCode := "ger", language := "German", iso := "deu", value := Core.WALS.F21A.ExponenceType.caseNumber }

theorem Phenomena.Morphology.Typology.russian_caseNumber : Core.WALS.F21A.lookup "rus" = some { walsCode := "rus", language := "Russian", iso := "rus", value := Core.WALS.F21A.ExponenceType.caseNumber }

theorem Phenomena.Morphology.Typology.english_noCase : Core.WALS.F21A.lookup "eng" = some { walsCode := "eng", language := "English", iso := "eng", value := Core.WALS.F21A.ExponenceType.noCase }

theorem Phenomena.Morphology.Typology.kayardild_caseTam : Core.WALS.F21A.lookup "kay" = some { walsCode := "kay", language := "Kayardild", iso := "gyd", value := Core.WALS.F21A.ExponenceType.caseTam }

def Phenomena.Morphology.Typology.ch21Distribution : List WALSCount

WALS Chapter 21 distribution, derived from F21A data (@cite{bickel-nichols-2013b}).

Equations

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

theorem Phenomena.Morphology.Typology.ch21_total : List.foldl (fun (acc : ℕ) (c : WALSCount) => acc + c.count) 0 ch21Distribution = 162

Ch 21 total: 162 languages (derived from F21A data).

def Phenomena.Morphology.Typology.toVerbSynthesis : Core.WALS.F22A.InflectionalSynthesis → Core.Morphology.VerbSynthesis

Map WALS 22A fine-grained categories to coarse synthesis levels. Boundaries align with WALS bin edges to avoid splitting categories.

Equations

• Phenomena.Morphology.Typology.toVerbSynthesis Core.WALS.F22A.InflectionalSynthesis.categoryPerWord0_1 = Core.Morphology.VerbSynthesis.low
• Phenomena.Morphology.Typology.toVerbSynthesis Core.WALS.F22A.InflectionalSynthesis.categoriesPerWord2_3 = Core.Morphology.VerbSynthesis.low
• Phenomena.Morphology.Typology.toVerbSynthesis Core.WALS.F22A.InflectionalSynthesis.categoriesPerWord4_5 = Core.Morphology.VerbSynthesis.moderate
• Phenomena.Morphology.Typology.toVerbSynthesis Core.WALS.F22A.InflectionalSynthesis.categoriesPerWord6_7 = Core.Morphology.VerbSynthesis.moderate
• Phenomena.Morphology.Typology.toVerbSynthesis Core.WALS.F22A.InflectionalSynthesis.categoriesPerWord8_9 = Core.Morphology.VerbSynthesis.high
• Phenomena.Morphology.Typology.toVerbSynthesis Core.WALS.F22A.InflectionalSynthesis.categoriesPerWord10_11 = Core.Morphology.VerbSynthesis.high
• Phenomena.Morphology.Typology.toVerbSynthesis Core.WALS.F22A.InflectionalSynthesis.categoriesPerWord12_13 = Core.Morphology.VerbSynthesis.high

theorem Phenomena.Morphology.Typology.mandarin_0_1 : Core.WALS.F22A.lookup "mnd" = some { walsCode := "mnd", language := "Mandarin", iso := "cmn", value := Core.WALS.F22A.InflectionalSynthesis.categoryPerWord0_1 }

theorem Phenomena.Morphology.Typology.english_2_3 : Core.WALS.F22A.lookup "eng" = some { walsCode := "eng", language := "English", iso := "eng", value := Core.WALS.F22A.InflectionalSynthesis.categoriesPerWord2_3 }

theorem Phenomena.Morphology.Typology.thai_2_3 : Core.WALS.F22A.lookup "tha" = some { walsCode := "tha", language := "Thai", iso := "tha", value := Core.WALS.F22A.InflectionalSynthesis.categoriesPerWord2_3 }

theorem Phenomena.Morphology.Typology.spanish_4_5 : Core.WALS.F22A.lookup "spa" = some { walsCode := "spa", language := "Spanish", iso := "spa", value := Core.WALS.F22A.InflectionalSynthesis.categoriesPerWord4_5 }

theorem Phenomena.Morphology.Typology.russian_4_5 : Core.WALS.F22A.lookup "rus" = some { walsCode := "rus", language := "Russian", iso := "rus", value := Core.WALS.F22A.InflectionalSynthesis.categoriesPerWord4_5 }

theorem Phenomena.Morphology.Typology.swahili_4_5 : Core.WALS.F22A.lookup "swa" = some { walsCode := "swa", language := "Swahili", iso := "swh", value := Core.WALS.F22A.InflectionalSynthesis.categoriesPerWord4_5 }

theorem Phenomena.Morphology.Typology.georgian_8_9 : Core.WALS.F22A.lookup "geo" = some { walsCode := "geo", language := "Georgian", iso := "kat", value := Core.WALS.F22A.InflectionalSynthesis.categoriesPerWord8_9 }

theorem Phenomena.Morphology.Typology.abkhaz_10_11 : Core.WALS.F22A.lookup "abk" = some { walsCode := "abk", language := "Abkhaz", iso := "abk", value := Core.WALS.F22A.InflectionalSynthesis.categoriesPerWord10_11 }

def Phenomena.Morphology.Typology.ch22Distribution : List WALSCount

WALS Chapter 22 distribution, derived from F22A data (@cite{bickel-nichols-2013c}).

Equations

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

theorem Phenomena.Morphology.Typology.ch22_total : List.foldl (fun (acc : ℕ) (c : WALSCount) => acc + c.count) 0 ch22Distribution = 145

Ch 22 total: 145 languages (derived from F22A data).

def Phenomena.Morphology.Typology.toLocusOfMarking : Core.WALS.F25A.LocusOfMarkingWholeLanguageTypology → Core.Morphology.LocusOfMarking

Map WALS 25A values to the 5-way LocusOfMarking classification.

Equations

• Phenomena.Morphology.Typology.toLocusOfMarking Core.WALS.F25A.LocusOfMarkingWholeLanguageTypology.headMarking = Core.Morphology.LocusOfMarking.headMarking
• Phenomena.Morphology.Typology.toLocusOfMarking Core.WALS.F25A.LocusOfMarkingWholeLanguageTypology.dependentMarking = Core.Morphology.LocusOfMarking.dependentMarking
• Phenomena.Morphology.Typology.toLocusOfMarking Core.WALS.F25A.LocusOfMarkingWholeLanguageTypology.doubleMarking = Core.Morphology.LocusOfMarking.doubleMarking
• Phenomena.Morphology.Typology.toLocusOfMarking Core.WALS.F25A.LocusOfMarkingWholeLanguageTypology.zeroMarking = Core.Morphology.LocusOfMarking.zeroMarking
• Phenomena.Morphology.Typology.toLocusOfMarking Core.WALS.F25A.LocusOfMarkingWholeLanguageTypology.inconsistentOrOther = Core.Morphology.LocusOfMarking.inconsistentOrOther

theorem Phenomena.Morphology.Typology.turkish_strongSuffix : Core.WALS.F26A.lookup "tur" = some { walsCode := "tur", language := "Turkish", iso := "tur", value := Core.WALS.F26A.PrefixSuffixPreference.stronglySuffixing }

theorem Phenomena.Morphology.Typology.japanese_strongSuffix : Core.WALS.F26A.lookup "jpn" = some { walsCode := "jpn", language := "Japanese", iso := "jpn", value := Core.WALS.F26A.PrefixSuffixPreference.stronglySuffixing }

theorem Phenomena.Morphology.Typology.russian_strongSuffix : Core.WALS.F26A.lookup "rus" = some { walsCode := "rus", language := "Russian", iso := "rus", value := Core.WALS.F26A.PrefixSuffixPreference.stronglySuffixing }

theorem Phenomena.Morphology.Typology.german_strongSuffix : Core.WALS.F26A.lookup "ger" = some { walsCode := "ger", language := "German", iso := "deu", value := Core.WALS.F26A.PrefixSuffixPreference.stronglySuffixing }

theorem Phenomena.Morphology.Typology.arabic_eg_weakSuffix : Core.WALS.F26A.lookup "aeg" = some { walsCode := "aeg", language := "Arabic (Egyptian)", iso := "arz", value := Core.WALS.F26A.PrefixSuffixPreference.weaklySuffixing }

theorem Phenomena.Morphology.Typology.swahili_weakPrefix : Core.WALS.F26A.lookup "swa" = some { walsCode := "swa", language := "Swahili", iso := "swh", value := Core.WALS.F26A.PrefixSuffixPreference.weaklyPrefixing }

theorem Phenomena.Morphology.Typology.navajo_strongPrefix : Core.WALS.F26A.lookup "nav" = some { walsCode := "nav", language := "Navajo", iso := "nav", value := Core.WALS.F26A.PrefixSuffixPreference.strongPrefixing }

theorem Phenomena.Morphology.Typology.thai_littleAffix : Core.WALS.F26A.lookup "tha" = some { walsCode := "tha", language := "Thai", iso := "tha", value := Core.WALS.F26A.PrefixSuffixPreference.littleAffixation }

theorem Phenomena.Morphology.Typology.tagalog_littleAffix : Core.WALS.F26A.lookup "tag" = some { walsCode := "tag", language := "Tagalog", iso := "tgl", value := Core.WALS.F26A.PrefixSuffixPreference.littleAffixation }

theorem Phenomena.Morphology.Typology.vietnamese_littleAffix : Core.WALS.F26A.lookup "vie" = some { walsCode := "vie", language := "Vietnamese", iso := "vie", value := Core.WALS.F26A.PrefixSuffixPreference.littleAffixation }

theorem Phenomena.Morphology.Typology.mandarin_strongSuffix : Core.WALS.F26A.lookup "mnd" = some { walsCode := "mnd", language := "Mandarin", iso := "cmn", value := Core.WALS.F26A.PrefixSuffixPreference.stronglySuffixing }

def Phenomena.Morphology.Typology.ch26Distribution : List WALSCount

WALS Chapter 26 distribution, derived from F26A data (@cite{dryer-haspelmath-2013}).

Equations

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

theorem Phenomena.Morphology.Typology.ch26_total : List.foldl (fun (acc : ℕ) (c : WALSCount) => acc + c.count) 0 ch26Distribution = 969

Ch 26 total: 969 languages (derived from F26A data).

theorem Phenomena.Morphology.Typology.tagalog_fullPartial : Core.WALS.F27A.lookup "tag" = some { walsCode := "tag", language := "Tagalog", iso := "tgl", value := Core.WALS.F27A.ReduplicationType.productiveFullAndPartialReduplication }

theorem Phenomena.Morphology.Typology.swahili_fullPartial : Core.WALS.F27A.lookup "swa" = some { walsCode := "swa", language := "Swahili", iso := "swh", value := Core.WALS.F27A.ReduplicationType.productiveFullAndPartialReduplication }

theorem Phenomena.Morphology.Typology.indonesian_fullOnly : Core.WALS.F27A.lookup "ind" = some { walsCode := "ind", language := "Indonesian", iso := "ind", value := Core.WALS.F27A.ReduplicationType.fullReduplicationOnly }

theorem Phenomena.Morphology.Typology.english_noRedup : Core.WALS.F27A.lookup "eng" = some { walsCode := "eng", language := "English", iso := "eng", value := Core.WALS.F27A.ReduplicationType.noProductiveReduplication }

theorem Phenomena.Morphology.Typology.arabic_eg_fullPartial : Core.WALS.F27A.lookup "aeg" = some { walsCode := "aeg", language := "Arabic (Egyptian)", iso := "arz", value := Core.WALS.F27A.ReduplicationType.productiveFullAndPartialReduplication }

def Phenomena.Morphology.Typology.ch27Distribution : List WALSCount

WALS Chapter 27 distribution, derived from F27A data (@cite{rubino-2013}).

Equations

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

theorem Phenomena.Morphology.Typology.ch27_total : List.foldl (fun (acc : ℕ) (c : WALSCount) => acc + c.count) 0 ch27Distribution = 368

Ch 27 total: 368 languages (derived from F27A data).

def Phenomena.Morphology.Typology.ch23Distribution : List WALSCount

WALS Chapter 23 distribution, derived from F23A data (N = 236).

Equations

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

theorem Phenomena.Morphology.Typology.ch23_total : List.foldl (fun (acc : ℕ) (c : WALSCount) => acc + c.count) 0 ch23Distribution = 236

Ch 23 total: 236 languages (derived from F23A data).

def Phenomena.Morphology.Typology.ch24Distribution : List WALSCount

WALS Chapter 24 distribution, derived from F24A data (N = 236).

Equations

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

theorem Phenomena.Morphology.Typology.ch24_total : List.foldl (fun (acc : ℕ) (c : WALSCount) => acc + c.count) 0 ch24Distribution = 236

Ch 24 total: 236 languages (derived from F24A data).

def Phenomena.Morphology.Typology.ch25aDistribution : List WALSCount

WALS Chapter 25A distribution, derived from F25A data (N = 236).

Equations

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

theorem Phenomena.Morphology.Typology.ch25a_total : List.foldl (fun (acc : ℕ) (c : WALSCount) => acc + c.count) 0 ch25aDistribution = 236

Ch 25A total: 236 languages (derived from F25A data).

def Phenomena.Morphology.Typology.ch25bDistribution : List WALSCount

WALS Chapter 25B distribution, derived from F25B data (N = 235).

Equations

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

theorem Phenomena.Morphology.Typology.ch25b_total : List.foldl (fun (acc : ℕ) (c : WALSCount) => acc + c.count) 0 ch25bDistribution = 235

Ch 25B total: 235 languages (derived from F25B data).

def Phenomena.Morphology.Typology.ch28Distribution : List WALSCount

WALS Chapter 28 distribution, derived from F28A data (N = 198).

Equations

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

theorem Phenomena.Morphology.Typology.ch28_total : List.foldl (fun (acc : ℕ) (c : WALSCount) => acc + c.count) 0 ch28Distribution = 198

Ch 28 total: 198 languages (derived from F28A data).

def Phenomena.Morphology.Typology.ch29Distribution : List WALSCount

WALS Chapter 29 distribution, derived from F29A data (N = 198).

Equations

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

theorem Phenomena.Morphology.Typology.ch29_total : List.foldl (fun (acc : ℕ) (c : WALSCount) => acc + c.count) 0 ch29Distribution = 198

Ch 29 total: 198 languages (derived from F29A data).

def Phenomena.Morphology.Typology.ch21bDistribution : List WALSCount

WALS Chapter 21B distribution, derived from F21B data (N = 160).

Equations

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

theorem Phenomena.Morphology.Typology.ch21b_total : List.foldl (fun (acc : ℕ) (c : WALSCount) => acc + c.count) 0 ch21bDistribution = 160

Ch 21B total: 160 languages (derived from F21B data).

def Phenomena.Morphology.Typology.ch62Distribution : List WALSCount

WALS Chapter 62A distribution, derived from F62A data (N = 168).

Equations

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

theorem Phenomena.Morphology.Typology.ch62_total : List.foldl (fun (acc : ℕ) (c : WALSCount) => acc + c.count) 0 ch62Distribution = 168

Ch 62 total: 168 languages (derived from F62A data).

def Phenomena.Morphology.Typology.ch79aDistribution : List WALSCount

WALS Chapter 79A distribution, derived from F79A data (N = 193).

Equations

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

theorem Phenomena.Morphology.Typology.ch79a_total : List.foldl (fun (acc : ℕ) (c : WALSCount) => acc + c.count) 0 ch79aDistribution = 193

Ch 79A total: 193 languages (derived from F79A data).

def Phenomena.Morphology.Typology.ch79bDistribution : List WALSCount

WALS Chapter 79B distribution, derived from F79B data (N = 193).

Equations

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

theorem Phenomena.Morphology.Typology.ch79b_total : List.foldl (fun (acc : ℕ) (c : WALSCount) => acc + c.count) 0 ch79bDistribution = 193

Ch 79B total: 193 languages (derived from F79B data).

def Phenomena.Morphology.Typology.ch80Distribution : List WALSCount

WALS Chapter 80A distribution, derived from F80A data (N = 193).

Equations

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

theorem Phenomena.Morphology.Typology.ch80_total : List.foldl (fun (acc : ℕ) (c : WALSCount) => acc + c.count) 0 ch80Distribution = 193

Ch 80 total: 193 languages (derived from F80A data).

Fragment profiles are defined in Fragments.{Language}.Morph with values derived from WALS data via Core.Morphology.wals* lookup helpers.

def Phenomena.Morphology.Typology.allMorphProfiles : List Core.Morphology.MorphProfile

All 18 morphological mechanism profiles.

Equations

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

theorem Phenomena.Morphology.Typology.allMorphProfiles_count : allMorphProfiles.length = 18

def Phenomena.Morphology.Typology.countByFusion (langs : List Core.Morphology.MorphProfile) (f : Core.Morphology.Fusion) : ℕ

Equations

• Phenomena.Morphology.Typology.countByFusion langs f = (List.filter (fun (p : Core.Morphology.MorphProfile) => p.fusion == f) langs).length

def Phenomena.Morphology.Typology.countByExponence (langs : List Core.Morphology.MorphProfile) (e : Core.Morphology.Exponence) : ℕ

Equations

• Phenomena.Morphology.Typology.countByExponence langs e = (List.filter (fun (p : Core.Morphology.MorphProfile) => p.exponence == e) langs).length

def Phenomena.Morphology.Typology.countByLocus (langs : List Core.Morphology.MorphProfile) (l : Core.Morphology.LocusOfMarking) : ℕ

Equations

• Phenomena.Morphology.Typology.countByLocus langs l = (List.filter (fun (p : Core.Morphology.MorphProfile) => p.locus == l) langs).length

def Phenomena.Morphology.Typology.countBySynthesis (langs : List Core.Morphology.MorphProfile) (s : Core.Morphology.VerbSynthesis) : ℕ

Equations

• Phenomena.Morphology.Typology.countBySynthesis langs s = (List.filter (fun (p : Core.Morphology.MorphProfile) => p.verbSynthesis == s) langs).length

Count values are determined by WALS-derived Fragment profiles. Values differ from the pre-refactor hand-specified profiles because WALS evaluates specific formatives, not overall typological tradition.

theorem Phenomena.Morphology.Typology.sample_concatenative_count : countByFusion allMorphProfiles Core.Morphology.Fusion.concatenative = 14

Fusion type distribution in our sample.

theorem Phenomena.Morphology.Typology.sample_nonlinear_count : countByFusion allMorphProfiles Core.Morphology.Fusion.nonlinear = 1

theorem Phenomena.Morphology.Typology.sample_isolating_count : countByFusion allMorphProfiles Core.Morphology.Fusion.isolating = 3

theorem Phenomena.Morphology.Typology.sample_monoexponential_count : countByExponence allMorphProfiles Core.Morphology.Exponence.monoexponential = 12

Exponence distribution in our sample.

theorem Phenomena.Morphology.Typology.sample_polyexponential_count : countByExponence allMorphProfiles Core.Morphology.Exponence.polyexponential = 5

theorem Phenomena.Morphology.Typology.sample_no_inflection_count : countByExponence allMorphProfiles Core.Morphology.Exponence.noCase = 1

theorem Phenomena.Morphology.Typology.sample_low_synthesis : countBySynthesis allMorphProfiles Core.Morphology.VerbSynthesis.low = 7

Verb synthesis distribution in our sample.

theorem Phenomena.Morphology.Typology.sample_moderate_synthesis : countBySynthesis allMorphProfiles Core.Morphology.VerbSynthesis.moderate = 9

theorem Phenomena.Morphology.Typology.sample_high_synthesis : countBySynthesis allMorphProfiles Core.Morphology.VerbSynthesis.high = 2

theorem Phenomena.Morphology.Typology.sample_dependent_marking : countByLocus allMorphProfiles Core.Morphology.LocusOfMarking.dependentMarking = 10

Locus of marking distribution in our sample.

theorem Phenomena.Morphology.Typology.sample_head_marking : countByLocus allMorphProfiles Core.Morphology.LocusOfMarking.headMarking = 1

theorem Phenomena.Morphology.Typology.sample_double_marking : countByLocus allMorphProfiles Core.Morphology.LocusOfMarking.doubleMarking = 4

theorem Phenomena.Morphology.Typology.sample_zero_marking : countByLocus allMorphProfiles Core.Morphology.LocusOfMarking.zeroMarking = 3

theorem Phenomena.Morphology.Typology.sample_inconsistent_marking : countByLocus allMorphProfiles Core.Morphology.LocusOfMarking.inconsistentOrOther = 0

theorem Phenomena.Morphology.Typology.fusion_counts_sum : countByFusion allMorphProfiles Core.Morphology.Fusion.concatenative + countByFusion allMorphProfiles Core.Morphology.Fusion.nonlinear + countByFusion allMorphProfiles Core.Morphology.Fusion.isolating = allMorphProfiles.length

Fusion counts sum to total.

theorem Phenomena.Morphology.Typology.locus_counts_sum : countByLocus allMorphProfiles Core.Morphology.LocusOfMarking.headMarking + countByLocus allMorphProfiles Core.Morphology.LocusOfMarking.dependentMarking + countByLocus allMorphProfiles Core.Morphology.LocusOfMarking.doubleMarking + countByLocus allMorphProfiles Core.Morphology.LocusOfMarking.zeroMarking + countByLocus allMorphProfiles Core.Morphology.LocusOfMarking.inconsistentOrOther = allMorphProfiles.length

Locus counts sum to total.

Generalization 1: Suffixing strongly dominates prefixing worldwide.

Greenberg's Universal 27: "If a language is exclusively suffixing, it is postpositional; if it is exclusively prefixing, it is prepositional." More broadly, suffixing is far more common than prefixing.

theorem Phenomena.Morphology.Typology.greenberg_universal_27_wals : have suff := (List.filter (fun (d : Core.WALS.Datapoint Core.WALS.F26A.PrefixSuffixPreference) => decide ((d.value == Core.WALS.F26A.PrefixSuffixPreference.stronglySuffixing) = true ∨ (d.value == Core.WALS.F26A.PrefixSuffixPreference.weaklySuffixing) = true)) Phenomena.Morphology.Typology.ch26✝).length; have pref := (List.filter (fun (d : Core.WALS.Datapoint Core.WALS.F26A.PrefixSuffixPreference) => decide ((d.value == Core.WALS.F26A.PrefixSuffixPreference.strongPrefixing) = true ∨ (d.value == Core.WALS.F26A.PrefixSuffixPreference.weaklyPrefixing) = true)) Phenomena.Morphology.Typology.ch26✝¹).length; suff > pref

theorem Phenomena.Morphology.Typology.suffixing_dominates_in_sample : have suffCount := (List.filter (fun (x : Core.Morphology.MorphProfile) => x.isSuffixing) allMorphProfiles).length; have prefCount := (List.filter (fun (x : Core.Morphology.MorphProfile) => x.isPrefixing) allMorphProfiles).length; suffCount > prefCount

Generalization 2: Concatenative morphology is the most common fusion type.

In the WALS Ch 20 data, exclusively concatenative languages form the largest single category. In our sample, concatenative languages also form the plurality.

theorem Phenomena.Morphology.Typology.concatenative_most_common_wals : have concat := (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F20A.FusionType) => x.value == Core.WALS.F20A.FusionType.exclusivelyConcatenative) Phenomena.Morphology.Typology.ch20✝).length; have isolating := (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F20A.FusionType) => x.value == Core.WALS.F20A.FusionType.exclusivelyIsolating) Phenomena.Morphology.Typology.ch20✝¹).length; have tonal := (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F20A.FusionType) => x.value == Core.WALS.F20A.FusionType.exclusivelyTonal) Phenomena.Morphology.Typology.ch20✝²).length; concat > isolating ∧ concat > tonal

theorem Phenomena.Morphology.Typology.concatenative_plurality_in_sample : countByFusion allMorphProfiles Core.Morphology.Fusion.concatenative > countByFusion allMorphProfiles Core.Morphology.Fusion.nonlinear ∧ countByFusion allMorphProfiles Core.Morphology.Fusion.concatenative > countByFusion allMorphProfiles Core.Morphology.Fusion.isolating

Generalization 3: Dependent-marking is the most common locus type

in our sample.

theorem Phenomena.Morphology.Typology.dependent_marking_common : countByLocus allMorphProfiles Core.Morphology.LocusOfMarking.dependentMarking ≥ countByLocus allMorphProfiles Core.Morphology.LocusOfMarking.headMarking

Generalization 4: Productive reduplication is present in a majority of

languages in the WALS Ch 27 data.

theorem Phenomena.Morphology.Typology.reduplication_in_majority_wals : have hasRedup := (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F27A.ReduplicationType) => x.value != Core.WALS.F27A.ReduplicationType.noProductiveReduplication) Phenomena.Morphology.Typology.ch27✝).length; hasRedup * 2 > Phenomena.Morphology.Typology.ch27✝¹.length

theorem Phenomena.Morphology.Typology.reduplication_attested_in_sample : (List.filter (fun (x : Core.Morphology.MorphProfile) => x.hasRedup) allMorphProfiles).length ≥ 3

Generalization 7: Concatenative languages are predominantly

monoexponential.

This is the defining correlation of agglutination: one-to-one mapping between form and meaning in the morphology.

theorem Phenomena.Morphology.Typology.concatenative_mostly_monoexponential : have concatLangs := List.filter (fun (x : Core.Morphology.MorphProfile) => x.isConcatenative) allMorphProfiles; have concatMono := List.filter (fun (x : Core.Morphology.MorphProfile) => x.isMono) concatLangs; concatMono.length * 2 > concatLangs.length

Generalization 8: Head-marking languages tend to have high verb

synthesis.

If grammatical relations are marked on the head (verb), then the verb carries agreement morphology for multiple arguments, driving up synthesis.

theorem Phenomena.Morphology.Typology.head_marking_high_synthesis : have headLangs := List.filter (fun (p : Core.Morphology.MorphProfile) => p.locus == Core.Morphology.LocusOfMarking.headMarking) allMorphProfiles; (headLangs.all fun (p : Core.Morphology.MorphProfile) => p.verbSynthesis == Core.Morphology.VerbSynthesis.moderate || p.verbSynthesis == Core.Morphology.VerbSynthesis.high) = true

Generalization: All languages with high verb synthesis have either

concatenative or nonlinear fusion (never isolating).

theorem Phenomena.Morphology.Typology.high_synthesis_not_isolating : (allMorphProfiles.all fun (p : Core.Morphology.MorphProfile) => if p.isHighSynthesis = true then !p.isIsolating else true) = true

theorem Phenomena.Morphology.Typology.ch26_suffixing_majority : 406 + 123 > (969 - 153) / 2

Ch 26: Suffixing (strongly + weakly) accounts for over half of languages with affixation (529/816 = 65%).

theorem Phenomena.Morphology.Typology.ch20_concatenative_majority : 58 + 28 + 24 > 160 / 2

Ch 20: Concatenative types (exclusively + strongly + weakly) account for the majority of the sample.

theorem Phenomena.Morphology.Typology.ch22_moderate_dominant : 39 + 45 + 24 > 145 / 2

Ch 22: Most languages have 2--7 categories per verb word. The extremes (0--1 and 12--13) are rare.

theorem Phenomena.Morphology.Typology.ch27_reduplication_split : have withRedup := 147 + 35; have withoutRedup := 186; withRedup > withoutRedup / 2 ∧ withoutRedup > withRedup / 2

Ch 27: Languages split roughly evenly between having productive reduplication and not.

theorem Phenomena.Morphology.Typology.morph_iso_length_3 : (allMorphProfiles.all fun (p : Core.Morphology.MorphProfile) => p.iso.length == 3) = true

All ISO codes in the morphological profiles are 3 characters.

theorem Phenomena.Morphology.Typology.morph_iso_unique : (List.map (fun (x : Core.Morphology.MorphProfile) => x.iso) allMorphProfiles).eraseDups.length = allMorphProfiles.length

No duplicate ISO codes in the morphological profiles.

WALS Grounding

Per-language grounding theorems verify that Fragment MorphProfile values are consistent with WALS generated data. Since profiles are now WALS-derived by construction (via wals* helpers), these theorems serve as regression tests: if WALS data changes, the corresponding theorem breaks.

theorem Phenomena.Morphology.Typology.english_ch20 : ((Core.WALS.F20A.lookup "eng").bind fun (x : Core.WALS.Datapoint Core.WALS.F20A.FusionType) => Core.Morphology.fromWALS20A x.value) = some Phenomena.Morphology.Typology.englishMorph✝.fusion

theorem Phenomena.Morphology.Typology.japanese_ch20 : ((Core.WALS.F20A.lookup "jpn").bind fun (x : Core.WALS.Datapoint Core.WALS.F20A.FusionType) => Core.Morphology.fromWALS20A x.value) = some Phenomena.Morphology.Typology.japaneseMorph✝.fusion

theorem Phenomena.Morphology.Typology.turkish_ch20 : ((Core.WALS.F20A.lookup "tur").bind fun (x : Core.WALS.Datapoint Core.WALS.F20A.FusionType) => Core.Morphology.fromWALS20A x.value) = some Phenomena.Morphology.Typology.turkishMorph✝.fusion

theorem Phenomena.Morphology.Typology.finnish_ch20 : ((Core.WALS.F20A.lookup "fin").bind fun (x : Core.WALS.Datapoint Core.WALS.F20A.FusionType) => Core.Morphology.fromWALS20A x.value) = some Phenomena.Morphology.Typology.finnishMorph✝.fusion

theorem Phenomena.Morphology.Typology.swahili_ch20 : ((Core.WALS.F20A.lookup "swa").bind fun (x : Core.WALS.Datapoint Core.WALS.F20A.FusionType) => Core.Morphology.fromWALS20A x.value) = some Phenomena.Morphology.Typology.swahiliMorph✝.fusion

theorem Phenomena.Morphology.Typology.hindi_ch20 : ((Core.WALS.F20A.lookup "hin").bind fun (x : Core.WALS.Datapoint Core.WALS.F20A.FusionType) => Core.Morphology.fromWALS20A x.value) = some Phenomena.Morphology.Typology.hindiMorph✝.fusion

theorem Phenomena.Morphology.Typology.tagalog_ch20 : ((Core.WALS.F20A.lookup "tag").bind fun (x : Core.WALS.Datapoint Core.WALS.F20A.FusionType) => Core.Morphology.fromWALS20A x.value) = some Phenomena.Morphology.Typology.tagalogMorph✝.fusion

theorem Phenomena.Morphology.Typology.hungarian_ch20 : ((Core.WALS.F20A.lookup "hun").bind fun (x : Core.WALS.Datapoint Core.WALS.F20A.FusionType) => Core.Morphology.fromWALS20A x.value) = some Phenomena.Morphology.Typology.hungarianMorph✝.fusion

theorem Phenomena.Morphology.Typology.korean_ch20 : ((Core.WALS.F20A.lookup "kor").bind fun (x : Core.WALS.Datapoint Core.WALS.F20A.FusionType) => Core.Morphology.fromWALS20A x.value) = some Phenomena.Morphology.Typology.koreanMorph✝.fusion

theorem Phenomena.Morphology.Typology.english_ch22 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F22A.InflectionalSynthesis) => Core.Morphology.fromWALS22A x.value) (Core.WALS.F22A.lookup "eng") = some Phenomena.Morphology.Typology.englishMorph✝.verbSynthesis

theorem Phenomena.Morphology.Typology.mandarin_ch22 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F22A.InflectionalSynthesis) => Core.Morphology.fromWALS22A x.value) (Core.WALS.F22A.lookup "mnd") = some Phenomena.Morphology.Typology.mandarinMorph✝.verbSynthesis

theorem Phenomena.Morphology.Typology.japanese_ch22 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F22A.InflectionalSynthesis) => Core.Morphology.fromWALS22A x.value) (Core.WALS.F22A.lookup "jpn") = some Phenomena.Morphology.Typology.japaneseMorph✝.verbSynthesis

theorem Phenomena.Morphology.Typology.turkish_ch22 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F22A.InflectionalSynthesis) => Core.Morphology.fromWALS22A x.value) (Core.WALS.F22A.lookup "tur") = some Phenomena.Morphology.Typology.turkishMorph✝.verbSynthesis

theorem Phenomena.Morphology.Typology.russian_ch22 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F22A.InflectionalSynthesis) => Core.Morphology.fromWALS22A x.value) (Core.WALS.F22A.lookup "rus") = some Phenomena.Morphology.Typology.russianMorph✝.verbSynthesis

theorem Phenomena.Morphology.Typology.georgian_ch22 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F22A.InflectionalSynthesis) => Core.Morphology.fromWALS22A x.value) (Core.WALS.F22A.lookup "geo") = some Phenomena.Morphology.Typology.georgianMorph✝.verbSynthesis

theorem Phenomena.Morphology.Typology.indonesian_ch22 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F22A.InflectionalSynthesis) => Core.Morphology.fromWALS22A x.value) (Core.WALS.F22A.lookup "ind") = some Phenomena.Morphology.Typology.indonesianMorph✝.verbSynthesis

theorem Phenomena.Morphology.Typology.korean_ch22 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F22A.InflectionalSynthesis) => Core.Morphology.fromWALS22A x.value) (Core.WALS.F22A.lookup "kor") = some Phenomena.Morphology.Typology.koreanMorph✝.verbSynthesis

theorem Phenomena.Morphology.Typology.spanish_ch22 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F22A.InflectionalSynthesis) => Core.Morphology.fromWALS22A x.value) (Core.WALS.F22A.lookup "spa") = some Phenomena.Morphology.Typology.spanishMorph✝.verbSynthesis

theorem Phenomena.Morphology.Typology.hungarian_ch22 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F22A.InflectionalSynthesis) => Core.Morphology.fromWALS22A x.value) (Core.WALS.F22A.lookup "hun") = some Phenomena.Morphology.Typology.hungarianMorph✝.verbSynthesis

theorem Phenomena.Morphology.Typology.thai_ch22 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F22A.InflectionalSynthesis) => Core.Morphology.fromWALS22A x.value) (Core.WALS.F22A.lookup "tha") = some Phenomena.Morphology.Typology.thaiMorph✝.verbSynthesis

theorem Phenomena.Morphology.Typology.japanese_ch26 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F26A.PrefixSuffixPreference) => Core.Morphology.fromWALS26A x.value) (Core.WALS.F26A.lookup "jpn") = some Phenomena.Morphology.Typology.japaneseMorph✝.prefixSuffix

theorem Phenomena.Morphology.Typology.turkish_ch26 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F26A.PrefixSuffixPreference) => Core.Morphology.fromWALS26A x.value) (Core.WALS.F26A.lookup "tur") = some Phenomena.Morphology.Typology.turkishMorph✝.prefixSuffix

theorem Phenomena.Morphology.Typology.finnish_ch26 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F26A.PrefixSuffixPreference) => Core.Morphology.fromWALS26A x.value) (Core.WALS.F26A.lookup "fin") = some Phenomena.Morphology.Typology.finnishMorph✝.prefixSuffix

theorem Phenomena.Morphology.Typology.swahili_ch26 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F26A.PrefixSuffixPreference) => Core.Morphology.fromWALS26A x.value) (Core.WALS.F26A.lookup "swa") = some Phenomena.Morphology.Typology.swahiliMorph✝.prefixSuffix

theorem Phenomena.Morphology.Typology.hindi_ch26 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F26A.PrefixSuffixPreference) => Core.Morphology.fromWALS26A x.value) (Core.WALS.F26A.lookup "hin") = some Phenomena.Morphology.Typology.hindiMorph✝.prefixSuffix

theorem Phenomena.Morphology.Typology.georgian_ch26 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F26A.PrefixSuffixPreference) => Core.Morphology.fromWALS26A x.value) (Core.WALS.F26A.lookup "geo") = some Phenomena.Morphology.Typology.georgianMorph✝.prefixSuffix

theorem Phenomena.Morphology.Typology.korean_ch26 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F26A.PrefixSuffixPreference) => Core.Morphology.fromWALS26A x.value) (Core.WALS.F26A.lookup "kor") = some Phenomena.Morphology.Typology.koreanMorph✝.prefixSuffix

theorem Phenomena.Morphology.Typology.hungarian_ch26 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F26A.PrefixSuffixPreference) => Core.Morphology.fromWALS26A x.value) (Core.WALS.F26A.lookup "hun") = some Phenomena.Morphology.Typology.hungarianMorph✝.prefixSuffix

theorem Phenomena.Morphology.Typology.thai_ch26 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F26A.PrefixSuffixPreference) => Core.Morphology.fromWALS26A x.value) (Core.WALS.F26A.lookup "tha") = some Phenomena.Morphology.Typology.thaiMorph✝.prefixSuffix

theorem Phenomena.Morphology.Typology.english_ch27 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F27A.ReduplicationType) => Core.Morphology.fromWALS27A x.value) (Core.WALS.F27A.lookup "eng") = some Phenomena.Morphology.Typology.englishMorph✝.reduplication

theorem Phenomena.Morphology.Typology.finnish_ch27 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F27A.ReduplicationType) => Core.Morphology.fromWALS27A x.value) (Core.WALS.F27A.lookup "fin") = some Phenomena.Morphology.Typology.finnishMorph✝.reduplication

theorem Phenomena.Morphology.Typology.russian_ch27 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F27A.ReduplicationType) => Core.Morphology.fromWALS27A x.value) (Core.WALS.F27A.lookup "rus") = some Phenomena.Morphology.Typology.russianMorph✝.reduplication

theorem Phenomena.Morphology.Typology.swahili_ch27 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F27A.ReduplicationType) => Core.Morphology.fromWALS27A x.value) (Core.WALS.F27A.lookup "swa") = some Phenomena.Morphology.Typology.swahiliMorph✝.reduplication

theorem Phenomena.Morphology.Typology.german_ch27 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F27A.ReduplicationType) => Core.Morphology.fromWALS27A x.value) (Core.WALS.F27A.lookup "ger") = some Phenomena.Morphology.Typology.germanMorph✝.reduplication

theorem Phenomena.Morphology.Typology.spanish_ch27 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F27A.ReduplicationType) => Core.Morphology.fromWALS27A x.value) (Core.WALS.F27A.lookup "spa") = some Phenomena.Morphology.Typology.spanishMorph✝.reduplication

theorem Phenomena.Morphology.Typology.tagalog_ch27 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F27A.ReduplicationType) => Core.Morphology.fromWALS27A x.value) (Core.WALS.F27A.lookup "tag") = some Phenomena.Morphology.Typology.tagalogMorph✝.reduplication

theorem Phenomena.Morphology.Typology.english_ch23 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F23A.LocusOfMarkingInTheClause) => Core.Morphology.fromWALS23A x.value) (Core.WALS.F23A.lookup "eng") = some Core.Morphology.LocusClause.dependentMarking

theorem Phenomena.Morphology.Typology.mandarin_ch23 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F23A.LocusOfMarkingInTheClause) => Core.Morphology.fromWALS23A x.value) (Core.WALS.F23A.lookup "mnd") = some Core.Morphology.LocusClause.dependentMarking

theorem Phenomena.Morphology.Typology.japanese_ch23 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F23A.LocusOfMarkingInTheClause) => Core.Morphology.fromWALS23A x.value) (Core.WALS.F23A.lookup "jpn") = some Core.Morphology.LocusClause.dependentMarking

theorem Phenomena.Morphology.Typology.turkish_ch23 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F23A.LocusOfMarkingInTheClause) => Core.Morphology.fromWALS23A x.value) (Core.WALS.F23A.lookup "tur") = some Core.Morphology.LocusClause.dependentMarking

theorem Phenomena.Morphology.Typology.finnish_ch23 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F23A.LocusOfMarkingInTheClause) => Core.Morphology.fromWALS23A x.value) (Core.WALS.F23A.lookup "fin") = some Core.Morphology.LocusClause.dependentMarking

theorem Phenomena.Morphology.Typology.russian_ch23 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F23A.LocusOfMarkingInTheClause) => Core.Morphology.fromWALS23A x.value) (Core.WALS.F23A.lookup "rus") = some Core.Morphology.LocusClause.dependentMarking

theorem Phenomena.Morphology.Typology.swahili_ch23 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F23A.LocusOfMarkingInTheClause) => Core.Morphology.fromWALS23A x.value) (Core.WALS.F23A.lookup "swa") = some Core.Morphology.LocusClause.headMarking

theorem Phenomena.Morphology.Typology.hindi_ch23 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F23A.LocusOfMarkingInTheClause) => Core.Morphology.fromWALS23A x.value) (Core.WALS.F23A.lookup "hin") = some Core.Morphology.LocusClause.doubleMarking

theorem Phenomena.Morphology.Typology.tagalog_ch23 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F23A.LocusOfMarkingInTheClause) => Core.Morphology.fromWALS23A x.value) (Core.WALS.F23A.lookup "tag") = some Core.Morphology.LocusClause.doubleMarking

theorem Phenomena.Morphology.Typology.hungarian_ch23 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F23A.LocusOfMarkingInTheClause) => Core.Morphology.fromWALS23A x.value) (Core.WALS.F23A.lookup "hun") = some Core.Morphology.LocusClause.dependentMarking

theorem Phenomena.Morphology.Typology.georgian_ch23 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F23A.LocusOfMarkingInTheClause) => Core.Morphology.fromWALS23A x.value) (Core.WALS.F23A.lookup "geo") = some Core.Morphology.LocusClause.doubleMarking

theorem Phenomena.Morphology.Typology.thai_ch23 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F23A.LocusOfMarkingInTheClause) => Core.Morphology.fromWALS23A x.value) (Core.WALS.F23A.lookup "tha") = some Core.Morphology.LocusClause.noMarking

theorem Phenomena.Morphology.Typology.indonesian_ch23 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F23A.LocusOfMarkingInTheClause) => Core.Morphology.fromWALS23A x.value) (Core.WALS.F23A.lookup "ind") = some Core.Morphology.LocusClause.noMarking

theorem Phenomena.Morphology.Typology.korean_ch23 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F23A.LocusOfMarkingInTheClause) => Core.Morphology.fromWALS23A x.value) (Core.WALS.F23A.lookup "kor") = some Core.Morphology.LocusClause.dependentMarking

theorem Phenomena.Morphology.Typology.german_ch23 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F23A.LocusOfMarkingInTheClause) => Core.Morphology.fromWALS23A x.value) (Core.WALS.F23A.lookup "ger") = some Core.Morphology.LocusClause.dependentMarking

theorem Phenomena.Morphology.Typology.spanish_ch23 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F23A.LocusOfMarkingInTheClause) => Core.Morphology.fromWALS23A x.value) (Core.WALS.F23A.lookup "spa") = some Core.Morphology.LocusClause.doubleMarking

theorem Phenomena.Morphology.Typology.english_ch24 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F24A.LocusOfMarkingInPossessiveNounPhrases) => Core.Morphology.fromWALS24A x.value) (Core.WALS.F24A.lookup "eng") = some Core.Morphology.LocusPossessive.dependentMarking

theorem Phenomena.Morphology.Typology.mandarin_ch24 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F24A.LocusOfMarkingInPossessiveNounPhrases) => Core.Morphology.fromWALS24A x.value) (Core.WALS.F24A.lookup "mnd") = some Core.Morphology.LocusPossessive.dependentMarking

theorem Phenomena.Morphology.Typology.japanese_ch24 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F24A.LocusOfMarkingInPossessiveNounPhrases) => Core.Morphology.fromWALS24A x.value) (Core.WALS.F24A.lookup "jpn") = some Core.Morphology.LocusPossessive.dependentMarking

theorem Phenomena.Morphology.Typology.turkish_ch24 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F24A.LocusOfMarkingInPossessiveNounPhrases) => Core.Morphology.fromWALS24A x.value) (Core.WALS.F24A.lookup "tur") = some Core.Morphology.LocusPossessive.doubleMarking

theorem Phenomena.Morphology.Typology.finnish_ch24 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F24A.LocusOfMarkingInPossessiveNounPhrases) => Core.Morphology.fromWALS24A x.value) (Core.WALS.F24A.lookup "fin") = some Core.Morphology.LocusPossessive.doubleMarking

theorem Phenomena.Morphology.Typology.russian_ch24 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F24A.LocusOfMarkingInPossessiveNounPhrases) => Core.Morphology.fromWALS24A x.value) (Core.WALS.F24A.lookup "rus") = some Core.Morphology.LocusPossessive.dependentMarking

theorem Phenomena.Morphology.Typology.swahili_ch24 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F24A.LocusOfMarkingInPossessiveNounPhrases) => Core.Morphology.fromWALS24A x.value) (Core.WALS.F24A.lookup "swa") = some Core.Morphology.LocusPossessive.dependentMarking

theorem Phenomena.Morphology.Typology.hindi_ch24 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F24A.LocusOfMarkingInPossessiveNounPhrases) => Core.Morphology.fromWALS24A x.value) (Core.WALS.F24A.lookup "hin") = some Core.Morphology.LocusPossessive.dependentMarking

theorem Phenomena.Morphology.Typology.tagalog_ch24 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F24A.LocusOfMarkingInPossessiveNounPhrases) => Core.Morphology.fromWALS24A x.value) (Core.WALS.F24A.lookup "tag") = some Core.Morphology.LocusPossessive.other

theorem Phenomena.Morphology.Typology.hungarian_ch24 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F24A.LocusOfMarkingInPossessiveNounPhrases) => Core.Morphology.fromWALS24A x.value) (Core.WALS.F24A.lookup "hun") = some Core.Morphology.LocusPossessive.headMarking

theorem Phenomena.Morphology.Typology.georgian_ch24 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F24A.LocusOfMarkingInPossessiveNounPhrases) => Core.Morphology.fromWALS24A x.value) (Core.WALS.F24A.lookup "geo") = some Core.Morphology.LocusPossessive.dependentMarking

theorem Phenomena.Morphology.Typology.thai_ch24 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F24A.LocusOfMarkingInPossessiveNounPhrases) => Core.Morphology.fromWALS24A x.value) (Core.WALS.F24A.lookup "tha") = some Core.Morphology.LocusPossessive.dependentMarking

theorem Phenomena.Morphology.Typology.indonesian_ch24 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F24A.LocusOfMarkingInPossessiveNounPhrases) => Core.Morphology.fromWALS24A x.value) (Core.WALS.F24A.lookup "ind") = some Core.Morphology.LocusPossessive.noMarking

theorem Phenomena.Morphology.Typology.korean_ch24 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F24A.LocusOfMarkingInPossessiveNounPhrases) => Core.Morphology.fromWALS24A x.value) (Core.WALS.F24A.lookup "kor") = some Core.Morphology.LocusPossessive.dependentMarking

theorem Phenomena.Morphology.Typology.german_ch24 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F24A.LocusOfMarkingInPossessiveNounPhrases) => Core.Morphology.fromWALS24A x.value) (Core.WALS.F24A.lookup "ger") = some Core.Morphology.LocusPossessive.dependentMarking

theorem Phenomena.Morphology.Typology.spanish_ch24 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F24A.LocusOfMarkingInPossessiveNounPhrases) => Core.Morphology.fromWALS24A x.value) (Core.WALS.F24A.lookup "spa") = some Core.Morphology.LocusPossessive.dependentMarking

theorem Phenomena.Morphology.Typology.english_ch25a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F25A.LocusOfMarkingWholeLanguageTypology) => Core.Morphology.fromWALS25A x.value) (Core.WALS.F25A.lookup "eng") = some Core.Morphology.WholeLanguageMarking.dependentMarking

theorem Phenomena.Morphology.Typology.mandarin_ch25a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F25A.LocusOfMarkingWholeLanguageTypology) => Core.Morphology.fromWALS25A x.value) (Core.WALS.F25A.lookup "mnd") = some Core.Morphology.WholeLanguageMarking.dependentMarking

theorem Phenomena.Morphology.Typology.japanese_ch25a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F25A.LocusOfMarkingWholeLanguageTypology) => Core.Morphology.fromWALS25A x.value) (Core.WALS.F25A.lookup "jpn") = some Core.Morphology.WholeLanguageMarking.dependentMarking

theorem Phenomena.Morphology.Typology.russian_ch25a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F25A.LocusOfMarkingWholeLanguageTypology) => Core.Morphology.fromWALS25A x.value) (Core.WALS.F25A.lookup "rus") = some Core.Morphology.WholeLanguageMarking.dependentMarking

theorem Phenomena.Morphology.Typology.korean_ch25a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F25A.LocusOfMarkingWholeLanguageTypology) => Core.Morphology.fromWALS25A x.value) (Core.WALS.F25A.lookup "kor") = some Core.Morphology.WholeLanguageMarking.dependentMarking

theorem Phenomena.Morphology.Typology.german_ch25a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F25A.LocusOfMarkingWholeLanguageTypology) => Core.Morphology.fromWALS25A x.value) (Core.WALS.F25A.lookup "ger") = some Core.Morphology.WholeLanguageMarking.dependentMarking

theorem Phenomena.Morphology.Typology.turkish_ch25a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F25A.LocusOfMarkingWholeLanguageTypology) => Core.Morphology.fromWALS25A x.value) (Core.WALS.F25A.lookup "tur") = some Core.Morphology.WholeLanguageMarking.inconsistentOrOther

theorem Phenomena.Morphology.Typology.finnish_ch25a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F25A.LocusOfMarkingWholeLanguageTypology) => Core.Morphology.fromWALS25A x.value) (Core.WALS.F25A.lookup "fin") = some Core.Morphology.WholeLanguageMarking.inconsistentOrOther

theorem Phenomena.Morphology.Typology.swahili_ch25a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F25A.LocusOfMarkingWholeLanguageTypology) => Core.Morphology.fromWALS25A x.value) (Core.WALS.F25A.lookup "swa") = some Core.Morphology.WholeLanguageMarking.inconsistentOrOther

theorem Phenomena.Morphology.Typology.hindi_ch25a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F25A.LocusOfMarkingWholeLanguageTypology) => Core.Morphology.fromWALS25A x.value) (Core.WALS.F25A.lookup "hin") = some Core.Morphology.WholeLanguageMarking.inconsistentOrOther

theorem Phenomena.Morphology.Typology.tagalog_ch25a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F25A.LocusOfMarkingWholeLanguageTypology) => Core.Morphology.fromWALS25A x.value) (Core.WALS.F25A.lookup "tag") = some Core.Morphology.WholeLanguageMarking.inconsistentOrOther

theorem Phenomena.Morphology.Typology.hungarian_ch25a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F25A.LocusOfMarkingWholeLanguageTypology) => Core.Morphology.fromWALS25A x.value) (Core.WALS.F25A.lookup "hun") = some Core.Morphology.WholeLanguageMarking.inconsistentOrOther

theorem Phenomena.Morphology.Typology.georgian_ch25a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F25A.LocusOfMarkingWholeLanguageTypology) => Core.Morphology.fromWALS25A x.value) (Core.WALS.F25A.lookup "geo") = some Core.Morphology.WholeLanguageMarking.inconsistentOrOther

theorem Phenomena.Morphology.Typology.thai_ch25a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F25A.LocusOfMarkingWholeLanguageTypology) => Core.Morphology.fromWALS25A x.value) (Core.WALS.F25A.lookup "tha") = some Core.Morphology.WholeLanguageMarking.inconsistentOrOther

theorem Phenomena.Morphology.Typology.indonesian_ch25a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F25A.LocusOfMarkingWholeLanguageTypology) => Core.Morphology.fromWALS25A x.value) (Core.WALS.F25A.lookup "ind") = some Core.Morphology.WholeLanguageMarking.zeroMarking

theorem Phenomena.Morphology.Typology.spanish_ch25a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F25A.LocusOfMarkingWholeLanguageTypology) => Core.Morphology.fromWALS25A x.value) (Core.WALS.F25A.lookup "spa") = some Core.Morphology.WholeLanguageMarking.inconsistentOrOther

theorem Phenomena.Morphology.Typology.arabic_eg_ch25a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F25A.LocusOfMarkingWholeLanguageTypology) => Core.Morphology.fromWALS25A x.value) (Core.WALS.F25A.lookup "aeg") = some Core.Morphology.WholeLanguageMarking.inconsistentOrOther

theorem Phenomena.Morphology.Typology.english_ch25b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F25B.ZeroMarkingOfAAndPArguments) => Core.Morphology.fromWALS25B x.value) (Core.WALS.F25B.lookup "eng") = some Core.Morphology.ZeroMarkingAP.nonZeroMarking

theorem Phenomena.Morphology.Typology.mandarin_ch25b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F25B.ZeroMarkingOfAAndPArguments) => Core.Morphology.fromWALS25B x.value) (Core.WALS.F25B.lookup "mnd") = some Core.Morphology.ZeroMarkingAP.nonZeroMarking

theorem Phenomena.Morphology.Typology.japanese_ch25b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F25B.ZeroMarkingOfAAndPArguments) => Core.Morphology.fromWALS25B x.value) (Core.WALS.F25B.lookup "jpn") = some Core.Morphology.ZeroMarkingAP.nonZeroMarking

theorem Phenomena.Morphology.Typology.turkish_ch25b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F25B.ZeroMarkingOfAAndPArguments) => Core.Morphology.fromWALS25B x.value) (Core.WALS.F25B.lookup "tur") = some Core.Morphology.ZeroMarkingAP.nonZeroMarking

theorem Phenomena.Morphology.Typology.finnish_ch25b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F25B.ZeroMarkingOfAAndPArguments) => Core.Morphology.fromWALS25B x.value) (Core.WALS.F25B.lookup "fin") = some Core.Morphology.ZeroMarkingAP.nonZeroMarking

theorem Phenomena.Morphology.Typology.russian_ch25b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F25B.ZeroMarkingOfAAndPArguments) => Core.Morphology.fromWALS25B x.value) (Core.WALS.F25B.lookup "rus") = some Core.Morphology.ZeroMarkingAP.nonZeroMarking

theorem Phenomena.Morphology.Typology.swahili_ch25b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F25B.ZeroMarkingOfAAndPArguments) => Core.Morphology.fromWALS25B x.value) (Core.WALS.F25B.lookup "swa") = some Core.Morphology.ZeroMarkingAP.nonZeroMarking

theorem Phenomena.Morphology.Typology.hindi_ch25b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F25B.ZeroMarkingOfAAndPArguments) => Core.Morphology.fromWALS25B x.value) (Core.WALS.F25B.lookup "hin") = some Core.Morphology.ZeroMarkingAP.nonZeroMarking

theorem Phenomena.Morphology.Typology.thai_ch25b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F25B.ZeroMarkingOfAAndPArguments) => Core.Morphology.fromWALS25B x.value) (Core.WALS.F25B.lookup "tha") = some Core.Morphology.ZeroMarkingAP.zeroMarking

theorem Phenomena.Morphology.Typology.indonesian_ch25b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F25B.ZeroMarkingOfAAndPArguments) => Core.Morphology.fromWALS25B x.value) (Core.WALS.F25B.lookup "ind") = some Core.Morphology.ZeroMarkingAP.zeroMarking

theorem Phenomena.Morphology.Typology.korean_ch25b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F25B.ZeroMarkingOfAAndPArguments) => Core.Morphology.fromWALS25B x.value) (Core.WALS.F25B.lookup "kor") = some Core.Morphology.ZeroMarkingAP.nonZeroMarking

theorem Phenomena.Morphology.Typology.german_ch25b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F25B.ZeroMarkingOfAAndPArguments) => Core.Morphology.fromWALS25B x.value) (Core.WALS.F25B.lookup "ger") = some Core.Morphology.ZeroMarkingAP.nonZeroMarking

theorem Phenomena.Morphology.Typology.spanish_ch25b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F25B.ZeroMarkingOfAAndPArguments) => Core.Morphology.fromWALS25B x.value) (Core.WALS.F25B.lookup "spa") = some Core.Morphology.ZeroMarkingAP.nonZeroMarking

theorem Phenomena.Morphology.Typology.english_ch28 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F28A.CaseSyncretism) => Core.Morphology.fromWALS28A x.value) (Core.WALS.F28A.lookup "eng") = some Core.Morphology.CaseSyncretism.coreCasesOnly

theorem Phenomena.Morphology.Typology.japanese_ch28 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F28A.CaseSyncretism) => Core.Morphology.fromWALS28A x.value) (Core.WALS.F28A.lookup "jpn") = some Core.Morphology.CaseSyncretism.noCaseMarking

theorem Phenomena.Morphology.Typology.turkish_ch28 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F28A.CaseSyncretism) => Core.Morphology.fromWALS28A x.value) (Core.WALS.F28A.lookup "tur") = some Core.Morphology.CaseSyncretism.noSyncretism

theorem Phenomena.Morphology.Typology.finnish_ch28 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F28A.CaseSyncretism) => Core.Morphology.fromWALS28A x.value) (Core.WALS.F28A.lookup "fin") = some Core.Morphology.CaseSyncretism.coreAndNonCore

theorem Phenomena.Morphology.Typology.russian_ch28 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F28A.CaseSyncretism) => Core.Morphology.fromWALS28A x.value) (Core.WALS.F28A.lookup "rus") = some Core.Morphology.CaseSyncretism.coreAndNonCore

theorem Phenomena.Morphology.Typology.swahili_ch28 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F28A.CaseSyncretism) => Core.Morphology.fromWALS28A x.value) (Core.WALS.F28A.lookup "swa") = some Core.Morphology.CaseSyncretism.noCaseMarking

theorem Phenomena.Morphology.Typology.hindi_ch28 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F28A.CaseSyncretism) => Core.Morphology.fromWALS28A x.value) (Core.WALS.F28A.lookup "hin") = some Core.Morphology.CaseSyncretism.coreAndNonCore

theorem Phenomena.Morphology.Typology.hungarian_ch28 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F28A.CaseSyncretism) => Core.Morphology.fromWALS28A x.value) (Core.WALS.F28A.lookup "hun") = some Core.Morphology.CaseSyncretism.noSyncretism

theorem Phenomena.Morphology.Typology.georgian_ch28 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F28A.CaseSyncretism) => Core.Morphology.fromWALS28A x.value) (Core.WALS.F28A.lookup "geo") = some Core.Morphology.CaseSyncretism.coreAndNonCore

theorem Phenomena.Morphology.Typology.thai_ch28 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F28A.CaseSyncretism) => Core.Morphology.fromWALS28A x.value) (Core.WALS.F28A.lookup "tha") = some Core.Morphology.CaseSyncretism.noCaseMarking

theorem Phenomena.Morphology.Typology.indonesian_ch28 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F28A.CaseSyncretism) => Core.Morphology.fromWALS28A x.value) (Core.WALS.F28A.lookup "ind") = some Core.Morphology.CaseSyncretism.noCaseMarking

theorem Phenomena.Morphology.Typology.korean_ch28 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F28A.CaseSyncretism) => Core.Morphology.fromWALS28A x.value) (Core.WALS.F28A.lookup "kor") = some Core.Morphology.CaseSyncretism.noCaseMarking

theorem Phenomena.Morphology.Typology.mandarin_ch28 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F28A.CaseSyncretism) => Core.Morphology.fromWALS28A x.value) (Core.WALS.F28A.lookup "mnd") = some Core.Morphology.CaseSyncretism.noCaseMarking

theorem Phenomena.Morphology.Typology.german_ch28 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F28A.CaseSyncretism) => Core.Morphology.fromWALS28A x.value) (Core.WALS.F28A.lookup "ger") = some Core.Morphology.CaseSyncretism.coreAndNonCore

theorem Phenomena.Morphology.Typology.spanish_ch28 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F28A.CaseSyncretism) => Core.Morphology.fromWALS28A x.value) (Core.WALS.F28A.lookup "spa") = some Core.Morphology.CaseSyncretism.coreAndNonCore

theorem Phenomena.Morphology.Typology.tagalog_ch28 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F28A.CaseSyncretism) => Core.Morphology.fromWALS28A x.value) (Core.WALS.F28A.lookup "tag") = some Core.Morphology.CaseSyncretism.noCaseMarking

theorem Phenomena.Morphology.Typology.english_ch29 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F29A.SyncretismInVerbalPersonNumberMarking) => Core.Morphology.fromWALS29A x.value) (Core.WALS.F29A.lookup "eng") = some Core.Morphology.VerbalSyncretism.syncretic

theorem Phenomena.Morphology.Typology.japanese_ch29 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F29A.SyncretismInVerbalPersonNumberMarking) => Core.Morphology.fromWALS29A x.value) (Core.WALS.F29A.lookup "jpn") = some Core.Morphology.VerbalSyncretism.noSubjectMarking

theorem Phenomena.Morphology.Typology.turkish_ch29 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F29A.SyncretismInVerbalPersonNumberMarking) => Core.Morphology.fromWALS29A x.value) (Core.WALS.F29A.lookup "tur") = some Core.Morphology.VerbalSyncretism.notSyncretic

theorem Phenomena.Morphology.Typology.finnish_ch29 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F29A.SyncretismInVerbalPersonNumberMarking) => Core.Morphology.fromWALS29A x.value) (Core.WALS.F29A.lookup "fin") = some Core.Morphology.VerbalSyncretism.notSyncretic

theorem Phenomena.Morphology.Typology.russian_ch29 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F29A.SyncretismInVerbalPersonNumberMarking) => Core.Morphology.fromWALS29A x.value) (Core.WALS.F29A.lookup "rus") = some Core.Morphology.VerbalSyncretism.notSyncretic

theorem Phenomena.Morphology.Typology.swahili_ch29 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F29A.SyncretismInVerbalPersonNumberMarking) => Core.Morphology.fromWALS29A x.value) (Core.WALS.F29A.lookup "swa") = some Core.Morphology.VerbalSyncretism.syncretic

theorem Phenomena.Morphology.Typology.hindi_ch29 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F29A.SyncretismInVerbalPersonNumberMarking) => Core.Morphology.fromWALS29A x.value) (Core.WALS.F29A.lookup "hin") = some Core.Morphology.VerbalSyncretism.syncretic

theorem Phenomena.Morphology.Typology.hungarian_ch29 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F29A.SyncretismInVerbalPersonNumberMarking) => Core.Morphology.fromWALS29A x.value) (Core.WALS.F29A.lookup "hun") = some Core.Morphology.VerbalSyncretism.notSyncretic

theorem Phenomena.Morphology.Typology.georgian_ch29 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F29A.SyncretismInVerbalPersonNumberMarking) => Core.Morphology.fromWALS29A x.value) (Core.WALS.F29A.lookup "geo") = some Core.Morphology.VerbalSyncretism.notSyncretic

theorem Phenomena.Morphology.Typology.thai_ch29 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F29A.SyncretismInVerbalPersonNumberMarking) => Core.Morphology.fromWALS29A x.value) (Core.WALS.F29A.lookup "tha") = some Core.Morphology.VerbalSyncretism.noSubjectMarking

theorem Phenomena.Morphology.Typology.indonesian_ch29 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F29A.SyncretismInVerbalPersonNumberMarking) => Core.Morphology.fromWALS29A x.value) (Core.WALS.F29A.lookup "ind") = some Core.Morphology.VerbalSyncretism.noSubjectMarking

theorem Phenomena.Morphology.Typology.korean_ch29 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F29A.SyncretismInVerbalPersonNumberMarking) => Core.Morphology.fromWALS29A x.value) (Core.WALS.F29A.lookup "kor") = some Core.Morphology.VerbalSyncretism.noSubjectMarking

theorem Phenomena.Morphology.Typology.mandarin_ch29 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F29A.SyncretismInVerbalPersonNumberMarking) => Core.Morphology.fromWALS29A x.value) (Core.WALS.F29A.lookup "mnd") = some Core.Morphology.VerbalSyncretism.noSubjectMarking

theorem Phenomena.Morphology.Typology.german_ch29 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F29A.SyncretismInVerbalPersonNumberMarking) => Core.Morphology.fromWALS29A x.value) (Core.WALS.F29A.lookup "ger") = some Core.Morphology.VerbalSyncretism.syncretic

theorem Phenomena.Morphology.Typology.spanish_ch29 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F29A.SyncretismInVerbalPersonNumberMarking) => Core.Morphology.fromWALS29A x.value) (Core.WALS.F29A.lookup "spa") = some Core.Morphology.VerbalSyncretism.syncretic

theorem Phenomena.Morphology.Typology.tagalog_ch29 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F29A.SyncretismInVerbalPersonNumberMarking) => Core.Morphology.fromWALS29A x.value) (Core.WALS.F29A.lookup "tag") = some Core.Morphology.VerbalSyncretism.noSubjectMarking

theorem Phenomena.Morphology.Typology.ch20_size : Phenomena.Morphology.Typology.ch20✝.length = 165

theorem Phenomena.Morphology.Typology.ch21_size : Phenomena.Morphology.Typology.ch21✝.length = 162

theorem Phenomena.Morphology.Typology.ch22_size : Phenomena.Morphology.Typology.ch22✝.length = 145

theorem Phenomena.Morphology.Typology.ch26_size : Phenomena.Morphology.Typology.ch26✝.length = 969

theorem Phenomena.Morphology.Typology.ch27_size : Phenomena.Morphology.Typology.ch27✝.length = 368

theorem Phenomena.Morphology.Typology.ch23_size : Phenomena.Morphology.Typology.ch23✝.length = 236

theorem Phenomena.Morphology.Typology.ch24_size : Phenomena.Morphology.Typology.ch24✝.length = 236

theorem Phenomena.Morphology.Typology.ch25a_size : Phenomena.Morphology.Typology.ch25a✝.length = 236

theorem Phenomena.Morphology.Typology.ch25b_size : Phenomena.Morphology.Typology.ch25b✝.length = 235

theorem Phenomena.Morphology.Typology.ch28_size : Phenomena.Morphology.Typology.ch28✝.length = 198

theorem Phenomena.Morphology.Typology.ch29_size : Phenomena.Morphology.Typology.ch29✝.length = 198

theorem Phenomena.Morphology.Typology.ch23_count_headMarking : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F23A.LocusOfMarkingInTheClause) => x.value == Core.WALS.F23A.LocusOfMarkingInTheClause.headMarking) Phenomena.Morphology.Typology.ch23✝).length = 71

theorem Phenomena.Morphology.Typology.ch23_count_dependentMarking : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F23A.LocusOfMarkingInTheClause) => x.value == Core.WALS.F23A.LocusOfMarkingInTheClause.dependentMarking) Phenomena.Morphology.Typology.ch23✝).length = 63

theorem Phenomena.Morphology.Typology.ch23_count_doubleMarking : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F23A.LocusOfMarkingInTheClause) => x.value == Core.WALS.F23A.LocusOfMarkingInTheClause.doubleMarking) Phenomena.Morphology.Typology.ch23✝).length = 58

theorem Phenomena.Morphology.Typology.ch23_count_noMarking : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F23A.LocusOfMarkingInTheClause) => x.value == Core.WALS.F23A.LocusOfMarkingInTheClause.noMarking) Phenomena.Morphology.Typology.ch23✝).length = 42

theorem Phenomena.Morphology.Typology.ch23_count_other : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F23A.LocusOfMarkingInTheClause) => x.value == Core.WALS.F23A.LocusOfMarkingInTheClause.other) Phenomena.Morphology.Typology.ch23✝).length = 2

theorem Phenomena.Morphology.Typology.ch24_count_headMarking : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F24A.LocusOfMarkingInPossessiveNounPhrases) => x.value == Core.WALS.F24A.LocusOfMarkingInPossessiveNounPhrases.headMarking) Phenomena.Morphology.Typology.ch24✝).length = 78

theorem Phenomena.Morphology.Typology.ch24_count_dependentMarking : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F24A.LocusOfMarkingInPossessiveNounPhrases) => x.value == Core.WALS.F24A.LocusOfMarkingInPossessiveNounPhrases.dependentMarking) Phenomena.Morphology.Typology.ch24✝).length = 98

theorem Phenomena.Morphology.Typology.ch24_count_doubleMarking : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F24A.LocusOfMarkingInPossessiveNounPhrases) => x.value == Core.WALS.F24A.LocusOfMarkingInPossessiveNounPhrases.doubleMarking) Phenomena.Morphology.Typology.ch24✝).length = 22

theorem Phenomena.Morphology.Typology.ch24_count_noMarking : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F24A.LocusOfMarkingInPossessiveNounPhrases) => x.value == Core.WALS.F24A.LocusOfMarkingInPossessiveNounPhrases.noMarking) Phenomena.Morphology.Typology.ch24✝).length = 32

theorem Phenomena.Morphology.Typology.ch24_count_other : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F24A.LocusOfMarkingInPossessiveNounPhrases) => x.value == Core.WALS.F24A.LocusOfMarkingInPossessiveNounPhrases.other) Phenomena.Morphology.Typology.ch24✝).length = 6

theorem Phenomena.Morphology.Typology.ch25a_count_headMarking : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F25A.LocusOfMarkingWholeLanguageTypology) => x.value == Core.WALS.F25A.LocusOfMarkingWholeLanguageTypology.headMarking) Phenomena.Morphology.Typology.ch25a✝).length = 47

theorem Phenomena.Morphology.Typology.ch25a_count_dependentMarking : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F25A.LocusOfMarkingWholeLanguageTypology) => x.value == Core.WALS.F25A.LocusOfMarkingWholeLanguageTypology.dependentMarking) Phenomena.Morphology.Typology.ch25a✝).length = 46

theorem Phenomena.Morphology.Typology.ch25a_count_doubleMarking : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F25A.LocusOfMarkingWholeLanguageTypology) => x.value == Core.WALS.F25A.LocusOfMarkingWholeLanguageTypology.doubleMarking) Phenomena.Morphology.Typology.ch25a✝).length = 16

theorem Phenomena.Morphology.Typology.ch25a_count_zeroMarking : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F25A.LocusOfMarkingWholeLanguageTypology) => x.value == Core.WALS.F25A.LocusOfMarkingWholeLanguageTypology.zeroMarking) Phenomena.Morphology.Typology.ch25a✝).length = 6

theorem Phenomena.Morphology.Typology.ch25a_count_inconsistentOrOther : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F25A.LocusOfMarkingWholeLanguageTypology) => x.value == Core.WALS.F25A.LocusOfMarkingWholeLanguageTypology.inconsistentOrOther) Phenomena.Morphology.Typology.ch25a✝).length = 121

theorem Phenomena.Morphology.Typology.ch25b_count_zeroMarking : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F25B.ZeroMarkingOfAAndPArguments) => x.value == Core.WALS.F25B.ZeroMarkingOfAAndPArguments.zeroMarking) Phenomena.Morphology.Typology.ch25b✝).length = 16

theorem Phenomena.Morphology.Typology.ch25b_count_nonZeroMarking : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F25B.ZeroMarkingOfAAndPArguments) => x.value == Core.WALS.F25B.ZeroMarkingOfAAndPArguments.nonZeroMarking) Phenomena.Morphology.Typology.ch25b✝).length = 219

theorem Phenomena.Morphology.Typology.ch28_count_noCaseMarking : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F28A.CaseSyncretism) => x.value == Core.WALS.F28A.CaseSyncretism.noCaseMarking) Phenomena.Morphology.Typology.ch28✝).length = 123

theorem Phenomena.Morphology.Typology.ch28_count_coreCasesOnly : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F28A.CaseSyncretism) => x.value == Core.WALS.F28A.CaseSyncretism.coreCasesOnly) Phenomena.Morphology.Typology.ch28✝).length = 18

theorem Phenomena.Morphology.Typology.ch28_count_coreAndNonCore : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F28A.CaseSyncretism) => x.value == Core.WALS.F28A.CaseSyncretism.coreAndNonCore) Phenomena.Morphology.Typology.ch28✝).length = 22

theorem Phenomena.Morphology.Typology.ch28_count_noSyncretism : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F28A.CaseSyncretism) => x.value == Core.WALS.F28A.CaseSyncretism.noSyncretism) Phenomena.Morphology.Typology.ch28✝).length = 35

theorem Phenomena.Morphology.Typology.ch29_count_noSubjectMarking : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F29A.SyncretismInVerbalPersonNumberMarking) => x.value == Core.WALS.F29A.SyncretismInVerbalPersonNumberMarking.noSubjectPersonNumberMarking) Phenomena.Morphology.Typology.ch29✝).length = 57

theorem Phenomena.Morphology.Typology.ch29_count_syncretic : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F29A.SyncretismInVerbalPersonNumberMarking) => x.value == Core.WALS.F29A.SyncretismInVerbalPersonNumberMarking.syncretic) Phenomena.Morphology.Typology.ch29✝).length = 60

theorem Phenomena.Morphology.Typology.ch29_count_notSyncretic : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F29A.SyncretismInVerbalPersonNumberMarking) => x.value == Core.WALS.F29A.SyncretismInVerbalPersonNumberMarking.notSyncretic) Phenomena.Morphology.Typology.ch29✝).length = 81

theorem Phenomena.Morphology.Typology.english_ch21b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F21B.ExponenceOfTenseAspectMoodInflection) => Core.Morphology.fromWALS21B x.value) (Core.WALS.F21B.lookup "eng") = some Core.Morphology.TAMExponence.monoexponential

theorem Phenomena.Morphology.Typology.mandarin_ch21b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F21B.ExponenceOfTenseAspectMoodInflection) => Core.Morphology.fromWALS21B x.value) (Core.WALS.F21B.lookup "mnd") = some Core.Morphology.TAMExponence.monoexponential

theorem Phenomena.Morphology.Typology.japanese_ch21b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F21B.ExponenceOfTenseAspectMoodInflection) => Core.Morphology.fromWALS21B x.value) (Core.WALS.F21B.lookup "jpn") = some Core.Morphology.TAMExponence.monoexponential

theorem Phenomena.Morphology.Typology.turkish_ch21b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F21B.ExponenceOfTenseAspectMoodInflection) => Core.Morphology.fromWALS21B x.value) (Core.WALS.F21B.lookup "tur") = some Core.Morphology.TAMExponence.monoexponential

theorem Phenomena.Morphology.Typology.finnish_ch21b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F21B.ExponenceOfTenseAspectMoodInflection) => Core.Morphology.fromWALS21B x.value) (Core.WALS.F21B.lookup "fin") = some Core.Morphology.TAMExponence.monoexponential

theorem Phenomena.Morphology.Typology.russian_ch21b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F21B.ExponenceOfTenseAspectMoodInflection) => Core.Morphology.fromWALS21B x.value) (Core.WALS.F21B.lookup "rus") = some Core.Morphology.TAMExponence.monoexponential

theorem Phenomena.Morphology.Typology.swahili_ch21b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F21B.ExponenceOfTenseAspectMoodInflection) => Core.Morphology.fromWALS21B x.value) (Core.WALS.F21B.lookup "swa") = some Core.Morphology.TAMExponence.monoexponential

theorem Phenomena.Morphology.Typology.hindi_ch21b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F21B.ExponenceOfTenseAspectMoodInflection) => Core.Morphology.fromWALS21B x.value) (Core.WALS.F21B.lookup "hin") = some Core.Morphology.TAMExponence.tamAgreement

theorem Phenomena.Morphology.Typology.tagalog_ch21b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F21B.ExponenceOfTenseAspectMoodInflection) => Core.Morphology.fromWALS21B x.value) (Core.WALS.F21B.lookup "tag") = some Core.Morphology.TAMExponence.monoexponential

theorem Phenomena.Morphology.Typology.hungarian_ch21b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F21B.ExponenceOfTenseAspectMoodInflection) => Core.Morphology.fromWALS21B x.value) (Core.WALS.F21B.lookup "hun") = some Core.Morphology.TAMExponence.monoexponential

theorem Phenomena.Morphology.Typology.georgian_ch21b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F21B.ExponenceOfTenseAspectMoodInflection) => Core.Morphology.fromWALS21B x.value) (Core.WALS.F21B.lookup "geo") = some Core.Morphology.TAMExponence.tamAgreement

theorem Phenomena.Morphology.Typology.thai_ch21b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F21B.ExponenceOfTenseAspectMoodInflection) => Core.Morphology.fromWALS21B x.value) (Core.WALS.F21B.lookup "tha") = some Core.Morphology.TAMExponence.monoexponential

theorem Phenomena.Morphology.Typology.indonesian_ch21b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F21B.ExponenceOfTenseAspectMoodInflection) => Core.Morphology.fromWALS21B x.value) (Core.WALS.F21B.lookup "ind") = some Core.Morphology.TAMExponence.monoexponential

theorem Phenomena.Morphology.Typology.korean_ch21b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F21B.ExponenceOfTenseAspectMoodInflection) => Core.Morphology.fromWALS21B x.value) (Core.WALS.F21B.lookup "kor") = some Core.Morphology.TAMExponence.monoexponential

theorem Phenomena.Morphology.Typology.german_ch21b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F21B.ExponenceOfTenseAspectMoodInflection) => Core.Morphology.fromWALS21B x.value) (Core.WALS.F21B.lookup "ger") = some Core.Morphology.TAMExponence.monoexponential

theorem Phenomena.Morphology.Typology.spanish_ch21b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F21B.ExponenceOfTenseAspectMoodInflection) => Core.Morphology.fromWALS21B x.value) (Core.WALS.F21B.lookup "spa") = some Core.Morphology.TAMExponence.tamAgreement

theorem Phenomena.Morphology.Typology.english_ch62 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F62A.ActionNominalConstructions) => Core.Morphology.fromWALS62A x.value) (Core.WALS.F62A.lookup "eng") = some Core.Morphology.ActionNominal.mixed

theorem Phenomena.Morphology.Typology.mandarin_ch62 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F62A.ActionNominalConstructions) => Core.Morphology.fromWALS62A x.value) (Core.WALS.F62A.lookup "mnd") = some Core.Morphology.ActionNominal.noActionNominals

theorem Phenomena.Morphology.Typology.japanese_ch62 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F62A.ActionNominalConstructions) => Core.Morphology.fromWALS62A x.value) (Core.WALS.F62A.lookup "jpn") = some Core.Morphology.ActionNominal.doublePossessive

theorem Phenomena.Morphology.Typology.turkish_ch62 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F62A.ActionNominalConstructions) => Core.Morphology.fromWALS62A x.value) (Core.WALS.F62A.lookup "tur") = some Core.Morphology.ActionNominal.possessiveAccusative

theorem Phenomena.Morphology.Typology.finnish_ch62 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F62A.ActionNominalConstructions) => Core.Morphology.fromWALS62A x.value) (Core.WALS.F62A.lookup "fin") = some Core.Morphology.ActionNominal.doublePossessive

theorem Phenomena.Morphology.Typology.russian_ch62 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F62A.ActionNominalConstructions) => Core.Morphology.fromWALS62A x.value) (Core.WALS.F62A.lookup "rus") = some Core.Morphology.ActionNominal.ergativePossessive

theorem Phenomena.Morphology.Typology.swahili_ch62 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F62A.ActionNominalConstructions) => Core.Morphology.fromWALS62A x.value) (Core.WALS.F62A.lookup "swa") = some Core.Morphology.ActionNominal.possessiveAccusative

theorem Phenomena.Morphology.Typology.hindi_ch62 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F62A.ActionNominalConstructions) => Core.Morphology.fromWALS62A x.value) (Core.WALS.F62A.lookup "hin") = some Core.Morphology.ActionNominal.possessiveAccusative

theorem Phenomena.Morphology.Typology.tagalog_ch62 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F62A.ActionNominalConstructions) => Core.Morphology.fromWALS62A x.value) (Core.WALS.F62A.lookup "tag") = some Core.Morphology.ActionNominal.possessiveAccusative

theorem Phenomena.Morphology.Typology.hungarian_ch62 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F62A.ActionNominalConstructions) => Core.Morphology.fromWALS62A x.value) (Core.WALS.F62A.lookup "hun") = some Core.Morphology.ActionNominal.restricted

theorem Phenomena.Morphology.Typology.georgian_ch62 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F62A.ActionNominalConstructions) => Core.Morphology.fromWALS62A x.value) (Core.WALS.F62A.lookup "geo") = some Core.Morphology.ActionNominal.ergativePossessive

theorem Phenomena.Morphology.Typology.thai_ch62 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F62A.ActionNominalConstructions) => Core.Morphology.fromWALS62A x.value) (Core.WALS.F62A.lookup "tha") = some Core.Morphology.ActionNominal.mixed

theorem Phenomena.Morphology.Typology.indonesian_ch62 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F62A.ActionNominalConstructions) => Core.Morphology.fromWALS62A x.value) (Core.WALS.F62A.lookup "ind") = some Core.Morphology.ActionNominal.ergativePossessive

theorem Phenomena.Morphology.Typology.korean_ch62 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F62A.ActionNominalConstructions) => Core.Morphology.fromWALS62A x.value) (Core.WALS.F62A.lookup "kor") = some Core.Morphology.ActionNominal.sentential

theorem Phenomena.Morphology.Typology.german_ch62 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F62A.ActionNominalConstructions) => Core.Morphology.fromWALS62A x.value) (Core.WALS.F62A.lookup "ger") = some Core.Morphology.ActionNominal.ergativePossessive

theorem Phenomena.Morphology.Typology.spanish_ch62 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F62A.ActionNominalConstructions) => Core.Morphology.fromWALS62A x.value) (Core.WALS.F62A.lookup "spa") = some Core.Morphology.ActionNominal.ergativePossessive

theorem Phenomena.Morphology.Typology.english_ch79a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F79A.SuppletionAccordingToTenseAndAspect) => Core.Morphology.fromWALS79A x.value) (Core.WALS.F79A.lookup "eng") = some Core.Morphology.SuppletionTA.tense

theorem Phenomena.Morphology.Typology.mandarin_ch79a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F79A.SuppletionAccordingToTenseAndAspect) => Core.Morphology.fromWALS79A x.value) (Core.WALS.F79A.lookup "mnd") = some Core.Morphology.SuppletionTA.none

theorem Phenomena.Morphology.Typology.japanese_ch79a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F79A.SuppletionAccordingToTenseAndAspect) => Core.Morphology.fromWALS79A x.value) (Core.WALS.F79A.lookup "jpn") = some Core.Morphology.SuppletionTA.none

theorem Phenomena.Morphology.Typology.turkish_ch79a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F79A.SuppletionAccordingToTenseAndAspect) => Core.Morphology.fromWALS79A x.value) (Core.WALS.F79A.lookup "tur") = some Core.Morphology.SuppletionTA.tense

theorem Phenomena.Morphology.Typology.finnish_ch79a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F79A.SuppletionAccordingToTenseAndAspect) => Core.Morphology.fromWALS79A x.value) (Core.WALS.F79A.lookup "fin") = some Core.Morphology.SuppletionTA.none

theorem Phenomena.Morphology.Typology.russian_ch79a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F79A.SuppletionAccordingToTenseAndAspect) => Core.Morphology.fromWALS79A x.value) (Core.WALS.F79A.lookup "rus") = some Core.Morphology.SuppletionTA.tenseAndAspect

theorem Phenomena.Morphology.Typology.swahili_ch79a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F79A.SuppletionAccordingToTenseAndAspect) => Core.Morphology.fromWALS79A x.value) (Core.WALS.F79A.lookup "swa") = some Core.Morphology.SuppletionTA.none

theorem Phenomena.Morphology.Typology.hindi_ch79a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F79A.SuppletionAccordingToTenseAndAspect) => Core.Morphology.fromWALS79A x.value) (Core.WALS.F79A.lookup "hin") = some Core.Morphology.SuppletionTA.tenseAndAspect

theorem Phenomena.Morphology.Typology.tagalog_ch79a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F79A.SuppletionAccordingToTenseAndAspect) => Core.Morphology.fromWALS79A x.value) (Core.WALS.F79A.lookup "tag") = some Core.Morphology.SuppletionTA.none

theorem Phenomena.Morphology.Typology.hungarian_ch79a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F79A.SuppletionAccordingToTenseAndAspect) => Core.Morphology.fromWALS79A x.value) (Core.WALS.F79A.lookup "hun") = some Core.Morphology.SuppletionTA.tense

theorem Phenomena.Morphology.Typology.georgian_ch79a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F79A.SuppletionAccordingToTenseAndAspect) => Core.Morphology.fromWALS79A x.value) (Core.WALS.F79A.lookup "geo") = some Core.Morphology.SuppletionTA.tenseAndAspect

theorem Phenomena.Morphology.Typology.thai_ch79a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F79A.SuppletionAccordingToTenseAndAspect) => Core.Morphology.fromWALS79A x.value) (Core.WALS.F79A.lookup "tha") = some Core.Morphology.SuppletionTA.none

theorem Phenomena.Morphology.Typology.indonesian_ch79a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F79A.SuppletionAccordingToTenseAndAspect) => Core.Morphology.fromWALS79A x.value) (Core.WALS.F79A.lookup "ind") = some Core.Morphology.SuppletionTA.none

theorem Phenomena.Morphology.Typology.korean_ch79a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F79A.SuppletionAccordingToTenseAndAspect) => Core.Morphology.fromWALS79A x.value) (Core.WALS.F79A.lookup "kor") = some Core.Morphology.SuppletionTA.none

theorem Phenomena.Morphology.Typology.german_ch79a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F79A.SuppletionAccordingToTenseAndAspect) => Core.Morphology.fromWALS79A x.value) (Core.WALS.F79A.lookup "ger") = some Core.Morphology.SuppletionTA.tense

theorem Phenomena.Morphology.Typology.spanish_ch79a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F79A.SuppletionAccordingToTenseAndAspect) => Core.Morphology.fromWALS79A x.value) (Core.WALS.F79A.lookup "spa") = some Core.Morphology.SuppletionTA.tenseAndAspect

theorem Phenomena.Morphology.Typology.english_ch79b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F79B.SuppletionInImperativesAndHortatives) => Core.Morphology.fromWALS79B x.value) (Core.WALS.F79B.lookup "eng") = some Core.Morphology.SuppletionImperative.none

theorem Phenomena.Morphology.Typology.mandarin_ch79b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F79B.SuppletionInImperativesAndHortatives) => Core.Morphology.fromWALS79B x.value) (Core.WALS.F79B.lookup "mnd") = some Core.Morphology.SuppletionImperative.none

theorem Phenomena.Morphology.Typology.japanese_ch79b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F79B.SuppletionInImperativesAndHortatives) => Core.Morphology.fromWALS79B x.value) (Core.WALS.F79B.lookup "jpn") = some Core.Morphology.SuppletionImperative.none

theorem Phenomena.Morphology.Typology.turkish_ch79b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F79B.SuppletionInImperativesAndHortatives) => Core.Morphology.fromWALS79B x.value) (Core.WALS.F79B.lookup "tur") = some Core.Morphology.SuppletionImperative.none

theorem Phenomena.Morphology.Typology.finnish_ch79b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F79B.SuppletionInImperativesAndHortatives) => Core.Morphology.fromWALS79B x.value) (Core.WALS.F79B.lookup "fin") = some Core.Morphology.SuppletionImperative.imperative

theorem Phenomena.Morphology.Typology.russian_ch79b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F79B.SuppletionInImperativesAndHortatives) => Core.Morphology.fromWALS79B x.value) (Core.WALS.F79B.lookup "rus") = some Core.Morphology.SuppletionImperative.imperative

theorem Phenomena.Morphology.Typology.swahili_ch79b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F79B.SuppletionInImperativesAndHortatives) => Core.Morphology.fromWALS79B x.value) (Core.WALS.F79B.lookup "swa") = some Core.Morphology.SuppletionImperative.imperative

theorem Phenomena.Morphology.Typology.hindi_ch79b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F79B.SuppletionInImperativesAndHortatives) => Core.Morphology.fromWALS79B x.value) (Core.WALS.F79B.lookup "hin") = some Core.Morphology.SuppletionImperative.none

theorem Phenomena.Morphology.Typology.tagalog_ch79b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F79B.SuppletionInImperativesAndHortatives) => Core.Morphology.fromWALS79B x.value) (Core.WALS.F79B.lookup "tag") = some Core.Morphology.SuppletionImperative.none

theorem Phenomena.Morphology.Typology.hungarian_ch79b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F79B.SuppletionInImperativesAndHortatives) => Core.Morphology.fromWALS79B x.value) (Core.WALS.F79B.lookup "hun") = some Core.Morphology.SuppletionImperative.alternating

theorem Phenomena.Morphology.Typology.georgian_ch79b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F79B.SuppletionInImperativesAndHortatives) => Core.Morphology.fromWALS79B x.value) (Core.WALS.F79B.lookup "geo") = some Core.Morphology.SuppletionImperative.imperative

theorem Phenomena.Morphology.Typology.thai_ch79b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F79B.SuppletionInImperativesAndHortatives) => Core.Morphology.fromWALS79B x.value) (Core.WALS.F79B.lookup "tha") = some Core.Morphology.SuppletionImperative.none

theorem Phenomena.Morphology.Typology.indonesian_ch79b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F79B.SuppletionInImperativesAndHortatives) => Core.Morphology.fromWALS79B x.value) (Core.WALS.F79B.lookup "ind") = some Core.Morphology.SuppletionImperative.none

theorem Phenomena.Morphology.Typology.korean_ch79b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F79B.SuppletionInImperativesAndHortatives) => Core.Morphology.fromWALS79B x.value) (Core.WALS.F79B.lookup "kor") = some Core.Morphology.SuppletionImperative.none

theorem Phenomena.Morphology.Typology.german_ch79b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F79B.SuppletionInImperativesAndHortatives) => Core.Morphology.fromWALS79B x.value) (Core.WALS.F79B.lookup "ger") = some Core.Morphology.SuppletionImperative.none

theorem Phenomena.Morphology.Typology.spanish_ch79b : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F79B.SuppletionInImperativesAndHortatives) => Core.Morphology.fromWALS79B x.value) (Core.WALS.F79B.lookup "spa") = some Core.Morphology.SuppletionImperative.imperative

theorem Phenomena.Morphology.Typology.english_ch80 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F80A.VerbalNumberAndSuppletion) => Core.Morphology.fromWALS80A x.value) (Core.WALS.F80A.lookup "eng") = some Core.Morphology.VerbalNumber.none

theorem Phenomena.Morphology.Typology.mandarin_ch80 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F80A.VerbalNumberAndSuppletion) => Core.Morphology.fromWALS80A x.value) (Core.WALS.F80A.lookup "mnd") = some Core.Morphology.VerbalNumber.none

theorem Phenomena.Morphology.Typology.japanese_ch80 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F80A.VerbalNumberAndSuppletion) => Core.Morphology.fromWALS80A x.value) (Core.WALS.F80A.lookup "jpn") = some Core.Morphology.VerbalNumber.none

theorem Phenomena.Morphology.Typology.turkish_ch80 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F80A.VerbalNumberAndSuppletion) => Core.Morphology.fromWALS80A x.value) (Core.WALS.F80A.lookup "tur") = some Core.Morphology.VerbalNumber.none

theorem Phenomena.Morphology.Typology.finnish_ch80 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F80A.VerbalNumberAndSuppletion) => Core.Morphology.fromWALS80A x.value) (Core.WALS.F80A.lookup "fin") = some Core.Morphology.VerbalNumber.none

theorem Phenomena.Morphology.Typology.russian_ch80 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F80A.VerbalNumberAndSuppletion) => Core.Morphology.fromWALS80A x.value) (Core.WALS.F80A.lookup "rus") = some Core.Morphology.VerbalNumber.none

theorem Phenomena.Morphology.Typology.swahili_ch80 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F80A.VerbalNumberAndSuppletion) => Core.Morphology.fromWALS80A x.value) (Core.WALS.F80A.lookup "swa") = some Core.Morphology.VerbalNumber.none

theorem Phenomena.Morphology.Typology.hindi_ch80 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F80A.VerbalNumberAndSuppletion) => Core.Morphology.fromWALS80A x.value) (Core.WALS.F80A.lookup "hin") = some Core.Morphology.VerbalNumber.none

theorem Phenomena.Morphology.Typology.tagalog_ch80 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F80A.VerbalNumberAndSuppletion) => Core.Morphology.fromWALS80A x.value) (Core.WALS.F80A.lookup "tag") = some Core.Morphology.VerbalNumber.none

theorem Phenomena.Morphology.Typology.hungarian_ch80 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F80A.VerbalNumberAndSuppletion) => Core.Morphology.fromWALS80A x.value) (Core.WALS.F80A.lookup "hun") = some Core.Morphology.VerbalNumber.none

theorem Phenomena.Morphology.Typology.georgian_ch80 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F80A.VerbalNumberAndSuppletion) => Core.Morphology.fromWALS80A x.value) (Core.WALS.F80A.lookup "geo") = some Core.Morphology.VerbalNumber.pairsNoSuppletion

theorem Phenomena.Morphology.Typology.thai_ch80 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F80A.VerbalNumberAndSuppletion) => Core.Morphology.fromWALS80A x.value) (Core.WALS.F80A.lookup "tha") = some Core.Morphology.VerbalNumber.none

theorem Phenomena.Morphology.Typology.indonesian_ch80 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F80A.VerbalNumberAndSuppletion) => Core.Morphology.fromWALS80A x.value) (Core.WALS.F80A.lookup "ind") = some Core.Morphology.VerbalNumber.none

theorem Phenomena.Morphology.Typology.korean_ch80 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F80A.VerbalNumberAndSuppletion) => Core.Morphology.fromWALS80A x.value) (Core.WALS.F80A.lookup "kor") = some Core.Morphology.VerbalNumber.none

theorem Phenomena.Morphology.Typology.german_ch80 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F80A.VerbalNumberAndSuppletion) => Core.Morphology.fromWALS80A x.value) (Core.WALS.F80A.lookup "ger") = some Core.Morphology.VerbalNumber.none

theorem Phenomena.Morphology.Typology.spanish_ch80 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F80A.VerbalNumberAndSuppletion) => Core.Morphology.fromWALS80A x.value) (Core.WALS.F80A.lookup "spa") = some Core.Morphology.VerbalNumber.none

theorem Phenomena.Morphology.Typology.ch21b_size : Phenomena.Morphology.Typology.ch21b✝.length = 160

theorem Phenomena.Morphology.Typology.ch62_size : Phenomena.Morphology.Typology.ch62✝.length = 168

theorem Phenomena.Morphology.Typology.ch79a_size : Phenomena.Morphology.Typology.ch79a✝.length = 193

theorem Phenomena.Morphology.Typology.ch79b_size : Phenomena.Morphology.Typology.ch79b✝.length = 193

theorem Phenomena.Morphology.Typology.ch80_size : Phenomena.Morphology.Typology.ch80✝.length = 193

theorem Phenomena.Morphology.Typology.ch21b_count_monoexponentialTam : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F21B.ExponenceOfTenseAspectMoodInflection) => x.value == Core.WALS.F21B.ExponenceOfTenseAspectMoodInflection.monoexponentialTam) Phenomena.Morphology.Typology.ch21b✝).length = 127

theorem Phenomena.Morphology.Typology.ch21b_count_tamAgreement : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F21B.ExponenceOfTenseAspectMoodInflection) => x.value == Core.WALS.F21B.ExponenceOfTenseAspectMoodInflection.tamAgreement) Phenomena.Morphology.Typology.ch21b✝).length = 19

theorem Phenomena.Morphology.Typology.ch21b_count_tamAgreementDiathesis : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F21B.ExponenceOfTenseAspectMoodInflection) => x.value == Core.WALS.F21B.ExponenceOfTenseAspectMoodInflection.tamAgreementDiathesis) Phenomena.Morphology.Typology.ch21b✝).length = 4

theorem Phenomena.Morphology.Typology.ch21b_count_tamAgreementConstruct : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F21B.ExponenceOfTenseAspectMoodInflection) => x.value == Core.WALS.F21B.ExponenceOfTenseAspectMoodInflection.tamAgreementConstruct) Phenomena.Morphology.Typology.ch21b✝).length = 1

theorem Phenomena.Morphology.Typology.ch21b_count_tamPolarity : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F21B.ExponenceOfTenseAspectMoodInflection) => x.value == Core.WALS.F21B.ExponenceOfTenseAspectMoodInflection.tamPolarity) Phenomena.Morphology.Typology.ch21b✝).length = 5

theorem Phenomena.Morphology.Typology.ch21b_count_noTam : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F21B.ExponenceOfTenseAspectMoodInflection) => x.value == Core.WALS.F21B.ExponenceOfTenseAspectMoodInflection.noTam) Phenomena.Morphology.Typology.ch21b✝).length = 4

theorem Phenomena.Morphology.Typology.ch62_count_sentential : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F62A.ActionNominalConstructions) => x.value == Core.WALS.F62A.ActionNominalConstructions.sentential) Phenomena.Morphology.Typology.ch62✝).length = 25

theorem Phenomena.Morphology.Typology.ch62_count_possessiveAccusative : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F62A.ActionNominalConstructions) => x.value == Core.WALS.F62A.ActionNominalConstructions.possessiveAccusative) Phenomena.Morphology.Typology.ch62✝).length = 29

theorem Phenomena.Morphology.Typology.ch62_count_ergativePossessive : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F62A.ActionNominalConstructions) => x.value == Core.WALS.F62A.ActionNominalConstructions.ergativePossessive) Phenomena.Morphology.Typology.ch62✝).length = 21

theorem Phenomena.Morphology.Typology.ch62_count_doublePossessive : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F62A.ActionNominalConstructions) => x.value == Core.WALS.F62A.ActionNominalConstructions.doublePossessive) Phenomena.Morphology.Typology.ch62✝).length = 7

theorem Phenomena.Morphology.Typology.ch62_count_other : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F62A.ActionNominalConstructions) => x.value == Core.WALS.F62A.ActionNominalConstructions.other) Phenomena.Morphology.Typology.ch62✝).length = 6

theorem Phenomena.Morphology.Typology.ch62_count_mixed : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F62A.ActionNominalConstructions) => x.value == Core.WALS.F62A.ActionNominalConstructions.mixed) Phenomena.Morphology.Typology.ch62✝).length = 14

theorem Phenomena.Morphology.Typology.ch62_count_restricted : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F62A.ActionNominalConstructions) => x.value == Core.WALS.F62A.ActionNominalConstructions.restricted) Phenomena.Morphology.Typology.ch62✝).length = 24

theorem Phenomena.Morphology.Typology.ch62_count_noActionNominals : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F62A.ActionNominalConstructions) => x.value == Core.WALS.F62A.ActionNominalConstructions.noActionNominals) Phenomena.Morphology.Typology.ch62✝).length = 42

theorem Phenomena.Morphology.Typology.ch79a_count_tense : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F79A.SuppletionAccordingToTenseAndAspect) => x.value == Core.WALS.F79A.SuppletionAccordingToTenseAndAspect.tense) Phenomena.Morphology.Typology.ch79a✝).length = 36

theorem Phenomena.Morphology.Typology.ch79a_count_aspect : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F79A.SuppletionAccordingToTenseAndAspect) => x.value == Core.WALS.F79A.SuppletionAccordingToTenseAndAspect.aspect) Phenomena.Morphology.Typology.ch79a✝).length = 10

theorem Phenomena.Morphology.Typology.ch79a_count_tenseAndAspect : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F79A.SuppletionAccordingToTenseAndAspect) => x.value == Core.WALS.F79A.SuppletionAccordingToTenseAndAspect.tenseAndAspect) Phenomena.Morphology.Typology.ch79a✝).length = 24

theorem Phenomena.Morphology.Typology.ch79a_count_none : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F79A.SuppletionAccordingToTenseAndAspect) => x.value == Core.WALS.F79A.SuppletionAccordingToTenseAndAspect.none) Phenomena.Morphology.Typology.ch79a✝).length = 123

theorem Phenomena.Morphology.Typology.ch79b_count_alternating : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F79B.SuppletionInImperativesAndHortatives) => x.value == Core.WALS.F79B.SuppletionInImperativesAndHortatives.aRegularAndASuppletiveFormAlternate) Phenomena.Morphology.Typology.ch79b✝).length = 8

theorem Phenomena.Morphology.Typology.ch79b_count_imperative : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F79B.SuppletionInImperativesAndHortatives) => x.value == Core.WALS.F79B.SuppletionInImperativesAndHortatives.imperative) Phenomena.Morphology.Typology.ch79b✝).length = 29

theorem Phenomena.Morphology.Typology.ch79b_count_hortative : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F79B.SuppletionInImperativesAndHortatives) => x.value == Core.WALS.F79B.SuppletionInImperativesAndHortatives.hortative) Phenomena.Morphology.Typology.ch79b✝).length = 2

theorem Phenomena.Morphology.Typology.ch79b_count_imperativeAndHortative : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F79B.SuppletionInImperativesAndHortatives) => x.value == Core.WALS.F79B.SuppletionInImperativesAndHortatives.imperativeAndHortative) Phenomena.Morphology.Typology.ch79b✝).length = 1

theorem Phenomena.Morphology.Typology.ch79b_count_none : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F79B.SuppletionInImperativesAndHortatives) => x.value == Core.WALS.F79B.SuppletionInImperativesAndHortatives.none) Phenomena.Morphology.Typology.ch79b✝).length = 153

theorem Phenomena.Morphology.Typology.ch80_count_none : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F80A.VerbalNumberAndSuppletion) => x.value == Core.WALS.F80A.VerbalNumberAndSuppletion.none) Phenomena.Morphology.Typology.ch80✝).length = 159

theorem Phenomena.Morphology.Typology.ch80_count_pairsNoSuppletion : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F80A.VerbalNumberAndSuppletion) => x.value == Core.WALS.F80A.VerbalNumberAndSuppletion.singularPluralPairsNoSuppletion) Phenomena.Morphology.Typology.ch80✝).length = 12

theorem Phenomena.Morphology.Typology.ch80_count_pairsSuppletion : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F80A.VerbalNumberAndSuppletion) => x.value == Core.WALS.F80A.VerbalNumberAndSuppletion.singularPluralPairsSuppletion) Phenomena.Morphology.Typology.ch80✝).length = 15

theorem Phenomena.Morphology.Typology.ch80_count_triplesNoSuppletion : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F80A.VerbalNumberAndSuppletion) => x.value == Core.WALS.F80A.VerbalNumberAndSuppletion.singularDualPluralTriplesNoSuppletion) Phenomena.Morphology.Typology.ch80✝).length = 5

theorem Phenomena.Morphology.Typology.ch80_count_triplesSuppletion : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F80A.VerbalNumberAndSuppletion) => x.value == Core.WALS.F80A.VerbalNumberAndSuppletion.singularDualPluralTriplesSuppletion) Phenomena.Morphology.Typology.ch80✝).length = 2