DFF-formal-definition