bor

formal source

  44  rcases a.is_bit with ha | ha <;> rcases b.is_bit with hb | hb <;> simp [ha, hb]
  45
  46/-- Arithmetic disjunction on stable states (`a + b - ab` on `0/1`). -/
  47def bor (a b : StableState) : StableState := by
  48  refine ⟨a.bit + b.bit - a.bit * b.bit, ?_⟩
  49  rcases a.is_bit with ha | ha <;> rcases b.is_bit with hb | hb <;> simp [ha, hb]
  50
  51/-- Arithmetic negation on stable states (`1 - a` on `0/1`). -/
  52def bnot (a : StableState) : StableState := by
  53  refine ⟨1 - a.bit, ?_⟩
  54  rcases a.is_bit with ha | ha <;> simp [ha]
  55
  56/-- The stable arithmetic states form a Boolean-style algebraic fragment. -/
  57theorem stable_forms_boolean_algebra :
  58    (∀ a b : StableState, (band a b).bit = a.bit * b.bit) ∧
  59    (∀ a b : StableState, (bor a b).bit = a.bit + b.bit - a.bit * b.bit) ∧
  60    (∀ a : StableState, (bnot a).bit = 1 - a.bit) := by
  61  constructor
  62  · intro a b
  63    rfl
  64  constructor
  65  · intro a b
  66    rfl
  67  · intro a
  68    rfl
  69
  70end PreLogicalCost
  71end Foundation
  72end IndisputableMonolith