Detecting when UNNEST after a sequence of NESTs and UNNESTs can always be reversed with a single NEST

Algebraic database languages for nested relations use two operators, NEST and UNNEST, which change the nesting levels of relations. Consider a first-normal form relation scheme R and a sequence SEQ of NEST and UNNEST operators on R, with the last operator being an UNNEST on attribute Y. SEQ is single-nest-reversible if, for all instances r of R, the relation instance that preceded UNNEST is obtained, if SEQ(r) is nested on attribute Y. In the present work, the authors give (1) a necessary and sufficient condition that decides whether SEQ is single-nest-reversible or not; (2) the algorithm TEST to check the condition in (1) in O(n⁸) time where n is the length of SEQ; and (3) sound and complete axioms for functional dependencies in one-level nested relations