Verb entry — core type

Framework-agnostic types for verb semantics: the selectional/inflectional enums (VoiceType, SenseTag, …; complementation enums live in Features/Complementation.lean) and the Verb structure that bundles the semantic fields shared across languages.

Verb is the semantic spine of a verb entry. Its fields are organised into facet structures under the Verb namespace — Verb.ArgStructure, Verb.Aspect, Verb.Presupposition, Verb.Causation, Verb.Attitude — which Verb composes via extends. Flat field access (v.frames, v.attitude, …) is preserved by extends-flattening, and language fragments extend Verb with their own inflectional paradigms. Complement selection is a list of typed Frames (Syntax/Clause/Frame.lean); frame-conditioned attitude/opacity/control lives on Verb.Reading rows; the legacy flat readers (v.complementType, v.controlType, …) are derived accessors over frames/readings.

Verb classification (factive, causative, attitude, …) is DERIVED from these primitive fields in Semantics/Verb/Basic.lean, not stipulated as an enum.

Main declarations

• Verb — the composed verb entry spine
• Verb.ArgStructure, Verb.Aspect, Verb.Presupposition, Verb.Causation, Verb.Attitude — the field facets

Design

[BS26a] [Day25] [Hei92] [Ica12] [Ken07] [Mai15] [QOR+25] [RHL24] [SB24] [RHL98]

Selectional and inflectional enums

inductive VoiceType : Type

Framework-neutral voice type for deriving argument structure properties.

Captures the external-argument dimension of the verb's syntactic frame without committing to a specific syntactic framework. Maps to Minimalist.VoiceFlavor via bridge theorems in interface files.

• agentive: External argument introduced (transitive/unergative)
• nonThematic: No external argument (unaccusative/anticausative)
• expletive: No specifier, no semantics (middle voice)
• reflexive: Agent that binds internal argument ([Woo15])
• experiencer: Experiencer external argument ([Woo15])

• agentive : VoiceType
• nonThematic : VoiceType
• expletive : VoiceType
• reflexive : VoiceType
• experiencer : VoiceType

@[implicit_reducible]

instance instDecidableEqVoiceType : DecidableEq VoiceType

Equations

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

def instReprVoiceType.repr : VoiceType → ℕ → Std.Format

Equations

• instReprVoiceType.repr VoiceType.agentive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "VoiceType.agentive")).group prec✝
• instReprVoiceType.repr VoiceType.nonThematic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "VoiceType.nonThematic")).group prec✝
• instReprVoiceType.repr VoiceType.expletive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "VoiceType.expletive")).group prec✝
• instReprVoiceType.repr VoiceType.reflexive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "VoiceType.reflexive")).group prec✝
• instReprVoiceType.repr VoiceType.experiencer prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "VoiceType.experiencer")).group prec✝

@[implicit_reducible]

instance instReprVoiceType : Repr VoiceType

Equations

• instReprVoiceType = { reprPrec := instReprVoiceType.repr }

def VoiceType.assignsTheta : VoiceType → Bool

Does this voice type introduce an external argument?

Equations

• VoiceType.agentive.assignsTheta = true
• VoiceType.reflexive.assignsTheta = true
• VoiceType.experiencer.assignsTheta = true
• VoiceType.nonThematic.assignsTheta = false
• VoiceType.expletive.assignsTheta = false

inductive PresupTriggerType : Type

Presupposition trigger type ([TBRS13] classification).

• Hard triggers: Always project (too, again, also)
• Soft triggers: Context-sensitive projection (stop, know)

• hardTrigger : PresupTriggerType
• softTrigger : PresupTriggerType
• prerequisiteSoft : PresupTriggerType

@[implicit_reducible]

instance instDecidableEqPresupTriggerType : DecidableEq PresupTriggerType

Equations

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

def instReprPresupTriggerType.repr : PresupTriggerType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance instReprPresupTriggerType : Repr PresupTriggerType

Equations

• instReprPresupTriggerType = { reprPrec := instReprPresupTriggerType.repr }

def PresupTriggerType.isSoft : PresupTriggerType → Bool

Is this trigger locally accommodatable (soft)? Both factive and prerequisite triggers are soft.

Equations

• PresupTriggerType.hardTrigger.isSoft = false
• PresupTriggerType.softTrigger.isSoft = true
• PresupTriggerType.prerequisiteSoft.isSoft = true

inductive ProjectionBehavior : Type

Complement presupposition projection behavior ([Kar73]).

Orthogonal to PresupTriggerType (whether the verb triggers presuppositions): this classifies what the verb does with presuppositions of its complement.

• plug: blocks all complement presuppositions (say, tell, promise)
• hole: lets all complement presuppositions project (know, regret, stop)
• filter: conditionally cancels some complement presuppositions (if...then, and, or)

• plug : ProjectionBehavior
• hole : ProjectionBehavior
• filter : ProjectionBehavior

@[implicit_reducible]

instance instDecidableEqProjectionBehavior : DecidableEq ProjectionBehavior

Equations

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

@[implicit_reducible]

instance instReprProjectionBehavior : Repr ProjectionBehavior

Equations

• instReprProjectionBehavior = { reprPrec := instReprProjectionBehavior.repr }

def instReprProjectionBehavior.repr : ProjectionBehavior → ℕ → Std.Format

Equations

• instReprProjectionBehavior.repr ProjectionBehavior.plug prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ProjectionBehavior.plug")).group prec✝
• instReprProjectionBehavior.repr ProjectionBehavior.hole prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ProjectionBehavior.hole")).group prec✝
• instReprProjectionBehavior.repr ProjectionBehavior.filter prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ProjectionBehavior.filter")).group prec✝

inductive SenseTag : Type

Disambiguates polysemous verb entries that share a citation form.

When a verb has multiple lexical entries (e.g., "remember" as implicative vs. "remember" as factive question-embedding), the SenseTag records why multiple entries exist:

• .default: primary/unmarked sense
• .rogative: question-embedding sense
• .causative: causative use of otherwise non-causative verb
• .instrumental: instrument-specific sense
• .occasion: occasion verb sense with experiencer subject

• default : SenseTag
• rogative : SenseTag
• causative : SenseTag
• instrumental : SenseTag
• occasion : SenseTag
• stative : SenseTag

@[implicit_reducible]

instance instDecidableEqSenseTag : DecidableEq SenseTag

Equations

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

def instReprSenseTag.repr : SenseTag → ℕ → Std.Format

Equations

• instReprSenseTag.repr SenseTag.default prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SenseTag.default")).group prec✝
• instReprSenseTag.repr SenseTag.rogative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SenseTag.rogative")).group prec✝
• instReprSenseTag.repr SenseTag.causative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SenseTag.causative")).group prec✝
• instReprSenseTag.repr SenseTag.instrumental prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SenseTag.instrumental")).group prec✝
• instReprSenseTag.repr SenseTag.occasion prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SenseTag.occasion")).group prec✝
• instReprSenseTag.repr SenseTag.stative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SenseTag.stative")).group prec✝

@[implicit_reducible]

instance instReprSenseTag : Repr SenseTag

Equations

• instReprSenseTag = { reprPrec := instReprSenseTag.repr }

inductive ImplicitInterp : Type

Interpretation of an implicit (unexpressed) argument.

Cross-linguistic: applies to any argument position where the verb allows the argument to be absent. The distinction captures whether the missing referent must be pragmatically recoverable (definite) or can be unspecified (indefinite). [Bru21], [Fil86].

• indef : ImplicitInterp
• def : ImplicitInterp

@[implicit_reducible]

instance instDecidableEqImplicitInterp : DecidableEq ImplicitInterp

Equations

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

def instReprImplicitInterp.repr : ImplicitInterp → ℕ → Std.Format

Equations

• instReprImplicitInterp.repr ImplicitInterp.indef prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ImplicitInterp.indef")).group prec✝
• instReprImplicitInterp.repr ImplicitInterp.def prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ImplicitInterp.def")).group prec✝

@[implicit_reducible]

instance instReprImplicitInterp : Repr ImplicitInterp

Equations

• instReprImplicitInterp = { reprPrec := instReprImplicitInterp.repr }

Field facets

Each facet groups a concern's fields; Verb composes them via extends, so flat access (v.complementType) is preserved.

structure Verb.ArgStructure : Type

Argument structure and realization: complement selection, control, proto-role entailments, voice, and implicit arguments.

• frames : List Frame

  Complement frames, citation frame first. [] for intransitives. The legacy ComplementType cells are the Frame.np, Frame.finiteClause, … smart constructors (Syntax/Clause/Frame.lean).

• subjectEntailments : Option ArgumentStructure.EntailmentProfile

  Proto-role entailment profile for the subject (external argument). The authoritative representation of argument semantics ([Dow91], [Gri11], [Lev19]). Convenience role labels can be derived via EntailmentProfile.toRole.

• objectEntailments : Option ArgumentStructure.EntailmentProfile

  Proto-role entailment profile for the first object (internal argument).

• unaccusative : Bool

  Is the verb unaccusative? (subject is underlying object) When voiceType is present, prefer derivedUnaccusative which derives this from Voice selection ([Kra96]).

• voiceType : Option VoiceType

  Framework-neutral voice type: determines whether an external argument is introduced. When set, derivedUnaccusative derives unaccusativity from this field, connecting the Fragment entry to Voice theory.

• passivizable : Bool

  Can the verb passivize?

• implicitObj : Option ImplicitInterp

  Can the direct object (theme/patient) be left unexpressed? Applies to monotransitives (eat vs devour) and the theme of ditransitives. none = object always required. [Bru21]

• implicitGoal : Option ImplicitInterp

  Can the goal/recipient argument be left unexpressed? Applies to the IO of double object constructions and the PP of dative frames. none = goal always required.

@[implicit_reducible]

instance Verb.instReprArgStructure : Repr ArgStructure

Equations

• Verb.instReprArgStructure = { reprPrec := Verb.instReprArgStructure.repr }

def Verb.instReprArgStructure.repr : ArgStructure → ℕ → Std.Format

Equations

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

def Verb.instBEqArgStructure.beq : ArgStructure → ArgStructure → Bool

Equations

• One or more equations did not get rendered due to their size.
• Verb.instBEqArgStructure.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Verb.instBEqArgStructure : BEq ArgStructure

Equations

• Verb.instBEqArgStructure = { beq := Verb.instBEqArgStructure.beq }

structure Verb.Aspect : Type

Aspectual class: Vendler class, degree-achievement scale, incrementality, and change-of-state type.

• vendlerClass : Option Features.VendlerClass

  [Ven57] aspectual class of the verb's base VP. For verbs whose class depends on the object NP (eat apples = activity, eat two apples = accomplishment), record the class with a quantized (bounded) object. none for verbs where Vendler class is inapplicable (e.g., clause-embedding verbs).

• degreeAchievementScale : Option Features.DegreeAchievement.DegreeAchievementScale

  For degree achievements: the scale structure from which default vendlerClass is derived. When present, vendlerClass should agree with degreeAchievementScale.defaultVendlerClass.

• verbIncClass : Option Semantics.Aspect.Incremental.VerbIncClass

  [Kri98] incrementality class of the object/theme role. .sinc = strictly incremental (eat, build); .inc = incremental with backups (read); .cumOnly = cumulative only (push, carry). none for intransitives and clause-embedding verbs.

• cosType : Option Features.ChangeOfState.CoSType

  For CoS verbs: which type (cessation, inception, continuation)?

@[implicit_reducible]

instance Verb.instReprAspect : Repr Aspect

Equations

• Verb.instReprAspect = { reprPrec := Verb.instReprAspect.repr }

def Verb.instReprAspect.repr : Aspect → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Verb.instBEqAspect : BEq Aspect

Equations

• Verb.instBEqAspect = { beq := Verb.instBEqAspect.beq }

def Verb.instBEqAspect.beq : Aspect → Aspect → Bool

Equations

• One or more equations did not get rendered due to their size.
• Verb.instBEqAspect.beq x✝¹ x✝ = false

structure Verb.Presupposition : Type

Presupposition profile: trigger type and complement-projection behavior.

• presupType : Option PresupTriggerType

  Is the verb a presupposition trigger?

• projectionBehavior : Option ProjectionBehavior

  How does the verb treat presuppositions of its complement? Orthogonal to presupType. [Kar73]

@[implicit_reducible]

instance Verb.instReprPresupposition : Repr Presupposition

Equations

• Verb.instReprPresupposition = { reprPrec := Verb.instReprPresupposition.repr }

def Verb.instReprPresupposition.repr : Presupposition → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Verb.instBEqPresupposition : BEq Presupposition

Equations

• Verb.instBEqPresupposition = { beq := Verb.instBEqPresupposition.beq }

def Verb.instBEqPresupposition.beq : Presupposition → Presupposition → Bool

Equations

• Verb.instBEqPresupposition.beq { presupType := a, projectionBehavior := a_1 } { presupType := b, projectionBehavior := b_1 } = (a == b && a_1 == b_1)
• Verb.instBEqPresupposition.beq x✝¹ x✝ = false

structure Verb.Causation : Type

Causal/implicative semantics: implicative polarity, causative mechanism, and psych-causative source.

• implicative : Option Features.Implicative

  For implicative verbs: complement entailment polarity (links to compositional semantics).

• causative : Option Features.Causative

  For causative verbs: force-dynamic mechanism (links to compositional semantics).

• causalSource : Option Causation.Psych.CausalSource

  Source of causation for psych causatives ([Kim24] UPH). .external = mind-external percept, .internal = mind-internal representation.

@[implicit_reducible]

instance Verb.instReprCausation : Repr Causation

Equations

• Verb.instReprCausation = { reprPrec := Verb.instReprCausation.repr }

def Verb.instReprCausation.repr : Causation → ℕ → Std.Format

Equations

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

def Verb.instBEqCausation.beq : Causation → Causation → Bool

Equations

• Verb.instBEqCausation.beq { implicative := a, causative := a_1, causalSource := a_2 } { implicative := b, causative := b_1, causalSource := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Verb.instBEqCausation.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Verb.instBEqCausation : BEq Causation

Equations

• Verb.instBEqCausation = { beq := Verb.instBEqCausation.beq }

structure Verb.Reading : Type

One frame-conditioned reading of a verb ([Bon22] §4.4.3 hanaxa; Greek thimame): per-frame overrides of the lexeme-level attitude and opacity (none = inherit Verb.attitude / Verb.opaqueContext), and the frame's control type.

• frame : Frame

  The frame this reading is conditioned on (one of the verb's frames; Verb.readingsWF).

• attitude : Option Features.Attitude

  Frame-conditioned attitude override.

• opaqueContext : Option Bool

  Frame-conditioned opacity override.

• control : Option ControlType

  Control type for this frame.

def Verb.instDecidableEqReading.decEq (x✝ x✝¹ : Reading) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Verb.instDecidableEqReading : DecidableEq Reading

Equations

• Verb.instDecidableEqReading = Verb.instDecidableEqReading.decEq

@[implicit_reducible]

instance Verb.instReprReading : Repr Reading

Equations

• Verb.instReprReading = { reprPrec := Verb.instReprReading.repr }

def Verb.instReprReading.repr : Reading → ℕ → Std.Format

Equations

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

structure Verb.Attitude : Type

Attitudinal and intensional properties: attitude classification, opacity, question-embedding, and complement monotonicity.

• opaqueContext : Bool

  Does the verb create an opaque context for its complement?

• attitude : Option Features.Attitude

  Unified attitude classification covering doxastic and preferential attitudes. Theoretical properties (C-distributivity, parasitic, etc.) are DERIVED.

• readings : List Reading

  Frame-conditioned readings ([Bon22] §4.4.3): per-frame attitude/opacity overrides and control, keyed to frames entries.

• takesQuestionBase : Bool

  For non-preferential question-embedding verbs (know, wonder, ask)

• complementSig : Option NaturalLogic.EntailmentSig

  Entailment signature of the complement position. Classifies this verb's monotonicity w.r.t. its clausal complement. .mono = upward monotone: the report is closed under entailment of the complement, as in Hintikka-style doxastic semantics ([Hin62]). Set only where the classification is textbook consensus (believe, think, know); preferential attitudes (want, hope) are contested ([Hei92]) and stay none.

def Verb.instReprAttitude.repr : Attitude → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Verb.instReprAttitude : Repr Attitude

Equations

• Verb.instReprAttitude = { reprPrec := Verb.instReprAttitude.repr }

def Verb.instBEqAttitude.beq : Attitude → Attitude → Bool

Equations

• One or more equations did not get rendered due to their size.
• Verb.instBEqAttitude.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Verb.instBEqAttitude : BEq Attitude

Equations

• Verb.instBEqAttitude = { beq := Verb.instBEqAttitude.beq }

structure Verbextends Verb.ArgStructure, Verb.Aspect, Verb.Presupposition, Verb.Causation, Verb.Attitude : Type

Cross-linguistic verb core: all semantic fields shared across languages.

Composes the Verb.* facets (argument structure, aspect, presupposition, causation, attitude, root) plus the citation form, speech-act status, and a polysemy disambiguator. Language-specific fragments extend this with morphological fields appropriate to their inflectional system.

• frames : List Frame
• subjectEntailments : Option ArgumentStructure.EntailmentProfile
• objectEntailments : Option ArgumentStructure.EntailmentProfile
• unaccusative : Bool
• voiceType : Option VoiceType
• passivizable : Bool
• implicitObj : Option ImplicitInterp
• implicitGoal : Option ImplicitInterp
• vendlerClass : Option Features.VendlerClass
• degreeAchievementScale : Option Features.DegreeAchievement.DegreeAchievementScale
• verbIncClass : Option Semantics.Aspect.Incremental.VerbIncClass
• cosType : Option Features.ChangeOfState.CoSType
• presupType : Option PresupTriggerType
• projectionBehavior : Option ProjectionBehavior
• implicative : Option Features.Implicative
• causative : Option Features.Causative
• causalSource : Option Causation.Psych.CausalSource
• opaqueContext : Bool
• attitude : Option Features.Attitude
• readings : List Reading
• takesQuestionBase : Bool
• complementSig : Option NaturalLogic.EntailmentSig
• levinClass : Option Semantics.Lexical.LevinClass

  [Lev93] verb class (§§ 9–57).

• root : Root

  The verb's lexical root — its entailment atoms, derived B&KG kind signature, and [Bha24] outcome axis. The content carrier the Verb API integrates around (P-HUB): the verb's signature / outcome / change-type are read off this root rather than the levinClass table. Total, with the trivial root {} (no annotation) as the ⊥.

• form : String

  Citation form (cross-linguistic)

• speechActVerb : Bool

  Does the verb denote the performance of an illocutionary act? True for speech-act verbs (say, tell, claim, ask). This is a genuine semantic primitive that cannot be derived from other fields.

• senseTag : SenseTag

  Disambiguates entries that share a citation form. Most verbs use .default; polysemous entries use descriptive tags.

@[implicit_reducible]

instance instReprVerb : Repr Verb

Equations

• instReprVerb = { reprPrec := instReprVerb.repr }

def instReprVerb.repr : Verb → ℕ → Std.Format

Equations

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

def instBEqVerb.beq : Verb → Verb → Bool

Equations

• One or more equations did not get rendered due to their size.
• instBEqVerb.beq x✝¹ x✝ = false

@[implicit_reducible]

instance instBEqVerb : BEq Verb

Equations

• instBEqVerb = { beq := instBEqVerb.beq }

Frame accessors

Flat readers over Verb.frames/Verb.readings, preserving the legacy enum-based call syntax: the citation frame's complement/control type and the alternate frame's, when present.

def Verb.complementType (v : Verb) : ComplementType

The citation (first) frame's legacy ComplementType cell.

Equations

• v.complementType = (v.frames.head?.bind Frame.toComplementType).getD ComplementType.none

def Verb.altComplementType (v : Verb) : Option ComplementType

The alternate (second) frame's legacy ComplementType cell.

Equations

• v.altComplementType = v.frames[1]?.bind Frame.toComplementType

def Verb.controlType (v : Verb) : ControlType

The control type of the reading keyed to the citation frame.

Equations

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

def Verb.altControlType (v : Verb) : ControlType

The control type of the reading keyed to the alternate frame.

Equations

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

def Verb.attitudeOn (v : Verb) (fr : Frame) : Option Features.Attitude

The effective attitude on frame fr: reading override, else lexeme default.

Equations

• v.attitudeOn fr = ((List.find? (fun (x : Verb.Reading) => x.frame == fr) v.readings).bind fun (x : Verb.Reading) => x.attitude).orElse fun (x : Unit) => v.attitude

def Verb.readingsWF (v : Verb) : Prop

Every reading is keyed to one of the verb's frames.

Equations

• v.readingsWF = ∀ r ∈ v.readings, r.frame ∈ v.frames

def Verb.codings (v : Verb) : List NoonanCompType

All [Noo07] codings across the verb's frames.

Equations

• v.codings = List.flatMap Frame.codings v.frames

def Verb.takesClauseForm (v : Verb) (cf : Features.ClauseForm) : Prop

Some frame of the verb records clause form cf.

Equations

• v.takesClauseForm cf = ∃ fr ∈ v.frames, fr.hasClauseForm cf