module module

`IndisputableMonolith.Patterns.GrayCycleGeneral`

show as: view Lean formalization →

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

generate prose now

depends on (5)

Lean names referenced from this declaration's body.

IndisputableMonolith.Patterns module_import
IndisputableMonolith.Patterns.GrayCode module_import
IndisputableMonolith.Patterns.GrayCodeAxioms module_import
IndisputableMonolith.Patterns.GrayCycle module_import
IndisputableMonolith.Patterns.GrayCycleBRGC module_import

declarations in this module (15)

def brgcPath L43
def allOnes L50
lemma allOnes_succ_eq_bit L52
lemma allOnes_testBit_lt L87
lemma allOnes_testBit_eq_false_at L103
theorem brgc_wrap_oneBitDiff L110
lemma natToGray_testBit_false_of_ge L184
theorem brgcPath_injective L204
lemma brgc_oneBit_step L233
def brgcGrayCycle L295
def brgcGrayCover L302
theorem exists_grayCycle L320
theorem exists_grayCover L324
theorem exists_grayCycle_of_le64 L327
theorem exists_grayCover_of_le64 L331