theorem proved term proof

`gray_code_one_bit_property`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 146theorem gray_code_one_bit_property :
 147  ∀ (d n : ℕ), n + 1 < 2^d →
 148    ∃! k : ℕ, k < d ∧
 149      (n ^^^ (n >>> 1)).testBit k ≠ ((n+1) ^^^ ((n+1) >>> 1)).testBit k :=

proof body

Term-mode proof.

 150  GrayCodeFacts.gray_code_one_bit_property
 151
 152end GrayCodeAxioms
 153end Patterns
 154end IndisputableMonolith

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

GrayCodeFacts in IndisputableMonolith.Patterns.GrayCodeAxioms decl_use
brgc_oneBit_step in IndisputableMonolith.Patterns.GrayCycleGeneral decl_use

depends on (1)

Lean names referenced from this declaration's body.

GrayCodeFacts in IndisputableMonolith.Patterns.GrayCodeAxioms decl_use