; GraphAtlas proof AE-05
; Statement: A design value that is the mean of three values and is rounded half up as Appendices N and T say is at most the level exactly when the three add up to at most 1064 tenths for the 24-hour PM2.5 level of 35, which holds for values kept in whole tenths, and at most 2264 for the 1-hour SO2 level of 75 ppb. The annual mean is at most 9.0 exactly when the three annual means, which need not be whole tenths, add up to less than 27.15. For PM10 the design value is at most 1.0 exactly when the three yearly counts of days add up to at most 3.
; About: roundExact applied to a mean of three values, and the comparison with the level in designRun. When the three values are kept in whole tenths and add up to t tenths, their mean is t over 30, and rounding it half up to p places is the whole number part of (2 t 10^p + 30) divided by 60, in units of 10^-p. For the annual form each year is the mean of four quarterly means, so the three add up to any real number a, and the mean a over 3 rounds half up to a tenth. The level and the places of each form are those of FORMS. For PM10 the mean of three counts, c over 3, is rounded half up to a tenth, which is the whole number part of (20 c + 3) divided by 6 in tenths.
; Source: 40 CFR Part 50, Appendices N, T and K, Appendix N section 4.3, Appendix T section 4.1(c), Appendix K section 2.1(b)
; Expected: unsat for each of the 4 checks below.
; Check with any SMT-LIB 2 solver, for example: z3 this-file.smt2

(declare-fun three_values_added_in_tenths () Int)
(declare-fun three_annual_means_added_in_tenths () Real)
(declare-fun three_yearly_counts_added () Int)
(assert (>= three_values_added_in_tenths 0))
(assert (<= three_values_added_in_tenths 60000))
(assert (>= three_annual_means_added_in_tenths 0.0))
(assert (<= three_annual_means_added_in_tenths 60000.0))
(assert (>= three_yearly_counts_added 0))
(assert (<= three_yearly_counts_added 1100))

; Goal 1, negated
(push 1)
(assert (not (let ((a!1 (<= (div (+ (* three_values_added_in_tenths 2) 30) 60) 35))) (= a!1 (<= three_values_added_in_tenths 1064)))))
(check-sat)
(pop 1)

; Goal 2, negated
(push 1)
(assert (not (let ((a!1 (<= (div (+ (* three_values_added_in_tenths 2) 30) 60) 75))) (= a!1 (<= three_values_added_in_tenths 2264)))))
(check-sat)
(pop 1)

; Goal 3, negated
(push 1)
(assert (not (let ((a!1 (<= (to_int (+ (/ three_annual_means_added_in_tenths 3.0) (/ 1.0 2.0))) 90))) (= a!1 (< three_annual_means_added_in_tenths (/ 543.0 2.0))))))
(check-sat)
(pop 1)

; Goal 4, negated
(push 1)
(assert (not (let ((a!1 (<= (div (+ (* three_yearly_counts_added 20) 3) 6) 10))) (= a!1 (<= three_yearly_counts_added 3)))))
(check-sat)
(pop 1)