theorem
proved
stable_forms_boolean_algebra
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.PreLogicalCost on GitHub at line 57.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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