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.


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.


BSD License


Session Region_Quadtrees