inductive Minimalism.Position : Type

Positions in the clause structure

• specCP : Position
• headC : Position
• specTP : Position
• headT : Position
• specvP : Position
• headv : Position
• headV : Position

instance Minimalism.instReprPosition : Repr Position

Equations

• Minimalism.instReprPosition = { reprPrec := Minimalism.instReprPosition.repr }

def Minimalism.instReprPosition.repr : Position → Nat → Std.Format

Equations

• Minimalism.instReprPosition.repr Minimalism.Position.specCP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Position.specCP")).group prec✝
• Minimalism.instReprPosition.repr Minimalism.Position.headC prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Position.headC")).group prec✝
• Minimalism.instReprPosition.repr Minimalism.Position.specTP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Position.specTP")).group prec✝
• Minimalism.instReprPosition.repr Minimalism.Position.headT prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Position.headT")).group prec✝
• Minimalism.instReprPosition.repr Minimalism.Position.specvP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Position.specvP")).group prec✝
• Minimalism.instReprPosition.repr Minimalism.Position.headv prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Position.headv")).group prec✝
• Minimalism.instReprPosition.repr Minimalism.Position.headV prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.Position.headV")).group prec✝

instance Minimalism.instDecidableEqPosition : DecidableEq Position

Equations

• Minimalism.instDecidableEqPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Minimalism.dominates : Position → Position → Bool

Equations

• Minimalism.dominates Minimalism.Position.specCP x✝ = (x✝ != Minimalism.Position.specCP)
• Minimalism.dominates Minimalism.Position.headC x✝ = (x✝ != Minimalism.Position.specCP && x✝ != Minimalism.Position.headC)
• Minimalism.dominates Minimalism.Position.specTP x✝ = (x✝ == Minimalism.Position.specvP || x✝ == Minimalism.Position.headv || x✝ == Minimalism.Position.headV)
• Minimalism.dominates Minimalism.Position.headT x✝ = (x✝ == Minimalism.Position.specvP || x✝ == Minimalism.Position.headv || x✝ == Minimalism.Position.headV)
• Minimalism.dominates Minimalism.Position.specvP x✝ = (x✝ == Minimalism.Position.headv || x✝ == Minimalism.Position.headV)
• Minimalism.dominates Minimalism.Position.headv Minimalism.Position.headV = true
• Minimalism.dominates x✝¹ x✝ = false

def Minimalism.structurallyPrecedes : Position → Position → Bool

Structural precedence in English (Spec-Head-Complement order)

Equations

• Minimalism.structurallyPrecedes Minimalism.Position.specCP Minimalism.Position.headC = true
• Minimalism.structurallyPrecedes Minimalism.Position.specCP Minimalism.Position.specTP = true
• Minimalism.structurallyPrecedes Minimalism.Position.specCP Minimalism.Position.headT = true
• Minimalism.structurallyPrecedes Minimalism.Position.specCP Minimalism.Position.specvP = true
• Minimalism.structurallyPrecedes Minimalism.Position.specCP Minimalism.Position.headv = true
• Minimalism.structurallyPrecedes Minimalism.Position.specCP Minimalism.Position.headV = true
• Minimalism.structurallyPrecedes Minimalism.Position.headC Minimalism.Position.specTP = true
• Minimalism.structurallyPrecedes Minimalism.Position.headC Minimalism.Position.headT = true
• Minimalism.structurallyPrecedes Minimalism.Position.headC Minimalism.Position.specvP = true
• Minimalism.structurallyPrecedes Minimalism.Position.headC Minimalism.Position.headv = true
• Minimalism.structurallyPrecedes Minimalism.Position.headC Minimalism.Position.headV = true
• Minimalism.structurallyPrecedes Minimalism.Position.specTP Minimalism.Position.headT = true
• Minimalism.structurallyPrecedes Minimalism.Position.specTP Minimalism.Position.specvP = true
• Minimalism.structurallyPrecedes Minimalism.Position.specTP Minimalism.Position.headv = true
• Minimalism.structurallyPrecedes Minimalism.Position.specTP Minimalism.Position.headV = true
• Minimalism.structurallyPrecedes Minimalism.Position.headT Minimalism.Position.specvP = true
• Minimalism.structurallyPrecedes Minimalism.Position.headT Minimalism.Position.headv = true
• Minimalism.structurallyPrecedes Minimalism.Position.headT Minimalism.Position.headV = true
• Minimalism.structurallyPrecedes Minimalism.Position.specvP Minimalism.Position.headv = true
• Minimalism.structurallyPrecedes Minimalism.Position.specvP Minimalism.Position.headV = true
• Minimalism.structurallyPrecedes Minimalism.Position.headv Minimalism.Position.headV = true
• Minimalism.structurallyPrecedes x✝¹ x✝ = false

theorem Minimalism.subject_precedes_t_base : structurallyPrecedes Position.specTP Position.headT = true

theorem Minimalism.c_precedes_subject : structurallyPrecedes Position.headC Position.specTP = true

theorem Minimalism.c_precedes_t : structurallyPrecedes Position.headC Position.headT = true

theorem Minimalism.spec_cp_is_first : structurallyPrecedes Position.specCP Position.headC = true ∧ structurallyPrecedes Position.specCP Position.specTP = true ∧ structurallyPrecedes Position.specCP Position.headT = true

inductive Minimalism.HeadPosition : Type

• base : Position → HeadPosition
• movedTo : Position → HeadPosition

def Minimalism.instReprHeadPosition.repr : HeadPosition → Nat → Std.Format

Equations

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

instance Minimalism.instReprHeadPosition : Repr HeadPosition

Equations

• Minimalism.instReprHeadPosition = { reprPrec := Minimalism.instReprHeadPosition.repr }

instance Minimalism.instDecidableEqHeadPosition : DecidableEq HeadPosition

Equations

• Minimalism.instDecidableEqHeadPosition = Minimalism.instDecidableEqHeadPosition.decEq

def Minimalism.instDecidableEqHeadPosition.decEq (x✝ x✝¹ : HeadPosition) : Decidable (x✝ = x✝¹)

Equations

• Minimalism.instDecidableEqHeadPosition.decEq (Minimalism.HeadPosition.base a) (Minimalism.HeadPosition.base b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Minimalism.instDecidableEqHeadPosition.decEq (Minimalism.HeadPosition.base a) (Minimalism.HeadPosition.movedTo a_1) = isFalse ⋯
• Minimalism.instDecidableEqHeadPosition.decEq (Minimalism.HeadPosition.movedTo a) (Minimalism.HeadPosition.base a_1) = isFalse ⋯
• Minimalism.instDecidableEqHeadPosition.decEq (Minimalism.HeadPosition.movedTo a) (Minimalism.HeadPosition.movedTo b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

inductive Minimalism.TPosition : Type

• inT : TPosition
• inC : TPosition

instance Minimalism.instReprTPosition : Repr TPosition

Equations

• Minimalism.instReprTPosition = { reprPrec := Minimalism.instReprTPosition.repr }

def Minimalism.instReprTPosition.repr : TPosition → Nat → Std.Format

Equations

• Minimalism.instReprTPosition.repr Minimalism.TPosition.inT prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.TPosition.inT")).group prec✝
• Minimalism.instReprTPosition.repr Minimalism.TPosition.inC prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.TPosition.inC")).group prec✝

instance Minimalism.instDecidableEqTPosition : DecidableEq TPosition

Equations

• Minimalism.instDecidableEqTPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Minimalism.tPronouncedAt (tPos : TPosition) : Position

Equations

• Minimalism.tPronouncedAt Minimalism.TPosition.inT = Minimalism.Position.headT
• Minimalism.tPronouncedAt Minimalism.TPosition.inC = Minimalism.Position.headC

theorem Minimalism.t_to_c_precedes_subject : structurallyPrecedes (tPronouncedAt TPosition.inC) Position.specTP = true

theorem Minimalism.subject_precedes_t_no_movement : structurallyPrecedes Position.specTP (tPronouncedAt TPosition.inT) = true

theorem Minimalism.t_to_c_reverses_order : structurallyPrecedes Position.specTP Position.headT = true ∧ structurallyPrecedes Position.headC Position.specTP = true

def Minimalism.tPrecedesSubject (tPos : TPosition) : Bool

Equations

• Minimalism.tPrecedesSubject tPos = Minimalism.structurallyPrecedes (Minimalism.tPronouncedAt tPos) Minimalism.Position.specTP

def Minimalism.subjectPrecedesT (tPos : TPosition) : Bool

Equations

• Minimalism.subjectPrecedesT tPos = Minimalism.structurallyPrecedes Minimalism.Position.specTP (Minimalism.tPronouncedAt tPos)

theorem Minimalism.t_to_c_gives_t_first : tPrecedesSubject TPosition.inC = true

theorem Minimalism.no_movement_gives_subj_first : subjectPrecedesT TPosition.inT = true