; GraphAtlas proof AE-04
; Statement: A daily value of PM10 that a monitor keeps in tenths is an exceedance of a level exactly when it is at least 5 below the next multiple of 10 above the level, so for the level of 150 it is an exceedance from 155.0 on. A day from 150.1 to 154.9 is above the level and is not counted, and every day that is counted is above the level.
; About: exceedanceEdge in src/kernel/aermod.ts. Appendix K counts a day when its value, rounded to the nearest 10 with a value that ends in 5 or more going up, is above the level. The day is a whole number of tenths t, so the rounded value is 10 times the whole number part of (t + 50) divided by 100. A level is 10 k + u for u from 0 to 9, and the statement holds for every such level. The code gives 1550 tenths for the level of the PM10 standard, and the proof uses that number.
; Source: 40 CFR Part 50, Appendix K, Section 1.0(b), the definition of an exceedance
; Expected: unsat for each of the 4 checks below.
; Check with any SMT-LIB 2 solver, for example: z3 this-file.smt2

(declare-fun daily_value_in_tenths () Int)
(declare-fun whole_tens_in_level () Int)
(declare-fun units_in_level () Int)
(assert (>= daily_value_in_tenths 0))
(assert (<= daily_value_in_tenths 100000))
(assert (>= whole_tens_in_level 0))
(assert (<= whole_tens_in_level 1000))
(assert (>= units_in_level 0))
(assert (<= units_in_level 9))

; Goal 1, negated
(push 1)
(assert (not (let ((a!1 (> (* (div (+ daily_value_in_tenths 50) 100) 10) (+ (* whole_tens_in_level 10) units_in_level))) (a!2 (>= daily_value_in_tenths (- (* (+ whole_tens_in_level 1) 100) 50)))) (= a!1 a!2))))
(check-sat)
(pop 1)

; Goal 2, negated
(push 1)
(assert (not (let ((a!1 (> (* (div (+ daily_value_in_tenths 50) 100) 10) 150))) (= a!1 (>= daily_value_in_tenths 1550)))))
(check-sat)
(pop 1)

; Goal 3, negated
(push 1)
(assert (not (let ((a!1 (> (* (div (+ daily_value_in_tenths 50) 100) 10) 150))) (=> (and (> daily_value_in_tenths 1500) (< daily_value_in_tenths 1550)) (not a!1)))))
(check-sat)
(pop 1)

; Goal 4, negated
(push 1)
(assert (not (let ((a!1 (> (* (div (+ daily_value_in_tenths 50) 100) 10) 150))) (=> a!1 (> daily_value_in_tenths 1500)))))
(check-sat)
(pop 1)