Reference · Logic

rainbow.math.logic.boolean-and

Logicsrc/rainbow/math/logic/boolean_and.clj1 definitions, 3 theorems

General soundness of the boolean AND used across the AHoF membership/monitor rows (interval containment, 2-D ODD boxes, polytope halfspaces, ...): and a b = if a then b else false (a Bool.rec over the first operand) Proved for ALL booleans a, b: and-implies-left : and a b = true -> a = true and-implies-right : and a b = true -> b = true and-sound : and a b = true -> (a = true) AND (b = true) The catalog rows established two-clause membership only on worked instances; these theorems make the conjunction's soundness universal, so any decidable two-clause test (lo<=x AND x<=hi, a1.x<=b1 AND a2.x<=b2, ...) that returns true genuinely entails both clauses. Case-split on the first operand via data/Bool.rec; the false branch is discharged by bool/false-not-true + proposition/explode. Native and axiom-free.

boolean/and :
  (x₁ x₂ : data/Bool)
  → data/Bool

boolean/and-implies-left :
  (a b : data/Bool)
  (h₁ : boolean/and a b = data/true)
  → a = data/true

boolean/and-implies-right :
  (a b : data/Bool)
  (h₁ : boolean/and a b = data/true)
  → b = data/true

boolean/and-sound :
  (a b : data/Bool)
  (h₁ : boolean/and a b = data/true)
  → proposition/conjunction (a = data/true) (b = data/true)