国民年金法第三十七条遺族基礎年金の支給要件.v

Require Import Nat.

Inductive Person :=
  | CPerson : nat -> option Person -> Person.

Definition 年齢 p :=
  let 'CPerson 年齢 配偶者 := p in 年齢.

Definition 配偶者 p :=
  let 'CPerson 年齢 配偶者 := p in 配偶者.

Definition 述語 := Person -> Prop.
Variable Is : Person -> 述語 -> Prop.
Notation "x 'は' y" := (Is x y) (at level 80).

Variable 配偶者である : Person -> 述語.
Notation "p 'の配偶者'" := (配偶者である p) (at level 190).
Variable 子である : Person -> 述語.
Notation "p 'の子'" := (子である p) (at level 190).

Variables 被保険者 被保険者であった : 述語.
Variables 死亡した 日本国内に住所を有す _60歳以上 _65歳未満: 述語.
Variables 老齢基礎年金の受給権者 老齢基礎年金の受給資格期間を満たしている: 述語.

Notation "n '歳以上'" := (fun p => 年齢 p >= n) (at level 300).
Notation "n '歳未満'" := (fun p => 年齢 p < n) (at level 300).

Variable 死亡日の前日において死亡日の属する月の前々月までに被保険者期間がある : 述語.
Variable 当該被保険者期間に係る保険料納付済期間 保険料免除期間 当該被保険者期間: nat.


Definition 支給要件 := forall p, exists q,
 (p は 被保険者 \/ p は 被保険者であった)
  /\ (q は (p の配偶者) \/ p は (q の子))
  /\ (
  (p は 被保険者 /\ p は 死亡した) \/
  (p は 被保険者であった /\ p は 日本国内に住所を有す /\ p は (60 歳以上) /\ p は (65 歳未満) /\ p は 死亡した) \/
  (p は 老齢基礎年金の受給権者 /\ p は 死亡した) \/
  (p は 老齢基礎年金の受給資格期間を満たしている /\ p は 死亡した)
) /\
~ (
(
(p は 被保険者 /\ p は 死亡した) \/
(p は 被保険者であった /\ p は 日本国内に住所を有す /\ p は (60 歳以上) /\ p は (65 歳未満) /\ p は 死亡した)
) /\ p は 死亡日の前日において死亡日の属する月の前々月までに被保険者期間がある
  /\ 当該被保険者期間に係る保険料納付済期間 + 保険料免除期間 < (当該被保険者期間 * 2 / 3)
).