Event predicates and the Event type are imported from Theories/Semantics/Events/Basic.lean — the unified event ontology. Tense-aspect code uses Event Time and EventPred W Time without referencing .sort (the field exists for Krifka-style consumers but is irrelevant for Klein-style tense composition).

@[reducible, inline]

abbrev Semantics.Aspect.Core.IntervalPred (W : Type u_1) (Time : Type u_2) [LinearOrder Time] : Type (max u_1 u_2)

Predicate over time intervals (output of IMPF/PRFV).

Equations

• Semantics.Aspect.Core.IntervalPred W Time = (W → Core.Time.Interval Time → Prop)

@[reducible, inline]

abbrev Semantics.Aspect.Core.PointPred (W : Type u_1) (Time : Type u_2) : Type (max u_2 u_1)

Predicate over time points (output of PERF, input to TENSE). Defined as WorldTimeIndex W Time → Prop to make the situation structure explicit in the tense-aspect pipeline, connecting directly to situation semantics (Elbourne, Percus, Kratzer).

Equations

• Semantics.Aspect.Core.PointPred W Time = (Core.WorldTimeIndex W Time → Prop)

inductive Semantics.Aspect.Core.ViewpointType : Type

Viewpoint aspect types. @cite{klein-1994} identified imperfective, perfective, perfect, and prospective. @cite{smith-1997} added the neutral viewpoint (default in the absence of overt aspect morphology).

• imperfective : ViewpointType
• perfective : ViewpointType
• perfect : ViewpointType
• prospective : ViewpointType
• neutral : ViewpointType

@[implicit_reducible]

instance Semantics.Aspect.Core.instDecidableEqViewpointType : DecidableEq ViewpointType

Equations

• Semantics.Aspect.Core.instDecidableEqViewpointType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Aspect.Core.instReprViewpointType : Repr ViewpointType

Equations

• Semantics.Aspect.Core.instReprViewpointType = { reprPrec := Semantics.Aspect.Core.instReprViewpointType.repr }

def Semantics.Aspect.Core.instReprViewpointType.repr : ViewpointType → ℕ → Std.Format

Equations

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

def Semantics.Aspect.Core.instInhabitedViewpointType.default : ViewpointType

Equations

• Semantics.Aspect.Core.instInhabitedViewpointType.default = Semantics.Aspect.Core.ViewpointType.imperfective

@[implicit_reducible]

instance Semantics.Aspect.Core.instInhabitedViewpointType : Inhabited ViewpointType

Equations

• Semantics.Aspect.Core.instInhabitedViewpointType = { default := Semantics.Aspect.Core.instInhabitedViewpointType.default }

inductive Semantics.Aspect.Core.ViewpointAspectB : Type

Bool-level viewpoint aspect, capturing the perfective/imperfective distinction without the full interval-based EventPred/IntervalPred machinery.

Used by Modal/Ability.lean (actuality inferences) and Phenomena/ActualityInferences/Data.lean where the key insight is simply "perfective requires actualization, imperfective doesn't."

• perfective : ViewpointAspectB
• imperfective : ViewpointAspectB

@[implicit_reducible]

instance Semantics.Aspect.Core.instDecidableEqViewpointAspectB : DecidableEq ViewpointAspectB

Equations

• Semantics.Aspect.Core.instDecidableEqViewpointAspectB x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Aspect.Core.instReprViewpointAspectB.repr : ViewpointAspectB → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Aspect.Core.instReprViewpointAspectB : Repr ViewpointAspectB

Equations

• Semantics.Aspect.Core.instReprViewpointAspectB = { reprPrec := Semantics.Aspect.Core.instReprViewpointAspectB.repr }

def Semantics.Aspect.Core.instInhabitedViewpointAspectB.default : ViewpointAspectB

Equations

• Semantics.Aspect.Core.instInhabitedViewpointAspectB.default = Semantics.Aspect.Core.ViewpointAspectB.perfective

@[implicit_reducible]

instance Semantics.Aspect.Core.instInhabitedViewpointAspectB : Inhabited ViewpointAspectB

Equations

• Semantics.Aspect.Core.instInhabitedViewpointAspectB = { default := Semantics.Aspect.Core.instInhabitedViewpointAspectB.default }

def Semantics.Aspect.Core.ViewpointType.toBoolAspect : ViewpointType → Option ViewpointAspectB

Project ViewpointType to the coarser perfective/imperfective distinction. Returns none for perfect and prospective (neither is simply perf/impf).

Equations

• Semantics.Aspect.Core.ViewpointType.perfective.toBoolAspect = some Semantics.Aspect.Core.ViewpointAspectB.perfective
• Semantics.Aspect.Core.ViewpointType.imperfective.toBoolAspect = some Semantics.Aspect.Core.ViewpointAspectB.imperfective
• Semantics.Aspect.Core.ViewpointType.perfect.toBoolAspect = none
• Semantics.Aspect.Core.ViewpointType.prospective.toBoolAspect = none
• Semantics.Aspect.Core.ViewpointType.neutral.toBoolAspect = none

def Semantics.Aspect.Core.ViewpointAspectB.toKleinViewpoint : ViewpointAspectB → ViewpointType

Embed ViewpointAspectB back into Klein's full classification.

Equations

• Semantics.Aspect.Core.ViewpointAspectB.perfective.toKleinViewpoint = Semantics.Aspect.Core.ViewpointType.perfective
• Semantics.Aspect.Core.ViewpointAspectB.imperfective.toKleinViewpoint = Semantics.Aspect.Core.ViewpointType.imperfective

theorem Semantics.Aspect.Core.toBoolAspect_toKleinViewpoint (a : ViewpointAspectB) : a.toKleinViewpoint.toBoolAspect = some a

Roundtrip: embedding then projecting is the identity.

def Semantics.Aspect.Core.ViewpointType.ttTSitRelation {Time : Type u_1} [LinearOrder Time] (v : ViewpointType) (tt tsit : Core.Time.Interval Time) : Prop

The TT↔TSit interval relation for each viewpoint (@cite{klein-1994}: 108).

Equations

• Semantics.Aspect.Core.ViewpointType.imperfective.ttTSitRelation tt tsit = tt.properSubinterval tsit
• Semantics.Aspect.Core.ViewpointType.perfective.ttTSitRelation tt tsit = tsit.subinterval tt
• Semantics.Aspect.Core.ViewpointType.perfect.ttTSitRelation tt tsit = tt.isAfter tsit
• Semantics.Aspect.Core.ViewpointType.prospective.ttTSitRelation tt tsit = tt.isBefore tsit
• Semantics.Aspect.Core.ViewpointType.neutral.ttTSitRelation tt tsit = tt.initialOverlap tsit

def Semantics.Aspect.Core.IMPF {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : Events.EventPred W Time) : IntervalPred W Time

IMPERFECTIVE: reference time properly contained in event runtime. @cite{klein-1994}: TT INCL TSit. @cite{knick-sharf-2026} eq. 25.

Equations

• Semantics.Aspect.Core.IMPF P w t = ∃ (e : Semantics.Events.Event Time), t.properSubinterval e.τ ∧ P w e

def Semantics.Aspect.Core.PRFV {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : Events.EventPred W Time) : IntervalPred W Time

PERFECTIVE: event runtime contained in reference time. @cite{klein-1994}: TT AT TSit (simplified to TSit ⊆ TT, following @cite{smith-1997}). @cite{knick-sharf-2026} eq. 28.

Equations

• Semantics.Aspect.Core.PRFV P w t = ∃ (e : Semantics.Events.Event Time), e.τ.subinterval t ∧ P w e

def Semantics.Aspect.Core.PROSP {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : Events.EventPred W Time) : IntervalPred W Time

PROSPECTIVE: reference time before situation time. @cite{klein-1994}: TT BEFORE TSit.

Equations

• Semantics.Aspect.Core.PROSP P w t = ∃ (e : Semantics.Events.Event Time), t.isBefore e.τ ∧ P w e

def Semantics.Aspect.Core.INIT_OVERLAP {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : Events.EventPred W Time) : IntervalPred W Time

INIT_OVERLAP: initial overlap between reference time and event runtime. @cite{pancheva-2003} eq. 7b: ⟦NEUTRAL⟧ = λP.λi.∃e[i ∂τ(e) & P(e)] The beginning of the eventuality is in the reference interval, but the end may extend beyond. Derives experiential perfect readings.

Renamed from NEUTRAL to avoid collision with @cite{smith-1997}'s neutral viewpoint (ViewpointType.neutral), which is a different concept. Pancheva's operator is an inner Asp₂ head; Smith's neutral viewpoint is a default viewpoint type.

Equations

• Semantics.Aspect.Core.INIT_OVERLAP P w t = ∃ (e : Semantics.Events.Event Time), t.initialOverlap e.τ ∧ P w e

def Semantics.Aspect.Core.RB {Time : Type u_1} [LinearOrder Time] (pts : Core.Time.Interval Time) (t : Time) : Prop

Right Boundary: PTS finishes at reference time point t.

Equations

• Semantics.Aspect.Core.RB pts t = (pts.finish = t)

def Semantics.Aspect.Core.LB {Time : Type u_1} [LinearOrder Time] (tLB : Time) (pts : Core.Time.Interval Time) : Prop

Left Boundary: PTS starts at time tLB.

Equations

• Semantics.Aspect.Core.LB tLB pts = (pts.start = tLB)

def Semantics.Aspect.Core.PERF {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (p : IntervalPred W Time) : PointPred W Time

PERFECT: introduces Perfect Time Span. @cite{knick-sharf-2026} eq. 22b — the standard XN-theoretic entry that K&S start from. Verified against the proceedings PDF.

K&S notation: λp_it.λt.∃t_PTS.[RB(t_PTS, t) ∧ p(t)]. The p(t) is written by K&S as application to the outer reference time, with the composition convention that t is bound to t_PTS when IMPF appears below PERF (paper §4.2.1, sentence after eq. 25). The implementation here applies p to pts directly (the post-composition meaning), which matches K&S's worked composition in their (26).

Equations

• Semantics.Aspect.Core.PERF p s = ∃ (pts : Core.Time.Interval Time), Semantics.Aspect.Core.RB pts s.time ∧ p s.world pts

def Semantics.Aspect.Core.PERF_XN {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (p : IntervalPred W Time) (tᵣ : Set Time) : PointPred W Time

PERFECT with Extended Now (K&S's revision: domain-restricted left boundary). @cite{knick-sharf-2026} eq. 23b. Verified against the proceedings PDF.

K&S notation: λp_it.λt.∃t_PTS.∃t_LB ⊆ tᵣ. [LB(t_LB, t_PTS) ∧ RB(t_PTS, t) ∧ p(t)]. The domain restriction tᵣ constrains where the LB can be placed; narrow focus on BEEN generates alternatives over tᵣ.

K&S's (23b) is not the standard XN entry — that's their (22b), realized here as PERF. (23b) is K&S's own revision adding an LB existential bounded by the domain restriction. The legacy name PERF_XN predates this clarification; both PERF and PERF_XN are XN-theoretic, the difference being the LB+domain-restriction.

Type-level simplification: K&S's t_LB is an initial subinterval of t_PTS (per their 23a), and t_LB ⊆ t_r compares two interval-sets. The implementation here uses tLB : Time (a single point) with ∃ tLB ∈ tᵣ (membership), simplifying K&S's set-theoretic LB to a single time witness inside the domain-restriction set. The simpler typing is sufficient for the empirical predictions K&S draw and avoids carrying intervals at every level.

Equations

• Semantics.Aspect.Core.PERF_XN p tᵣ s = ∃ (pts : Core.Time.Interval Time), ∃ tLB ∈ tᵣ, Semantics.Aspect.Core.LB tLB pts ∧ Semantics.Aspect.Core.RB pts s.time ∧ p s.world pts

theorem Semantics.Aspect.Core.impf_is_klein_imperfective {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : Events.EventPred W Time) (w : W) (t : Core.Time.Interval Time) : IMPF P w t ↔ ∃ (e : Events.Event Time), ViewpointType.imperfective.ttTSitRelation t e.τ ∧ P w e

IMPF matches Klein's IMPERFECTIVE: ∃e where TT ⊂ TSit.

theorem Semantics.Aspect.Core.prfv_is_klein_perfective {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : Events.EventPred W Time) (w : W) (t : Core.Time.Interval Time) : PRFV P w t ↔ ∃ (e : Events.Event Time), ViewpointType.perfective.ttTSitRelation t e.τ ∧ P w e

PRFV matches Klein's PERFECTIVE: ∃e where TSit ⊆ TT.

@[reducible, inline]

abbrev Semantics.Aspect.Core.perfProg {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : Events.EventPred W Time) : PointPred W Time

"has been V-ing" = PERF(IMPF(V)).

Equations

• Semantics.Aspect.Core.perfProg P = Semantics.Aspect.Core.PERF (Semantics.Aspect.Core.IMPF P)

@[reducible, inline]

abbrev Semantics.Aspect.Core.perfSimple {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : Events.EventPred W Time) : PointPred W Time

"has V-ed" = PERF(PRFV(V)).

Equations

• Semantics.Aspect.Core.perfSimple P = Semantics.Aspect.Core.PERF (Semantics.Aspect.Core.PRFV P)

theorem Semantics.Aspect.Core.perf_impf_unfold {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : Events.EventPred W Time) (w : W) (t : Time) : perfProg P { world := w, time := t } ↔ ∃ (pts : Core.Time.Interval Time) (e : Events.Event Time), RB pts t ∧ pts.properSubinterval e.τ ∧ P w e

PERF(IMPF(P)) unfolds: ∃ PTS and event, with PTS right-bounded at t, the PTS properly inside the event, and P holds of the event.

theorem Semantics.Aspect.Core.perf_prfv_unfold {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : Events.EventPred W Time) (w : W) (t : Time) : perfSimple P { world := w, time := t } ↔ ∃ (pts : Core.Time.Interval Time) (e : Events.Event Time), RB pts t ∧ e.τ.subinterval pts ∧ P w e

PERF(PRFV(P)) unfolds: ∃ PTS and event, with PTS right-bounded at t, the event inside the PTS, and P holds of the event.

theorem Semantics.Aspect.Core.perf_xn_entails_perf {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (p : IntervalPred W Time) (tᵣ : Set Time) (w : W) (t : Time) : PERF_XN p tᵣ { world := w, time := t } → PERF p { world := w, time := t }

Extended Now entails basic perfect (PERF_XN is stronger).

theorem Semantics.Aspect.Core.perf_xn_univ_iff_perf {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (p : IntervalPred W Time) (w : W) (t : Time) : PERF_XN p Set.univ { world := w, time := t } ↔ PERF p { world := w, time := t }

With maximal domain (Set.univ), PERF_XN collapses to PERF.

theorem Semantics.Aspect.Core.perf_xn_monotone {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (p : IntervalPred W Time) (tᵣ₁ tᵣ₂ : Set Time) (hSub : tᵣ₁ ⊆ tᵣ₂) (w : W) (t : Time) : PERF_XN p tᵣ₁ { world := w, time := t } → PERF_XN p tᵣ₂ { world := w, time := t }

Narrower domain restriction is stronger (monotone in tᵣ).

theorem Semantics.Aspect.Core.impf_entails_event {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : Events.EventPred W Time) (w : W) (t : Core.Time.Interval Time) : IMPF P w t → ∃ (e : Events.Event Time), P w e

IMPF entails an event exists.

theorem Semantics.Aspect.Core.prfv_entails_event {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : Events.EventPred W Time) (w : W) (t : Core.Time.Interval Time) : PRFV P w t → ∃ (e : Events.Event Time), P w e

PRFV entails an event exists.

theorem Semantics.Aspect.Core.perf_monotone {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (p q : IntervalPred W Time) (h : ∀ (w : W) (t : Core.Time.Interval Time), p w t → q w t) (w : W) (t : Time) : PERF p { world := w, time := t } → PERF q { world := w, time := t }

PERF is monotone: p ⊆ q → PERF(p) ⊆ PERF(q).

theorem Semantics.Aspect.Core.impf_prfv_opposite_containment {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : Events.EventPred W Time) (w : W) (t : Core.Time.Interval Time) : (IMPF P w t → ∃ (e : Events.Event Time), P w e ∧ t.properSubinterval e.τ) ∧ (PRFV P w t → ∃ (e : Events.Event Time), P w e ∧ e.τ.subinterval t)

IMPF and PRFV impose opposite containment directions. IMPF: reference ⊂ event runtime. PRFV: event runtime ⊆ reference.

@cite{pancheva-2003} decomposes perfect participles into two aspect heads: [T [Asp₁=PERFECT [Asp₂=VIEWPOINT [vP]]]]. The inner Asp₂ (UNBOUNDED, INIT_OVERLAP, or BOUNDED) determines the perfect type (universal, experiential, or resultative). The outer Asp₁ = PERFECT introduces the PTS via a final subinterval relation rather than a point-based right boundary.

def Semantics.Aspect.Core.UNBOUNDED {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : Events.EventPred W Time) : IntervalPred W Time

Pancheva's UNBOUNDED (Asp₂): non-strict ⊆ variant of IMPF. ⟦UNBOUNDED⟧ = λP.λi.∃e[i ⊆ τ(e) & P(e)] (@cite{pancheva-2003}: 282, eq. 7b). Differs from IMPF in using non-strict ⊆ rather than strict ⊂.

Equations

• Semantics.Aspect.Core.UNBOUNDED P w t = ∃ (e : Semantics.Events.Event Time), t.subinterval e.τ ∧ P w e

def Semantics.Aspect.Core.BOUNDED {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : Events.EventPred W Time) : IntervalPred W Time

Pancheva's BOUNDED (Asp₂): strict ⊂ variant of PRFV. ⟦BOUNDED⟧ = λP.λi.∃e[τ(e) ⊂ i & P(e)] (@cite{pancheva-2003}: 282, eq. 7b). Differs from PRFV in using strict ⊂ rather than non-strict ⊆.

Equations

• Semantics.Aspect.Core.BOUNDED P w t = ∃ (e : Semantics.Events.Event Time), e.τ.properSubinterval t ∧ P w e

theorem Semantics.Aspect.Core.impf_entails_unbounded {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : Events.EventPred W Time) (w : W) (t : Core.Time.Interval Time) : IMPF P w t → UNBOUNDED P w t

IMPF (strict ⊂) entails UNBOUNDED (non-strict ⊆).

theorem Semantics.Aspect.Core.bounded_entails_prfv {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : Events.EventPred W Time) (w : W) (t : Core.Time.Interval Time) : BOUNDED P w t → PRFV P w t

BOUNDED (strict ⊂) entails PRFV (non-strict ⊆).

def Semantics.Aspect.Core.PERF_P {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (p : IntervalPred W Time) : IntervalPred W Time

Pancheva-style interval-level PERFECT (Asp₁). ⟦PERFECT⟧ = λp.λi.∃i'[PTS(i', i) & p(i')] (@cite{pancheva-2003}: 284, eq. 9b). PTS(i', i) iff i is a final subinterval of i': i ⊆ i' ∧ i.finish = i'.finish.

Equations

• Semantics.Aspect.Core.PERF_P p w i = ∃ (pts : Core.Time.Interval Time), i.finalSubinterval pts ∧ p w pts

theorem Semantics.Aspect.Core.perf_p_at_point_iff_perf {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (p : IntervalPred W Time) (w : W) (t : Time) : PERF_P p w (Core.Time.Interval.point t) ↔ PERF p { world := w, time := t }

Point-based PERF is the special case of interval-based PERF_P where the reference interval degenerates to a point [t, t].

theorem Semantics.Aspect.Core.perf_p_monotone {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (p q : IntervalPred W Time) (h : ∀ (w : W) (t : Core.Time.Interval Time), p w t → q w t) (w : W) (i : Core.Time.Interval Time) : PERF_P p w i → PERF_P q w i

PERF_P is monotone: if p entails q, then PERF_P(p) entails PERF_P(q).

inductive Semantics.Aspect.Core.PerfectType : Type

@cite{pancheva-2003} perfect type classification. The embedded Asp₂ determines the perfect reading:

• universal = PERFECT(UNBOUNDED): event ongoing throughout PTS
• experiential = PERFECT(NEUTRAL): event began within PTS
• resultative = PERFECT(BOUNDED): event completed within PTS Note: Pancheva's resultative properly involves a result state relation; BOUNDED is a simplification sufficient for the temporal structure.

• universal : PerfectType
• experiential : PerfectType
• resultative : PerfectType

@[implicit_reducible]

instance Semantics.Aspect.Core.instDecidableEqPerfectType : DecidableEq PerfectType

Equations

• Semantics.Aspect.Core.instDecidableEqPerfectType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Aspect.Core.instReprPerfectType : Repr PerfectType

Equations

• Semantics.Aspect.Core.instReprPerfectType = { reprPrec := Semantics.Aspect.Core.instReprPerfectType.repr }

def Semantics.Aspect.Core.instReprPerfectType.repr : PerfectType → ℕ → Std.Format

Equations

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

@[reducible, inline]

abbrev Semantics.Aspect.Core.universalPerfect {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : Events.EventPred W Time) : IntervalPred W Time

Universal perfect: PERF_P(UNBOUNDED(V)). "has been running" — event ongoing throughout PTS. @cite{pancheva-2003}: explains why universal reading requires imperfective.

Equations

• Semantics.Aspect.Core.universalPerfect P = Semantics.Aspect.Core.PERF_P (Semantics.Aspect.Core.UNBOUNDED P)

@[reducible, inline]

abbrev Semantics.Aspect.Core.experientialPerfect {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : Events.EventPred W Time) : IntervalPred W Time

Experiential perfect: PERF_P(INIT_OVERLAP(V)). "has visited Paris" — event began within PTS. @cite{pancheva-2003}: initial-overlap aspect allows event to extend beyond PTS.

Equations

• Semantics.Aspect.Core.experientialPerfect P = Semantics.Aspect.Core.PERF_P (Semantics.Aspect.Core.INIT_OVERLAP P)

@[reducible, inline]

abbrev Semantics.Aspect.Core.resultativePerfect {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : Events.EventPred W Time) : IntervalPred W Time

Resultative perfect: PERF_P(BOUNDED(V)). "has broken the vase" — event completed within PTS. Simplified: properly involves result state (@cite{pancheva-2003}: 288).

Equations

• Semantics.Aspect.Core.resultativePerfect P = Semantics.Aspect.Core.PERF_P (Semantics.Aspect.Core.BOUNDED P)

theorem Semantics.Aspect.Core.perf_prog_entails_universal_at_point {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (P : Events.EventPred W Time) (w : W) (t : Time) : perfProg P { world := w, time := t } → universalPerfect P w (Core.Time.Interval.point t)

perfProg at a point entails universalPerfect at that point. Since IMPF (strict ⊂) entails UNBOUNDED (non-strict ⊆), PERF(IMPF(V)) entails PERF(UNBOUNDED(V)) = universalPerfect.

def Semantics.Aspect.Core.IntervalPred.atPoint {Time : Type u_1} [LinearOrder Time] {W : Type u_2} (p : IntervalPred W Time) : PointPred W Time

Evaluate an interval predicate at a point (trivial interval [t, t]). Bridge for non-perfect forms.

Equations

• p.atPoint s = p s.world (Core.Time.Interval.point s.time)