大学の無線LAN

システム更新前のアクセスポイントが確保してあるので、それを各部屋に配れば改善するはずですが、

　　まぁ、シス管の人手不足とか、自分のやる気とか

いろいろ。でも、

　　PoE なんだよな

今のスイッチで動くんだったっけ? と思ったが動くらしいです。

もっとも、

　　遠隔授業は、基本、有線派

家でもそうしたいが、配線がなかなかな。

Bijection と invariant

　record Bijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m)　where
　 field
　　　 fun←　:　S → R
　　　 fun→　:　R → S
　　　 fiso← : (x : R)　→ fun← ( fun→ x )　≡ x
　　　 fiso→ : (x : S ) → fun→ ( fun← x )　≡ x

ですね。割と当たり前なんだが、

　　Bijection ℕ (ℕ ∧ ℕ) と Bijection ℕ ( List Bool )

後者は今年のお正月にやって、敗れさっていたらしい。ぜんぜん簡単なんですが、Agda で書くのはな。

なんですが、やっと invariant を書くのになれたみたい。

fun← ( fun→ x )　≡ x　を直接証明しようとすると、関数の引数を調整しながら

　 定義と同じように項 fun← ( fun→ x ) が展開されるようにする

というのが必要になるんですが、これがだいたいうまくいかない。なんだけど、

　record Invariant (i : S)　: Set
　 field
　　 j : R
　　 k1 : fun← i ≡ j
　　 k0 : fun→ j ≡ i

というように書いてやると、k1/k0 個別に調整できるので楽になるというわけ。induction で、Invariant を作れば完成と。

ま、証明の細かい面倒さは避けられないけど。

この Bijection は超準解析や集合の濃度でも使うからな。

これで、Agda の練習用の問題は一通りできた感じ。

　　素数が無限にある
　　素数の平方根が無理数

https://github.com/shinji-kono/automaton-in-agda

原神

まだ、やってたりするんですけどね。このゲーム、課金のポイントと必要性がわからんのだよな。

問題は英語モードでやってるので、検索が良くわからん。人の名前が英語だし。つまらん台詞読む根性が...

金の林檎諸島は半分位まわりました。(と数値には出てる

Daily Mission は退屈だし、効率も良くないのでやめました。武器とか進化とかめんどくさい。

でも、夏のイベントでだいぶ成長させたので、雪山の頂上まではいけました。

Golden House が終わってないんだが、越えられそうではある。

うっかり、World level を上げてしまうと、いろいろ倒せなくなる。(きまった mission をクリアしなければ上がらない

World Levev 4 / Adeventure Lank 45 です。

なのだが、また、いろいろ倒せるようになってるな。Electro Hypostasis とかは、まだ、だめ。

もっとも、そこを目標にしなくても、ちんたら、お使いするのでも良いんだよな。

ノンアルコールビール

なんか、こう飯屋が早く閉まるのがなぁ。酒飲まないので、やせた人も多いんじゃないかな。

カフェで早めに夕ご飯でも、なんかノリがな

　　で、気分的に

ま、ちょっと癒される気もするかな。

割と酒強い方なので、そんなに変わらないから、アルコール入ってても入ってなくても差がない的な?!

わけわかんないもの

板にガラス玉がはめてあるオブジェっぽいもの

これも北上原の販売所にある

光とか当てるとどうにかなるとか

とうがん

どしゃぶり続きですが、

　　ingress は、やってます

北中城の販売所のとうがん。

カフェクッチェのとうがん入りのグリーンカレーを思い出すな。

テレビっ子

と呼ばれた世代なんですけどね。もちろん死語ですが。

結局、BDレコーダーだけでなくアンテナ全滅らしい。BDレコーダ SKP 75 x 2 は割と気に入ってた機械ですが、

　　D端子とかでも映らず

ただ、DLNA経由なら観れます。取り出す方法はないな。メニュー打てればいいんだけど、視覚に頼ったUIだからな。

東芝RDだったがWebリモコンに画面が映ったんだが。中身、Linuxなんだから ssh よこせとも思うけどね。

修理すると2万5千円飛ぶので、2台だから新品かった方が良いな。それでも、いくつか選択肢が

1) そのままアンテナ修理してもらう

2) CATVに乗り換える (月2千円

3) 録画はやめ、Netfliex とかで良い

まぁ、fj と同じで「テレビ視聴」ってのを動態保存したい気はする。テレビっ子ですからね。

録画整理も無意味な楽しみではあるからなぁ。この前も2015なベストヒットUSAとか発掘してました。

-