IndisputableMonolith.Patterns.GrayCycle

declarations in this module (20)

• def OneBitDiff L37
• lemma OneBitDiff_symm L40
• structure GrayCycle L53
• structure GrayCover L62
• theorem grayCover_min_ticks L68
• theorem grayCover_eight_tick_min L71
• def pattern3 L82
• def gray8At L95
• def grayCycle3Path L106
• theorem gray8At_injective L109
• def toNat3 L117
• lemma toNat3_pattern3 L122
• theorem pattern3_injective L126
• theorem grayCycle3_injective L132
• theorem grayCycle3_bijective L137
• theorem grayCycle3_surjective L154
• theorem grayCycle3_oneBit_step L157
• def grayCycle3 L203
• theorem grayCycle3_period L209
• def grayCover3 L212