A defining equality must have an interpreted left-hand side. Functions nested within an uninterpreted function must also be uninterpreted. Functions nested within an uninterpreted function must also be uninterpreted. Equalities within an equivalence expression must either both be interpreted or both uninterpreted.