A term is constructed from constants and variables by applications of operations. All names used in terms may be qualified by the intended types, and the intended sort of the term may be specified. Note that the condition of a conditional term is a formula, not a term.