Simon's Factorization Theorem is a powerful tool in the study of formal languages, and is key to many algorithms and theoretical results.
The theorem states that, given a regular language, we can decompose any word to a bounded-height tree that allows reasoning about all infixes of the word in a compact manner.
In this work, we generalize Simon's factorization theorem to languages of trees. This generalization brings about many challenges involving the manipulation of trees and forests. Specifically, even defining what a decomposition of trees means is highly nontrivial. We provide such a notion, and show how to obtain it (with a caveat).