; GraphAtlas proof IC-04
; Statement: Before the operational charge, a life, catastrophe or market risk has the part of the insurance risk charge that is its share inside its category, c x (R x c) / A, times the weighted charge of the category over the aggregate. Non-life and credit take their own charge times that factor. The parts add up to the aggregate. The terms c x (R x c) of each table add up to the square of the charge of their category, and the terms of Table 34 add up to the square of the aggregate. Terms that add up to the square of a number add up to it when divided by it. A factor times shares that add up to a charge adds up to the factor times it.
; About: icsRequirement in src/kernel/ics.ts, with the shares of aggregate in src/kernel/aggregate.ts and the factor that icsRequirement takes as the weighted charge of the category over the total at the top. The tables are exact decimals. The four identities are polynomial identities, and the solver proves that the two sides of each are one polynomial. The three steps are stated for free numbers, with no table in them, so that a solver has little to hold at once, and the identities show that the numbers of the engine are such numbers. The third step is that a weight over the aggregate times a charge is the charge times the weight over the aggregate, which is how the factor of a category times its charge is its share at the top. A charge of zero has parts of zero, which the tests show. The downward table of Table 16 has the same identity, and the tests cover it with the second program.
; Source: IAIS Insurance Capital Standard, Level 2 text of 5 December 2024, L2-335 and L1-141
; Expected: unsat for each of the 7 checks below.
; Check with any SMT-LIB 2 solver, for example: z3 this-file.smt2

(declare-fun expense_charge () Real)
(declare-fun lapse_charge () Real)
(declare-fun morbidity_charge () Real)
(declare-fun longevity_charge () Real)
(declare-fun mortality_charge () Real)
(declare-fun credit_and_surety_charge () Real)
(declare-fun pandemic_charge () Real)
(declare-fun terrorism_charge () Real)
(declare-fun natural_charge () Real)
(declare-fun concentration_charge () Real)
(declare-fun currency_charge () Real)
(declare-fun real_estate_charge () Real)
(declare-fun equity_charge () Real)
(declare-fun spread_charge () Real)
(declare-fun interest_rate_charge () Real)
(declare-fun credit_charge () Real)
(declare-fun market_charge () Real)
(declare-fun catastrophe_charge () Real)
(declare-fun non_life_charge () Real)
(declare-fun life_charge () Real)
(declare-fun category_charge () Real)
(declare-fun term_6 () Real)
(declare-fun term_5 () Real)
(declare-fun term_4 () Real)
(declare-fun term_3 () Real)
(declare-fun term_2 () Real)
(declare-fun term_1 () Real)
(declare-fun own_charge () Real)
(declare-fun factor () Real)
(declare-fun share_6 () Real)
(declare-fun share_5 () Real)
(declare-fun share_4 () Real)
(declare-fun share_3 () Real)
(declare-fun share_2 () Real)
(declare-fun share_1 () Real)
(declare-fun aggregate () Real)
(declare-fun weighted_charge () Real)
(declare-fun top_charge () Real)

; Goal 1, negated
(push 1)
(assert (not (let ((a!1 (* morbidity_charge (+ (+ 0.0 (* (/ 1.0 4.0) mortality_charge)) (* 0.0 longevity_charge) (* 1.0 morbidity_charge) (* 0.0 lapse_charge) (* (/ 1.0 2.0) expense_charge)))) (a!2 (* expense_charge (+ (+ 0.0 (* (/ 1.0 4.0) mortality_charge)) (* (/ 1.0 4.0) longevity_charge) (* (/ 1.0 2.0) morbidity_charge) (* (/ 1.0 2.0) lapse_charge) (* 1.0 expense_charge))))) (let ((a!3 (+ 0.0 (* mortality_charge (+ 0.0 (* 1.0 mortality_charge) (* (- (/ 1.0 4.0)) longevity_charge) (* (/ 1.0 4.0) morbidity_charge) (* 0.0 lapse_charge) (* (/ 1.0 4.0) expense_charge))) (* longevity_charge (+ 0.0 (* (- (/ 1.0 4.0)) mortality_charge) (* 1.0 longevity_charge) (* 0.0 morbidity_charge) (* (/ 1.0 4.0) lapse_charge) (* (/ 1.0 4.0) expense_charge))) a!1 (* lapse_charge (+ 0.0 (* 0.0 mortality_charge) (* (/ 1.0 4.0) longevity_charge) (* 0.0 morbidity_charge) (* 1.0 lapse_charge) (* (/ 1.0 2.0) expense_charge))) a!2))) (= a!3 a!3)))))
(check-sat)
(pop 1)

; Goal 2, negated
(push 1)
(assert (not (let ((a!1 (* terrorism_charge (+ (+ 0.0 (* 0.0 natural_charge)) (* 1.0 terrorism_charge) (* 0.0 pandemic_charge) (* 0.0 credit_and_surety_charge)))) (a!2 (+ (+ (+ 0.0 (* 0.0 natural_charge)) (* 0.0 terrorism_charge)) (* 1.0 pandemic_charge) (* 0.0 credit_and_surety_charge))) (a!3 (+ (+ (+ 0.0 (* 0.0 natural_charge)) (* 0.0 terrorism_charge)) (* 0.0 pandemic_charge) (* 1.0 credit_and_surety_charge)))) (let ((a!4 (+ 0.0 (* natural_charge (+ 0.0 (* 1.0 natural_charge) (* 0.0 terrorism_charge) (* 0.0 pandemic_charge) (* 0.0 credit_and_surety_charge))) a!1 (* pandemic_charge a!2) (* credit_and_surety_charge a!3)))) (= a!4 a!4)))))
(check-sat)
(pop 1)

; Goal 3, negated
(push 1)
(assert (not (let ((a!1 (* spread_charge (+ (+ 0.0 (* (/ 1.0 4.0) interest_rate_charge)) (* 1.0 spread_charge) (* (/ 3.0 4.0) equity_charge) (* (/ 1.0 2.0) real_estate_charge) (* (/ 1.0 4.0) currency_charge) (* 0.0 concentration_charge)))) (a!2 (* equity_charge (+ (+ 0.0 (* (/ 1.0 4.0) interest_rate_charge)) (* (/ 3.0 4.0) spread_charge) (* 1.0 equity_charge) (* (/ 1.0 2.0) real_estate_charge) (* (/ 1.0 4.0) currency_charge) (* 0.0 concentration_charge)))) (a!3 (* real_estate_charge (+ (+ 0.0 (* (/ 1.0 4.0) interest_rate_charge)) (* (/ 1.0 2.0) spread_charge) (* (/ 1.0 2.0) equity_charge) (* 1.0 real_estate_charge) (* (/ 1.0 4.0) currency_charge) (* 0.0 concentration_charge)))) (a!4 (* currency_charge (+ (+ 0.0 (* (/ 1.0 4.0) interest_rate_charge)) (* (/ 1.0 4.0) spread_charge) (* (/ 1.0 4.0) equity_charge) (* (/ 1.0 4.0) real_estate_charge) (* 1.0 currency_charge) (* 0.0 concentration_charge))))) (let ((a!5 (+ 0.0 (* interest_rate_charge (+ 0.0 (* 1.0 interest_rate_charge) (* (/ 1.0 4.0) spread_charge) (* (/ 1.0 4.0) equity_charge) (* (/ 1.0 4.0) real_estate_charge) (* (/ 1.0 4.0) currency_charge) (* 0.0 concentration_charge))) a!1 a!2 a!3 a!4 (* concentration_charge (+ 0.0 (* 0.0 interest_rate_charge) (* 0.0 spread_charge) (* 0.0 equity_charge) (* 0.0 real_estate_charge) (* 0.0 currency_charge) (* 1.0 concentration_charge)))))) (= a!5 a!5)))))
(check-sat)
(pop 1)

; Goal 4, negated
(push 1)
(assert (not (let ((a!1 (* catastrophe_charge (+ (+ 0.0 (* (/ 1.0 4.0) life_charge) (* (/ 1.0 4.0) non_life_charge)) (* 1.0 catastrophe_charge) (* (/ 1.0 4.0) market_charge) (* (/ 1.0 4.0) credit_charge)))) (a!2 (+ (+ 0.0 (* (/ 1.0 4.0) life_charge) (* (/ 1.0 4.0) non_life_charge)) (* (/ 1.0 4.0) catastrophe_charge)))) (let ((a!3 (+ 0.0 (* life_charge (+ 0.0 (* 1.0 life_charge) (* 0.0 non_life_charge) (* (/ 1.0 4.0) catastrophe_charge) (* (/ 1.0 4.0) market_charge) (* (/ 1.0 4.0) credit_charge))) (* non_life_charge (+ 0.0 (* 0.0 life_charge) (* 1.0 non_life_charge) (* (/ 1.0 4.0) catastrophe_charge) (* (/ 1.0 4.0) market_charge) (* (/ 1.0 4.0) credit_charge))) a!1 (* market_charge (+ a!2 (* 1.0 market_charge) (* (/ 1.0 4.0) credit_charge))) (* credit_charge (+ a!2 (* (/ 1.0 4.0) market_charge) (* 1.0 credit_charge)))))) (= a!3 a!3)))))
(check-sat)
(pop 1)

; Goal 5, negated
(push 1)
(assert (not (=> (and (> category_charge 0.0) (= (+ 0.0 term_1 term_2 term_3 term_4 term_5 term_6) (* category_charge category_charge))) (= (+ 0.0 (/ term_1 category_charge) (/ term_2 category_charge) (/ term_3 category_charge) (/ term_4 category_charge) (/ term_5 category_charge) (/ term_6 category_charge)) category_charge))))
(check-sat)
(pop 1)

; Goal 6, negated
(push 1)
(assert (not (=> (= (+ 0.0 share_1 share_2 share_3 share_4 share_5 share_6) own_charge) (= (+ 0.0 (* factor share_1) (* factor share_2) (* factor share_3) (* factor share_4) (* factor share_5) (* factor share_6)) (* factor own_charge)))))
(check-sat)
(pop 1)

; Goal 7, negated
(push 1)
(assert (not (=> (> aggregate 0.0) (= (* (/ weighted_charge aggregate) top_charge) (/ (* top_charge weighted_charge) aggregate)))))
(check-sat)
(pop 1)