# 反函數：交換有限雙射表並求非零斜率仿射函數的反函數

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-inverse-function/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-inverse-function-01 · production-20261019-adopted-96



## 目標與範圍

（一）A={1,2,3}、B={4,5,6}，p(1)=5、p(2)=6、p(3)=4。先確認 p 是雙射，再交換有序對得到候選 q，驗證 q 是總函數 B→A，並逐側檢查 q(p(x))=x 與 p(q(y))=y。（二）f:ℝ→ℝ，f(x)=−4x+6（m=−4≠0）：求反函數 g(y)=uy+v，u、v 以最簡、正分母的有理數表示，並對所有實數驗證兩側恆等式。（三）說明 h(1)=4、h(2)=4、h(3)=6 的交換表不是 B→A 的函數，以及 f^{-1} 不是 1/f。

依 MKO 假設：有限表先確認是宣告 A→B 的雙射（a1）；候選先驗為總函數再查兩側恆等式（a2）；仿射例子為 f:ℝ→ℝ、m≠0，係數以最簡正分母有理數表示（a3）。仿射部分以代數恆等式對所有實數證明，不是抽樣。不處理一般單側反函數理論、反函數唯一性或機器證明；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- function_def
- injective_surjective_def
- composition_def
- frac_rules
- distributive
- numeric_evaluation


- G1 — A={1,2,3}、B={4,5,6}；p:A→B，p(1)=5、p(2)=6、p(3)=4。
- G2 — f:ℝ→ℝ，f(x)=−4x+6，即 m=−4、b=6。
- G3 — h:A→B，h(1)=4、h(2)=4、h(3)=6。
- G4 — 驗收標準（MKO a2）：候選 g 是雙射 f:A→B 的反函數，當且僅當 g 是總函數 B→A，且對每個 x∈A 有 g(f(x))=x、對每個 y∈B 有 f(g(y))=y。


- p,q — 有限雙射表與交換後的表
- f,g — 仿射函數 f(x)=−4x+6 與其反函數
- h — 非雙射的有限表
- R^{\mathsf T} — 交換關係 {(b,a) ∣ (a,b)∈R}
- \mathrm{id}_A — A 上的恆等函數





## 規則與來源


- function_def · prerequisite — 函數：f:A→B 對每個 a∈A 指定恰好一個 f(a)∈B。兩函數相等 ⇔ 定義域、對應域相同且對每個 a 都有相同值。
- injective_surjective_def · prerequisite — 單射：f(a)=f(a′) ⇒ a=a′。滿射：每個 b∈B 都有 a∈A 使 f(a)=b。雙射：既單又滿，此時有唯一反函數 f⁻¹ 使 f⁻¹∘f=id_A、f∘f⁻¹=id_B。
- composition_def · prerequisite — 合成：對 f:A→B 與 g:B→C，g∘f:A→C 定義為 (g∘f)(a)=g(f(a))。
- frac_rules · prerequisite — 分數運算（分母皆非零）：a/c+b/c=(a+b)/c；(a/b)(c/d)=(ac)/(bd)；(a/b)/(c/d)=(ad)/(bc)（另需 c≠0）；a/b=(ak)/(bk)（k≠0）。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
- cartesian_product_def · prerequisite — 笛卡兒積：A×B 是所有有序對 (a,b)（a∈A、b∈B）的集合；(a,b)=(c,d) ⇔ a=c 且 b=d。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
- mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
- add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
- add_comm · prerequisite — 加法交換律：u+v=v+u。
- add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
- add_zero · prerequisite — 加法單位元：u+0=u。
- mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
- mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
- mul_one · prerequisite — 乘法單位元：1·u=u。
- iff_intro · prerequisite — 雙條件：P⇒Q 與 Q⇒P 都成立時，P⇔Q 成立；反之亦然。
- neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- mko_inverse_def · cited — 若 f:A→B 是雙射，反函數 g:B→A 由每個 b 的唯一原像定義，滿足 g(f(x))=x（x∈A）及 f(g(y))=y（y∈B）。有限表可以交換有序對後建立 g；若 f 非雙射，交換表不能自動成為這個 B→A 的反函數。 · mko-inverse-function
- mko_bijective_fiber · cited — 總函數 f:A→B 為雙射，當且僅當它同時單射與滿射；等價地，每個 b∈B 的纖維恰有一個元素。 · mko-bijective
- swap_table · prerequisite — 交換表：關係 R⊆A×B 的交換為 R^T={(b,a) ∣ (a,b)∈R}⊆B×A。b 在 R^T 中作為第一坐標出現的次數，等於 b 在 R 中作為第二坐標出現的次數。
- L_solve_affine · lemma — 對實數 m≠0、b、x、y：y=mx+b ⇔ x=(y−b)/m。





## 逐步主鏈

S01 · implies操作前

p(1)=5,\ p(2)=6,\ p(3)=4

操作後

p^{-1}(\{4\})=\{3\},\ p^{-1}(\{5\})=\{1\},\ p^{-1}(\{6\})=\{2\}\ \Rightarrow\ p\ \text{bijective}

條件：無

規則：mko_bijective_fiber · 依賴：G1, mko_bijective_fiber

葉節點依據：mko_bijective_fiber + set_builder + numeric_evaluation

MKO 假設 a1 要求先確認 p 是宣告 A→B 的雙射。掃描 A 的三個元素：目標 4 只由 3 達到、5 只由 1 達到、6 只由 2 達到。B 的每個目標的纖維都恰有一個元素，所以 p 是雙射。



S02 · definition操作前

p=\{(1,5),(2,6),(3,4)\}

操作後

q=p^{\mathsf T}=\{(5,1),(6,2),(4,3)\}

條件：無

規則：swap_table · 依賴：G1

葉節點依據：swap_table + cartesian_product_def

把 p 寫成有序對的集合，交換每一對的兩個坐標，得到候選 q。此時 q 只是 B×A 的一個子集合（關係）；它是否為函數 B→A 必須另外檢查（a2）。



S03 · implies操作前

q=\{(4,3),(5,1),(6,2)\}

操作後

q:B\to A\ \text{total};\ q(4)=3,\ q(5)=1,\ q(6)=2

條件：無

規則：function_def · 依賴：S01, S02

葉節點依據：function_def + swap_table + set_builder

依 swap_table，b 在 q 中作為第一坐標出現的次數等於 b 在 p 中作為值出現的次數，也就是纖維 p^{-1}({b}) 的大小，由 S01 都是 1。所以 4、5、6 各恰好出現一次：每個 b 有值（總）且只有一個值（單值），值 3、1、2 都在 A 中。q 是總函數 B→A。



S04 · implies操作前

x\in A=\{1,2,3\}

操作後

q(p(x))=x\ \ \forall x\in A

條件：無

規則：case_analysis · 依賴：G1, S03

葉節點依據：case_analysis + composition_def + numeric_evaluation

A 恰有三個元素，逐一檢查就是窮盡所有情形的證明，不是抽樣：q(p(1))=q(5)=1，q(p(2))=q(6)=2，q(p(3))=q(4)=3。所以 q∘p=id_A。



S05 · implies操作前

y\in B=\{4,5,6\}

操作後

p(q(y))=y\ \ \forall y\in B

條件：無

規則：case_analysis · 依賴：G1, S03

葉節點依據：case_analysis + composition_def + numeric_evaluation

第二個恆等式必須另外檢查，因為代表公式 g(f(x))=x 只呈現其中一側：p(q(4))=p(3)=4，p(q(5))=p(1)=5，p(q(6))=p(2)=6。B 的三個元素全部檢查過，所以 p∘q=id_B。



S06 · implies操作前

q:B\to A\ \text{total},\ q\circ p=\mathrm{id}_A,\ p\circ q=\mathrm{id}_B

操作後

q=p^{-1}

條件：無

規則：mko_inverse_def · 依賴：S03, S04, S05, G4

葉節點依據：mko_inverse_def + and_intro_elim

G4 的三個要求都已成立：q 是總函數（S03）、q∘p=id_A（S04）、p∘q=id_B（S05）。而且 q(b) 正是 S01 中 b 的唯一原像，與 MKO 的定義一致。所以 q 是 p 的反函數。



S07 · equivalent操作前

y=-4x+6

操作後

x=\frac{y-6}{-4}

條件：-4\neq 0

規則：L_solve_affine · 依賴：G2

葉節點依據：eq_congruence + mul_inverse_nonzero

轉到仿射例子。對任意實數 y，依引理 L_solve_affine（m=−4、b=6）：y=−4x+6 ⇔ x=(y−6)/(−4)。引理在 S07.1、S07.2 證明，需要 m=−4≠0。



S08 · implies操作前

\forall y\in\mathbb{R}:\ \bigl(f(x)=y\iff x=\tfrac{y-6}{-4}\bigr)

操作後

f^{-1}(\{y\})=\{\tfrac{y-6}{-4}\}\ \Rightarrow\ f\ \text{bijective}

條件：無

規則：mko_bijective_fiber · 依賴：S07, mko_bijective_fiber

葉節點依據：mko_bijective_fiber + set_builder + iff_intro

對每個實數 y：S07 的 ⇐ 方向說明實數 (y−6)/(−4) 在 y 的纖維中（存在），⇒ 方向說明纖維中任何元素都等於它（唯一）。所以每個纖維恰有一個元素，f 是雙射，滿足 a1 的前提。



S09 · definition操作前

y\in\mathbb{R}

操作後

g(y)=\frac{y-6}{-4}

條件：無

規則：mko_inverse_def · 依賴：S08

葉節點依據：mko_inverse_def + function_def

依 MKO，反函數把每個 y 送到它的唯一原像；由 S08，這個原像是 (y−6)/(−4)。分母 −4≠0，對每個實數 y 都有定義，所以 g 是總函數 ℝ→ℝ。



S10 · equivalent操作前

\frac{y-6}{-4}

操作後

-\frac{1}{4}y+\frac{3}{2}

條件：-4\neq 0

規則：frac_rules · 依賴：S09

葉節點依據：frac_rules + neg_mul

改寫成 g(y)=uy+v 的形式，得 u=−1/4、v=3/2，細節在 S10.1、S10.2。這與 MKO 的公式一致：u=1/m=1/(−4)=−1/4，v=−b/m=−6/(−4)=3/2。兩個係數都已約到最簡，分母 4 與 2 為正。



S11 · implies操作前

x\in\mathbb{R}\ \text{arbitrary}

操作後

g(f(x))=-\tfrac{1}{4}(-4x+6)+\tfrac{3}{2}=x

條件：無

規則：forall_intro · 依賴：G2, S10

葉節點依據：composition_def + distributive + neg_mul + add_inverse + forall_intro

任取實數 x：g(f(x))=−(1/4)(−4x+6)+3/2=x−3/2+3/2=x（分配律與符號規則）。x 沒有任何附加條件，所以對所有實數成立，這是代數恆等式而不是有限核對。



S12 · implies操作前

y\in\mathbb{R}\ \text{arbitrary}

操作後

f(g(y))=-4\bigl(-\tfrac{1}{4}y+\tfrac{3}{2}\bigr)+6=y

條件：無

規則：forall_intro · 依賴：G2, S10

葉節點依據：composition_def + distributive + neg_mul + add_inverse + forall_intro

另一側：任取實數 y，f(g(y))=−4(−(1/4)y+3/2)+6=y−6+6=y。兩側恆等式都對所有實數成立。



S13 · implies操作前

g\ \text{total},\ g\circ f=\mathrm{id}_{\mathbb{R}},\ f\circ g=\mathrm{id}_{\mathbb{R}}

操作後

f^{-1}(y)=-\tfrac{1}{4}y+\tfrac{3}{2}

條件：無

規則：mko_inverse_def · 依賴：S09, S11, S12, G4

葉節點依據：mko_inverse_def + and_intro_elim + numeric_evaluation

g 是總函數（S09），兩側恆等式成立（S11、S12），依 G4 g 是 f 的反函數。具體例：f(2)=−2，而 g(−2)=1/2+3/2=2，回到 2。



S14 · implies操作前

f^{-1}(2)=1,\ \frac{1}{f(2)}=-\frac{1}{2}

操作後

f^{-1}\neq\frac{1}{f}

條件：無

規則：function_def · 依賴：S13, G2

葉節點依據：function_def + numeric_evaluation + frac_rules

f^{-1}(2)=−(1/4)·2+3/2=1，但 f(2)=−2，所以 1/f(2)=−1/2。兩個函數在同一輸入 2 的值不同，依函數相等的定義，f^{-1}≠1/f。此外 f(3/2)=0，1/f 在 x=3/2 根本沒有定義，而 f^{-1} 對每個實數都有定義。上標 −1 表示合成意義下的反，不是倒數。



S15 · implies操作前

h^{\mathsf T}=\{(4,1),(4,2),(6,3)\}

操作後

h^{\mathsf T}\ \text{not a function}\ B\to A

條件：無

規則：function_def · 依賴：G3

葉節點依據：function_def + swap_table + set_builder

交換 h 的表：4 同時對應 1 與 2（不是單值），5 沒有對應（不是總的），函數的兩個要求都不滿足。這對應 h 的纖維概況 (2,0,1)：h 不是雙射，依 a1 不能用交換表當作反函數。事實上沒有任何 r:B→A 能滿足 h(r(y))=y 對所有 y∈B，因為取 y=5 需要 h(r(5))=5，而 5 不是 h 的值。



S16 · implies操作前

\text{S06, S13, S14, S15}

操作後

q=p^{-1};\ f^{-1}(y)=-\tfrac{1}{4}y+\tfrac{3}{2};\ h^{\mathsf T}\ \text{rejected};\ f^{-1}\neq 1/f

條件：無

規則：and_intro_elim · 依賴：S06, S13, S14, S15

葉節點依據：and_intro_elim

整理三部分：有限雙射表交換後得到 p 的反函數 q；仿射函數的反函數係數 u=−1/4、v=3/2；非雙射的交換表被拒絕，反函數也與倒數區分開。







## 局部子步與引理

S07.1 · equivalent操作前

y=mx+b

操作後

y-b=mx

條件：無

規則：eq_congruence · 依賴：eq_congruence

葉節點依據：eq_congruence + add_assoc + add_comm + add_inverse + add_zero

兩邊同減 b：(mx+b)−b=mx（加法結合律與反元素）。反向是兩邊同加 b。



S07.2 · equivalent操作前

y-b=mx

操作後

x=\frac{y-b}{m}

條件：m\neq 0

規則：mul_inverse_nonzero · 依賴：S07.1, mul_inverse_nonzero

葉節點依據：eq_congruence + mul_inverse_nonzero + mul_assoc + mul_comm + mul_one

因 m≠0，1/m 存在；兩邊同乘 1/m 得 (y−b)/m=x。反向是兩邊同乘 m。若 m=0，此步不能做，而且 f(x)=b 是常數函數，根本不是雙射。S07.1 與 S07.2 合起來證得引理 L_solve_affine。



S10.1 · equivalent操作前

\frac{y-6}{-4}

操作後

\frac{y}{-4}-\frac{6}{-4}

條件：-4\neq 0

規則：frac_rules · 依賴：S09, frac_rules

葉節點依據：frac_rules

同分母分式的加減：(a−c)/d=a/d−c/d（d=−4≠0）。反向是把兩個同分母分式合併。



S10.2 · equivalent操作前

\frac{y}{-4}-\frac{6}{-4}

操作後

-\frac{1}{4}y+\frac{3}{2}

條件：無

規則：frac_rules · 依賴：S10.1, neg_mul

葉節點依據：frac_rules + neg_mul + numeric_evaluation

把負分母移到分子：y/(−4)=−y/4=(−1/4)y；6/(−4)=−6/4=−3/2（以 gcd(6,4)=2 約分），減去 −3/2 即加 3/2。所以 u=−1/4、v=3/2，gcd(1,4)=1、gcd(3,2)=1，分母為正。







## 逐步反向審查


- S16 · sufficient_goal_reduction · S06, S13, S14, S15, and_intro_elim — 目標 G 是 goal 的三部分。足夠條件 H 為 S06、S13、S14、S15 的合取，各自已從已知正向證成；H⇒G 只用合取引入。
- S15 · premise_audit · function_def, swap_table, G3 — 任一個要求失敗就足以否定「是函數」；這裡兩個都失敗。結論只關於 h，不影響 p、f。
- S14 · premise_audit · function_def, numeric_evaluation, S13 — 否定兩函數相等只需一個取值不同的輸入；本步不宣稱它們在每一點都不同。
- S13 · premise_audit · S09, S11, S12, mko_inverse_def — 三個驗收條件都已逐一成立；具體例只是示意，不是證明的一部分。
- S12 · premise_audit · composition_def, distributive, neg_mul, forall_intro — 與 S11 對稱；此側不能由 S11 推出，所以單獨證明。
- S11 · premise_audit · composition_def, distributive, neg_mul, forall_intro — 需要 f(x)∈ℝ 位於 g 的定義域，合成才有定義；推廣到所有 x 只因 x 是任意取的。
- S10.2 · inverse_equivalence · frac_rules, neg_mul — 分子分母同乘 −1 與約分都是等值改寫，可逆。
- S10.1 · inverse_equivalence · frac_rules — 分式加法規則雙向成立，前提只有分母不為零。
- S10 · inverse_equivalence · frac_rules, neg_mul — S10.1、S10.2 兩個子步都是對所有 y 成立的恆等改寫，所以兩個式子定義同一個函數。
- S09 · premise_audit · S08, mko_inverse_def, function_def — 只是依唯一原像命名函數；兩側恆等式仍在 S11、S12 另行驗證。
- S08 · premise_audit · S07, mko_bijective_fiber, iff_intro — 兩個方向都要用：只有 ⇐ 只給滿射，只有 ⇒ 只給單射。
- S07.2 · inverse_equivalence · mul_inverse_nonzero, eq_congruence — 乘 1/m 與乘 m 互為反運算，前提 m≠0，正是 MKO a3 的條件。
- S07.1 · inverse_equivalence · eq_congruence, add_inverse — 減 b 與加 b 互為反運算，對任何實數 b 都可做。
- S07 · inverse_equivalence · L_solve_affine — 引理兩個方向都在子步中證明，條件 −4≠0 成立。
- S06 · premise_audit · S03, S04, S05, mko_inverse_def — 需要三個條件同時成立；只有其中一側恆等式不夠（見錯誤控制）。
- S05 · premise_audit · case_analysis, composition_def, S03 — q 的值都在 A，p∘q 有定義；三個情形窮盡 B。
- S04 · premise_audit · case_analysis, composition_def, S03 — 合成有定義，因為 p 的值都在 B，也就是 q 的定義域；三個情形窮盡 A。這只是一側的恆等式，另一側在 S05。
- S03 · premise_audit · S01, swap_table, function_def — 總性需要每個纖維至少一個元素（p 滿射），單值性需要至多一個元素（p 單射），兩者都由 S01 提供。若 p 不是雙射，這一步就會失敗（見 S15）。
- S02 · premise_audit · swap_table, cartesian_product_def — 只是構造一個集合並命名，不宣稱 q 是函數。
- S01 · premise_audit · G1, mko_bijective_fiber, set_builder — 需要掃描全部三個輸入並檢查宣告陪域的全部三個目標；只用纖維刻畫的 ⇐ 方向。





## 錯誤控制與反例

反函數不是倒數MKO 的誤解之一是把 f^{-1} 當成 1/f。上標 −1 表示對合成的反：f^{-1}(2)=1，但 1/f(2)=−1/2（S14）。而且 1/f 在 x=3/2 沒有定義（f(3/2)=0），f^{-1} 卻對每個實數都有定義。

非雙射的交換表不是反函數另一個誤解是不管是否雙射都交換表。h 的纖維概況是 (2,0,1)，交換後 4 對應兩個值、5 沒有值，不是 B→A 的函數（S15）。MKO 要求先確認雙射（a1），再交換。

兩側恆等式都要查只有一側成立時不是反函數。例：p′:{1,2}→{4,5,6}，p′(1)=4、p′(2)=5；候選 r:{4,5,6}→{1,2}，r(4)=1、r(5)=2、r(6)=1 是總函數，且對每個 x∈{1,2} 都有 r(p′(x))=x，但 p′(r(6))=p′(1)=4≠6。r 只是左反函數。本稿對 q 與 g 都分別驗證兩側（S04、S05、S11、S12）。


- g(y)=1/(−4y+6) 是 f 的反函數 → reject — 這是 1/f，不是反函數：f(0)=6，而 1/(−4·6+6)=−1/18≠0，所以 g(f(0))≠0。
- h 的交換表 {(4,1),(4,2),(6,3)} 是 h 的反函數 → reject — 它不是 B→A 的函數：4 有兩個值，5 沒有值；h 不是雙射。
- r(4)=1、r(5)=2、r(6)=1 滿足 r(p′(x))=x，所以 r 是 p′ 的反函數 → reject — 另一側不成立：p′(r(6))=p′(1)=4≠6。
- f(x)=−4x+6 的反函數是 g(y)=(y+6)/(−4) → reject — 符號錯：f(0)=6，而 (6+6)/(−4)=−3≠0；正確的是 (y−6)/(−4)。





## 結論與限制

p 的纖維概況為 (1,1,1)，是雙射；交換表 q 是總函數 B→A，q(4)=3、q(5)=1、q(6)=2，且 q∘p=id_A、p∘q=id_B，所以 q=p^{-1}。f(x)=−4x+6 是雙射，反函數為 f^{-1}(y)=(y−6)/(−4)=−(1/4)y+3/2，即 u=−1/4、v=3/2，兩側恆等式對所有實數成立。h 的交換表不是 B→A 的函數（4 有兩個值、5 沒有值）；f^{-1}(2)=1 而 1/f(2)=−1/2，所以 f^{-1}≠1/f。


- 本稿不另證反函數的唯一性；只驗證構造出的 q 與 g 符合 MKO 的兩側定義。
- N3 至 N5 是一次多項式在格點上的恆等式核對，與 S10 至 S12 的代數推導互相獨立。





## 驗證及來源綁定

14 個本稿宣告算術檢查；只支持所列算式。


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: a9ff58a9eb164d3ba3885c3f347bc130c608c3b605ef14409ff4d974ddfcb2e6
- original source SHA-256: a9ff58a9eb164d3ba3885c3f347bc130c608c3b605ef14409ff4d974ddfcb2e6
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-inverse-function-01.json)