; GraphAtlas proof IC-05
; Statement: The tax effect taken off the insurance risk charge lies between zero and 80 per cent of the notional effect, which is the requirement times the group effective tax rate, so at least a fifth of the requirement is left. The carry-back component is at most 85 per cent of the notional effect. The net deferred tax asset is at most 15 per cent of the requirement and is never held against a net liability. An asset can only lower what is used, and a sum of components between nothing and the cap is what is used. It holds for any notional effect up to the requirement and any three sub-groups, capacity, earnings and deferred taxes.
; About: taxEffect in src/kernel/ics.ts for the limited rule of L2-349, with the constants UTILISATION_TEXT, CARRY_BACK_TEXT, FUTURE_INCOME_TEXT and DTA_CAP_TEXT as exact decimals. The notional effect is the requirement times the rate, and the proof takes it as any number from zero up to the requirement, which that product always is for a rate from 0 to 1, because a solver divides more easily by a number than by a product. Each sub-group has the share of it that its liabilities are of the total, the capacity counted for it is the smaller of the share and its carry-back capacity, and the used amount is the sum of the components held between zero and the cap. The default rule uses the cap itself. The proof has three sub-groups, and the same shares add up to the notional effect for any number.
; Source: IAIS Insurance Capital Standard, Level 2 text of 5 December 2024, L2-347 to L2-353
; Expected: unsat for each of the 10 checks below.
; Check with any SMT-LIB 2 solver, for example: z3 this-file.smt2

(declare-fun requirement () Real)
(declare-fun tax_rate () Real)
(declare-fun liabilities_1 () Real)
(declare-fun liabilities_2 () Real)
(declare-fun liabilities_3 () Real)
(declare-fun total_liabilities () Real)
(declare-fun notional_tax_effect () Real)
(declare-fun capacity_1 () Real)
(declare-fun capacity_2 () Real)
(declare-fun capacity_3 () Real)
(declare-fun earnings () Real)
(declare-fun liability () Real)
(declare-fun asset () Real)
(declare-fun projected_loss () Bool)
(assert (>= requirement 0.0))
(assert (>= tax_rate 0.0))
(assert (<= tax_rate 1.0))
(assert (>= liabilities_1 0.0))
(assert (>= liabilities_2 0.0))
(assert (>= liabilities_3 0.0))
(assert (= total_liabilities (+ 0.0 liabilities_1 liabilities_2 liabilities_3)))
(assert (> total_liabilities 0.0))
(assert (>= notional_tax_effect 0.0))
(assert (<= notional_tax_effect requirement))
(assert (>= capacity_1 0.0))
(assert (>= capacity_2 0.0))
(assert (>= capacity_3 0.0))
(assert (>= earnings 0.0))
(assert (>= liability 0.0))
(assert (>= asset 0.0))

; Lemma 1, negated
(push 1)
(assert (not (= (+ 0.0 (/ (* notional_tax_effect liabilities_1) total_liabilities) (/ (* notional_tax_effect liabilities_2) total_liabilities) (/ (* notional_tax_effect liabilities_3) total_liabilities)) notional_tax_effect)))
(check-sat)
(pop 1)
; Lemma 1 holds, so later checks may use it
(assert (= (+ 0.0 (/ (* notional_tax_effect liabilities_1) total_liabilities) (/ (* notional_tax_effect liabilities_2) total_liabilities) (/ (* notional_tax_effect liabilities_3) total_liabilities)) notional_tax_effect))

; Lemma 2, negated
(push 1)
(assert (not (let ((a!1 (ite (<= (/ (* notional_tax_effect liabilities_1) total_liabilities) capacity_1) (/ (* notional_tax_effect liabilities_1) total_liabilities) capacity_1)) (a!2 (ite (<= (/ (* notional_tax_effect liabilities_2) total_liabilities) capacity_2) (/ (* notional_tax_effect liabilities_2) total_liabilities) capacity_2)) (a!3 (ite (<= (/ (* notional_tax_effect liabilities_3) total_liabilities) capacity_3) (/ (* notional_tax_effect liabilities_3) total_liabilities) capacity_3))) (<= (+ 0.0 a!1 a!2 a!3) (+ 0.0 (/ (* notional_tax_effect liabilities_1) total_liabilities) (/ (* notional_tax_effect liabilities_2) total_liabilities) (/ (* notional_tax_effect liabilities_3) total_liabilities))))))
(check-sat)
(pop 1)
; Lemma 2 holds, so later checks may use it
(assert (let ((a!1 (ite (<= (/ (* notional_tax_effect liabilities_1) total_liabilities) capacity_1) (/ (* notional_tax_effect liabilities_1) total_liabilities) capacity_1)) (a!2 (ite (<= (/ (* notional_tax_effect liabilities_2) total_liabilities) capacity_2) (/ (* notional_tax_effect liabilities_2) total_liabilities) capacity_2)) (a!3 (ite (<= (/ (* notional_tax_effect liabilities_3) total_liabilities) capacity_3) (/ (* notional_tax_effect liabilities_3) total_liabilities) capacity_3))) (<= (+ 0.0 a!1 a!2 a!3) (+ 0.0 (/ (* notional_tax_effect liabilities_1) total_liabilities) (/ (* notional_tax_effect liabilities_2) total_liabilities) (/ (* notional_tax_effect liabilities_3) total_liabilities)))))

; Goal 1, negated
(push 1)
(assert (not (let ((a!1 (ite (<= (/ (* notional_tax_effect liabilities_1) total_liabilities) capacity_1) (/ (* notional_tax_effect liabilities_1) total_liabilities) capacity_1)) (a!2 (ite (<= (/ (* notional_tax_effect liabilities_2) total_liabilities) capacity_2) (/ (* notional_tax_effect liabilities_2) total_liabilities) capacity_2)) (a!3 (ite (<= (/ (* notional_tax_effect liabilities_3) total_liabilities) capacity_3) (/ (* notional_tax_effect liabilities_3) total_liabilities) capacity_3)) (a!5 (ite (<= (* (/ 3.0 20.0) requirement) (- asset liability)) (* (/ 3.0 20.0) requirement) (- asset liability)))) (let ((a!4 (+ (* (/ 17.0 20.0) (+ 0.0 a!1 a!2 a!3)) (ite projected_loss 0.0 (* (/ 1.0 2.0) earnings tax_rate)) (ite (>= 0.0 (- liability asset)) 0.0 (- liability asset))))) (let ((a!6 (<= (* (/ 4.0 5.0) notional_tax_effect) (- a!4 (ite (>= 0.0 a!5) 0.0 a!5))))) (let ((a!7 (ite a!6 (* (/ 4.0 5.0) notional_tax_effect) (- a!4 (ite (>= 0.0 a!5) 0.0 a!5))))) (>= (ite (>= 0.0 a!7) 0.0 a!7) 0.0)))))))
(check-sat)
(pop 1)

; Goal 2, negated
(push 1)
(assert (not (let ((a!1 (ite (<= (/ (* notional_tax_effect liabilities_1) total_liabilities) capacity_1) (/ (* notional_tax_effect liabilities_1) total_liabilities) capacity_1)) (a!2 (ite (<= (/ (* notional_tax_effect liabilities_2) total_liabilities) capacity_2) (/ (* notional_tax_effect liabilities_2) total_liabilities) capacity_2)) (a!3 (ite (<= (/ (* notional_tax_effect liabilities_3) total_liabilities) capacity_3) (/ (* notional_tax_effect liabilities_3) total_liabilities) capacity_3)) (a!5 (ite (<= (* (/ 3.0 20.0) requirement) (- asset liability)) (* (/ 3.0 20.0) requirement) (- asset liability)))) (let ((a!4 (+ (* (/ 17.0 20.0) (+ 0.0 a!1 a!2 a!3)) (ite projected_loss 0.0 (* (/ 1.0 2.0) earnings tax_rate)) (ite (>= 0.0 (- liability asset)) 0.0 (- liability asset))))) (let ((a!6 (<= (* (/ 4.0 5.0) notional_tax_effect) (- a!4 (ite (>= 0.0 a!5) 0.0 a!5))))) (let ((a!7 (ite a!6 (* (/ 4.0 5.0) notional_tax_effect) (- a!4 (ite (>= 0.0 a!5) 0.0 a!5))))) (<= (ite (>= 0.0 a!7) 0.0 a!7) (* (/ 4.0 5.0) notional_tax_effect))))))))
(check-sat)
(pop 1)

; Goal 3, negated
(push 1)
(assert (not (let ((a!1 (ite (<= (/ (* notional_tax_effect liabilities_1) total_liabilities) capacity_1) (/ (* notional_tax_effect liabilities_1) total_liabilities) capacity_1)) (a!2 (ite (<= (/ (* notional_tax_effect liabilities_2) total_liabilities) capacity_2) (/ (* notional_tax_effect liabilities_2) total_liabilities) capacity_2)) (a!3 (ite (<= (/ (* notional_tax_effect liabilities_3) total_liabilities) capacity_3) (/ (* notional_tax_effect liabilities_3) total_liabilities) capacity_3)) (a!5 (ite (<= (* (/ 3.0 20.0) requirement) (- asset liability)) (* (/ 3.0 20.0) requirement) (- asset liability)))) (let ((a!4 (+ (* (/ 17.0 20.0) (+ 0.0 a!1 a!2 a!3)) (ite projected_loss 0.0 (* (/ 1.0 2.0) earnings tax_rate)) (ite (>= 0.0 (- liability asset)) 0.0 (- liability asset))))) (let ((a!6 (<= (* (/ 4.0 5.0) notional_tax_effect) (- a!4 (ite (>= 0.0 a!5) 0.0 a!5))))) (let ((a!7 (ite a!6 (* (/ 4.0 5.0) notional_tax_effect) (- a!4 (ite (>= 0.0 a!5) 0.0 a!5))))) (>= (- requirement (ite (>= 0.0 a!7) 0.0 a!7)) (* (/ 1.0 5.0) requirement))))))))
(check-sat)
(pop 1)

; Goal 4, negated
(push 1)
(assert (not (let ((a!1 (ite (<= (/ (* notional_tax_effect liabilities_1) total_liabilities) capacity_1) (/ (* notional_tax_effect liabilities_1) total_liabilities) capacity_1)) (a!2 (ite (<= (/ (* notional_tax_effect liabilities_2) total_liabilities) capacity_2) (/ (* notional_tax_effect liabilities_2) total_liabilities) capacity_2)) (a!3 (ite (<= (/ (* notional_tax_effect liabilities_3) total_liabilities) capacity_3) (/ (* notional_tax_effect liabilities_3) total_liabilities) capacity_3))) (<= (* (/ 17.0 20.0) (+ 0.0 a!1 a!2 a!3)) (* (/ 17.0 20.0) notional_tax_effect)))))
(check-sat)
(pop 1)

; Goal 5, negated
(push 1)
(assert (not (let ((a!1 (ite (<= (* (/ 3.0 20.0) requirement) (- asset liability)) (* (/ 3.0 20.0) requirement) (- asset liability)))) (<= (ite (>= 0.0 a!1) 0.0 a!1) (* (/ 3.0 20.0) requirement)))))
(check-sat)
(pop 1)

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

; Goal 7, negated
(push 1)
(assert (not (let ((a!1 (ite (<= (/ (* notional_tax_effect liabilities_1) total_liabilities) capacity_1) (/ (* notional_tax_effect liabilities_1) total_liabilities) capacity_1)) (a!2 (ite (<= (/ (* notional_tax_effect liabilities_2) total_liabilities) capacity_2) (/ (* notional_tax_effect liabilities_2) total_liabilities) capacity_2)) (a!3 (ite (<= (/ (* notional_tax_effect liabilities_3) total_liabilities) capacity_3) (/ (* notional_tax_effect liabilities_3) total_liabilities) capacity_3)) (a!5 (ite (<= (* (/ 3.0 20.0) requirement) (- asset liability)) (* (/ 3.0 20.0) requirement) (- asset liability)))) (let ((a!4 (+ (* (/ 17.0 20.0) (+ 0.0 a!1 a!2 a!3)) (ite projected_loss 0.0 (* (/ 1.0 2.0) earnings tax_rate)) (ite (>= 0.0 (- liability asset)) 0.0 (- liability asset))))) (let ((a!6 (<= (* (/ 4.0 5.0) notional_tax_effect) (- a!4 (ite (>= 0.0 a!5) 0.0 a!5))))) (let ((a!7 (ite a!6 (* (/ 4.0 5.0) notional_tax_effect) (- a!4 (ite (>= 0.0 a!5) 0.0 a!5))))) (<= (ite (>= 0.0 a!7) 0.0 a!7) a!4)))))))
(check-sat)
(pop 1)

; Goal 8, negated
(push 1)
(assert (not (let ((a!1 (ite (<= (/ (* notional_tax_effect liabilities_1) total_liabilities) capacity_1) (/ (* notional_tax_effect liabilities_1) total_liabilities) capacity_1)) (a!2 (ite (<= (/ (* notional_tax_effect liabilities_2) total_liabilities) capacity_2) (/ (* notional_tax_effect liabilities_2) total_liabilities) capacity_2)) (a!3 (ite (<= (/ (* notional_tax_effect liabilities_3) total_liabilities) capacity_3) (/ (* notional_tax_effect liabilities_3) total_liabilities) capacity_3)) (a!5 (ite (<= (* (/ 3.0 20.0) requirement) (- asset liability)) (* (/ 3.0 20.0) requirement) (- asset liability)))) (let ((a!4 (+ (* (/ 17.0 20.0) (+ 0.0 a!1 a!2 a!3)) (ite projected_loss 0.0 (* (/ 1.0 2.0) earnings tax_rate)) (ite (>= 0.0 (- liability asset)) 0.0 (- liability asset))))) (let ((a!6 (>= (- a!4 (ite (>= 0.0 a!5) 0.0 a!5)) 0.0)) (a!7 (<= (- a!4 (ite (>= 0.0 a!5) 0.0 a!5)) (* (/ 4.0 5.0) notional_tax_effect))) (a!8 (<= (* (/ 4.0 5.0) notional_tax_effect) (- a!4 (ite (>= 0.0 a!5) 0.0 a!5))))) (let ((a!9 (ite a!8 (* (/ 4.0 5.0) notional_tax_effect) (- a!4 (ite (>= 0.0 a!5) 0.0 a!5))))) (let ((a!10 (= (ite (>= 0.0 a!9) 0.0 a!9) (- a!4 (ite (>= 0.0 a!5) 0.0 a!5))))) (=> (and a!6 a!7) a!10))))))))
(check-sat)
(pop 1)