Allen's Interval Relations

@cite{allen-1983}

The thirteen jointly-exhaustive, pairwise-disjoint relations that can hold between two intervals on a linear order. Originally introduced by James F. Allen for temporal reasoning in AI, this is the canonical relation algebra that Reichenbach, Klein, Pancheva, and Declerck all draw from — every temporal predicate in linglib is a (possibly singleton) subset of these thirteen atomic relations.

Atom	Symbol	Inverse	Defining inequality
precedes	p	precededBy	i.finish < j.start
meets	m	metBy	i.finish = j.start
overlaps	o	overlappedBy	i.start < j.start < i.finish < j.finish
finishedBy	F	finishes	i.start < j.start, i.finish = j.finish
contains	D	during	i.start < j.start, j.finish < i.finish
starts	s	startedBy	i.start = j.start, i.finish < j.finish
equal	e	equal	i.start = j.start, i.finish = j.finish
startedBy	S	starts	i.start = j.start, j.finish < i.finish
during	d	contains	j.start < i.start, i.finish < j.finish
finishes	f	finishedBy	j.start < i.start, i.finish = j.finish
overlappedBy	O	overlaps	j.start < i.start < j.finish < i.finish
metBy	M	meets	i.start = j.finish
precededBy	P	precedes	j.finish < i.start

For any two intervals on a linear order, at least one atomic relation holds (holds_exists). When both intervals are non-degenerate (start < finish), exactly one holds (holds_unique). The non-degeneracy hypothesis matches @cite{allen-1983}'s original setup: on point intervals at the same location, meets, metBy, and equal all hold simultaneously, so uniqueness genuinely fails on degenerate inputs. Both proofs use mathlib's order decision procedure for LinearOrder.

Existing Interval predicates (subinterval, isBefore, finalSubinterval, …) are unions of atomic Allen relations — see the Predicate Bridges section.

The Allen algebra also has a 13×13 composition table giving, for each pair (r, s), the set of relations consistent with i r j ∧ j s k. We provide identity laws and the principal compositions used by tense theory; the full table is left as a TODO.

Core.Time.Relation (in Time.lean) is the point analogue (operating on Time × Time); on point intervals it collapses to {precedes, equal, precededBy} (the only three Allen relations consistent with zero-length intervals).

inductive Core.Time.AllenRelation : Type

The thirteen atomic Allen relations between two intervals on a linear order (@cite{allen-1983}). Naming follows Allen 1983; each atom has an inverse obtained by swapping the two interval arguments — see AllenRelation.inverse.

• precedes : AllenRelation

  i.finish < j.start — i ends strictly before j starts.

• meets : AllenRelation

  i.finish = j.start — i's right endpoint is j's left endpoint.

• overlaps : AllenRelation

  i.start < j.start < i.finish < j.finish — proper overlap on the right of i.

• finishedBy : AllenRelation

  i.start < j.start ∧ i.finish = j.finish — j is a final subinterval of i.

• contains : AllenRelation

  i.start < j.start ∧ j.finish < i.finish — j strictly inside i.

• starts : AllenRelation

  i.start = j.start ∧ i.finish < j.finish — i is a proper initial subinterval of j.

• equal : AllenRelation

  i.start = j.start ∧ i.finish = j.finish — identical intervals.

• startedBy : AllenRelation

  i.start = j.start ∧ j.finish < i.finish — j is a proper initial subinterval of i.

• during : AllenRelation

  j.start < i.start ∧ i.finish < j.finish — i strictly inside j.

• finishes : AllenRelation

  j.start < i.start ∧ i.finish = j.finish — i is a final subinterval of j.

• overlappedBy : AllenRelation

  j.start < i.start < j.finish < i.finish — proper overlap on the left of i.

• metBy : AllenRelation

  i.start = j.finish — i's left endpoint is j's right endpoint.

• precededBy : AllenRelation

  j.finish < i.start — j ends strictly before i starts.

@[implicit_reducible]

instance Core.Time.instDecidableEqAllenRelation : DecidableEq AllenRelation

Equations

• Core.Time.instDecidableEqAllenRelation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.Time.instReprAllenRelation : Repr AllenRelation

Equations

• Core.Time.instReprAllenRelation = { reprPrec := Core.Time.instReprAllenRelation.repr }

def Core.Time.instReprAllenRelation.repr : AllenRelation → ℕ → Std.Format

Equations

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

def Core.Time.instInhabitedAllenRelation.default : AllenRelation

Equations

• Core.Time.instInhabitedAllenRelation.default = Core.Time.AllenRelation.precedes

@[implicit_reducible]

instance Core.Time.instInhabitedAllenRelation : Inhabited AllenRelation

Equations

• Core.Time.instInhabitedAllenRelation = { default := Core.Time.instInhabitedAllenRelation.default }

def Core.Time.AllenRelation.inverse : AllenRelation → AllenRelation

The inverse of an atom: the relation that holds when the two intervals are swapped. equal is the unique self-inverse atom.

Equations

• Core.Time.AllenRelation.precedes.inverse = Core.Time.AllenRelation.precededBy
• Core.Time.AllenRelation.meets.inverse = Core.Time.AllenRelation.metBy
• Core.Time.AllenRelation.overlaps.inverse = Core.Time.AllenRelation.overlappedBy
• Core.Time.AllenRelation.finishedBy.inverse = Core.Time.AllenRelation.finishes
• Core.Time.AllenRelation.contains.inverse = Core.Time.AllenRelation.during
• Core.Time.AllenRelation.starts.inverse = Core.Time.AllenRelation.startedBy
• Core.Time.AllenRelation.equal.inverse = Core.Time.AllenRelation.equal
• Core.Time.AllenRelation.startedBy.inverse = Core.Time.AllenRelation.starts
• Core.Time.AllenRelation.during.inverse = Core.Time.AllenRelation.contains
• Core.Time.AllenRelation.finishes.inverse = Core.Time.AllenRelation.finishedBy
• Core.Time.AllenRelation.overlappedBy.inverse = Core.Time.AllenRelation.overlaps
• Core.Time.AllenRelation.metBy.inverse = Core.Time.AllenRelation.meets
• Core.Time.AllenRelation.precededBy.inverse = Core.Time.AllenRelation.precedes

@[simp]

theorem Core.Time.AllenRelation.inverse_inverse (r : AllenRelation) : r.inverse.inverse = r

theorem Core.Time.AllenRelation.inverse_eq_self_iff (r : AllenRelation) : r.inverse = r ↔ r = equal

equal is the unique self-inverse atom.

def Core.Time.AllenRelation.all : List AllenRelation

The set of all thirteen atoms — useful for stating exhaustiveness.

Equations

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

theorem Core.Time.AllenRelation.all_length : all.length = 13

theorem Core.Time.AllenRelation.mem_all (r : AllenRelation) : r ∈ all

def Core.Time.AllenRelation.holds {Time : Type u_1} [LinearOrder Time] : AllenRelation → Interval Time → Interval Time → Prop

r.holds i j is true iff atomic Allen relation r is the one that holds between intervals i and j. The defining inequalities follow @cite{allen-1983}.

Equations

• Core.Time.AllenRelation.precedes.holds x✝¹ x✝ = (x✝¹.finish < x✝.start)
• Core.Time.AllenRelation.meets.holds x✝¹ x✝ = (x✝¹.finish = x✝.start)
• Core.Time.AllenRelation.overlaps.holds x✝¹ x✝ = (x✝¹.start < x✝.start ∧ x✝.start < x✝¹.finish ∧ x✝¹.finish < x✝.finish)
• Core.Time.AllenRelation.finishedBy.holds x✝¹ x✝ = (x✝¹.start < x✝.start ∧ x✝¹.finish = x✝.finish)
• Core.Time.AllenRelation.contains.holds x✝¹ x✝ = (x✝¹.start < x✝.start ∧ x✝.finish < x✝¹.finish)
• Core.Time.AllenRelation.starts.holds x✝¹ x✝ = (x✝¹.start = x✝.start ∧ x✝¹.finish < x✝.finish)
• Core.Time.AllenRelation.equal.holds x✝¹ x✝ = (x✝¹.start = x✝.start ∧ x✝¹.finish = x✝.finish)
• Core.Time.AllenRelation.startedBy.holds x✝¹ x✝ = (x✝¹.start = x✝.start ∧ x✝.finish < x✝¹.finish)
• Core.Time.AllenRelation.during.holds x✝¹ x✝ = (x✝.start < x✝¹.start ∧ x✝¹.finish < x✝.finish)
• Core.Time.AllenRelation.finishes.holds x✝¹ x✝ = (x✝.start < x✝¹.start ∧ x✝¹.finish = x✝.finish)
• Core.Time.AllenRelation.overlappedBy.holds x✝¹ x✝ = (x✝.start < x✝¹.start ∧ x✝¹.start < x✝.finish ∧ x✝.finish < x✝¹.finish)
• Core.Time.AllenRelation.metBy.holds x✝¹ x✝ = (x✝¹.start = x✝.finish)
• Core.Time.AllenRelation.precededBy.holds x✝¹ x✝ = (x✝.finish < x✝¹.start)

theorem Core.Time.AllenRelation.holds_inverse {Time : Type u_1} [LinearOrder Time] (r : AllenRelation) (i j : Interval Time) : r.holds i j ↔ r.inverse.holds j i

Holds is symmetric under inversion: r holds of (i, j) iff r⁻¹ holds of (j, i). This is the central algebraic property of the inverse operation.

def Core.Time.AllenRelation.witness {Time : Type u_1} [LinearOrder Time] (i j : Interval Time) : { r : AllenRelation // r.holds i j }

Exhaustiveness (constructive witness): every interval pair satisfies at least one atomic Allen relation, computably. The case-split mirrors @cite{allen-1983}'s exhaustive enumeration: trichotomy on i.finish vs j.start, then i.start vs j.finish, then refinement on i.start vs j.start and i.finish vs j.finish. Used to derive the constructive Interval.allenRel projection.

Equations

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

theorem Core.Time.AllenRelation.holds_exists {Time : Type u_1} [LinearOrder Time] (i j : Interval Time) : ∃ (r : AllenRelation), r.holds i j

Exhaustiveness (existence half): every interval pair satisfies at least one atomic Allen relation. Existential projection of witness.

Each non-degenerate interval pair (i, j) has a four-tuple signature: the pairwise sgn (lt/eq/gt) of every endpoint of i with every endpoint of j. The thirteen Allen atoms correspond bijectively to thirteen of the 81 possible signature tuples (the other 68 are excluded by i.start < i.finish and j.start < j.finish). Factoring uniqueness through this signature reduces the 169-case cross-product cases r₁ <;> cases r₂ (which needs 6× the default heartbeat budget) into two 13-case lemmas.

def Core.Time.sgn {Time : Type u_1} [LinearOrder Time] (a b : Time) : Ordering

Three-way sign of a vs b on a linear order.

Equations

• Core.Time.sgn a b = if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt

theorem Core.Time.sgn_lt {Time : Type u_1} [LinearOrder Time] {a b : Time} (h : a < b) : sgn a b = Ordering.lt

theorem Core.Time.sgn_eq {Time : Type u_1} [LinearOrder Time] {a b : Time} (h : a = b) : sgn a b = Ordering.eq

theorem Core.Time.sgn_gt {Time : Type u_1} [LinearOrder Time] {a b : Time} (h : b < a) : sgn a b = Ordering.gt

def Core.Time.signature {Time : Type u_1} [LinearOrder Time] (i j : Interval Time) : Ordering × Ordering × Ordering × Ordering

The 4-tuple signature of an interval pair: pairwise comparisons of (i.start vs j.start, i.start vs j.finish, i.finish vs j.start, i.finish vs j.finish).

Equations

• Core.Time.signature i j = (Core.Time.sgn i.start j.start, Core.Time.sgn i.start j.finish, Core.Time.sgn i.finish j.start, Core.Time.sgn i.finish j.finish)

def Core.Time.AllenRelation.expectedSig : AllenRelation → Ordering × Ordering × Ordering × Ordering

The expected signature of each Allen atom — the unique 4-tuple of pairwise endpoint comparisons forced by the atom's defining inequalities together with non-degeneracy of both intervals.

Equations

• Core.Time.AllenRelation.precedes.expectedSig = (Ordering.lt, Ordering.lt, Ordering.lt, Ordering.lt)
• Core.Time.AllenRelation.meets.expectedSig = (Ordering.lt, Ordering.lt, Ordering.eq, Ordering.lt)
• Core.Time.AllenRelation.overlaps.expectedSig = (Ordering.lt, Ordering.lt, Ordering.gt, Ordering.lt)
• Core.Time.AllenRelation.finishedBy.expectedSig = (Ordering.lt, Ordering.lt, Ordering.gt, Ordering.eq)
• Core.Time.AllenRelation.contains.expectedSig = (Ordering.lt, Ordering.lt, Ordering.gt, Ordering.gt)
• Core.Time.AllenRelation.starts.expectedSig = (Ordering.eq, Ordering.lt, Ordering.gt, Ordering.lt)
• Core.Time.AllenRelation.equal.expectedSig = (Ordering.eq, Ordering.lt, Ordering.gt, Ordering.eq)
• Core.Time.AllenRelation.startedBy.expectedSig = (Ordering.eq, Ordering.lt, Ordering.gt, Ordering.gt)
• Core.Time.AllenRelation.during.expectedSig = (Ordering.gt, Ordering.lt, Ordering.gt, Ordering.lt)
• Core.Time.AllenRelation.finishes.expectedSig = (Ordering.gt, Ordering.lt, Ordering.gt, Ordering.eq)
• Core.Time.AllenRelation.overlappedBy.expectedSig = (Ordering.gt, Ordering.lt, Ordering.gt, Ordering.gt)
• Core.Time.AllenRelation.metBy.expectedSig = (Ordering.gt, Ordering.eq, Ordering.gt, Ordering.gt)
• Core.Time.AllenRelation.precededBy.expectedSig = (Ordering.gt, Ordering.gt, Ordering.gt, Ordering.gt)

theorem Core.Time.AllenRelation.expectedSig_injective (r₁ r₂ : AllenRelation) (h : r₁.expectedSig = r₂.expectedSig) : r₁ = r₂

The thirteen expected signatures are pairwise distinct: any two atoms with the same signature are equal. (13-case diagonal + 156 trivial simp contradictions on Ordering constructor mismatch.)

theorem Core.Time.AllenRelation.signature_of_holds {Time : Type u_1} [LinearOrder Time] (r : AllenRelation) (i j : Interval Time) (hi : i.start < i.finish) (hj : j.start < j.finish) (h : r.holds i j) : signature i j = r.expectedSig

If atom r holds of a non-degenerate interval pair, the pair's signature is exactly r.expectedSig. (13 cases, each computing four sgn components via Prod.ext + the appropriate sgn_* lemma + order.)

theorem Core.Time.AllenRelation.holds_unique {Time : Type u_1} [LinearOrder Time] (i j : Interval Time) (hi : i.start < i.finish) (hj : j.start < j.finish) (r₁ r₂ : AllenRelation) (h₁ : r₁.holds i j) (h₂ : r₂.holds i j) : r₁ = r₂

Uniqueness (pairwise disjointness): on non-degenerate intervals (i.start < i.finish and j.start < j.finish), at most one atom holds of a given pair. Combined with holds_exists, this gives the key property of Allen's algebra: the thirteen atoms partition the space of (proper) interval pairs into thirteen exhaustive, pairwise-disjoint cases.

The non-degeneracy hypothesis is essential: at a single time point t, taking i = j = ⟨t, t, le_refl t⟩ makes meets (t = t), metBy (t = t), and equal (t = t ∧ t = t) all hold simultaneously. @cite{allen-1983} sidesteps this by assuming strict intervals throughout.

Proof: factor through the 4-tuple signature. Both r₁ and r₂ force the same signature (signature_of_holds), and distinct atoms have distinct signatures (expectedSig_injective).

Many natural temporal predicates correspond to unions of Allen atoms — "at least one of these atoms holds." We express this uniformly via holdsIn, and name the atom-sets that appear in the Interval predicate API. Each existing Interval predicate is then a projection from a named atom-set: this exposes the algebraic structure (S₁ ⊆ S₂ ⇒ holdsIn S₁ ⇒ holdsIn S₂) and grounds each predicate in the Allen algebra by construction.

Singleton sets (`precedesSet`, `meetsSet`) recover individual atoms
as predicates; longer sets give the union predicates that linguistic
theory typically works with. The atom sets are first-class data, so
later modules (`Domain`, `RelationOrigin`, …) can manipulate them
uniformly without committing to a specific predicate at the
type level. 

def Core.Time.AllenRelation.holdsIn {Time : Type u_1} [LinearOrder Time] (S : List AllenRelation) (i j : Interval Time) : Prop

"holdsIn S i j" iff some atom in the list S is the relation holding between i and j. Singleton lists yield exact-atom predicates; longer lists yield union predicates.

Equations

• Core.Time.AllenRelation.holdsIn S i j = ∃ r ∈ S, r.holds i j

@[simp]

theorem Core.Time.AllenRelation.holdsIn_nil {Time : Type u_1} [LinearOrder Time] (i j : Interval Time) : holdsIn [] i j ↔ False

@[simp]

theorem Core.Time.AllenRelation.holdsIn_singleton {Time : Type u_1} [LinearOrder Time] (r : AllenRelation) (i j : Interval Time) : holdsIn [r] i j ↔ r.holds i j

theorem Core.Time.AllenRelation.holdsIn_cons {Time : Type u_1} [LinearOrder Time] (r : AllenRelation) (S : List AllenRelation) (i j : Interval Time) : holdsIn (r :: S) i j ↔ r.holds i j ∨ holdsIn S i j

theorem Core.Time.AllenRelation.holdsIn_mono {Time : Type u_1} [LinearOrder Time] {S₁ S₂ : List AllenRelation} (h : ∀ r ∈ S₁, r ∈ S₂) (i j : Interval Time) : holdsIn S₁ i j → holdsIn S₂ i j

Subset monotonicity: enlarging the atom set weakens the predicate.

def Core.Time.AllenRelation.precedesSet : List AllenRelation

{precedes} — i.e., Interval.precedes.

Equations

• Core.Time.AllenRelation.precedesSet = [Core.Time.AllenRelation.precedes]

def Core.Time.AllenRelation.equalSet : List AllenRelation

{equal} — interval coincidence; on point intervals collapses to point equality, the relation behind Reichenbach's R = P etc.

Equations

• Core.Time.AllenRelation.equalSet = [Core.Time.AllenRelation.equal]

def Core.Time.AllenRelation.meetsSet : List AllenRelation

{meets} — i.e., Interval.meets.

Equations

• Core.Time.AllenRelation.meetsSet = [Core.Time.AllenRelation.meets]

def Core.Time.AllenRelation.beforeSet : List AllenRelation

{precedes, meets} — i.e., Interval.isBefore: strict precedence plus meeting (the conflation i.finish ≤ j.start represents).

Equations

• Core.Time.AllenRelation.beforeSet = [Core.Time.AllenRelation.precedes, Core.Time.AllenRelation.meets]

def Core.Time.AllenRelation.afterSet : List AllenRelation

{precededBy, metBy} — i.e., Interval.isAfter.

Equations

• Core.Time.AllenRelation.afterSet = [Core.Time.AllenRelation.precededBy, Core.Time.AllenRelation.metBy]

def Core.Time.AllenRelation.containmentSet : List AllenRelation

{starts, equal, finishes, during} — i.e., Interval.subinterval: every way i can be contained in j.

Equations

• Core.Time.AllenRelation.containmentSet = [Core.Time.AllenRelation.starts, Core.Time.AllenRelation.equal, Core.Time.AllenRelation.finishes, Core.Time.AllenRelation.during]

def Core.Time.AllenRelation.properContainmentSet : List AllenRelation

{starts, finishes, during} — i.e., Interval.properSubinterval: proper containment (excludes equal).

Equations

• Core.Time.AllenRelation.properContainmentSet = [Core.Time.AllenRelation.starts, Core.Time.AllenRelation.finishes, Core.Time.AllenRelation.during]

def Core.Time.AllenRelation.finalContainmentSet : List AllenRelation

{finishes, equal} — i.e., Interval.finalSubinterval: contained and sharing the right endpoint.

Equations

• Core.Time.AllenRelation.finalContainmentSet = [Core.Time.AllenRelation.finishes, Core.Time.AllenRelation.equal]

def Core.Time.AllenRelation.reverseContainmentSet : List AllenRelation

{startedBy, equal, finishedBy, contains} — the inverse of containmentSet: every way i can contain j.

Equations

• Core.Time.AllenRelation.reverseContainmentSet = [Core.Time.AllenRelation.startedBy, Core.Time.AllenRelation.equal, Core.Time.AllenRelation.finishedBy, Core.Time.AllenRelation.contains]

def Core.Time.AllenRelation.overlapSet : List AllenRelation

Eleven atoms — every relation except strict precedence in either direction — i.e., Interval.overlaps's union characterization.

Equations

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

Existing Interval predicates equated to projections from named Allen atom-sets via holdsIn. The singleton-atom predicates (precedes, meets) collapse to Iff.rfl; the union predicates require structural-form ↔ disjunction-form translations. These are the only place where the structural definitions in Core/Temporal/Time.lean meet the Allen algebra; downstream modules should depend on the Allen side.

theorem Core.Time.Interval.precedes_iff_allen {Time : Type u_1} [LinearOrder Time] (i j : Interval Time) : i.precedes j ↔ AllenRelation.holdsIn AllenRelation.precedesSet i j

Interval.precedes is exactly the Allen precedes atom.

theorem Core.Time.Interval.meets_iff_allen {Time : Type u_1} [LinearOrder Time] (i j : Interval Time) : i.meets j ↔ AllenRelation.holdsIn AllenRelation.meetsSet i j

Interval.meets is exactly the Allen meets atom.

theorem Core.Time.Interval.isBefore_iff_allen {Time : Type u_1} [LinearOrder Time] (i j : Interval Time) : i.isBefore j ↔ AllenRelation.holdsIn AllenRelation.beforeSet i j

Interval.isBefore (≤) is the union {precedes, meets} — Allen's strict precedes plus meets. This conflation of two atoms into one weakened predicate is exactly the kind of imprecision the Allen algebra removes.

theorem Core.Time.Interval.isAfter_iff_allen {Time : Type u_1} [LinearOrder Time] (i j : Interval Time) : i.isAfter j ↔ AllenRelation.holdsIn AllenRelation.afterSet i j

Interval.isAfter is the inverse of isBefore: {precededBy, metBy}.

theorem Core.Time.Interval.subinterval_iff_allen {Time : Type u_1} [LinearOrder Time] (i j : Interval Time) : i.subinterval j ↔ AllenRelation.holdsIn AllenRelation.containmentSet i j

Interval.subinterval (i ⊆ j) is the union {starts, equal, finishes, during} — every way i can be contained in j without sharing the wrong boundary.

theorem Core.Time.Interval.finalSubinterval_iff_allen {Time : Type u_1} [LinearOrder Time] (i j : Interval Time) : i.finalSubinterval j ↔ AllenRelation.holdsIn AllenRelation.finalContainmentSet i j

Interval.finalSubinterval is the union {finishes, equal} — contained in j and sharing j's right endpoint.

theorem Core.Time.Interval.properSubinterval_iff_allen {Time : Type u_1} [LinearOrder Time] (i j : Interval Time) : i.properSubinterval j ↔ AllenRelation.holdsIn AllenRelation.properContainmentSet i j

Interval.properSubinterval is the union {starts, finishes, during} — containment that excludes the equal case.

@[implicit_reducible]

instance Core.Time.AllenRelation.holds_decidable {Time : Type u_1} [LinearOrder Time] [DecidableEq Time] [DecidableRel fun (x1 x2 : Time) => x1 < x2] (r : AllenRelation) (i j : Interval Time) : Decidable (r.holds i j)

holds is decidable on a linear order (provided < and = are).

Equations

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

The full Allen composition table assigns to each pair (r, s) the set of relations consistent with i r j ∧ j s k. The table has 169 entries and is left as a TODO. We provide the identity laws plus the principal transitive closures used by tense theory.

Convention: `holds_*_trans` reads "if r holds of (i, j) and r holds
of (j, k), then r holds of (i, k)" for the relations that are transitive. 

theorem Core.Time.AllenRelation.holds_equal_left {Time : Type u_1} [LinearOrder Time] {i j k : Interval Time} (r : AllenRelation) (h₁ : equal.holds i j) (h₂ : r.holds j k) : r.holds i k

equal is a left identity: if i = j and j r k, then i r k.

theorem Core.Time.AllenRelation.holds_equal_right {Time : Type u_1} [LinearOrder Time] {i j k : Interval Time} (r : AllenRelation) (h₁ : r.holds i j) (h₂ : equal.holds j k) : r.holds i k

equal is a right identity: if i r j and j = k, then i r k.

theorem Core.Time.AllenRelation.holds_precedes_trans {Time : Type u_1} [LinearOrder Time] {i j k : Interval Time} (h₁ : precedes.holds i j) (h₂ : precedes.holds j k) : precedes.holds i k

precedes is transitive: i p j ∧ j p k → i p k. (The composition table entry precedes ∘ precedes is the singleton {precedes}.) The proof chains i.finish < j.start ≤ j.finish < k.start via j.valid.

theorem Core.Time.AllenRelation.holds_during_trans {Time : Type u_1} [LinearOrder Time] {i j k : Interval Time} (h₁ : during.holds i j) (h₂ : during.holds j k) : during.holds i k

The during relation is transitive: i ⊏ j ∧ j ⊏ k → i ⊏ k. (Composition entry during ∘ during = {during}.)

theorem Core.Time.AllenRelation.holds_contains_trans {Time : Type u_1} [LinearOrder Time] {i j k : Interval Time} (h₁ : contains.holds i j) (h₂ : contains.holds j k) : contains.holds i k

The contains relation is transitive (mirror of during).

The projection from interval pairs to Allen atoms — the inverse direction of holds. Defined by the constructive AllenRelation.witness, which case-splits on endpoint trichotomies. By holds_unique, on non-degenerate intervals the projection is forced — any atom that holds equals it. Together with holdsIn, this gives a full abstraction-and-projection layer over the algebra.

def Core.Time.Interval.allenRel {Time : Type u_1} [LinearOrder Time] (i j : Interval Time) : AllenRelation

The Allen atom currently holding between two intervals. Computable; extracted from the constructive AllenRelation.witness. For non-degenerate intervals this is well-defined: allenRel_unique proves every witness equals the projection.

Equations

• i.allenRel j = ↑(Core.Time.AllenRelation.witness i j)

theorem Core.Time.Interval.allenRel_holds {Time : Type u_1} [LinearOrder Time] (i j : Interval Time) : (i.allenRel j).holds i j

The projected atom does hold between the intervals.

theorem Core.Time.Interval.allenRel_unique {Time : Type u_1} [LinearOrder Time] (i j : Interval Time) (hi : i.start < i.finish) (hj : j.start < j.finish) {r : AllenRelation} (h : r.holds i j) : r = i.allenRel j

For non-degenerate intervals, the projection is unique: every atom that holds equals allenRel i j. This is the core "well- definedness" theorem for the projection — it justifies treating allenRel i j as the Allen relation between the two intervals.

theorem Core.Time.Interval.allenRel_mem_iff_holdsIn {Time : Type u_1} [LinearOrder Time] (i j : Interval Time) (hi : i.start < i.finish) (hj : j.start < j.finish) (S : List AllenRelation) : i.allenRel j ∈ S ↔ AllenRelation.holdsIn S i j

The projection lands in the named atom-set iff the corresponding holdsIn predicate holds. (For non-degenerate intervals; uses uniqueness to convert membership to existence.)