Reference · Logic

rainbow.math.logic.interval-membership-sound

Logicsrc/rainbow/math/logic/interval_membership_sound.clj1 definitions, 1 theorems

Universal soundness of the two-clause interval/box membership test, composing the general boolean-AND soundness (rainbow.math.logic.boolean-and) with the decidable order: contains? lo hi x = and (decide (lo <= x)) (decide (x <= hi)) Proved for ALL lo, hi, x: contains-sound : contains? lo hi x = true -> (lo <= x) AND (x <= hi) So whenever the membership test accepts a point, the point provably satisfies both interval bounds -- the universal guarantee behind the AHoF interval/reachability/box membership rows (V40, V41, V33, V34, V59, ...), which the catalog only exercised on worked instances. Native and axiom-free; chains rainbow.math.logic.boolean-and.

ims/contains? :
  (x₁ x₂ x₃ : ℚ≥0)
  → data/Bool

ims/contains-sound :
  (lo hi x : ℚ≥0)
  (h₁ : ims/contains? lo hi x = data/true)
  → proposition/conjunction (lo ≤ x) (x ≤ hi)