; GraphAtlas proof AE-02
; Statement: In every stability class both spreads of the plume grow with the distance downwind, from 100 m to 10 km. At every distance the spread of a more stable class is smaller than that of the class before it, both across the wind and upward.
; About: sigmaY and sigmaZ in src/kernel/aermod.ts, built from the rows of SPREAD_Y and SPREAD_Z as they are shipped. The spread across the wind is a x over the square root of 1 + b x. The spread upward is a x, or a x over the square root of 1 + b x, or a x over 1 + b x, by class. Each is written as the equation that a positive spread satisfies, so that the proof needs no square root, and the coefficients are the decimals of Table 4.5 of the Handbook. The distance is a real number from 100 to 10,000 metres, the range in which the functions accept one.
; Source: Handbook on Atmospheric Diffusion (Hanna, Briggs and Hosker, 1982), Table 4.5, formulas recommended by Briggs for open country
; Expected: unsat for each of the 22 checks below.
; Check with any SMT-LIB 2 solver, for example: z3 this-file.smt2

(declare-fun distance () Real)
(declare-fun farther_distance () Real)
(declare-fun across_A_far () Real)
(declare-fun across_A_near () Real)
(declare-fun up_A_far () Real)
(declare-fun up_A_near () Real)
(declare-fun across_B_far () Real)
(declare-fun across_B_near () Real)
(declare-fun up_B_far () Real)
(declare-fun up_B_near () Real)
(declare-fun across_C_far () Real)
(declare-fun across_C_near () Real)
(declare-fun up_C_far () Real)
(declare-fun up_C_near () Real)
(declare-fun across_D_far () Real)
(declare-fun across_D_near () Real)
(declare-fun up_D_far () Real)
(declare-fun up_D_near () Real)
(declare-fun across_E_far () Real)
(declare-fun across_E_near () Real)
(declare-fun up_E_far () Real)
(declare-fun up_E_near () Real)
(declare-fun across_F_far () Real)
(declare-fun across_F_near () Real)
(declare-fun up_F_far () Real)
(declare-fun up_F_near () Real)
(declare-fun across_B () Real)
(declare-fun across_A () Real)
(declare-fun up_B () Real)
(declare-fun up_A () Real)
(declare-fun across_C () Real)
(declare-fun up_C () Real)
(declare-fun across_D () Real)
(declare-fun up_D () Real)
(declare-fun across_E () Real)
(declare-fun up_E () Real)
(declare-fun across_F () Real)
(declare-fun up_F () Real)
(assert (>= distance 100.0))
(assert (< distance farther_distance))
(assert (<= farther_distance 10000.0))

; Goal 1, negated
(push 1)
(assert (not (let ((a!1 (= (* across_A_near across_A_near (+ (* (/ 1.0 10000.0) distance) 1.0)) (* (* (/ 11.0 50.0) (/ 11.0 50.0)) distance distance))) (a!2 (= (* across_A_far across_A_far (+ (* (/ 1.0 10000.0) farther_distance) 1.0)) (* (* (/ 11.0 50.0) (/ 11.0 50.0)) farther_distance farther_distance)))) (=> (and (> across_A_near 0.0) a!1 (> across_A_far 0.0) a!2) (< across_A_near across_A_far)))))
(check-sat)
(pop 1)

; Goal 2, negated
(push 1)
(assert (not (=> (and (> up_A_near 0.0) (= up_A_near (* (/ 1.0 5.0) distance)) (> up_A_far 0.0) (= up_A_far (* (/ 1.0 5.0) farther_distance))) (< up_A_near up_A_far))))
(check-sat)
(pop 1)

; Goal 3, negated
(push 1)
(assert (not (let ((a!1 (= (* across_B_near across_B_near (+ (* (/ 1.0 10000.0) distance) 1.0)) (* (* (/ 4.0 25.0) (/ 4.0 25.0)) distance distance))) (a!2 (= (* across_B_far across_B_far (+ (* (/ 1.0 10000.0) farther_distance) 1.0)) (* (* (/ 4.0 25.0) (/ 4.0 25.0)) farther_distance farther_distance)))) (=> (and (> across_B_near 0.0) a!1 (> across_B_far 0.0) a!2) (< across_B_near across_B_far)))))
(check-sat)
(pop 1)

; Goal 4, negated
(push 1)
(assert (not (=> (and (> up_B_near 0.0) (= up_B_near (* (/ 3.0 25.0) distance)) (> up_B_far 0.0) (= up_B_far (* (/ 3.0 25.0) farther_distance))) (< up_B_near up_B_far))))
(check-sat)
(pop 1)

; Goal 5, negated
(push 1)
(assert (not (let ((a!1 (= (* across_C_near across_C_near (+ (* (/ 1.0 10000.0) distance) 1.0)) (* (* (/ 11.0 100.0) (/ 11.0 100.0)) distance distance))) (a!2 (= (* across_C_far across_C_far (+ (* (/ 1.0 10000.0) farther_distance) 1.0)) (* (* (/ 11.0 100.0) (/ 11.0 100.0)) farther_distance farther_distance)))) (=> (and (> across_C_near 0.0) a!1 (> across_C_far 0.0) a!2) (< across_C_near across_C_far)))))
(check-sat)
(pop 1)

; Goal 6, negated
(push 1)
(assert (not (let ((a!1 (= (* up_C_near up_C_near (+ (* (/ 1.0 5000.0) distance) 1.0)) (* (* (/ 2.0 25.0) (/ 2.0 25.0)) distance distance))) (a!2 (= (* up_C_far up_C_far (+ (* (/ 1.0 5000.0) farther_distance) 1.0)) (* (* (/ 2.0 25.0) (/ 2.0 25.0)) farther_distance farther_distance)))) (=> (and (> up_C_near 0.0) a!1 (> up_C_far 0.0) a!2) (< up_C_near up_C_far)))))
(check-sat)
(pop 1)

; Goal 7, negated
(push 1)
(assert (not (let ((a!1 (= (* across_D_near across_D_near (+ (* (/ 1.0 10000.0) distance) 1.0)) (* (* (/ 2.0 25.0) (/ 2.0 25.0)) distance distance))) (a!2 (= (* across_D_far across_D_far (+ (* (/ 1.0 10000.0) farther_distance) 1.0)) (* (* (/ 2.0 25.0) (/ 2.0 25.0)) farther_distance farther_distance)))) (=> (and (> across_D_near 0.0) a!1 (> across_D_far 0.0) a!2) (< across_D_near across_D_far)))))
(check-sat)
(pop 1)

; Goal 8, negated
(push 1)
(assert (not (let ((a!1 (= (* up_D_near up_D_near (+ (* (/ 3.0 2000.0) distance) 1.0)) (* (* (/ 3.0 50.0) (/ 3.0 50.0)) distance distance))) (a!2 (= (* up_D_far up_D_far (+ (* (/ 3.0 2000.0) farther_distance) 1.0)) (* (* (/ 3.0 50.0) (/ 3.0 50.0)) farther_distance farther_distance)))) (=> (and (> up_D_near 0.0) a!1 (> up_D_far 0.0) a!2) (< up_D_near up_D_far)))))
(check-sat)
(pop 1)

; Goal 9, negated
(push 1)
(assert (not (let ((a!1 (= (* across_E_near across_E_near (+ (* (/ 1.0 10000.0) distance) 1.0)) (* (* (/ 3.0 50.0) (/ 3.0 50.0)) distance distance))) (a!2 (= (* across_E_far across_E_far (+ (* (/ 1.0 10000.0) farther_distance) 1.0)) (* (* (/ 3.0 50.0) (/ 3.0 50.0)) farther_distance farther_distance)))) (=> (and (> across_E_near 0.0) a!1 (> across_E_far 0.0) a!2) (< across_E_near across_E_far)))))
(check-sat)
(pop 1)

; Goal 10, negated
(push 1)
(assert (not (let ((a!1 (= (* up_E_near (+ (* (/ 3.0 10000.0) distance) 1.0)) (* (/ 3.0 100.0) distance))) (a!2 (= (* up_E_far (+ (* (/ 3.0 10000.0) farther_distance) 1.0)) (* (/ 3.0 100.0) farther_distance)))) (=> (and (> up_E_near 0.0) a!1 (> up_E_far 0.0) a!2) (< up_E_near up_E_far)))))
(check-sat)
(pop 1)

; Goal 11, negated
(push 1)
(assert (not (let ((a!1 (= (* across_F_near across_F_near (+ (* (/ 1.0 10000.0) distance) 1.0)) (* (* (/ 1.0 25.0) (/ 1.0 25.0)) distance distance))) (a!2 (= (* across_F_far across_F_far (+ (* (/ 1.0 10000.0) farther_distance) 1.0)) (* (* (/ 1.0 25.0) (/ 1.0 25.0)) farther_distance farther_distance)))) (=> (and (> across_F_near 0.0) a!1 (> across_F_far 0.0) a!2) (< across_F_near across_F_far)))))
(check-sat)
(pop 1)

; Goal 12, negated
(push 1)
(assert (not (let ((a!1 (= (* up_F_near (+ (* (/ 3.0 10000.0) distance) 1.0)) (* (/ 2.0 125.0) distance))) (a!2 (= (* up_F_far (+ (* (/ 3.0 10000.0) farther_distance) 1.0)) (* (/ 2.0 125.0) farther_distance)))) (=> (and (> up_F_near 0.0) a!1 (> up_F_far 0.0) a!2) (< up_F_near up_F_far)))))
(check-sat)
(pop 1)

; Goal 13, negated
(push 1)
(assert (not (let ((a!1 (= (* across_A across_A (+ (* (/ 1.0 10000.0) distance) 1.0)) (* (/ 11.0 50.0) (/ 11.0 50.0) distance distance))) (a!2 (= (* across_B across_B (+ (* (/ 1.0 10000.0) distance) 1.0)) (* (/ 4.0 25.0) (/ 4.0 25.0) distance distance)))) (=> (and (> across_A 0.0) a!1 (> across_B 0.0) a!2) (> across_A across_B)))))
(check-sat)
(pop 1)

; Goal 14, negated
(push 1)
(assert (not (=> (and (> up_A 0.0) (= up_A (* (/ 1.0 5.0) distance)) (> up_B 0.0) (= up_B (* (/ 3.0 25.0) distance))) (> up_A up_B))))
(check-sat)
(pop 1)

; Goal 15, negated
(push 1)
(assert (not (let ((a!1 (= (* across_B across_B (+ (* (/ 1.0 10000.0) distance) 1.0)) (* (/ 4.0 25.0) (/ 4.0 25.0) distance distance))) (a!2 (= (* across_C across_C (+ (* (/ 1.0 10000.0) distance) 1.0)) (* (/ 11.0 100.0) (/ 11.0 100.0) distance distance)))) (=> (and (> across_B 0.0) a!1 (> across_C 0.0) a!2) (> across_B across_C)))))
(check-sat)
(pop 1)

; Goal 16, negated
(push 1)
(assert (not (let ((a!1 (= (* up_C up_C (+ (* (/ 1.0 5000.0) distance) 1.0)) (* (/ 2.0 25.0) (/ 2.0 25.0) distance distance)))) (=> (and (> up_B 0.0) (= up_B (* (/ 3.0 25.0) distance)) (> up_C 0.0) a!1) (> up_B up_C)))))
(check-sat)
(pop 1)

; Goal 17, negated
(push 1)
(assert (not (let ((a!1 (= (* across_C across_C (+ (* (/ 1.0 10000.0) distance) 1.0)) (* (/ 11.0 100.0) (/ 11.0 100.0) distance distance))) (a!2 (= (* across_D across_D (+ (* (/ 1.0 10000.0) distance) 1.0)) (* (/ 2.0 25.0) (/ 2.0 25.0) distance distance)))) (=> (and (> across_C 0.0) a!1 (> across_D 0.0) a!2) (> across_C across_D)))))
(check-sat)
(pop 1)

; Goal 18, negated
(push 1)
(assert (not (let ((a!1 (= (* up_C up_C (+ (* (/ 1.0 5000.0) distance) 1.0)) (* (/ 2.0 25.0) (/ 2.0 25.0) distance distance))) (a!2 (= (* up_D up_D (+ (* (/ 3.0 2000.0) distance) 1.0)) (* (/ 3.0 50.0) (/ 3.0 50.0) distance distance)))) (=> (and (> up_C 0.0) a!1 (> up_D 0.0) a!2) (> up_C up_D)))))
(check-sat)
(pop 1)

; Goal 19, negated
(push 1)
(assert (not (let ((a!1 (= (* across_D across_D (+ (* (/ 1.0 10000.0) distance) 1.0)) (* (/ 2.0 25.0) (/ 2.0 25.0) distance distance))) (a!2 (= (* across_E across_E (+ (* (/ 1.0 10000.0) distance) 1.0)) (* (/ 3.0 50.0) (/ 3.0 50.0) distance distance)))) (=> (and (> across_D 0.0) a!1 (> across_E 0.0) a!2) (> across_D across_E)))))
(check-sat)
(pop 1)

; Goal 20, negated
(push 1)
(assert (not (let ((a!1 (= (* up_D up_D (+ (* (/ 3.0 2000.0) distance) 1.0)) (* (/ 3.0 50.0) (/ 3.0 50.0) distance distance))) (a!2 (= (* up_E (+ (* (/ 3.0 10000.0) distance) 1.0)) (* (/ 3.0 100.0) distance)))) (=> (and (> up_D 0.0) a!1 (> up_E 0.0) a!2) (> up_D up_E)))))
(check-sat)
(pop 1)

; Goal 21, negated
(push 1)
(assert (not (let ((a!1 (= (* across_E across_E (+ (* (/ 1.0 10000.0) distance) 1.0)) (* (/ 3.0 50.0) (/ 3.0 50.0) distance distance))) (a!2 (= (* across_F across_F (+ (* (/ 1.0 10000.0) distance) 1.0)) (* (/ 1.0 25.0) (/ 1.0 25.0) distance distance)))) (=> (and (> across_E 0.0) a!1 (> across_F 0.0) a!2) (> across_E across_F)))))
(check-sat)
(pop 1)

; Goal 22, negated
(push 1)
(assert (not (let ((a!1 (= (* up_E (+ (* (/ 3.0 10000.0) distance) 1.0)) (* (/ 3.0 100.0) distance))) (a!2 (= (* up_F (+ (* (/ 3.0 10000.0) distance) 1.0)) (* (/ 2.0 125.0) distance)))) (=> (and (> up_E 0.0) a!1 (> up_F 0.0) a!2) (> up_E up_F)))))
(check-sat)
(pop 1)