| View: | Hide Browser | Browser on the left | Browser on the right | Dictionary |
| Report: | General Info |
| General Info | |
| Name | unnamed1 |
| Expression | post: Result implies (h>=o and h < Hours_in_day) and (m>=0 and m < Minutes_in_hour) and (s>=0 and s < Seconds_in_minute) |
| Base Classes | Operation |