; GraphAtlas proof RS-03
; Statement: The variance that the formula of Mack gives to the last development year, which rests on a single ratio, is never below zero and never above either of the two estimates before it. It is the continuation of their decline when they do not rise, the earlier of the two when they rise, and nothing when the earlier is nothing.
; About: mack in src/kernel/reserving.ts, at the line that sets the last variance from the two before it. The earlier variance a and the later variance b are any two numbers that are not below zero. The continuation of their decline is b x b / a.
; Source: Mack (1993), ASTIN Bulletin 23(2), pages 213 to 225, The estimator of the variance of the last development year
; Expected: unsat for each of the 6 checks below.
; Check with any SMT-LIB 2 solver, for example: z3 this-file.smt2

(declare-fun earlier_variance () Real)
(declare-fun later_variance () Real)
(assert (>= earlier_variance 0.0))
(assert (>= later_variance 0.0))

; Goal 1, negated
(push 1)
(assert (not (let ((a!1 (ite (= earlier_variance (to_real 0)) 0.0 (/ (* later_variance later_variance) earlier_variance)))) (let ((a!2 (ite (<= (ite (<= a!1 earlier_variance) a!1 earlier_variance) later_variance) (ite (<= a!1 earlier_variance) a!1 earlier_variance) later_variance))) (>= a!2 0.0)))))
(check-sat)
(pop 1)

; Goal 2, negated
(push 1)
(assert (not (let ((a!1 (ite (= earlier_variance (to_real 0)) 0.0 (/ (* later_variance later_variance) earlier_variance)))) (let ((a!2 (ite (<= (ite (<= a!1 earlier_variance) a!1 earlier_variance) later_variance) (ite (<= a!1 earlier_variance) a!1 earlier_variance) later_variance))) (<= a!2 earlier_variance)))))
(check-sat)
(pop 1)

; Goal 3, negated
(push 1)
(assert (not (let ((a!1 (ite (= earlier_variance (to_real 0)) 0.0 (/ (* later_variance later_variance) earlier_variance)))) (let ((a!2 (ite (<= (ite (<= a!1 earlier_variance) a!1 earlier_variance) later_variance) (ite (<= a!1 earlier_variance) a!1 earlier_variance) later_variance))) (<= a!2 later_variance)))))
(check-sat)
(pop 1)

; Goal 4, negated
(push 1)
(assert (not (let ((a!1 (ite (= earlier_variance (to_real 0)) 0.0 (/ (* later_variance later_variance) earlier_variance)))) (let ((a!2 (ite (<= (ite (<= a!1 earlier_variance) a!1 earlier_variance) later_variance) (ite (<= a!1 earlier_variance) a!1 earlier_variance) later_variance))) (=> (and (> earlier_variance 0.0) (<= later_variance earlier_variance)) (= a!2 (/ (* later_variance later_variance) earlier_variance)))))))
(check-sat)
(pop 1)

; Goal 5, negated
(push 1)
(assert (not (let ((a!1 (ite (= earlier_variance (to_real 0)) 0.0 (/ (* later_variance later_variance) earlier_variance)))) (let ((a!2 (ite (<= (ite (<= a!1 earlier_variance) a!1 earlier_variance) later_variance) (ite (<= a!1 earlier_variance) a!1 earlier_variance) later_variance))) (=> (> later_variance earlier_variance) (= a!2 earlier_variance))))))
(check-sat)
(pop 1)

; Goal 6, negated
(push 1)
(assert (not (let ((a!1 (ite (= earlier_variance (to_real 0)) 0.0 (/ (* later_variance later_variance) earlier_variance)))) (let ((a!2 (ite (<= (ite (<= a!1 earlier_variance) a!1 earlier_variance) later_variance) (ite (<= a!1 earlier_variance) a!1 earlier_variance) later_variance))) (=> (= earlier_variance (to_real 0)) (= a!2 (to_real 0)))))))
(check-sat)
(pop 1)