年金給付の支給は、これを支給すべき事由が生じた日の属する月の翌月から始め、権利が消滅し た日の属する月で終るものとする。
２ 年金給付は、その支給を停止すべき事由が生じたときは、その事由が生じた日の属する月の翌 月からその事由が消滅した日の属する月までの分の支給を停止する。ただし、これらの日が同じ月 に属する場合は、支給を停止しない。
３ 年金給付は、毎年二月、四月、六月、八月、十月及び十二月の六期に、それぞれの前月までの 分を支払う。ただし、前支払期月に支払うべきであつた年金又は権利が消滅した場合若しくは年金 の支給を停止した場合におけるその期の年金は、その支払期月でない月であつても、支払うものと する。
7.8.2 論理式
# f18.py 第十八条 年金の支給期間及び支払期月，通則版
from essentials import *
受給権月=期間(支給事由発生,受給権利消滅)
支給=(lambda m:And(Not(停止(m)),受給権月(m))) 停止=期間(停止事由発生,停止事由消滅)
年金支払額=(lambda m:
If(偶数月(m),年金支給額(m-2)+年金支給額(m-1),0)) 年金支給額=(lambda m:
If(支給(m),年金額(m),0))
# 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)))
7.8.3 検証
# v18.py
from essentials import * # honnin_v18
from f18 import * #第十八条年金の支給期間及び支払期月
m1=Int(’m1’) m2=Int(’m2’) s=Solver() t=Solver() r=Solver()
t.add(停止(10500/30+1))
print(’10500/30+1’,’停止’,t.check())
# 10500/30+1 停止 unsat
# 停止せず、月10500/30には停止事由発生と消滅が共に起きるから。
r.add(停止(12500/30+1))
print(’12500/30+1’,’停止’,r.check())
# 12500/30+1 停止 sat
s.add(支給(m1)) s.add(停止(m2)) s.push()
s.add(m1==m2)
print(’支給と停止が同じ月に起きるか？’,s.check())
# unsat
s.pop()
s.add(m1==m2+1)
print(’停止の翌月に支給されることがあるか？’,s.check()) print (s.model())
# 停止の翌月に支給されることがあるか？
# sat
# [m2 = 433,
# d1!10 = 12500,
# d1!9 = 10000,
# d2!8 = [else -> 13000]]
a=Int(’a’)
r.add(年金支払額(440)==a)
print(’月440の支払額は？’,r.check()) print(’a=’,r.model()[a])
# sat
# a=140000
# honnin_v18.py
# 第十八条の検証で使用
from essentials import *
支給事由発生=(lambda d:d==10000) 受給権利消滅=(lambda d:d==14000)
停止事由発生=(lambda d:Or(d==10500,d==12500)) 停止事由消滅=(lambda d:Or(d==10520,d==13000)) 年金額=(lambda m:70000)
7.8.4 ノート
• この条文は通則として述べらており，すべての年金種別に対して共通である．論理式f18 は年金種別パラメータkが省略されており，年金給付一般に関連する検証はこれによって 行う．
• 一方，論理式f18_specificでは，年金種別を表す給付型パラメータkが導入されている．
支給事由発生(k)などの条件は，通則個別述語結合規則_第十八条において，年金種別ごと の条件に対応づけられる．パラメータkは，f15で定義された数え上げ型給付に属する値を 取る．
• 期間はdefinitionsで定義されているが，期間(f,g)は条件fを最初に満たす日d1の属 月の翌月から、条件gを最初に満たす日d2の属月までの月mの集合を表す．このような f,gの対が複数ある場合は、それらの集合を合算したものである。
期間=(lambda f,g:(lambda m:
Exists(d1,
And(f(d1),属月(d1)+1<=m, ForAll(d2,
Implies(And(g(d2),d1<=d2), m<=属月(d2)))))))
• ３の ただし 以後の随時支払い時期については省略されている．逐条解釈TACによると，
この随時支払には次の２つの場合がある．（１）前回の標準支払以降に起きた，権利の消滅 あるいは支払い停止により，次回の標準支払時に払うべき年金の支払，（２）請求認定の遅 れによる支払遅延分の支払．いずれも，年金原簿に記録されていれば論理式記述に於いても 対処可能である．
• v18は，通則版のf18単独での検証を実データに関して行ったものである．複数の年金が関 係する個別版f18_specificの検証は，第二十条併給の調整に関連してv20で行った．ま た，f18に関して抽象日付けデータを使った記号的検証を行った．（参照7.23）