Kuniwak · June 18, 2025 00:59
diff --git a/coin_problem_fl.txt b/coin_problem_fl.txt
 M: ℕ     （支払い金額）
 S: coin multiset     （財布）
 W1, W2, W3: coin multiset     （渡す貨幣）
 O1, O2, O3: coin multiset     （お釣り）
 submultiset: 'a multiset ⇒ 'a multiset ⇒ bool     （多重集合が包含されていれば真、そうでなければ偽）
 card: 'a multiset ⇒ ℕ     （多重集合の要素数）
 norm: coin multiset ⇒ bool     （貨幣の多重集合が正規形であれば真、そうでなければ偽）
 val: coin multiset ⇒ ℕ     （貨幣の多重集合の価値）
 Pay(M, S, O, W) ≡ submultiset(W1, S) ∧ val(W) - val(O) = M ∧ norm(O) ∧ norm(S - W + O)     （支払い関係が成立していれば真、そうでなければ偽）

 ∀M S O1 O2 W1 W2. Pay(M, S, O1, W1) ⟶ Pay(M, S, O2, W2) ⟶ (∀O3 W3. Pay(M, S, O3, W3) ⟶ card(W1) ≦ card(W3)) ⟶ (∀O3 W3. Pay(M, S, O3, W3) ⟶ card(W2) ≦ card(W3)) ⟶ W1 = W2
diff --git a/coin_problem_nl.txt b/coin_problem_nl.txt
 ある金額についてその価値をもつ紙幣と硬貨の組み合わせのうちその総数が最小の組み合わせを正規形と呼ぶ。
 なお貨幣として1円硬貨、5円硬貨、10円硬貨、50円硬貨、100円硬貨、500円硬貨、1000円紙幣、5000円紙幣、10000円紙幣のみがあるとする。
 この貨幣の構成は倍数条件を満たすので、どんな金額にも正規形が存在し、かつ正規形は唯一である。

 Q. お釣りは常に正規形であるとし、かつお釣りを受け取った後の財布を正規化するような渡し方が存在するどんな支払い金額および手元の財布の状況でも、渡す総数を最小にする渡し方は唯一か？
	M: ℕ （支払い金額）
	S: coin multiset （財布）
	W1, W2, W3: coin multiset （渡す貨幣）
	O1, O2, O3: coin multiset （お釣り）
	submultiset: 'a multiset ⇒ 'a multiset ⇒ bool （多重集合が包含されていれば真、そうでなければ偽）
	card: 'a multiset ⇒ ℕ （多重集合の要素数）
	norm: coin multiset ⇒ bool （貨幣の多重集合が正規形であれば真、そうでなければ偽）
	val: coin multiset ⇒ ℕ （貨幣の多重集合の価値）
	Pay(M, S, O, W) ≡ submultiset(W1, S) ∧ val(W) - val(O) = M ∧ norm(O) ∧ norm(S - W + O) （支払い関係が成立していれば真、そうでなければ偽）

	∀M S O1 O2 W1 W2. Pay(M, S, O1, W1) ⟶ Pay(M, S, O2, W2) ⟶ (∀O3 W3. Pay(M, S, O3, W3) ⟶ card(W1) ≦ card(W3)) ⟶ (∀O3 W3. Pay(M, S, O3, W3) ⟶ card(W2) ≦ card(W3)) ⟶ W1 = W2
	ある金額についてその価値をもつ紙幣と硬貨の組み合わせのうちその総数が最小の組み合わせを正規形と呼ぶ。
	なお貨幣として1円硬貨、5円硬貨、10円硬貨、50円硬貨、100円硬貨、500円硬貨、1000円紙幣、5000円紙幣、10000円紙幣のみがあるとする。
	この貨幣の構成は倍数条件を満たすので、どんな金額にも正規形が存在し、かつ正規形は唯一である。

	Q. お釣りは常に正規形であるとし、かつお釣りを受け取った後の財布を正規化するような渡し方が存在するどんな支払い金額および手元の財布の状況でも、渡す総数を最小にする渡し方は唯一か？