Mercurial > hg > Papers > 2021 > soto-prosym

changeset 13:76c3378c61dc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ADD カンペが完成
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Sat, 08 Jan 2022 09:53:19 +0900
parents 62e56d73f104
children 393c839f987b
files MindMap/slide.html slide/note.md slide/slide.md
diffstat 3 files changed, 178 insertions(+), 60 deletions(-) [+]
line wrap: on
line diff
--- a/MindMap/slide.html	Fri Jan 07 00:58:07 2022 +0900
+++ b/MindMap/slide.html	Sat Jan 08 09:53:19 2022 +0900
@@ -48,7 +48,7 @@
    top: 300px;
    text-align: center;
 }
-" data-heading-divider="1" class="title" data-marpit-pagination="1" data-marpit-pagination-total="28" style="--paginate:true;--class:title;--theme:default;--style:section {
+" data-heading-divider="1" class="title" data-marpit-pagination="1" data-marpit-pagination-total="29" style="--paginate:true;--class:title;--theme:default;--style:section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -131,7 +131,7 @@
    top: 300px;
    text-align: center;
 }
-" data-heading-divider="1" class="slide" data-marpit-pagination="2" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section {
+" data-heading-divider="1" class="slide" data-marpit-pagination="2" data-marpit-pagination-total="29" style="--paginate:true;--class:slide;--theme:default;--style:section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -227,7 +227,7 @@
    top: 300px;
    text-align: center;
 }
-" data-heading-divider="1" class="slide" data-marpit-pagination="3" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section {
+" data-heading-divider="1" class="slide" data-marpit-pagination="3" data-marpit-pagination-total="29" style="--paginate:true;--class:slide;--theme:default;--style:section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -318,7 +318,7 @@
    top: 300px;
    text-align: center;
 }
-" data-heading-divider="1" class="slide" data-marpit-pagination="4" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section {
+" data-heading-divider="1" class="slide" data-marpit-pagination="4" data-marpit-pagination-total="29" style="--paginate:true;--class:slide;--theme:default;--style:section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -413,7 +413,7 @@
    top: 300px;
    text-align: center;
 }
-" data-heading-divider="1" class="slide" data-marpit-pagination="5" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section {
+" data-heading-divider="1" class="slide" data-marpit-pagination="5" data-marpit-pagination-total="29" style="--paginate:true;--class:slide;--theme:default;--style:section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -462,10 +462,10 @@
 open Env
 </span></span></foreignObject></svg></code></pre>
 <p>型に対応する値の導入(intro)</p>
-<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>record {varx = zero ; vary = suc zero}
+<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>record {varn = zero ; vari = suc zero}
 </span></span></foreignObject></svg></code></pre>
 <p>record の値のアクセス(elim)</p>
-<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>(env : Env) → varx env
+<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>(env : Env) → varn env
 </span></span></foreignObject></svg></code></pre>
 </section>
 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="6" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
@@ -507,7 +507,7 @@
    top: 300px;
    text-align: center;
 }
-" data-heading-divider="1" class="slide" data-marpit-pagination="6" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section {
+" data-heading-divider="1" class="slide" data-marpit-pagination="6" data-marpit-pagination-total="29" style="--paginate:true;--class:slide;--theme:default;--style:section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -601,7 +601,7 @@
    top: 300px;
    text-align: center;
 }
-" data-heading-divider="1" class="slide" data-marpit-pagination="7" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section {
+" data-heading-divider="1" class="slide" data-marpit-pagination="7" data-marpit-pagination-total="29" style="--paginate:true;--class:slide;--theme:default;--style:section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -697,7 +697,7 @@
    top: 300px;
    text-align: center;
 }
-" data-heading-divider="1" class="slide" data-marpit-pagination="8" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section {
+" data-heading-divider="1" class="slide" data-marpit-pagination="8" data-marpit-pagination-total="29" style="--paginate:true;--class:slide;--theme:default;--style:section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -792,7 +792,7 @@
    top: 300px;
    text-align: center;
 }
-" data-heading-divider="1" class="fig_cg" data-marpit-pagination="9" data-marpit-pagination-total="28" style="--paginate:true;--class:fig_cg;--theme:default;--style:section {
+" data-heading-divider="1" class="fig_cg" data-marpit-pagination="9" data-marpit-pagination-total="29" style="--paginate:true;--class:fig_cg;--theme:default;--style:section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -875,7 +875,7 @@
    top: 300px;
    text-align: center;
 }
-" data-heading-divider="1" class="slide" data-marpit-pagination="10" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section {
+" data-heading-divider="1" class="slide" data-marpit-pagination="10" data-marpit-pagination-total="29" style="--paginate:true;--class:slide;--theme:default;--style:section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -931,7 +931,6 @@
 <ul>
 <li><code>{-# TERMINATING #-}</code></li>
 <li>with 文</li>
-<li>型と値</li>
 </ul>
 </section>
 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="11" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
@@ -973,7 +972,7 @@
    top: 300px;
    text-align: center;
 }
-" data-heading-divider="1" class="slide" data-marpit-pagination="11" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section {
+" data-heading-divider="1" class="slide" data-marpit-pagination="11" data-marpit-pagination-total="29" style="--paginate:true;--class:slide;--theme:default;--style:section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -1066,7 +1065,7 @@
    top: 300px;
    text-align: center;
 }
-" data-heading-divider="1" class="slide" data-marpit-pagination="12" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section {
+" data-heading-divider="1" class="slide" data-marpit-pagination="12" data-marpit-pagination-total="29" style="--paginate:true;--class:slide;--theme:default;--style:section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -1161,7 +1160,7 @@
    top: 300px;
    text-align: center;
 }
-" data-heading-divider="1" class="slide" data-marpit-pagination="13" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section {
+" data-heading-divider="1" class="slide" data-marpit-pagination="13" data-marpit-pagination-total="29" style="--paginate:true;--class:slide;--theme:default;--style:section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -1214,7 +1213,6 @@
 </span></span></foreignObject></svg></code></pre>
 <ul>
 <li>conversion1はPre Condition をPost Conditionに変換する</li>
-<li>whileLoopSeg</li>
 <li>⊤</li>
 </ul>
 </section>
@@ -1257,7 +1255,7 @@
    top: 300px;
    text-align: center;
 }
-" data-heading-divider="1" class="slide" data-marpit-pagination="14" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section {
+" data-heading-divider="1" class="slide" data-marpit-pagination="14" data-marpit-pagination-total="29" style="--paginate:true;--class:slide;--theme:default;--style:section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -1350,7 +1348,89 @@
    top: 300px;
    text-align: center;
 }
-" data-heading-divider="1" class="slide" data-marpit-pagination="15" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section {
+" data-heading-divider="1" class="slide" data-marpit-pagination="15" data-marpit-pagination-total="29" style="--paginate:true;--class:slide;--theme:default;--style:section {
+  background-color: #FFFFFF;
+  font-size: 28px;
+  color: #4b4b4b;
+  font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
+  background-image: url(&quot;logo.svg&quot;);
+  background-position: right 3% bottom 2%;
+  background-repeat: no-repeat;
+  background-attachment: 5%;
+  background-size: 20% auto;
+}
+
+  section.title h1 {
+    color: #808db5;
+    text-align: center;
+    }
+  
+  section.title p {
+      bottom: 25%;
+      width: 100%;
+      position: absolute;
+      font-size: 25px;
+      color: #4b4b4b;
+      background: linear-gradient(transparent 90%, #ffcc00 0%);
+  }
+
+section.slide h1 {
+    width: 95%;
+    color: white;
+    background-color: #808db5;
+    position: absolute;
+    left: 50px; 
+    top: 35px;
+}
+
+section.fig_cg p {
+   top: 300px;
+   text-align: center;
+}
+;--heading-divider:1;" data-size="16:9">
+<h1>Binary Tree</h1>
+<p>時間が余りそうならやる</p>
+</section>
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="16" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
+  background-color: #FFFFFF;
+  font-size: 28px;
+  color: #4b4b4b;
+  font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
+  background-image: url(&quot;logo.svg&quot;);
+  background-position: right 3% bottom 2%;
+  background-repeat: no-repeat;
+  background-attachment: 5%;
+  background-size: 20% auto;
+}
+
+  section.title h1 {
+    color: #808db5;
+    text-align: center;
+    }
+  
+  section.title p {
+      bottom: 25%;
+      width: 100%;
+      position: absolute;
+      font-size: 25px;
+      color: #4b4b4b;
+      background: linear-gradient(transparent 90%, #ffcc00 0%);
+  }
+
+section.slide h1 {
+    width: 95%;
+    color: white;
+    background-color: #808db5;
+    position: absolute;
+    left: 50px; 
+    top: 35px;
+}
+
+section.fig_cg p {
+   top: 300px;
+   text-align: center;
+}
+" data-heading-divider="1" class="slide" data-marpit-pagination="16" data-marpit-pagination-total="29" style="--paginate:true;--class:slide;--theme:default;--style:section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -1402,7 +1482,7 @@
 </span></span></foreignObject></svg></code></pre>
 <p>置き換えるnodeまでTreeを辿り、Stackに逆順にTreeを積んでいく</p>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="16" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="17" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -1441,7 +1521,7 @@
    top: 300px;
    text-align: center;
 }
-" data-heading-divider="1" class="slide" data-marpit-pagination="16" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section {
+" data-heading-divider="1" class="slide" data-marpit-pagination="17" data-marpit-pagination-total="29" style="--paginate:true;--class:slide;--theme:default;--style:section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -1500,7 +1580,7 @@
 ... | tri&gt; ¬a ¬b c = next key value (node key₁ value₁ left repl ) st
 </span></span></foreignObject></svg></code></pre>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="17" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="18" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -1539,7 +1619,7 @@
    top: 300px;
    text-align: center;
 }
-" data-heading-divider="1" class="slide" data-marpit-pagination="17" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section {
+" data-heading-divider="1" class="slide" data-marpit-pagination="18" data-marpit-pagination-total="29" style="--paginate:true;--class:slide;--theme:default;--style:section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -1593,7 +1673,7 @@
 <li>2つの木の1つのnodeが入れ替わっていることを示す</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="18" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="19" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -1632,7 +1712,7 @@
    top: 300px;
    text-align: center;
 }
-" data-heading-divider="1" class="slide" data-marpit-pagination="18" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section {
+" data-heading-divider="1" class="slide" data-marpit-pagination="19" data-marpit-pagination-total="29" style="--paginate:true;--class:slide;--theme:default;--style:section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -1693,7 +1773,7 @@
       → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄)) 
 </span></span></foreignObject></svg></code></pre>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="19" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="20" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -1732,7 +1812,7 @@
    top: 300px;
    text-align: center;
 }
-" data-heading-divider="1" class="slide" data-marpit-pagination="19" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section {
+" data-heading-divider="1" class="slide" data-marpit-pagination="20" data-marpit-pagination-total="29" style="--paginate:true;--class:slide;--theme:default;--style:section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -1789,7 +1869,7 @@
       → stackInvariant key tree₁ tree0 (tree₁ ∷ st)
 </span></span></foreignObject></svg></code></pre>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="20" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="21" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -1828,7 +1908,7 @@
    top: 300px;
    text-align: center;
 }
-" data-heading-divider="1" class="slide" data-marpit-pagination="20" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section {
+" data-heading-divider="1" class="slide" data-marpit-pagination="21" data-marpit-pagination-total="29" style="--paginate:true;--class:slide;--theme:default;--style:section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -1884,7 +1964,7 @@
           → replacedTree key value (node k v1 t1 t2) (node k v1 t t2) 
 </span></span></foreignObject></svg></code></pre>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="21" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="22" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -1923,7 +2003,7 @@
    top: 300px;
    text-align: center;
 }
-" data-heading-divider="1" class="slide" data-marpit-pagination="21" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section {
+" data-heading-divider="1" class="slide" data-marpit-pagination="22" data-marpit-pagination-total="29" style="--paginate:true;--class:slide;--theme:default;--style:section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -1976,7 +2056,7 @@
                 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )  → t ) → t
 </span></span></foreignObject></svg></code></pre>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="22" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="23" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -2015,7 +2095,7 @@
    top: 300px;
    text-align: center;
 }
-" data-heading-divider="1" class="slide" data-marpit-pagination="22" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section {
+" data-heading-divider="1" class="slide" data-marpit-pagination="23" data-marpit-pagination-total="29" style="--paginate:true;--class:slide;--theme:default;--style:section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -2070,7 +2150,7 @@
      ci : C key tree stack     -- data continuation
 </span></span></foreignObject></svg></code></pre>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="23" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="24" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -2109,7 +2189,7 @@
    top: 300px;
    text-align: center;
 }
-" data-heading-divider="1" class="slide" data-marpit-pagination="23" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section {
+" data-heading-divider="1" class="slide" data-marpit-pagination="24" data-marpit-pagination-total="29" style="--paginate:true;--class:slide;--theme:default;--style:section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -2165,7 +2245,7 @@
         → findPR key (node key₁ v1 tree tree₁) st C → key &gt; key₁  → C key tree₁ (tree₁ ∷ st)
 </span></span></foreignObject></svg></code></pre>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="24" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="25" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -2204,7 +2284,7 @@
    top: 300px;
    text-align: center;
 }
-" data-heading-divider="1" class="slide" data-marpit-pagination="24" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section {
+" data-heading-divider="1" class="slide" data-marpit-pagination="25" data-marpit-pagination-total="29" style="--paginate:true;--class:slide;--theme:default;--style:section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -2263,7 +2343,7 @@
      ci : C tree repl stack     -- data continuation
 </span></span></foreignObject></svg></code></pre>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="25" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="26" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -2302,7 +2382,7 @@
    top: 300px;
    text-align: center;
 }
-" data-heading-divider="1" class="slide" data-marpit-pagination="25" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section {
+" data-heading-divider="1" class="slide" data-marpit-pagination="26" data-marpit-pagination-total="29" style="--paginate:true;--class:slide;--theme:default;--style:section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -2361,7 +2441,7 @@
        $ λ t1 s1 P2 found? → insertTreeSpec0 t1 value (lemma6 t1 s1 found? P2) 
 </span></span></foreignObject></svg></code></pre>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="26" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="27" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -2400,7 +2480,7 @@
    top: 300px;
    text-align: center;
 }
-" data-heading-divider="1" class="slide" data-marpit-pagination="26" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section {
+" data-heading-divider="1" class="slide" data-marpit-pagination="27" data-marpit-pagination-total="29" style="--paginate:true;--class:slide;--theme:default;--style:section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -2446,7 +2526,7 @@
 <p>これにより木を用いるプログラムでの証明を記述できる<br />
 insert Tree や Find Node の停止性も証明されている</p>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="27" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="28" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -2485,7 +2565,7 @@
    top: 300px;
    text-align: center;
 }
-" data-heading-divider="1" class="slide" data-marpit-pagination="27" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section {
+" data-heading-divider="1" class="slide" data-marpit-pagination="28" data-marpit-pagination-total="29" style="--paginate:true;--class:slide;--theme:default;--style:section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -2542,10 +2622,8 @@
 <li>xv.6への適用</li>
 <li>モデル検査</li>
 </ul>
-<p>読めない間は待っている<br />
-tree</p>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="28" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="29" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -2584,7 +2662,7 @@
    top: 300px;
    text-align: center;
 }
-" data-heading-divider="1" class="slide" data-marpit-pagination="28" data-marpit-pagination-total="28" style="--paginate:true;--class:slide;--theme:default;--style:section {
+" data-heading-divider="1" class="slide" data-marpit-pagination="29" data-marpit-pagination-total="29" style="--paginate:true;--class:slide;--theme:default;--style:section {
   background-color: #FFFFFF;
   font-size: 28px;
   color: #4b4b4b;
@@ -2643,11 +2721,11 @@
 
 sample2 : (A : Set ) → (B : Set ) → Set
 sample2 a b = b
-```</p></div><div class="bespoke-marp-note" data-index="14" tabindex="0"><p>findは全部書いても大丈夫そう</p></div><div class="bespoke-marp-note" data-index="15" tabindex="0"><p>これは途中省略してよさそう</p></div><div class="bespoke-marp-note" data-index="17" tabindex="0"><p>t-leaf はコンストラクタ
+```</p></div><div class="bespoke-marp-note" data-index="15" tabindex="0"><p>findは全部書いても大丈夫そう</p></div><div class="bespoke-marp-note" data-index="16" tabindex="0"><p>これは途中省略してよさそう</p></div><div class="bespoke-marp-note" data-index="18" tabindex="0"><p>t-leaf はコンストラクタ
 
 
 コードの解説
 省略した方がたぶん絶対良い
 right と left なんかはほとんど対照的なので省略とかでよさそう
-あとは、木構造の仕様を満たすためにData型になっている説明があるとよさそう</p></div><div class="bespoke-marp-note" data-index="18" tabindex="0"><p>Keyの比較が入っているから</p></div><div class="bespoke-marp-note" data-index="27" tabindex="0"><p>英語版も欲しい</p></div><script>/*!! License: https://unpkg.com/@marp-team/marp-cli@1.5.0/lib/bespoke.js.LICENSE.txt */
+あとは、木構造の仕様を満たすためにData型になっている説明があるとよさそう</p></div><div class="bespoke-marp-note" data-index="19" tabindex="0"><p>Keyの比較が入っているから</p></div><div class="bespoke-marp-note" data-index="28" tabindex="0"><p>英語版も欲しい</p></div><script>/*!! License: https://unpkg.com/@marp-team/marp-cli@1.5.0/lib/bespoke.js.LICENSE.txt */
 !function(){"use strict";const e=document.body,t=(...e)=>history.replaceState(...e),n="presenter",r="next",o=["",n,r],a="data-bespoke-marp-",i=(e,{protocol:t,host:n,pathname:r,hash:o}=location)=>{const a=e.toString();return`${t}//${n}${r}${a?"?":""}${a}${o}`},s=()=>e.dataset.bespokeView,l=e=>new URLSearchParams(location.search).get(e),c=(e,n={})=>{var r;const o={location,setter:t,...n},a=new URLSearchParams(o.location.search);for(const t of Object.keys(e)){const n=e[t];"string"==typeof n?a.set(t,n):a.delete(t)}try{o.setter({...null!==(r=window.history.state)&&void 0!==r?r:{}},"",i(a,o.location))}catch(e){console.error(e)}},d=(()=>{const e="bespoke-marp";try{return localStorage.setItem(e,e),localStorage.removeItem(e),!0}catch(e){return!1}})(),f=e=>{try{return localStorage.getItem(e)}catch(e){return null}},u=(e,t)=>{try{return localStorage.setItem(e,t),!0}catch(e){return!1}},m=e=>{try{return localStorage.removeItem(e),!0}catch(e){return!1}},g=(e,t)=>{const n="aria-hidden";t?e.setAttribute(n,"true"):e.removeAttribute(n)},p=e=>{e.parent.classList.add("bespoke-marp-parent"),e.slides.forEach((e=>e.classList.add("bespoke-marp-slide"))),e.on("activate",(t=>{const n="bespoke-marp-active",r=t.slide,o=r.classList,a=!o.contains(n);if(e.slides.forEach((e=>{e.classList.remove(n),g(e,!0)})),o.add(n),g(r,!1),a){const e=`${n}-ready`;o.add(e),document.body.clientHeight,o.remove(e)}}))},v=e=>{let t=0,n=0;Object.defineProperty(e,"fragments",{enumerable:!0,value:e.slides.map((e=>[null,...e.querySelectorAll("[data-marpit-fragment]")]))});const r=r=>void 0!==e.fragments[t][n+r],o=(r,o)=>{t=r,n=o,e.fragments.forEach(((e,t)=>{e.forEach(((e,n)=>{if(null==e)return;const i=t<r||t===r&&n<=o;e.setAttribute(`${a}fragment`,(i?"":"in")+"active");const s=`${a}current-fragment`;t===r&&n===o?e.setAttribute(s,"current"):e.removeAttribute(s)}))})),e.fragmentIndex=o;const i={slide:e.slides[r],index:r,fragments:e.fragments[r],fragmentIndex:o};e.fire("fragment",i)};e.on("next",(({fragment:a=!0})=>{if(a){if(r(1))return o(t,n+1),!1;const a=t+1;e.fragments[a]&&o(a,0)}else{const r=e.fragments[t].length;if(n+1<r)return o(t,r-1),!1;const a=e.fragments[t+1];a&&o(t+1,a.length-1)}})),e.on("prev",(({fragment:a=!0})=>{if(r(-1)&&a)return o(t,n-1),!1;const i=t-1;e.fragments[i]&&o(i,e.fragments[i].length-1)})),e.on("slide",(({index:t,fragment:n})=>{let r=0;if(void 0!==n){const o=e.fragments[t];if(o){const{length:e}=o;r=-1===n?e-1:Math.min(Math.max(n,0),e-1)}}o(t,r)})),o(0,0)},h=document,y=()=>!(!h.fullscreenEnabled&&!h.webkitFullscreenEnabled),x=()=>!(!h.fullscreenElement&&!h.webkitFullscreenElement),w=e=>{e.fullscreen=()=>{y()&&(async()=>{return x()?null===(e=h.exitFullscreen||h.webkitExitFullscreen)||void 0===e?void 0:e.call(h):((e=h.body)=>{var t;return null===(t=e.requestFullscreen||e.webkitRequestFullscreen)||void 0===t?void 0:t.call(e)})();var e})()},document.addEventListener("keydown",(t=>{"f"!==t.key&&"F11"!==t.key||t.altKey||t.ctrlKey||t.metaKey||!y()||(e.fullscreen(),t.preventDefault())}))},b="bespoke-marp-inactive",k=(e=2e3)=>({parent:t,fire:n})=>{const r=t.classList,o=e=>n(`marp-${e?"":"in"}active`);let a;const i=()=>{a&&clearTimeout(a),a=setTimeout((()=>{r.add(b),o()}),e),r.contains(b)&&(r.remove(b),o(!0))};for(const e of["mousedown","mousemove","touchend"])document.addEventListener(e,i);setTimeout(i,0)},E=["AUDIO","BUTTON","INPUT","SELECT","TEXTAREA","VIDEO"],L=e=>{e.parent.addEventListener("keydown",(e=>{if(!e.target)return;const t=e.target;(E.includes(t.nodeName)||"true"===t.contentEditable)&&e.stopPropagation()}))},$=e=>{window.addEventListener("load",(()=>{for(const t of e.slides){const e=t.querySelector("[data-marp-fitting]")?"":"hideable";t.setAttribute(`${a}load`,e)}}))},P=({interval:e=250}={})=>t=>{document.addEventListener("keydown",(e=>{if(" "===e.key&&e.shiftKey)t.prev();else if("ArrowLeft"===e.key||"ArrowUp"===e.key||"PageUp"===e.key)t.prev({fragment:!e.shiftKey});else if(" "!==e.key||e.shiftKey)if("ArrowRight"===e.key||"ArrowDown"===e.key||"PageDown"===e.key)t.next({fragment:!e.shiftKey});else if("End"===e.key)t.slide(t.slides.length-1,{fragment:-1});else{if("Home"!==e.key)return;t.slide(0)}else t.next();e.preventDefault()}));let n,r,o=0;t.parent.addEventListener("wheel",(a=>{let i=!1;const s=(e,t)=>{e&&(i=i||((e,t)=>((e,t)=>{const n="X"===t?"Width":"Height";return e[`client${n}`]<e[`scroll${n}`]})(e,t)&&((e,t)=>{const{overflow:n}=e,r=e[`overflow${t}`];return"auto"===n||"scroll"===n||"auto"===r||"scroll"===r})(getComputedStyle(e),t))(e,t)),(null==e?void 0:e.parentElement)&&s(e.parentElement,t)};if(0!==a.deltaX&&s(a.target,"X"),0!==a.deltaY&&s(a.target,"Y"),i)return;a.preventDefault();const l=Math.sqrt(a.deltaX**2+a.deltaY**2);if(void 0!==a.wheelDelta){if(void 0===a.webkitForce&&Math.abs(a.wheelDelta)<40)return;if(a.deltaMode===a.DOM_DELTA_PIXEL&&l<4)return}else if(a.deltaMode===a.DOM_DELTA_PIXEL&&l<12)return;r&&clearTimeout(r),r=setTimeout((()=>{n=0}),e);const c=Date.now()-o<e,d=l<=n;if(n=l,c||d)return;let f;(a.deltaX>0||a.deltaY>0)&&(f="next"),(a.deltaX<0||a.deltaY<0)&&(f="prev"),f&&(t[f](),o=Date.now())}))},S=(e=".bespoke-marp-osc")=>{const t=document.querySelector(e);if(!t)return()=>{};const n=(e,n)=>{t.querySelectorAll(`[${a}osc=${JSON.stringify(e)}]`).forEach(n)};return y()||n("fullscreen",(e=>e.style.display="none")),d||n("presenter",(e=>{e.disabled=!0,e.title="Presenter view is disabled due to restricted localStorage."})),e=>{t.addEventListener("click",(t=>{if(t.target instanceof HTMLElement){const{bespokeMarpOsc:n}=t.target.dataset;n&&t.target.blur();const r={fragment:!t.shiftKey};"next"===n?e.next(r):"prev"===n?e.prev(r):"fullscreen"===n?null==e||e.fullscreen():"presenter"===n&&e.openPresenterView()}})),e.parent.appendChild(t),e.on("activate",(({index:t})=>{n("page",(n=>n.textContent=`Page ${t+1} of ${e.slides.length}`))})),e.on("fragment",(({index:t,fragments:r,fragmentIndex:o})=>{n("prev",(e=>e.disabled=0===t&&0===o)),n("next",(n=>n.disabled=t===e.slides.length-1&&o===r.length-1))})),e.on("marp-active",(()=>g(t,!1))),e.on("marp-inactive",(()=>g(t,!0))),y()&&(e=>{for(const t of["","webkit"])h.addEventListener(t+"fullscreenchange",e)})((()=>n("fullscreen",(e=>e.classList.toggle("exit",y()&&x())))))}},I=e=>{window.addEventListener("message",(t=>{if(t.origin!==window.origin)return;const[n,r]=t.data.split(":");if("navigate"===n){const[t,n]=r.split(",");let o=Number.parseInt(t,10),a=Number.parseInt(n,10)+1;a>=e.fragments[o].length&&(o+=1,a=0),e.slide(o,{fragment:a})}}))};var T=["area","base","br","col","command","embed","hr","img","input","keygen","link","meta","param","source","track","wbr"];let A=e=>String(e).replace(/[&<>"']/g,(e=>`&${C[e]};`)),C={"&":"amp","<":"lt",">":"gt",'"':"quot","'":"apos"},N="dangerouslySetInnerHTML",K={className:"class",htmlFor:"for"},O={};function D(e,t){let n=[],r="";t=t||{};for(let e=arguments.length;e-- >2;)n.push(arguments[e]);if("function"==typeof e)return t.children=n.reverse(),e(t);if(e){if(r+="<"+e,t)for(let e in t)!1!==t[e]&&null!=t[e]&&e!==N&&(r+=` ${K[e]?K[e]:A(e)}="${A(t[e])}"`);r+=">"}if(-1===T.indexOf(e)){if(t[N])r+=t[N].__html;else for(;n.length;){let e=n.pop();if(e)if(e.pop)for(let t=e.length;t--;)n.push(e[t]);else r+=!0===O[e]?e:A(e)}r+=e?`</${e}>`:""}return O[r]=!0,r}const M=({children:e})=>D(null,null,...e),q="bespoke-marp-presenter-",_={container:`${q}container`,next:`${q}next`,nextContainer:`${q}next-container`,noteContainer:`${q}note-container`,infoContainer:`${q}info-container`,infoPage:`${q}info-page`,infoPageText:`${q}info-page-text`,infoPagePrev:`${q}info-page-prev`,infoPageNext:`${q}info-page-next`,infoTime:`${q}info-time`,infoTimer:`${q}info-timer`},U=e=>{const{title:t}=document;document.title="[Presenter view]"+(t?` - ${t}`:"");const n={},r=e=>(n[e]=n[e]||document.querySelector(`.${e}`),n[e]);document.body.appendChild((e=>{const t=document.createElement("div");return t.className=_.container,t.appendChild(e),t.insertAdjacentHTML("beforeend",D(M,null,D("div",{class:_.nextContainer},D("iframe",{class:_.next,src:"?view=next"})),D("div",{class:_.noteContainer}),D("div",{class:_.infoContainer},D("div",{class:_.infoPage},D("button",{class:_.infoPagePrev,tabindex:"-1",title:"Previous"},"Previous"),D("span",{class:_.infoPageText}),D("button",{class:_.infoPageNext,tabindex:"-1",title:"Next"},"Next")),D("time",{class:_.infoTime,title:"Current time"}),D("div",{class:_.infoTimer})))),t})(e.parent)),(e=>{r(_.nextContainer).addEventListener("click",(()=>e.next()));const t=r(_.next),n=(o=t,(e,t)=>{var n;return null===(n=o.contentWindow)||void 0===n?void 0:n.postMessage(`navigate:${e},${t}`,"null"===window.origin?"*":window.origin)});var o;t.addEventListener("load",(()=>{r(_.nextContainer).classList.add("active"),n(e.slide(),e.fragmentIndex),e.on("fragment",(({index:e,fragmentIndex:t})=>n(e,t)))}));const a=document.querySelectorAll(".bespoke-marp-note");a.forEach((e=>{e.addEventListener("keydown",(e=>e.stopPropagation())),r(_.noteContainer).appendChild(e)})),e.on("activate",(()=>a.forEach((t=>t.classList.toggle("active",t.dataset.index==e.slide()))))),e.on("activate",(({index:t})=>{r(_.infoPageText).textContent=`${t+1} / ${e.slides.length}`}));const i=r(_.infoPagePrev),s=r(_.infoPageNext);i.addEventListener("click",(t=>{i.blur(),e.prev({fragment:!t.shiftKey})})),s.addEventListener("click",(t=>{s.blur(),e.next({fragment:!t.shiftKey})})),e.on("fragment",(({index:t,fragments:n,fragmentIndex:r})=>{i.disabled=0===t&&0===r,s.disabled=t===e.slides.length-1&&r===n.length-1}));const l=()=>r(_.infoTime).textContent=(new Date).toLocaleTimeString();l(),setInterval(l,250)})(e)},V=e=>{if(!(e=>e.syncKey&&"string"==typeof e.syncKey)(e))throw new Error("The current instance of Bespoke.js is invalid for Marp bespoke presenter plugin.");Object.defineProperties(e,{openPresenterView:{enumerable:!0,value:X},presenterUrl:{enumerable:!0,get:F}}),d&&document.addEventListener("keydown",(t=>{"p"!==t.key||t.altKey||t.ctrlKey||t.metaKey||(t.preventDefault(),e.openPresenterView())}))};function X(){const{max:e,floor:t}=Math,n=e(t(.85*window.innerWidth),640),r=e(t(.85*window.innerHeight),360);return window.open(this.presenterUrl,q+this.syncKey,`width=${n},height=${r},menubar=no,toolbar=no`)}function F(){const e=new URLSearchParams(location.search);return e.set("view","presenter"),e.set("sync",this.syncKey),i(e)}const B=e=>{const t=s();return t===r&&e.appendChild(document.createElement("span")),{"":V,[n]:U,[r]:I}[t]},R=e=>{e.on("activate",(t=>{document.querySelectorAll(".bespoke-progress-parent > .bespoke-progress-bar").forEach((n=>{n.style.flexBasis=100*t.index/(e.slides.length-1)+"%"}))}))},j=e=>{const t=Number.parseInt(e,10);return Number.isNaN(t)?null:t},H=(e={})=>{const t={history:!0,...e};return e=>{let n=!0;const r=e=>{const t=n;try{return n=!0,e()}finally{n=t}},o=(t={fragment:!0})=>{((t,n)=>{const{min:r,max:o}=Math,{fragments:a,slides:i}=e,s=o(0,r(t,i.length-1)),l=o(0,r(n||0,a[s].length-1));s===e.slide()&&l===e.fragmentIndex||e.slide(s,{fragment:l})})((j(location.hash.slice(1))||1)-1,t.fragment?j(l("f")||""):null)};e.on("fragment",(({index:e,fragmentIndex:r})=>{n||c({f:0===r||r.toString()},{location:{...location,hash:`#${e+1}`},setter:(...e)=>t.history?history.pushState(...e):history.replaceState(...e)})})),setTimeout((()=>{o(),window.addEventListener("hashchange",(()=>r((()=>{o({fragment:!1}),c({f:void 0})})))),window.addEventListener("popstate",(()=>{n||r((()=>o()))})),n=!1}),0)}},Y=(e={})=>{var n;const r=e.key||(null===(n=window.history.state)||void 0===n?void 0:n.marpBespokeSyncKey)||Math.random().toString(36).slice(2),o=`bespoke-marp-sync-${r}`;var a;a={marpBespokeSyncKey:r},c({},{setter:(e,...n)=>t({...e,...a},...n)});const i=()=>{const e=f(o);return e?JSON.parse(e):Object.create(null)},s=e=>{const t=i(),n={...t,...e(t)};return u(o,JSON.stringify(n)),n},l=()=>{window.removeEventListener("pageshow",l),s((e=>({reference:(e.reference||0)+1})))};return e=>{l(),Object.defineProperty(e,"syncKey",{value:r,enumerable:!0});let t=!0;setTimeout((()=>{e.on("fragment",(e=>{t&&s((()=>({index:e.index,fragmentIndex:e.fragmentIndex})))}))}),0),window.addEventListener("storage",(n=>{if(n.key===o&&n.oldValue&&n.newValue){const r=JSON.parse(n.oldValue),o=JSON.parse(n.newValue);if(r.index!==o.index||r.fragmentIndex!==o.fragmentIndex)try{t=!1,e.slide(o.index,{fragment:o.fragmentIndex})}finally{t=!0}}}));const n=()=>{const{reference:e}=i();void 0===e||e<=1?m(o):s((()=>({reference:e-1})))};window.addEventListener("pagehide",(e=>{e.persisted&&window.addEventListener("pageshow",l),n()})),e.on("destroy",n)}},{PI:J,abs:W,sqrt:z,atan2:G}=Math,Q={passive:!0},Z=({slope:e=-.7,swipeThreshold:t=30}={})=>n=>{let r;const o=n.parent,a=e=>{const t=o.getBoundingClientRect();return{x:e.pageX-(t.left+t.right)/2,y:e.pageY-(t.top+t.bottom)/2}};o.addEventListener("touchstart",(({touches:e})=>{r=1===e.length?a(e[0]):void 0}),Q),o.addEventListener("touchmove",(e=>{if(r)if(1===e.touches.length){e.preventDefault();const t=a(e.touches[0]),n=t.x-r.x,o=t.y-r.y;r.delta=z(W(n)**2+W(o)**2),r.radian=G(n,o)}else r=void 0})),o.addEventListener("touchend",(o=>{if(r){if(r.delta&&r.delta>=t&&r.radian){const t=(r.radian-e+J)%(2*J)-J;n[t<0?"next":"prev"](),o.stopPropagation()}r=void 0}}),Q)},ee="_tA",te=e=>{const t=document.documentTransition;if(!t)return;let n;e._tP=!1;const r=(n,{back:r,cond:o})=>a=>{const i=e.slides[e.slide()].querySelector("section[data-transition]");if(!i)return!0;const s=document.querySelector(".bespoke-marp-osc"),l=s?[s]:void 0;if(e._tP){if(a._tA){e._tP=!1;try{t.start({sharedElements:l}).catch((()=>{}))}catch(e){}return!0}}else{if(!o(a))return!0;e._tP=t.prepare({rootTransition:a.back||r?i.dataset.transitionBack:i.dataset.transition,sharedElements:l}).then((()=>n(a))).catch((()=>n(a)))}return!1};e.on("prev",r((t=>e.prev({...t,[ee]:!0})),{back:!0,cond:e=>{var t;return e.index>0&&!((null===(t=e.fragment)||void 0===t||t)&&n.fragmentIndex>0)}})),e.on("next",r((t=>e.next({...t,[ee]:!0})),{cond:t=>t.index+1<e.slides.length&&!(n.fragmentIndex+1<n.fragments.length)})),setTimeout((()=>{e.on("slide",r((t=>e.slide(t.index,{...t,[ee]:!0})),{cond:t=>{const n=e.slide();return t.index!==n&&(t.back=t.index<n,!0)}}))}),0),e.on("fragment",(e=>{n=e}))};let ne;const re=()=>(void 0===ne&&(ne="wakeLock"in navigator&&navigator.wakeLock),ne),oe=async()=>{const e=re();if(e)try{return await e.request("screen")}catch(e){console.warn(e)}return null},ae=async()=>{if(!re())return;let e;const t=()=>{e&&"visible"===document.visibilityState&&oe()};for(const e of["visibilitychange","fullscreenchange"])document.addEventListener(e,t);return e=await oe(),e};((t=document.getElementById("p"))=>{(()=>{const t=l("view");e.dataset.bespokeView=t===r||t===n?t:""})();const a=(e=>{const t=l(e);return c({[e]:void 0}),t})("sync")||void 0;var i,d,f,u,m,g,h,y,x,b,E,I;i=t,d=((...e)=>{const t=o.findIndex((e=>s()===e));return e.map((([e,n])=>e[t]&&n)).filter((e=>e))})([[1,1,0],Y({key:a})],[[1,1,1],B(t)],[[1,1,0],L],[[1,1,1],p],[[1,0,0],k()],[[1,1,1],$],[[1,1,1],H({history:!1})],[[1,1,0],P()],[[1,1,0],w],[[1,0,0],R],[[1,1,0],Z()],[[1,0,0],S()],[[1,0,0],te],[[1,1,1],v],[[1,1,0],ae]),u=1===(i.parent||i).nodeType?i.parent||i:document.querySelector(i.parent||i),m=[].filter.call("string"==typeof i.slides?u.querySelectorAll(i.slides):i.slides||u.children,(function(e){return"SCRIPT"!==e.nodeName})),g={},h=function(e,t){return(t=t||{}).index=m.indexOf(e),t.slide=e,t},b=function(e,t){m[e]&&(f&&x("deactivate",h(f,t)),f=m[e],x("activate",h(f,t)))},E=function(e,t){var n=m.indexOf(f)+e;x(e>0?"next":"prev",h(f,t))&&b(n,t)},I={off:y=function(e,t){g[e]=(g[e]||[]).filter((function(e){return e!==t}))},on:function(e,t){return(g[e]||(g[e]=[])).push(t),y.bind(null,e,t)},fire:x=function(e,t){return(g[e]||[]).reduce((function(e,n){return e&&!1!==n(t)}),!0)},slide:function(e,t){if(!arguments.length)return m.indexOf(f);x("slide",h(m[e],t))&&b(e,t)},next:E.bind(null,1),prev:E.bind(null,-1),parent:u,slides:m,destroy:function(e){x("destroy",h(f,e)),g={}}},(d||[]).forEach((function(e){e(I)})),f||b(0)})()}();</script></body></html>
\ No newline at end of file
--- a/slide/note.md	Fri Jan 07 00:58:07 2022 +0900
+++ b/slide/note.md	Sat Jan 08 09:53:19 2022 +0900
@@ -17,7 +17,7 @@
 もそのまま読む
 
 # Agda の基本
-Agda の基本となる型の１つである Data 型について説明します
+Agda の基本となる型の１つである Record 型について説明します
 
 record Env とあるところで Env という Record 型を定義  
 することを示しています
@@ -25,7 +25,7 @@
 そしてその中にvarnとvariがあり、その型が自然数であることを定義しています
 
 次に、記述する際の導入が以下のようになり
-varxに0を、variに1を定義しています
+varnに0を、variに1を定義しています
 
 導入後は変数 スペース record名でその中身にアクセスできます
 
@@ -63,7 +63,7 @@
 画像はよなおせ
 
 # Hoare logic
-プログラム が事前条件 P に関して停止し、停止後には必ず事後条件 Q が成り立つならば、プログラム S は、事前条件 P と事後条件 Q とに関して正当（correct）であるという
+コマンド が事前条件 P に関して停止し、停止後には必ず事後条件 Q が成り立つならば、プログラム S は、事前条件 P と事後条件 Q とに関して正当（correct）であるという
 
 簡単な例としてGears Agdaにてwhile loopを検証します
 
@@ -88,15 +88,14 @@
 
 # post condition 
 先ほど実装したノーマルレベルなwhile loopに対して
-事前条件となるPre / Post Condition を追加した実装をします
+条件となるPre / Post Condition を追加した実装をします
 
 そのまえにterminatingが付いていると停止性の証明をしたことにはならないので～
-
+loopを分割した実装を行います
 
 このconditionはループしたい回数は
 これからループする回数とループした回数の和と等しいというものです
 
-exitのPostConditionもつけるべきだな…
 
 # loopの接続
 loopが前のページのWhile LoopSeg だな
@@ -120,3 +119,46 @@
 そのまま読むよ
 
 Condition 
+
+# BTの実装
+これはノーマルレベルの BinaryTree の find 実装になります
+
+これが行っているのはkeyと等しいnodeを見つける
+
+なので入力されているtreeのkeyと比較し
+等しかった場合は終了
+
+入力のkeyの方が小さい場合は
+左のtreeを次のfindの対象とし
+今回対象のtreeをstackに積む
+
+# replace tree
+
+先ほどと同じように入力のkeyと比較し
+今度は木を再構成するので
+
+# Invariant
+Binary Treeの証明には３つのInvariant（不変条件）をもちいる
+あとはそのまま読む
+
+# find hoare condition
+
+最初のtreeInvariant tree ∧ stackInvariantが
+pre conditionで、
+treeInvariant と stackInvariantを満たしていることを証明する
+
+nextには次のInvariant と現在の木の深さが最大ではないことを示しています
+
+exitなのでfindを終了する際には
+valueを見つけられなかったことを表す
+tree1がleefか
+
+valueを見つけたことを表す
+tree1のkeyが入力のkeyといっちしていることを表します
+
+# カンペ
+synchronized queue
+- 読めない間は待っている
+concurrent tree
+- 
+
--- a/slide/slide.md	Fri Jan 07 00:58:07 2022 +0900
+++ b/slide/slide.md	Sat Jan 08 09:53:19 2022 +0900
@@ -154,9 +154,8 @@
 - Contextによる並列実行
 - monadに相当するData構造
 
-# 
-<!-- class: fig_cg  -->
-![height:700px](meta_cg_dg.svg)
+# Normal level と Meta Level の対応
+![height:400px](meta-cg-dg.jpg)
 
 # Gears Agda と Hoare Logic
 <!-- class: slide -->
@@ -447,8 +446,7 @@
 - xv.6への適用
 - モデル検査
 
-読めない間は待っている
-tree
+
 
 # まとめ
 - Gears Agda にて Binary Tree を検証することができた