; GraphAtlas proof WL-02
; Statement: Inside the family, a vehicle that demands more energy never gets a lower interpolated CO2, provided the high vehicle emits at least as much as the low one.
; About: interpolateCo2 in src/kernel/wltp.ts, as a statement about real numbers, with the weight defined as in WL-01.
; Source: Regulation (EU) 2017/1151, Annex XXI, Sub-Annex 7, paragraph 3.2.3.2.4
; Expected: unsat for each of the 1 check below.
; Check with any SMT-LIB 2 solver, for example: z3 this-file.smt2

(declare-fun energy_high () Real)
(declare-fun energy_low () Real)
(declare-fun energy_first () Real)
(declare-fun energy_second () Real)
(declare-fun weight_first () Real)
(declare-fun weight_second () Real)
(declare-fun co2_high () Real)
(declare-fun co2_low () Real)
(assert (< energy_low energy_high))
(assert (>= energy_first energy_low))
(assert (<= energy_first energy_second))
(assert (<= energy_second energy_high))
(assert (= (* weight_first (- energy_high energy_low)) (- energy_first energy_low)))
(assert (= (* weight_second (- energy_high energy_low)) (- energy_second energy_low)))
(assert (<= co2_low co2_high))

; Goal 1, negated
(push 1)
(assert (not (<= (+ co2_low (* weight_first (- co2_high co2_low))) (+ co2_low (* weight_second (- co2_high co2_low))))))
(check-sat)
(pop 1)