; GraphAtlas proof AE-03
; Statement: A day read as a monitor network keeps it is never above the same day read as a model takes it. It is below it by less than 0.2 for a mean of 24 hours and by less than 0.1 for the highest hour. The network cuts each hour off at a tenth and then cuts the mean of those off at a tenth again.
; About: dayAsMonitor and dayAsModel in src/kernel/aermod.ts for the 24 hours of one day. The hourly values are real numbers from 0 to 10,000. A monitor keeps each hour as a whole number of tenths, the greatest whole number not above ten times the hour, and keeps the day as the whole number of tenths that is not above the mean of those. A model takes the mean of the hours, or the highest hour, as it is. The statement compares the two in tenths.
; Source: 40 CFR Part 50, Appendix N and Appendix T, Appendix N section 3.0(b) and (c), Appendix T section 2(c) and section 4.1
; Expected: unsat for each of the 4 checks below.
; Check with any SMT-LIB 2 solver, for example: z3 this-file.smt2

(declare-fun hour_0 () Real)
(declare-fun hour_1 () Real)
(declare-fun hour_2 () Real)
(declare-fun hour_3 () Real)
(declare-fun hour_4 () Real)
(declare-fun hour_5 () Real)
(declare-fun hour_6 () Real)
(declare-fun hour_7 () Real)
(declare-fun hour_8 () Real)
(declare-fun hour_9 () Real)
(declare-fun hour_10 () Real)
(declare-fun hour_11 () Real)
(declare-fun hour_12 () Real)
(declare-fun hour_13 () Real)
(declare-fun hour_14 () Real)
(declare-fun hour_15 () Real)
(declare-fun hour_16 () Real)
(declare-fun hour_17 () Real)
(declare-fun hour_18 () Real)
(declare-fun hour_19 () Real)
(declare-fun hour_20 () Real)
(declare-fun hour_21 () Real)
(declare-fun hour_22 () Real)
(declare-fun hour_23 () Real)
(assert (and (>= hour_0 0.0) (<= hour_0 10000.0)))
(assert (and (>= hour_1 0.0) (<= hour_1 10000.0)))
(assert (and (>= hour_2 0.0) (<= hour_2 10000.0)))
(assert (and (>= hour_3 0.0) (<= hour_3 10000.0)))
(assert (and (>= hour_4 0.0) (<= hour_4 10000.0)))
(assert (and (>= hour_5 0.0) (<= hour_5 10000.0)))
(assert (and (>= hour_6 0.0) (<= hour_6 10000.0)))
(assert (and (>= hour_7 0.0) (<= hour_7 10000.0)))
(assert (and (>= hour_8 0.0) (<= hour_8 10000.0)))
(assert (and (>= hour_9 0.0) (<= hour_9 10000.0)))
(assert (and (>= hour_10 0.0) (<= hour_10 10000.0)))
(assert (and (>= hour_11 0.0) (<= hour_11 10000.0)))
(assert (and (>= hour_12 0.0) (<= hour_12 10000.0)))
(assert (and (>= hour_13 0.0) (<= hour_13 10000.0)))
(assert (and (>= hour_14 0.0) (<= hour_14 10000.0)))
(assert (and (>= hour_15 0.0) (<= hour_15 10000.0)))
(assert (and (>= hour_16 0.0) (<= hour_16 10000.0)))
(assert (and (>= hour_17 0.0) (<= hour_17 10000.0)))
(assert (and (>= hour_18 0.0) (<= hour_18 10000.0)))
(assert (and (>= hour_19 0.0) (<= hour_19 10000.0)))
(assert (and (>= hour_20 0.0) (<= hour_20 10000.0)))
(assert (and (>= hour_21 0.0) (<= hour_21 10000.0)))
(assert (and (>= hour_22 0.0) (<= hour_22 10000.0)))
(assert (and (>= hour_23 0.0) (<= hour_23 10000.0)))

; Goal 1, negated
(push 1)
(assert (not (let ((a!1 (div (+ (to_int (* hour_0 10.0)) (to_int (* hour_1 10.0)) (to_int (* hour_2 10.0)) (to_int (* hour_3 10.0)) (to_int (* hour_4 10.0)) (to_int (* hour_5 10.0)) (to_int (* hour_6 10.0)) (to_int (* hour_7 10.0)) (to_int (* hour_8 10.0)) (to_int (* hour_9 10.0)) (to_int (* hour_10 10.0)) (to_int (* hour_11 10.0)) (to_int (* hour_12 10.0)) (to_int (* hour_13 10.0)) (to_int (* hour_14 10.0)) (to_int (* hour_15 10.0)) (to_int (* hour_16 10.0)) (to_int (* hour_17 10.0)) (to_int (* hour_18 10.0)) (to_int (* hour_19 10.0)) (to_int (* hour_20 10.0)) (to_int (* hour_21 10.0)) (to_int (* hour_22 10.0)) (to_int (* hour_23 10.0))) 24))) (<= (to_real a!1) (* (/ (+ hour_0 hour_1 hour_2 hour_3 hour_4 hour_5 hour_6 hour_7 hour_8 hour_9 hour_10 hour_11 hour_12 hour_13 hour_14 hour_15 hour_16 hour_17 hour_18 hour_19 hour_20 hour_21 hour_22 hour_23) 24.0) 10.0)))))
(check-sat)
(pop 1)

; Goal 2, negated
(push 1)
(assert (not (let ((a!1 (div (+ (to_int (* hour_0 10.0)) (to_int (* hour_1 10.0)) (to_int (* hour_2 10.0)) (to_int (* hour_3 10.0)) (to_int (* hour_4 10.0)) (to_int (* hour_5 10.0)) (to_int (* hour_6 10.0)) (to_int (* hour_7 10.0)) (to_int (* hour_8 10.0)) (to_int (* hour_9 10.0)) (to_int (* hour_10 10.0)) (to_int (* hour_11 10.0)) (to_int (* hour_12 10.0)) (to_int (* hour_13 10.0)) (to_int (* hour_14 10.0)) (to_int (* hour_15 10.0)) (to_int (* hour_16 10.0)) (to_int (* hour_17 10.0)) (to_int (* hour_18 10.0)) (to_int (* hour_19 10.0)) (to_int (* hour_20 10.0)) (to_int (* hour_21 10.0)) (to_int (* hour_22 10.0)) (to_int (* hour_23 10.0))) 24))) (< (* (/ (+ hour_0 hour_1 hour_2 hour_3 hour_4 hour_5 hour_6 hour_7 hour_8 hour_9 hour_10 hour_11 hour_12 hour_13 hour_14 hour_15 hour_16 hour_17 hour_18 hour_19 hour_20 hour_21 hour_22 hour_23) 24.0) 10.0) (to_real (+ a!1 2))))))
(check-sat)
(pop 1)

; Goal 3, negated
(push 1)
(assert (not (let ((a!1 (ite (>= (to_int (* hour_0 10.0)) (to_int (* hour_1 10.0))) (to_int (* hour_0 10.0)) (to_int (* hour_1 10.0)))) (a!24 (ite (>= (ite (>= hour_0 hour_1) hour_0 hour_1) hour_2) (ite (>= hour_0 hour_1) hour_0 hour_1) hour_2))) (let ((a!2 (ite (>= a!1 (to_int (* hour_2 10.0))) a!1 (to_int (* hour_2 10.0)))) (a!25 (ite (>= (ite (>= a!24 hour_3) a!24 hour_3) hour_4) (ite (>= a!24 hour_3) a!24 hour_3) hour_4))) (let ((a!3 (ite (>= a!2 (to_int (* hour_3 10.0))) a!2 (to_int (* hour_3 10.0)))) (a!26 (ite (>= (ite (>= a!25 hour_5) a!25 hour_5) hour_6) (ite (>= a!25 hour_5) a!25 hour_5) hour_6))) (let ((a!4 (ite (>= a!3 (to_int (* hour_4 10.0))) a!3 (to_int (* hour_4 10.0)))) (a!27 (ite (>= (ite (>= a!26 hour_7) a!26 hour_7) hour_8) (ite (>= a!26 hour_7) a!26 hour_7) hour_8))) (let ((a!5 (ite (>= a!4 (to_int (* hour_5 10.0))) a!4 (to_int (* hour_5 10.0)))) (a!28 (ite (>= (ite (>= a!27 hour_9) a!27 hour_9) hour_10) (ite (>= a!27 hour_9) a!27 hour_9) hour_10))) (let ((a!6 (ite (>= a!5 (to_int (* hour_6 10.0))) a!5 (to_int (* hour_6 10.0)))) (a!29 (ite (>= (ite (>= a!28 hour_11) a!28 hour_11) hour_12) (ite (>= a!28 hour_11) a!28 hour_11) hour_12))) (let ((a!7 (ite (>= a!6 (to_int (* hour_7 10.0))) a!6 (to_int (* hour_7 10.0)))) (a!30 (ite (>= (ite (>= a!29 hour_13) a!29 hour_13) hour_14) (ite (>= a!29 hour_13) a!29 hour_13) hour_14))) (let ((a!8 (ite (>= a!7 (to_int (* hour_8 10.0))) a!7 (to_int (* hour_8 10.0)))) (a!31 (ite (>= (ite (>= a!30 hour_15) a!30 hour_15) hour_16) (ite (>= a!30 hour_15) a!30 hour_15) hour_16))) (let ((a!9 (ite (>= a!8 (to_int (* hour_9 10.0))) a!8 (to_int (* hour_9 10.0)))) (a!32 (ite (>= (ite (>= a!31 hour_17) a!31 hour_17) hour_18) (ite (>= a!31 hour_17) a!31 hour_17) hour_18))) (let ((a!10 (ite (>= a!9 (to_int (* hour_10 10.0))) a!9 (to_int (* hour_10 10.0)))) (a!33 (ite (>= (ite (>= a!32 hour_19) a!32 hour_19) hour_20) (ite (>= a!32 hour_19) a!32 hour_19) hour_20))) (let ((a!11 (ite (>= a!10 (to_int (* hour_11 10.0))) a!10 (to_int (* hour_11 10.0)))) (a!34 (ite (>= (ite (>= a!33 hour_21) a!33 hour_21) hour_22) (ite (>= a!33 hour_21) a!33 hour_21) hour_22))) (let ((a!12 (ite (>= a!11 (to_int (* hour_12 10.0))) a!11 (to_int (* hour_12 10.0))))) (let ((a!13 (ite (>= a!12 (to_int (* hour_13 10.0))) a!12 (to_int (* hour_13 10.0))))) (let ((a!14 (ite (>= a!13 (to_int (* hour_14 10.0))) a!13 (to_int (* hour_14 10.0))))) (let ((a!15 (ite (>= a!14 (to_int (* hour_15 10.0))) a!14 (to_int (* hour_15 10.0))))) (let ((a!16 (ite (>= a!15 (to_int (* hour_16 10.0))) a!15 (to_int (* hour_16 10.0))))) (let ((a!17 (ite (>= a!16 (to_int (* hour_17 10.0))) a!16 (to_int (* hour_17 10.0))))) (let ((a!18 (ite (>= a!17 (to_int (* hour_18 10.0))) a!17 (to_int (* hour_18 10.0))))) (let ((a!19 (ite (>= a!18 (to_int (* hour_19 10.0))) a!18 (to_int (* hour_19 10.0))))) (let ((a!20 (ite (>= a!19 (to_int (* hour_20 10.0))) a!19 (to_int (* hour_20 10.0))))) (let ((a!21 (ite (>= a!20 (to_int (* hour_21 10.0))) a!20 (to_int (* hour_21 10.0))))) (let ((a!22 (ite (>= a!21 (to_int (* hour_22 10.0))) a!21 (to_int (* hour_22 10.0))))) (let ((a!23 (ite (>= a!22 (to_int (* hour_23 10.0))) a!22 (to_int (* hour_23 10.0))))) (<= (to_real a!23) (* (ite (>= a!34 hour_23) a!34 hour_23) 10.0)))))))))))))))))))))))))))
(check-sat)
(pop 1)

; Goal 4, negated
(push 1)
(assert (not (let ((a!1 (ite (>= (ite (>= hour_0 hour_1) hour_0 hour_1) hour_2) (ite (>= hour_0 hour_1) hour_0 hour_1) hour_2)) (a!12 (ite (>= (to_int (* hour_0 10.0)) (to_int (* hour_1 10.0))) (to_int (* hour_0 10.0)) (to_int (* hour_1 10.0))))) (let ((a!2 (ite (>= (ite (>= a!1 hour_3) a!1 hour_3) hour_4) (ite (>= a!1 hour_3) a!1 hour_3) hour_4)) (a!13 (ite (>= a!12 (to_int (* hour_2 10.0))) a!12 (to_int (* hour_2 10.0))))) (let ((a!3 (ite (>= (ite (>= a!2 hour_5) a!2 hour_5) hour_6) (ite (>= a!2 hour_5) a!2 hour_5) hour_6)) (a!14 (ite (>= a!13 (to_int (* hour_3 10.0))) a!13 (to_int (* hour_3 10.0))))) (let ((a!4 (ite (>= (ite (>= a!3 hour_7) a!3 hour_7) hour_8) (ite (>= a!3 hour_7) a!3 hour_7) hour_8)) (a!15 (ite (>= a!14 (to_int (* hour_4 10.0))) a!14 (to_int (* hour_4 10.0))))) (let ((a!5 (ite (>= (ite (>= a!4 hour_9) a!4 hour_9) hour_10) (ite (>= a!4 hour_9) a!4 hour_9) hour_10)) (a!16 (ite (>= a!15 (to_int (* hour_5 10.0))) a!15 (to_int (* hour_5 10.0))))) (let ((a!6 (ite (>= (ite (>= a!5 hour_11) a!5 hour_11) hour_12) (ite (>= a!5 hour_11) a!5 hour_11) hour_12)) (a!17 (ite (>= a!16 (to_int (* hour_6 10.0))) a!16 (to_int (* hour_6 10.0))))) (let ((a!7 (ite (>= (ite (>= a!6 hour_13) a!6 hour_13) hour_14) (ite (>= a!6 hour_13) a!6 hour_13) hour_14)) (a!18 (ite (>= a!17 (to_int (* hour_7 10.0))) a!17 (to_int (* hour_7 10.0))))) (let ((a!8 (ite (>= (ite (>= a!7 hour_15) a!7 hour_15) hour_16) (ite (>= a!7 hour_15) a!7 hour_15) hour_16)) (a!19 (ite (>= a!18 (to_int (* hour_8 10.0))) a!18 (to_int (* hour_8 10.0))))) (let ((a!9 (ite (>= (ite (>= a!8 hour_17) a!8 hour_17) hour_18) (ite (>= a!8 hour_17) a!8 hour_17) hour_18)) (a!20 (ite (>= a!19 (to_int (* hour_9 10.0))) a!19 (to_int (* hour_9 10.0))))) (let ((a!10 (ite (>= (ite (>= a!9 hour_19) a!9 hour_19) hour_20) (ite (>= a!9 hour_19) a!9 hour_19) hour_20)) (a!21 (ite (>= a!20 (to_int (* hour_10 10.0))) a!20 (to_int (* hour_10 10.0))))) (let ((a!11 (ite (>= (ite (>= a!10 hour_21) a!10 hour_21) hour_22) (ite (>= a!10 hour_21) a!10 hour_21) hour_22)) (a!22 (ite (>= a!21 (to_int (* hour_11 10.0))) a!21 (to_int (* hour_11 10.0))))) (let ((a!23 (ite (>= a!22 (to_int (* hour_12 10.0))) a!22 (to_int (* hour_12 10.0))))) (let ((a!24 (ite (>= a!23 (to_int (* hour_13 10.0))) a!23 (to_int (* hour_13 10.0))))) (let ((a!25 (ite (>= a!24 (to_int (* hour_14 10.0))) a!24 (to_int (* hour_14 10.0))))) (let ((a!26 (ite (>= a!25 (to_int (* hour_15 10.0))) a!25 (to_int (* hour_15 10.0))))) (let ((a!27 (ite (>= a!26 (to_int (* hour_16 10.0))) a!26 (to_int (* hour_16 10.0))))) (let ((a!28 (ite (>= a!27 (to_int (* hour_17 10.0))) a!27 (to_int (* hour_17 10.0))))) (let ((a!29 (ite (>= a!28 (to_int (* hour_18 10.0))) a!28 (to_int (* hour_18 10.0))))) (let ((a!30 (ite (>= a!29 (to_int (* hour_19 10.0))) a!29 (to_int (* hour_19 10.0))))) (let ((a!31 (ite (>= a!30 (to_int (* hour_20 10.0))) a!30 (to_int (* hour_20 10.0))))) (let ((a!32 (ite (>= a!31 (to_int (* hour_21 10.0))) a!31 (to_int (* hour_21 10.0))))) (let ((a!33 (ite (>= a!32 (to_int (* hour_22 10.0))) a!32 (to_int (* hour_22 10.0))))) (let ((a!34 (ite (>= a!33 (to_int (* hour_23 10.0))) a!33 (to_int (* hour_23 10.0))))) (< (* (ite (>= a!11 hour_23) a!11 hour_23) 10.0) (to_real (+ a!34 1))))))))))))))))))))))))))))
(check-sat)
(pop 1)