The paper presents an extension of Higher-order Duration Calculus
(HDC,Zhou, Guelev and Zhan, 1999) by a polyadic least fixed point
operator and a class of non-logical symbols with a finite variability
restriction on their interpretations, which classifies these symbols
as intermediate between rigid symbols and flexible symbols as known
in DC. The least fixed point operator and the new kind of symbols
enable straightforward specification of recursion and data
manipulation by HDC. The paper contains a completeness theorem about
an extension of the proof system for HDC by axioms about the new
operator and symbols of finite variability for a class of so called
simple formulas, which extends the original class of simple formulas
in DC with iteration introduced in (Dang and Wang, 1994). The new
class extends the original one by allowing subformulas of finite
variability and existential quantification over both individual and
program variables. The completeness theorem is proved by the method
of local elimination of the extending operator, which was earlier
used for a similar purpose in (Guelev, 1998). Simple formulas suffice
to accommodate specification of Verilog semantics by HDC as in (Zhu
and He, 2000). The axioms about polyadic least fixed point operator
are paraphrases of the rules known from the propositional modal
mu-calculus(Kozen, 1983).