A問題

https://gist.github.com/2391779

ヒントの制約からなんとか関数を自動で生成したかった。

eexists (fun ch =>
  match ch with
    | "a" => _  | "b" => _  | "c" => _  | "d" => _
    | "e" => _  | "f" => _  | "g" => _  | "h" => _
    | "i" => _  | "j" => _  | "k" => _  | "l" => _
    | "m" => _  | "n" => _  | "o" => _  | "p" => _
    | "q" => _  | "r" => _  | "s" => _  | "t" => _
    | "u" => _  | "v" => _  | "w" => _  | "x" => _
    | "y" => _  | "z" => _
    | _ => ch
  end).

このへんまではまあ手で書いてやっても許されるだろう。で、ヒントをこの関数に食わせて reflexitivity で決定していく。
あれ、一個文字が確定しないぞ、しかたがないからほかの条件から埋めていくか。

しかし、ほかの条件はすごく重い。計算させようとしてすぐにemacsが凍りつく状態にないやがったので諦めて手で指定する。
ほかのプロパティーも重いのでかなり妥協して、Permutationだけにしたんだけど、やっぱり計算では証明できなくて非常に悲しい証明を書いてしまった。

OCamlを抽出して実行してもよかったんだけどめんどくさいから、trを抽出する。

tail -n +2 | tr ynficwlbkuomxsevzpdrjgthaq a-z | awk '{printf "Case #%d: %s\n", NR, $0}'

最終的にone liner