; GraphAtlas proof RS-01
; Statement: For positive amounts, the development factor of a year is the mean of the ratios from that year to the next, weighted by the amounts of the first of the two. So it is not below the smallest of those ratios and not above the largest, and it is their common value when they are all alike.
; About: developmentFactors in src/kernel/reserving.ts, which divides the total of the later amounts by the total of the earlier ones, over the origin years that have both. Three origin years stand for any number of them. A ratio is a later amount over the earlier amount of the same origin year, so the later amount is the earlier amount times the ratio. Each quotient is written as the number whose product with its divisor is the dividend, which for a divisor above zero is the same number.
; Source: Mack (1993), ASTIN Bulletin 23(2), pages 213 to 225, The estimator of the development factors
; Expected: unsat for each of the 4 checks below.
; Check with any SMT-LIB 2 solver, for example: z3 this-file.smt2

(declare-fun earlier_1 () Real)
(declare-fun earlier_2 () Real)
(declare-fun earlier_3 () Real)
(declare-fun ratio_1 () Real)
(declare-fun ratio_2 () Real)
(declare-fun ratio_3 () Real)
(declare-fun factor () Real)
(assert (> earlier_1 0.0))
(assert (> earlier_2 0.0))
(assert (> earlier_3 0.0))
(assert (> ratio_1 0.0))
(assert (> ratio_2 0.0))
(assert (> ratio_3 0.0))
(assert (= (* factor (+ earlier_1 earlier_2 earlier_3)) (+ (* earlier_1 ratio_1) (* earlier_2 ratio_2) (* earlier_3 ratio_3))))

; Goal 1, negated
(push 1)
(assert (not (= (* factor (+ earlier_1 earlier_2 earlier_3)) (+ (* earlier_1 ratio_1) (* earlier_2 ratio_2) (* earlier_3 ratio_3)))))
(check-sat)
(pop 1)

; Goal 2, negated
(push 1)
(assert (not (or (>= factor ratio_1) (>= factor ratio_2) (>= factor ratio_3))))
(check-sat)
(pop 1)

; Goal 3, negated
(push 1)
(assert (not (or (<= factor ratio_1) (<= factor ratio_2) (<= factor ratio_3))))
(check-sat)
(pop 1)

; Goal 4, negated
(push 1)
(assert (not (=> (and (= ratio_1 ratio_2) (= ratio_2 ratio_3)) (= factor ratio_1))))
(check-sat)
(pop 1)