つづき
上の続き
というわけで、
(oN oN tr n) (oN oN tr m) --> (exec_tr tr (m_n_mod3 m n)); (oN oN tr (succ m))
に書き換わらないといけないわけだ。
これは
let.apply_2nd_3rd = abs x, y do end let.oN_sub = abs oN, tr, x, _y, z do ... end
を使って
let.oN = abs my, tr, n, oM do oM(apply_2nd_3rd, oN_sub(my, tr), n) end
とするとなぜかうまくいく。
(oN oN tr n) (oN oN tr m) --> (oN oN tr m) apply_2nd_3rd (oN_sub oN tr) n --> apply_2nd_3rd apply_2nd_3rd (oN_sub oN tr) m (oN_sub oN tr) n --> oN_sub oN tr m (oN_sub oN tr) n
まあ、動いていればそれでいい。
というわけで、oN_subの実装は
let.oN_sub = abs oN, tr, x, _y, z do exec_tr(tr, m_n_mod3(x, z)) oN(oN, tr, succ(x)) end
ということになる。
残っている問題は (m-n)%3 をどうするかだ。