No Such Blog or Diary

乱択アルゴリズムの証明とか Coq でできるのかなとか思って検索かけたら，Alea: a library for reasoning on randomized algorithms in Coq とかいうまさにそれってのが出てきた．面白そうなのでそのうち調べよう．

いつからおかしくなってたのか，ヒンジ部のパーツが微妙に歪んでディスプレイの開閉がスムーズでなくなってた．約10年位 let'snote を使い続けているけれど物理的な故障は初めて．どこで痛めたのやら……

今ひとつ logic における interpolation のイメージが良くわからん．恒真な implication を順序だと思って並べだ時の間を探すってことで良いのだろうか．最初の人がこれを interpolation と読んだ意図はなんだらう？

閑話休題．

何かおかしいので寝よう．

台湾ラーメンが辛かった……　味がわからなくなる辛さの閾値が低めなのでスープまで飲み干すとか無理というか苦行でしかない．

閑話休題．

鉄骨に磁気が残るのか．どの程度の強度なんだろう？

JAL だと FDA 便で小牧になるのでちょっと微妙？

そして空港から名古屋駅行きのバスでICカードが使えないとかいうのに驚いた．不便すぎる．

朝イチで電話があったので引き取りに行ってきた．無事異音解消とのこと．

んで，メンテノートを見てみたらピストンコンロッドキットとピストンリングリプレースメントキットとかいう名前の交換部品が使われたらしい．ピストンとリングを替えてオイルの噴射するところも直したと言ってたので，オイルジェットが微妙に詰まり気味だったからコンロッドとピストン一式変えてみましたとかいう感じかね．

つまりあの音はスラップ音とか言う奴だったのか……

だがしかし，はっきりとした音はなくなったけれどまだ微妙に紙を擦ったような微かな音がしとるなぁ．まあいいか．

閑話休題．

やっぱり車もサービスマニュアル（修理書？）を入手しておくかな……