print(s.model()) #[m=351]
# 月351は年金A,Bともに支給される。
# 補題AB, 停止解除みなし申請の定義に必要(in specialization_a18_AB) r=Solver()
for k in [年金A,年金B]:
r.add(ForAll(d,
Implies(And(k==年金A,支給事由発生(年金B)(d)), And(停止事由発生(k)(d),支給(k)(属月(d)))))) print(r.check()) # sat 補題ABは成立
# f18_specific.py 第十八条 年金の支給期間及び支払期月，個別版
# k:給付型パラメータ
from essentials import *
from specialization_a18 import * # 通則個別述語対応規則_第十八条
受給権月=(lambda k:期間(支給事由発生(k),受給権利消滅(k)))
支給=(lambda k:(lambda m:And(受給権月(k)(m),Not(停止(k)(m))))) 停止=(lambda k:期間(停止事由発生(k),停止事由消滅(k)))
年金支払額=(lambda k:(lambda m:
If(偶数月(m),年金支給額(k)(m-2)+年金支給額(k)(m-1),0))) 年金支給額=(lambda k:(lambda m:If(支給(k)(m),年金額(k)(m),0)))
# specialization_a18_AB
# 第十八条用通則個別述語結合規則 for 年金A,B from honnin_AB import * #年金原簿_年金A,B 年金AB,(年金A,年金B)=EnumSort(’AB’,(’A’,’B’))
# 以下，k:年金AB, d:日
支給事由発生=(lambda k:(lambda d:
If(k==年金A,A年金受給権利発生(d),B年金受給権利発生(d)))) 受給権利消滅=(lambda k:(lambda d:
If(k==年金A,A年金受給権利消滅(d),B年金受給権利消滅(d)))) 停止事由発生=(lambda k:(lambda d:
停止事由消滅=(lambda k:(lambda d:
If(k==年金A,Or(A年金停止解除申請(d),停止解除みなし申請(年金A)(d)), Or(B年金停止解除申請(d),停止解除みなし申請(年金B)(d))))) 停止解除みなし申請=(lambda k:(lambda d:
And(k==年金A,支給事由発生(年金B)(d)))) #補題AB
# honnin_AB
# 第二十条併給の調整の検証で使用
from essentials import *
A年金受給権利発生=(lambda d: d==10000) A年金受給権利消滅=(lambda d: d==14000) A年金停止解除申請=(lambda d: d==12000) B年金受給権利発生=(lambda d: d==10500) B年金受給権利消滅=(lambda d: d==12000) B年金停止解除申請=(lambda d: d==10500)
# *--- A ---*
# | *--- B ---* |
# | | | |
# A受給権発生 B受給権発生 B受給権利消滅 A受給権利消滅
#
---*---*---*---*---# d: 10000 10500 12000 14000
# | B支給事由発生
# | | |B停止事由発生後，停止解除申請
# | | V
# | | B受給 m351=10500/30+1
# | | """"""""""""""""""""
# V V
# A支給事由発生 A停止事由発生
# | |
# *- A支給-*
# m335 m350=10500/30
# =100000/30+1 |
# V
# A停止解除みなし申請
# |
# V
# A受給 m351
# """""""""""
7.9.4 ノート t
• 第二十条では，第一項において，併給不可能な年金給付の組み合わせが述べられており，第 二，第三および第四項においては，併給の状況が生じた場合に受給権者が年金を選択するメ カニズムが述べられている．ここでは，それに従って選択を行った場合にどのようなことが 起こる得るかを検証した．具体的には，第三項が誤りであることが分かる．
• 第一項では併給不可能性が生じるメカニズムは以下のようであると述べられている．既に年 金Aの受給権が成立し年金給付の支給を受けている者（Aの受給権者）が新たにAと併給不 可能なBの受給権も取得すると，Aの支給は停止する．この時，第一項における記述がA,B について対称的であることから，Aの受給権が既に成立していることにより，(今成立したば かりの）Bの受給権による給付も停止され(行われず），結局，A,Bともに支給されない．
• 受給権者は，第二項で規定されている支給停止解除申請を利用して，停止中のA,Bのうちか ら受給したい年金給付を選択する事ができる．
• ここで問題となるのが第三項の存在である．Bの受給権の成立した日の属する月に年金Aが 支払われることは，前月に既に決まっているので（第十八条），第三項により，Aに対する解 除申請が自動的になされ，従って，次月にはAが支給されることになる．よって，もし，当 月にBに対する停止解除申請を出すと，次月にはBも支給されてしまうことになる．(年金 原簿honnin_ABおよび付属の図を参照)．
• 第三項がなければ問題は起こらない．なお，現実の運用としては，Bの受給権が成立したと きに，AかBかの選択をするための選択申出書を提出するようになっており，問題が起こら ないようにしている．
• honnin_ABとspecialization_a18_ABは，第I編で与えたものとは表現は異なるが，内 容は同一である．