; GraphAtlas proof AE-01
; Statement: For every number of days with data in a year, from 1 to 366, the rank that Table 1 of Appendix N gives for the 98th percentile is the smallest whole number that is at least 2 per cent of the days, and the rank that Table 1 of Appendix T gives for the 99th percentile is the smallest whole number that is at least 1 per cent of them. Every count of days has a rank, and more days never lower it.
; About: rankFor in src/kernel/aermod.ts with the tables RANK_98 and RANK_99 as they are shipped. The rank of a count is the rank of the first row whose range holds it, as the code finds it. The statement is that the rank r satisfies r x 50 >= days and (r - 1) x 50 < days for the 98th percentile, and the same with 100 for the 99th. That is to say that r is the days divided by 50, or by 100, and rounded up.
; Source: 40 CFR Part 50, Appendix N and Appendix T, Table 1 of each
; Expected: unsat for each of the 8 checks below.
; Check with any SMT-LIB 2 solver, for example: z3 this-file.smt2

(declare-fun days_with_data () Int)
(declare-fun more_days_with_data () Int)
(assert (>= days_with_data 1))
(assert (<= days_with_data 366))
(assert (>= more_days_with_data days_with_data))
(assert (<= more_days_with_data 366))

; Goal 1, negated
(push 1)
(assert (not (let ((a!1 (ite (and (>= days_with_data 301) (<= days_with_data 350)) 7 (ite (and (>= days_with_data 351) (<= days_with_data 366)) 8 0)))) (let ((a!2 (ite (and (>= days_with_data 201) (<= days_with_data 250)) 5 (ite (and (>= days_with_data 251) (<= days_with_data 300)) 6 a!1)))) (let ((a!3 (ite (and (>= days_with_data 101) (<= days_with_data 150)) 3 (ite (and (>= days_with_data 151) (<= days_with_data 200)) 4 a!2)))) (let ((a!4 (ite (and (>= days_with_data 1) (<= days_with_data 50)) 1 (ite (and (>= days_with_data 51) (<= days_with_data 100)) 2 a!3)))) (>= a!4 1)))))))
(check-sat)
(pop 1)

; Goal 2, negated
(push 1)
(assert (not (let ((a!1 (ite (and (>= days_with_data 201) (<= days_with_data 300)) 3 (ite (and (>= days_with_data 301) (<= days_with_data 366)) 4 0)))) (let ((a!2 (ite (and (>= days_with_data 1) (<= days_with_data 100)) 1 (ite (and (>= days_with_data 101) (<= days_with_data 200)) 2 a!1)))) (>= a!2 1)))))
(check-sat)
(pop 1)

; Goal 3, negated
(push 1)
(assert (not (let ((a!1 (ite (and (>= days_with_data 301) (<= days_with_data 350)) 7 (ite (and (>= days_with_data 351) (<= days_with_data 366)) 8 0)))) (let ((a!2 (ite (and (>= days_with_data 201) (<= days_with_data 250)) 5 (ite (and (>= days_with_data 251) (<= days_with_data 300)) 6 a!1)))) (let ((a!3 (ite (and (>= days_with_data 101) (<= days_with_data 150)) 3 (ite (and (>= days_with_data 151) (<= days_with_data 200)) 4 a!2)))) (let ((a!4 (ite (and (>= days_with_data 1) (<= days_with_data 50)) 1 (ite (and (>= days_with_data 51) (<= days_with_data 100)) 2 a!3)))) (>= (* a!4 50) days_with_data)))))))
(check-sat)
(pop 1)

; Goal 4, negated
(push 1)
(assert (not (let ((a!1 (ite (and (>= days_with_data 301) (<= days_with_data 350)) 7 (ite (and (>= days_with_data 351) (<= days_with_data 366)) 8 0)))) (let ((a!2 (ite (and (>= days_with_data 201) (<= days_with_data 250)) 5 (ite (and (>= days_with_data 251) (<= days_with_data 300)) 6 a!1)))) (let ((a!3 (ite (and (>= days_with_data 101) (<= days_with_data 150)) 3 (ite (and (>= days_with_data 151) (<= days_with_data 200)) 4 a!2)))) (let ((a!4 (ite (and (>= days_with_data 1) (<= days_with_data 50)) 1 (ite (and (>= days_with_data 51) (<= days_with_data 100)) 2 a!3)))) (< (* (- a!4 1) 50) days_with_data)))))))
(check-sat)
(pop 1)

; Goal 5, negated
(push 1)
(assert (not (let ((a!1 (ite (and (>= days_with_data 201) (<= days_with_data 300)) 3 (ite (and (>= days_with_data 301) (<= days_with_data 366)) 4 0)))) (let ((a!2 (ite (and (>= days_with_data 1) (<= days_with_data 100)) 1 (ite (and (>= days_with_data 101) (<= days_with_data 200)) 2 a!1)))) (>= (* a!2 100) days_with_data)))))
(check-sat)
(pop 1)

; Goal 6, negated
(push 1)
(assert (not (let ((a!1 (ite (and (>= days_with_data 201) (<= days_with_data 300)) 3 (ite (and (>= days_with_data 301) (<= days_with_data 366)) 4 0)))) (let ((a!2 (ite (and (>= days_with_data 1) (<= days_with_data 100)) 1 (ite (and (>= days_with_data 101) (<= days_with_data 200)) 2 a!1)))) (< (* (- a!2 1) 100) days_with_data)))))
(check-sat)
(pop 1)

; Goal 7, negated
(push 1)
(assert (not (let ((a!1 (ite (and (>= more_days_with_data 301) (<= more_days_with_data 350)) 7 (ite (and (>= more_days_with_data 351) (<= more_days_with_data 366)) 8 0))) (a!5 (ite (and (>= days_with_data 301) (<= days_with_data 350)) 7 (ite (and (>= days_with_data 351) (<= days_with_data 366)) 8 0)))) (let ((a!2 (ite (and (>= more_days_with_data 201) (<= more_days_with_data 250)) 5 (ite (and (>= more_days_with_data 251) (<= more_days_with_data 300)) 6 a!1))) (a!6 (ite (and (>= days_with_data 201) (<= days_with_data 250)) 5 (ite (and (>= days_with_data 251) (<= days_with_data 300)) 6 a!5)))) (let ((a!3 (ite (and (>= more_days_with_data 101) (<= more_days_with_data 150)) 3 (ite (and (>= more_days_with_data 151) (<= more_days_with_data 200)) 4 a!2))) (a!7 (ite (and (>= days_with_data 101) (<= days_with_data 150)) 3 (ite (and (>= days_with_data 151) (<= days_with_data 200)) 4 a!6)))) (let ((a!4 (ite (and (>= more_days_with_data 1) (<= more_days_with_data 50)) 1 (ite (and (>= more_days_with_data 51) (<= more_days_with_data 100)) 2 a!3))) (a!8 (ite (and (>= days_with_data 1) (<= days_with_data 50)) 1 (ite (and (>= days_with_data 51) (<= days_with_data 100)) 2 a!7)))) (>= a!4 a!8)))))))
(check-sat)
(pop 1)

; Goal 8, negated
(push 1)
(assert (not (let ((a!1 (ite (and (>= more_days_with_data 201) (<= more_days_with_data 300)) 3 (ite (and (>= more_days_with_data 301) (<= more_days_with_data 366)) 4 0))) (a!3 (ite (and (>= days_with_data 201) (<= days_with_data 300)) 3 (ite (and (>= days_with_data 301) (<= days_with_data 366)) 4 0)))) (let ((a!2 (ite (and (>= more_days_with_data 1) (<= more_days_with_data 100)) 1 (ite (and (>= more_days_with_data 101) (<= more_days_with_data 200)) 2 a!1))) (a!4 (ite (and (>= days_with_data 1) (<= days_with_data 100)) 1 (ite (and (>= days_with_data 101) (<= days_with_data 200)) 2 a!3)))) (>= a!2 a!4)))))
(check-sat)
(pop 1)