7.3 第八条 資格取得の時期
7.3.3 検証
# v8.py
# 年金原簿honnin_v7をテストデータとする検証 from essentials import * # honnin_v7 from f8 import *
d=Int(’d’) s=Solver()
p=ForAll(d,Implies(成立に至る(被保険者)(d),被保険者資格取得(d))) s.add(p)
print(s.check()) # sat t=Solver()
q=ForAll(d,Implies(被保険者資格取得(d),成立に至る(被保険者)(d))) t.add(q)
print(t.check()) # unsat
# 実際，成立に至る(被保険者)(d)は，d=201に対してのみTrueとなるが，
# 被保険者資格取得(d)は，d=201,301に対してTrueとなる．
u=Solver()
u.add(成立に至る(被保険者)(d)) print(u.check()) # sat
print(u.model()) # d=201 u.add(d!=201)
print(u.check()) # unsat v=Solver()
v.add(被保険者資格取得(d)) print(v.check()) # sat print(v.model()) # d=301 v.add(d!=301)
print(v.check()) # sat print(v.model()) # d=201
7.3.4 ノート
• この条文は，（前日まで成立していなかった）被保険者の資格がある日dに成立に至るため の条件についてのべたものである．すなわち，論理式で書けば，
And(Not(被保険者(d-1)),被保険者(d))
あるいは，マクロ表現
成立に至る=lambda f:lambda d:And(Not(f(d-1),f(d))) を使うと（7.21参照），
成立に至る(被保険者)(d)
である．したがって，この条文は新しい内容を付加するものではなく，第七条から機械的に 判断できることを明文化したものと考えられる．
• f8は，条文の構造に従って条文の内容を論理式に変換したものである．条文の意図から，任 意の日dに関して，
被保険者資格取得(d) ⇔成立に至る(被保険者)(d) が期待されるが，検証の結果，これは成立しない．すなわち，
被保険者資格取得(d) ⇐成立に至る(被保険者)(d) は成立するが，逆の
被保険者資格取得(d) ⇒成立に至る(被保険者)(d)
は成立しない．この意味で第七条の条文は正しくないと考えられる．
• 以下は，条文を論理式表現に変換するうえでのコメントである．
1. 条文中の第一号から第五号の全てにおいて，「達したとき」，「至ったとき」などの表現 がされており，かつ，本文中でこれらを引用するときにも，「該当するに至った日に」と している．「至る」という隣り合う２つの時点を参照する概念が，字義通りに二重に使 われることは考えにくいので，本文中での引用は，単に「該当する日に」と解釈した．
2. f8の論理式表現はマクロAND，OR，NOT，成立に至るの使用によりコンパクトになり，
また，条文の言語表現に近いものになっている．これらのマクロはdefinitionsで定 義されているが，以下のような内容である．
– AND，OR，NOTはBool上の論理演算子And，Or，NotをInt->Bool上に拡張した ものであり，例えば，
AND(f,g)(d)==And(f(d),g(d)) OR(f,g)(d)==Or(f(d),g(d)) NOT(f)(d)==Not(f(d)) である．
– 成立に至る(f)(d)は，日d-1では成立していなかったfが日dで成立すること を表す．
• 成立に至るオペレータについては，以下が成立する．
成立に至る(OR(f,g))=OR(AND(成立に至る(f),前日に不成立(g)), AND(成立に至る(g),前日に不成立(f)))
成立に至る(AND(f,g))=OR(AND(成立に至る(f),g),AND(成立に至る(g),f)) ただし，前日に不成立=lambda f:lambda d:Not(f(d-1))
これを繰り返し用いて，成立に至る(被保険者)を展開することにより，プリミティブな述
しながら，結果は煩雑なものになる．
• f8_1は，前日において被保険者が成立しないことをNot(被保険者(d-1))として陽に与え た場合の論理式である．見かけはより簡単であるが，これに意味があるかどうかは分から ない．
• f8_1が正しいことに関しては，v8_1においてテストデータhonnin_v7のもとで．任意の 日dに関して，被保険者資格取得(d)==成立に至る(被保険者)(d)が示されている．また，
f8_1に対応する条文は，例えば，次のようになる．
被保険者でなかった者が被保険者の資格を獲得するのは，以下の各号のいずれかが成立す る日である．
一 厚生年金保険の被保険者となったとき．
二 二十歳以上六十歳未満，第二号被保険者の配偶者，および，主に第二号被保険者の収入 により生計維持，のいずれもが成立したとき．
三 二十歳以上六十歳未満，日本国内に住所を有する，および，厚生年金保険法老齢等受給 可能でない，のいずれもが成立したとき．
# f8_1.py 第八条 資格取得の時期（ひとつの改訂版）
from essentials import *
from f7 import * # 第七条被保険者の資格
被保険者資格取得=(lambda d:
And(Not(被保険者(d-1)),
Or(厚生年金保険の被保険者(d), And(二十歳以上六十歳未満(d),
第二号被保険者の配偶者(d),
主に第二号被保険者の収入により生計維持(d)), And(二十歳以上六十歳未満(d),
日本国内に住所を有する(d),
Not(厚生年金保険法老齢等受給可能(d))))))
# v8_1.py
# 年金原簿honnin_v7に関してf8_1が正しいことの検証 from essentials import * # honnin_v7
from f8_1 import * d=Int(’d’)
p=ForAll(d,被保険者資格取得(d)==成立に至る(被保険者)(d)) t=Solver()
t.add(p)
print(t.check()) # sat