The CoLiS project aims at applying techniques from deductive program verification and analysis of tree transformations to the problem of analyzing shell scripts. The data structure that is manipulated by these scripts, namely the file system tree, is a complex one.

We plan to use feature trees as an abstract representation of file system tree transformations. We thus investigate an extension of these feature trees that includes the update operation, which expresses that two trees are similar except in a particular subtree where there might have been changes.

We show that the first-order theory of this algebra is decidable via a weak quantifier elimination procedure which is allowed to swap existential quantifiers for universal quantifiers.