Prefix and projection onto state in duration calculus

We study a new operator of projection onto state and the prefix operator in the extension µHDC of DC by quantifiers over state and a polyadic least fixed point operator. We give axioms and rules to enable deduction in the extension of µHDC by the new operators. Our axioms can be used to eliminate the new operators from formulas in a practically significant fragment of µHDC. This entails the decidability of certain subfragments of this fragment is preserved in the presence of the new operators