| Expression | Month_known_validity: not month_known implies not day_known
Day_known_validity: not day_known implies not hour_known
Hour_known_validity: not hour_known implies not minute_known
Enclosing_interval: month_known implies enclosing_interval.lower.day = 1
and enclosing_interval.upper.day = days_in_month(month, year) and not
month_known implies enclosing_interval.lower.month = 1 and
enclosing_interval.upper.month = Months_in_year and
enclosing_interval.lower.day = 1 and enclosing_interval.upper.day =
days_in_month(Months_in_year, year) and
minute_known implies enclosing_interval.lower.second = 1 and
enclosing_interval.upper.second = Seconds_in_minute and
not minute_known implies enclosing_interval.lower.minute = 1 and
enclosing_interval.upper.minute = Minutes_in_hour and
enclosing_interval.lower.second = 1 and enclosing_interval.upper.second =
Seconds_in_minute |