; GraphAtlas proof RS-04
; Statement: The ultimate forward rate of a year is the rate of the year before, or that rate plus 15 basis points, or that rate less 15 basis points. It rises exactly when the rate before the limit is at least 15 basis points above the rate of the year before, and falls exactly when it is at least 15 basis points below. It never ends farther from the rate before the limit than it began, and a higher rate before the limit never gives a lower ultimate rate.
; About: limitUfr in src/kernel/curve.ts. A rate is a whole number of millionths, which is how the code compares two rates, so 15 basis points is 1500 of them and a step is that many.
; Source: EIOPA-BoS-26-198, technical documentation of May 2026, Annex C, paragraph C.2.2
; Expected: unsat for each of the 5 checks below.
; Check with any SMT-LIB 2 solver, for example: z3 this-file.smt2

(declare-fun ufr_before_the_limit () Int)
(declare-fun a_higher_ufr_before_the_limit () Int)
(declare-fun previous_ufr () Int)
(assert (>= a_higher_ufr_before_the_limit ufr_before_the_limit))

; Goal 1, negated
(push 1)
(assert (not (let ((a!1 (ite (>= ufr_before_the_limit (+ previous_ufr 1500)) (+ previous_ufr 1500) (ite (<= ufr_before_the_limit (- previous_ufr 1500)) (- previous_ufr 1500) previous_ufr)))) (or (= a!1 previous_ufr) (= a!1 (+ previous_ufr 1500)) (= a!1 (- previous_ufr 1500))))))
(check-sat)
(pop 1)

; Goal 2, negated
(push 1)
(assert (not (let ((a!1 (ite (>= ufr_before_the_limit (+ previous_ufr 1500)) (+ previous_ufr 1500) (ite (<= ufr_before_the_limit (- previous_ufr 1500)) (- previous_ufr 1500) previous_ufr)))) (= (> a!1 previous_ufr) (>= ufr_before_the_limit (+ previous_ufr 1500))))))
(check-sat)
(pop 1)

; Goal 3, negated
(push 1)
(assert (not (let ((a!1 (ite (>= ufr_before_the_limit (+ previous_ufr 1500)) (+ previous_ufr 1500) (ite (<= ufr_before_the_limit (- previous_ufr 1500)) (- previous_ufr 1500) previous_ufr)))) (= (< a!1 previous_ufr) (<= ufr_before_the_limit (- previous_ufr 1500))))))
(check-sat)
(pop 1)

; Goal 4, negated
(push 1)
(assert (not (let ((a!1 (ite (>= ufr_before_the_limit (+ previous_ufr 1500)) (+ previous_ufr 1500) (ite (<= ufr_before_the_limit (- previous_ufr 1500)) (- previous_ufr 1500) previous_ufr)))) (<= (ite (>= (- a!1 ufr_before_the_limit) 0) (- a!1 ufr_before_the_limit) (- (- a!1 ufr_before_the_limit))) (ite (>= (- previous_ufr ufr_before_the_limit) 0) (- previous_ufr ufr_before_the_limit) (- (- previous_ufr ufr_before_the_limit)))))))
(check-sat)
(pop 1)

; Goal 5, negated
(push 1)
(assert (not (let ((a!1 (ite (>= a_higher_ufr_before_the_limit (+ previous_ufr 1500)) (+ previous_ufr 1500) (ite (<= a_higher_ufr_before_the_limit (- previous_ufr 1500)) (- previous_ufr 1500) previous_ufr))) (a!2 (ite (>= ufr_before_the_limit (+ previous_ufr 1500)) (+ previous_ufr 1500) (ite (<= ufr_before_the_limit (- previous_ufr 1500)) (- previous_ufr 1500) previous_ufr)))) (>= a!1 a!2))))
(check-sat)
(pop 1)