### Abstract

The original Gray code after Frank Gray, also known as reflected binary code (RBC), is an ordering of the binary numeral system such that two successive values differ only in one bit. We provide a theory for a non-Boolean Gray code, which is a generalisation of the idea for an arbitrary base. Contained is the necessary theoretical environment to express and reason about the respective properties.

### License

BSD License

### Topics

- Mathematics/Combinatorics
- Computer science/Algorithms/Mathematical

### Related publications

- Sankar, K. J., Pandharipande, V. M., & Moharir, P. S. (n.d.). Generalized gray codes. Proceedings of 2004 International Symposium on Intelligent Signal Processing and Communication Systems, 2004. ISPACS 2004. https://doi.org/10.1109/ispacs.2004.1439140

### Session Gray_Codes

- Encoding_Nat
- Code_Word_Dist
- Non_Boolean_Gray

## Cite

×

Gray_Codes-AFP

    @article{Gray_Codes-AFP,
      author  = {Maximilian Spitz},
      title   = {Gray Codes for Arbitrary Numeral Systems},
      journal = {Archive of Formal Proofs},
      month   = {July},
      year    = {2023},
      note    = {\url{https://isa-afp.org/entries/Gray_Codes.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Jul 11, 2023 : Isabelle2022