@cite{goldberg-jackendoff-2004}: The English Resultative as a Family of Constructions

@cite{goldberg-jackendoff-2004}

Paper data and per-datum verifications for @cite{goldberg-jackendoff-2004}. The construction-theoretic primitives (ResultativeSubconstruction, SubeventDesc, the fusion machinery, the universal-quantifier theorems) live in Theories/Syntax/ConstructionGrammar/Resultatives.lean, which this file imports.

Key claims

1. The English resultative is not one construction but a family of four subconstructions organized along two dimensions: causative/noncausative × property/path RP
2. Every resultative has a dual subevent structure: a verbal subevent (from the verb) and a constructional subevent (CAUSE + BECOME/GO from the construction)
3. The verbal and constructional subevents are linked by typed semantic relations: MEANS, RESULT, INSTANCE, or CO-OCCURRENCE
4. Full Argument Realization (FAR): all obligatory arguments of both verb and construction must be syntactically realized; shared arguments fuse
5. Semantic Coherence: verb role rV and construction role rC may fuse only if rV is construable as an instance of rC
6. Aspectual constraint: resultatives are telic iff the RP denotes a bounded path/property
7. Temporal constraint: the constructional subevent cannot temporally precede the verbal subevent

File contents

This file holds:

• The paper's eight resultative entries (hammerFlat, kickIntoField, …) and the allEntries list — concrete data points the paper discusses.
• Per-datum verification theorems demonstrating the paper's data is consistent with the construction theory.
• A separate empirical-data layer (ResultativeType, ResultativeDatum, allExamples, aspectualContrasts) holding theory-neutral grammaticality judgments and aspectual contrasts drawn from §§2–8 of the paper.

Empirical data: resultative entries

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.hammerFlat : ConstructionGrammar.Resultatives.ResultativeEntry

Equations

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

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.kickIntoField : ConstructionGrammar.Resultatives.ResultativeEntry

Equations

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

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.freezeSolid : ConstructionGrammar.Resultatives.ResultativeEntry

Equations

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

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.rollIntoField : ConstructionGrammar.Resultatives.ResultativeEntry

Equations

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

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.drinkSick : ConstructionGrammar.Resultatives.ResultativeEntry

Equations

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

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.laughSilly : ConstructionGrammar.Resultatives.ResultativeEntry

Equations

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

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.swingShut : ConstructionGrammar.Resultatives.ResultativeEntry

Equations

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

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.wipeClean : ConstructionGrammar.Resultatives.ResultativeEntry

Equations

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

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.allEntries : List ConstructionGrammar.Resultatives.ResultativeEntry

All resultative entries.

Equations

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

Per-datum verification theorems

theorem Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.hammerFlat_is_causativeProperty : hammerFlat.subconstruction = ConstructionGrammar.Resultatives.ResultativeSubconstruction.causativeProperty

theorem Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.kickIntoField_is_causativePath : kickIntoField.subconstruction = ConstructionGrammar.Resultatives.ResultativeSubconstruction.causativePath

theorem Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.freezeSolid_is_noncausativeProperty : freezeSolid.subconstruction = ConstructionGrammar.Resultatives.ResultativeSubconstruction.noncausativeProperty

theorem Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.rollIntoField_is_noncausativePath : rollIntoField.subconstruction = ConstructionGrammar.Resultatives.ResultativeSubconstruction.noncausativePath

theorem Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.hammerFlat_means : hammerFlat.subeventRelation = ConstructionGrammar.Resultatives.SubeventRelation.means

theorem Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.freezeSolid_means : freezeSolid.subeventRelation = ConstructionGrammar.Resultatives.SubeventRelation.means

theorem Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.drinkSick_means : drinkSick.subeventRelation = ConstructionGrammar.Resultatives.SubeventRelation.means

theorem Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.all_core_entries_use_means : (allEntries.all fun (x : ConstructionGrammar.Resultatives.ResultativeEntry) => x.subeventRelation == ConstructionGrammar.Resultatives.SubeventRelation.means) = true

All four core subconstructions use MEANS (§3, summary 97a–d). RESULT is reserved for sound-emission and disappearance subconstructions.

theorem Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.causative_entries_have_cause : ((List.filter (fun (x : ConstructionGrammar.Resultatives.ResultativeEntry) => x.subconstruction.isCausative) allEntries).all fun (x : ConstructionGrammar.Resultatives.ResultativeEntry) => x.dualSubevent.constructional.hasCause) = true

Causative entries have CAUSE in their derived constructional subevent.

theorem Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.noncausative_entries_no_cause : ((List.filter (fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => !e.subconstruction.isCausative) allEntries).all fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => !e.dualSubevent.constructional.hasCause) = true

Noncausative entries lack CAUSE in their derived constructional subevent.

theorem Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.all_constructional_have_become : (allEntries.all fun (x : ConstructionGrammar.Resultatives.ResultativeEntry) => x.dualSubevent.constructional.hasBecome) = true

All derived constructional subevents have BECOME.

theorem Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.noncausative_no_object_selection : ((List.filter (fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => !e.subconstruction.isCausative) allEntries).all fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => e.objectSelection == none) = true

Noncausative (intransitive) entries have no object selection.

theorem Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.causative_have_object_selection : ((List.filter (fun (x : ConstructionGrammar.Resultatives.ResultativeEntry) => x.subconstruction.isCausative) allEntries).all fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => e.objectSelection.isSome) = true

All causative entries specify an object selection mode.

theorem Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.bounded_entries_telic : ((List.filter (fun (x : ConstructionGrammar.Resultatives.ResultativeEntry) => x.rpBoundedness == ConstructionGrammar.Resultatives.Boundedness.bounded) allEntries).all fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => (ConstructionGrammar.Resultatives.resultativeAspect e.rpBoundedness).telicity == Features.Telicity.telic) = true

All entries with bounded RP are telic.

Theorems migrated from Theories.Semantics.Causation.Resultatives

These theorems quantify over allEntries (paper-specific data) and therefore belong with the paper, not in the Theory layer.

theorem Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.causative_resultative_has_cause : ((List.filter (fun (x : ConstructionGrammar.Resultatives.ResultativeEntry) => x.subconstruction.isCausative) allEntries).all fun (x : ConstructionGrammar.Resultatives.ResultativeEntry) => x.dualSubevent.constructional.hasCause) = true

All causative entries in the data have CAUSE.

theorem Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.causative_means_have_cause : ((List.filter (fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => e.subconstruction.isCausative && e.subeventRelation == ConstructionGrammar.Resultatives.SubeventRelation.means) allEntries).all fun (x : ConstructionGrammar.Resultatives.ResultativeEntry) => x.dualSubevent.constructional.hasCause) = true

MEANS-relation causative entries all have CAUSE.

theorem Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.activity_entries_become_accomplishments : ((List.filter (fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => e.bareVerbClass == Features.VendlerClass.activity && e.rpBoundedness == ConstructionGrammar.Resultatives.Boundedness.bounded) allEntries).all fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => ConstructionGrammar.Resultatives.resultativeVendlerClass e.rpBoundedness == Features.VendlerClass.accomplishment) = true

Activity verbs in the data with bounded RPs become accomplishments.

theorem Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.all_have_become : (allEntries.all fun (x : ConstructionGrammar.Resultatives.ResultativeEntry) => x.dualSubevent.constructional.hasBecome) = true

All resultative entries have BECOME.

Per-entry verb class participation

The construction-verb interaction across the four canonical Levin classes that @cite{goldberg-jackendoff-2004} discuss: manner verbs (hit = hammer/kick), change-of-state verbs (otherCoS = freeze), motion verbs (mannerOfMotion = roll/swing), and removing verbs (wipe).

theorem Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.all_entries_fused_cos : (allEntries.all fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => e.fusedMC.changeOfState) = true

All entries acquire CoS from the construction, regardless of verb class.

theorem Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.all_entries_resultative_alternation : (allEntries.all fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => ConstructionGrammar.predictedAlternationInConstruction e.verbMC e.subconstruction.toConstruction Semantics.Lexical.DiathesisAlternation.resultative) = true

All entries participate in the resultative alternation (none are instrument-spec).

theorem Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.causative_entries_causative_alternation : ((List.filter (fun (x : ConstructionGrammar.Resultatives.ResultativeEntry) => x.subconstruction.isCausative) allEntries).all fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => ConstructionGrammar.predictedAlternationInConstruction e.verbMC e.subconstruction.toConstruction Semantics.Lexical.DiathesisAlternation.causativeInchoative) = true

Causative entries all acquire the causative alternation.

theorem Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.noncausative_entries_no_new_causation : ((List.filter (fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => !e.subconstruction.isCausative) allEntries).all fun (e : ConstructionGrammar.Resultatives.ResultativeEntry) => decide (ConstructionGrammar.predictedAlternationInConstruction e.verbMC e.subconstruction.toConstruction Semantics.Lexical.DiathesisAlternation.causativeInchoative = e.verbMC.predictedAlternation Semantics.Lexical.DiathesisAlternation.causativeInchoative)) = true

Noncausative entries do NOT acquire the causative alternation (unless the verb already has causation — freeze/otherCoS does).

theorem Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.hammer_gains_cos_causation : hammerFlat.verbMC.changeOfState = false ∧ hammerFlat.verbMC.causation = false ∧ hammerFlat.fusedMC.changeOfState = true ∧ hammerFlat.fusedMC.causation = true

Hammer (hit-class): no CoS or causation alone → both added by causative construction.

theorem Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.freeze_already_has_cos : freezeSolid.verbMC.changeOfState = true ∧ freezeSolid.verbMC.causation = true ∧ freezeSolid.fusedMC = freezeSolid.verbMC

Freeze (otherCoS): already has CoS + causation → construction doesn't change profile.

theorem Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.roll_gains_cos_only : rollIntoField.verbMC.changeOfState = false ∧ rollIntoField.fusedMC.changeOfState = true ∧ rollIntoField.fusedMC.causation = false

Roll (manner-of-motion): gains CoS from construction; no causation (noncausative).

theorem Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.laugh_gains_cos_causation : laughSilly.verbMC.changeOfState = false ∧ laughSilly.verbMC.causation = false ∧ laughSilly.fusedMC.changeOfState = true ∧ laughSilly.fusedMC.causation = true

Laugh (performance): pure manner verb — construction adds CoS + causation.

theorem Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.wipe_already_has_everything : wipeClean.verbMC.changeOfState = true ∧ wipeClean.verbMC.causation = true ∧ wipeClean.fusedMC = wipeClean.verbMC

Wipe (wipe-class): already has full profile — construction is redundant.

Empirical data: grammaticality judgments

Theory-neutral grammaticality judgments and aspectual contrasts drawn from §§2–8 of the paper. These provide the shared data layer that other studies (Dendikken, Tay, Levin) connect to their own analyses.

inductive Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.ResultativeType : Type

What type of resultative is exemplified.

Extends the paper's 2×2 matrix (§2) with fake reflexives (§5) and anticausative property resultatives (@cite{levin-2026}).

• causativeProperty : ResultativeType
• causativePath : ResultativeType
• noncausativeProperty : ResultativeType
• noncausativePath : ResultativeType
• fakeReflexive : ResultativeType
• anticausativeProperty : ResultativeType

  Anticausative: verb doesn't alternate alone; construction licenses it (@cite{levin-2026}). Distinct from noncausativeProperty (e.g., freeze solid) where the verb independently shows the causative alternation.

@[implicit_reducible]

instance Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.instReprResultativeType : Repr ResultativeType

Equations

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

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.instReprResultativeType.repr : ResultativeType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.instDecidableEqResultativeType : DecidableEq ResultativeType

Equations

• Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.instDecidableEqResultativeType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.ResultativeDatum : Type

A single resultative example with judgment data.

• exId : String

  Example identifier

• sentence : String

  The sentence

• judgment : Features.Acceptability

  Acceptability judgment

• resType : ResultativeType

  Which resultative subtype

• phenomenon : String

  What phenomenon this illustrates

@[implicit_reducible]

instance Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.instReprResultativeDatum : Repr ResultativeDatum

Equations

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

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.instReprResultativeDatum.repr : ResultativeDatum → ℕ → Std.Format

Equations

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

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.instBEqResultativeDatum.beq : ResultativeDatum → ResultativeDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.instBEqResultativeDatum.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.instBEqResultativeDatum : BEq ResultativeDatum

Equations

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

Causative property resultatives (§2, ex. 5a, 7a)

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.hammer_flat : ResultativeDatum

Equations

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

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.wipe_clean : ResultativeDatum

Equations

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

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.paint_red : ResultativeDatum

Equations

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

Causative path resultatives (§2, ex. 5b)

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.kick_into_field : ResultativeDatum

Equations

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

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.push_off_table : ResultativeDatum

Equations

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

Noncausative property resultatives (§2, ex. 6a)

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.freeze_solid : ResultativeDatum

Equations

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

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.swing_shut : ResultativeDatum

Equations

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

Noncausative path resultatives (§2, ex. 6b)

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.roll_into_field : ResultativeDatum

Equations

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

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.slide_off_table : ResultativeDatum

Equations

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

Fake reflexive resultatives (§5, ex. 9)

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.laugh_silly : ResultativeDatum

Equations

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

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.drink_sick : ResultativeDatum

Equations

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

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.run_ragged : ResultativeDatum

Equations

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

Aspectual contrasts (§4, Principle 27)

structure Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.AspectualContrast : Type

An aspectual contrast pair.

• sentence : String

  Sentence with temporal adverbial

• judgment : Features.Acceptability

  Acceptability

• adverbialType : String

  Which adverbial type

• description : String

  Description

@[implicit_reducible]

instance Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.instReprAspectualContrast : Repr AspectualContrast

Equations

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

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.instReprAspectualContrast.repr : AspectualContrast → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.instBEqAspectualContrast : BEq AspectualContrast

Equations

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

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.instBEqAspectualContrast.beq : AspectualContrast → AspectualContrast → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.instBEqAspectualContrast.beq x✝¹ x✝ = false

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.hammer_flat_in : AspectualContrast

Equations

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

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.hammer_flat_for : AspectualContrast

Equations

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

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.hammer_bare_for : AspectualContrast

Equations

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

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.hammer_bare_in : AspectualContrast

Equations

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

Unacceptable resultatives (§6, semantic coherence violations)

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.eat_full : ResultativeDatum

Equations

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

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.sleep_flat : ResultativeDatum

Equations

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

Aggregate data

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.allExamples : List ResultativeDatum

Equations

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

def Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.aspectualContrasts : List AspectualContrast

Equations

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

Empirical verification

theorem Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.has_all_resultative_types : (allExamples.any fun (x : ResultativeDatum) => x.resType == ResultativeType.causativeProperty) = true ∧ (allExamples.any fun (x : ResultativeDatum) => x.resType == ResultativeType.causativePath) = true ∧ (allExamples.any fun (x : ResultativeDatum) => x.resType == ResultativeType.noncausativeProperty) = true ∧ (allExamples.any fun (x : ResultativeDatum) => x.resType == ResultativeType.noncausativePath) = true ∧ (allExamples.any fun (x : ResultativeDatum) => x.resType == ResultativeType.fakeReflexive) = true

All four resultative types are attested in the data.

theorem Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.has_both_judgments : (allExamples.any fun (x : ResultativeDatum) => x.judgment == Features.Acceptability.ok) = true ∧ (allExamples.any fun (x : ResultativeDatum) => x.judgment == Features.Acceptability.unacceptable) = true

Both grammatical and ungrammatical examples are represented.

theorem Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.aspectual_both_adverbials : (aspectualContrasts.any fun (x : AspectualContrast) => x.adverbialType == "in-adverbial") = true ∧ (aspectualContrasts.any fun (x : AspectualContrast) => x.adverbialType == "for-adverbial") = true

The aspectual contrast data includes both in- and for-adverbials.

theorem Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.telic_adverbial_pattern : (hammer_flat_in.judgment == Features.Acceptability.ok) = true ∧ (hammer_flat_for.judgment == Features.Acceptability.unacceptable) = true

Telic resultatives accept in-adverbials and reject for-adverbials.

theorem Phenomena.Constructions.Resultatives.Studies.GoldbergJackendoff2004.atelic_adverbial_pattern : (hammer_bare_for.judgment == Features.Acceptability.ok) = true

Atelic bare activities accept for-adverbials.