Mercurial > hg > Papers > 2018 > ryokka-sigos

--- a/Paper/auto/sigos.el	Mon Apr 23 21:44:32 2018 +0900
+++ b/Paper/auto/sigos.el	Sat May 19 19:14:19 2018 +0900
@@ -14,13 +14,13 @@
    (add-to-list 'LaTeX-verbatim-environments-local "Verbatim*")
    (add-to-list 'LaTeX-verbatim-environments-local "Verbatim")
    (add-to-list 'LaTeX-verbatim-environments-local "lstlisting")
-   (add-to-list 'LaTeX-verbatim-macros-with-braces-local "lstinline")
    (add-to-list 'LaTeX-verbatim-macros-with-braces-local "url")
    (add-to-list 'LaTeX-verbatim-macros-with-braces-local "path")
+   (add-to-list 'LaTeX-verbatim-macros-with-braces-local "lstinline")
+   (add-to-list 'LaTeX-verbatim-macros-with-delims-local "url")
+   (add-to-list 'LaTeX-verbatim-macros-with-delims-local "path")
    (add-to-list 'LaTeX-verbatim-macros-with-delims-local "Verb")
    (add-to-list 'LaTeX-verbatim-macros-with-delims-local "lstinline")
-   (add-to-list 'LaTeX-verbatim-macros-with-delims-local "url")
-   (add-to-list 'LaTeX-verbatim-macros-with-delims-local "path")
    (TeX-run-style-hooks
     "latex2e"
     "ipsjpapers"
--- a/Paper/sigos.bib	Mon Apr 23 21:44:32 2018 +0900
+++ b/Paper/sigos.bib	Sat May 19 19:14:19 2018 +0900
@@ -44,7 +44,7 @@
 @misc{agda,
     title = {The Agda wiki},
     howpublished = {\url{http://wiki.portal.chalmers.se/agda/pmwiki.php}},
-    note = {Accessed: 2018/2/9(Fri)}
+    note = {Accessed: 2018/4/23(Fri)}
 }


@@ -68,9 +68,9 @@
 @Comment % \\\verb|http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf|

 @misc{agda-documentation,
-    title = {Welcome to Agda’s documentation! — Agda 2.6.0 documentation},
-    howpublished = {\url{http://agda.readthedocs.io/en/latest/index.html}},
-    note = {Accessed: 2018/2/9(Fri)}
+    title = {Welcome to Agda’s documentation! — Agda latest documentation},
+    howpublished = {\url{http://agda.readthedocs.io/en/latest/}},
+    note = {Accessed: 2018/4/23(Mon)}
 }

 @book{Stump:2016:VFP:2841316,
Binary file Paper/sigos.pdf has changed
--- a/Paper/sigos.tex	Mon Apr 23 21:44:32 2018 +0900
+++ b/Paper/sigos.tex	Sat May 19 19:14:19 2018 +0900
@@ -63,7 +63,7 @@

 % 和文表題
 \title{GearsOS の Agda による記述と検証}
-% 英文$\lambda$式表題
+% 英文$\lambda$@$式表題
 \etitle{}

 % 所属ラベルの定義
@@ -208,9 +208,11 @@
 Agda ではこの型に対応する$\lambda$項を与えると証明が完了したことになる。

 \begin{lstlisting}[caption=pushとpop,label=push-pop]
-   push->pop : {l : Level } {D : Set l} (x : D ) (s : SingleLinkedStack D ) ->
-       pushStack ( stackInSomeState s )  x (\s -> popStack s ( \s3 x1 -> (Just x
-       ≡ x1 )  ))
+push->pop : {l : Level} {D : Set l} (x : D )
+        (s : SingleLinkedStack D) ->
+        pushStack (stackInSomeState s)
+        x (\s -> popStack s
+        ( \s3 x1 -> (Just x ≡ x1)))
 \end{lstlisting}

 このように、CodeGear を Agda で記述し、継続部分に証明すべき性質を Agda で記述する。
@@ -247,7 +249,10 @@
 $\lambda$式では\verb+\+の他に$\lambda$で表記することもできる。

 \begin{lstlisting}[caption=pushStack の関数定義,label=push-stack-func]
-  pushStack d next = push (stackMethods ) (stack ) d (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } ))
+  pushStack d next = push (stackMethods)
+            (stack) d (\s1 -> next
+            (record {stack = s1
+            ; stackMethods = stackMethods}))
 \end{lstlisting}

 ここで書かれている \verb+record+ は C における構造体に相当するレコード型というデー
@@ -292,8 +297,8 @@

 \begin{lstlisting}[caption=パターンマッチの例,label=pattern-match]
 popSingleLinkedStack stack cs with (top stack)
-...                                | Nothing = cs stack  Nothing
-...                                | Just d  = cs stack1 (Just data1)
+...    | Nothing = cs stack  Nothing
+...    | Just d  = cs stack1 (Just data1)
   where
     data1  = datum d
     stack1 = record { top = (next d) }
@@ -308,7 +313,11 @@
 たものと同じになるという論理式を型に書き、証明を行なった。

 \begin{lstlisting}[caption=pushとpopを使った証明,label=push-pop]
-push->pop : {l : Level } {D : Set l} (x : D ) (s : SingleLinkedStack D ) -> pushStack ( stackInSomeState s )  x ( \s1 -> popStack s1 ( \s3 x1 -> (Just x ≡ x1)))
+push->pop : {l : Level} {D : Set l}
+        (x : D) (s : SingleLinkedStack D)
+        -> pushStack (stackInSomeState s) x
+        (\s1 -> popStack s1 (\s3 x1
+        -> (Just x ≡ x1)))
 push->pop {l} {D} x s = refl
 \end{lstlisting}

@@ -453,9 +462,10 @@
 これにより、抽象化した Stack に対して push 、 pop を行うと push したものと同じも
 のを受け取れることが証明できた。

- \lstinputlisting[label=agda-in-some-state, caption=抽象的なStackの定義とpush$->$push$->$pop2 の証明]{src/AgdaStackSomeState.agda.replaced}
+\lstinputlisting[label=agda-in-some-state, caption=抽象的なStackの定義とpush$\rightarrow$push$\rightarrow$pop2 の証明]{src/AgdaStackSomeState.agda.replaced}

-今回の研究では、Agda を用いて GearsOS 上のモジュール化である interface の記述に
+\section{まとめ}
+本論文では、Agda を用いて GearsOS 上のモジュール化である interface の記述に
 ついて検討、実装した。また、継続を用いた記述をすることで計算途中のデータの形など
 を確認することができることが分かった。その他に、interface の記述を通しての証明が行えることが分かった。
--- a/Paper/src/AgdaStackSomeState.agda	Mon Apr 23 21:44:32 2018 +0900
+++ b/Paper/src/AgdaStackSomeState.agda	Sat May 19 19:14:19 2018 +0900
@@ -1,5 +1,5 @@
-stackInSomeState : {l m : Level } {D : Set l} {t : Set m } (s : SingleLinkedStack D ) -> Stack {l} {m} D {t}  ( SingleLinkedStack  D )
+stackInSomeState : {l m : Level} {D : Set l} {t : Set m} (s : SingleLinkedStack D) -> Stack {l} {m} D {t}  ( SingleLinkedStack  D)
 stackInSomeState s =  record { stack = s ; stackMethods = singleLinkedStackSpec }

-push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) -> pushStack ( stackInSomeState s )  x ( \s1 -> pushStack s1 y ( \s2 -> pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
-push->push->pop2 {l} {D} x y s = record { pi1 = refl ; pi2 = refl }
+push->push->pop2 : {l : Level} {D : Set l} (x y : D) (s : SingleLinkedStack D) -> pushStack (stackInSomeState s) x (\s1 -> pushStack s1 y (\s2 -> pop2Stack s2 (\s3 y1 x1 -> (Just x ≡ x1) ∧ (Just y ≡ y1))))
+push->push->pop2 {l} {D} x y s = record {pi1 = refl ; pi2 = refl}
--- a/Slide/fig/cbc-hoare.xbb	Mon Apr 23 21:44:32 2018 +0900
+++ b/Slide/fig/cbc-hoare.xbb	Sat May 19 19:14:19 2018 +0900
@@ -1,8 +1,8 @@
-%%Title: cbc-hoare.pdf
-%%Creator: extractbb 20160307
+%%Title: fig/cbc-hoare.pdf
+%%Creator: extractbb 20180217
 %%BoundingBox: 0 0 580 175
 %%HiResBoundingBox: 0.000000 0.000000 580.000000 175.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Wed Feb 21 01:38:18 2018
+%%CreationDate: Tue May 15 18:15:06 2018
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Slide/fig/fanctionLoop.svg	Sat May 19 19:14:19 2018 +0900
@@ -0,0 +1,150 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<svg xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" width="647pt" height="168pt" viewBox="0 0 647 168" version="1.1">
+<defs>
+<g>
+<symbol overflow="visible" id="glyph0-0">
+<path style="stroke:none;" d="M 6.546875 -10.65625 L 1.625 -10.65625 L 1.625 -0.75 L 6.546875 -0.75 Z M 7.359375 -11.390625 L 7.359375 -0.015625 L 0.8125 -0.015625 L 0.8125 -11.390625 Z M 7.359375 -11.390625 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-1">
+<path style="stroke:none;" d="M 5.84375 0 L 7.203125 0 L 7.203125 -8.265625 L 5.84375 -8.265625 Z M 5.84375 -9.765625 L 7.203125 -9.765625 L 7.203125 -11.421875 L 5.84375 -11.421875 Z M 1.578125 -7.078125 L 1.578125 0 L 2.9375 0 L 2.9375 -7.078125 L 4.546875 -7.078125 L 4.546875 -8.265625 L 2.9375 -8.265625 L 2.9375 -9.421875 C 2.9375 -9.785156 3.023438 -10.03125 3.203125 -10.15625 C 3.390625 -10.289062 3.648438 -10.359375 3.984375 -10.359375 C 4.097656 -10.359375 4.222656 -10.347656 4.359375 -10.328125 C 4.503906 -10.304688 4.632812 -10.273438 4.75 -10.234375 L 4.75 -11.421875 C 4.625 -11.460938 4.476562 -11.492188 4.3125 -11.515625 C 4.144531 -11.535156 4 -11.546875 3.875 -11.546875 C 3.125 -11.546875 2.550781 -11.375 2.15625 -11.03125 C 1.769531 -10.6875 1.578125 -10.175781 1.578125 -9.5 L 1.578125 -8.265625 L 0.1875 -8.265625 L 0.1875 -7.078125 Z M 1.578125 -7.078125 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-2">
+<path style="stroke:none;" d="M 1.03125 -8.265625 L 1.03125 0 L 2.390625 0 L 2.390625 -4.671875 C 2.390625 -5.046875 2.4375 -5.390625 2.53125 -5.703125 C 2.632812 -6.015625 2.785156 -6.285156 2.984375 -6.515625 C 3.191406 -6.753906 3.445312 -6.9375 3.75 -7.0625 C 4.050781 -7.195312 4.410156 -7.265625 4.828125 -7.265625 C 5.347656 -7.265625 5.757812 -7.113281 6.0625 -6.8125 C 6.363281 -6.519531 6.515625 -6.113281 6.515625 -5.59375 L 6.515625 0 L 7.875 0 L 7.875 -5.4375 C 7.875 -5.882812 7.828125 -6.289062 7.734375 -6.65625 C 7.640625 -7.03125 7.476562 -7.347656 7.25 -7.609375 C 7.03125 -7.878906 6.738281 -8.085938 6.375 -8.234375 C 6.019531 -8.390625 5.570312 -8.46875 5.03125 -8.46875 C 3.800781 -8.46875 2.90625 -7.960938 2.34375 -6.953125 L 2.296875 -6.953125 L 2.296875 -8.265625 Z M 1.03125 -8.265625 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-3">
+<path style="stroke:none;" d="M 2.015625 -4.0625 C 2.015625 -4.46875 2.054688 -4.863281 2.140625 -5.25 C 2.222656 -5.632812 2.359375 -5.972656 2.546875 -6.265625 C 2.742188 -6.566406 3.003906 -6.804688 3.328125 -6.984375 C 3.648438 -7.171875 4.039062 -7.265625 4.5 -7.265625 C 4.96875 -7.265625 5.363281 -7.175781 5.6875 -7 C 6.019531 -6.820312 6.289062 -6.585938 6.5 -6.296875 C 6.707031 -6.015625 6.859375 -5.679688 6.953125 -5.296875 C 7.054688 -4.921875 7.109375 -4.53125 7.109375 -4.125 C 7.109375 -3.738281 7.0625 -3.359375 6.96875 -2.984375 C 6.875 -2.617188 6.722656 -2.285156 6.515625 -1.984375 C 6.316406 -1.691406 6.054688 -1.457031 5.734375 -1.28125 C 5.421875 -1.101562 5.035156 -1.015625 4.578125 -1.015625 C 4.140625 -1.015625 3.753906 -1.097656 3.421875 -1.265625 C 3.097656 -1.429688 2.832031 -1.660156 2.625 -1.953125 C 2.414062 -2.242188 2.257812 -2.570312 2.15625 -2.9375 C 2.0625 -3.300781 2.015625 -3.675781 2.015625 -4.0625 Z M 8.421875 0 L 8.421875 -11.421875 L 7.0625 -11.421875 L 7.0625 -7.171875 L 7.03125 -7.171875 C 6.875 -7.410156 6.6875 -7.613281 6.46875 -7.78125 C 6.25 -7.945312 6.015625 -8.082031 5.765625 -8.1875 C 5.523438 -8.289062 5.28125 -8.363281 5.03125 -8.40625 C 4.789062 -8.445312 4.566406 -8.46875 4.359375 -8.46875 C 3.722656 -8.46875 3.164062 -8.351562 2.6875 -8.125 C 2.21875 -7.894531 1.828125 -7.582031 1.515625 -7.1875 C 1.203125 -6.800781 0.96875 -6.347656 0.8125 -5.828125 C 0.65625 -5.304688 0.578125 -4.75 0.578125 -4.15625 C 0.578125 -3.570312 0.65625 -3.019531 0.8125 -2.5 C 0.976562 -1.976562 1.21875 -1.519531 1.53125 -1.125 C 1.84375 -0.726562 2.234375 -0.410156 2.703125 -0.171875 C 3.179688 0.0546875 3.742188 0.171875 4.390625 0.171875 C 4.960938 0.171875 5.488281 0.0703125 5.96875 -0.125 C 6.445312 -0.332031 6.800781 -0.664062 7.03125 -1.125 L 7.0625 -1.125 L 7.0625 0 Z M 8.421875 0 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-4">
+<path style="stroke:none;" d="M 1.234375 -11.421875 L 1.234375 0 L 2.671875 0 L 2.671875 -9.171875 L 2.703125 -9.171875 L 8.671875 0 L 10.34375 0 L 10.34375 -11.421875 L 8.890625 -11.421875 L 8.890625 -2.15625 L 8.859375 -2.15625 L 2.84375 -11.421875 Z M 1.234375 -11.421875 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-5">
+<path style="stroke:none;" d="M 2.015625 -4.125 C 2.015625 -4.625 2.082031 -5.066406 2.21875 -5.453125 C 2.351562 -5.847656 2.535156 -6.175781 2.765625 -6.4375 C 3.003906 -6.707031 3.28125 -6.910156 3.59375 -7.046875 C 3.90625 -7.191406 4.238281 -7.265625 4.59375 -7.265625 C 4.945312 -7.265625 5.28125 -7.191406 5.59375 -7.046875 C 5.90625 -6.910156 6.175781 -6.707031 6.40625 -6.4375 C 6.644531 -6.175781 6.832031 -5.847656 6.96875 -5.453125 C 7.101562 -5.066406 7.171875 -4.625 7.171875 -4.125 C 7.171875 -3.625 7.101562 -3.175781 6.96875 -2.78125 C 6.832031 -2.394531 6.644531 -2.070312 6.40625 -1.8125 C 6.175781 -1.550781 5.90625 -1.351562 5.59375 -1.21875 C 5.28125 -1.082031 4.945312 -1.015625 4.59375 -1.015625 C 4.238281 -1.015625 3.90625 -1.082031 3.59375 -1.21875 C 3.28125 -1.351562 3.003906 -1.550781 2.765625 -1.8125 C 2.535156 -2.070312 2.351562 -2.394531 2.21875 -2.78125 C 2.082031 -3.175781 2.015625 -3.625 2.015625 -4.125 Z M 0.578125 -4.125 C 0.578125 -3.519531 0.660156 -2.953125 0.828125 -2.421875 C 1.003906 -1.898438 1.257812 -1.445312 1.59375 -1.0625 C 1.9375 -0.675781 2.359375 -0.375 2.859375 -0.15625 C 3.359375 0.0625 3.9375 0.171875 4.59375 0.171875 C 5.25 0.171875 5.828125 0.0625 6.328125 -0.15625 C 6.828125 -0.375 7.242188 -0.675781 7.578125 -1.0625 C 7.921875 -1.445312 8.175781 -1.898438 8.34375 -2.421875 C 8.519531 -2.953125 8.609375 -3.519531 8.609375 -4.125 C 8.609375 -4.738281 8.519531 -5.304688 8.34375 -5.828125 C 8.175781 -6.359375 7.921875 -6.816406 7.578125 -7.203125 C 7.242188 -7.597656 6.828125 -7.90625 6.328125 -8.125 C 5.828125 -8.351562 5.25 -8.46875 4.59375 -8.46875 C 3.9375 -8.46875 3.359375 -8.351562 2.859375 -8.125 C 2.359375 -7.90625 1.9375 -7.597656 1.59375 -7.203125 C 1.257812 -6.816406 1.003906 -6.359375 0.828125 -5.828125 C 0.660156 -5.304688 0.578125 -4.738281 0.578125 -4.125 Z M 0.578125 -4.125 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-6">
+<path style="stroke:none;" d="M 6.765625 -4.921875 L 2.015625 -4.921875 C 2.035156 -5.242188 2.101562 -5.546875 2.21875 -5.828125 C 2.34375 -6.109375 2.503906 -6.351562 2.703125 -6.5625 C 2.910156 -6.78125 3.15625 -6.953125 3.4375 -7.078125 C 3.71875 -7.203125 4.035156 -7.265625 4.390625 -7.265625 C 4.722656 -7.265625 5.03125 -7.203125 5.3125 -7.078125 C 5.601562 -6.953125 5.851562 -6.785156 6.0625 -6.578125 C 6.269531 -6.367188 6.429688 -6.117188 6.546875 -5.828125 C 6.671875 -5.546875 6.742188 -5.242188 6.765625 -4.921875 Z M 8.078125 -2.625 L 6.734375 -2.625 C 6.617188 -2.082031 6.375 -1.675781 6 -1.40625 C 5.632812 -1.144531 5.164062 -1.015625 4.59375 -1.015625 C 4.144531 -1.015625 3.753906 -1.085938 3.421875 -1.234375 C 3.085938 -1.378906 2.8125 -1.578125 2.59375 -1.828125 C 2.382812 -2.078125 2.234375 -2.363281 2.140625 -2.6875 C 2.046875 -3.019531 2.003906 -3.367188 2.015625 -3.734375 L 8.203125 -3.734375 C 8.222656 -4.234375 8.175781 -4.757812 8.0625 -5.3125 C 7.957031 -5.863281 7.757812 -6.375 7.46875 -6.84375 C 7.175781 -7.3125 6.785156 -7.695312 6.296875 -8 C 5.804688 -8.3125 5.195312 -8.46875 4.46875 -8.46875 C 3.894531 -8.46875 3.367188 -8.359375 2.890625 -8.140625 C 2.421875 -7.929688 2.015625 -7.632812 1.671875 -7.25 C 1.328125 -6.863281 1.054688 -6.410156 0.859375 -5.890625 C 0.671875 -5.367188 0.578125 -4.789062 0.578125 -4.15625 C 0.597656 -3.53125 0.691406 -2.945312 0.859375 -2.40625 C 1.023438 -1.875 1.269531 -1.414062 1.59375 -1.03125 C 1.925781 -0.65625 2.332031 -0.359375 2.8125 -0.140625 C 3.300781 0.0664062 3.878906 0.171875 4.546875 0.171875 C 5.484375 0.171875 6.257812 -0.0625 6.875 -0.53125 C 7.5 -1 7.898438 -1.695312 8.078125 -2.625 Z M 8.078125 -2.625 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-7">
+<path style="stroke:none;" d="M 0.96875 -8.265625 L 0.96875 0 L 2.34375 0 L 2.34375 -3.6875 C 2.34375 -4.21875 2.394531 -4.6875 2.5 -5.09375 C 2.601562 -5.507812 2.769531 -5.859375 3 -6.140625 C 3.238281 -6.429688 3.550781 -6.648438 3.9375 -6.796875 C 4.320312 -6.953125 4.785156 -7.03125 5.328125 -7.03125 L 5.328125 -8.46875 C 4.585938 -8.488281 3.976562 -8.335938 3.5 -8.015625 C 3.019531 -7.691406 2.613281 -7.195312 2.28125 -6.53125 L 2.25 -6.53125 L 2.25 -8.265625 Z M 0.96875 -8.265625 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-8">
+<path style="stroke:none;" d="M 1.078125 -8.265625 L 1.078125 3.15625 L 2.4375 3.15625 L 2.4375 -1.109375 L 2.46875 -1.109375 C 2.613281 -0.859375 2.796875 -0.648438 3.015625 -0.484375 C 3.234375 -0.316406 3.460938 -0.1875 3.703125 -0.09375 C 3.953125 0 4.203125 0.0664062 4.453125 0.109375 C 4.703125 0.148438 4.929688 0.171875 5.140625 0.171875 C 5.765625 0.171875 6.3125 0.0625 6.78125 -0.15625 C 7.257812 -0.382812 7.65625 -0.691406 7.96875 -1.078125 C 8.289062 -1.460938 8.523438 -1.914062 8.671875 -2.4375 C 8.828125 -2.96875 8.90625 -3.523438 8.90625 -4.109375 C 8.90625 -4.691406 8.828125 -5.242188 8.671875 -5.765625 C 8.515625 -6.296875 8.273438 -6.757812 7.953125 -7.15625 C 7.640625 -7.5625 7.242188 -7.878906 6.765625 -8.109375 C 6.296875 -8.347656 5.742188 -8.46875 5.109375 -8.46875 C 4.523438 -8.46875 3.992188 -8.363281 3.515625 -8.15625 C 3.035156 -7.945312 2.6875 -7.613281 2.46875 -7.15625 L 2.4375 -7.15625 L 2.4375 -8.265625 Z M 7.46875 -4.203125 C 7.46875 -3.796875 7.425781 -3.398438 7.34375 -3.015625 C 7.257812 -2.640625 7.117188 -2.300781 6.921875 -2 C 6.734375 -1.695312 6.484375 -1.457031 6.171875 -1.28125 C 5.859375 -1.101562 5.460938 -1.015625 4.984375 -1.015625 C 4.515625 -1.015625 4.113281 -1.097656 3.78125 -1.265625 C 3.457031 -1.441406 3.191406 -1.675781 2.984375 -1.96875 C 2.773438 -2.257812 2.625 -2.59375 2.53125 -2.96875 C 2.4375 -3.34375 2.390625 -3.734375 2.390625 -4.140625 C 2.390625 -4.523438 2.429688 -4.90625 2.515625 -5.28125 C 2.609375 -5.65625 2.753906 -5.988281 2.953125 -6.28125 C 3.160156 -6.570312 3.421875 -6.804688 3.734375 -6.984375 C 4.054688 -7.171875 4.445312 -7.265625 4.90625 -7.265625 C 5.34375 -7.265625 5.722656 -7.175781 6.046875 -7 C 6.378906 -6.832031 6.648438 -6.601562 6.859375 -6.3125 C 7.066406 -6.03125 7.21875 -5.703125 7.3125 -5.328125 C 7.414062 -4.960938 7.46875 -4.585938 7.46875 -4.203125 Z M 7.46875 -4.203125 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-9">
+<path style="stroke:none;" d="M 1.109375 -11.421875 L 1.109375 0 L 2.46875 0 L 2.46875 -11.421875 Z M 1.109375 -11.421875 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-10">
+<path style="stroke:none;" d="M 8.359375 -0.03125 C 8.117188 0.101562 7.789062 0.171875 7.375 0.171875 C 7.019531 0.171875 6.738281 0.0703125 6.53125 -0.125 C 6.320312 -0.320312 6.21875 -0.644531 6.21875 -1.09375 C 5.84375 -0.644531 5.40625 -0.320312 4.90625 -0.125 C 4.414062 0.0703125 3.882812 0.171875 3.3125 0.171875 C 2.9375 0.171875 2.582031 0.128906 2.25 0.046875 C 1.914062 -0.0351562 1.625 -0.164062 1.375 -0.34375 C 1.132812 -0.53125 0.941406 -0.769531 0.796875 -1.0625 C 0.648438 -1.351562 0.578125 -1.707031 0.578125 -2.125 C 0.578125 -2.59375 0.65625 -2.976562 0.8125 -3.28125 C 0.976562 -3.582031 1.191406 -3.820312 1.453125 -4 C 1.710938 -4.1875 2.007812 -4.328125 2.34375 -4.421875 C 2.675781 -4.523438 3.019531 -4.609375 3.375 -4.671875 C 3.75 -4.742188 4.101562 -4.796875 4.4375 -4.828125 C 4.769531 -4.867188 5.066406 -4.925781 5.328125 -5 C 5.585938 -5.070312 5.789062 -5.171875 5.9375 -5.296875 C 6.082031 -5.429688 6.15625 -5.628906 6.15625 -5.890625 C 6.15625 -6.191406 6.097656 -6.429688 5.984375 -6.609375 C 5.878906 -6.785156 5.738281 -6.921875 5.5625 -7.015625 C 5.382812 -7.117188 5.1875 -7.1875 4.96875 -7.21875 C 4.75 -7.25 4.53125 -7.265625 4.3125 -7.265625 C 3.738281 -7.265625 3.257812 -7.15625 2.875 -6.9375 C 2.488281 -6.71875 2.28125 -6.304688 2.25 -5.703125 L 0.890625 -5.703125 C 0.910156 -6.210938 1.015625 -6.640625 1.203125 -6.984375 C 1.398438 -7.335938 1.660156 -7.625 1.984375 -7.84375 C 2.304688 -8.0625 2.671875 -8.21875 3.078125 -8.3125 C 3.492188 -8.414062 3.9375 -8.46875 4.40625 -8.46875 C 4.769531 -8.46875 5.132812 -8.4375 5.5 -8.375 C 5.875 -8.320312 6.207031 -8.210938 6.5 -8.046875 C 6.800781 -7.890625 7.039062 -7.660156 7.21875 -7.359375 C 7.40625 -7.054688 7.5 -6.664062 7.5 -6.1875 L 7.5 -1.9375 C 7.5 -1.613281 7.515625 -1.378906 7.546875 -1.234375 C 7.585938 -1.085938 7.71875 -1.015625 7.9375 -1.015625 C 8.050781 -1.015625 8.191406 -1.039062 8.359375 -1.09375 Z M 6.140625 -4.265625 C 5.972656 -4.140625 5.75 -4.046875 5.46875 -3.984375 C 5.195312 -3.929688 4.90625 -3.882812 4.59375 -3.84375 C 4.289062 -3.8125 3.984375 -3.769531 3.671875 -3.71875 C 3.367188 -3.664062 3.09375 -3.585938 2.84375 -3.484375 C 2.601562 -3.378906 2.40625 -3.226562 2.25 -3.03125 C 2.09375 -2.832031 2.015625 -2.5625 2.015625 -2.21875 C 2.015625 -2 2.054688 -1.8125 2.140625 -1.65625 C 2.234375 -1.5 2.351562 -1.375 2.5 -1.28125 C 2.644531 -1.1875 2.8125 -1.117188 3 -1.078125 C 3.195312 -1.035156 3.398438 -1.015625 3.609375 -1.015625 C 4.054688 -1.015625 4.441406 -1.070312 4.765625 -1.1875 C 5.085938 -1.3125 5.347656 -1.46875 5.546875 -1.65625 C 5.753906 -1.84375 5.90625 -2.046875 6 -2.265625 C 6.09375 -2.484375 6.140625 -2.6875 6.140625 -2.875 Z M 6.140625 -4.265625 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-11">
+<path style="stroke:none;" d="M 6.640625 -5.609375 L 8.046875 -5.609375 C 7.992188 -6.109375 7.863281 -6.535156 7.65625 -6.890625 C 7.457031 -7.242188 7.203125 -7.535156 6.890625 -7.765625 C 6.578125 -8.003906 6.210938 -8.179688 5.796875 -8.296875 C 5.390625 -8.410156 4.953125 -8.46875 4.484375 -8.46875 C 3.828125 -8.46875 3.253906 -8.351562 2.765625 -8.125 C 2.273438 -7.894531 1.867188 -7.578125 1.546875 -7.171875 C 1.222656 -6.773438 0.976562 -6.304688 0.8125 -5.765625 C 0.65625 -5.222656 0.578125 -4.644531 0.578125 -4.03125 C 0.578125 -3.414062 0.660156 -2.847656 0.828125 -2.328125 C 0.992188 -1.804688 1.238281 -1.359375 1.5625 -0.984375 C 1.882812 -0.617188 2.285156 -0.332031 2.765625 -0.125 C 3.253906 0.0703125 3.816406 0.171875 4.453125 0.171875 C 5.503906 0.171875 6.335938 -0.101562 6.953125 -0.65625 C 7.566406 -1.207031 7.945312 -2 8.09375 -3.03125 L 6.703125 -3.03125 C 6.617188 -2.382812 6.382812 -1.882812 6 -1.53125 C 5.625 -1.1875 5.101562 -1.015625 4.4375 -1.015625 C 4.007812 -1.015625 3.640625 -1.097656 3.328125 -1.265625 C 3.015625 -1.429688 2.757812 -1.65625 2.5625 -1.9375 C 2.375 -2.226562 2.234375 -2.550781 2.140625 -2.90625 C 2.054688 -3.269531 2.015625 -3.644531 2.015625 -4.03125 C 2.015625 -4.445312 2.054688 -4.847656 2.140625 -5.234375 C 2.222656 -5.628906 2.363281 -5.972656 2.5625 -6.265625 C 2.757812 -6.566406 3.023438 -6.804688 3.359375 -6.984375 C 3.691406 -7.171875 4.101562 -7.265625 4.59375 -7.265625 C 5.164062 -7.265625 5.625 -7.117188 5.96875 -6.828125 C 6.3125 -6.546875 6.535156 -6.140625 6.640625 -5.609375 Z M 6.640625 -5.609375 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-12">
+<path style="stroke:none;" d="M 8.15625 -0.703125 L 8.15625 -8.265625 L 6.875 -8.265625 L 6.875 -7.09375 L 6.859375 -7.09375 C 6.617188 -7.550781 6.28125 -7.894531 5.84375 -8.125 C 5.40625 -8.351562 4.925781 -8.46875 4.40625 -8.46875 C 3.6875 -8.46875 3.082031 -8.328125 2.59375 -8.046875 C 2.101562 -7.773438 1.707031 -7.429688 1.40625 -7.015625 C 1.101562 -6.597656 0.890625 -6.128906 0.765625 -5.609375 C 0.640625 -5.085938 0.578125 -4.582031 0.578125 -4.09375 C 0.578125 -3.53125 0.65625 -2.992188 0.8125 -2.484375 C 0.96875 -1.984375 1.195312 -1.539062 1.5 -1.15625 C 1.8125 -0.78125 2.195312 -0.476562 2.65625 -0.25 C 3.113281 -0.03125 3.648438 0.078125 4.265625 0.078125 C 4.804688 0.078125 5.3125 -0.0390625 5.78125 -0.28125 C 6.257812 -0.519531 6.613281 -0.894531 6.84375 -1.40625 L 6.875 -1.40625 L 6.875 -0.859375 C 6.875 -0.398438 6.828125 0.015625 6.734375 0.390625 C 6.648438 0.773438 6.503906 1.101562 6.296875 1.375 C 6.097656 1.65625 5.84375 1.867188 5.53125 2.015625 C 5.226562 2.171875 4.851562 2.25 4.40625 2.25 C 4.175781 2.25 3.9375 2.222656 3.6875 2.171875 C 3.445312 2.128906 3.222656 2.054688 3.015625 1.953125 C 2.804688 1.847656 2.628906 1.707031 2.484375 1.53125 C 2.335938 1.363281 2.257812 1.15625 2.25 0.90625 L 0.890625 0.90625 C 0.910156 1.351562 1.023438 1.734375 1.234375 2.046875 C 1.453125 2.359375 1.722656 2.609375 2.046875 2.796875 C 2.378906 2.992188 2.742188 3.132812 3.140625 3.21875 C 3.546875 3.300781 3.9375 3.34375 4.3125 3.34375 C 5.632812 3.34375 6.601562 3.003906 7.21875 2.328125 C 7.84375 1.660156 8.15625 0.648438 8.15625 -0.703125 Z M 4.359375 -1.109375 C 3.910156 -1.109375 3.535156 -1.195312 3.234375 -1.375 C 2.929688 -1.5625 2.6875 -1.804688 2.5 -2.109375 C 2.320312 -2.421875 2.195312 -2.765625 2.125 -3.140625 C 2.050781 -3.515625 2.015625 -3.882812 2.015625 -4.25 C 2.015625 -4.644531 2.054688 -5.023438 2.140625 -5.390625 C 2.234375 -5.753906 2.378906 -6.070312 2.578125 -6.34375 C 2.773438 -6.625 3.03125 -6.847656 3.34375 -7.015625 C 3.65625 -7.179688 4.03125 -7.265625 4.46875 -7.265625 C 4.894531 -7.265625 5.253906 -7.175781 5.546875 -7 C 5.847656 -6.832031 6.09375 -6.609375 6.28125 -6.328125 C 6.46875 -6.046875 6.601562 -5.726562 6.6875 -5.375 C 6.769531 -5.019531 6.8125 -4.660156 6.8125 -4.296875 C 6.8125 -3.921875 6.765625 -3.539062 6.671875 -3.15625 C 6.585938 -2.769531 6.445312 -2.421875 6.25 -2.109375 C 6.0625 -1.804688 5.8125 -1.5625 5.5 -1.375 C 5.1875 -1.195312 4.804688 -1.109375 4.359375 -1.109375 Z M 4.359375 -1.109375 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-13">
+<path style="stroke:none;" d="M 2.90625 -8.265625 L 2.90625 -10.75 L 1.546875 -10.75 L 1.546875 -8.265625 L 0.140625 -8.265625 L 0.140625 -7.078125 L 1.546875 -7.078125 L 1.546875 -1.8125 C 1.546875 -1.425781 1.582031 -1.113281 1.65625 -0.875 C 1.738281 -0.644531 1.851562 -0.460938 2 -0.328125 C 2.15625 -0.203125 2.359375 -0.113281 2.609375 -0.0625 C 2.859375 -0.0195312 3.160156 0 3.515625 0 L 4.5625 0 L 4.5625 -1.203125 L 3.9375 -1.203125 C 3.71875 -1.203125 3.539062 -1.207031 3.40625 -1.21875 C 3.28125 -1.238281 3.175781 -1.273438 3.09375 -1.328125 C 3.019531 -1.378906 2.96875 -1.453125 2.9375 -1.546875 C 2.914062 -1.648438 2.90625 -1.78125 2.90625 -1.9375 L 2.90625 -7.078125 L 4.5625 -7.078125 L 4.5625 -8.265625 Z M 2.90625 -8.265625 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-14">
+<path style="stroke:none;" d="M 3.84375 -10.140625 L 3.84375 0 L 5.359375 0 L 5.359375 -10.140625 L 9.171875 -10.140625 L 9.171875 -11.421875 L 0.03125 -11.421875 L 0.03125 -10.140625 Z M 3.84375 -10.140625 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-15">
+<path style="stroke:none;" d="M 0.796875 -5.09375 L 0.796875 -3.8125 L 5.421875 -3.8125 L 5.421875 -5.09375 Z M 0.796875 -5.09375 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-16">
+<path style="stroke:none;" d="M 2.46875 -9.765625 L 2.46875 -11.421875 L 1.109375 -11.421875 L 1.109375 -9.765625 Z M 1.109375 -8.265625 L 1.109375 0 L 2.46875 0 L 2.46875 -8.265625 Z M 1.109375 -8.265625 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-17">
+<path style="stroke:none;" d="M 1.859375 -2.609375 L 0.5 -2.609375 C 0.519531 -2.097656 0.625 -1.660156 0.8125 -1.296875 C 1.007812 -0.941406 1.265625 -0.65625 1.578125 -0.4375 C 1.898438 -0.21875 2.269531 -0.0625 2.6875 0.03125 C 3.101562 0.125 3.539062 0.171875 4 0.171875 C 4.414062 0.171875 4.832031 0.128906 5.25 0.046875 C 5.675781 -0.0234375 6.054688 -0.160156 6.390625 -0.359375 C 6.722656 -0.566406 6.992188 -0.832031 7.203125 -1.15625 C 7.410156 -1.488281 7.515625 -1.910156 7.515625 -2.421875 C 7.515625 -2.816406 7.4375 -3.144531 7.28125 -3.40625 C 7.132812 -3.675781 6.929688 -3.898438 6.671875 -4.078125 C 6.421875 -4.253906 6.132812 -4.394531 5.8125 -4.5 C 5.488281 -4.601562 5.15625 -4.691406 4.8125 -4.765625 C 4.5 -4.835938 4.179688 -4.910156 3.859375 -4.984375 C 3.535156 -5.054688 3.242188 -5.140625 2.984375 -5.234375 C 2.734375 -5.335938 2.523438 -5.46875 2.359375 -5.625 C 2.191406 -5.78125 2.109375 -5.972656 2.109375 -6.203125 C 2.109375 -6.421875 2.160156 -6.59375 2.265625 -6.71875 C 2.378906 -6.851562 2.519531 -6.960938 2.6875 -7.046875 C 2.851562 -7.128906 3.039062 -7.1875 3.25 -7.21875 C 3.457031 -7.25 3.664062 -7.265625 3.875 -7.265625 C 4.09375 -7.265625 4.3125 -7.238281 4.53125 -7.1875 C 4.75 -7.144531 4.945312 -7.066406 5.125 -6.953125 C 5.3125 -6.847656 5.460938 -6.707031 5.578125 -6.53125 C 5.703125 -6.351562 5.773438 -6.132812 5.796875 -5.875 L 7.15625 -5.875 C 7.125 -6.375 7.015625 -6.789062 6.828125 -7.125 C 6.648438 -7.457031 6.40625 -7.722656 6.09375 -7.921875 C 5.789062 -8.117188 5.441406 -8.257812 5.046875 -8.34375 C 4.660156 -8.425781 4.234375 -8.46875 3.765625 -8.46875 C 3.398438 -8.46875 3.03125 -8.421875 2.65625 -8.328125 C 2.289062 -8.234375 1.960938 -8.09375 1.671875 -7.90625 C 1.378906 -7.71875 1.140625 -7.472656 0.953125 -7.171875 C 0.765625 -6.878906 0.671875 -6.523438 0.671875 -6.109375 C 0.671875 -5.578125 0.800781 -5.160156 1.0625 -4.859375 C 1.332031 -4.566406 1.664062 -4.335938 2.0625 -4.171875 C 2.46875 -4.003906 2.90625 -3.875 3.375 -3.78125 C 3.84375 -3.6875 4.273438 -3.582031 4.671875 -3.46875 C 5.078125 -3.363281 5.410156 -3.21875 5.671875 -3.03125 C 5.941406 -2.851562 6.078125 -2.585938 6.078125 -2.234375 C 6.078125 -1.984375 6.015625 -1.773438 5.890625 -1.609375 C 5.765625 -1.441406 5.601562 -1.316406 5.40625 -1.234375 C 5.207031 -1.148438 4.988281 -1.09375 4.75 -1.0625 C 4.519531 -1.03125 4.296875 -1.015625 4.078125 -1.015625 C 3.796875 -1.015625 3.523438 -1.039062 3.265625 -1.09375 C 3.003906 -1.144531 2.769531 -1.226562 2.5625 -1.34375 C 2.351562 -1.46875 2.1875 -1.632812 2.0625 -1.84375 C 1.9375 -2.050781 1.867188 -2.304688 1.859375 -2.609375 Z M 1.859375 -2.609375 "/>
+</symbol>
+</g>
+</defs>
+<g id="surface1">
+<path style="fill-rule:nonzero;fill:rgb(100%,100%,100%);fill-opacity:1;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 194.910156 82.542969 C 223.03125 96.601562 223.03125 119.398438 194.910156 133.457031 C 166.792969 147.515625 121.207031 147.515625 93.089844 133.457031 C 64.96875 119.398438 64.96875 96.601562 93.089844 82.542969 C 121.207031 68.484375 166.792969 68.484375 194.910156 82.542969 " transform="matrix(1,0,0,1,0,-42)"/>
+<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-1" x="111.256" y="71.776001"/>
+  <use xlink:href="#glyph0-2" x="119.544" y="71.776001"/>
+  <use xlink:href="#glyph0-3" x="128.44" y="71.776001"/>
+  <use xlink:href="#glyph0-4" x="137.928" y="71.776001"/>
+  <use xlink:href="#glyph0-5" x="149.48" y="71.776001"/>
+  <use xlink:href="#glyph0-3" x="158.664" y="71.776001"/>
+  <use xlink:href="#glyph0-6" x="168.152" y="71.776001"/>
+</g>
+<path style="fill-rule:nonzero;fill:rgb(100%,100%,100%);fill-opacity:1;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 374.910156 82.542969 C 403.03125 96.601562 403.03125 119.398438 374.910156 133.457031 C 346.792969 147.515625 301.207031 147.515625 273.089844 133.457031 C 244.96875 119.398438 244.96875 96.601562 273.089844 82.542969 C 301.207031 68.484375 346.792969 68.484375 374.910156 82.542969 " transform="matrix(1,0,0,1,0,-42)"/>
+<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-7" x="278.368" y="71.776001"/>
+</g>
+<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-6" x="283.408" y="71.776001"/>
+  <use xlink:href="#glyph0-8" x="292" y="71.776001"/>
+  <use xlink:href="#glyph0-9" x="301.488" y="71.776001"/>
+  <use xlink:href="#glyph0-10" x="305.04" y="71.776001"/>
+  <use xlink:href="#glyph0-11" x="313.632" y="71.776001"/>
+  <use xlink:href="#glyph0-6" x="322.224" y="71.776001"/>
+  <use xlink:href="#glyph0-4" x="330.816" y="71.776001"/>
+  <use xlink:href="#glyph0-5" x="342.368" y="71.776001"/>
+  <use xlink:href="#glyph0-3" x="351.552" y="71.776001"/>
+  <use xlink:href="#glyph0-6" x="361.04" y="71.776001"/>
+</g>
+<path style="fill:none;stroke-width:2;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 216 108 L 239.101562 108 " transform="matrix(1,0,0,1,0,-42)"/>
+<path style="fill-rule:nonzero;fill:rgb(0%,0%,0%);fill-opacity:1;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 248.699219 108 L 239.101562 104.398438 L 239.101562 111.601562 Z M 248.699219 108 " transform="matrix(1,0,0,1,0,-42)"/>
+<path style="fill:none;stroke-width:2;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 396 108 L 419.101562 108 " transform="matrix(1,0,0,1,0,-42)"/>
+<path style="fill-rule:nonzero;fill:rgb(0%,0%,0%);fill-opacity:1;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 428.699219 108 L 419.101562 104.398438 L 419.101562 111.601562 Z M 428.699219 108 " transform="matrix(1,0,0,1,0,-42)"/>
+<path style="fill:none;stroke-width:2;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 121.597656 154.90625 C 116.976562 167.921875 114.246094 180.738281 117 189 C 124.648438 211.949219 163.351562 211.949219 171 189 C 174.605469 178.183594 168.8125 159.5625 161.679688 142.902344 " transform="matrix(1,0,0,1,0,-42)"/>
+<path style="fill-rule:nonzero;fill:rgb(0%,0%,0%);fill-opacity:1;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 125.113281 145.972656 L 118.246094 153.589844 L 124.945312 156.226562 Z M 125.113281 145.972656 " transform="matrix(1,0,0,1,0,-42)"/>
+<path style="fill:none;stroke-width:2;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 301 154.789062 C 296.175781 167.847656 293.246094 180.710938 295.898438 189 C 303.234375 211.949219 341.933594 211.949219 349.898438 189 C 353.644531 178.195312 348.121094 159.605469 341.226562 142.960938 " transform="matrix(1,0,0,1,0,-42)"/>
+<path style="fill-rule:nonzero;fill:rgb(0%,0%,0%);fill-opacity:1;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 304.625 145.902344 L 297.667969 153.433594 L 304.335938 156.152344 Z M 304.625 145.902344 " transform="matrix(1,0,0,1,0,-42)"/>
+<path style="fill:none;stroke-width:2;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 482.136719 155.011719 C 477.65625 168.074219 475.066406 180.9375 477.917969 189.226562 C 485.828125 212.238281 524.527344 212.238281 531.917969 189.226562 C 535.410156 178.347656 529.363281 159.605469 522.011719 142.859375 " transform="matrix(1,0,0,1,0,-42)"/>
+<path style="fill-rule:nonzero;fill:rgb(0%,0%,0%);fill-opacity:1;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 485.558594 146.039062 L 478.773438 153.726562 L 485.503906 156.292969 Z M 485.558594 146.039062 " transform="matrix(1,0,0,1,0,-42)"/>
+<path style="fill-rule:nonzero;fill:rgb(100%,100%,100%);fill-opacity:1;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 554.910156 82.542969 C 583.03125 96.601562 583.03125 119.398438 554.910156 133.457031 C 526.792969 147.515625 481.207031 147.515625 453.089844 133.457031 C 424.96875 119.398438 424.96875 96.601562 453.089844 82.542969 C 481.207031 68.484375 526.792969 68.484375 554.910156 82.542969 " transform="matrix(1,0,0,1,0,-42)"/>
+<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-12" x="477.624" y="71.776001"/>
+  <use xlink:href="#glyph0-6" x="486.808" y="71.776001"/>
+  <use xlink:href="#glyph0-13" x="495.4" y="71.776001"/>
+  <use xlink:href="#glyph0-14" x="500.44" y="71.776001"/>
+</g>
+<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-7" x="508.152" y="71.776001"/>
+</g>
+<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-6" x="513.192" y="71.776001"/>
+  <use xlink:href="#glyph0-6" x="521.784" y="71.776001"/>
+</g>
+<path style="fill:none;stroke-width:2;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-dasharray:8,8;stroke-miterlimit:10;" d="M 617.101562 108 L 576 108 " transform="matrix(1,0,0,1,0,-42)"/>
+<path style="fill-rule:nonzero;fill:rgb(0%,0%,0%);fill-opacity:1;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 626.699219 108 L 617.101562 104.398438 L 617.101562 111.601562 Z M 626.699219 108 " transform="matrix(1,0,0,1,0,-42)"/>
+<path style="fill:none;stroke-width:2;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-dasharray:8,8;stroke-miterlimit:10;" d="M 9 108 L 59.101562 108 " transform="matrix(1,0,0,1,0,-42)"/>
+<path style="fill-rule:nonzero;fill:rgb(0%,0%,0%);fill-opacity:1;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 68.699219 108 L 59.101562 104.398438 L 59.101562 111.601562 Z M 68.699219 108 " transform="matrix(1,0,0,1,0,-42)"/>
+<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-8" x="5.136" y="20.776001"/>
+  <use xlink:href="#glyph0-7" x="14.624" y="20.776001"/>
+</g>
+<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-6" x="19.664" y="20.776001"/>
+  <use xlink:href="#glyph0-15" x="28.256" y="20.776001"/>
+  <use xlink:href="#glyph0-11" x="34.48" y="20.776001"/>
+  <use xlink:href="#glyph0-5" x="43.072" y="20.776001"/>
+  <use xlink:href="#glyph0-2" x="52.256" y="20.776001"/>
+  <use xlink:href="#glyph0-3" x="61.152" y="20.776001"/>
+  <use xlink:href="#glyph0-16" x="70.64" y="20.776001"/>
+  <use xlink:href="#glyph0-13" x="74.192" y="20.776001"/>
+  <use xlink:href="#glyph0-16" x="79.232" y="20.776001"/>
+  <use xlink:href="#glyph0-5" x="82.784" y="20.776001"/>
+  <use xlink:href="#glyph0-2" x="91.968" y="20.776001"/>
+</g>
+<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-8" x="173.84" y="20.776001"/>
+  <use xlink:href="#glyph0-5" x="183.328" y="20.776001"/>
+  <use xlink:href="#glyph0-17" x="192.512" y="20.776001"/>
+  <use xlink:href="#glyph0-13" x="200.512" y="20.776001"/>
+  <use xlink:href="#glyph0-15" x="205.552" y="20.776001"/>
+  <use xlink:href="#glyph0-11" x="211.776" y="20.776001"/>
+  <use xlink:href="#glyph0-5" x="220.368" y="20.776001"/>
+  <use xlink:href="#glyph0-2" x="229.552" y="20.776001"/>
+  <use xlink:href="#glyph0-3" x="238.448" y="20.776001"/>
+  <use xlink:href="#glyph0-16" x="247.936" y="20.776001"/>
+  <use xlink:href="#glyph0-13" x="251.488" y="20.776001"/>
+  <use xlink:href="#glyph0-16" x="256.528" y="20.776001"/>
+  <use xlink:href="#glyph0-5" x="260.08" y="20.776001"/>
+  <use xlink:href="#glyph0-2" x="269.264" y="20.776001"/>
+</g>
+</g>
+</svg>
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Slide/fig/funcLoopinAutomata.svg	Sat May 19 19:14:19 2018 +0900
@@ -0,0 +1,284 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<svg xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" width="489pt" height="473pt" viewBox="0 0 489 473" version="1.1">
+<defs>
+<g>
+<symbol overflow="visible" id="glyph0-0">
+<path style="stroke:none;" d="M 6.546875 -10.65625 L 1.625 -10.65625 L 1.625 -0.75 L 6.546875 -0.75 Z M 7.359375 -11.390625 L 7.359375 -0.015625 L 0.8125 -0.015625 L 0.8125 -11.390625 Z M 7.359375 -11.390625 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-1">
+<path style="stroke:none;" d="M 5.84375 0 L 7.203125 0 L 7.203125 -8.265625 L 5.84375 -8.265625 Z M 5.84375 -9.765625 L 7.203125 -9.765625 L 7.203125 -11.421875 L 5.84375 -11.421875 Z M 1.578125 -7.078125 L 1.578125 0 L 2.9375 0 L 2.9375 -7.078125 L 4.546875 -7.078125 L 4.546875 -8.265625 L 2.9375 -8.265625 L 2.9375 -9.421875 C 2.9375 -9.785156 3.023438 -10.03125 3.203125 -10.15625 C 3.390625 -10.289062 3.648438 -10.359375 3.984375 -10.359375 C 4.097656 -10.359375 4.222656 -10.347656 4.359375 -10.328125 C 4.503906 -10.304688 4.632812 -10.273438 4.75 -10.234375 L 4.75 -11.421875 C 4.625 -11.460938 4.476562 -11.492188 4.3125 -11.515625 C 4.144531 -11.535156 4 -11.546875 3.875 -11.546875 C 3.125 -11.546875 2.550781 -11.375 2.15625 -11.03125 C 1.769531 -10.6875 1.578125 -10.175781 1.578125 -9.5 L 1.578125 -8.265625 L 0.1875 -8.265625 L 0.1875 -7.078125 Z M 1.578125 -7.078125 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-2">
+<path style="stroke:none;" d="M 1.03125 -8.265625 L 1.03125 0 L 2.390625 0 L 2.390625 -4.671875 C 2.390625 -5.046875 2.4375 -5.390625 2.53125 -5.703125 C 2.632812 -6.015625 2.785156 -6.285156 2.984375 -6.515625 C 3.191406 -6.753906 3.445312 -6.9375 3.75 -7.0625 C 4.050781 -7.195312 4.410156 -7.265625 4.828125 -7.265625 C 5.347656 -7.265625 5.757812 -7.113281 6.0625 -6.8125 C 6.363281 -6.519531 6.515625 -6.113281 6.515625 -5.59375 L 6.515625 0 L 7.875 0 L 7.875 -5.4375 C 7.875 -5.882812 7.828125 -6.289062 7.734375 -6.65625 C 7.640625 -7.03125 7.476562 -7.347656 7.25 -7.609375 C 7.03125 -7.878906 6.738281 -8.085938 6.375 -8.234375 C 6.019531 -8.390625 5.570312 -8.46875 5.03125 -8.46875 C 3.800781 -8.46875 2.90625 -7.960938 2.34375 -6.953125 L 2.296875 -6.953125 L 2.296875 -8.265625 Z M 1.03125 -8.265625 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-3">
+<path style="stroke:none;" d="M 2.015625 -4.0625 C 2.015625 -4.46875 2.054688 -4.863281 2.140625 -5.25 C 2.222656 -5.632812 2.359375 -5.972656 2.546875 -6.265625 C 2.742188 -6.566406 3.003906 -6.804688 3.328125 -6.984375 C 3.648438 -7.171875 4.039062 -7.265625 4.5 -7.265625 C 4.96875 -7.265625 5.363281 -7.175781 5.6875 -7 C 6.019531 -6.820312 6.289062 -6.585938 6.5 -6.296875 C 6.707031 -6.015625 6.859375 -5.679688 6.953125 -5.296875 C 7.054688 -4.921875 7.109375 -4.53125 7.109375 -4.125 C 7.109375 -3.738281 7.0625 -3.359375 6.96875 -2.984375 C 6.875 -2.617188 6.722656 -2.285156 6.515625 -1.984375 C 6.316406 -1.691406 6.054688 -1.457031 5.734375 -1.28125 C 5.421875 -1.101562 5.035156 -1.015625 4.578125 -1.015625 C 4.140625 -1.015625 3.753906 -1.097656 3.421875 -1.265625 C 3.097656 -1.429688 2.832031 -1.660156 2.625 -1.953125 C 2.414062 -2.242188 2.257812 -2.570312 2.15625 -2.9375 C 2.0625 -3.300781 2.015625 -3.675781 2.015625 -4.0625 Z M 8.421875 0 L 8.421875 -11.421875 L 7.0625 -11.421875 L 7.0625 -7.171875 L 7.03125 -7.171875 C 6.875 -7.410156 6.6875 -7.613281 6.46875 -7.78125 C 6.25 -7.945312 6.015625 -8.082031 5.765625 -8.1875 C 5.523438 -8.289062 5.28125 -8.363281 5.03125 -8.40625 C 4.789062 -8.445312 4.566406 -8.46875 4.359375 -8.46875 C 3.722656 -8.46875 3.164062 -8.351562 2.6875 -8.125 C 2.21875 -7.894531 1.828125 -7.582031 1.515625 -7.1875 C 1.203125 -6.800781 0.96875 -6.347656 0.8125 -5.828125 C 0.65625 -5.304688 0.578125 -4.75 0.578125 -4.15625 C 0.578125 -3.570312 0.65625 -3.019531 0.8125 -2.5 C 0.976562 -1.976562 1.21875 -1.519531 1.53125 -1.125 C 1.84375 -0.726562 2.234375 -0.410156 2.703125 -0.171875 C 3.179688 0.0546875 3.742188 0.171875 4.390625 0.171875 C 4.960938 0.171875 5.488281 0.0703125 5.96875 -0.125 C 6.445312 -0.332031 6.800781 -0.664062 7.03125 -1.125 L 7.0625 -1.125 L 7.0625 0 Z M 8.421875 0 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-4">
+<path style="stroke:none;" d="M 1.234375 -11.421875 L 1.234375 0 L 2.671875 0 L 2.671875 -9.171875 L 2.703125 -9.171875 L 8.671875 0 L 10.34375 0 L 10.34375 -11.421875 L 8.890625 -11.421875 L 8.890625 -2.15625 L 8.859375 -2.15625 L 2.84375 -11.421875 Z M 1.234375 -11.421875 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-5">
+<path style="stroke:none;" d="M 2.015625 -4.125 C 2.015625 -4.625 2.082031 -5.066406 2.21875 -5.453125 C 2.351562 -5.847656 2.535156 -6.175781 2.765625 -6.4375 C 3.003906 -6.707031 3.28125 -6.910156 3.59375 -7.046875 C 3.90625 -7.191406 4.238281 -7.265625 4.59375 -7.265625 C 4.945312 -7.265625 5.28125 -7.191406 5.59375 -7.046875 C 5.90625 -6.910156 6.175781 -6.707031 6.40625 -6.4375 C 6.644531 -6.175781 6.832031 -5.847656 6.96875 -5.453125 C 7.101562 -5.066406 7.171875 -4.625 7.171875 -4.125 C 7.171875 -3.625 7.101562 -3.175781 6.96875 -2.78125 C 6.832031 -2.394531 6.644531 -2.070312 6.40625 -1.8125 C 6.175781 -1.550781 5.90625 -1.351562 5.59375 -1.21875 C 5.28125 -1.082031 4.945312 -1.015625 4.59375 -1.015625 C 4.238281 -1.015625 3.90625 -1.082031 3.59375 -1.21875 C 3.28125 -1.351562 3.003906 -1.550781 2.765625 -1.8125 C 2.535156 -2.070312 2.351562 -2.394531 2.21875 -2.78125 C 2.082031 -3.175781 2.015625 -3.625 2.015625 -4.125 Z M 0.578125 -4.125 C 0.578125 -3.519531 0.660156 -2.953125 0.828125 -2.421875 C 1.003906 -1.898438 1.257812 -1.445312 1.59375 -1.0625 C 1.9375 -0.675781 2.359375 -0.375 2.859375 -0.15625 C 3.359375 0.0625 3.9375 0.171875 4.59375 0.171875 C 5.25 0.171875 5.828125 0.0625 6.328125 -0.15625 C 6.828125 -0.375 7.242188 -0.675781 7.578125 -1.0625 C 7.921875 -1.445312 8.175781 -1.898438 8.34375 -2.421875 C 8.519531 -2.953125 8.609375 -3.519531 8.609375 -4.125 C 8.609375 -4.738281 8.519531 -5.304688 8.34375 -5.828125 C 8.175781 -6.359375 7.921875 -6.816406 7.578125 -7.203125 C 7.242188 -7.597656 6.828125 -7.90625 6.328125 -8.125 C 5.828125 -8.351562 5.25 -8.46875 4.59375 -8.46875 C 3.9375 -8.46875 3.359375 -8.351562 2.859375 -8.125 C 2.359375 -7.90625 1.9375 -7.597656 1.59375 -7.203125 C 1.257812 -6.816406 1.003906 -6.359375 0.828125 -5.828125 C 0.660156 -5.304688 0.578125 -4.738281 0.578125 -4.125 Z M 0.578125 -4.125 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-6">
+<path style="stroke:none;" d="M 6.765625 -4.921875 L 2.015625 -4.921875 C 2.035156 -5.242188 2.101562 -5.546875 2.21875 -5.828125 C 2.34375 -6.109375 2.503906 -6.351562 2.703125 -6.5625 C 2.910156 -6.78125 3.15625 -6.953125 3.4375 -7.078125 C 3.71875 -7.203125 4.035156 -7.265625 4.390625 -7.265625 C 4.722656 -7.265625 5.03125 -7.203125 5.3125 -7.078125 C 5.601562 -6.953125 5.851562 -6.785156 6.0625 -6.578125 C 6.269531 -6.367188 6.429688 -6.117188 6.546875 -5.828125 C 6.671875 -5.546875 6.742188 -5.242188 6.765625 -4.921875 Z M 8.078125 -2.625 L 6.734375 -2.625 C 6.617188 -2.082031 6.375 -1.675781 6 -1.40625 C 5.632812 -1.144531 5.164062 -1.015625 4.59375 -1.015625 C 4.144531 -1.015625 3.753906 -1.085938 3.421875 -1.234375 C 3.085938 -1.378906 2.8125 -1.578125 2.59375 -1.828125 C 2.382812 -2.078125 2.234375 -2.363281 2.140625 -2.6875 C 2.046875 -3.019531 2.003906 -3.367188 2.015625 -3.734375 L 8.203125 -3.734375 C 8.222656 -4.234375 8.175781 -4.757812 8.0625 -5.3125 C 7.957031 -5.863281 7.757812 -6.375 7.46875 -6.84375 C 7.175781 -7.3125 6.785156 -7.695312 6.296875 -8 C 5.804688 -8.3125 5.195312 -8.46875 4.46875 -8.46875 C 3.894531 -8.46875 3.367188 -8.359375 2.890625 -8.140625 C 2.421875 -7.929688 2.015625 -7.632812 1.671875 -7.25 C 1.328125 -6.863281 1.054688 -6.410156 0.859375 -5.890625 C 0.671875 -5.367188 0.578125 -4.789062 0.578125 -4.15625 C 0.597656 -3.53125 0.691406 -2.945312 0.859375 -2.40625 C 1.023438 -1.875 1.269531 -1.414062 1.59375 -1.03125 C 1.925781 -0.65625 2.332031 -0.359375 2.8125 -0.140625 C 3.300781 0.0664062 3.878906 0.171875 4.546875 0.171875 C 5.484375 0.171875 6.257812 -0.0625 6.875 -0.53125 C 7.5 -1 7.898438 -1.695312 8.078125 -2.625 Z M 8.078125 -2.625 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-7">
+<path style="stroke:none;" d="M 1.859375 -2.609375 L 0.5 -2.609375 C 0.519531 -2.097656 0.625 -1.660156 0.8125 -1.296875 C 1.007812 -0.941406 1.265625 -0.65625 1.578125 -0.4375 C 1.898438 -0.21875 2.269531 -0.0625 2.6875 0.03125 C 3.101562 0.125 3.539062 0.171875 4 0.171875 C 4.414062 0.171875 4.832031 0.128906 5.25 0.046875 C 5.675781 -0.0234375 6.054688 -0.160156 6.390625 -0.359375 C 6.722656 -0.566406 6.992188 -0.832031 7.203125 -1.15625 C 7.410156 -1.488281 7.515625 -1.910156 7.515625 -2.421875 C 7.515625 -2.816406 7.4375 -3.144531 7.28125 -3.40625 C 7.132812 -3.675781 6.929688 -3.898438 6.671875 -4.078125 C 6.421875 -4.253906 6.132812 -4.394531 5.8125 -4.5 C 5.488281 -4.601562 5.15625 -4.691406 4.8125 -4.765625 C 4.5 -4.835938 4.179688 -4.910156 3.859375 -4.984375 C 3.535156 -5.054688 3.242188 -5.140625 2.984375 -5.234375 C 2.734375 -5.335938 2.523438 -5.46875 2.359375 -5.625 C 2.191406 -5.78125 2.109375 -5.972656 2.109375 -6.203125 C 2.109375 -6.421875 2.160156 -6.59375 2.265625 -6.71875 C 2.378906 -6.851562 2.519531 -6.960938 2.6875 -7.046875 C 2.851562 -7.128906 3.039062 -7.1875 3.25 -7.21875 C 3.457031 -7.25 3.664062 -7.265625 3.875 -7.265625 C 4.09375 -7.265625 4.3125 -7.238281 4.53125 -7.1875 C 4.75 -7.144531 4.945312 -7.066406 5.125 -6.953125 C 5.3125 -6.847656 5.460938 -6.707031 5.578125 -6.53125 C 5.703125 -6.351562 5.773438 -6.132812 5.796875 -5.875 L 7.15625 -5.875 C 7.125 -6.375 7.015625 -6.789062 6.828125 -7.125 C 6.648438 -7.457031 6.40625 -7.722656 6.09375 -7.921875 C 5.789062 -8.117188 5.441406 -8.257812 5.046875 -8.34375 C 4.660156 -8.425781 4.234375 -8.46875 3.765625 -8.46875 C 3.398438 -8.46875 3.03125 -8.421875 2.65625 -8.328125 C 2.289062 -8.234375 1.960938 -8.09375 1.671875 -7.90625 C 1.378906 -7.71875 1.140625 -7.472656 0.953125 -7.171875 C 0.765625 -6.878906 0.671875 -6.523438 0.671875 -6.109375 C 0.671875 -5.578125 0.800781 -5.160156 1.0625 -4.859375 C 1.332031 -4.566406 1.664062 -4.335938 2.0625 -4.171875 C 2.46875 -4.003906 2.90625 -3.875 3.375 -3.78125 C 3.84375 -3.6875 4.273438 -3.582031 4.671875 -3.46875 C 5.078125 -3.363281 5.410156 -3.21875 5.671875 -3.03125 C 5.941406 -2.851562 6.078125 -2.585938 6.078125 -2.234375 C 6.078125 -1.984375 6.015625 -1.773438 5.890625 -1.609375 C 5.765625 -1.441406 5.601562 -1.316406 5.40625 -1.234375 C 5.207031 -1.148438 4.988281 -1.09375 4.75 -1.0625 C 4.519531 -1.03125 4.296875 -1.015625 4.078125 -1.015625 C 3.796875 -1.015625 3.523438 -1.039062 3.265625 -1.09375 C 3.003906 -1.144531 2.769531 -1.226562 2.5625 -1.34375 C 2.351562 -1.46875 2.1875 -1.632812 2.0625 -1.84375 C 1.9375 -2.050781 1.867188 -2.304688 1.859375 -2.609375 Z M 1.859375 -2.609375 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-8">
+<path style="stroke:none;" d="M 8.359375 -0.03125 C 8.117188 0.101562 7.789062 0.171875 7.375 0.171875 C 7.019531 0.171875 6.738281 0.0703125 6.53125 -0.125 C 6.320312 -0.320312 6.21875 -0.644531 6.21875 -1.09375 C 5.84375 -0.644531 5.40625 -0.320312 4.90625 -0.125 C 4.414062 0.0703125 3.882812 0.171875 3.3125 0.171875 C 2.9375 0.171875 2.582031 0.128906 2.25 0.046875 C 1.914062 -0.0351562 1.625 -0.164062 1.375 -0.34375 C 1.132812 -0.53125 0.941406 -0.769531 0.796875 -1.0625 C 0.648438 -1.351562 0.578125 -1.707031 0.578125 -2.125 C 0.578125 -2.59375 0.65625 -2.976562 0.8125 -3.28125 C 0.976562 -3.582031 1.191406 -3.820312 1.453125 -4 C 1.710938 -4.1875 2.007812 -4.328125 2.34375 -4.421875 C 2.675781 -4.523438 3.019531 -4.609375 3.375 -4.671875 C 3.75 -4.742188 4.101562 -4.796875 4.4375 -4.828125 C 4.769531 -4.867188 5.066406 -4.925781 5.328125 -5 C 5.585938 -5.070312 5.789062 -5.171875 5.9375 -5.296875 C 6.082031 -5.429688 6.15625 -5.628906 6.15625 -5.890625 C 6.15625 -6.191406 6.097656 -6.429688 5.984375 -6.609375 C 5.878906 -6.785156 5.738281 -6.921875 5.5625 -7.015625 C 5.382812 -7.117188 5.1875 -7.1875 4.96875 -7.21875 C 4.75 -7.25 4.53125 -7.265625 4.3125 -7.265625 C 3.738281 -7.265625 3.257812 -7.15625 2.875 -6.9375 C 2.488281 -6.71875 2.28125 -6.304688 2.25 -5.703125 L 0.890625 -5.703125 C 0.910156 -6.210938 1.015625 -6.640625 1.203125 -6.984375 C 1.398438 -7.335938 1.660156 -7.625 1.984375 -7.84375 C 2.304688 -8.0625 2.671875 -8.21875 3.078125 -8.3125 C 3.492188 -8.414062 3.9375 -8.46875 4.40625 -8.46875 C 4.769531 -8.46875 5.132812 -8.4375 5.5 -8.375 C 5.875 -8.320312 6.207031 -8.210938 6.5 -8.046875 C 6.800781 -7.890625 7.039062 -7.660156 7.21875 -7.359375 C 7.40625 -7.054688 7.5 -6.664062 7.5 -6.1875 L 7.5 -1.9375 C 7.5 -1.613281 7.515625 -1.378906 7.546875 -1.234375 C 7.585938 -1.085938 7.71875 -1.015625 7.9375 -1.015625 C 8.050781 -1.015625 8.191406 -1.039062 8.359375 -1.09375 Z M 6.140625 -4.265625 C 5.972656 -4.140625 5.75 -4.046875 5.46875 -3.984375 C 5.195312 -3.929688 4.90625 -3.882812 4.59375 -3.84375 C 4.289062 -3.8125 3.984375 -3.769531 3.671875 -3.71875 C 3.367188 -3.664062 3.09375 -3.585938 2.84375 -3.484375 C 2.601562 -3.378906 2.40625 -3.226562 2.25 -3.03125 C 2.09375 -2.832031 2.015625 -2.5625 2.015625 -2.21875 C 2.015625 -2 2.054688 -1.8125 2.140625 -1.65625 C 2.234375 -1.5 2.351562 -1.375 2.5 -1.28125 C 2.644531 -1.1875 2.8125 -1.117188 3 -1.078125 C 3.195312 -1.035156 3.398438 -1.015625 3.609375 -1.015625 C 4.054688 -1.015625 4.441406 -1.070312 4.765625 -1.1875 C 5.085938 -1.3125 5.347656 -1.46875 5.546875 -1.65625 C 5.753906 -1.84375 5.90625 -2.046875 6 -2.265625 C 6.09375 -2.484375 6.140625 -2.6875 6.140625 -2.875 Z M 6.140625 -4.265625 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-9">
+<path style="stroke:none;" d="M 0.96875 -8.265625 L 0.96875 0 L 2.34375 0 L 2.34375 -3.6875 C 2.34375 -4.21875 2.394531 -4.6875 2.5 -5.09375 C 2.601562 -5.507812 2.769531 -5.859375 3 -6.140625 C 3.238281 -6.429688 3.550781 -6.648438 3.9375 -6.796875 C 4.320312 -6.953125 4.785156 -7.03125 5.328125 -7.03125 L 5.328125 -8.46875 C 4.585938 -8.488281 3.976562 -8.335938 3.5 -8.015625 C 3.019531 -7.691406 2.613281 -7.195312 2.28125 -6.53125 L 2.25 -6.53125 L 2.25 -8.265625 Z M 0.96875 -8.265625 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-10">
+<path style="stroke:none;" d="M 6.640625 -5.609375 L 8.046875 -5.609375 C 7.992188 -6.109375 7.863281 -6.535156 7.65625 -6.890625 C 7.457031 -7.242188 7.203125 -7.535156 6.890625 -7.765625 C 6.578125 -8.003906 6.210938 -8.179688 5.796875 -8.296875 C 5.390625 -8.410156 4.953125 -8.46875 4.484375 -8.46875 C 3.828125 -8.46875 3.253906 -8.351562 2.765625 -8.125 C 2.273438 -7.894531 1.867188 -7.578125 1.546875 -7.171875 C 1.222656 -6.773438 0.976562 -6.304688 0.8125 -5.765625 C 0.65625 -5.222656 0.578125 -4.644531 0.578125 -4.03125 C 0.578125 -3.414062 0.660156 -2.847656 0.828125 -2.328125 C 0.992188 -1.804688 1.238281 -1.359375 1.5625 -0.984375 C 1.882812 -0.617188 2.285156 -0.332031 2.765625 -0.125 C 3.253906 0.0703125 3.816406 0.171875 4.453125 0.171875 C 5.503906 0.171875 6.335938 -0.101562 6.953125 -0.65625 C 7.566406 -1.207031 7.945312 -2 8.09375 -3.03125 L 6.703125 -3.03125 C 6.617188 -2.382812 6.382812 -1.882812 6 -1.53125 C 5.625 -1.1875 5.101562 -1.015625 4.4375 -1.015625 C 4.007812 -1.015625 3.640625 -1.097656 3.328125 -1.265625 C 3.015625 -1.429688 2.757812 -1.65625 2.5625 -1.9375 C 2.375 -2.226562 2.234375 -2.550781 2.140625 -2.90625 C 2.054688 -3.269531 2.015625 -3.644531 2.015625 -4.03125 C 2.015625 -4.445312 2.054688 -4.847656 2.140625 -5.234375 C 2.222656 -5.628906 2.363281 -5.972656 2.5625 -6.265625 C 2.757812 -6.566406 3.023438 -6.804688 3.359375 -6.984375 C 3.691406 -7.171875 4.101562 -7.265625 4.59375 -7.265625 C 5.164062 -7.265625 5.625 -7.117188 5.96875 -6.828125 C 6.3125 -6.546875 6.535156 -6.140625 6.640625 -5.609375 Z M 6.640625 -5.609375 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-11">
+<path style="stroke:none;" d="M 1.03125 -11.421875 L 1.03125 0 L 2.390625 0 L 2.390625 -4.671875 C 2.390625 -5.046875 2.4375 -5.390625 2.53125 -5.703125 C 2.632812 -6.015625 2.785156 -6.285156 2.984375 -6.515625 C 3.191406 -6.753906 3.445312 -6.9375 3.75 -7.0625 C 4.050781 -7.195312 4.410156 -7.265625 4.828125 -7.265625 C 5.347656 -7.265625 5.757812 -7.113281 6.0625 -6.8125 C 6.363281 -6.519531 6.515625 -6.113281 6.515625 -5.59375 L 6.515625 0 L 7.875 0 L 7.875 -5.4375 C 7.875 -5.882812 7.828125 -6.289062 7.734375 -6.65625 C 7.640625 -7.03125 7.476562 -7.347656 7.25 -7.609375 C 7.03125 -7.878906 6.738281 -8.085938 6.375 -8.234375 C 6.019531 -8.390625 5.570312 -8.46875 5.03125 -8.46875 C 4.78125 -8.46875 4.523438 -8.4375 4.265625 -8.375 C 4.003906 -8.320312 3.753906 -8.238281 3.515625 -8.125 C 3.273438 -8.019531 3.054688 -7.878906 2.859375 -7.703125 C 2.671875 -7.523438 2.523438 -7.3125 2.421875 -7.0625 L 2.390625 -7.0625 L 2.390625 -11.421875 Z M 1.03125 -11.421875 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-12">
+<path style="stroke:none;" d="M 1.25 -11.421875 L 1.25 0 L 2.765625 0 L 2.765625 -5.234375 L 8.015625 -5.234375 L 8.015625 -6.515625 L 2.765625 -6.515625 L 2.765625 -10.140625 L 8.75 -10.140625 L 8.75 -11.421875 Z M 1.25 -11.421875 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-13">
+<path style="stroke:none;" d="M 2.46875 -9.765625 L 2.46875 -11.421875 L 1.109375 -11.421875 L 1.109375 -9.765625 Z M 1.109375 -8.265625 L 1.109375 0 L 2.46875 0 L 2.46875 -8.265625 Z M 1.109375 -8.265625 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-14">
+<path style="stroke:none;" d=""/>
+</symbol>
+<symbol overflow="visible" id="glyph0-15">
+<path style="stroke:none;" d="M 9.28125 -7.984375 L 10.796875 -7.984375 C 10.710938 -8.585938 10.53125 -9.117188 10.25 -9.578125 C 9.976562 -10.046875 9.632812 -10.4375 9.21875 -10.75 C 8.800781 -11.0625 8.320312 -11.296875 7.78125 -11.453125 C 7.25 -11.617188 6.6875 -11.703125 6.09375 -11.703125 C 5.21875 -11.703125 4.441406 -11.539062 3.765625 -11.21875 C 3.085938 -10.90625 2.519531 -10.476562 2.0625 -9.9375 C 1.613281 -9.394531 1.269531 -8.753906 1.03125 -8.015625 C 0.800781 -7.285156 0.6875 -6.507812 0.6875 -5.6875 C 0.6875 -4.851562 0.796875 -4.070312 1.015625 -3.34375 C 1.234375 -2.613281 1.5625 -1.984375 2 -1.453125 C 2.4375 -0.921875 2.984375 -0.503906 3.640625 -0.203125 C 4.304688 0.0976562 5.082031 0.25 5.96875 0.25 C 7.425781 0.25 8.578125 -0.144531 9.421875 -0.9375 C 10.265625 -1.738281 10.757812 -2.859375 10.90625 -4.296875 L 9.390625 -4.296875 C 9.359375 -3.828125 9.257812 -3.390625 9.09375 -2.984375 C 8.9375 -2.585938 8.71875 -2.238281 8.4375 -1.9375 C 8.15625 -1.644531 7.816406 -1.414062 7.421875 -1.25 C 7.035156 -1.09375 6.59375 -1.015625 6.09375 -1.015625 C 5.414062 -1.015625 4.828125 -1.140625 4.328125 -1.390625 C 3.835938 -1.648438 3.4375 -1.992188 3.125 -2.421875 C 2.8125 -2.859375 2.578125 -3.363281 2.421875 -3.9375 C 2.273438 -4.519531 2.203125 -5.140625 2.203125 -5.796875 C 2.203125 -6.390625 2.273438 -6.960938 2.421875 -7.515625 C 2.578125 -8.078125 2.8125 -8.570312 3.125 -9 C 3.4375 -9.425781 3.835938 -9.769531 4.328125 -10.03125 C 4.816406 -10.289062 5.398438 -10.421875 6.078125 -10.421875 C 6.878906 -10.421875 7.570312 -10.21875 8.15625 -9.8125 C 8.738281 -9.40625 9.113281 -8.796875 9.28125 -7.984375 Z M 9.28125 -7.984375 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-16">
+<path style="stroke:none;" d="M 7.859375 -8.078125 L 9.296875 -8.078125 C 9.273438 -8.710938 9.15625 -9.253906 8.9375 -9.703125 C 8.71875 -10.160156 8.414062 -10.535156 8.03125 -10.828125 C 7.65625 -11.128906 7.21875 -11.347656 6.71875 -11.484375 C 6.21875 -11.628906 5.675781 -11.703125 5.09375 -11.703125 C 4.5625 -11.703125 4.046875 -11.632812 3.546875 -11.5 C 3.054688 -11.363281 2.613281 -11.160156 2.21875 -10.890625 C 1.832031 -10.617188 1.519531 -10.269531 1.28125 -9.84375 C 1.050781 -9.425781 0.9375 -8.929688 0.9375 -8.359375 C 0.9375 -7.828125 1.039062 -7.390625 1.25 -7.046875 C 1.457031 -6.703125 1.734375 -6.421875 2.078125 -6.203125 C 2.429688 -5.984375 2.828125 -5.804688 3.265625 -5.671875 C 3.703125 -5.535156 4.144531 -5.414062 4.59375 -5.3125 C 5.050781 -5.21875 5.5 -5.117188 5.9375 -5.015625 C 6.375 -4.921875 6.765625 -4.796875 7.109375 -4.640625 C 7.453125 -4.492188 7.726562 -4.296875 7.9375 -4.046875 C 8.144531 -3.804688 8.25 -3.488281 8.25 -3.09375 C 8.25 -2.675781 8.164062 -2.332031 8 -2.0625 C 7.832031 -1.789062 7.609375 -1.578125 7.328125 -1.421875 C 7.046875 -1.273438 6.734375 -1.171875 6.390625 -1.109375 C 6.046875 -1.046875 5.703125 -1.015625 5.359375 -1.015625 C 4.929688 -1.015625 4.515625 -1.066406 4.109375 -1.171875 C 3.703125 -1.273438 3.347656 -1.4375 3.046875 -1.65625 C 2.742188 -1.882812 2.5 -2.171875 2.3125 -2.515625 C 2.125 -2.867188 2.03125 -3.285156 2.03125 -3.765625 L 0.59375 -3.765625 C 0.59375 -3.066406 0.71875 -2.460938 0.96875 -1.953125 C 1.21875 -1.453125 1.554688 -1.035156 1.984375 -0.703125 C 2.421875 -0.378906 2.925781 -0.140625 3.5 0.015625 C 4.070312 0.171875 4.675781 0.25 5.3125 0.25 C 5.832031 0.25 6.359375 0.1875 6.890625 0.0625 C 7.421875 -0.0507812 7.894531 -0.242188 8.3125 -0.515625 C 8.738281 -0.785156 9.085938 -1.132812 9.359375 -1.5625 C 9.640625 -2 9.78125 -2.523438 9.78125 -3.140625 C 9.78125 -3.703125 9.675781 -4.171875 9.46875 -4.546875 C 9.257812 -4.921875 8.976562 -5.226562 8.625 -5.46875 C 8.28125 -5.71875 7.890625 -5.910156 7.453125 -6.046875 C 7.015625 -6.191406 6.566406 -6.316406 6.109375 -6.421875 C 5.660156 -6.535156 5.21875 -6.632812 4.78125 -6.71875 C 4.34375 -6.8125 3.953125 -6.925781 3.609375 -7.0625 C 3.265625 -7.207031 2.988281 -7.390625 2.78125 -7.609375 C 2.570312 -7.828125 2.46875 -8.113281 2.46875 -8.46875 C 2.46875 -8.84375 2.535156 -9.15625 2.671875 -9.40625 C 2.816406 -9.65625 3.007812 -9.851562 3.25 -10 C 3.488281 -10.144531 3.765625 -10.25 4.078125 -10.3125 C 4.390625 -10.382812 4.707031 -10.421875 5.03125 -10.421875 C 5.8125 -10.421875 6.457031 -10.234375 6.96875 -9.859375 C 7.476562 -9.492188 7.773438 -8.898438 7.859375 -8.078125 Z M 7.859375 -8.078125 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-17">
+<path style="stroke:none;" d="M 1.25 -11.421875 L 1.25 0 L 8.8125 0 L 8.8125 -1.28125 L 2.765625 -1.28125 L 2.765625 -11.421875 Z M 1.25 -11.421875 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-18">
+<path style="stroke:none;" d="M 1.078125 -8.265625 L 1.078125 3.15625 L 2.4375 3.15625 L 2.4375 -1.109375 L 2.46875 -1.109375 C 2.613281 -0.859375 2.796875 -0.648438 3.015625 -0.484375 C 3.234375 -0.316406 3.460938 -0.1875 3.703125 -0.09375 C 3.953125 0 4.203125 0.0664062 4.453125 0.109375 C 4.703125 0.148438 4.929688 0.171875 5.140625 0.171875 C 5.765625 0.171875 6.3125 0.0625 6.78125 -0.15625 C 7.257812 -0.382812 7.65625 -0.691406 7.96875 -1.078125 C 8.289062 -1.460938 8.523438 -1.914062 8.671875 -2.4375 C 8.828125 -2.96875 8.90625 -3.523438 8.90625 -4.109375 C 8.90625 -4.691406 8.828125 -5.242188 8.671875 -5.765625 C 8.515625 -6.296875 8.273438 -6.757812 7.953125 -7.15625 C 7.640625 -7.5625 7.242188 -7.878906 6.765625 -8.109375 C 6.296875 -8.347656 5.742188 -8.46875 5.109375 -8.46875 C 4.523438 -8.46875 3.992188 -8.363281 3.515625 -8.15625 C 3.035156 -7.945312 2.6875 -7.613281 2.46875 -7.15625 L 2.4375 -7.15625 L 2.4375 -8.265625 Z M 7.46875 -4.203125 C 7.46875 -3.796875 7.425781 -3.398438 7.34375 -3.015625 C 7.257812 -2.640625 7.117188 -2.300781 6.921875 -2 C 6.734375 -1.695312 6.484375 -1.457031 6.171875 -1.28125 C 5.859375 -1.101562 5.460938 -1.015625 4.984375 -1.015625 C 4.515625 -1.015625 4.113281 -1.097656 3.78125 -1.265625 C 3.457031 -1.441406 3.191406 -1.675781 2.984375 -1.96875 C 2.773438 -2.257812 2.625 -2.59375 2.53125 -2.96875 C 2.4375 -3.34375 2.390625 -3.734375 2.390625 -4.140625 C 2.390625 -4.523438 2.429688 -4.90625 2.515625 -5.28125 C 2.609375 -5.65625 2.753906 -5.988281 2.953125 -6.28125 C 3.160156 -6.570312 3.421875 -6.804688 3.734375 -6.984375 C 4.054688 -7.171875 4.445312 -7.265625 4.90625 -7.265625 C 5.34375 -7.265625 5.722656 -7.175781 6.046875 -7 C 6.378906 -6.832031 6.648438 -6.601562 6.859375 -6.3125 C 7.066406 -6.03125 7.21875 -5.703125 7.3125 -5.328125 C 7.414062 -4.960938 7.46875 -4.585938 7.46875 -4.203125 Z M 7.46875 -4.203125 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-19">
+<path style="stroke:none;" d="M 1.25 -11.421875 L 1.25 0 L 2.765625 0 L 2.765625 -4.875 L 6.484375 -4.875 C 6.859375 -4.875 7.15625 -4.816406 7.375 -4.703125 C 7.601562 -4.597656 7.785156 -4.453125 7.921875 -4.265625 C 8.054688 -4.078125 8.15625 -3.859375 8.21875 -3.609375 C 8.28125 -3.359375 8.335938 -3.09375 8.390625 -2.8125 C 8.441406 -2.539062 8.472656 -2.257812 8.484375 -1.96875 C 8.492188 -1.675781 8.503906 -1.40625 8.515625 -1.15625 C 8.523438 -0.90625 8.546875 -0.675781 8.578125 -0.46875 C 8.617188 -0.269531 8.691406 -0.113281 8.796875 0 L 10.5 0 C 10.332031 -0.1875 10.207031 -0.40625 10.125 -0.65625 C 10.050781 -0.914062 9.992188 -1.179688 9.953125 -1.453125 C 9.910156 -1.734375 9.882812 -2.015625 9.875 -2.296875 C 9.863281 -2.585938 9.847656 -2.875 9.828125 -3.15625 C 9.796875 -3.425781 9.75 -3.691406 9.6875 -3.953125 C 9.625 -4.210938 9.53125 -4.441406 9.40625 -4.640625 C 9.289062 -4.847656 9.128906 -5.023438 8.921875 -5.171875 C 8.710938 -5.328125 8.441406 -5.4375 8.109375 -5.5 L 8.109375 -5.53125 C 8.804688 -5.726562 9.3125 -6.085938 9.625 -6.609375 C 9.9375 -7.128906 10.09375 -7.738281 10.09375 -8.4375 C 10.09375 -9.363281 9.785156 -10.09375 9.171875 -10.625 C 8.554688 -11.15625 7.707031 -11.421875 6.625 -11.421875 Z M 5.9375 -6.15625 L 2.765625 -6.15625 L 2.765625 -10.140625 L 6.546875 -10.140625 C 7.253906 -10.140625 7.769531 -9.957031 8.09375 -9.59375 C 8.414062 -9.238281 8.578125 -8.769531 8.578125 -8.1875 C 8.578125 -7.769531 8.503906 -7.429688 8.359375 -7.171875 C 8.210938 -6.910156 8.019531 -6.703125 7.78125 -6.546875 C 7.539062 -6.390625 7.257812 -6.285156 6.9375 -6.234375 C 6.625 -6.179688 6.289062 -6.15625 5.9375 -6.15625 Z M 5.9375 -6.15625 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-20">
+<path style="stroke:none;" d="M 8.15625 -0.703125 L 8.15625 -8.265625 L 6.875 -8.265625 L 6.875 -7.09375 L 6.859375 -7.09375 C 6.617188 -7.550781 6.28125 -7.894531 5.84375 -8.125 C 5.40625 -8.351562 4.925781 -8.46875 4.40625 -8.46875 C 3.6875 -8.46875 3.082031 -8.328125 2.59375 -8.046875 C 2.101562 -7.773438 1.707031 -7.429688 1.40625 -7.015625 C 1.101562 -6.597656 0.890625 -6.128906 0.765625 -5.609375 C 0.640625 -5.085938 0.578125 -4.582031 0.578125 -4.09375 C 0.578125 -3.53125 0.65625 -2.992188 0.8125 -2.484375 C 0.96875 -1.984375 1.195312 -1.539062 1.5 -1.15625 C 1.8125 -0.78125 2.195312 -0.476562 2.65625 -0.25 C 3.113281 -0.03125 3.648438 0.078125 4.265625 0.078125 C 4.804688 0.078125 5.3125 -0.0390625 5.78125 -0.28125 C 6.257812 -0.519531 6.613281 -0.894531 6.84375 -1.40625 L 6.875 -1.40625 L 6.875 -0.859375 C 6.875 -0.398438 6.828125 0.015625 6.734375 0.390625 C 6.648438 0.773438 6.503906 1.101562 6.296875 1.375 C 6.097656 1.65625 5.84375 1.867188 5.53125 2.015625 C 5.226562 2.171875 4.851562 2.25 4.40625 2.25 C 4.175781 2.25 3.9375 2.222656 3.6875 2.171875 C 3.445312 2.128906 3.222656 2.054688 3.015625 1.953125 C 2.804688 1.847656 2.628906 1.707031 2.484375 1.53125 C 2.335938 1.363281 2.257812 1.15625 2.25 0.90625 L 0.890625 0.90625 C 0.910156 1.351562 1.023438 1.734375 1.234375 2.046875 C 1.453125 2.359375 1.722656 2.609375 2.046875 2.796875 C 2.378906 2.992188 2.742188 3.132812 3.140625 3.21875 C 3.546875 3.300781 3.9375 3.34375 4.3125 3.34375 C 5.632812 3.34375 6.601562 3.003906 7.21875 2.328125 C 7.84375 1.660156 8.15625 0.648438 8.15625 -0.703125 Z M 4.359375 -1.109375 C 3.910156 -1.109375 3.535156 -1.195312 3.234375 -1.375 C 2.929688 -1.5625 2.6875 -1.804688 2.5 -2.109375 C 2.320312 -2.421875 2.195312 -2.765625 2.125 -3.140625 C 2.050781 -3.515625 2.015625 -3.882812 2.015625 -4.25 C 2.015625 -4.644531 2.054688 -5.023438 2.140625 -5.390625 C 2.234375 -5.753906 2.378906 -6.070312 2.578125 -6.34375 C 2.773438 -6.625 3.03125 -6.847656 3.34375 -7.015625 C 3.65625 -7.179688 4.03125 -7.265625 4.46875 -7.265625 C 4.894531 -7.265625 5.253906 -7.175781 5.546875 -7 C 5.847656 -6.832031 6.09375 -6.609375 6.28125 -6.328125 C 6.46875 -6.046875 6.601562 -5.726562 6.6875 -5.375 C 6.769531 -5.019531 6.8125 -4.660156 6.8125 -4.296875 C 6.8125 -3.921875 6.765625 -3.539062 6.671875 -3.15625 C 6.585938 -2.769531 6.445312 -2.421875 6.25 -2.109375 C 6.0625 -1.804688 5.8125 -1.5625 5.5 -1.375 C 5.1875 -1.195312 4.804688 -1.109375 4.359375 -1.109375 Z M 4.359375 -1.109375 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-21">
+<path style="stroke:none;" d="M 2.90625 -8.265625 L 2.90625 -10.75 L 1.546875 -10.75 L 1.546875 -8.265625 L 0.140625 -8.265625 L 0.140625 -7.078125 L 1.546875 -7.078125 L 1.546875 -1.8125 C 1.546875 -1.425781 1.582031 -1.113281 1.65625 -0.875 C 1.738281 -0.644531 1.851562 -0.460938 2 -0.328125 C 2.15625 -0.203125 2.359375 -0.113281 2.609375 -0.0625 C 2.859375 -0.0195312 3.160156 0 3.515625 0 L 4.5625 0 L 4.5625 -1.203125 L 3.9375 -1.203125 C 3.71875 -1.203125 3.539062 -1.207031 3.40625 -1.21875 C 3.28125 -1.238281 3.175781 -1.273438 3.09375 -1.328125 C 3.019531 -1.378906 2.96875 -1.453125 2.9375 -1.546875 C 2.914062 -1.648438 2.90625 -1.78125 2.90625 -1.9375 L 2.90625 -7.078125 L 4.5625 -7.078125 L 4.5625 -8.265625 Z M 2.90625 -8.265625 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-22">
+<path style="stroke:none;" d="M 1.578125 -7.078125 L 1.578125 0 L 2.9375 0 L 2.9375 -7.078125 L 4.546875 -7.078125 L 4.546875 -8.265625 L 2.9375 -8.265625 L 2.9375 -9.421875 C 2.9375 -9.785156 3.023438 -10.03125 3.203125 -10.15625 C 3.390625 -10.289062 3.648438 -10.359375 3.984375 -10.359375 C 4.097656 -10.359375 4.222656 -10.347656 4.359375 -10.328125 C 4.503906 -10.304688 4.632812 -10.273438 4.75 -10.234375 L 4.75 -11.421875 C 4.625 -11.460938 4.476562 -11.492188 4.3125 -11.515625 C 4.144531 -11.535156 4 -11.546875 3.875 -11.546875 C 3.125 -11.546875 2.550781 -11.375 2.15625 -11.03125 C 1.769531 -10.6875 1.578125 -10.175781 1.578125 -9.5 L 1.578125 -8.265625 L 0.1875 -8.265625 L 0.1875 -7.078125 Z M 1.578125 -7.078125 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-23">
+<path style="stroke:none;" d="M 7.0625 -2.84375 L 7.0625 -11.421875 L 5.53125 -11.421875 L 5.53125 -3.078125 C 5.53125 -2.441406 5.398438 -1.9375 5.140625 -1.5625 C 4.878906 -1.195312 4.40625 -1.015625 3.71875 -1.015625 C 3.34375 -1.015625 3.035156 -1.066406 2.796875 -1.171875 C 2.554688 -1.285156 2.367188 -1.441406 2.234375 -1.640625 C 2.097656 -1.847656 2.003906 -2.085938 1.953125 -2.359375 C 1.898438 -2.640625 1.875 -2.945312 1.875 -3.28125 L 1.875 -3.765625 L 0.359375 -3.765625 L 0.359375 -3.0625 C 0.359375 -1.96875 0.644531 -1.140625 1.21875 -0.578125 C 1.789062 -0.0234375 2.613281 0.25 3.6875 0.25 C 4.320312 0.25 4.851562 0.164062 5.28125 0 C 5.71875 -0.175781 6.066406 -0.410156 6.328125 -0.703125 C 6.585938 -1.003906 6.773438 -1.335938 6.890625 -1.703125 C 7.003906 -2.078125 7.0625 -2.457031 7.0625 -2.84375 Z M 7.0625 -2.84375 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-24">
+<path style="stroke:none;" d="M 7.875 0 L 7.875 -8.265625 L 6.515625 -8.265625 L 6.515625 -3.59375 C 6.515625 -3.226562 6.460938 -2.882812 6.359375 -2.5625 C 6.253906 -2.25 6.097656 -1.972656 5.890625 -1.734375 C 5.691406 -1.503906 5.441406 -1.328125 5.140625 -1.203125 C 4.835938 -1.078125 4.476562 -1.015625 4.0625 -1.015625 C 3.539062 -1.015625 3.128906 -1.160156 2.828125 -1.453125 C 2.535156 -1.753906 2.390625 -2.160156 2.390625 -2.671875 L 2.390625 -8.265625 L 1.03125 -8.265625 L 1.03125 -2.828125 C 1.03125 -2.378906 1.070312 -1.972656 1.15625 -1.609375 C 1.25 -1.242188 1.40625 -0.925781 1.625 -0.65625 C 1.851562 -0.382812 2.148438 -0.175781 2.515625 -0.03125 C 2.878906 0.101562 3.332031 0.171875 3.875 0.171875 C 4.476562 0.171875 5.003906 0.0507812 5.453125 -0.1875 C 5.898438 -0.425781 6.269531 -0.800781 6.5625 -1.3125 L 6.59375 -1.3125 L 6.59375 0 Z M 7.875 0 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-25">
+<path style="stroke:none;" d="M 5.703125 0 L 5.703125 -11.34375 L 4.65625 -11.34375 C 4.582031 -10.914062 4.441406 -10.5625 4.234375 -10.28125 C 4.035156 -10.007812 3.789062 -9.789062 3.5 -9.625 C 3.207031 -9.46875 2.878906 -9.359375 2.515625 -9.296875 C 2.148438 -9.242188 1.773438 -9.21875 1.390625 -9.21875 L 1.390625 -8.125 L 4.34375 -8.125 L 4.34375 0 Z M 5.703125 0 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-26">
+<path style="stroke:none;" d="M 3.265625 3.15625 L 4.296875 3.15625 C 3.546875 1.925781 3.003906 0.710938 2.671875 -0.484375 C 2.347656 -1.691406 2.1875 -2.96875 2.1875 -4.3125 C 2.1875 -5.625 2.347656 -6.878906 2.671875 -8.078125 C 2.992188 -9.273438 3.535156 -10.484375 4.296875 -11.703125 L 3.265625 -11.703125 C 2.429688 -10.597656 1.800781 -9.40625 1.375 -8.125 C 0.957031 -6.84375 0.75 -5.570312 0.75 -4.3125 C 0.75 -3.613281 0.804688 -2.941406 0.921875 -2.296875 C 1.046875 -1.660156 1.21875 -1.035156 1.4375 -0.421875 C 1.65625 0.179688 1.914062 0.773438 2.21875 1.359375 C 2.53125 1.953125 2.878906 2.550781 3.265625 3.15625 Z M 3.265625 3.15625 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-27">
+<path style="stroke:none;" d="M 1.109375 -11.421875 L 1.109375 0 L 2.46875 0 L 2.46875 -3.140625 L 3.75 -4.3125 L 6.578125 0 L 8.296875 0 L 4.78125 -5.265625 L 8.0625 -8.265625 L 6.234375 -8.265625 L 2.46875 -4.65625 L 2.46875 -11.421875 Z M 1.109375 -11.421875 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-28">
+<path style="stroke:none;" d="M 4.265625 1.109375 C 4.109375 1.515625 3.953125 1.851562 3.796875 2.125 C 3.640625 2.40625 3.46875 2.632812 3.28125 2.8125 C 3.101562 2.988281 2.894531 3.113281 2.65625 3.1875 C 2.425781 3.269531 2.164062 3.3125 1.875 3.3125 C 1.707031 3.3125 1.546875 3.300781 1.390625 3.28125 C 1.234375 3.257812 1.078125 3.222656 0.921875 3.171875 L 0.921875 1.921875 C 1.046875 1.972656 1.179688 2.015625 1.328125 2.046875 C 1.484375 2.085938 1.617188 2.109375 1.734375 2.109375 C 2.003906 2.109375 2.234375 2.039062 2.421875 1.90625 C 2.609375 1.78125 2.75 1.59375 2.84375 1.34375 L 3.40625 -0.046875 L 0.125 -8.265625 L 1.65625 -8.265625 L 4.078125 -1.5 L 4.109375 -1.5 L 6.4375 -8.265625 L 7.875 -8.265625 Z M 4.265625 1.109375 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-29">
+<path style="stroke:none;" d="M -0.140625 3.15625 L 0.875 3.15625 C 1.707031 2.050781 2.332031 0.863281 2.75 -0.40625 C 3.175781 -1.675781 3.390625 -2.941406 3.390625 -4.203125 C 3.390625 -4.910156 3.332031 -5.582031 3.21875 -6.21875 C 3.101562 -6.863281 2.9375 -7.492188 2.71875 -8.109375 C 2.5 -8.722656 2.234375 -9.320312 1.921875 -9.90625 C 1.609375 -10.5 1.257812 -11.097656 0.875 -11.703125 L -0.140625 -11.703125 C 0.597656 -10.472656 1.128906 -9.25 1.453125 -8.03125 C 1.785156 -6.820312 1.953125 -5.546875 1.953125 -4.203125 C 1.953125 -2.898438 1.789062 -1.648438 1.46875 -0.453125 C 1.144531 0.742188 0.609375 1.945312 -0.140625 3.15625 Z M -0.140625 3.15625 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-30">
+<path style="stroke:none;" d="M 3.25 -4.359375 L 0.140625 0 L 1.796875 0 L 4.09375 -3.421875 L 6.40625 0 L 8.140625 0 L 4.9375 -4.46875 L 7.796875 -8.265625 L 6.15625 -8.265625 L 4.09375 -5.375 L 2.109375 -8.265625 L 0.375 -8.265625 Z M 3.25 -4.359375 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-31">
+<path style="stroke:none;" d="M 9.796875 -1.421875 L 10.1875 0 L 11.15625 0 L 11.15625 -6.015625 L 6.140625 -6.015625 L 6.140625 -4.734375 L 9.796875 -4.734375 C 9.816406 -4.210938 9.742188 -3.722656 9.578125 -3.265625 C 9.421875 -2.816406 9.1875 -2.421875 8.875 -2.078125 C 8.5625 -1.742188 8.175781 -1.484375 7.71875 -1.296875 C 7.257812 -1.109375 6.726562 -1.015625 6.125 -1.015625 C 5.488281 -1.015625 4.925781 -1.140625 4.4375 -1.390625 C 3.957031 -1.640625 3.550781 -1.972656 3.21875 -2.390625 C 2.882812 -2.816406 2.628906 -3.300781 2.453125 -3.84375 C 2.285156 -4.394531 2.203125 -4.96875 2.203125 -5.5625 C 2.203125 -6.175781 2.273438 -6.769531 2.421875 -7.34375 C 2.578125 -7.925781 2.8125 -8.441406 3.125 -8.890625 C 3.4375 -9.347656 3.84375 -9.71875 4.34375 -10 C 4.84375 -10.28125 5.4375 -10.421875 6.125 -10.421875 C 6.550781 -10.421875 6.953125 -10.367188 7.328125 -10.265625 C 7.710938 -10.160156 8.050781 -10.003906 8.34375 -9.796875 C 8.644531 -9.597656 8.894531 -9.34375 9.09375 -9.03125 C 9.300781 -8.71875 9.441406 -8.34375 9.515625 -7.90625 L 11.046875 -7.90625 C 10.929688 -8.570312 10.726562 -9.144531 10.4375 -9.625 C 10.144531 -10.101562 9.78125 -10.492188 9.34375 -10.796875 C 8.914062 -11.109375 8.425781 -11.335938 7.875 -11.484375 C 7.332031 -11.628906 6.75 -11.703125 6.125 -11.703125 C 5.21875 -11.703125 4.425781 -11.53125 3.75 -11.1875 C 3.070312 -10.851562 2.503906 -10.398438 2.046875 -9.828125 C 1.597656 -9.265625 1.257812 -8.609375 1.03125 -7.859375 C 0.800781 -7.109375 0.6875 -6.316406 0.6875 -5.484375 C 0.6875 -4.742188 0.804688 -4.023438 1.046875 -3.328125 C 1.296875 -2.628906 1.65625 -2.015625 2.125 -1.484375 C 2.59375 -0.953125 3.160156 -0.53125 3.828125 -0.21875 C 4.503906 0.09375 5.269531 0.25 6.125 0.25 C 6.800781 0.25 7.46875 0.117188 8.125 -0.140625 C 8.789062 -0.398438 9.347656 -0.828125 9.796875 -1.421875 Z M 9.796875 -1.421875 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-32">
+<path style="stroke:none;" d="M 0.796875 -5.09375 L 0.796875 -3.8125 L 5.421875 -3.8125 L 5.421875 -5.09375 Z M 0.796875 -5.09375 "/>
+</symbol>
+</g>
+</defs>
+<g id="surface1">
+<path style="fill:none;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 423 288 L 468 288 L 468 540 L 423 540 M 153 540 L 108 540 L 108 288 L 153 288 " transform="matrix(1,0,0,1,-89,-70)"/>
+<path style="fill:none;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 274.511719 239.199219 L 234 288 L 135 288 " transform="matrix(1,0,0,1,-89,-70)"/>
+<path style="fill:none;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 299.90625 239.199219 L 342 288 L 468 288 " transform="matrix(1,0,0,1,-89,-70)"/>
+<path style="fill:none;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 108 540 L 468 540 " transform="matrix(1,0,0,1,-89,-70)"/>
+<path style="fill-rule:nonzero;fill:rgb(100%,100%,100%);fill-opacity:1;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 338.910156 82.542969 C 367.03125 96.601562 367.03125 119.398438 338.910156 133.457031 C 310.792969 147.515625 265.207031 147.515625 237.089844 133.457031 C 208.96875 119.398438 208.96875 96.601562 237.089844 82.542969 C 265.207031 68.484375 310.792969 68.484375 338.910156 82.542969 " transform="matrix(1,0,0,1,-89,-70)"/>
+<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-1" x="166.256" y="43.776001"/>
+  <use xlink:href="#glyph0-2" x="174.544" y="43.776001"/>
+  <use xlink:href="#glyph0-3" x="183.44" y="43.776001"/>
+  <use xlink:href="#glyph0-4" x="192.928" y="43.776001"/>
+  <use xlink:href="#glyph0-5" x="204.48" y="43.776001"/>
+  <use xlink:href="#glyph0-3" x="213.664" y="43.776001"/>
+  <use xlink:href="#glyph0-6" x="223.152" y="43.776001"/>
+</g>
+<path style="fill:none;stroke-width:2;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 265.597656 154.90625 C 260.976562 167.921875 258.246094 180.738281 261 189 C 268.648438 211.949219 307.351562 211.949219 315 189 C 318.605469 178.183594 312.8125 159.5625 305.679688 142.902344 " transform="matrix(1,0,0,1,-89,-70)"/>
+<path style="fill-rule:nonzero;fill:rgb(0%,0%,0%);fill-opacity:1;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 269.113281 145.972656 L 262.246094 153.589844 L 268.945312 156.226562 Z M 269.113281 145.972656 " transform="matrix(1,0,0,1,-89,-70)"/>
+<path style="fill-rule:nonzero;fill:rgb(100%,100%,100%);fill-opacity:1;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 338.910156 307.542969 C 367.03125 321.601562 367.03125 344.398438 338.910156 358.457031 C 310.792969 372.515625 265.207031 372.515625 237.089844 358.457031 C 208.96875 344.398438 208.96875 321.601562 237.089844 307.542969 C 265.207031 293.484375 310.792969 293.484375 338.910156 307.542969 " transform="matrix(1,0,0,1,-89,-70)"/>
+<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-7" x="155.736" y="268.776001"/>
+  <use xlink:href="#glyph0-6" x="163.736" y="268.776001"/>
+  <use xlink:href="#glyph0-8" x="172.328" y="268.776001"/>
+  <use xlink:href="#glyph0-9" x="180.92" y="268.776001"/>
+</g>
+<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-10" x="185.96" y="268.776001"/>
+  <use xlink:href="#glyph0-11" x="194.552" y="268.776001"/>
+  <use xlink:href="#glyph0-4" x="203.448" y="268.776001"/>
+  <use xlink:href="#glyph0-5" x="215" y="268.776001"/>
+  <use xlink:href="#glyph0-3" x="224.184" y="268.776001"/>
+  <use xlink:href="#glyph0-6" x="233.672" y="268.776001"/>
+</g>
+<path style="fill:none;stroke-width:2;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 233.070312 356.277344 C 219.59375 360.355469 206.585938 362.574219 198 360 C 172.503906 352.351562 172.503906 313.648438 198 306 C 203.875 304.238281 211.824219 304.722656 220.574219 306.507812 " transform="matrix(1,0,0,1,-89,-70)"/>
+<path style="fill-rule:nonzero;fill:rgb(0%,0%,0%);fill-opacity:1;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 229.875 308.902344 L 221.472656 303.023438 L 219.679688 309.996094 Z M 229.875 308.902344 " transform="matrix(1,0,0,1,-89,-70)"/>
+<path style="fill:none;stroke-width:2;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 356.242188 307.183594 C 364.671875 305.632812 372.308594 305.324219 378 307.101562 C 403.496094 315.066406 403.496094 353.765625 378 361.101562 C 369.253906 363.617188 355.921875 361.105469 342.179688 356.710938 " transform="matrix(1,0,0,1,-89,-70)"/>
+<path style="fill-rule:nonzero;fill:rgb(0%,0%,0%);fill-opacity:1;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 346.898438 309.410156 L 357.070312 310.683594 L 355.402344 303.679688 Z M 346.898438 309.410156 " transform="matrix(1,0,0,1,-89,-70)"/>
+<path style="fill-rule:nonzero;fill:rgb(100%,100%,100%);fill-opacity:1;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 437.910156 442.542969 C 466.03125 456.601562 466.03125 479.398438 437.910156 493.457031 C 409.792969 507.515625 364.207031 507.515625 336.089844 493.457031 C 307.96875 479.398438 307.96875 456.601562 336.089844 442.542969 C 364.207031 428.484375 409.792969 428.484375 437.910156 442.542969 " transform="matrix(1,0,0,1,-89,-70)"/>
+<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-12" x="261.848" y="403.776001"/>
+  <use xlink:href="#glyph0-13" x="271.032" y="403.776001"/>
+  <use xlink:href="#glyph0-2" x="274.584" y="403.776001"/>
+  <use xlink:href="#glyph0-3" x="283.48" y="403.776001"/>
+  <use xlink:href="#glyph0-14" x="292.968" y="403.776001"/>
+  <use xlink:href="#glyph0-15" x="297.416" y="403.776001"/>
+  <use xlink:href="#glyph0-8" x="308.968" y="403.776001"/>
+  <use xlink:href="#glyph0-7" x="317.56" y="403.776001"/>
+  <use xlink:href="#glyph0-6" x="325.56" y="403.776001"/>
+</g>
+<path style="fill:none;stroke-width:2;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 312.792969 366.808594 L 354.578125 423.789062 " transform="matrix(1,0,0,1,-89,-70)"/>
+<path style="fill-rule:nonzero;fill:rgb(0%,0%,0%);fill-opacity:1;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 360.257812 431.53125 L 357.480469 421.660156 L 351.675781 425.917969 Z M 360.257812 431.53125 " transform="matrix(1,0,0,1,-89,-70)"/>
+<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-16" x="152.3251" y="159.976701"/>
+  <use xlink:href="#glyph0-6" x="162.6931" y="159.976701"/>
+  <use xlink:href="#glyph0-8" x="171.2851" y="159.976701"/>
+  <use xlink:href="#glyph0-9" x="179.8771" y="159.976701"/>
+</g>
+<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-10" x="184.9171" y="159.976701"/>
+  <use xlink:href="#glyph0-11" x="193.5091" y="159.976701"/>
+  <use xlink:href="#glyph0-14" x="202.4051" y="159.976701"/>
+  <use xlink:href="#glyph0-17" x="206.8531" y="159.976701"/>
+  <use xlink:href="#glyph0-5" x="215.7491" y="159.976701"/>
+  <use xlink:href="#glyph0-5" x="224.9331" y="159.976701"/>
+  <use xlink:href="#glyph0-18" x="234.1171" y="159.976701"/>
+</g>
+<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-19" x="48.184" y="267.776001"/>
+  <use xlink:href="#glyph0-13" x="59.144" y="267.776001"/>
+  <use xlink:href="#glyph0-20" x="62.696" y="267.776001"/>
+  <use xlink:href="#glyph0-11" x="71.88" y="267.776001"/>
+  <use xlink:href="#glyph0-21" x="80.776" y="267.776001"/>
+</g>
+<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-17" x="314.4736" y="267.776001"/>
+  <use xlink:href="#glyph0-6" x="323.3696" y="267.776001"/>
+  <use xlink:href="#glyph0-22" x="331.9616" y="267.776001"/>
+  <use xlink:href="#glyph0-21" x="336.6976" y="267.776001"/>
+</g>
+<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-23" x="256.0363" y="325.776001"/>
+  <use xlink:href="#glyph0-24" x="264.3403" y="325.776001"/>
+  <use xlink:href="#glyph0-7" x="273.2363" y="325.776001"/>
+  <use xlink:href="#glyph0-21" x="281.2363" y="325.776001"/>
+  <use xlink:href="#glyph0-14" x="286.2763" y="325.776001"/>
+  <use xlink:href="#glyph0-25" x="290.7243" y="325.776001"/>
+</g>
+<path style="fill:none;stroke-width:2;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 144 108 L 203.101562 108 " transform="matrix(1,0,0,1,-89,-70)"/>
+<path style="fill-rule:nonzero;fill:rgb(0%,0%,0%);fill-opacity:1;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 212.699219 108 L 203.101562 104.398438 L 203.101562 111.601562 Z M 212.699219 108 " transform="matrix(1,0,0,1,-89,-70)"/>
+<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-4" x="5.6145" y="25.776001"/>
+  <use xlink:href="#glyph0-5" x="17.1665" y="25.776001"/>
+  <use xlink:href="#glyph0-3" x="26.3505" y="25.776001"/>
+  <use xlink:href="#glyph0-6" x="35.8385" y="25.776001"/>
+  <use xlink:href="#glyph0-26" x="44.4305" y="25.776001"/>
+  <use xlink:href="#glyph0-27" x="48.5745" y="25.776001"/>
+  <use xlink:href="#glyph0-6" x="56.8785" y="25.776001"/>
+  <use xlink:href="#glyph0-28" x="65.4705" y="25.776001"/>
+  <use xlink:href="#glyph0-25" x="73.4705" y="25.776001"/>
+  <use xlink:href="#glyph0-29" x="82.3665" y="25.776001"/>
+</g>
+<path style="fill-rule:nonzero;fill:rgb(100%,100%,100%);fill-opacity:1;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 554.910156 82.542969 C 583.03125 96.601562 583.03125 119.398438 554.910156 133.457031 C 526.792969 147.515625 481.207031 147.515625 453.089844 133.457031 C 424.96875 119.398438 424.96875 96.601562 453.089844 82.542969 C 481.207031 68.484375 526.792969 68.484375 554.910156 82.542969 " transform="matrix(1,0,0,1,-89,-70)"/>
+<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-2" x="362.856" y="43.776001"/>
+  <use xlink:href="#glyph0-6" x="371.752" y="43.776001"/>
+  <use xlink:href="#glyph0-30" x="380.344" y="43.776001"/>
+  <use xlink:href="#glyph0-21" x="388.632" y="43.776001"/>
+  <use xlink:href="#glyph0-15" x="393.672" y="43.776001"/>
+  <use xlink:href="#glyph0-5" x="405.224" y="43.776001"/>
+  <use xlink:href="#glyph0-3" x="414.408" y="43.776001"/>
+  <use xlink:href="#glyph0-6" x="423.896" y="43.776001"/>
+  <use xlink:href="#glyph0-31" x="432.488" y="43.776001"/>
+  <use xlink:href="#glyph0-6" x="444.632" y="43.776001"/>
+  <use xlink:href="#glyph0-8" x="453.224" y="43.776001"/>
+  <use xlink:href="#glyph0-9" x="461.816" y="43.776001"/>
+</g>
+<path style="fill:none;stroke-width:2;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-dasharray:8,8;stroke-miterlimit:10;" d="M 360 108 L 419.101562 108 " transform="matrix(1,0,0,1,-89,-70)"/>
+<path style="fill-rule:nonzero;fill:rgb(0%,0%,0%);fill-opacity:1;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 428.699219 108 L 419.101562 104.398438 L 419.101562 111.601562 Z M 428.699219 108 " transform="matrix(1,0,0,1,-89,-70)"/>
+<path style="fill-rule:nonzero;fill:rgb(100%,100%,100%);fill-opacity:1;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 248.910156 442.542969 C 277.03125 456.601562 277.03125 479.398438 248.910156 493.457031 C 220.792969 507.515625 175.207031 507.515625 147.089844 493.457031 C 118.96875 479.398438 118.96875 456.601562 147.089844 442.542969 C 175.207031 428.484375 220.792969 428.484375 248.910156 442.542969 " transform="matrix(1,0,0,1,-89,-70)"/>
+<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-4" x="57.736" y="403.776001"/>
+  <use xlink:href="#glyph0-5" x="69.288" y="403.776001"/>
+  <use xlink:href="#glyph0-21" x="78.472" y="403.776001"/>
+  <use xlink:href="#glyph0-14" x="83.512" y="403.776001"/>
+  <use xlink:href="#glyph0-12" x="87.96" y="403.776001"/>
+  <use xlink:href="#glyph0-13" x="97.144" y="403.776001"/>
+  <use xlink:href="#glyph0-2" x="100.696" y="403.776001"/>
+  <use xlink:href="#glyph0-3" x="109.592" y="403.776001"/>
+  <use xlink:href="#glyph0-14" x="119.08" y="403.776001"/>
+  <use xlink:href="#glyph0-15" x="123.528" y="403.776001"/>
+  <use xlink:href="#glyph0-8" x="135.08" y="403.776001"/>
+  <use xlink:href="#glyph0-7" x="143.672" y="403.776001"/>
+  <use xlink:href="#glyph0-6" x="151.672" y="403.776001"/>
+</g>
+<path style="fill:none;stroke-width:2;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 265.226562 367.160156 L 227.929688 423.105469 " transform="matrix(1,0,0,1,-89,-70)"/>
+<path style="fill-rule:nonzero;fill:rgb(0%,0%,0%);fill-opacity:1;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 222.605469 431.09375 L 230.925781 425.101562 L 224.933594 421.109375 Z M 222.605469 431.09375 " transform="matrix(1,0,0,1,-89,-70)"/>
+<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-4" x="94.848" y="325.776001"/>
+  <use xlink:href="#glyph0-5" x="106.4" y="325.776001"/>
+  <use xlink:href="#glyph0-21" x="115.584" y="325.776001"/>
+  <use xlink:href="#glyph0-11" x="120.624" y="325.776001"/>
+  <use xlink:href="#glyph0-13" x="129.52" y="325.776001"/>
+  <use xlink:href="#glyph0-2" x="133.072" y="325.776001"/>
+  <use xlink:href="#glyph0-20" x="141.968" y="325.776001"/>
+</g>
+<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-18" x="24.136" y="91.776001"/>
+  <use xlink:href="#glyph0-9" x="33.624" y="91.776001"/>
+</g>
+<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-6" x="38.664" y="91.776001"/>
+  <use xlink:href="#glyph0-32" x="47.256" y="91.776001"/>
+  <use xlink:href="#glyph0-10" x="53.48" y="91.776001"/>
+  <use xlink:href="#glyph0-5" x="62.072" y="91.776001"/>
+  <use xlink:href="#glyph0-2" x="71.256" y="91.776001"/>
+  <use xlink:href="#glyph0-3" x="80.152" y="91.776001"/>
+  <use xlink:href="#glyph0-13" x="89.64" y="91.776001"/>
+  <use xlink:href="#glyph0-21" x="93.192" y="91.776001"/>
+  <use xlink:href="#glyph0-13" x="98.232" y="91.776001"/>
+  <use xlink:href="#glyph0-5" x="101.784" y="91.776001"/>
+  <use xlink:href="#glyph0-2" x="110.968" y="91.776001"/>
+</g>
+<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-18" x="264.84" y="91.776001"/>
+  <use xlink:href="#glyph0-5" x="274.328" y="91.776001"/>
+  <use xlink:href="#glyph0-7" x="283.512" y="91.776001"/>
+  <use xlink:href="#glyph0-21" x="291.512" y="91.776001"/>
+  <use xlink:href="#glyph0-32" x="296.552" y="91.776001"/>
+  <use xlink:href="#glyph0-10" x="302.776" y="91.776001"/>
+  <use xlink:href="#glyph0-5" x="311.368" y="91.776001"/>
+  <use xlink:href="#glyph0-2" x="320.552" y="91.776001"/>
+  <use xlink:href="#glyph0-3" x="329.448" y="91.776001"/>
+  <use xlink:href="#glyph0-13" x="338.936" y="91.776001"/>
+  <use xlink:href="#glyph0-21" x="342.488" y="91.776001"/>
+  <use xlink:href="#glyph0-13" x="347.528" y="91.776001"/>
+  <use xlink:href="#glyph0-5" x="351.08" y="91.776001"/>
+  <use xlink:href="#glyph0-2" x="360.264" y="91.776001"/>
+</g>
+</g>
+</svg>
--- a/Slide/fig/hoare-logic.xbb	Mon Apr 23 21:44:32 2018 +0900
+++ b/Slide/fig/hoare-logic.xbb	Sat May 19 19:14:19 2018 +0900
@@ -1,8 +1,8 @@
-%%Title: hoare-logic.pdf
-%%Creator: extractbb 20160307
+%%Title: fig/hoare-logic.pdf
+%%Creator: extractbb 20180217
 %%BoundingBox: 0 0 580 76
 %%HiResBoundingBox: 0.000000 0.000000 580.000000 76.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Wed Feb 21 01:38:18 2018
+%%CreationDate: Tue May 15 18:15:06 2018
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Slide/fig/meta.svg	Sat May 19 19:14:19 2018 +0900
@@ -0,0 +1,162 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<svg xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" width="958pt" height="148pt" viewBox="0 0 958 148" version="1.1">
+<defs>
+<g>
+<symbol overflow="visible" id="glyph0-0">
+<path style="stroke:none;" d="M 6.546875 -10.65625 L 1.625 -10.65625 L 1.625 -0.75 L 6.546875 -0.75 Z M 7.359375 -11.390625 L 7.359375 -0.015625 L 0.8125 -0.015625 L 0.8125 -11.390625 Z M 7.359375 -11.390625 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-1">
+<path style="stroke:none;" d="M 1.28125 -11.421875 L 1.28125 0 L 2.71875 0 L 2.71875 -9.5 L 2.75 -9.5 L 6.3125 0 L 7.609375 0 L 11.1875 -9.5 L 11.21875 -9.5 L 11.21875 0 L 12.65625 0 L 12.65625 -11.421875 L 10.578125 -11.421875 L 6.953125 -1.828125 L 3.359375 -11.421875 Z M 1.28125 -11.421875 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-2">
+<path style="stroke:none;" d="M 6.765625 -4.921875 L 2.015625 -4.921875 C 2.035156 -5.242188 2.101562 -5.546875 2.21875 -5.828125 C 2.34375 -6.109375 2.503906 -6.351562 2.703125 -6.5625 C 2.910156 -6.78125 3.15625 -6.953125 3.4375 -7.078125 C 3.71875 -7.203125 4.035156 -7.265625 4.390625 -7.265625 C 4.722656 -7.265625 5.03125 -7.203125 5.3125 -7.078125 C 5.601562 -6.953125 5.851562 -6.785156 6.0625 -6.578125 C 6.269531 -6.367188 6.429688 -6.117188 6.546875 -5.828125 C 6.671875 -5.546875 6.742188 -5.242188 6.765625 -4.921875 Z M 8.078125 -2.625 L 6.734375 -2.625 C 6.617188 -2.082031 6.375 -1.675781 6 -1.40625 C 5.632812 -1.144531 5.164062 -1.015625 4.59375 -1.015625 C 4.144531 -1.015625 3.753906 -1.085938 3.421875 -1.234375 C 3.085938 -1.378906 2.8125 -1.578125 2.59375 -1.828125 C 2.382812 -2.078125 2.234375 -2.363281 2.140625 -2.6875 C 2.046875 -3.019531 2.003906 -3.367188 2.015625 -3.734375 L 8.203125 -3.734375 C 8.222656 -4.234375 8.175781 -4.757812 8.0625 -5.3125 C 7.957031 -5.863281 7.757812 -6.375 7.46875 -6.84375 C 7.175781 -7.3125 6.785156 -7.695312 6.296875 -8 C 5.804688 -8.3125 5.195312 -8.46875 4.46875 -8.46875 C 3.894531 -8.46875 3.367188 -8.359375 2.890625 -8.140625 C 2.421875 -7.929688 2.015625 -7.632812 1.671875 -7.25 C 1.328125 -6.863281 1.054688 -6.410156 0.859375 -5.890625 C 0.671875 -5.367188 0.578125 -4.789062 0.578125 -4.15625 C 0.597656 -3.53125 0.691406 -2.945312 0.859375 -2.40625 C 1.023438 -1.875 1.269531 -1.414062 1.59375 -1.03125 C 1.925781 -0.65625 2.332031 -0.359375 2.8125 -0.140625 C 3.300781 0.0664062 3.878906 0.171875 4.546875 0.171875 C 5.484375 0.171875 6.257812 -0.0625 6.875 -0.53125 C 7.5 -1 7.898438 -1.695312 8.078125 -2.625 Z M 8.078125 -2.625 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-3">
+<path style="stroke:none;" d="M 2.90625 -8.265625 L 2.90625 -10.75 L 1.546875 -10.75 L 1.546875 -8.265625 L 0.140625 -8.265625 L 0.140625 -7.078125 L 1.546875 -7.078125 L 1.546875 -1.8125 C 1.546875 -1.425781 1.582031 -1.113281 1.65625 -0.875 C 1.738281 -0.644531 1.851562 -0.460938 2 -0.328125 C 2.15625 -0.203125 2.359375 -0.113281 2.609375 -0.0625 C 2.859375 -0.0195312 3.160156 0 3.515625 0 L 4.5625 0 L 4.5625 -1.203125 L 3.9375 -1.203125 C 3.71875 -1.203125 3.539062 -1.207031 3.40625 -1.21875 C 3.28125 -1.238281 3.175781 -1.273438 3.09375 -1.328125 C 3.019531 -1.378906 2.96875 -1.453125 2.9375 -1.546875 C 2.914062 -1.648438 2.90625 -1.78125 2.90625 -1.9375 L 2.90625 -7.078125 L 4.5625 -7.078125 L 4.5625 -8.265625 Z M 2.90625 -8.265625 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-4">
+<path style="stroke:none;" d="M 8.359375 -0.03125 C 8.117188 0.101562 7.789062 0.171875 7.375 0.171875 C 7.019531 0.171875 6.738281 0.0703125 6.53125 -0.125 C 6.320312 -0.320312 6.21875 -0.644531 6.21875 -1.09375 C 5.84375 -0.644531 5.40625 -0.320312 4.90625 -0.125 C 4.414062 0.0703125 3.882812 0.171875 3.3125 0.171875 C 2.9375 0.171875 2.582031 0.128906 2.25 0.046875 C 1.914062 -0.0351562 1.625 -0.164062 1.375 -0.34375 C 1.132812 -0.53125 0.941406 -0.769531 0.796875 -1.0625 C 0.648438 -1.351562 0.578125 -1.707031 0.578125 -2.125 C 0.578125 -2.59375 0.65625 -2.976562 0.8125 -3.28125 C 0.976562 -3.582031 1.191406 -3.820312 1.453125 -4 C 1.710938 -4.1875 2.007812 -4.328125 2.34375 -4.421875 C 2.675781 -4.523438 3.019531 -4.609375 3.375 -4.671875 C 3.75 -4.742188 4.101562 -4.796875 4.4375 -4.828125 C 4.769531 -4.867188 5.066406 -4.925781 5.328125 -5 C 5.585938 -5.070312 5.789062 -5.171875 5.9375 -5.296875 C 6.082031 -5.429688 6.15625 -5.628906 6.15625 -5.890625 C 6.15625 -6.191406 6.097656 -6.429688 5.984375 -6.609375 C 5.878906 -6.785156 5.738281 -6.921875 5.5625 -7.015625 C 5.382812 -7.117188 5.1875 -7.1875 4.96875 -7.21875 C 4.75 -7.25 4.53125 -7.265625 4.3125 -7.265625 C 3.738281 -7.265625 3.257812 -7.15625 2.875 -6.9375 C 2.488281 -6.71875 2.28125 -6.304688 2.25 -5.703125 L 0.890625 -5.703125 C 0.910156 -6.210938 1.015625 -6.640625 1.203125 -6.984375 C 1.398438 -7.335938 1.660156 -7.625 1.984375 -7.84375 C 2.304688 -8.0625 2.671875 -8.21875 3.078125 -8.3125 C 3.492188 -8.414062 3.9375 -8.46875 4.40625 -8.46875 C 4.769531 -8.46875 5.132812 -8.4375 5.5 -8.375 C 5.875 -8.320312 6.207031 -8.210938 6.5 -8.046875 C 6.800781 -7.890625 7.039062 -7.660156 7.21875 -7.359375 C 7.40625 -7.054688 7.5 -6.664062 7.5 -6.1875 L 7.5 -1.9375 C 7.5 -1.613281 7.515625 -1.378906 7.546875 -1.234375 C 7.585938 -1.085938 7.71875 -1.015625 7.9375 -1.015625 C 8.050781 -1.015625 8.191406 -1.039062 8.359375 -1.09375 Z M 6.140625 -4.265625 C 5.972656 -4.140625 5.75 -4.046875 5.46875 -3.984375 C 5.195312 -3.929688 4.90625 -3.882812 4.59375 -3.84375 C 4.289062 -3.8125 3.984375 -3.769531 3.671875 -3.71875 C 3.367188 -3.664062 3.09375 -3.585938 2.84375 -3.484375 C 2.601562 -3.378906 2.40625 -3.226562 2.25 -3.03125 C 2.09375 -2.832031 2.015625 -2.5625 2.015625 -2.21875 C 2.015625 -2 2.054688 -1.8125 2.140625 -1.65625 C 2.234375 -1.5 2.351562 -1.375 2.5 -1.28125 C 2.644531 -1.1875 2.8125 -1.117188 3 -1.078125 C 3.195312 -1.035156 3.398438 -1.015625 3.609375 -1.015625 C 4.054688 -1.015625 4.441406 -1.070312 4.765625 -1.1875 C 5.085938 -1.3125 5.347656 -1.46875 5.546875 -1.65625 C 5.753906 -1.84375 5.90625 -2.046875 6 -2.265625 C 6.09375 -2.484375 6.140625 -2.6875 6.140625 -2.875 Z M 6.140625 -4.265625 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-5">
+<path style="stroke:none;" d=""/>
+</symbol>
+<symbol overflow="visible" id="glyph0-6">
+<path style="stroke:none;" d="M 2.765625 -1.28125 L 2.765625 -10.140625 L 5.328125 -10.140625 C 6.035156 -10.140625 6.628906 -10.039062 7.109375 -9.84375 C 7.585938 -9.644531 7.976562 -9.359375 8.28125 -8.984375 C 8.582031 -8.609375 8.800781 -8.148438 8.9375 -7.609375 C 9.070312 -7.066406 9.140625 -6.457031 9.140625 -5.78125 C 9.140625 -5.070312 9.066406 -4.46875 8.921875 -3.96875 C 8.773438 -3.476562 8.585938 -3.066406 8.359375 -2.734375 C 8.140625 -2.398438 7.890625 -2.132812 7.609375 -1.9375 C 7.328125 -1.75 7.039062 -1.601562 6.75 -1.5 C 6.457031 -1.40625 6.179688 -1.34375 5.921875 -1.3125 C 5.671875 -1.289062 5.460938 -1.28125 5.296875 -1.28125 Z M 1.25 -11.421875 L 1.25 0 L 5.171875 0 C 6.117188 0 6.9375 -0.128906 7.625 -0.390625 C 8.320312 -0.660156 8.894531 -1.046875 9.34375 -1.546875 C 9.789062 -2.054688 10.117188 -2.679688 10.328125 -3.421875 C 10.546875 -4.171875 10.65625 -5.023438 10.65625 -5.984375 C 10.65625 -7.816406 10.179688 -9.179688 9.234375 -10.078125 C 8.285156 -10.972656 6.929688 -11.421875 5.171875 -11.421875 Z M 1.25 -11.421875 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-7">
+<path style="stroke:none;" d="M 7.859375 -8.078125 L 9.296875 -8.078125 C 9.273438 -8.710938 9.15625 -9.253906 8.9375 -9.703125 C 8.71875 -10.160156 8.414062 -10.535156 8.03125 -10.828125 C 7.65625 -11.128906 7.21875 -11.347656 6.71875 -11.484375 C 6.21875 -11.628906 5.675781 -11.703125 5.09375 -11.703125 C 4.5625 -11.703125 4.046875 -11.632812 3.546875 -11.5 C 3.054688 -11.363281 2.613281 -11.160156 2.21875 -10.890625 C 1.832031 -10.617188 1.519531 -10.269531 1.28125 -9.84375 C 1.050781 -9.425781 0.9375 -8.929688 0.9375 -8.359375 C 0.9375 -7.828125 1.039062 -7.390625 1.25 -7.046875 C 1.457031 -6.703125 1.734375 -6.421875 2.078125 -6.203125 C 2.429688 -5.984375 2.828125 -5.804688 3.265625 -5.671875 C 3.703125 -5.535156 4.144531 -5.414062 4.59375 -5.3125 C 5.050781 -5.21875 5.5 -5.117188 5.9375 -5.015625 C 6.375 -4.921875 6.765625 -4.796875 7.109375 -4.640625 C 7.453125 -4.492188 7.726562 -4.296875 7.9375 -4.046875 C 8.144531 -3.804688 8.25 -3.488281 8.25 -3.09375 C 8.25 -2.675781 8.164062 -2.332031 8 -2.0625 C 7.832031 -1.789062 7.609375 -1.578125 7.328125 -1.421875 C 7.046875 -1.273438 6.734375 -1.171875 6.390625 -1.109375 C 6.046875 -1.046875 5.703125 -1.015625 5.359375 -1.015625 C 4.929688 -1.015625 4.515625 -1.066406 4.109375 -1.171875 C 3.703125 -1.273438 3.347656 -1.4375 3.046875 -1.65625 C 2.742188 -1.882812 2.5 -2.171875 2.3125 -2.515625 C 2.125 -2.867188 2.03125 -3.285156 2.03125 -3.765625 L 0.59375 -3.765625 C 0.59375 -3.066406 0.71875 -2.460938 0.96875 -1.953125 C 1.21875 -1.453125 1.554688 -1.035156 1.984375 -0.703125 C 2.421875 -0.378906 2.925781 -0.140625 3.5 0.015625 C 4.070312 0.171875 4.675781 0.25 5.3125 0.25 C 5.832031 0.25 6.359375 0.1875 6.890625 0.0625 C 7.421875 -0.0507812 7.894531 -0.242188 8.3125 -0.515625 C 8.738281 -0.785156 9.085938 -1.132812 9.359375 -1.5625 C 9.640625 -2 9.78125 -2.523438 9.78125 -3.140625 C 9.78125 -3.703125 9.675781 -4.171875 9.46875 -4.546875 C 9.257812 -4.921875 8.976562 -5.226562 8.625 -5.46875 C 8.28125 -5.71875 7.890625 -5.910156 7.453125 -6.046875 C 7.015625 -6.191406 6.566406 -6.316406 6.109375 -6.421875 C 5.660156 -6.535156 5.21875 -6.632812 4.78125 -6.71875 C 4.34375 -6.8125 3.953125 -6.925781 3.609375 -7.0625 C 3.265625 -7.207031 2.988281 -7.390625 2.78125 -7.609375 C 2.570312 -7.828125 2.46875 -8.113281 2.46875 -8.46875 C 2.46875 -8.84375 2.535156 -9.15625 2.671875 -9.40625 C 2.816406 -9.65625 3.007812 -9.851562 3.25 -10 C 3.488281 -10.144531 3.765625 -10.25 4.078125 -10.3125 C 4.390625 -10.382812 4.707031 -10.421875 5.03125 -10.421875 C 5.8125 -10.421875 6.457031 -10.234375 6.96875 -9.859375 C 7.476562 -9.492188 7.773438 -8.898438 7.859375 -8.078125 Z M 7.859375 -8.078125 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-8">
+<path style="stroke:none;" d="M 8.15625 -0.703125 L 8.15625 -8.265625 L 6.875 -8.265625 L 6.875 -7.09375 L 6.859375 -7.09375 C 6.617188 -7.550781 6.28125 -7.894531 5.84375 -8.125 C 5.40625 -8.351562 4.925781 -8.46875 4.40625 -8.46875 C 3.6875 -8.46875 3.082031 -8.328125 2.59375 -8.046875 C 2.101562 -7.773438 1.707031 -7.429688 1.40625 -7.015625 C 1.101562 -6.597656 0.890625 -6.128906 0.765625 -5.609375 C 0.640625 -5.085938 0.578125 -4.582031 0.578125 -4.09375 C 0.578125 -3.53125 0.65625 -2.992188 0.8125 -2.484375 C 0.96875 -1.984375 1.195312 -1.539062 1.5 -1.15625 C 1.8125 -0.78125 2.195312 -0.476562 2.65625 -0.25 C 3.113281 -0.03125 3.648438 0.078125 4.265625 0.078125 C 4.804688 0.078125 5.3125 -0.0390625 5.78125 -0.28125 C 6.257812 -0.519531 6.613281 -0.894531 6.84375 -1.40625 L 6.875 -1.40625 L 6.875 -0.859375 C 6.875 -0.398438 6.828125 0.015625 6.734375 0.390625 C 6.648438 0.773438 6.503906 1.101562 6.296875 1.375 C 6.097656 1.65625 5.84375 1.867188 5.53125 2.015625 C 5.226562 2.171875 4.851562 2.25 4.40625 2.25 C 4.175781 2.25 3.9375 2.222656 3.6875 2.171875 C 3.445312 2.128906 3.222656 2.054688 3.015625 1.953125 C 2.804688 1.847656 2.628906 1.707031 2.484375 1.53125 C 2.335938 1.363281 2.257812 1.15625 2.25 0.90625 L 0.890625 0.90625 C 0.910156 1.351562 1.023438 1.734375 1.234375 2.046875 C 1.453125 2.359375 1.722656 2.609375 2.046875 2.796875 C 2.378906 2.992188 2.742188 3.132812 3.140625 3.21875 C 3.546875 3.300781 3.9375 3.34375 4.3125 3.34375 C 5.632812 3.34375 6.601562 3.003906 7.21875 2.328125 C 7.84375 1.660156 8.15625 0.648438 8.15625 -0.703125 Z M 4.359375 -1.109375 C 3.910156 -1.109375 3.535156 -1.195312 3.234375 -1.375 C 2.929688 -1.5625 2.6875 -1.804688 2.5 -2.109375 C 2.320312 -2.421875 2.195312 -2.765625 2.125 -3.140625 C 2.050781 -3.515625 2.015625 -3.882812 2.015625 -4.25 C 2.015625 -4.644531 2.054688 -5.023438 2.140625 -5.390625 C 2.234375 -5.753906 2.378906 -6.070312 2.578125 -6.34375 C 2.773438 -6.625 3.03125 -6.847656 3.34375 -7.015625 C 3.65625 -7.179688 4.03125 -7.265625 4.46875 -7.265625 C 4.894531 -7.265625 5.253906 -7.175781 5.546875 -7 C 5.847656 -6.832031 6.09375 -6.609375 6.28125 -6.328125 C 6.46875 -6.046875 6.601562 -5.726562 6.6875 -5.375 C 6.769531 -5.019531 6.8125 -4.660156 6.8125 -4.296875 C 6.8125 -3.921875 6.765625 -3.539062 6.671875 -3.15625 C 6.585938 -2.769531 6.445312 -2.421875 6.25 -2.109375 C 6.0625 -1.804688 5.8125 -1.5625 5.5 -1.375 C 5.1875 -1.195312 4.804688 -1.109375 4.359375 -1.109375 Z M 4.359375 -1.109375 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-9">
+<path style="stroke:none;" d="M 1.03125 -8.265625 L 1.03125 0 L 2.390625 0 L 2.390625 -5.15625 C 2.390625 -5.3125 2.425781 -5.507812 2.5 -5.75 C 2.582031 -5.988281 2.710938 -6.21875 2.890625 -6.4375 C 3.066406 -6.664062 3.296875 -6.859375 3.578125 -7.015625 C 3.859375 -7.179688 4.195312 -7.265625 4.59375 -7.265625 C 4.90625 -7.265625 5.15625 -7.21875 5.34375 -7.125 C 5.539062 -7.03125 5.695312 -6.898438 5.8125 -6.734375 C 5.9375 -6.578125 6.019531 -6.382812 6.0625 -6.15625 C 6.113281 -5.9375 6.140625 -5.691406 6.140625 -5.421875 L 6.140625 0 L 7.5 0 L 7.5 -5.15625 C 7.5 -5.789062 7.691406 -6.300781 8.078125 -6.6875 C 8.460938 -7.070312 8.988281 -7.265625 9.65625 -7.265625 C 9.988281 -7.265625 10.257812 -7.210938 10.46875 -7.109375 C 10.675781 -7.015625 10.835938 -6.882812 10.953125 -6.71875 C 11.078125 -6.5625 11.160156 -6.367188 11.203125 -6.140625 C 11.242188 -5.921875 11.265625 -5.679688 11.265625 -5.421875 L 11.265625 0 L 12.625 0 L 12.625 -6.0625 C 12.625 -6.488281 12.554688 -6.851562 12.421875 -7.15625 C 12.285156 -7.457031 12.097656 -7.703125 11.859375 -7.890625 C 11.617188 -8.085938 11.332031 -8.234375 11 -8.328125 C 10.664062 -8.421875 10.289062 -8.46875 9.875 -8.46875 C 9.332031 -8.46875 8.832031 -8.34375 8.375 -8.09375 C 7.925781 -7.851562 7.5625 -7.507812 7.28125 -7.0625 C 7.113281 -7.570312 6.820312 -7.929688 6.40625 -8.140625 C 5.988281 -8.359375 5.523438 -8.46875 5.015625 -8.46875 C 3.847656 -8.46875 2.957031 -8 2.34375 -7.0625 L 2.296875 -7.0625 L 2.296875 -8.265625 Z M 1.03125 -8.265625 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-10">
+<path style="stroke:none;" d="M 1.03125 -8.265625 L 1.03125 0 L 2.390625 0 L 2.390625 -4.671875 C 2.390625 -5.046875 2.4375 -5.390625 2.53125 -5.703125 C 2.632812 -6.015625 2.785156 -6.285156 2.984375 -6.515625 C 3.191406 -6.753906 3.445312 -6.9375 3.75 -7.0625 C 4.050781 -7.195312 4.410156 -7.265625 4.828125 -7.265625 C 5.347656 -7.265625 5.757812 -7.113281 6.0625 -6.8125 C 6.363281 -6.519531 6.515625 -6.113281 6.515625 -5.59375 L 6.515625 0 L 7.875 0 L 7.875 -5.4375 C 7.875 -5.882812 7.828125 -6.289062 7.734375 -6.65625 C 7.640625 -7.03125 7.476562 -7.347656 7.25 -7.609375 C 7.03125 -7.878906 6.738281 -8.085938 6.375 -8.234375 C 6.019531 -8.390625 5.570312 -8.46875 5.03125 -8.46875 C 3.800781 -8.46875 2.90625 -7.960938 2.34375 -6.953125 L 2.296875 -6.953125 L 2.296875 -8.265625 Z M 1.03125 -8.265625 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-11">
+<path style="stroke:none;" d="M 9.28125 -7.984375 L 10.796875 -7.984375 C 10.710938 -8.585938 10.53125 -9.117188 10.25 -9.578125 C 9.976562 -10.046875 9.632812 -10.4375 9.21875 -10.75 C 8.800781 -11.0625 8.320312 -11.296875 7.78125 -11.453125 C 7.25 -11.617188 6.6875 -11.703125 6.09375 -11.703125 C 5.21875 -11.703125 4.441406 -11.539062 3.765625 -11.21875 C 3.085938 -10.90625 2.519531 -10.476562 2.0625 -9.9375 C 1.613281 -9.394531 1.269531 -8.753906 1.03125 -8.015625 C 0.800781 -7.285156 0.6875 -6.507812 0.6875 -5.6875 C 0.6875 -4.851562 0.796875 -4.070312 1.015625 -3.34375 C 1.234375 -2.613281 1.5625 -1.984375 2 -1.453125 C 2.4375 -0.921875 2.984375 -0.503906 3.640625 -0.203125 C 4.304688 0.0976562 5.082031 0.25 5.96875 0.25 C 7.425781 0.25 8.578125 -0.144531 9.421875 -0.9375 C 10.265625 -1.738281 10.757812 -2.859375 10.90625 -4.296875 L 9.390625 -4.296875 C 9.359375 -3.828125 9.257812 -3.390625 9.09375 -2.984375 C 8.9375 -2.585938 8.71875 -2.238281 8.4375 -1.9375 C 8.15625 -1.644531 7.816406 -1.414062 7.421875 -1.25 C 7.035156 -1.09375 6.59375 -1.015625 6.09375 -1.015625 C 5.414062 -1.015625 4.828125 -1.140625 4.328125 -1.390625 C 3.835938 -1.648438 3.4375 -1.992188 3.125 -2.421875 C 2.8125 -2.859375 2.578125 -3.363281 2.421875 -3.9375 C 2.273438 -4.519531 2.203125 -5.140625 2.203125 -5.796875 C 2.203125 -6.390625 2.273438 -6.960938 2.421875 -7.515625 C 2.578125 -8.078125 2.8125 -8.570312 3.125 -9 C 3.4375 -9.425781 3.835938 -9.769531 4.328125 -10.03125 C 4.816406 -10.289062 5.398438 -10.421875 6.078125 -10.421875 C 6.878906 -10.421875 7.570312 -10.21875 8.15625 -9.8125 C 8.738281 -9.40625 9.113281 -8.796875 9.28125 -7.984375 Z M 9.28125 -7.984375 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-12">
+<path style="stroke:none;" d="M 2.015625 -4.125 C 2.015625 -4.625 2.082031 -5.066406 2.21875 -5.453125 C 2.351562 -5.847656 2.535156 -6.175781 2.765625 -6.4375 C 3.003906 -6.707031 3.28125 -6.910156 3.59375 -7.046875 C 3.90625 -7.191406 4.238281 -7.265625 4.59375 -7.265625 C 4.945312 -7.265625 5.28125 -7.191406 5.59375 -7.046875 C 5.90625 -6.910156 6.175781 -6.707031 6.40625 -6.4375 C 6.644531 -6.175781 6.832031 -5.847656 6.96875 -5.453125 C 7.101562 -5.066406 7.171875 -4.625 7.171875 -4.125 C 7.171875 -3.625 7.101562 -3.175781 6.96875 -2.78125 C 6.832031 -2.394531 6.644531 -2.070312 6.40625 -1.8125 C 6.175781 -1.550781 5.90625 -1.351562 5.59375 -1.21875 C 5.28125 -1.082031 4.945312 -1.015625 4.59375 -1.015625 C 4.238281 -1.015625 3.90625 -1.082031 3.59375 -1.21875 C 3.28125 -1.351562 3.003906 -1.550781 2.765625 -1.8125 C 2.535156 -2.070312 2.351562 -2.394531 2.21875 -2.78125 C 2.082031 -3.175781 2.015625 -3.625 2.015625 -4.125 Z M 0.578125 -4.125 C 0.578125 -3.519531 0.660156 -2.953125 0.828125 -2.421875 C 1.003906 -1.898438 1.257812 -1.445312 1.59375 -1.0625 C 1.9375 -0.675781 2.359375 -0.375 2.859375 -0.15625 C 3.359375 0.0625 3.9375 0.171875 4.59375 0.171875 C 5.25 0.171875 5.828125 0.0625 6.328125 -0.15625 C 6.828125 -0.375 7.242188 -0.675781 7.578125 -1.0625 C 7.921875 -1.445312 8.175781 -1.898438 8.34375 -2.421875 C 8.519531 -2.953125 8.609375 -3.519531 8.609375 -4.125 C 8.609375 -4.738281 8.519531 -5.304688 8.34375 -5.828125 C 8.175781 -6.359375 7.921875 -6.816406 7.578125 -7.203125 C 7.242188 -7.597656 6.828125 -7.90625 6.328125 -8.125 C 5.828125 -8.351562 5.25 -8.46875 4.59375 -8.46875 C 3.9375 -8.46875 3.359375 -8.351562 2.859375 -8.125 C 2.359375 -7.90625 1.9375 -7.597656 1.59375 -7.203125 C 1.257812 -6.816406 1.003906 -6.359375 0.828125 -5.828125 C 0.660156 -5.304688 0.578125 -4.738281 0.578125 -4.125 Z M 0.578125 -4.125 "/>
+</symbol>
+<symbol overflow="visible" id="glyph0-13">
+<path style="stroke:none;" d="M 2.015625 -4.0625 C 2.015625 -4.46875 2.054688 -4.863281 2.140625 -5.25 C 2.222656 -5.632812 2.359375 -5.972656 2.546875 -6.265625 C 2.742188 -6.566406 3.003906 -6.804688 3.328125 -6.984375 C 3.648438 -7.171875 4.039062 -7.265625 4.5 -7.265625 C 4.96875 -7.265625 5.363281 -7.175781 5.6875 -7 C 6.019531 -6.820312 6.289062 -6.585938 6.5 -6.296875 C 6.707031 -6.015625 6.859375 -5.679688 6.953125 -5.296875 C 7.054688 -4.921875 7.109375 -4.53125 7.109375 -4.125 C 7.109375 -3.738281 7.0625 -3.359375 6.96875 -2.984375 C 6.875 -2.617188 6.722656 -2.285156 6.515625 -1.984375 C 6.316406 -1.691406 6.054688 -1.457031 5.734375 -1.28125 C 5.421875 -1.101562 5.035156 -1.015625 4.578125 -1.015625 C 4.140625 -1.015625 3.753906 -1.097656 3.421875 -1.265625 C 3.097656 -1.429688 2.832031 -1.660156 2.625 -1.953125 C 2.414062 -2.242188 2.257812 -2.570312 2.15625 -2.9375 C 2.0625 -3.300781 2.015625 -3.675781 2.015625 -4.0625 Z M 8.421875 0 L 8.421875 -11.421875 L 7.0625 -11.421875 L 7.0625 -7.171875 L 7.03125 -7.171875 C 6.875 -7.410156 6.6875 -7.613281 6.46875 -7.78125 C 6.25 -7.945312 6.015625 -8.082031 5.765625 -8.1875 C 5.523438 -8.289062 5.28125 -8.363281 5.03125 -8.40625 C 4.789062 -8.445312 4.566406 -8.46875 4.359375 -8.46875 C 3.722656 -8.46875 3.164062 -8.351562 2.6875 -8.125 C 2.21875 -7.894531 1.828125 -7.582031 1.515625 -7.1875 C 1.203125 -6.800781 0.96875 -6.347656 0.8125 -5.828125 C 0.65625 -5.304688 0.578125 -4.75 0.578125 -4.15625 C 0.578125 -3.570312 0.65625 -3.019531 0.8125 -2.5 C 0.976562 -1.976562 1.21875 -1.519531 1.53125 -1.125 C 1.84375 -0.726562 2.234375 -0.410156 2.703125 -0.171875 C 3.179688 0.0546875 3.742188 0.171875 4.390625 0.171875 C 4.960938 0.171875 5.488281 0.0703125 5.96875 -0.125 C 6.445312 -0.332031 6.800781 -0.664062 7.03125 -1.125 L 7.0625 -1.125 L 7.0625 0 Z M 8.421875 0 "/>
+</symbol>
+</g>
+</defs>
+<g id="surface1">
+<path style="fill-rule:nonzero;fill:rgb(100%,100%,100%);fill-opacity:1;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-dasharray:4,4;stroke-miterlimit:10;" d="M 405 252 L 621 252 L 621 396 L 405 396 Z M 405 252 " transform="matrix(1,0,0,1,-25,-250)"/>
+<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-1" x="418.792" y="22"/>
+  <use xlink:href="#glyph0-2" x="432.728" y="22"/>
+  <use xlink:href="#glyph0-3" x="441.32" y="22"/>
+  <use xlink:href="#glyph0-4" x="446.36" y="22"/>
+  <use xlink:href="#glyph0-5" x="454.952" y="22"/>
+  <use xlink:href="#glyph0-6" x="459.4" y="22"/>
+  <use xlink:href="#glyph0-4" x="470.664" y="22"/>
+  <use xlink:href="#glyph0-3" x="479.256" y="22"/>
+  <use xlink:href="#glyph0-4" x="484.296" y="22"/>
+  <use xlink:href="#glyph0-7" x="492.888" y="22"/>
+  <use xlink:href="#glyph0-2" x="503.256" y="22"/>
+  <use xlink:href="#glyph0-8" x="511.848" y="22"/>
+  <use xlink:href="#glyph0-9" x="521.032" y="22"/>
+  <use xlink:href="#glyph0-2" x="534.68" y="22"/>
+  <use xlink:href="#glyph0-10" x="543.272" y="22"/>
+  <use xlink:href="#glyph0-3" x="552.168" y="22"/>
+</g>
+<path style="fill-rule:nonzero;fill:rgb(100%,100%,100%);fill-opacity:1;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 959.910156 298.542969 C 988.03125 312.601562 988.03125 335.398438 959.910156 349.457031 C 931.792969 363.515625 886.207031 363.515625 858.089844 349.457031 C 829.96875 335.398438 829.96875 312.601562 858.089844 298.542969 C 886.207031 284.484375 931.792969 284.484375 959.910156 298.542969 " transform="matrix(1,0,0,1,-25,-250)"/>
+<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-11" x="832.432" y="79.776001"/>
+  <use xlink:href="#glyph0-12" x="843.984" y="79.776001"/>
+  <use xlink:href="#glyph0-13" x="853.168" y="79.776001"/>
+  <use xlink:href="#glyph0-2" x="862.656" y="79.776001"/>
+  <use xlink:href="#glyph0-7" x="871.248" y="79.776001"/>
+  <use xlink:href="#glyph0-2" x="881.616" y="79.776001"/>
+  <use xlink:href="#glyph0-8" x="890.208" y="79.776001"/>
+  <use xlink:href="#glyph0-9" x="899.392" y="79.776001"/>
+  <use xlink:href="#glyph0-2" x="913.04" y="79.776001"/>
+  <use xlink:href="#glyph0-10" x="921.632" y="79.776001"/>
+  <use xlink:href="#glyph0-3" x="930.528" y="79.776001"/>
+  <use xlink:href="#glyph0-5" x="935.568" y="79.776001"/>
+</g>
+<path style="fill-rule:nonzero;fill:rgb(100%,100%,100%);fill-opacity:1;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-dasharray:4,4;stroke-miterlimit:10;" d="M 338.910156 298.542969 C 367.03125 312.601562 367.03125 335.398438 338.910156 349.457031 C 310.792969 363.515625 265.207031 363.515625 237.089844 349.457031 C 208.96875 335.398438 208.96875 312.601562 237.089844 298.542969 C 265.207031 284.484375 310.792969 284.484375 338.910156 298.542969 " transform="matrix(1,0,0,1,-25,-250)"/>
+<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-1" x="244.92" y="70.552002"/>
+  <use xlink:href="#glyph0-2" x="258.856" y="70.552002"/>
+  <use xlink:href="#glyph0-3" x="267.448" y="70.552002"/>
+  <use xlink:href="#glyph0-4" x="272.488" y="70.552002"/>
+</g>
+<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-11" x="211.432" y="89"/>
+  <use xlink:href="#glyph0-12" x="222.984" y="89"/>
+  <use xlink:href="#glyph0-13" x="232.168" y="89"/>
+  <use xlink:href="#glyph0-2" x="241.656" y="89"/>
+  <use xlink:href="#glyph0-7" x="250.248" y="89"/>
+  <use xlink:href="#glyph0-2" x="260.616" y="89"/>
+  <use xlink:href="#glyph0-8" x="269.208" y="89"/>
+  <use xlink:href="#glyph0-9" x="278.392" y="89"/>
+  <use xlink:href="#glyph0-2" x="292.04" y="89"/>
+  <use xlink:href="#glyph0-10" x="300.632" y="89"/>
+  <use xlink:href="#glyph0-3" x="309.528" y="89"/>
+  <use xlink:href="#glyph0-5" x="314.568" y="89"/>
+</g>
+<path style="fill-rule:nonzero;fill:rgb(100%,100%,100%);fill-opacity:1;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 441 288 L 585 288 L 585 360 L 441 360 Z M 441 288 " transform="matrix(1,0,0,1,-25,-250)"/>
+<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-6" x="439.096" y="79.776001"/>
+  <use xlink:href="#glyph0-4" x="450.36" y="79.776001"/>
+  <use xlink:href="#glyph0-3" x="458.952" y="79.776001"/>
+  <use xlink:href="#glyph0-4" x="463.992" y="79.776001"/>
+  <use xlink:href="#glyph0-7" x="472.584" y="79.776001"/>
+  <use xlink:href="#glyph0-2" x="482.952" y="79.776001"/>
+  <use xlink:href="#glyph0-8" x="491.544" y="79.776001"/>
+  <use xlink:href="#glyph0-9" x="500.728" y="79.776001"/>
+  <use xlink:href="#glyph0-2" x="514.376" y="79.776001"/>
+  <use xlink:href="#glyph0-10" x="522.968" y="79.776001"/>
+  <use xlink:href="#glyph0-3" x="531.864" y="79.776001"/>
+</g>
+<path style="fill-rule:nonzero;fill:rgb(100%,100%,100%);fill-opacity:1;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-dasharray:4,4;stroke-miterlimit:10;" d="M 779.910156 298.542969 C 808.03125 312.601562 808.03125 335.398438 779.910156 349.457031 C 751.792969 363.515625 706.207031 363.515625 678.089844 349.457031 C 649.96875 335.398438 649.96875 312.601562 678.089844 298.542969 C 706.207031 284.484375 751.792969 284.484375 779.910156 298.542969 " transform="matrix(1,0,0,1,-25,-250)"/>
+<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-1" x="685.92" y="70.552002"/>
+  <use xlink:href="#glyph0-2" x="699.856" y="70.552002"/>
+  <use xlink:href="#glyph0-3" x="708.448" y="70.552002"/>
+  <use xlink:href="#glyph0-4" x="713.488" y="70.552002"/>
+</g>
+<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-11" x="652.432" y="89"/>
+  <use xlink:href="#glyph0-12" x="663.984" y="89"/>
+  <use xlink:href="#glyph0-13" x="673.168" y="89"/>
+  <use xlink:href="#glyph0-2" x="682.656" y="89"/>
+  <use xlink:href="#glyph0-7" x="691.248" y="89"/>
+  <use xlink:href="#glyph0-2" x="701.616" y="89"/>
+  <use xlink:href="#glyph0-8" x="710.208" y="89"/>
+  <use xlink:href="#glyph0-9" x="719.392" y="89"/>
+  <use xlink:href="#glyph0-2" x="733.04" y="89"/>
+  <use xlink:href="#glyph0-10" x="741.632" y="89"/>
+  <use xlink:href="#glyph0-3" x="750.528" y="89"/>
+  <use xlink:href="#glyph0-5" x="755.568" y="89"/>
+</g>
+<path style="fill-rule:nonzero;fill:rgb(100%,100%,100%);fill-opacity:1;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 149.910156 298.542969 C 178.03125 312.601562 178.03125 335.398438 149.910156 349.457031 C 121.792969 363.515625 76.207031 363.515625 48.089844 349.457031 C 19.96875 335.398438 19.96875 312.601562 48.089844 298.542969 C 76.207031 284.484375 121.792969 284.484375 149.910156 298.542969 " transform="matrix(1,0,0,1,-25,-250)"/>
+<g style="fill:rgb(0%,0%,0%);fill-opacity:1;">
+  <use xlink:href="#glyph0-11" x="22.432" y="79.776001"/>
+  <use xlink:href="#glyph0-12" x="33.984" y="79.776001"/>
+  <use xlink:href="#glyph0-13" x="43.168" y="79.776001"/>
+  <use xlink:href="#glyph0-2" x="52.656" y="79.776001"/>
+  <use xlink:href="#glyph0-7" x="61.248" y="79.776001"/>
+  <use xlink:href="#glyph0-2" x="71.616" y="79.776001"/>
+  <use xlink:href="#glyph0-8" x="80.208" y="79.776001"/>
+  <use xlink:href="#glyph0-9" x="89.392" y="79.776001"/>
+  <use xlink:href="#glyph0-2" x="103.04" y="79.776001"/>
+  <use xlink:href="#glyph0-10" x="111.632" y="79.776001"/>
+  <use xlink:href="#glyph0-3" x="120.528" y="79.776001"/>
+  <use xlink:href="#glyph0-5" x="125.568" y="79.776001"/>
+</g>
+<path style="fill:none;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 171 324 L 216 324 " transform="matrix(1,0,0,1,-25,-250)"/>
+<path style="fill:none;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 801 324 L 827.101562 324 " transform="matrix(1,0,0,1,-25,-250)"/>
+<path style="fill-rule:nonzero;fill:rgb(0%,0%,0%);fill-opacity:1;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 835.101562 324 L 827.101562 321 L 827.101562 327 Z M 835.101562 324 " transform="matrix(1,0,0,1,-25,-250)"/>
+<path style="fill:none;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-dasharray:4,4;stroke-miterlimit:10;" d="M 360 324 L 405 324 " transform="matrix(1,0,0,1,-25,-250)"/>
+<path style="fill:none;stroke-width:1;stroke-linecap:round;stroke-linejoin:round;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-dasharray:4,4;stroke-miterlimit:10;" d="M 621 324 L 647.101562 324 " transform="matrix(1,0,0,1,-25,-250)"/>
+<path style="fill-rule:nonzero;fill:rgb(0%,0%,0%);fill-opacity:1;stroke-width:1;stroke-linecap:butt;stroke-linejoin:miter;stroke:rgb(0%,0%,0%);stroke-opacity:1;stroke-miterlimit:10;" d="M 655.101562 324 L 647.101562 321 L 647.101562 327 Z M 655.101562 324 " transform="matrix(1,0,0,1,-25,-250)"/>
+</g>
+</svg>
--- a/Slide/fig/meta.xbb	Mon Apr 23 21:44:32 2018 +0900
+++ b/Slide/fig/meta.xbb	Sat May 19 19:14:19 2018 +0900
@@ -1,8 +1,8 @@
-%%Title: meta.pdf
-%%Creator: extractbb 20160307
+%%Title: fig/meta.pdf
+%%Creator: extractbb 20180217
 %%BoundingBox: 0 0 958 148
 %%HiResBoundingBox: 0.000000 0.000000 958.000000 148.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Wed Feb 21 01:38:18 2018
+%%CreationDate: Tue May 15 18:15:06 2018
--- a/Slide/prosym.md	Mon Apr 23 21:44:32 2018 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,245 +0,0 @@
-title: GearsOSのAgdaによる記述と検証
-author: Masataka Hokama, Shinji Kono
-profile: 琉球大学
-lang: Japanese
-code-engine: coderay
-
-
-<!-- 卒論のスライド -->
-
-## プログラムの信頼性の保証
-* 動作するプログラムの信頼性を保証したい
-* 信頼性の保証をするためにはプログラムの仕様を検証する必要がある
-* プログラムの仕様を検証するにはモデル検査と **定理証明** の２つの手法がある
-  * モデル検査 はプログラムの持つ状態を数え上げて仕様を満たしているかを確認する
-  * 定理証明　はプログラムの性質を論理式で記述し、型を生成する関数を定義することで証明を記述できる
-* また、当研究室では検証しやすい単位として CodeGear、DataGear という単位を用いてプログラムを記述する手法を提案している
-
-## プログラムの信頼性の保証
-* 今回は **定理証明** をつかって仕様を検証した
-* 定理証明には定理証明支援系の言語 Agda を使用する
-  * Agda では型でプログラムの性質を論理式で記述し、型に対応する関数部分で論理式を解くことで証明を記述できる
-* データ構造を仕様と実装に分けて記述するために現在ある Stack 実装とは別に Stack の仕様部分を Interface で記述した
-<!-- interface の説明 -->
-* 今回は Agda を用いて CodeGear 、DataGear、という単位と Interface を定義した
-* CodeGear、DataGear という単位を用いて実装された Stack を Interface を通して呼び出し、その性質の一部について証明を行なった
-
-
-## CodeGear と DataGear
-* CodeGear とはプログラムを記述する際の処理の単位である
-* DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータが全て入っている
-* CodeGear はメタ計算によって CodeGear へ接続される
-* メタ計算を切り替えることで処理に変更を加えることなくプログラムの性質を検証できる
-
-<div style="text-align: center;">
-    <img src="./fig/cgdg.svg" alt="goto" width="800">
-</div>
-
-
-## Agda での popSingleLinkedStack の型
-* Agda の 関数部分は **関数名 = 値**
-* この型は stack を受け取り、stack の先頭を取って、次の関数に渡すという関数の型
-* popSingleLinkedStack は Stack のpop のCodeGearで、継続に型Maybe aを受けとるCodeGear( ** (fa -> t) -> t** )に渡す
-* stack は空の可能性があるので Maybe a を返す
-
-
-```AGDA
-popSingleLinkedStack : SingleLinkedStack a ->
-   (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
-```
-
-## Maybe
-* **Maybe** はNothingかJustの２つの場合を持つ型でAgda の **data** として定義されている
-* Just か Nothing はパターンマッチで場合分けする
-Nothing と Just a は Maybe を生成する constructor
-
-```AGDA
-data Maybe a : Set where
-  Nothing : Maybe a
-  Just    : a -> Maybe a
-```
-
-## data を用いた等式の Agda での証明
-* x ≡ x はAgdaでは常に正しい論理式
-* data は **data データ名 : 型** と書く
-* **refl** は左右の項が等しいことを表す x ≡ x を生成する項
-*  x ≡ x を証明したい時には refl と書く
-
-```AGDA
-data _≡_ {a} {A : Set a} (x : A) : A → Set a where
-  refl : x ≡ x
-```
-
-## Agda でのpopSingleLinkedStack での定義
-* Agdaでの関数の定義は **関数名 = 関数の実装** の書く
-* 関数名と = の間にある stack と cs は引数
-* popSingleLinkedStack では stack を受け取り、 stack の中から data を取り出し、新しいstack を継続し、次の CodeGear に継続している
-* stack の top は Maybe a なので Nothing と Just
-* 関数部分では with で data のパターンマッチを行うことができる
-
-
-```AGDA
-popSingleLinkedStack stack cs with (top stack)
-popSingleLinkedStack stack cs | Nothing = cs stack  Nothing
-popSingleLinkedStack stack cs | Just d  = cs record  { top = (next d) } (Just (datum d))
-```
-
-## SingleLinkedStack の定義(recordの例)
-* record は複数のデータをまとめて記述する型
-* **record レコード名** を書き、その次の行の **field** 後に **フィールド名:型名** と列挙する
-* SingleLinkedStack では top というフィールドに Maybe のかかっている Element 型の要素aが定義されている
-* Element では record で data と次の要素 next が定義されている
-
-```AGDA
-record SingleLinkedStack (a : Set) : Set where
-  field
-    top : Maybe (Element a)
-```
-
-## pushSingleLinkedStackの定義とrecordの構築
-* 実際に record を構築するときの例として **pushSingleLinkedStack** の関数部分を扱う
-* pushSingleLinkedStack では stack と data を受け取り、 CodeGear 中で Data を stack に入れ、新しいstack を継続し、次の CodeGear に継続している
-* record の構築は関数側で行う
-* **record** の後ろの {} 内部で **フィールド名 = 値** で列挙する
-* 複数のレコードを書くときは **;** で区切る
-
-```Agda
-pushSingleLinkedStack stack datum next =
-    next record {top = Just (record {datum = datum;next =(top stack)})}
-```
-
-## Agda での Interface の定義
-* singleLinkedStack の仕様を実装とは別に記述するために record を使い、 Stack の Interface を記述した
-* ここでの push、 pop は仕様のみの記述で実装とはここでは関係ない
-* t は継続を返す型を表す
-* 実装は関数の中で record を構築し、singleLinkedStack での push 、 pop と繋げられる
-
-```AGDA
-record StackMethods {n m : Level } (a : Set n )
-    {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where
-      field
-        push : stackImpl -> a -> (stackImpl -> t) -> t
-        pop  : stackImpl -> (stackImpl -> Maybe a -> t) -> t
-```
-
-
-## 証明の概要
-* 今回は singleLinkedStack の実装を抽象的に表す Interface を通し、 **任意の数** を push し pop したとき、
-push した値と pop した値が等しくなることを証明する
-* このとき、どのような状態の Stack に push し、 pop をしても値が等しくなることを示したい
-* そのため、**状態の不定な** Stack を作成する関数を作成した
-
-## 不定な Stack を作成する stackInSomeState という関数の定義
-* 不定なstackは入力(s : SingleLinkedStack a )で与える
-* 入力は定義時点では決まっていないので不定
-* stackInSomeState は stack を受け取り、状態の決まっていない stack を record で作成する
-
-```AGDA
-stackInSomeState : (s : SingleLinkedStack a ) -> Stack a ( SingleLinkedStack  a )
-stackInSomeState s =  record { stack = s ; stackMethods = singleLinkedStackSpec }
-```
-
-## Agda での Interface を含めた部分的な証明
-*  push を２回したときの値と、直後に pop を2回して取れた値が等しいことを示している
-* Agda 中では不明な部分を **?** と書くことができ、**?** 部分には証明が入る
-* 証明部分はラムダ式で与える
-* はじめにに型部分に注目する
-
-```AGDA
-push->push->pop2 : {l : Level } {a : Set l} (x y : a ) (s : SingleLinkedStack a ) ->
-    pushStack ( stackInSomeState s )  x ( \s1 -> pushStack s1 y ( \s2 ->
-    pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
-push->push->pop2 {l} {a} x y s = ?
-```
-
-## ラムダ式
-* **\s1 ->** はラムダ式で push->push->pop2 の型では次の CodeGear 部分にラムダ式を使いStackを渡している
-
-```AGDA
-push->push->pop2 : {l : Level } {a : Set l} (x y : a ) (s : SingleLinkedStack a ) ->
-    pushStack ( stackInSomeState s )  x ( \s1 -> pushStack s1 y ( \s2 ->
-    pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
-```
-
-
-## Agda での Interface を含めた部分的な証明
-* ? 部分はコンパイル時に Agda から内部に入る型を示してもらえる
-* ここでは最終的に **(Just x ≡ x1) ∧ (Just y ≡ y1)** が返ってくる
-* (x ≡ x1)と(y ≡ y1)の２つが同時成り立ってほしい
-* そこで **∧** の部分を record で定義した
-
-```AGDA
-push->push->pop2 {l} {a} x y s = { }0
-```
-
-```AGDA
--- Goal
-?0 : pushStack (stackInSomeState s) x
-(λ s1 →
-   pushStack s1 y
-   (λ s2 → pop2Stack s2 (λ s3 y1 x1 → (Just x ≡ x1) ∧ (Just y ≡ y1))))
-```
-
-## Agda での Interface を含めた部分的な証明(∧)
-* a と b の２つの証明から a かつ b という証明をするために ** ∧ ** を定義した
-* 異なる２つのものを引数にとり、それらがレコードに存在することを示せればよい
-<!-- * 直積を表す型を定義する -->
-
-```AGDA
-record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where
-  field
-    pi1 : a
-    pi2 : b
-```
-
-## Agda での Interface を含めた部分的な証明
-* x と x1 が等しいことは **refl** で証明できる
-* ∧ でまとめた pi1、pi2は両方共等しいはずなので両方に refl を使う
-* pi1、pi2の両方に refl を代入することで証明することができた
-* これにより証明の目的であった「どのような状態の Stack に push し、 pop をしても値が等しくなる」ことを証明することができた
-
-```AGDA
-push->push->pop2 : {l : Level } {a : Set l} (x y : a ) (s : SingleLinkedStack a ) ->
-    pushStack ( stackInSomeState s )  x ( \s1 -> pushStack s1 y ( \s2 ->
-    pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
-push->push->pop2 {l} {a} x y s = record { pi1 = refl ; pi2 = refl }
-```
-
-## まとめと今後の課題
-* 本研究では CodeGear、DataGear を Agda で定義することができた
-* また Agda で Interface の記述及び Interface を含めた一部の証明を行えた
-* これにより、 Interface を経由しても一部の性質は実装と同様の働きをすることが証明できた
-<!-- * また、これにより CbC での Interface 記述では考えられていなかった細かな記述が明らかになった -->
-* 今後の課題としては  継続を用いた Agda で Hoare Logic を表現し、その Hoare Logic をベースとして証明を行えるかを確認する
-* また RedBlackTree の挿入、削除の性質に関する証明も行おうと考えている
-
-
-## Hoare Logic
-* Hoare Logic は Tony Hoare によって提案されたプログラムの部分的な正当性を検証するための手法
-* 前の状態を{P}(Pre-Condition)、後の状態を{Q}(Post-Condition)とし、前状態を C (Command) によって変更する
-* この {P} C {Q} でプログラムを部分的に表すことができるp
-
-<div style="text-align: center;">
-    <img src="./fig/hoare.svg" alt="hoare" width="1000">
-</div>
-
-
-## Hoare Logic と CbC
-
-* Hoare Logic の状態と処理を CodeGear、 DataGear の単位で考えることができると考えている
-
-<div style="text-align: center;">
-    <img src="./fig/hoare-cbc.svg" alt="cbc-hoare" width="800">
-</div>
-
-
-## Element
-* Element の説明
-```AGDA
-record Element {l : Level} (a : Set l) : Set l where
-  inductive
-  constructor cons
-  field
-    datum : a  -- `data` is reserved by Agda.
-    next : Maybe (Element a)
-```
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Slide/sigos.html	Sat May 19 19:14:19 2018 +0900
@@ -0,0 +1,558 @@
+<!DOCTYPE html>
+<html>
+<head>
+   <meta http-equiv="content-type" content="text/html;charset=utf-8">
+   <title>GearsOSのAgdaによる記述と検証</title>
+
+<meta name="generator" content="Slide Show (S9) v2.5.0 on Ruby 2.4.1 (2017-03-22) [x86_64-darwin16]">
+<meta name="author"    content="Masataka Hokama, Shinji Kono" >
+
+<!-- style sheet links -->
+<link rel="stylesheet" href="s6/themes/projection.css"   media="screen,projection">
+<link rel="stylesheet" href="s6/themes/screen.css"       media="screen">
+<link rel="stylesheet" href="s6/themes/print.css"        media="print">
+<link rel="stylesheet" href="s6/themes/blank.css"        media="screen,projection">
+
+<!-- JS -->
+<script src="s6/js/jquery-1.11.3.min.js"></script>
+<script src="s6/js/jquery.slideshow.js"></script>
+<script src="s6/js/jquery.slideshow.counter.js"></script>
+<script src="s6/js/jquery.slideshow.controls.js"></script>
+<script src="s6/js/jquery.slideshow.footer.js"></script>
+<script src="s6/js/jquery.slideshow.autoplay.js"></script>
+
+<!-- prettify -->
+<link rel="stylesheet" href="scripts/prettify.css">
+<script src="scripts/prettify.js"></script>
+
+<script>
+  $(document).ready( function() {
+    Slideshow.init();
+
+    $('code').each(function(_, el) {
+      if (!el.classList.contains('noprettyprint')) {
+        el.classList.add('prettyprint');
+      }
+    });
+    prettyPrint();
+  } );
+
+
+</script>
+
+<!-- Better Browser Banner for Microsoft Internet Explorer (IE) -->
+<!--[if IE]>
+<script src="s6/js/jquery.microsoft.js"></script>
+<![endif]-->
+
+
+
+</head>
+<body>
+
+<div class="layout">
+  <div id="header"></div>
+  <div id="footer">
+    <div align="right">
+      <img src="s6/images/logo.svg" width="200px">
+    </div>
+  </div>
+</div>
+
+<div class="presentation">
+
+  <div class='slide cover'>
+    <table width="90%" height="90%" border="0" align="center">
+      <tr>
+        <td>
+          <div align="center">
+            <h1><font color="#808db5">GearsOSのAgdaによる記述と検証</font></h1>
+          </div>
+        </td>
+      </tr>
+      <tr>
+        <td>
+          <div align="left">
+            Masataka Hokama, Shinji Kono
+            琉球大学
+            <hr style="color:#ffcc00;background-color:#ffcc00;text-align:left;border:none;width:100%;height:0.2em;">
+          </div>
+        </td>
+      </tr>
+    </table>
+  </div>
+
+<div class='slide '>
+<!-- === begin markdown block ===
+
+      generated by markdown/1.2.0 on Ruby 2.4.1 (2017-03-22) [x86_64-darwin16]
+                on 2018-05-19 17:31:37 +0900 with Markdown engine kramdown (1.15.0)
+                  using options {}
+  -->
+<!-- <span style="background-color:#ffcc99"> </span> -->
+<!-- ```C -->
+<!-- <span style="background-color:#ffcc99">hoge</span> -->
+<!-- ``` -->
+
+
+<!-- _S9SLIDE_ -->
+<h2 id="section">本発表の流れ</h2>
+<ul>
+  <li>研究目的</li>
+  <li>CodeGear と DataGear の説明</li>
+  <li>Agda での記述</li>
+  <li>Agda での CodeGear 、 DataGear 、 Interface の表現</li>
+  <li>実際に行なった証明</li>
+  <li>証明の改善</li>
+  <li>まとめ</li>
+</ul>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="section-1">プログラムの信頼性の保証</h2>
+<ul>
+  <li>動作するプログラムの信頼性を保証したい</li>
+  <li>保証をするためには仕様を検証する必要がある</li>
+  <li>仕様を検証するにはモデル検査と <strong>定理証明</strong> の２つの手法がある
+    <ul>
+      <li>モデル検査 はプログラムの持つ状態を数え上げて仕様を満たしているかを確認するもの</li>
+      <li>定理証明　はプログラムの性質を論理式で記述し、型を生成する関数を定義することで証明を記述できるもの</li>
+    </ul>
+  </li>
+  <li>当研究室では検証しやすい単位として CodeGear、DataGear という単位を用いてプログラムを記述する手法を提案している</li>
+</ul>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="section-2">プログラムの信頼性の保証</h2>
+<ul>
+  <li>本研究では <strong>定理証明支援系</strong> の言語 <strong>Agda</strong> をつかって仕様を検証した</li>
+  <li>データ構造を仕様と実装に分けて記述するため、モジュール化の仕組みである <strong>Interface</strong> を記述した</li>
+  <li>今回は Agda で CodeGear 、DataGear、という単位と Interface を定義した</li>
+  <li>また、 CodeGear 、DataGear を用いて Agda 上に実装された Stack を Interface を通して呼び出し、その性質の一部について証明を行った</li>
+</ul>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="codegear--datagear-">CodeGear と DataGear の定義</h2>
+<ul>
+  <li>CodeGear とはプログラムを記述する際の処理の単位</li>
+  <li>DataGear は CodeGear で扱うデータの単位で、処理に必要なデータが全て入っている</li>
+  <li>CodeGear はメタ計算によって別の CodeGear へ接続される</li>
+</ul>
+
+<div style="text-align: center;">
+    <img src="./fig/cgdg.svg" alt="goto" width="800" />
+</div>
+
+<!-- ## Agda での CodeGear、 DataGear　の表現 -->
+<!-- * CodeGear は処理の単位なので、 Agda では通常関数として記述するものとする -->
+<!-- * DataGear はレコード型で定義できるため、 Agda の record を使用し記述する -->
+
+<p>次のスライドからは Agda の記述について解説を行う</p>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="agda-">Agda での型</h2>
+<ul>
+  <li>Agda の 型は <strong>関数名 : 型</strong> のように <strong>:</strong> を使って定義される</li>
+  <li>ここでは Stack の<strong>実装</strong>である <strong>popSingleLinkedStack</strong> の型を例とする</li>
+  <li>この型は stack を受け取り、stack の先頭を取って、次の関数に渡すという関数の型</li>
+  <li>stack は空の可能性があるので Maybe a を返す</li>
+  <li>popSingleLinkedStack は Stack の pop のCodeGearで、継続に型 Maybe a を受けとる CodeGear <span style="background-color:#ffcc99">( <strong>(fa -&gt; t) -&gt; t</strong>)</span> に渡す</li>
+</ul>
+
+<pre lang="AGDA"><code>popSingleLinkedStack : SingleLinkedStack a -&gt;
+   (Code : SingleLinkedStack a -&gt; (Maybe a) -&gt; t) -&gt; t
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="maybe">Maybe</h2>
+<ul>
+  <li><strong>Maybe</strong> はNothingかJustの２つの場合を持つ型で Agda の <strong>data</strong> として定義されている</li>
+  <li>Just か Nothing はパターンマッチで場合分けするNothing と Just a は Maybe を生成する constructor</li>
+</ul>
+
+<pre lang="AGDA"><code>data Maybe a : Set where
+  Nothing : Maybe a
+  Just    : a -&gt; Maybe a
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="data-">data を用いた等式の証明</h2>
+<ul>
+  <li>x ≡ x は Agda では常に正しい論理式</li>
+  <li>data は <strong>data データ名 : 型</strong></li>
+  <li><strong>refl</strong> は左右の項が等しいことを表す x ≡ x を生成する項</li>
+  <li>x ≡ x を証明したい時には refl と書く</li>
+</ul>
+
+<pre lang="AGDA"><code>data _≡_ {a} {A : Set a} (x : A) : A → Set a where
+  refl : x ≡ x
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="agda--1">Agda での関数</h2>
+<ul>
+  <li>Agda での関数定義は <strong>関数名 = 関数の実装</strong></li>
+  <li>ここでは <strong>popSingleLinkedStack</strong> の関数を例とする</li>
+  <li>引数は <strong>関数名</strong> と <strong>=</strong> の間に記述する</li>
+  <li>stack と 次の CodeGear である cs を受け取り、 stack の中から data を取り出し、新しい stack に継続し、次の CodeGear へと stack 渡している</li>
+  <li>stack の top は Maybe a なので Nothing か Just が返ってくる</li>
+  <li><strong>with</strong> で data のパターンマッチができる</li>
+</ul>
+
+<pre lang="AGDA"><code>popSingleLinkedStack stack cs with (top stack)
+popSingleLinkedStack stack cs | Nothing = cs stack  Nothing
+popSingleLinkedStack stack cs | Just d  = cs record  { top = (next d) } (Just (datum d))
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="agda--record">Agda での record　の定義</h2>
+<ul>
+  <li>record は複数のデータをまとめて記述する型</li>
+  <li><strong>record レコード名</strong> を書き、その次の行の <strong>field</strong> 後に <strong>フィールド名:型名</strong> と列挙する</li>
+  <li>ここでは SingleLinkedStack の定義を例とする</li>
+  <li>定義では top フィールドのみを定義しているが複数定義することもできる</li>
+  <li>top には Element 型の要素 a が定義されており、 <strong>Element</strong> 型は現在の <strong>data</strong> と次の data を指す <strong>next</strong> を定義している</li>
+</ul>
+
+<pre lang="AGDA"><code>record SingleLinkedStack (a : Set) : Set where
+  field
+    top : Maybe (Element a)
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="agda--record-">Agda での record の構築</h2>
+<ul>
+  <li>record の構築は関数側</li>
+  <li><strong>record</strong> 後ろの <strong>{}</strong> 内部で <strong>フィールド名 = 値</strong> で列挙する</li>
+  <li>複数のレコードを記述するさいは <strong>;</strong> で区切る</li>
+  <li>例として <strong>pushSingleLinkedStack</strong> の関数部分を扱う</li>
+  <li>pushSingleLinkedStack では stack と data を受け取り、 CodeGear 中で Data を stack に入れ、新しいstack を継続し、次の CodeGear に継続している</li>
+</ul>
+
+<pre lang="Agda"><code>pushSingleLinkedStack stack datum next =
+    next record {top = Just (record {datum = datum;next =(top stack)})}
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="agda--interface-">Agda での Interface の定義</h2>
+<ul>
+  <li>Stack の仕様を実装とは別に記述するために record で Stack の Interface を記述した</li>
+  <li>ここでの push、 pop は仕様の型のみ記述され、実装は構築時に与える</li>
+  <li>t は継続を返す型を表し、次の CodeGear を指す</li>
+  <li>ここでの push 、 pop は pushSingleLinkedStack 、 popSingleLinkedStack に繋げる</li>
+</ul>
+
+<pre lang="AGDA"><code>record StackMethods {n m : Level } (a : Set n )
+    {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where
+      field
+        push : stackImpl -&gt; a -&gt; (stackImpl -&gt; t) -&gt; t
+        pop  : stackImpl -&gt; (stackImpl -&gt; Maybe a -&gt; t) -&gt; t
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="section-3">証明の概要</h2>
+<ul>
+  <li>今回は Interface を通して、 <strong>任意の数</strong> を stack に push し、データが入った stack に対して pop を行なう</li>
+  <li>このとき push した値と pop した値が等しくなることを証明する</li>
+  <li>また、どのような状態の Stack に push し、 pop をしても値が等しくなることを示したい</li>
+  <li>そのため、<strong>状態の不定な</strong> Stack を作成する関数を定義した</li>
+</ul>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="stack-">状態が不定な Stack の定義</h2>
+<ul>
+  <li>ここでは状態が不定な Stack を作成する関数 <strong>stackInSomeState</strong> を定義する</li>
+  <li>不定なstackを入力(s : SingleLinkedStack a )で与える</li>
+  <li>stackInSomeState は stack を受け取り、状態の決まっていない stack を構築する</li>
+</ul>
+
+<pre lang="AGDA"><code>stackInSomeState : (s : SingleLinkedStack a ) -&gt; Stack a ( SingleLinkedStack  a )
+stackInSomeState s =  record { stack = s ; stackMethods = singleLinkedStackSpec }
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="agda--interface--1">Agda での Interface を含めた部分的な証明</h2>
+<ul>
+  <li>証明部分は型部分にラムダ式で与える</li>
+  <li><strong>push-&gt;push-&gt;pop2</strong>では push を２回したときの値と、直後に pop を2回して取れた値が等しいことを型に記述している</li>
+</ul>
+
+<pre lang="AGDA"><code>push-&gt;push-&gt;pop2 : {l : Level } {a : Set l} (x y : a ) (s : SingleLinkedStack a ) -&gt;
+    pushStack ( stackInSomeState s )  x ( \s1 -&gt; pushStack s1 y ( \s2 -&gt;
+    pop2Stack s2 ( \s3 y1 x1 -&gt; (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
+push-&gt;push-&gt;pop2 {l} {a} x y s = ?
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="section-4">ラムダ式</h2>
+<ul>
+  <li><strong>\s1 -&gt;</strong> はラムダ式で push-&gt;push-&gt;pop2 の型では次の CodeGear 部分にラムダ式を使いStackを渡している</li>
+</ul>
+
+<pre lang="AGDA"><code>push-&gt;push-&gt;pop2 : {l : Level } {a : Set l} (x y : a ) (s : SingleLinkedStack a ) -&gt;
+    pushStack ( stackInSomeState s )  x ( \s1 -&gt;* pushStack s1 y ( \s2 -&gt;
+    pop2Stack s2 ( \s3 y1 x1 -&gt; (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="agda--interface--2">Agda での Interface を含めた部分的な証明</h2>
+<ul>
+  <li>Agda では不明な部分を <strong>?</strong> と書くことができる</li>
+  <li><strong>?</strong> 部分はコンパイルすると <strong>{}n</strong> のように番号が付き、Agda から内部に入る型を示してもらえる</li>
+</ul>
+
+<pre lang="AGDA"><code>push-&gt;push-&gt;pop2 {l} {a} x y s = { }0
+</code></pre>
+
+<pre lang="AGDA"><code>-- Goal
+?0 : pushStack (stackInSomeState s) x
+(λ s1 →
+   pushStack s1 y
+   (λ s2 → pop2Stack s2 (λ s3 y1 x1 → (Just x ≡ x1) ∧ (Just y ≡ y1))))
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="agda--interface--3">Agda での Interface を含めた部分的な証明</h2>
+<ul>
+  <li>ここでは最終的に <strong>(Just x ≡ x1) ∧ (Just y ≡ y1)</strong> が返ってくる必要がある</li>
+  <li><strong>(x ≡ x1)</strong> と <strong>(y ≡ y1)</strong> の２つが同時に成り立つ必要がある</li>
+  <li>そこで <strong>∧</strong> の部分を record で定義した</li>
+</ul>
+
+<pre lang="AGDA"><code>-- Goal
+?0 : pushStack (stackInSomeState s) x
+(λ s1 →
+   pushStack s1 y
+   (λ s2 → pop2Stack s2 (λ s3 y1 x1 → (Just x ≡ x1) ∧ (Just y ≡ y1))))
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="agda--interface--4">Agda での Interface を含めた部分的な証明(∧)</h2>
+<ul>
+  <li>a と b の２つの証明から a かつ b という証明を行うため <strong>∧</strong> を定義する</li>
+  <li>これには異なる２つのものを引数にとり、それらがレコードに同時に存在することが示せれば良い</li>
+  <li><strong>∧</strong> は 型 a と 型b をもつ2つの要素を左右にとり、 それらが同時に存在することを示すレコード型</li>
+</ul>
+
+<pre lang="AGDA"><code>record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where
+  field
+    pi1 : a
+    pi2 : b
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="agda--interface--5">Agda での Interface を含めた部分的な証明</h2>
+<ul>
+  <li>定義した ∧ を関数部分で構築する</li>
+  <li>ここでは <strong>pi1</strong> 、 <strong>pi2</strong> の両方を <strong>?</strong> としておく</li>
+</ul>
+
+<pre lang="AGDA"><code>push-&gt;push-&gt;pop2 : {l : Level } {a : Set l} (x y : a ) (s : SingleLinkedStack a ) -&gt;
+    pushStack ( stackInSomeState s )  x ( \s1 -&gt; pushStack s1 y ( \s2 -&gt;
+    pop2Stack s2 ( \s3 y1 x1 -&gt; (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
+push-&gt;push-&gt;pop2 {l} {a} x y s = record { pi1 = { }0 ; pi2 = { }1 }
+</code></pre>
+
+<pre lang="AGDA"><code>?0 : Just x ≡
+Just
+(Element.datum
+ (.stack.element (stack (stackInSomeState s)) x
+  (λ s1 →
+     pushStack
+     (record
+      { stack = s1 ; stackMethods = stackMethods (stackInSomeState s) })
+     y
+     (λ s2 →
+        pop2Stack s2 (λ s3 y1 x1 → (Just x ≡ x1) ∧ (Just y ≡ y1))))))
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="agda--interface--6">Agda での Interface を含めた部分的な証明</h2>
+<ul>
+  <li>∧ で定義された左右に <strong>x ≡ x1</strong> と　<strong>y ≡ y1</strong> が入る</li>
+  <li><strong>x ≡ x1</strong>、　<strong>y ≡ y1</strong> は共に <strong>refl</strong> で証明できる</li>
+  <li>pi1、pi2 は両方 refl が入ることで証明ができる</li>
+  <li>また、型に書かれた順で値が取り出されている為、最後のラムダ式で stack の性質である FIFO 通りに値が取れていることが分かる</li>
+  <li>これにより証明の目的であった「どのような状態の Stack に push し、 pop をしても値が等しくなる」ことを証明することができた</li>
+</ul>
+
+<pre lang="AGDA"><code>push-&gt;push-&gt;pop2 : {l : Level } {a : Set l} (x y : a ) (s : SingleLinkedStack a ) -&gt;
+    pushStack ( stackInSomeState s )  x ( \s1 -&gt; pushStack s1 y ( \s2 -&gt;
+    pop2Stack s2 ( \s3 y1 x1 -&gt; (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
+push-&gt;push-&gt;pop2 {l} {a} x y s = record { pi1 = refl ; pi2 = refl }
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="section-5">手証明での限界</h2>
+<ul>
+  <li>現在 Binary Tree に対して近い証明を書いている</li>
+  <li>これは 「Tree に対して node を put し、 get した時取れる node の値は put した node と等しい」というもの</li>
+  <li>Tree に対する操作では root Node から Node を辿る Loop があり、それを展開しながら証明を書く</li>
+  <li>Agda 側が put した node と get した node が等しいことを分かってくれず、証明が完成していない…</li>
+  <li>今後は新しい証明規則を導入して証明を行おうと考えている</li>
+</ul>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="hoare-logic">Hoare Logic</h2>
+<ul>
+  <li>Hoare Logic は Tony Hoare によって提案されたプログラムの部分的な正当性を検証するための手法</li>
+  <li>前の状態を{P}(Pre-Condition)、後の状態を{Q}(Post-Condition)とし、前状態を C (Command) によって変更するといったもの</li>
+  <li>この {P} C {Q} でプログラムを部分的に表すことができる</li>
+  <li>{P} が成り立つときに、 C を実行すると、実行後は必ず {Q} が成り立つとき、部分的に正当である</li>
+</ul>
+
+<div style="text-align: center;">
+    <img src="./fig/hoare.svg" alt="hoare" width="1000" />
+</div>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="hoare-logic--cbc">Hoare Logic と CbC</h2>
+
+<ul>
+  <li>Hoare Logic の状態と処理を CodeGear、 DataGear の単位で考えることができると考えている</li>
+  <li>Pre-condition を input DataGear , Post-Conditon を output DataGear , Command は CodeGear そのものとして扱えると考えている。</li>
+</ul>
+
+<div style="text-align: center;">
+    <img src="./fig/hoare-cbc.svg" alt="cbc-hoare" width="800" />
+</div>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="hoare-logic--binary-tree">Hoare Logic での例 (Binary Tree)</h2>
+
+<!-- * この例では Node を put するための関数 "putTree" の移り変わりである。 -->
+<ul>
+  <li>この例では今後の証明に使おうとしている BinaryTree での put, get を例にする。</li>
+  <li>初めに Node を put するべき位置を調べる “findNode” を行い root から ノードを辿っている。ここでは辿ったノードを Stack に保存する</li>
+  <li>次に put すべき位置から木を再構成する”replaceNode”を行い、 Stack に保存したノードを辿り、木を再構築していく</li>
+</ul>
+
+<div style="text-align: center;">
+    <img src="./fig/fanctionLoop.svg" alt="f-loop" width="500" />
+</div>
+
+<p>ここでは findNode に注目する。</p>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="hoare-logic--binary-tree--findnode">Hoare Logic での例 (Binary Tree : findNode)</h2>
+<ul>
+  <li>findNode では引数として受け取ったノードと木の現在見ているノードを比較して ノードを入れる位置を決定している</li>
+  <li>また、Tree を再構築するために辿った node を Stack に保存している</li>
+  <li>この時 Hoare Logic 上での {P} 、 {Q} は <strong>Tree と Stack の総量</strong> になると考えている</li>
+  <li>{P} が 元のTree と 中身のないStack で、 {Q} が 中身のないTree と 全てのNodeが入ったStack となる
+<!-- * replaceNode では逆に {P} が 中身のないTree と 全てのNodeが入ったStack で、 {Q} が Nodeが更新されたTree と 中身のないStack となるはずである --></li>
+  <li>このように <strong>C</strong> で不変な変数を見つけることでループなどの処理も部分的に正当であると証明することができる</li>
+</ul>
+
+<div style="text-align: center;">
+    <img src="./fig/funcLoopinAutomata.svg" alt="f-loop-auto" width="500" />
+</div>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="section-6">まとめと今後の方針</h2>
+
+<ul>
+  <li>本研究では CodeGear、DataGear を Agda で定義することができた</li>
+  <li>また Agda で Interface の記述及び Interface を含めた証明を行うことができた</li>
+  <li>これにより、 Interface を経由しても一部の性質は実装と同様の働きをすることが証明できた</li>
+  <li>また、CbC での Interface 記述では考えられていなかった細かな記述が明らかになった</li>
+  <li>今後の方針としては  継続を用いた Agda で Hoare Logic を表現し、その Hoare Logic をベースとして証明が行えるかを検討する</li>
+</ul>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="element">Element</h2>
+<ul lang="AGDA">
+  <li>Element の説明</li>
+</ul>
+<pre><code>record Element {l : Level} (a : Set l) : Set l where
+  inductive
+  constructor cons
+  field
+    datum : a  -- `data` is reserved by Agda.
+    next : Maybe (Element a)
+</code></pre>
+
+<!-- === end markdown block === -->
+</div>
+
+
+</div><!-- presentation -->
+</body>
+</html>
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Slide/sigos.md	Sat May 19 19:14:19 2018 +0900
@@ -0,0 +1,318 @@
+title: GearsOSのAgdaによる記述と検証
+author: Masataka Hokama, Shinji Kono
+profile: 琉球大学
+lang: Japanese
+code-engine: coderay
+
+<!-- <span style="background-color:#ffcc99"> </span> -->
+<!-- ```C -->
+<!-- <span style="background-color:#ffcc99">hoge</span> -->
+<!-- ``` -->
+
+
+## 本発表の流れ
+* 研究目的
+* CodeGear と DataGear の説明
+* Agda での記述
+* Agda での CodeGear 、 DataGear 、 Interface の表現
+* 実際に行なった証明
+* 証明の改善
+* まとめ
+
+## プログラムの信頼性の保証
+* 動作するプログラムの信頼性を保証したい
+* 保証をするためには仕様を検証する必要がある
+* 仕様を検証するにはモデル検査と **定理証明** の２つの手法がある
+  * モデル検査 はプログラムの持つ状態を数え上げて仕様を満たしているかを確認するもの
+  * 定理証明　はプログラムの性質を論理式で記述し、型を生成する関数を定義することで証明を記述できるもの
+* 当研究室では検証しやすい単位として CodeGear、DataGear という単位を用いてプログラムを記述する手法を提案している
+
+## プログラムの信頼性の保証
+* 本研究では **定理証明支援系** の言語 **Agda** をつかって仕様を検証した
+* 当研究室では 信頼性の高い ~ として GearsOS という OS を開発している
+* CodeGear DataGear での プログラミングは 関数型に近いかたちのプログラミングになる
+* Agda は関数型言語であるため 近い形になると考えた~
+* データ構造を仕様と実装に分けて記述するため、モジュール化の仕組みである **Interface** を記述した
+* 今回は Agda で CodeGear 、DataGear、という単位と Interface を定義した
+* また、 CodeGear 、DataGear を用いて Agda 上に実装された Stack を Interface を通して呼び出し、その性質の一部について証明を行った
+
+## CodeGear と DataGear の定義
+* CodeGear とはプログラムを記述する際の処理の単位
+* DataGear は CodeGear で扱うデータの単位で、処理に必要なデータが全て入っている
+* CodeGear はメタ計算によって別の CodeGear へ接続される
+
+<div style="text-align: center;">
+    <img src="./fig/meta.svg" alt="goto" width="800">
+</div>
+
+<!-- ## Agda での CodeGear、 DataGear　の表現 -->
+<!-- * CodeGear は処理の単位なので、 Agda では通常関数として記述するものとする -->
+<!-- * DataGear はレコード型で定義できるため、 Agda の record を使用し記述する -->
+
+次のスライドからは Agda の記述について解説を行う
+
+## Agda での型
+<!-- a->b->c  a ->(b->c) でスライド一枚 -->
+<!-- Code : SingleLinkedStack a -> (Maybe a) -> t の部分も上のスライドに入れる 写真にあるやつを例に入れる -->
+<!-- t の話もいれる -->
+* Agda の 型は **関数名 : 型** のように **:** を使って定義される
+* ここでは Stack の**実装**である **popSingleLinkedStack** の型を例とする
+* この型は stack を受け取り、stack の先頭を取って、次の関数に渡すという関数の型
+* stack は空の可能性があるので Maybe a を返す
+* popSingleLinkedStack は Stack の pop のCodeGearで、継続に型 Maybe a を受けとる CodeGear <span style="background-color:#ffcc99">( **(fa -> t) -> t**)</span> に渡す
+
+```AGDA
+popSingleLinkedStack : SingleLinkedStack a ->
+   (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
+```
+
+## Maybe
+(x : A) の説明
+* **Maybe** はNothingかJustの２つの場合を持つ型で Agda の **data** として定義されている
+* Just か Nothing はパターンマッチで場合分けするNothing と Just a は Maybe を生成する constructor
+
+```AGDA
+data Maybe a : Set where
+  Nothing : Maybe a
+  Just    : a -> Maybe a
+```
+
+## data を用いた等式の証明
+<!-- sym x==y,y==x の 証明をいれる 写真 -->
+* x ≡ x は Agda では常に正しい論理式
+* data は **data データ名 : 型**
+* **refl** は左右の項が等しいことを表す x ≡ x を生成する項
+*  x ≡ x を証明したい時には refl と書く
+
+```AGDA
+data _≡_ {a} {A : Set a} (x : A) : A → Set a where
+  refl : x ≡ x
+```
+
+## Agda での関数
+<!-- with と | で場合分けができます -->
+* Agda での関数定義は **関数名 = 関数の実装**
+* ここでは **popSingleLinkedStack** の関数を例とする
+* 引数は **関数名** と **=** の間に記述する
+* stack と 次の CodeGear である cs を受け取り、 stack の中から data を取り出し、新しい stack に継続し、次の CodeGear へと stack 渡している
+* stack の top は Maybe a なので Nothing か Just が返ってくる
+* **with** で data のパターンマッチができる
+
+```AGDA
+popSingleLinkedStack stack cs with (top stack)
+popSingleLinkedStack stack cs | Nothing = cs stack  Nothing
+popSingleLinkedStack stack cs | Just d  = cs record  { top = (next d) } (Just (datum d))
+```
+
+## Agda での record　の定義
+<!-- data が表してるのは等式と場合分け -->
+<!-- data の直積 object が欲しい Agda では~ -->
+<!-- Element のスライドもいれる -->
+<!-- top はアクセサ -->
+* record は複数のデータをまとめて記述する型
+* **record レコード名** を書き、その次の行の **field** 後に **フィールド名:型名** と列挙する
+* ここでは SingleLinkedStack の定義を例とする
+* 定義では top フィールドのみを定義しているが複数定義することもできる
+* top には Element 型の要素 a が定義されており、 **Element** 型は現在の **data** と次の data を指す **next** を定義している
+
+```AGDA
+record SingleLinkedStack (a : Set) : Set where
+  field
+    top : Maybe (Element a)
+```
+
+## Element
+* Element の説明
+```AGDA
+record Element {l : Level} (a : Set l) : Set l where
+  inductive
+  constructor cons
+  field
+    datum : a  -- `data` is reserved by Agda.
+    next : Maybe (Element a)
+```
+
+
+## Agda での record の構築
+* record の構築は関数側
+* **record** 後ろの **{}** 内部で **フィールド名 = 値** で列挙する
+* 複数のレコードを記述するさいは **;** で区切る
+* 例として **pushSingleLinkedStack** の関数部分を扱う
+* pushSingleLinkedStack では stack と data を受け取り、 CodeGear 中で Data を stack に入れ、新しいstack を継続し、次の CodeGear に継続している
+
+```Agda
+pushSingleLinkedStack stack datum next =
+    next record {top = Just (record {datum = datum;next =(top stack)})}
+```
+
+## Agda での Interface の定義
+<!-- Si -> a -> Si -->
+<!-- Si -> a (Si -> t) -> t -->
+<!-- t は 不定な感じ -->
+* Stack の仕様を実装とは別に記述するために record で Stack の Interface を記述した
+* ここでの push、 pop は仕様の型のみ記述され、実装は構築時に与える
+* t は継続を返す型を表し、次の CodeGear を指す
+* ここでの push 、 pop は pushSingleLinkedStack 、 popSingleLinkedStack に繋げる
+
+```AGDA
+record StackMethods {n m : Level } (a : Set n )
+    {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where
+      field
+        push : stackImpl -> a -> (stackImpl -> t) -> t
+        pop  : stackImpl -> (stackImpl -> Maybe a -> t) -> t
+```
+
+## 証明の概要
+* 今回は Interface を通して、 **任意の数** を stack に push し、データが入った stack に対して pop を行なう
+* このとき push した値と pop した値が等しくなることを証明する
+* また、どのような状態の Stack に push し、 pop をしても値が等しくなることを示したい
+* そのため、**状態の不定な** Stack を作成する関数を定義した
+
+## 状態が不定な Stack の定義
+* ここでは状態が不定な Stack を作成する関数 **stackInSomeState** を定義する
+* 不定なstackを入力(s : SingleLinkedStack a )で与える
+* stackInSomeState は stack を受け取り、状態の決まっていない stack を構築する
+
+```AGDA
+stackInSomeState : (s : SingleLinkedStack a ) -> Stack a ( SingleLinkedStack  a )
+stackInSomeState s =  record { stack = s ; stackMethods = singleLinkedStackSpec }
+```
+
+## Agda での Interface を含めた部分的な証明
+* 証明部分は型部分にラムダ式で与える
+* **push->push->pop2**では push を２回したときの値と、直後に pop を2回して取れた値が等しいことを型に記述している
+
+```AGDA
+push->push->pop2 : {l : Level } {a : Set l} (x y : a ) (s : SingleLinkedStack a ) ->
+    pushStack ( stackInSomeState s )  x ( \s1 -> pushStack s1 y ( \s2 ->
+    pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
+push->push->pop2 {l} {a} x y s = ?
+```
+
+## ラムダ式
+* **\s1 ->** はラムダ式で push->push->pop2 の型では次の CodeGear 部分にラムダ式を使いStackを渡している
+
+```AGDA
+push->push->pop2 : {l : Level } {a : Set l} (x y : a ) (s : SingleLinkedStack a ) ->
+    pushStack ( stackInSomeState s )  x ( \s1 ->* pushStack s1 y ( \s2 ->
+    pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
+```
+
+## Agda での Interface を含めた部分的な証明
+* Agda では不明な部分を **?** と書くことができる
+* **?** 部分はコンパイルすると **{}n** のように番号が付き、Agda から内部に入る型を示してもらえる
+
+```AGDA
+push->push->pop2 {l} {a} x y s = { }0
+```
+
+```AGDA
+-- Goal
+?0 : pushStack (stackInSomeState s) x
+(λ s1 →
+   pushStack s1 y
+   (λ s2 → pop2Stack s2 (λ s3 y1 x1 → (Just x ≡ x1) ∧ (Just y ≡ y1))))
+```
+
+## Agda での Interface を含めた部分的な証明
+* ここでは最終的に **(Just x ≡ x1) ∧ (Just y ≡ y1)** が返ってくる必要がある
+* **(x ≡ x1)** と **(y ≡ y1)** の２つが同時に成り立つ必要がある
+* そこで **∧** の部分を record で定義した
+
+```AGDA
+-- Goal
+?0 : pushStack (stackInSomeState s) x
+(λ s1 →
+   pushStack s1 y
+   (λ s2 → pop2Stack s2 (λ s3 y1 x1 → (Just x ≡ x1) ∧ (Just y ≡ y1))))
+```
+
+## Agda での Interface を含めた部分的な証明(∧)
+* a と b の２つの証明から a かつ b という証明を行うため **∧** を定義する
+* これには異なる２つのものを引数にとり、それらがレコードに同時に存在することが示せれば良い
+* **∧** は 型 a と 型b をもつ2つの要素を左右にとり、 それらが同時に存在することを示すレコード型
+
+```AGDA
+record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where
+  field
+    pi1 : a
+    pi2 : b
+```
+
+## Agda での Interface を含めた部分的な証明
+* 定義した ∧ を関数部分で構築する
+* ここでは **pi1** 、 **pi2** の両方を **?** としておく
+
+
+```AGDA
+push->push->pop2 : {l : Level } {a : Set l} (x y : a ) (s : SingleLinkedStack a ) ->
+    pushStack ( stackInSomeState s )  x ( \s1 -> pushStack s1 y ( \s2 ->
+    pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
+push->push->pop2 {l} {a} x y s = record { pi1 = { }0 ; pi2 = { }1 }
+```
+
+```AGDA
+?0 : Just x ≡
+Just
+(Element.datum
+ (.stack.element (stack (stackInSomeState s)) x
+  (λ s1 →
+     pushStack
+     (record
+      { stack = s1 ; stackMethods = stackMethods (stackInSomeState s) })
+     y
+     (λ s2 →
+        pop2Stack s2 (λ s3 y1 x1 → (Just x ≡ x1) ∧ (Just y ≡ y1))))))
+```
+
+## Agda での Interface を含めた部分的な証明
+* ∧ で定義された左右に **x ≡ x1** と　**y ≡ y1** が入る
+* **x ≡ x1**、　**y ≡ y1** は共に **refl** で証明できる
+* pi1、pi2 は両方 refl が入ることで証明ができる
+* また、型に書かれた順で値が取り出されている為、最後のラムダ式で stack の性質である FIFO 通りに値が取れていることが分かる
+* これにより証明の目的であった「どのような状態の Stack に push し、 pop をしても値が等しくなる」ことを証明することができた
+
+```AGDA
+push->push->pop2 : {l : Level } {a : Set l} (x y : a ) (s : SingleLinkedStack a ) ->
+    pushStack ( stackInSomeState s )  x ( \s1 -> pushStack s1 y ( \s2 ->
+    pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
+push->push->pop2 {l} {a} x y s = record { pi1 = refl ; pi2 = refl }
+```
+
+## 手証明での限界
+* 現在 Binary Tree に対して近い証明を書いている
+* これは 「Tree に対して node を put し、 get した時取れる node の値は put した node と等しい」というもの
+* Tree に対する操作では root Node から Node を辿る Loop があり、それを展開しながら証明を書く
+* Agda 側が put した node と get した node が等しいことを分かってくれず、証明が完成していない…
+* 今後は新しい証明規則を導入して証明を行おうと考えている
+
+## Hoare Logic
+* Hoare Logic は Tony Hoare によって提案されたプログラムの部分的な正当性を検証するための手法
+* 前の状態を{P}(Pre-Condition)、後の状態を{Q}(Post-Condition)とし、前状態を C (Command) によって変更するといったもの
+* この {P} C {Q} でプログラムを部分的に表すことができる
+* {P} が成り立つときに、 C を実行すると、実行後は必ず {Q} が成り立つとき、部分的に正当である
+
+<div style="text-align: center;">
+    <img src="./fig/hoare.svg" alt="hoare" width="1000">
+</div>
+
+
+## Hoare Logic と CbC
+
+* Hoare Logic の状態と処理を CodeGear、 DataGear の単位で考えることができると考えている
+* Pre-condition を input DataGear , Post-Conditon を output DataGear , Command は CodeGear そのものとして扱えると考えている。
+
+<div style="text-align: center;">
+    <img src="./fig/hoare-cbc.svg" alt="cbc-hoare" width="800">
+</div>
+
+
+
+## まとめと今後の方針
+* 本研究では CodeGear、DataGear を Agda で定義することができた
+* また Agda で Interface の記述及び Interface を含めた証明を行うことができた
+* これにより、 Interface を経由しても一部の性質は実装と同様の働きをすることが証明できた
+* また、CbC での Interface 記述では考えられていなかった細かな記述が明らかになった
+* 今後は RedBlackTree や syncronisedQueue に対して証明を行う
+<!-- * 今後の方針としては  継続を用いた Agda で Hoare Logic を表現し、その Hoare Logic をベースとして証明が行えるかを検討する -->
+