Region Quadtrees

Tobias Nipkow 📧

January 26, 2024

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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

Session Region_Quadtrees

Cite

× 
@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