def
definition
bnot
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.PreLogicalCost on GitHub at line 52.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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