; GraphAtlas proof RS-02
; Statement: In a triangle of four origin years, what the chain ladder expects to be paid in the three calendar years to come adds up to the reserve, which is the ultimate less the latest amount of each origin year. The first year pays the next factor of every open origin year, and when no factor is below one, no payment is below zero.
; About: chainLadder in src/kernel/reserving.ts, for four origin years. The payment of a calendar year is, for each origin year that has not finished, the rise from one development year to the next. The latest amounts l1 to l3 of the three open origin years and the factors f0 to f2 are any positive numbers.
; Source: Mack (1993), ASTIN Bulletin 23(2), pages 213 to 225, The chain ladder projection
; Expected: unsat for each of the 3 checks below.
; Check with any SMT-LIB 2 solver, for example: z3 this-file.smt2

(declare-fun latest_1 () Real)
(declare-fun latest_2 () Real)
(declare-fun latest_3 () Real)
(declare-fun factor_0 () Real)
(declare-fun factor_1 () Real)
(declare-fun factor_2 () Real)
(assert (> latest_1 0.0))
(assert (> latest_2 0.0))
(assert (> latest_3 0.0))
(assert (> factor_0 0.0))
(assert (> factor_1 0.0))
(assert (> factor_2 0.0))

; Goal 1, negated
(push 1)
(assert (not (let ((a!1 (- (* (* (* latest_3 factor_0) factor_1) factor_2) (* (* latest_3 factor_0) factor_1))) (a!3 (- (* (* (* latest_3 factor_0) factor_1) factor_2) latest_3))) (let ((a!2 (+ (- (* latest_1 factor_2) latest_1) (- (* latest_2 factor_1) latest_2) (- (* latest_3 factor_0) latest_3) (- (* (* latest_2 factor_1) factor_2) (* latest_2 factor_1)) (- (* (* latest_3 factor_0) factor_1) (* latest_3 factor_0)) a!1)) (a!4 (+ (- (* latest_1 factor_2) latest_1) (- (* (* latest_2 factor_1) factor_2) latest_2) a!3))) (= a!2 a!4)))))
(check-sat)
(pop 1)

; Goal 2, negated
(push 1)
(assert (not (= (+ (- (* latest_1 factor_2) latest_1) (- (* latest_2 factor_1) latest_2) (- (* latest_3 factor_0) latest_3)) (+ (* latest_1 (- factor_2 1.0)) (* latest_2 (- factor_1 1.0)) (* latest_3 (- factor_0 1.0))))))
(check-sat)
(pop 1)

; Goal 3, negated
(push 1)
(assert (not (let ((a!1 (>= (+ (- (* latest_1 factor_2) latest_1) (- (* latest_2 factor_1) latest_2) (- (* latest_3 factor_0) latest_3)) 0.0)) (a!2 (+ (- (* (* latest_2 factor_1) factor_2) (* latest_2 factor_1)) (- (* (* latest_3 factor_0) factor_1) (* latest_3 factor_0)))) (a!3 (- (* (* (* latest_3 factor_0) factor_1) factor_2) (* (* latest_3 factor_0) factor_1)))) (=> (and (>= factor_0 1.0) (>= factor_1 1.0) (>= factor_2 1.0)) (and a!1 (>= a!2 0.0) (>= a!3 0.0))))))
(check-sat)
(pop 1)