### Abstract

These theories formalize region quadtrees, which are traditionally used to represent two-dimensional images of (black and white) pixels. Building on these quadtrees, addition and multiplication of recursive block matrices are verified. The generalization of region quadtrees to \(k\) dimensions is also formalized.

### License

BSD License

### Topics

- Computer science/Data structures

### Session Region_Quadtrees

- Quad_Base
- Quad_Tree
- Quad_Matrix
- KD_Region_Tree
- KD_Region_Tree2
- KD_Region_Nested

## Cite

×

Region_Quadtrees-AFP

    @article{Region_Quadtrees-AFP,
      author  = {Tobias Nipkow},
      title   = {Region Quadtrees},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2024},
      note    = {\url{https://isa-afp.org/entries/Region_Quadtrees.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest