Hudson (2010): An Introduction to Word Grammar

This file formalizes the worked examples of Part I of [Hud10] on the default-inheritance substrate DefaultInheritance. Default inheritance is the book's engine. An exemplar inherits every property of the concepts above it in the isA taxonomy except those overridden lower down. So a penguin exemplar inherits lays eggs from bird but doesn't fly from penguin (Figure 2.8, inherited_flight_e2), and a diesel car exemplar runs on diesel rather than the default petrol (Figure 3.18, inherited_fuel_e). The book's searcher climbs the taxonomy from the exemplar and keeps the first answer it finds (Section 2.5.3). The substrate proves that this answer is an inherited one for every climb that starts at the bottom (DefaultInheritance.mem_inherited_of_find?_eq_some). Multiple inheritance can leave a conflict with no recognized resolution, the Nixon diamond of Figure 2.7. Nixon inherits both accepts war and rejects war as credulous conclusions and neither as a skeptical one (inherited_war_nixon, not_entails_war_nixon), and the two climbs that visit his parents in opposite orders find different answers (search_war_nixon). Nixon's own choice, a copy of accepts war at his node, settles the conflict (nixon_resolved). Choice sets keep such conflicts from arising. No one is both male and female, or both adult and child, so a property attached to the members of either choice set is never inherited twice, although man, boy, woman and girl each inherit from two concepts (Figure 3.9, subsingleton_inherited_sex, subsingleton_inherited_age).

Relational concepts are defined in terms of existing ones: parent merges mother and father, grandmother is the mother of a parent, and ancestor is the recursive closure of parent (Section 3.2.7, ancestor). The definition of grandmother is a relational Triangle, one node's two relations converging on a third, and the same triangle is the syntactic pattern of raising: an auxiliary's subject is also its valent's subject (Figure 7.6). Closing the asserted subjects under the triangle along the valent chain (raise) makes he the subject of every verb in He keeps seeming to have forgotten to go (Figure 7.12, he_subject_of_go).

Implementation notes

• A property is an attribute, a partial map from concepts to values, and two values compete when they are values of one attribute. The book's competition between links one of which isA the other (Section 3.5.3) is not modelled.
• Only exemplars inherit (Section 2.5). DefaultInheritance.inherited is defined at every concept, and the theorems query the exemplars.
• Each taxonomy is declared by its immediate isA links, and its order is their reflexive transitive closure (partialOrderOfCovers).
• The kinship system of Figure 8.16 is built from mother and father on an arbitrary type of people, with sex as predicates; the compositions are mathlib's Relation.Comp and Relation.TransGen.

References

• [Hud10]

Default inheritance

inductive Hudson2010.Bird : Type

The concepts of Figure 2.8: birds, the typical sparrow, the exceptional penguin, and an exemplar of each.

• bird : Bird
• sparrow : Bird
• penguin : Bird
• e1 : Bird
• e2 : Bird

@[instance_reducible]

instance Hudson2010.instDecidableEqBird : DecidableEq Bird

Equations

• Hudson2010.instDecidableEqBird x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Hudson2010.instFintypeBird : Fintype Bird

Equations

• Hudson2010.instFintypeBird = { elems := { val := ↑Hudson2010.Bird.enumList, nodup := Hudson2010.Bird.enumList_nodup }, complete := Hudson2010.instFintypeBird._proof_1 }

def Hudson2010.Bird.parents : Bird → List Bird

The concepts each concept of Figure 2.8 immediately isA.

Equations

• Hudson2010.Bird.bird.parents = []
• Hudson2010.Bird.sparrow.parents = [Hudson2010.Bird.bird]
• Hudson2010.Bird.penguin.parents = [Hudson2010.Bird.bird]
• Hudson2010.Bird.e1.parents = [Hudson2010.Bird.sparrow]
• Hudson2010.Bird.e2.parents = [Hudson2010.Bird.penguin]

def Hudson2010.Bird.rank : Bird → ℕ

The depth of a concept below bird.

Equations

• Hudson2010.Bird.bird.rank = 0
• Hudson2010.Bird.sparrow.rank = 1
• Hudson2010.Bird.penguin.rank = 1
• Hudson2010.Bird.e1.rank = 2
• Hudson2010.Bird.e2.rank = 2

@[instance_reducible]

instance Hudson2010.instPartialOrderBird : PartialOrder Bird

Equations

• Hudson2010.instPartialOrderBird = partialOrderOfCovers (fun (a b : Hudson2010.Bird) => b ∈ a.parents) Hudson2010.Bird.rank Hudson2010.instPartialOrderBird._proof_1

@[instance_reducible]

instance Hudson2010.instDecidableLEBird : DecidableLE Bird

Equations

• Hudson2010.instDecidableLEBird = decidableLEOfCovers [Hudson2010.Bird.bird, Hudson2010.Bird.sparrow, Hudson2010.Bird.penguin] Hudson2010.instDecidableLEBird._proof_1

inductive Hudson2010.Flight : Type

How a bird moves.

• flies : Flight
• doesntFly : Flight

@[instance_reducible]

instance Hudson2010.instDecidableEqFlight : DecidableEq Flight

Equations

• Hudson2010.instDecidableEqFlight x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Hudson2010.Reproduction : Type

How a bird reproduces.

• laysEggs : Reproduction

@[instance_reducible]

instance Hudson2010.instDecidableEqReproduction : DecidableEq Reproduction

Equations

• Hudson2010.instDecidableEqReproduction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Hudson2010.flight : Bird → Option Flight

Figure 2.8: birds fly, and penguins do not.

Equations

• Hudson2010.flight Hudson2010.Bird.bird = some Hudson2010.Flight.flies
• Hudson2010.flight Hudson2010.Bird.penguin = some Hudson2010.Flight.doesntFly
• Hudson2010.flight x✝ = none

def Hudson2010.reproduction : Bird → Option Reproduction

Figure 2.8: birds lay eggs.

Equations

• Hudson2010.reproduction Hudson2010.Bird.bird = some Hudson2010.Reproduction.laysEggs
• Hudson2010.reproduction x✝ = none

theorem Hudson2010.e2_le_bird : Bird.e2 ≤ Bird.bird

theorem Hudson2010.sparrow_not_le_penguin : ¬Bird.sparrow ≤ Bird.penguin

theorem Hudson2010.inherited_flight_e1 : DefaultInheritance.inherited flight Bird.e1 = {Flight.flies}

A sparrow exemplar inherits the default of bird.

theorem Hudson2010.inherited_flight_e2 : DefaultInheritance.inherited flight Bird.e2 = {Flight.doesntFly}

A penguin exemplar inherits doesn't fly, the lower of the competing properties (Section 2.5.3).

theorem Hudson2010.inherited_reproduction_e2 : DefaultInheritance.inherited reproduction Bird.e2 = {Reproduction.laysEggs}

The override leaves the other defaults intact: the exceptional penguin still inherits what bird specifies about reproduction.

inductive Hudson2010.Car : Type

The concepts of Figure 3.18: cars, the exceptional diesel car, and an exemplar of each.

• car : Car
• dieselCar : Car
• e : Car
• e' : Car

@[instance_reducible]

instance Hudson2010.instDecidableEqCar : DecidableEq Car

Equations

• Hudson2010.instDecidableEqCar x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Hudson2010.instFintypeCar : Fintype Car

Equations

• Hudson2010.instFintypeCar = { elems := { val := ↑Hudson2010.Car.enumList, nodup := Hudson2010.Car.enumList_nodup }, complete := Hudson2010.instFintypeCar._proof_1 }

def Hudson2010.Car.parents : Car → List Car

The concepts each concept of Figure 3.18 immediately isA.

Equations

• Hudson2010.Car.car.parents = []
• Hudson2010.Car.dieselCar.parents = [Hudson2010.Car.car]
• Hudson2010.Car.e'.parents = [Hudson2010.Car.car]
• Hudson2010.Car.e.parents = [Hudson2010.Car.dieselCar]

def Hudson2010.Car.rank : Car → ℕ

The depth of a concept below car.

Equations

• Hudson2010.Car.car.rank = 0
• Hudson2010.Car.dieselCar.rank = 1
• Hudson2010.Car.e'.rank = 1
• Hudson2010.Car.e.rank = 2

@[instance_reducible]

instance Hudson2010.instPartialOrderCar : PartialOrder Car

Equations

• Hudson2010.instPartialOrderCar = partialOrderOfCovers (fun (a b : Hudson2010.Car) => b ∈ a.parents) Hudson2010.Car.rank Hudson2010.instPartialOrderCar._proof_1

@[instance_reducible]

instance Hudson2010.instDecidableLECar : DecidableLE Car

Equations

• Hudson2010.instDecidableLECar = decidableLEOfCovers [Hudson2010.Car.car, Hudson2010.Car.dieselCar] Hudson2010.instDecidableLECar._proof_1

inductive Hudson2010.Fuel : Type

A car's fuel.

• petrol : Fuel
• diesel : Fuel

@[instance_reducible]

instance Hudson2010.instDecidableEqFuel : DecidableEq Fuel

Equations

• Hudson2010.instDecidableEqFuel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Hudson2010.fuel : Car → Option Fuel

Figure 3.18: petrol is the default car fuel and diesel the exception.

Equations

• Hudson2010.fuel Hudson2010.Car.car = some Hudson2010.Fuel.petrol
• Hudson2010.fuel Hudson2010.Car.dieselCar = some Hudson2010.Fuel.diesel
• Hudson2010.fuel x✝ = none

theorem Hudson2010.inherited_fuel_e : DefaultInheritance.inherited fuel Car.e = {Fuel.diesel}

The diesel car exemplar inherits the link to diesel before it reaches petrol.

theorem Hudson2010.inherited_fuel_e' : DefaultInheritance.inherited fuel Car.e' = {Fuel.petrol}

The Nixon diamond

inductive Hudson2010.Person : Type

The concepts of Figure 2.7: Nixon is both a Republican and a Quaker.

• person : Person
• republican : Person
• quaker : Person
• nixon : Person

@[instance_reducible]

instance Hudson2010.instDecidableEqPerson : DecidableEq Person

Equations

• Hudson2010.instDecidableEqPerson x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Hudson2010.instFintypePerson : Fintype Person

Equations

• Hudson2010.instFintypePerson = { elems := { val := ↑Hudson2010.Person.enumList, nodup := Hudson2010.Person.enumList_nodup }, complete := Hudson2010.instFintypePerson._proof_1 }

def Hudson2010.Person.parents : Person → List Person

The concepts each concept of Figure 2.7 immediately isA.

Equations

• Hudson2010.Person.person.parents = []
• Hudson2010.Person.republican.parents = [Hudson2010.Person.person]
• Hudson2010.Person.quaker.parents = [Hudson2010.Person.person]
• Hudson2010.Person.nixon.parents = [Hudson2010.Person.republican, Hudson2010.Person.quaker]

def Hudson2010.Person.rank : Person → ℕ

The depth of a concept below person.

Equations

• Hudson2010.Person.person.rank = 0
• Hudson2010.Person.republican.rank = 1
• Hudson2010.Person.quaker.rank = 1
• Hudson2010.Person.nixon.rank = 2

@[instance_reducible]

instance Hudson2010.instPartialOrderPerson : PartialOrder Person

Equations

• Hudson2010.instPartialOrderPerson = partialOrderOfCovers (fun (a b : Hudson2010.Person) => b ∈ a.parents) Hudson2010.Person.rank Hudson2010.instPartialOrderPerson._proof_1

@[instance_reducible]

instance Hudson2010.instDecidableLEPerson : DecidableLE Person

Equations

• Hudson2010.instDecidableLEPerson = decidableLEOfCovers [Hudson2010.Person.person, Hudson2010.Person.republican, Hudson2010.Person.quaker] Hudson2010.instDecidableLEPerson._proof_1

inductive Hudson2010.Stance : Type

A view of war.

• accepts : Stance
• rejects : Stance

@[instance_reducible]

instance Hudson2010.instDecidableEqStance : DecidableEq Stance

Equations

• Hudson2010.instDecidableEqStance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Hudson2010.war : Person → Option Stance

Figure 2.7: Republicans accept war and Quakers reject it.

Equations

• Hudson2010.war Hudson2010.Person.republican = some Hudson2010.Stance.accepts
• Hudson2010.war Hudson2010.Person.quaker = some Hudson2010.Stance.rejects
• Hudson2010.war x✝ = none

theorem Hudson2010.inherited_war_nixon : DefaultInheritance.inherited war Person.nixon = {Stance.accepts, Stance.rejects}

Nixon inherits both views of war, a conflict with no recognized resolution (Section 2.4.2): each view is a credulous conclusion, and neither is a skeptical one.

theorem Hudson2010.not_entails_war_nixon (s : Stance) : ¬Nonmonotonic.Entails inferInstance (DefaultInheritance.specifiers war Person.nixon) {m : Person | war m = some s}

Neither view of war is a skeptical conclusion: Nixon's specifiers preferentially entail neither.

theorem Hudson2010.search_war_nixon : (List.find? (fun (x : Person) => decide (x ∈ DefaultInheritance.specifiers war Person.nixon)) [Person.nixon, Person.republican, Person.quaker, Person.person]).bind war = some Stance.accepts ∧ (List.find? (fun (x : Person) => decide (x ∈ DefaultInheritance.specifiers war Person.nixon)) [Person.nixon, Person.quaker, Person.republican, Person.person]).bind war = some Stance.rejects

Climbing from Nixon through Republican first finds accepts war, and through Quaker first finds rejects war. Both climbs start at the bottom, so both answers are inherited.

theorem Hudson2010.nixon_resolved : DefaultInheritance.inherited (Function.update war Person.nixon (some Stance.accepts)) Person.nixon = {Stance.accepts}

Nixon's resolution: a copy of accepts war at his own node wins (Section 2.4.2).

Choice sets

inductive Hudson2010.Human : Type

The concepts of Figure 3.9: a person is male or female and adult or child, and man, boy, woman and girl are the four combinations.

• person : Human
• male : Human
• female : Human
• adult : Human
• child : Human
• man : Human
• boy : Human
• woman : Human
• girl : Human

@[instance_reducible]

instance Hudson2010.instDecidableEqHuman : DecidableEq Human

Equations

• Hudson2010.instDecidableEqHuman x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Hudson2010.instFintypeHuman : Fintype Human

Equations

• Hudson2010.instFintypeHuman = { elems := { val := ↑Hudson2010.Human.enumList, nodup := Hudson2010.Human.enumList_nodup }, complete := Hudson2010.instFintypeHuman._proof_1 }

def Hudson2010.Human.parents : Human → List Human

The concepts each concept of Figure 3.9 immediately isA.

Equations

• Hudson2010.Human.person.parents = []
• Hudson2010.Human.male.parents = [Hudson2010.Human.person]
• Hudson2010.Human.female.parents = [Hudson2010.Human.person]
• Hudson2010.Human.adult.parents = [Hudson2010.Human.person]
• Hudson2010.Human.child.parents = [Hudson2010.Human.person]
• Hudson2010.Human.man.parents = [Hudson2010.Human.male, Hudson2010.Human.adult]
• Hudson2010.Human.boy.parents = [Hudson2010.Human.male, Hudson2010.Human.child]
• Hudson2010.Human.woman.parents = [Hudson2010.Human.female, Hudson2010.Human.adult]
• Hudson2010.Human.girl.parents = [Hudson2010.Human.female, Hudson2010.Human.child]

def Hudson2010.Human.rank : Human → ℕ

The depth of a concept below person.

Equations

• Hudson2010.Human.person.rank = 0
• Hudson2010.Human.male.rank = 1
• Hudson2010.Human.female.rank = 1
• Hudson2010.Human.adult.rank = 1
• Hudson2010.Human.child.rank = 1
• Hudson2010.Human.man.rank = 2
• Hudson2010.Human.boy.rank = 2
• Hudson2010.Human.woman.rank = 2
• Hudson2010.Human.girl.rank = 2

@[instance_reducible]

instance Hudson2010.instPartialOrderHuman : PartialOrder Human

Equations

• Hudson2010.instPartialOrderHuman = partialOrderOfCovers (fun (a b : Hudson2010.Human) => b ∈ a.parents) Hudson2010.Human.rank Hudson2010.instPartialOrderHuman._proof_1

@[instance_reducible]

instance Hudson2010.instDecidableLEHuman : DecidableLE Human

Equations

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

def Hudson2010.sex : Set Human

The choice set sex of Figure 3.8.

Equations

• Hudson2010.sex = {Hudson2010.Human.male, Hudson2010.Human.female}

def Hudson2010.age : Set Human

The choice set age of Figure 3.9.

Equations

• Hudson2010.age = {Hudson2010.Human.adult, Hudson2010.Human.child}

theorem Hudson2010.pairwiseDisjoint_sex : sex.PairwiseDisjoint Set.Iic

Only one member of a choice set may be chosen (Section 3.3.2): no concept isA both male and female.

theorem Hudson2010.pairwiseDisjoint_age : age.PairwiseDisjoint Set.Iic

No concept isA both adult and child.

theorem Hudson2010.subsingleton_inherited_sex {β : Type u_1} {att : Human → Option β} (h : ∀ (m : Human), (att m).isSome = true → m ∈ sex) (a : Human) : (DefaultInheritance.inherited att a).Subsingleton

A property attached only to the members of the choice set sex is inherited at most once (Section 2.4.3).

theorem Hudson2010.subsingleton_inherited_age {β : Type u_1} {att : Human → Option β} (h : ∀ (m : Human), (att m).isSome = true → m ∈ age) (a : Human) : (DefaultInheritance.inherited att a).Subsingleton

A property attached only to the members of the choice set age is inherited at most once.

Relational concepts

def Hudson2010.parent {α : Type u_1} (mother father : α → α → Prop) (x p : α) : Prop

Figure 8.16 (a): a person's parent is either their mother or their father.

Equations

• Hudson2010.parent mother father x p = (mother x p ∨ father x p)

def Hudson2010.child {α : Type u_1} (mother father : α → α → Prop) (x c : α) : Prop

Figure 8.16 (b): a person's child is anyone whose parent they are.

Equations

• Hudson2010.child mother father x c = Hudson2010.parent mother father c x

def Hudson2010.grandmother {α : Type u_1} (mother father : α → α → Prop) : α → α → Prop

Figure 3.7: a grandmother is the mother of a parent, a relational triangle.

Equations

• Hudson2010.grandmother mother father = Relation.Comp (Hudson2010.parent mother father) mother

def Hudson2010.grandparent {α : Type u_1} (mother father : α → α → Prop) : α → α → Prop

Figure 3.17: a grandparent is a parent's parent.

Equations

• Hudson2010.grandparent mother father = Relation.Comp (Hudson2010.parent mother father) (Hudson2010.parent mother father)

theorem Hudson2010.comp_grandparent_parent {α : Type u_1} (mother father : α → α → Prop) : Relation.Comp (grandparent mother father) (parent mother father) = Relation.Comp (parent mother father) (Relation.Comp (parent mother father) (parent mother father))

Figure 3.17: a great-grandparent is a grandparent's parent, and the Recycling Principle of Section 3.5.2 builds it on grandparent rather than as the parent of a parent of a parent, to which it is nonetheless equal.

def Hudson2010.ancestor {α : Type u_1} (mother father : α → α → Prop) : α → α → Prop

Section 3.2.7: a person's ancestor is either their parent or an ancestor of their parent, the recursive definition.

Equations

• Hudson2010.ancestor mother father = Relation.TransGen (Hudson2010.parent mother father)

theorem Hudson2010.ancestor_iff {α : Type u_1} (mother father : α → α → Prop) (x a : α) : ancestor mother father x a ↔ parent mother father x a ∨ ∃ (p : α), parent mother father x p ∧ ancestor mother father p a

theorem Hudson2010.ancestor_of_grandparent {α : Type u_1} (mother father : α → α → Prop) {x g : α} (h : grandparent mother father x g) : ancestor mother father x g

A grandparent is an ancestor.

def Hudson2010.brother {α : Type u_1} (mother father : α → α → Prop) (male : α → Prop) (x b : α) : Prop

Figure 8.16 (c): brothers and sisters are the sons and daughters of a parent.

Equations

• Hudson2010.brother mother father male x b = (Relation.Comp (Hudson2010.parent mother father) (Hudson2010.child mother father) x b ∧ male b ∧ x ≠ b)

def Hudson2010.sister {α : Type u_1} (mother father : α → α → Prop) (female : α → Prop) (x s : α) : Prop

Equations

• Hudson2010.sister mother father female x s = (Relation.Comp (Hudson2010.parent mother father) (Hudson2010.child mother father) x s ∧ female s ∧ x ≠ s)

def Hudson2010.uncle {α : Type u_1} (mother father : α → α → Prop) (male : α → Prop) : α → α → Prop

Figure 8.16 (d): uncles and aunts are the brothers and sisters of a parent.

Equations

• Hudson2010.uncle mother father male = Relation.Comp (Hudson2010.parent mother father) (Hudson2010.brother mother father male)

def Hudson2010.aunt {α : Type u_1} (mother father : α → α → Prop) (female : α → Prop) : α → α → Prop

Equations

• Hudson2010.aunt mother father female = Relation.Comp (Hudson2010.parent mother father) (Hudson2010.sister mother father female)

theorem Hudson2010.uncle_of_parent_brother {α : Type u_1} (mother father : α → α → Prop) (male : α → Prop) {x p u : α} (hp : parent mother father x p) (hb : brother mother father male p u) : uncle mother father male x u

A parent's brother is an uncle, though not conversely once Figure 8.16 (e) extends the relation to the husbands of aunts.

Triangles in kinship and in syntax

def Hudson2010.Triangle {α : Type u_1} (r₁ r₂ r₃ : α → α → Prop) : Prop

The triangle of Figure 7.6: a node's r₁ value and r₂ value stand in r₃.

Equations

• Hudson2010.Triangle r₁ r₂ r₃ = ∀ (x y z : α), r₁ x y → r₂ x z → r₃ y z

theorem Hudson2010.triangle_grandmother {α : Type u_1} (mother father : α → α → Prop) : Triangle (child mother father) mother (grandmother mother father)

In kinship: a person's mother is their child's grandmother.

def Hudson2010.Raising {α : Type u_1} (valent subj : α → α → Prop) : Prop

Raising, the syntactic triangle: a word's subject is also its valent's subject.

Equations

• Hudson2010.Raising valent subj = Hudson2010.Triangle valent subj subj

def Hudson2010.raise {α : Type u_1} (valent subj : α → α → Prop) (v s : α) : Prop

The subjects derived from the asserted ones by closing under the triangle along the valent chain.

Equations

• Hudson2010.raise valent subj v s = ∃ (h : α), subj h s ∧ Relation.ReflTransGen valent h v

theorem Hudson2010.subj_le_raise {α : Type u_1} (valent subj : α → α → Prop) (x s : α) : subj x s → raise valent subj x s

theorem Hudson2010.raising_raise {α : Type u_1} (valent subj : α → α → Prop) : Raising valent (raise valent subj)

The derived subjects satisfy the triangle.

theorem Hudson2010.raise_le_of_raising {α : Type u_1} (valent subj : α → α → Prop) {S : α → α → Prop} (hS : Raising valent S) (hsubj : ∀ (x s : α), subj x s → S x s) (v s : α) : raise valent subj v s → S v s

Any subject relation containing the asserted subjects and closed under the triangle contains the derived subjects: raise is the least closure.

theorem Hudson2010.raise_of_transGen {α : Type u_1} (valent subj : α → α → Prop) {h v s : α} (hs : subj h s) (hchain : Relation.TransGen valent h v) : raise valent subj v s

Section 7.2.6: the subject is shared down a chain of valents, however long, the recursion of Figure 7.12.

Figure 7.12

inductive Hudson2010.W : Type

The words of He keeps seeming to have forgotten to go.

• he : W
• keeps : W
• seeming : W
• to₁ : W
• have : W
• forgotten : W
• to₂ : W
• go : W

@[instance_reducible]

instance Hudson2010.instDecidableEqW : DecidableEq W

Equations

• Hudson2010.instDecidableEqW x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Hudson2010.instReprW : Repr W

Equations

• Hudson2010.instReprW = { reprPrec := Hudson2010.instReprW.repr }

def Hudson2010.instReprW.repr : W → ℕ → Std.Format

Equations

• Hudson2010.instReprW.repr Hudson2010.W.he prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hudson2010.W.he")).group prec✝
• Hudson2010.instReprW.repr Hudson2010.W.keeps prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hudson2010.W.keeps")).group prec✝
• Hudson2010.instReprW.repr Hudson2010.W.seeming prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hudson2010.W.seeming")).group prec✝
• Hudson2010.instReprW.repr Hudson2010.W.to₁ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hudson2010.W.to₁")).group prec✝
• Hudson2010.instReprW.repr Hudson2010.W.have prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hudson2010.W.have")).group prec✝
• Hudson2010.instReprW.repr Hudson2010.W.forgotten prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hudson2010.W.forgotten")).group prec✝
• Hudson2010.instReprW.repr Hudson2010.W.to₂ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hudson2010.W.to₂")).group prec✝
• Hudson2010.instReprW.repr Hudson2010.W.go prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hudson2010.W.go")).group prec✝

def Hudson2010.valent : W → W → Prop

The valent chain of Figure 7.12, each verb's valent the next.

Equations

• Hudson2010.valent Hudson2010.W.keeps Hudson2010.W.seeming = True
• Hudson2010.valent Hudson2010.W.seeming Hudson2010.W.to₁ = True
• Hudson2010.valent Hudson2010.W.to₁ Hudson2010.W.have = True
• Hudson2010.valent Hudson2010.W.have Hudson2010.W.forgotten = True
• Hudson2010.valent Hudson2010.W.forgotten Hudson2010.W.to₂ = True
• Hudson2010.valent Hudson2010.W.to₂ Hudson2010.W.go = True
• Hudson2010.valent x✝¹ x✝ = False

def Hudson2010.asserted : W → W → Prop

The one asserted subject: he is the subject of keeps.

Equations

• Hudson2010.asserted Hudson2010.W.keeps Hudson2010.W.he = True
• Hudson2010.asserted x✝¹ x✝ = False

theorem Hudson2010.he_subject_of_go : raise valent asserted W.go W.he

He is the subject of go, six triangles down the chain.