7.2 第七条 被保険者の資格
And(二十歳以上六十歳未満(d), 被扶養配偶者(d)))
被扶養配偶者=(lambda d:
And(第二号被保険者の配偶者(d),
主に第二号被保険者の収入により生計維持(d), Not(第二号被保険者(d))))
7.2.3 検証
# v7.py
# 第七条の検証
# 年金原簿honnin_v7のもとでは，同じ日に異なる種別の被保険者にはなれないことの検証
# d：日を表す変数，Int：整数型の変数を作り出すZ3の関数である．
import time
from essentials import * # honnin_v7 from f7_primitive import *
start=time.time() d=Int(’d’)
s=Solver()
p=Or(And(第一号被保険者(d),第二号被保険者(d)), And(第一号被保険者(d),第三号被保険者(d)), And(第二号被保険者(d),第三号被保険者(d))) s.add(p)
print(s.check())
# unsat
# 第一号被保険者になる日の確認
print(充足リスト(成立に至る(第一号被保険者),10))
# [550, 201]
# なお，honnin_v7においては，第一号，第二号，第三号被保険者である日が，それぞれ
# 以下のようであるが，これは次のようにして確認できる．
# 第一号被保険者：日201〜日300 および 日550〜日599
# 第二号被保険者：日301〜日499
# 第三号被保険者：日500〜日549
t=Solver()
p1=ForAll(d,第一号被保険者(d)==Or(And(201<=d,d<=300),And(550<=d,d<=599))) p2=ForAll(d,第二号被保険者(d)==And(301<=d,d<=499))
p3=ForAll(d,第三号被保険者(d)==And(500<=d,d<=549)) t.add(p1,p2,p3)
print(t.check())
# sat
print(time.time()-start,’sec’)
# 0.07591009140014648 sec
# honnin_v7.py
# 第七条，第八条，第九条，第十一条の検証で使用
from essentials import *
年齢=(lambda d:26+d/360)
二十歳以上六十歳未満=(lambda d:And(20<=年齢(d),年齢(d)<60)) 日本国内に住所を有する=(lambda d:And(200<d,d<600))
厚生年金保険法老齢等受給可能=(lambda d:False) 厚生年金保険の被保険者=(lambda d:And(300<d,d<500)) 第二号被保険者の配偶者=(lambda d:And(400<d,d<550))
主に第二号被保険者の収入により生計維持=(lambda d:And(400<d,d<550))
# *----日本在住---*
# | |
# | *----企業に勤務---* |
# | | | |
# | | *----結婚---* |
# | | | | | |
#
---*---*---*---*---*---*---# d=201 301 401 499 549 599
# | || || || |
# *--第一号----**---第二号---**-第三号--**-第一号--*
# なお，以下はhonnin_v7を第十一条期間の検証で用いた場合の，各被保険者期間を示す．
# m= 6 9 10 15 16 17 18 19
# 第一号被保険者期間 [6, 7, 8, 9, 18, 19]
# 第二号被保険者期間 [10, 11, 12, 13, 14, 15]
# 第三号被保険者期間 [16, 17]
# v7_func
# 第七条の検証
# 同時に異なる種別の被保険者にはなれないことを，v7の場合のように具体的な
# 年金原簿に対してではなく，より一般的に検証する．
# "日本国内に住所を有する などを述語変数として扱い，これににいかなる述語を代入
# しても充足出来ないことを示す．
from essentials import * # honnin_v7_func from f7 import *
d=Int(’d’) s=Solver()
p=Or(And(第一号被保険者(d),第二号被保険者(d)), And(第一号被保険者(d),第三号被保険者(d)), And(第二号被保険者(d),第三号被保険者(d))) s.add(p)
print(s.check())
# unsat
# honnin_v7_func.py
# v7_funcで使用
from essentials import *
二十歳以上六十歳未満=lambda d:True
日本国内に住所を有する=Function(’f’,IntSort(),BoolSort()) 厚生年金保険法老齢等受給可能=lambda d:False
厚生年金保険の被保険者=Function(’g’,IntSort(),BoolSort()) 第二号被保険者の配偶者=Function(’h’,IntSort(),BoolSort())
主に第二号被保険者の収入により生計維持=Function(’h’,IntSort(),BoolSort())
7.2.4 ノート
• 条文の内容を忠実に論理式に直したものである．なお，条文中の２および３については，こ れらを考慮して「主として第二号被保険者の収入により生計を維持すること」の認定が適切 の行われ，年金原簿に反映されていると仮定した．
• 検証は3種類の年金原簿データに関して行った．
1. honnin_v7
具体的な日データとしの年金原簿．日本国内に住所を有するなどは，具体的な述語とし てあたえられている．
2. honnin_v7_func
関数変数を許す充足性判定を利用した検証のための年金原簿．日本国内に住所を有する などが関数IntSort→BoolSortを表す変数として定義されており，honnin_v7_func ではこれらの変数への述語の割り当てに関する充足性判定により，honnin_v7より一 般的な検証が行われている．簡単のために，二十歳以上六十歳未満は常にTrueとした．
3. honnin_v7_abs
抽象日付けデータ型を利用した検証のための年金原簿．具体的な内容に関しては，7.23 において述べる．