この法律において、「保険料納付済期間」とは、第七条第一項第一号に規定する被保険者として の被保険者期間のうち納付された保険料（第九十六条の規定により徴収された保険料を含み、第九 十条の二第一項から第三項までの規定によりその一部の額につき納付することを要しないものとさ れた保険料につきその残余の額が納付又は徴収されたものを除く。以下同じ。）に係るもの、第七 条第一項第二号に規定する被保険者としての被保険者期間及び同項第三号に規定する被保険者とし ての被保険者期間を合算した期間をいう。
２ この法律において、「保険料免除期間」とは、保険料全額免除期間、保険料四分の三免除期間、
保険料半額免除期間及び保険料四分の一免除期間を合算した期間をいう。
３ この法律において、「保険料全額免除期間」とは、第七条第一項第一号に規定する被保険者と しての被保険者期間であつて第八十九条第一項、第九十条第一項又は第九十条の三第一項の規定に より納付することを要しないものとされた保険料に係るもののうち、第九十四条第四項の規定によ り納付されたものとみなされる保険料に係る被保険者期間を除いたものを合算した期間をいう。
４ この法律において、「保険料四分の三免除期間」とは、第七条第一項第一号に規定する被保険 者としての被保険者期間であつて第九十条の二第一項の規定によりその四分の三の額につき納付す ることを要しないものとされた保険料（納付することを要しないものとされた四分の三の額以外の 四分の一の額につき納付されたものに限る。）に係るもののうち、第九十四条第四項の規定により 納付されたものとみなされる保険料に係る被保険者期間を除いたものを合算した期間をいう。
５ この法律において、「保険料半額免除期間」とは、第七条第一項第一号に規定する被保険者と しての被保険者期間であつて第九十条の二第二項の規定によりその半額につき納付することを要し ないものとされた保険料（納付することを要しないものとされた半額以外の半額につき納付された ものに限る。）に係るもののうち、第九十四条第四項の規定により納付されたものとみなされる保 険料に係る被保険者期間を除いたものを合算した期間をいう。
６ この法律において、「保険料四分の一免除期間」とは、第七条第一項第一号に規定する被保険 者としての被保険者期間であつて第九十条の二第三項の規定によりその四分の一の額につき納付す ることを要しないものとされた保険料（納付することを要しないものとされた四分の一の額以外の 四分の三の額につき納付されたものに限る。）に係るもののうち、第九十四条第四項の規定により 納付されたものとみなされる保険料に係る被保険者期間を除いたものを合算した期間をいう。
（７，８，９ 省略）
7.1.2 論理式
# f5.py 第五条 用語の定義
from essentials import *
from f11 import 第一号被保険者期間,第二号被保険者期間,第三号被保険者期間 from f89 import 保険料法定免除要件
from f90 import 保険料全額免除要件
from f90_2 import 保険料四分の三免除要件,保険料半額免除要件,保険料四分の一免除要件 from f90_3 import 保険料免除_学生要件
# from essentials 追納により納付とみなされる期間,保険料納付済み,
# 残りの四分の一納付,残りの半額納付,残りの四分の三納付
# m:月に関する変数
保険料納付済期間=(lambda m:
Or(And(第一号被保険者期間(m),保険料納付済み(m)), 第二号被保険者期間(m),
第三号被保険者期間(m))) 保険料免除期間=(lambda m:
Or(保険料全額免除期間(m), 保険料四分の三免除期間(m), 保険料半額免除期間(m), 保険料四分の一免除期間(m))) 保険料全額免除期間=(lambda m:
And(第一号被保険者期間(m), Or(保険料法定免除要件(m),
保険料全額免除要件(m), 保険料免除_学生要件(m)),
Not(追納により納付とみなされる期間(m)))) 保険料全額免除期間_学生を除く=(lambda m:
And(第一号被保険者期間(m), Or(保険料法定免除要件(m),
保険料全額免除要件(m)),
Not(追納により納付とみなされる期間(m)))) 保険料四分の三免除期間=(lambda m:
And(第一号被保険者期間(m), 保険料四分の三免除要件(m),
Not(追納により納付とみなされる期間(m)))) 保険料半額免除期間=(lambda m:
And(第一号被保険者期間(m), 残りの半額納付(m), 保険料半額免除要件(m),
Not(追納により納付とみなされる期間(m)))) 保険料四分の一免除期間=(lambda m:
And(第一号被保険者期間(m), 保険料四分の一免除要件(m), 残りの四分の三納付(m),
Not(追納により納付とみなされる期間(m))))
7.1.3 検証
# v5.py
# 年金原簿honnin_v5のもとでの第五条の検証
from essentials import * # honnin_v5, haiguusha_v5, setainushi_v5 from f5 import *
import time
start=time.time() m=500
L=充足リスト(保険料納付済期間,m) print(’保険料納付済期間’,L) L=充足リスト(保険料免除期間,m) print(’保険料免除期間’,L)
L=充足リスト(保険料全額免除期間,m) print(’保険料全額免除期間’,L)
L=充足リスト(保険料四分の三免除期間,m) print(’保険料四分の三免除期間’,L) L=充足リスト(保険料半額免除期間,m) print(’保険料半額免除期間’,L)
L=充足リスト(保険料四分の一免除期間,m) print(’保険料四分の一免除期間’,L)
print(’実行時間’,time.time()-start, ’sec’)
# 保険料納付済期間 [17, 10, 19, 6, 16, 15, 14, 9, 13, 11, 12]
# 保険料免除期間 [8, 7, 18]
# 保険料全額免除期間 [18]
# 保険料四分の三免除期間 []
# 保険料半額免除期間 [7, 8]
# 保険料四分の一免除期間 []
# 実行時間 0.8100388050079346 sec
7.1.4 ノート
• 第五条では，保険料納付期間や免除期間が定義されている．これらは，納付や免除が行われ た月の集合であり，第二十六条や二十七条において老齢基礎年金の支給要件や年金額を算定 する場合の基礎になるものである．これらの期間の定義には，
– 被保険者期間を決定する規則（第十一条）
– 各種の保険料免除要件を定める規則（第八十九、九十条、九十条の二，九十条の三）
– 保険料納付に関する記録(年金原簿) が必要になる．
なお，保険料の納付については，正常な納付の他に，滞納者に対する督促を経て徴収され たもの（第九十六条），申請により免除された保険料が後で納付さたもの（追納，第九十四 条）が含まれること，また，一部免除の場合の残りの保険料の納付は保険料納付期間には含 まれないことが述べられている．
• 条文の論理式化f5においては，条文モジュールf11,f89,f90,f90_2,f90_3から必要な述 語がインポートされ，更に，いくつかの述語が年金原簿モジュールからインポートされてい る（保険料納付済み，追納により納付とみなされる期間,残りの四分の一・半額・四分の三 納付).
• 論理式化は条文の内容をそのまま論理式に直したものではあるが，字義的な変換を行う事は 困難で，条文の内容の理解が必要である．例えば，条文では第七条について述べられている が，必要なのは第十一条であり，これは言及されていない．
• 検証では小さな年金原簿モジュールhonnin_v5（7.19参照）を用い，定義されている納付，
免除期間が正しく計算されることを確認した．検証スクリプト中，充足リスト(f,m)は述 語f(i)がi=0,...,m-1の範囲で充足される（Trueとなる）iのリストを返す関数であり，
definitionsモジュールで定義されている．(7.21参照)