; GraphAtlas proof PR-01
; Statement: The MRM class is defined for every VEV, is between 1 and 7, never decreases as the VEV rises, and changes class exactly at the limits in the table.
; About: mrmClass in src/kernel/priips.ts, built from MRM_TABLE with the exact binary value of each limit.
; Source: Commission Delegated Regulation (EU) 2017/653, Annex II, Part 1, point 2
; Expected: unsat for each of the 8 checks below.
; Check with any SMT-LIB 2 solver, for example: z3 this-file.smt2

(declare-fun vev_b () Real)
(declare-fun vev_a () Real)
(assert (<= vev_a vev_b))

; Goal 1, negated
(push 1)
(assert (not (let ((a!1 (ite (< vev_a (/ 3602879701896397.0 18014398509481984.0)) 4 (ite (< vev_a (/ 5404319552844595.0 18014398509481984.0)) 5 (ite (<= vev_a (/ 3602879701896397.0 4503599627370496.0)) 6 7)))) (a!3 (ite (< vev_b (/ 3602879701896397.0 18014398509481984.0)) 4 (ite (< vev_b (/ 5404319552844595.0 18014398509481984.0)) 5 (ite (<= vev_b (/ 3602879701896397.0 4503599627370496.0)) 6 7))))) (let ((a!2 (ite (< vev_a (/ 5764607523034235.0 1152921504606846976.0)) 1 (ite (< vev_a (/ 3602879701896397.0 72057594037927936.0)) 2 (ite (< vev_a (/ 1080863910568919.0 9007199254740992.0)) 3 a!1)))) (a!4 (ite (< vev_b (/ 5764607523034235.0 1152921504606846976.0)) 1 (ite (< vev_b (/ 3602879701896397.0 72057594037927936.0)) 2 (ite (< vev_b (/ 1080863910568919.0 9007199254740992.0)) 3 a!3))))) (and (>= a!2 1) (<= a!2 7) (>= a!4 1) (<= a!4 7))))))
(check-sat)
(pop 1)

; Goal 2, negated
(push 1)
(assert (not (let ((a!1 (ite (< vev_a (/ 3602879701896397.0 18014398509481984.0)) 4 (ite (< vev_a (/ 5404319552844595.0 18014398509481984.0)) 5 (ite (<= vev_a (/ 3602879701896397.0 4503599627370496.0)) 6 7)))) (a!3 (ite (< vev_b (/ 3602879701896397.0 18014398509481984.0)) 4 (ite (< vev_b (/ 5404319552844595.0 18014398509481984.0)) 5 (ite (<= vev_b (/ 3602879701896397.0 4503599627370496.0)) 6 7))))) (let ((a!2 (ite (< vev_a (/ 5764607523034235.0 1152921504606846976.0)) 1 (ite (< vev_a (/ 3602879701896397.0 72057594037927936.0)) 2 (ite (< vev_a (/ 1080863910568919.0 9007199254740992.0)) 3 a!1)))) (a!4 (ite (< vev_b (/ 5764607523034235.0 1152921504606846976.0)) 1 (ite (< vev_b (/ 3602879701896397.0 72057594037927936.0)) 2 (ite (< vev_b (/ 1080863910568919.0 9007199254740992.0)) 3 a!3))))) (<= a!2 a!4)))))
(check-sat)
(pop 1)

; Goal 3, negated
(push 1)
(assert (not (let ((a!1 (ite (< vev_a (/ 3602879701896397.0 18014398509481984.0)) 4 (ite (< vev_a (/ 5404319552844595.0 18014398509481984.0)) 5 (ite (<= vev_a (/ 3602879701896397.0 4503599627370496.0)) 6 7))))) (let ((a!2 (ite (< vev_a (/ 5764607523034235.0 1152921504606846976.0)) 1 (ite (< vev_a (/ 3602879701896397.0 72057594037927936.0)) 2 (ite (< vev_a (/ 1080863910568919.0 9007199254740992.0)) 3 a!1))))) (and (=> (< vev_a (/ 5764607523034235.0 1152921504606846976.0)) (<= a!2 1)) (=> (>= vev_a (/ 5764607523034235.0 1152921504606846976.0)) (>= a!2 2)))))))
(check-sat)
(pop 1)

; Goal 4, negated
(push 1)
(assert (not (let ((a!1 (ite (< vev_a (/ 3602879701896397.0 18014398509481984.0)) 4 (ite (< vev_a (/ 5404319552844595.0 18014398509481984.0)) 5 (ite (<= vev_a (/ 3602879701896397.0 4503599627370496.0)) 6 7))))) (let ((a!2 (ite (< vev_a (/ 5764607523034235.0 1152921504606846976.0)) 1 (ite (< vev_a (/ 3602879701896397.0 72057594037927936.0)) 2 (ite (< vev_a (/ 1080863910568919.0 9007199254740992.0)) 3 a!1))))) (and (=> (< vev_a (/ 3602879701896397.0 72057594037927936.0)) (<= a!2 2)) (=> (>= vev_a (/ 3602879701896397.0 72057594037927936.0)) (>= a!2 3)))))))
(check-sat)
(pop 1)

; Goal 5, negated
(push 1)
(assert (not (let ((a!1 (ite (< vev_a (/ 3602879701896397.0 18014398509481984.0)) 4 (ite (< vev_a (/ 5404319552844595.0 18014398509481984.0)) 5 (ite (<= vev_a (/ 3602879701896397.0 4503599627370496.0)) 6 7))))) (let ((a!2 (ite (< vev_a (/ 5764607523034235.0 1152921504606846976.0)) 1 (ite (< vev_a (/ 3602879701896397.0 72057594037927936.0)) 2 (ite (< vev_a (/ 1080863910568919.0 9007199254740992.0)) 3 a!1))))) (and (=> (< vev_a (/ 1080863910568919.0 9007199254740992.0)) (<= a!2 3)) (=> (>= vev_a (/ 1080863910568919.0 9007199254740992.0)) (>= a!2 4)))))))
(check-sat)
(pop 1)

; Goal 6, negated
(push 1)
(assert (not (let ((a!1 (ite (< vev_a (/ 3602879701896397.0 18014398509481984.0)) 4 (ite (< vev_a (/ 5404319552844595.0 18014398509481984.0)) 5 (ite (<= vev_a (/ 3602879701896397.0 4503599627370496.0)) 6 7))))) (let ((a!2 (ite (< vev_a (/ 5764607523034235.0 1152921504606846976.0)) 1 (ite (< vev_a (/ 3602879701896397.0 72057594037927936.0)) 2 (ite (< vev_a (/ 1080863910568919.0 9007199254740992.0)) 3 a!1))))) (and (=> (< vev_a (/ 3602879701896397.0 18014398509481984.0)) (<= a!2 4)) (=> (>= vev_a (/ 3602879701896397.0 18014398509481984.0)) (>= a!2 5)))))))
(check-sat)
(pop 1)

; Goal 7, negated
(push 1)
(assert (not (let ((a!1 (ite (< vev_a (/ 3602879701896397.0 18014398509481984.0)) 4 (ite (< vev_a (/ 5404319552844595.0 18014398509481984.0)) 5 (ite (<= vev_a (/ 3602879701896397.0 4503599627370496.0)) 6 7))))) (let ((a!2 (ite (< vev_a (/ 5764607523034235.0 1152921504606846976.0)) 1 (ite (< vev_a (/ 3602879701896397.0 72057594037927936.0)) 2 (ite (< vev_a (/ 1080863910568919.0 9007199254740992.0)) 3 a!1))))) (and (=> (< vev_a (/ 5404319552844595.0 18014398509481984.0)) (<= a!2 5)) (=> (>= vev_a (/ 5404319552844595.0 18014398509481984.0)) (>= a!2 6)))))))
(check-sat)
(pop 1)

; Goal 8, negated
(push 1)
(assert (not (let ((a!1 (ite (< vev_a (/ 3602879701896397.0 18014398509481984.0)) 4 (ite (< vev_a (/ 5404319552844595.0 18014398509481984.0)) 5 (ite (<= vev_a (/ 3602879701896397.0 4503599627370496.0)) 6 7))))) (let ((a!2 (ite (< vev_a (/ 5764607523034235.0 1152921504606846976.0)) 1 (ite (< vev_a (/ 3602879701896397.0 72057594037927936.0)) 2 (ite (< vev_a (/ 1080863910568919.0 9007199254740992.0)) 3 a!1))))) (and (=> (<= vev_a (/ 3602879701896397.0 4503599627370496.0)) (<= a!2 6)) (=> (> vev_a (/ 3602879701896397.0 4503599627370496.0)) (>= a!2 7)))))))
(check-sat)
(pop 1)