oupo
https://blog.hatena.ne.jp/oupo/
oupoの日記
https://oupo.hatenadiary.com/
logic
二つの命題が相互依存になって、二つの証明の帰納法を同時に実行することで解消するという大掛かりな方法になってしまった。 既知とする命題 既知の命題1: λx.Q ≡α λy.Q' ⇔ Q' ≡α [y/x]Q かつ [x≡y または y ∉ FV(Q)] 既知の命題2: R' ≡α R, λy.Q' ≡α λx.Q ⇒ [R'/y]Q' ≡α [R/x]Q この二つは補助定理1.2.36により証明できる。 既知の命題3: M →1 Nに長さn+1の証明図がある ⇔ Nとα同値なN'が存在しM ▷1 N'に長さnの証明図がある 既知の命題4: M →1 Nに長さnの証明図がありN' ≡α N ⇒ …
190
<iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Foupo.hatenadiary.com%2Fentry%2F20121210%2F1355116211" title="M ≡α M', M →1β N ならば M' →1β N - oupoの日記" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe>
Hatena Blog
https://hatena.blog
2012-12-10 14:10:11
M ≡α M', M →1β N ならば M' →1β N
rich
https://oupo.hatenadiary.com/entry/20121210/1355116211
1.0
100%