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