Mercurial > hg > Papers > 2021 > soto-prosym

comparison MindMap/slide.html @ 10:60d4617eac84

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix slide intro
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Thu, 06 Jan 2022 13:59:12 +0900
parents e02e29a614c9
children 62e56d73f104
comparison
equal deleted inserted replaced
9:e02e29a614c9 10:60d4617eac84
7 * 7 *
8 * @auto-scaling true 8 * @auto-scaling true
9 * @size 16:9 1280px 720px 9 * @size 16:9 1280px 720px
10 * @size 4:3 960px 720px 10 * @size 4:3 960px 720px
11 */div#p>svg>foreignObject>section{-ms-text-size-adjust:100%;-webkit-text-size-adjust:100%;word-wrap:break-word;background-color:#fff;color:#24292f;font-family:-apple-system,BlinkMacSystemFont,Segoe UI,Helvetica,Arial,sans-serif,Apple Color Emoji,Segoe UI Emoji;font-size:16px;line-height:1.5;margin:0}div#p>svg>foreignObject>section{--marpit-root-font-size:16px}div#p>svg>foreignObject>section .octicon{fill:currentColor;display:inline-block;vertical-align:text-bottom}div#p>svg>foreignObject>section h1:hover .anchor .octicon-link:before,div#p>svg>foreignObject>section h2:hover .anchor .octicon-link:before,div#p>svg>foreignObject>section h3:hover .anchor .octicon-link:before,div#p>svg>foreignObject>section h4:hover .anchor .octicon-link:before,div#p>svg>foreignObject>section h5:hover .anchor .octicon-link:before,div#p>svg>foreignObject>section h6:hover .anchor .octicon-link:before{background-color:currentColor;content:" ";display:inline-block;height:16px;-webkit-mask-image:url('data:image/svg+xml;charset=utf-8,<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 16 16" aria-hidden="true"><path fill-rule="evenodd" d="M7.775 3.275a.75.75 0 0 0 1.06 1.06l1.25-1.25a2 2 0 1 1 2.83 2.83l-2.5 2.5a2 2 0 0 1-2.83 0 .75.75 0 0 0-1.06 1.06 3.5 3.5 0 0 0 4.95 0l2.5-2.5a3.5 3.5 0 0 0-4.95-4.95l-1.25 1.25zm-4.69 9.64a2 2 0 0 1 0-2.83l2.5-2.5a2 2 0 0 1 2.83 0 .75.75 0 0 0 1.06-1.06 3.5 3.5 0 0 0-4.95 0l-2.5 2.5a3.5 3.5 0 0 0 4.95 4.95l1.25-1.25a.75.75 0 0 0-1.06-1.06l-1.25 1.25a2 2 0 0 1-2.83 0z"/></svg>');mask-image:url('data:image/svg+xml;charset=utf-8,<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 16 16" aria-hidden="true"><path fill-rule="evenodd" d="M7.775 3.275a.75.75 0 0 0 1.06 1.06l1.25-1.25a2 2 0 1 1 2.83 2.83l-2.5 2.5a2 2 0 0 1-2.83 0 .75.75 0 0 0-1.06 1.06 3.5 3.5 0 0 0 4.95 0l2.5-2.5a3.5 3.5 0 0 0-4.95-4.95l-1.25 1.25zm-4.69 9.64a2 2 0 0 1 0-2.83l2.5-2.5a2 2 0 0 1 2.83 0 .75.75 0 0 0 1.06-1.06 3.5 3.5 0 0 0-4.95 0l-2.5 2.5a3.5 3.5 0 0 0 4.95 4.95l1.25-1.25a.75.75 0 0 0-1.06-1.06l-1.25 1.25a2 2 0 0 1-2.83 0z"/></svg>');width:16px}div#p>svg>foreignObject>section details,div#p>svg>foreignObject>section figcaption,div#p>svg>foreignObject>section figure{display:block}div#p>svg>foreignObject>section summary{display:list-item}div#p>svg>foreignObject>section a{background-color:transparent;color:#0969da;text-decoration:none}div#p>svg>foreignObject>section a:active,div#p>svg>foreignObject>section a:hover{outline-width:0}div#p>svg>foreignObject>section abbr[title]{border-bottom:none;-webkit-text-decoration:underline dotted;text-decoration:underline dotted}div#p>svg>foreignObject>section b,div#p>svg>foreignObject>section strong{font-weight:600}div#p>svg>foreignObject>section dfn{font-style:italic}div#p>svg>foreignObject>section h1{border-bottom:1px solid #d8dee4;font-size:2em;font-weight:600;margin:.67em 0;padding-bottom:.3em}div#p>svg>foreignObject>section mark{background-color:#ff0;color:#24292f}div#p>svg>foreignObject>section small{font-size:90%}div#p>svg>foreignObject>section sub,div#p>svg>foreignObject>section sup{font-size:75%;line-height:0;position:relative;vertical-align:baseline}div#p>svg>foreignObject>section sub{bottom:-.25em}div#p>svg>foreignObject>section sup{top:-.5em}div#p>svg>foreignObject>section img{background-color:#fff;border-style:none;box-sizing:content-box;max-width:100%}div#p>svg>foreignObject>section code,div#p>svg>foreignObject>section kbd,div#p>svg>foreignObject>section pre,div#p>svg>foreignObject>section samp{font-family:monospace,monospace;font-size:1em}div#p>svg>foreignObject>section figure{margin:1em 40px}div#p>svg>foreignObject>section hr{background:transparent;background-color:#d0d7de;border:0;box-sizing:content-box;height:.25em;margin:24px 0;overflow:hidden;padding:0}div#p>svg>foreignObject>section [type=reset],div#p>svg>foreignObject>section [type=submit],div#p>svg>foreignObject>section html [type=button]{-webkit-appearance:button}div#p>svg>foreignObject>section [type=button]::-moz-focus-inner,div#p>svg>foreignObject>section [type=reset]::-moz-focus-inner,div#p>svg>foreignObject>section [type=submit]::-moz-focus-inner{border-style:none;padding:0}div#p>svg>foreignObject>section [type=button]:-moz-focusring,div#p>svg>foreignObject>section [type=reset]:-moz-focusring,div#p>svg>foreignObject>section [type=submit]:-moz-focusring{outline:1px dotted ButtonText}div#p>svg>foreignObject>section [type=checkbox],div#p>svg>foreignObject>section [type=radio]{box-sizing:border-box;padding:0}div#p>svg>foreignObject>section [type=number]::-webkit-inner-spin-button,div#p>svg>foreignObject>section [type=number]::-webkit-outer-spin-button{height:auto}div#p>svg>foreignObject>section [type=search]{-webkit-appearance:textfield;outline-offset:-2px}div#p>svg>foreignObject>section [type=search]::-webkit-search-cancel-button,div#p>svg>foreignObject>section [type=search]::-webkit-search-decoration{-webkit-appearance:none}div#p>svg>foreignObject>section ::-webkit-input-placeholder{color:inherit;opacity:.54}div#p>svg>foreignObject>section ::-webkit-file-upload-button{-webkit-appearance:button;font:inherit}div#p>svg>foreignObject>section a:hover{text-decoration:underline}div#p>svg>foreignObject>section hr:after,div#p>svg>foreignObject>section hr:before{content:"";display:table}div#p>svg>foreignObject>section hr:after{clear:both}div#p>svg>foreignObject>section table{border-collapse:collapse;border-spacing:0;display:block;max-width:100%;overflow:auto;width:-webkit-max-content;width:-moz-max-content;width:max-content}div#p>svg>foreignObject>section td,div#p>svg>foreignObject>section th{padding:0}div#p>svg>foreignObject>section details summary{cursor:pointer}div#p>svg>foreignObject>section details:not([open])>:not(summary){display:none!important}div#p>svg>foreignObject>section kbd{background-color:#f6f8fa;border:1px solid rgba(175,184,193,.2);border-radius:6px;box-shadow:inset 0 -1px 0 rgba(175,184,193,.2);color:#24292f;display:inline-block;font:11px ui-monospace,SFMono-Regular,SF Mono,Menlo,Consolas,Liberation Mono,monospace;line-height:10px;padding:3px 5px;vertical-align:middle}div#p>svg>foreignObject>section h1,div#p>svg>foreignObject>section h2,div#p>svg>foreignObject>section h3,div#p>svg>foreignObject>section h4,div#p>svg>foreignObject>section h5,div#p>svg>foreignObject>section h6{font-weight:600;line-height:1.25;margin-bottom:16px;margin-top:24px}div#p>svg>foreignObject>section h2{border-bottom:1px solid #d8dee4;font-size:1.5em;font-weight:600;padding-bottom:.3em}div#p>svg>foreignObject>section h3{font-size:1.25em;font-weight:600}div#p>svg>foreignObject>section h4{font-size:1em;font-weight:600}div#p>svg>foreignObject>section h5{font-size:.875em;font-weight:600}div#p>svg>foreignObject>section h6{color:#57606a;font-size:.85em;font-weight:600}div#p>svg>foreignObject>section p{margin-bottom:10px;margin-top:0}div#p>svg>foreignObject>section blockquote{border-left:.25em solid #d0d7de;color:#57606a;margin:0;padding:0 1em}div#p>svg>foreignObject>section ol,div#p>svg>foreignObject>section ul{margin-bottom:0;margin-top:0;padding-left:2em}div#p>svg>foreignObject>section ol ol,div#p>svg>foreignObject>section ul ol{list-style-type:lower-roman}div#p>svg>foreignObject>section ol ol ol,div#p>svg>foreignObject>section ol ul ol,div#p>svg>foreignObject>section ul ol ol,div#p>svg>foreignObject>section ul ul ol{list-style-type:lower-alpha}div#p>svg>foreignObject>section dd{margin-left:0}div#p>svg>foreignObject>section code,div#p>svg>foreignObject>section pre,div#p>svg>foreignObject>section tt{font-family:ui-monospace,SFMono-Regular,SF Mono,Menlo,Consolas,Liberation Mono,monospace;font-size:12px}div#p>svg>foreignObject>section pre{word-wrap:normal;margin-bottom:0;margin-top:0}div#p>svg>foreignObject>section :-ms-input-placeholder{color:#6e7781;opacity:1}div#p>svg>foreignObject>section ::-moz-placeholder{color:#6e7781;opacity:1}div#p>svg>foreignObject>section ::placeholder{color:#6e7781;opacity:1}div#p>svg>foreignObject>section .pl-c{color:#6e7781}div#p>svg>foreignObject>section .pl-c1,div#p>svg>foreignObject>section .pl-s .pl-v{color:#0550ae}div#p>svg>foreignObject>section .pl-e,div#p>svg>foreignObject>section .pl-en{color:#8250df}div#p>svg>foreignObject>section .pl-s .pl-s1,div#p>svg>foreignObject>section .pl-smi{color:#24292f}div#p>svg>foreignObject>section .pl-ent{color:#116329}div#p>svg>foreignObject>section .pl-k{color:#cf222e}div#p>svg>foreignObject>section .pl-pds,div#p>svg>foreignObject>section .pl-s,div#p>svg>foreignObject>section .pl-s .pl-pse .pl-s1,div#p>svg>foreignObject>section .pl-sr,div#p>svg>foreignObject>section .pl-sr .pl-cce,div#p>svg>foreignObject>section .pl-sr .pl-sra,div#p>svg>foreignObject>section .pl-sr .pl-sre{color:#0a3069}div#p>svg>foreignObject>section .pl-smw,div#p>svg>foreignObject>section .pl-v{color:#953800}div#p>svg>foreignObject>section .pl-bu{color:#82071e}div#p>svg>foreignObject>section .pl-ii{background-color:#82071e;color:#f6f8fa}div#p>svg>foreignObject>section .pl-c2{background-color:#cf222e;color:#f6f8fa}div#p>svg>foreignObject>section .pl-sr .pl-cce{color:#116329;font-weight:700}div#p>svg>foreignObject>section .pl-ml{color:#3b2300}div#p>svg>foreignObject>section .pl-mh,div#p>svg>foreignObject>section .pl-mh .pl-en,div#p>svg>foreignObject>section .pl-ms{color:#0550ae;font-weight:700}div#p>svg>foreignObject>section .pl-mi{color:#24292f;font-style:italic}div#p>svg>foreignObject>section .pl-mb{color:#24292f;font-weight:700}div#p>svg>foreignObject>section .pl-md{background-color:#ffebe9;color:#82071e}div#p>svg>foreignObject>section .pl-mi1{background-color:#dafbe1;color:#116329}div#p>svg>foreignObject>section .pl-mc{background-color:#ffd8b5;color:#953800}div#p>svg>foreignObject>section .pl-mi2{background-color:#0550ae;color:#eaeef2}div#p>svg>foreignObject>section .pl-mdr{color:#8250df;font-weight:700}div#p>svg>foreignObject>section .pl-ba{color:#57606a}div#p>svg>foreignObject>section .pl-sg{color:#8c959f}div#p>svg>foreignObject>section .pl-corl{color:#0a3069;text-decoration:underline}div#p>svg>foreignObject>section [data-catalyst]{display:block}div#p>svg>foreignObject>section g-emoji{font-family:Apple Color Emoji,Segoe UI Emoji,Segoe UI Symbol;font-size:1em;font-style:normal!important;font-weight:400;line-height:1;vertical-align:-.075em}div#p>svg>foreignObject>section g-emoji img{height:1em;width:1em}div#p>svg>foreignObject>section:after,div#p>svg>foreignObject>section:before{ 11 */div#p>svg>foreignObject>section{-ms-text-size-adjust:100%;-webkit-text-size-adjust:100%;word-wrap:break-word;background-color:#fff;color:#24292f;font-family:-apple-system,BlinkMacSystemFont,Segoe UI,Helvetica,Arial,sans-serif,Apple Color Emoji,Segoe UI Emoji;font-size:16px;line-height:1.5;margin:0}div#p>svg>foreignObject>section{--marpit-root-font-size:16px}div#p>svg>foreignObject>section .octicon{fill:currentColor;display:inline-block;vertical-align:text-bottom}div#p>svg>foreignObject>section h1:hover .anchor .octicon-link:before,div#p>svg>foreignObject>section h2:hover .anchor .octicon-link:before,div#p>svg>foreignObject>section h3:hover .anchor .octicon-link:before,div#p>svg>foreignObject>section h4:hover .anchor .octicon-link:before,div#p>svg>foreignObject>section h5:hover .anchor .octicon-link:before,div#p>svg>foreignObject>section h6:hover .anchor .octicon-link:before{background-color:currentColor;content:" ";display:inline-block;height:16px;-webkit-mask-image:url('data:image/svg+xml;charset=utf-8,<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 16 16" aria-hidden="true"><path fill-rule="evenodd" d="M7.775 3.275a.75.75 0 0 0 1.06 1.06l1.25-1.25a2 2 0 1 1 2.83 2.83l-2.5 2.5a2 2 0 0 1-2.83 0 .75.75 0 0 0-1.06 1.06 3.5 3.5 0 0 0 4.95 0l2.5-2.5a3.5 3.5 0 0 0-4.95-4.95l-1.25 1.25zm-4.69 9.64a2 2 0 0 1 0-2.83l2.5-2.5a2 2 0 0 1 2.83 0 .75.75 0 0 0 1.06-1.06 3.5 3.5 0 0 0-4.95 0l-2.5 2.5a3.5 3.5 0 0 0 4.95 4.95l1.25-1.25a.75.75 0 0 0-1.06-1.06l-1.25 1.25a2 2 0 0 1-2.83 0z"/></svg>');mask-image:url('data:image/svg+xml;charset=utf-8,<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 16 16" aria-hidden="true"><path fill-rule="evenodd" d="M7.775 3.275a.75.75 0 0 0 1.06 1.06l1.25-1.25a2 2 0 1 1 2.83 2.83l-2.5 2.5a2 2 0 0 1-2.83 0 .75.75 0 0 0-1.06 1.06 3.5 3.5 0 0 0 4.95 0l2.5-2.5a3.5 3.5 0 0 0-4.95-4.95l-1.25 1.25zm-4.69 9.64a2 2 0 0 1 0-2.83l2.5-2.5a2 2 0 0 1 2.83 0 .75.75 0 0 0 1.06-1.06 3.5 3.5 0 0 0-4.95 0l-2.5 2.5a3.5 3.5 0 0 0 4.95 4.95l1.25-1.25a.75.75 0 0 0-1.06-1.06l-1.25 1.25a2 2 0 0 1-2.83 0z"/></svg>');width:16px}div#p>svg>foreignObject>section details,div#p>svg>foreignObject>section figcaption,div#p>svg>foreignObject>section figure{display:block}div#p>svg>foreignObject>section summary{display:list-item}div#p>svg>foreignObject>section a{background-color:transparent;color:#0969da;text-decoration:none}div#p>svg>foreignObject>section a:active,div#p>svg>foreignObject>section a:hover{outline-width:0}div#p>svg>foreignObject>section abbr[title]{border-bottom:none;-webkit-text-decoration:underline dotted;text-decoration:underline dotted}div#p>svg>foreignObject>section b,div#p>svg>foreignObject>section strong{font-weight:600}div#p>svg>foreignObject>section dfn{font-style:italic}div#p>svg>foreignObject>section h1{border-bottom:1px solid #d8dee4;font-size:2em;font-weight:600;margin:.67em 0;padding-bottom:.3em}div#p>svg>foreignObject>section mark{background-color:#ff0;color:#24292f}div#p>svg>foreignObject>section small{font-size:90%}div#p>svg>foreignObject>section sub,div#p>svg>foreignObject>section sup{font-size:75%;line-height:0;position:relative;vertical-align:baseline}div#p>svg>foreignObject>section sub{bottom:-.25em}div#p>svg>foreignObject>section sup{top:-.5em}div#p>svg>foreignObject>section img{background-color:#fff;border-style:none;box-sizing:content-box;max-width:100%}div#p>svg>foreignObject>section code,div#p>svg>foreignObject>section kbd,div#p>svg>foreignObject>section pre,div#p>svg>foreignObject>section samp{font-family:monospace,monospace;font-size:1em}div#p>svg>foreignObject>section figure{margin:1em 40px}div#p>svg>foreignObject>section hr{background:transparent;background-color:#d0d7de;border:0;box-sizing:content-box;height:.25em;margin:24px 0;overflow:hidden;padding:0}div#p>svg>foreignObject>section [type=reset],div#p>svg>foreignObject>section [type=submit],div#p>svg>foreignObject>section html [type=button]{-webkit-appearance:button}div#p>svg>foreignObject>section [type=button]::-moz-focus-inner,div#p>svg>foreignObject>section [type=reset]::-moz-focus-inner,div#p>svg>foreignObject>section [type=submit]::-moz-focus-inner{border-style:none;padding:0}div#p>svg>foreignObject>section [type=button]:-moz-focusring,div#p>svg>foreignObject>section [type=reset]:-moz-focusring,div#p>svg>foreignObject>section [type=submit]:-moz-focusring{outline:1px dotted ButtonText}div#p>svg>foreignObject>section [type=checkbox],div#p>svg>foreignObject>section [type=radio]{box-sizing:border-box;padding:0}div#p>svg>foreignObject>section [type=number]::-webkit-inner-spin-button,div#p>svg>foreignObject>section [type=number]::-webkit-outer-spin-button{height:auto}div#p>svg>foreignObject>section [type=search]{-webkit-appearance:textfield;outline-offset:-2px}div#p>svg>foreignObject>section [type=search]::-webkit-search-cancel-button,div#p>svg>foreignObject>section [type=search]::-webkit-search-decoration{-webkit-appearance:none}div#p>svg>foreignObject>section ::-webkit-input-placeholder{color:inherit;opacity:.54}div#p>svg>foreignObject>section ::-webkit-file-upload-button{-webkit-appearance:button;font:inherit}div#p>svg>foreignObject>section a:hover{text-decoration:underline}div#p>svg>foreignObject>section hr:after,div#p>svg>foreignObject>section hr:before{content:"";display:table}div#p>svg>foreignObject>section hr:after{clear:both}div#p>svg>foreignObject>section table{border-collapse:collapse;border-spacing:0;display:block;max-width:100%;overflow:auto;width:-webkit-max-content;width:-moz-max-content;width:max-content}div#p>svg>foreignObject>section td,div#p>svg>foreignObject>section th{padding:0}div#p>svg>foreignObject>section details summary{cursor:pointer}div#p>svg>foreignObject>section details:not([open])>:not(summary){display:none!important}div#p>svg>foreignObject>section kbd{background-color:#f6f8fa;border:1px solid rgba(175,184,193,.2);border-radius:6px;box-shadow:inset 0 -1px 0 rgba(175,184,193,.2);color:#24292f;display:inline-block;font:11px ui-monospace,SFMono-Regular,SF Mono,Menlo,Consolas,Liberation Mono,monospace;line-height:10px;padding:3px 5px;vertical-align:middle}div#p>svg>foreignObject>section h1,div#p>svg>foreignObject>section h2,div#p>svg>foreignObject>section h3,div#p>svg>foreignObject>section h4,div#p>svg>foreignObject>section h5,div#p>svg>foreignObject>section h6{font-weight:600;line-height:1.25;margin-bottom:16px;margin-top:24px}div#p>svg>foreignObject>section h2{border-bottom:1px solid #d8dee4;font-size:1.5em;font-weight:600;padding-bottom:.3em}div#p>svg>foreignObject>section h3{font-size:1.25em;font-weight:600}div#p>svg>foreignObject>section h4{font-size:1em;font-weight:600}div#p>svg>foreignObject>section h5{font-size:.875em;font-weight:600}div#p>svg>foreignObject>section h6{color:#57606a;font-size:.85em;font-weight:600}div#p>svg>foreignObject>section p{margin-bottom:10px;margin-top:0}div#p>svg>foreignObject>section blockquote{border-left:.25em solid #d0d7de;color:#57606a;margin:0;padding:0 1em}div#p>svg>foreignObject>section ol,div#p>svg>foreignObject>section ul{margin-bottom:0;margin-top:0;padding-left:2em}div#p>svg>foreignObject>section ol ol,div#p>svg>foreignObject>section ul ol{list-style-type:lower-roman}div#p>svg>foreignObject>section ol ol ol,div#p>svg>foreignObject>section ol ul ol,div#p>svg>foreignObject>section ul ol ol,div#p>svg>foreignObject>section ul ul ol{list-style-type:lower-alpha}div#p>svg>foreignObject>section dd{margin-left:0}div#p>svg>foreignObject>section code,div#p>svg>foreignObject>section pre,div#p>svg>foreignObject>section tt{font-family:ui-monospace,SFMono-Regular,SF Mono,Menlo,Consolas,Liberation Mono,monospace;font-size:12px}div#p>svg>foreignObject>section pre{word-wrap:normal;margin-bottom:0;margin-top:0}div#p>svg>foreignObject>section :-ms-input-placeholder{color:#6e7781;opacity:1}div#p>svg>foreignObject>section ::-moz-placeholder{color:#6e7781;opacity:1}div#p>svg>foreignObject>section ::placeholder{color:#6e7781;opacity:1}div#p>svg>foreignObject>section .pl-c{color:#6e7781}div#p>svg>foreignObject>section .pl-c1,div#p>svg>foreignObject>section .pl-s .pl-v{color:#0550ae}div#p>svg>foreignObject>section .pl-e,div#p>svg>foreignObject>section .pl-en{color:#8250df}div#p>svg>foreignObject>section .pl-s .pl-s1,div#p>svg>foreignObject>section .pl-smi{color:#24292f}div#p>svg>foreignObject>section .pl-ent{color:#116329}div#p>svg>foreignObject>section .pl-k{color:#cf222e}div#p>svg>foreignObject>section .pl-pds,div#p>svg>foreignObject>section .pl-s,div#p>svg>foreignObject>section .pl-s .pl-pse .pl-s1,div#p>svg>foreignObject>section .pl-sr,div#p>svg>foreignObject>section .pl-sr .pl-cce,div#p>svg>foreignObject>section .pl-sr .pl-sra,div#p>svg>foreignObject>section .pl-sr .pl-sre{color:#0a3069}div#p>svg>foreignObject>section .pl-smw,div#p>svg>foreignObject>section .pl-v{color:#953800}div#p>svg>foreignObject>section .pl-bu{color:#82071e}div#p>svg>foreignObject>section .pl-ii{background-color:#82071e;color:#f6f8fa}div#p>svg>foreignObject>section .pl-c2{background-color:#cf222e;color:#f6f8fa}div#p>svg>foreignObject>section .pl-sr .pl-cce{color:#116329;font-weight:700}div#p>svg>foreignObject>section .pl-ml{color:#3b2300}div#p>svg>foreignObject>section .pl-mh,div#p>svg>foreignObject>section .pl-mh .pl-en,div#p>svg>foreignObject>section .pl-ms{color:#0550ae;font-weight:700}div#p>svg>foreignObject>section .pl-mi{color:#24292f;font-style:italic}div#p>svg>foreignObject>section .pl-mb{color:#24292f;font-weight:700}div#p>svg>foreignObject>section .pl-md{background-color:#ffebe9;color:#82071e}div#p>svg>foreignObject>section .pl-mi1{background-color:#dafbe1;color:#116329}div#p>svg>foreignObject>section .pl-mc{background-color:#ffd8b5;color:#953800}div#p>svg>foreignObject>section .pl-mi2{background-color:#0550ae;color:#eaeef2}div#p>svg>foreignObject>section .pl-mdr{color:#8250df;font-weight:700}div#p>svg>foreignObject>section .pl-ba{color:#57606a}div#p>svg>foreignObject>section .pl-sg{color:#8c959f}div#p>svg>foreignObject>section .pl-corl{color:#0a3069;text-decoration:underline}div#p>svg>foreignObject>section [data-catalyst]{display:block}div#p>svg>foreignObject>section g-emoji{font-family:Apple Color Emoji,Segoe UI Emoji,Segoe UI Symbol;font-size:1em;font-style:normal!important;font-weight:400;line-height:1;vertical-align:-.075em}div#p>svg>foreignObject>section g-emoji img{height:1em;width:1em}div#p>svg>foreignObject>section:after,div#p>svg>foreignObject>section:before{
12 /* content:""; */display:table}div#p>svg>foreignObject>section:after{clear:both}div#p>svg>foreignObject>section>:first-child{margin-top:0!important}div#p>svg>foreignObject>section>:last-child{margin-bottom:0!important}div#p>svg>foreignObject>section a:not([href]){color:inherit;text-decoration:none}div#p>svg>foreignObject>section .absent{color:#cf222e}div#p>svg>foreignObject>section .anchor{float:left;line-height:1;margin-left:-20px;padding-right:4px}div#p>svg>foreignObject>section .anchor:focus{outline:none}div#p>svg>foreignObject>section blockquote,div#p>svg>foreignObject>section details,div#p>svg>foreignObject>section dl,div#p>svg>foreignObject>section ol,div#p>svg>foreignObject>section p,div#p>svg>foreignObject>section pre,div#p>svg>foreignObject>section table,div#p>svg>foreignObject>section ul{margin-bottom:16px;margin-top:0}div#p>svg>foreignObject>section blockquote>:first-child{margin-top:0}div#p>svg>foreignObject>section blockquote>:last-child{margin-bottom:0}div#p>svg>foreignObject>section sup>a:before{content:"["}div#p>svg>foreignObject>section sup>a:after{content:"]"}div#p>svg>foreignObject>section h1 .octicon-link,div#p>svg>foreignObject>section h2 .octicon-link,div#p>svg>foreignObject>section h3 .octicon-link,div#p>svg>foreignObject>section h4 .octicon-link,div#p>svg>foreignObject>section h5 .octicon-link,div#p>svg>foreignObject>section h6 .octicon-link{color:#24292f;vertical-align:middle;visibility:hidden}div#p>svg>foreignObject>section h1:hover .anchor,div#p>svg>foreignObject>section h2:hover .anchor,div#p>svg>foreignObject>section h3:hover .anchor,div#p>svg>foreignObject>section h4:hover .anchor,div#p>svg>foreignObject>section h5:hover .anchor,div#p>svg>foreignObject>section h6:hover .anchor{text-decoration:none}div#p>svg>foreignObject>section h1:hover .anchor .octicon-link,div#p>svg>foreignObject>section h2:hover .anchor .octicon-link,div#p>svg>foreignObject>section h3:hover .anchor .octicon-link,div#p>svg>foreignObject>section h4:hover .anchor .octicon-link,div#p>svg>foreignObject>section h5:hover .anchor .octicon-link,div#p>svg>foreignObject>section h6:hover .anchor .octicon-link{visibility:visible}div#p>svg>foreignObject>section h1 code,div#p>svg>foreignObject>section h1 tt,div#p>svg>foreignObject>section h2 code,div#p>svg>foreignObject>section h2 tt,div#p>svg>foreignObject>section h3 code,div#p>svg>foreignObject>section h3 tt,div#p>svg>foreignObject>section h4 code,div#p>svg>foreignObject>section h4 tt,div#p>svg>foreignObject>section h5 code,div#p>svg>foreignObject>section h5 tt,div#p>svg>foreignObject>section h6 code,div#p>svg>foreignObject>section h6 tt{font-size:inherit;padding:0 .2em}div#p>svg>foreignObject>section ol.no-list,div#p>svg>foreignObject>section ul.no-list{list-style-type:none;padding:0}div#p>svg>foreignObject>section ol[type="1"]{list-style-type:decimal}div#p>svg>foreignObject>section ol[type=a]{list-style-type:lower-alpha}div#p>svg>foreignObject>section ol[type=i]{list-style-type:lower-roman}div#p>svg>foreignObject>section div>ol:not([type]){list-style-type:decimal}div#p>svg>foreignObject>section ol ol,div#p>svg>foreignObject>section ol ul,div#p>svg>foreignObject>section ul ol,div#p>svg>foreignObject>section ul ul{margin-bottom:0;margin-top:0}div#p>svg>foreignObject>section li>p{margin-top:16px}div#p>svg>foreignObject>section li+li{margin-top:.25em}div#p>svg>foreignObject>section dl{padding:0}div#p>svg>foreignObject>section dl dt{font-size:1em;font-style:italic;font-weight:600;margin-top:16px;padding:0}div#p>svg>foreignObject>section dl dd{margin-bottom:16px;padding:0 16px}div#p>svg>foreignObject>section table th{font-weight:600}div#p>svg>foreignObject>section table td,div#p>svg>foreignObject>section table th{border:1px solid #d0d7de;padding:6px 13px}div#p>svg>foreignObject>section table tr{background-color:#fff;border-top:1px solid #d8dee4}div#p>svg>foreignObject>section table tr:nth-child(2n){background-color:#f6f8fa}div#p>svg>foreignObject>section table img{background-color:transparent}div#p>svg>foreignObject>section img[align=right]{padding-left:20px}div#p>svg>foreignObject>section img[align=left]{padding-right:20px}div#p>svg>foreignObject>section .emoji{background-color:transparent;max-width:none;vertical-align:text-top}div#p>svg>foreignObject>section span.frame,div#p>svg>foreignObject>section span.frame>span{display:block;overflow:hidden}div#p>svg>foreignObject>section span.frame>span{border:1px solid #d0d7de;float:left;margin:13px 0 0;padding:7px;width:auto}div#p>svg>foreignObject>section span.frame span img{display:block;float:left}div#p>svg>foreignObject>section span.frame span span{clear:both;color:#24292f;display:block;padding:5px 0 0}div#p>svg>foreignObject>section span.align-center{clear:both;display:block;overflow:hidden}div#p>svg>foreignObject>section span.align-center>span{display:block;margin:13px auto 0;overflow:hidden;text-align:center}div#p>svg>foreignObject>section span.align-center span img{margin:0 auto;text-align:center}div#p>svg>foreignObject>section span.align-right{clear:both;display:block;overflow:hidden}div#p>svg>foreignObject>section span.align-right>span{display:block;margin:13px 0 0;overflow:hidden;text-align:right}div#p>svg>foreignObject>section span.align-right span img{margin:0;text-align:right}div#p>svg>foreignObject>section span.float-left{display:block;float:left;margin-right:13px;overflow:hidden}div#p>svg>foreignObject>section span.float-left span{margin:13px 0 0}div#p>svg>foreignObject>section span.float-right{display:block;float:right;margin-left:13px;overflow:hidden}div#p>svg>foreignObject>section span.float-right>span{display:block;margin:13px auto 0;overflow:hidden;text-align:right}div#p>svg>foreignObject>section code,div#p>svg>foreignObject>section tt{background-color:rgba(175,184,193,.2);border-radius:6px;font-size:85%;margin:0;padding:.2em .4em}div#p>svg>foreignObject>section code br,div#p>svg>foreignObject>section tt br{display:none}div#p>svg>foreignObject>section del code{text-decoration:inherit}div#p>svg>foreignObject>section pre code{font-size:100%}div#p>svg>foreignObject>section pre>code{background:transparent;border:0;margin:0;padding:0;white-space:pre;word-break:normal}div#p>svg>foreignObject>section .highlight{margin-bottom:16px}div#p>svg>foreignObject>section .highlight pre{margin-bottom:0;word-break:normal}div#p>svg>foreignObject>section pre{background-color:#f6f8fa;border-radius:6px;font-size:85%;line-height:1.45;overflow:auto;padding:16px}div#p>svg>foreignObject>section pre code,div#p>svg>foreignObject>section pre tt{word-wrap:normal;background-color:transparent;border:0;display:inline;line-height:inherit;margin:0;max-width:auto;overflow:visible;padding:0}div#p>svg>foreignObject>section .csv-data td,div#p>svg>foreignObject>section .csv-data th{font-size:12px;line-height:1;overflow:hidden;padding:5px;text-align:left;white-space:nowrap}div#p>svg>foreignObject>section .csv-data .blob-num{background:#fff;border:0;padding:10px 8px 9px;text-align:right}div#p>svg>foreignObject>section .csv-data tr{border-top:0}div#p>svg>foreignObject>section .csv-data th{background:#f6f8fa;border-top:0;font-weight:600}div#p>svg>foreignObject>section .footnotes{border-top:1px solid #d0d7de;color:#57606a;font-size:12px}div#p>svg>foreignObject>section div#p>svg>foreignObject>section section.footnotes{--marpit-root-font-size:12px}div#p>svg>foreignObject>section .footnotes ol{padding-left:16px}div#p>svg>foreignObject>section .footnotes li{position:relative}div#p>svg>foreignObject>section .footnotes li:target:before{border:2px solid #0969da;border-radius:6px;bottom:-8px;content:"";left:-24px;pointer-events:none;position:absolute;right:-8px;top:-8px}div#p>svg>foreignObject>section .footnotes li:target{color:#24292f}div#p>svg>foreignObject>section .footnotes .data-footnote-backref g-emoji{font-family:monospace}div#p>svg>foreignObject>section [hidden]{display:none!important}div#p>svg>foreignObject>section ::-webkit-calendar-picker-indicator{filter:invert(50%)}div#p>svg>foreignObject>section .hljs{background:#fff;color:#333;display:block;overflow-x:auto;padding:.5em}div#p>svg>foreignObject>section .hljs-comment,div#p>svg>foreignObject>section .hljs-meta{color:#969896}div#p>svg>foreignObject>section .hljs-emphasis,div#p>svg>foreignObject>section .hljs-quote,div#p>svg>foreignObject>section .hljs-strong,div#p>svg>foreignObject>section .hljs-template-variable,div#p>svg>foreignObject>section .hljs-variable{color:#df5000}div#p>svg>foreignObject>section .hljs-keyword,div#p>svg>foreignObject>section .hljs-selector-tag,div#p>svg>foreignObject>section .hljs-type{color:#d73a49}div#p>svg>foreignObject>section .hljs-attribute,div#p>svg>foreignObject>section .hljs-bullet,div#p>svg>foreignObject>section .hljs-literal,div#p>svg>foreignObject>section .hljs-symbol{color:#0086b3}div#p>svg>foreignObject>section .hljs-name,div#p>svg>foreignObject>section .hljs-section{color:#63a35c}div#p>svg>foreignObject>section .hljs-tag{color:#333}div#p>svg>foreignObject>section .hljs-attr,div#p>svg>foreignObject>section .hljs-selector-attr,div#p>svg>foreignObject>section .hljs-selector-class,div#p>svg>foreignObject>section .hljs-selector-id,div#p>svg>foreignObject>section .hljs-selector-pseudo,div#p>svg>foreignObject>section .hljs-title{color:#6f42c1}div#p>svg>foreignObject>section .hljs-addition{background-color:#eaffea;color:#55a532}div#p>svg>foreignObject>section .hljs-deletion{background-color:#ffecec;color:#bd2c00}div#p>svg>foreignObject>section .hljs-link{text-decoration:underline}div#p>svg>foreignObject>section .hljs-number{color:#005cc5}div#p>svg>foreignObject>section .hljs-string{color:#032f62}div#p>svg>foreignObject>section svg[data-marp-fitting=svg]{max-height:563px}div#p>svg>foreignObject>section h1{color:#246;font-size:1.6em}div#p>svg>foreignObject>section h1,div#p>svg>foreignObject>section h2{border-bottom:none}div#p>svg>foreignObject>section h2{font-size:1.3em}div#p>svg>foreignObject>section h3{font-size:1.1em}div#p>svg>foreignObject>section h4{font-size:1.05em}div#p>svg>foreignObject>section h5{font-size:1em}div#p>svg>foreignObject>section h6{font-size:.9em}div#p>svg>foreignObject>section h1 strong,div#p>svg>foreignObject>section h2 strong,div#p>svg>foreignObject>section h3 strong,div#p>svg>foreignObject>section h4 strong,div#p>svg>foreignObject>section h5 strong,div#p>svg>foreignObject>section h6 strong{color:#48c;font-weight:inherit}div#p>svg>foreignObject>section hr{height:0;padding-top:.25em}div#p>svg>foreignObject>section pre{border:1px solid #999;line-height:1.15;overflow:visible}div#p>svg>foreignObject>section pre code svg[data-marp-fitting=svg]{max-height:529px}div#p>svg>foreignObject>section footer,div#p>svg>foreignObject>section header{color:hsla(0,0%,40%,.75);font-size:18px;left:30px;margin:0;position:absolute}div#p>svg>foreignObject>section header{top:21px}div#p>svg>foreignObject>section footer{bottom:21px}div#p>svg>foreignObject>section{align-items:stretch;background:#fff;display:flex;flex-flow:column nowrap;font-size:29px;height:720px;justify-content:center;padding:78.5px;width:1280px}div#p>svg>foreignObject>section{--marpit-root-font-size:29px}div#p>svg>foreignObject>section>:last-child,div#p>svg>foreignObject>section[data-footer]>:nth-last-child(2){margin-bottom:0}div#p>svg>foreignObject>section>:first-child,div#p>svg>foreignObject>section>header:first-child+*{margin-top:0}div#p>svg>foreignObject>section:after{bottom:21px;color:#777;font-size:24px;padding:0;position:absolute;right:30px}div#p>svg>foreignObject>section:after{--marpit-root-font-size:24px}div#p>svg>foreignObject>section.invert{background-color:#222;color:#e6eaf0}div#p>svg>foreignObject>section.invert:after{color:#999}div#p>svg>foreignObject>section.invert img{background-color:transparent}div#p>svg>foreignObject>section.invert a{color:#50b3ff}div#p>svg>foreignObject>section.invert h1{color:#a3c5e7}div#p>svg>foreignObject>section.invert h2,div#p>svg>foreignObject>section.invert h3,div#p>svg>foreignObject>section.invert h4,div#p>svg>foreignObject>section.invert h5{color:#ebeff5}div#p>svg>foreignObject>section.invert blockquote,div#p>svg>foreignObject>section.invert h6{border-color:#3d3f43;color:#939699}div#p>svg>foreignObject>section.invert h1 strong,div#p>svg>foreignObject>section.invert h2 strong,div#p>svg>foreignObject>section.invert h3 strong,div#p>svg>foreignObject>section.invert h4 strong,div#p>svg>foreignObject>section.invert h5 strong,div#p>svg>foreignObject>section.invert h6 strong{color:#7bf}div#p>svg>foreignObject>section.invert hr{background-color:#3d3f43}div#p>svg>foreignObject>section.invert footer,div#p>svg>foreignObject>section.invert header{color:hsla(0,0%,60%,.75)}div#p>svg>foreignObject>section.invert code,div#p>svg>foreignObject>section.invert kbd{background-color:#111}div#p>svg>foreignObject>section.invert kbd{border-color:#666;box-shadow:inset 0 -1px 0 #555;color:#e6eaf0}div#p>svg>foreignObject>section.invert table tr{background-color:#12181d;border-color:#60657b}div#p>svg>foreignObject>section.invert table tr:nth-child(2n){background-color:#1b2024}div#p>svg>foreignObject>section.invert table td,div#p>svg>foreignObject>section.invert table th{border-color:#5b5e61}div#p>svg>foreignObject>section.invert pre{background-color:#0a0e12;border-color:#777}div#p>svg>foreignObject>section.invert pre code{background-color:transparent}div#p>svg>foreignObject>section[data-color] h1,div#p>svg>foreignObject>section[data-color] h2,div#p>svg>foreignObject>section[data-color] h3,div#p>svg>foreignObject>section[data-color] h4,div#p>svg>foreignObject>section[data-color] h5,div#p>svg>foreignObject>section[data-color] h6{color:currentColor}div#p>svg>foreignObject>section{width:1280px;height:720px}div#p>svg>foreignObject>section{background-color:#FFFFFF;font-size:28px;color:#4b4b4b;font-family:"Droid Sans Mono","Hiragino Maru Gothic ProN";background-image:url("logo.svg");background-position:right 3% bottom 2%;background-repeat:no-repeat;background-attachment:5%;background-size:20% auto}div#p>svg>foreignObject>section{--marpit-root-font-size:28px}div#p>svg>foreignObject>section.title h1{color:#808db5;text-align:center}div#p>svg>foreignObject>section.title p{bottom:25%;width:100%;position:absolute;font-size:25px;color:#4b4b4b;background:linear-gradient(transparent 90%,#ffcc00 0%)}div#p>svg>foreignObject>section.slide h1{width:95%;color:white;background-color:#808db5;position:absolute;left:50px;top:35px}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]{columns:initial!important;display:block!important;padding:0!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]:after,div#p>svg>foreignObject>section[data-marpit-advanced-background=background]:before,div#p>svg>foreignObject>section[data-marpit-advanced-background=content]:after,div#p>svg>foreignObject>section[data-marpit-advanced-background=content]:before{display:none!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container]{all:initial;display:flex;flex-direction:row;height:100%;overflow:hidden;width:100%}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container][data-marpit-advanced-background-direction=vertical]{flex-direction:column}div#p>svg>foreignObject>section[data-marpit-advanced-background=background][data-marpit-advanced-background-split]>div[data-marpit-advanced-background-container]{width:var(--marpit-advanced-background-split,50%)}div#p>svg>foreignObject>section[data-marpit-advanced-background=background][data-marpit-advanced-background-split=right]>div[data-marpit-advanced-background-container]{margin-left:calc(100% - var(--marpit-advanced-background-split, 50%))}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container]>figure{all:initial;background-position:center;background-repeat:no-repeat;background-size:cover;flex:auto;margin:0}div#p>svg>foreignObject>section[data-marpit-advanced-background=content],div#p>svg>foreignObject>section[data-marpit-advanced-background=pseudo]{background:transparent!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=pseudo],div#p>svg[data-marpit-svg]>foreignObject[data-marpit-advanced-background=pseudo]{pointer-events:none!important}div#p>svg>foreignObject>section[data-marpit-advanced-background-split]{width:100%;height:100%}</style></head><body><div class="bespoke-marp-osc"><button data-bespoke-marp-osc="prev" tabindex="-1" title="Previous slide">Previous slide</button><span data-bespoke-marp-osc="page"></span><button data-bespoke-marp-osc="next" tabindex="-1" title="Next slide">Next slide</button><button data-bespoke-marp-osc="fullscreen" tabindex="-1" title="Toggle fullscreen (f)">Toggle fullscreen</button><button data-bespoke-marp-osc="presenter" tabindex="-1" title="Open presenter view (p)">Open presenter view</button></div><div id="p"><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="1" data-paginate="true" data-class="title" data-theme="default" data-style="section { 12 /* content:""; */display:table}div#p>svg>foreignObject>section:after{clear:both}div#p>svg>foreignObject>section>:first-child{margin-top:0!important}div#p>svg>foreignObject>section>:last-child{margin-bottom:0!important}div#p>svg>foreignObject>section a:not([href]){color:inherit;text-decoration:none}div#p>svg>foreignObject>section .absent{color:#cf222e}div#p>svg>foreignObject>section .anchor{float:left;line-height:1;margin-left:-20px;padding-right:4px}div#p>svg>foreignObject>section .anchor:focus{outline:none}div#p>svg>foreignObject>section blockquote,div#p>svg>foreignObject>section details,div#p>svg>foreignObject>section dl,div#p>svg>foreignObject>section ol,div#p>svg>foreignObject>section p,div#p>svg>foreignObject>section pre,div#p>svg>foreignObject>section table,div#p>svg>foreignObject>section ul{margin-bottom:16px;margin-top:0}div#p>svg>foreignObject>section blockquote>:first-child{margin-top:0}div#p>svg>foreignObject>section blockquote>:last-child{margin-bottom:0}div#p>svg>foreignObject>section sup>a:before{content:"["}div#p>svg>foreignObject>section sup>a:after{content:"]"}div#p>svg>foreignObject>section h1 .octicon-link,div#p>svg>foreignObject>section h2 .octicon-link,div#p>svg>foreignObject>section h3 .octicon-link,div#p>svg>foreignObject>section h4 .octicon-link,div#p>svg>foreignObject>section h5 .octicon-link,div#p>svg>foreignObject>section h6 .octicon-link{color:#24292f;vertical-align:middle;visibility:hidden}div#p>svg>foreignObject>section h1:hover .anchor,div#p>svg>foreignObject>section h2:hover .anchor,div#p>svg>foreignObject>section h3:hover .anchor,div#p>svg>foreignObject>section h4:hover .anchor,div#p>svg>foreignObject>section h5:hover .anchor,div#p>svg>foreignObject>section h6:hover .anchor{text-decoration:none}div#p>svg>foreignObject>section h1:hover .anchor .octicon-link,div#p>svg>foreignObject>section h2:hover .anchor .octicon-link,div#p>svg>foreignObject>section h3:hover .anchor .octicon-link,div#p>svg>foreignObject>section h4:hover .anchor .octicon-link,div#p>svg>foreignObject>section h5:hover .anchor .octicon-link,div#p>svg>foreignObject>section h6:hover .anchor .octicon-link{visibility:visible}div#p>svg>foreignObject>section h1 code,div#p>svg>foreignObject>section h1 tt,div#p>svg>foreignObject>section h2 code,div#p>svg>foreignObject>section h2 tt,div#p>svg>foreignObject>section h3 code,div#p>svg>foreignObject>section h3 tt,div#p>svg>foreignObject>section h4 code,div#p>svg>foreignObject>section h4 tt,div#p>svg>foreignObject>section h5 code,div#p>svg>foreignObject>section h5 tt,div#p>svg>foreignObject>section h6 code,div#p>svg>foreignObject>section h6 tt{font-size:inherit;padding:0 .2em}div#p>svg>foreignObject>section ol.no-list,div#p>svg>foreignObject>section ul.no-list{list-style-type:none;padding:0}div#p>svg>foreignObject>section ol[type="1"]{list-style-type:decimal}div#p>svg>foreignObject>section ol[type=a]{list-style-type:lower-alpha}div#p>svg>foreignObject>section ol[type=i]{list-style-type:lower-roman}div#p>svg>foreignObject>section div>ol:not([type]){list-style-type:decimal}div#p>svg>foreignObject>section ol ol,div#p>svg>foreignObject>section ol ul,div#p>svg>foreignObject>section ul ol,div#p>svg>foreignObject>section ul ul{margin-bottom:0;margin-top:0}div#p>svg>foreignObject>section li>p{margin-top:16px}div#p>svg>foreignObject>section li+li{margin-top:.25em}div#p>svg>foreignObject>section dl{padding:0}div#p>svg>foreignObject>section dl dt{font-size:1em;font-style:italic;font-weight:600;margin-top:16px;padding:0}div#p>svg>foreignObject>section dl dd{margin-bottom:16px;padding:0 16px}div#p>svg>foreignObject>section table th{font-weight:600}div#p>svg>foreignObject>section table td,div#p>svg>foreignObject>section table th{border:1px solid #d0d7de;padding:6px 13px}div#p>svg>foreignObject>section table tr{background-color:#fff;border-top:1px solid #d8dee4}div#p>svg>foreignObject>section table tr:nth-child(2n){background-color:#f6f8fa}div#p>svg>foreignObject>section table img{background-color:transparent}div#p>svg>foreignObject>section img[align=right]{padding-left:20px}div#p>svg>foreignObject>section img[align=left]{padding-right:20px}div#p>svg>foreignObject>section .emoji{background-color:transparent;max-width:none;vertical-align:text-top}div#p>svg>foreignObject>section span.frame,div#p>svg>foreignObject>section span.frame>span{display:block;overflow:hidden}div#p>svg>foreignObject>section span.frame>span{border:1px solid #d0d7de;float:left;margin:13px 0 0;padding:7px;width:auto}div#p>svg>foreignObject>section span.frame span img{display:block;float:left}div#p>svg>foreignObject>section span.frame span span{clear:both;color:#24292f;display:block;padding:5px 0 0}div#p>svg>foreignObject>section span.align-center{clear:both;display:block;overflow:hidden}div#p>svg>foreignObject>section span.align-center>span{display:block;margin:13px auto 0;overflow:hidden;text-align:center}div#p>svg>foreignObject>section span.align-center span img{margin:0 auto;text-align:center}div#p>svg>foreignObject>section span.align-right{clear:both;display:block;overflow:hidden}div#p>svg>foreignObject>section span.align-right>span{display:block;margin:13px 0 0;overflow:hidden;text-align:right}div#p>svg>foreignObject>section span.align-right span img{margin:0;text-align:right}div#p>svg>foreignObject>section span.float-left{display:block;float:left;margin-right:13px;overflow:hidden}div#p>svg>foreignObject>section span.float-left span{margin:13px 0 0}div#p>svg>foreignObject>section span.float-right{display:block;float:right;margin-left:13px;overflow:hidden}div#p>svg>foreignObject>section span.float-right>span{display:block;margin:13px auto 0;overflow:hidden;text-align:right}div#p>svg>foreignObject>section code,div#p>svg>foreignObject>section tt{background-color:rgba(175,184,193,.2);border-radius:6px;font-size:85%;margin:0;padding:.2em .4em}div#p>svg>foreignObject>section code br,div#p>svg>foreignObject>section tt br{display:none}div#p>svg>foreignObject>section del code{text-decoration:inherit}div#p>svg>foreignObject>section pre code{font-size:100%}div#p>svg>foreignObject>section pre>code{background:transparent;border:0;margin:0;padding:0;white-space:pre;word-break:normal}div#p>svg>foreignObject>section .highlight{margin-bottom:16px}div#p>svg>foreignObject>section .highlight pre{margin-bottom:0;word-break:normal}div#p>svg>foreignObject>section pre{background-color:#f6f8fa;border-radius:6px;font-size:85%;line-height:1.45;overflow:auto;padding:16px}div#p>svg>foreignObject>section pre code,div#p>svg>foreignObject>section pre tt{word-wrap:normal;background-color:transparent;border:0;display:inline;line-height:inherit;margin:0;max-width:auto;overflow:visible;padding:0}div#p>svg>foreignObject>section .csv-data td,div#p>svg>foreignObject>section .csv-data th{font-size:12px;line-height:1;overflow:hidden;padding:5px;text-align:left;white-space:nowrap}div#p>svg>foreignObject>section .csv-data .blob-num{background:#fff;border:0;padding:10px 8px 9px;text-align:right}div#p>svg>foreignObject>section .csv-data tr{border-top:0}div#p>svg>foreignObject>section .csv-data th{background:#f6f8fa;border-top:0;font-weight:600}div#p>svg>foreignObject>section .footnotes{border-top:1px solid #d0d7de;color:#57606a;font-size:12px}div#p>svg>foreignObject>section div#p>svg>foreignObject>section section.footnotes{--marpit-root-font-size:12px}div#p>svg>foreignObject>section .footnotes ol{padding-left:16px}div#p>svg>foreignObject>section .footnotes li{position:relative}div#p>svg>foreignObject>section .footnotes li:target:before{border:2px solid #0969da;border-radius:6px;bottom:-8px;content:"";left:-24px;pointer-events:none;position:absolute;right:-8px;top:-8px}div#p>svg>foreignObject>section .footnotes li:target{color:#24292f}div#p>svg>foreignObject>section .footnotes .data-footnote-backref g-emoji{font-family:monospace}div#p>svg>foreignObject>section [hidden]{display:none!important}div#p>svg>foreignObject>section ::-webkit-calendar-picker-indicator{filter:invert(50%)}div#p>svg>foreignObject>section .hljs{background:#fff;color:#333;display:block;overflow-x:auto;padding:.5em}div#p>svg>foreignObject>section .hljs-comment,div#p>svg>foreignObject>section .hljs-meta{color:#969896}div#p>svg>foreignObject>section .hljs-emphasis,div#p>svg>foreignObject>section .hljs-quote,div#p>svg>foreignObject>section .hljs-strong,div#p>svg>foreignObject>section .hljs-template-variable,div#p>svg>foreignObject>section .hljs-variable{color:#df5000}div#p>svg>foreignObject>section .hljs-keyword,div#p>svg>foreignObject>section .hljs-selector-tag,div#p>svg>foreignObject>section .hljs-type{color:#d73a49}div#p>svg>foreignObject>section .hljs-attribute,div#p>svg>foreignObject>section .hljs-bullet,div#p>svg>foreignObject>section .hljs-literal,div#p>svg>foreignObject>section .hljs-symbol{color:#0086b3}div#p>svg>foreignObject>section .hljs-name,div#p>svg>foreignObject>section .hljs-section{color:#63a35c}div#p>svg>foreignObject>section .hljs-tag{color:#333}div#p>svg>foreignObject>section .hljs-attr,div#p>svg>foreignObject>section .hljs-selector-attr,div#p>svg>foreignObject>section .hljs-selector-class,div#p>svg>foreignObject>section .hljs-selector-id,div#p>svg>foreignObject>section .hljs-selector-pseudo,div#p>svg>foreignObject>section .hljs-title{color:#6f42c1}div#p>svg>foreignObject>section .hljs-addition{background-color:#eaffea;color:#55a532}div#p>svg>foreignObject>section .hljs-deletion{background-color:#ffecec;color:#bd2c00}div#p>svg>foreignObject>section .hljs-link{text-decoration:underline}div#p>svg>foreignObject>section .hljs-number{color:#005cc5}div#p>svg>foreignObject>section .hljs-string{color:#032f62}div#p>svg>foreignObject>section svg[data-marp-fitting=svg]{max-height:563px}div#p>svg>foreignObject>section h1{color:#246;font-size:1.6em}div#p>svg>foreignObject>section h1,div#p>svg>foreignObject>section h2{border-bottom:none}div#p>svg>foreignObject>section h2{font-size:1.3em}div#p>svg>foreignObject>section h3{font-size:1.1em}div#p>svg>foreignObject>section h4{font-size:1.05em}div#p>svg>foreignObject>section h5{font-size:1em}div#p>svg>foreignObject>section h6{font-size:.9em}div#p>svg>foreignObject>section h1 strong,div#p>svg>foreignObject>section h2 strong,div#p>svg>foreignObject>section h3 strong,div#p>svg>foreignObject>section h4 strong,div#p>svg>foreignObject>section h5 strong,div#p>svg>foreignObject>section h6 strong{color:#48c;font-weight:inherit}div#p>svg>foreignObject>section hr{height:0;padding-top:.25em}div#p>svg>foreignObject>section pre{border:1px solid #999;line-height:1.15;overflow:visible}div#p>svg>foreignObject>section pre code svg[data-marp-fitting=svg]{max-height:529px}div#p>svg>foreignObject>section footer,div#p>svg>foreignObject>section header{color:hsla(0,0%,40%,.75);font-size:18px;left:30px;margin:0;position:absolute}div#p>svg>foreignObject>section header{top:21px}div#p>svg>foreignObject>section footer{bottom:21px}div#p>svg>foreignObject>section{align-items:stretch;background:#fff;display:flex;flex-flow:column nowrap;font-size:29px;height:720px;justify-content:center;padding:78.5px;width:1280px}div#p>svg>foreignObject>section{--marpit-root-font-size:29px}div#p>svg>foreignObject>section>:last-child,div#p>svg>foreignObject>section[data-footer]>:nth-last-child(2){margin-bottom:0}div#p>svg>foreignObject>section>:first-child,div#p>svg>foreignObject>section>header:first-child+*{margin-top:0}div#p>svg>foreignObject>section:after{bottom:21px;color:#777;font-size:24px;padding:0;position:absolute;right:30px}div#p>svg>foreignObject>section:after{--marpit-root-font-size:24px}div#p>svg>foreignObject>section.invert{background-color:#222;color:#e6eaf0}div#p>svg>foreignObject>section.invert:after{color:#999}div#p>svg>foreignObject>section.invert img{background-color:transparent}div#p>svg>foreignObject>section.invert a{color:#50b3ff}div#p>svg>foreignObject>section.invert h1{color:#a3c5e7}div#p>svg>foreignObject>section.invert h2,div#p>svg>foreignObject>section.invert h3,div#p>svg>foreignObject>section.invert h4,div#p>svg>foreignObject>section.invert h5{color:#ebeff5}div#p>svg>foreignObject>section.invert blockquote,div#p>svg>foreignObject>section.invert h6{border-color:#3d3f43;color:#939699}div#p>svg>foreignObject>section.invert h1 strong,div#p>svg>foreignObject>section.invert h2 strong,div#p>svg>foreignObject>section.invert h3 strong,div#p>svg>foreignObject>section.invert h4 strong,div#p>svg>foreignObject>section.invert h5 strong,div#p>svg>foreignObject>section.invert h6 strong{color:#7bf}div#p>svg>foreignObject>section.invert hr{background-color:#3d3f43}div#p>svg>foreignObject>section.invert footer,div#p>svg>foreignObject>section.invert header{color:hsla(0,0%,60%,.75)}div#p>svg>foreignObject>section.invert code,div#p>svg>foreignObject>section.invert kbd{background-color:#111}div#p>svg>foreignObject>section.invert kbd{border-color:#666;box-shadow:inset 0 -1px 0 #555;color:#e6eaf0}div#p>svg>foreignObject>section.invert table tr{background-color:#12181d;border-color:#60657b}div#p>svg>foreignObject>section.invert table tr:nth-child(2n){background-color:#1b2024}div#p>svg>foreignObject>section.invert table td,div#p>svg>foreignObject>section.invert table th{border-color:#5b5e61}div#p>svg>foreignObject>section.invert pre{background-color:#0a0e12;border-color:#777}div#p>svg>foreignObject>section.invert pre code{background-color:transparent}div#p>svg>foreignObject>section[data-color] h1,div#p>svg>foreignObject>section[data-color] h2,div#p>svg>foreignObject>section[data-color] h3,div#p>svg>foreignObject>section[data-color] h4,div#p>svg>foreignObject>section[data-color] h5,div#p>svg>foreignObject>section[data-color] h6{color:currentColor}div#p>svg>foreignObject>section{width:1280px;height:720px}div#p>svg>foreignObject>section{background-color:#FFFFFF;font-size:28px;color:#4b4b4b;font-family:"Droid Sans Mono","Hiragino Maru Gothic ProN";background-image:url("logo.svg");background-position:right 3% bottom 2%;background-repeat:no-repeat;background-attachment:5%;background-size:20% auto}div#p>svg>foreignObject>section{--marpit-root-font-size:28px}div#p>svg>foreignObject>section.title h1{color:#808db5;text-align:center}div#p>svg>foreignObject>section.title p{bottom:25%;width:100%;position:absolute;font-size:25px;color:#4b4b4b;background:linear-gradient(transparent 90%,#ffcc00 0%)}div#p>svg>foreignObject>section.slide h1{width:95%;color:white;background-color:#808db5;position:absolute;left:50px;top:35px}div#p>svg>foreignObject>section.fig_cg p{top:300px;text-align:center}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]{columns:initial!important;display:block!important;padding:0!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]:after,div#p>svg>foreignObject>section[data-marpit-advanced-background=background]:before,div#p>svg>foreignObject>section[data-marpit-advanced-background=content]:after,div#p>svg>foreignObject>section[data-marpit-advanced-background=content]:before{display:none!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container]{all:initial;display:flex;flex-direction:row;height:100%;overflow:hidden;width:100%}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container][data-marpit-advanced-background-direction=vertical]{flex-direction:column}div#p>svg>foreignObject>section[data-marpit-advanced-background=background][data-marpit-advanced-background-split]>div[data-marpit-advanced-background-container]{width:var(--marpit-advanced-background-split,50%)}div#p>svg>foreignObject>section[data-marpit-advanced-background=background][data-marpit-advanced-background-split=right]>div[data-marpit-advanced-background-container]{margin-left:calc(100% - var(--marpit-advanced-background-split, 50%))}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container]>figure{all:initial;background-position:center;background-repeat:no-repeat;background-size:cover;flex:auto;margin:0}div#p>svg>foreignObject>section[data-marpit-advanced-background=content],div#p>svg>foreignObject>section[data-marpit-advanced-background=pseudo]{background:transparent!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=pseudo],div#p>svg[data-marpit-svg]>foreignObject[data-marpit-advanced-background=pseudo]{pointer-events:none!important}div#p>svg>foreignObject>section[data-marpit-advanced-background-split]{width:100%;height:100%}</style></head><body><div class="bespoke-marp-osc"><button data-bespoke-marp-osc="prev" tabindex="-1" title="Previous slide">Previous slide</button><span data-bespoke-marp-osc="page"></span><button data-bespoke-marp-osc="next" tabindex="-1" title="Next slide">Next slide</button><button data-bespoke-marp-osc="fullscreen" tabindex="-1" title="Toggle fullscreen (f)">Toggle fullscreen</button><button data-bespoke-marp-osc="presenter" tabindex="-1" title="Open presenter view (p)">Open presenter view</button></div><div id="p"><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="1" data-paginate="true" data-class="title" data-theme="default" data-style="section {
13 background-color: #FFFFFF; 13 background-color: #FFFFFF;
14 font-size: 28px; 14 font-size: 28px;
15 color: #4b4b4b; 15 color: #4b4b4b;
16 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 16 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
17 background-image: url(&quot;logo.svg&quot;); 17 background-image: url(&quot;logo.svg&quot;);
18 background-position: right 3% bottom 2%; 18 background-position: right 3% bottom 2%;
19 background-repeat: no-repeat; 19 background-repeat: no-repeat;
20 background-attachment: 5%; 20 background-attachment: 5%;
21 background-size: 20% auto; 21 background-size: 20% auto;
22 } 22 }
23 23
24 section.title h1 { 24 section.title h1 {
25 color: #808db5; 25 color: #808db5;
26 text-align: center; 26 text-align: center;
27 } 27 }
28 28
29 section.title p { 29 section.title p {
30 bottom: 25%; 30 bottom: 25%;
31 width: 100%; 31 width: 100%;
32 position: absolute; 32 position: absolute;
33 font-size: 25px; 33 font-size: 25px;
34 color: #4b4b4b; 34 color: #4b4b4b;
35 background: linear-gradient(transparent 90%, #ffcc00 0%); 35 background: linear-gradient(transparent 90%, #ffcc00 0%);
36 } 36 }
37 37
38 section.slide h1 { 38 section.slide h1 {
39 width: 95%; 39 width: 95%;
40 color: white; 40 color: white;
41 background-color: #808db5; 41 background-color: #808db5;
42 position: absolute; 42 position: absolute;
43 left: 50px; 43 left: 50px;
44 top: 35px; 44 top: 35px;
45 } 45 }
46 " data-heading-divider="1" class="title" data-marpit-pagination="1" data-marpit-pagination-total="26" style="--paginate:true;--class:title;--theme:default;--style:section { 46
47 background-color: #FFFFFF; 47 section.fig_cg p {
48 font-size: 28px; 48 top: 300px;
49 color: #4b4b4b; 49 text-align: center;
50 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 50 }
51 background-image: url(&quot;logo.svg&quot;); 51 " data-heading-divider="1" class="title" data-marpit-pagination="1" data-marpit-pagination-total="24" style="--paginate:true;--class:title;--theme:default;--style:section {
52 background-position: right 3% bottom 2%; 52 background-color: #FFFFFF;
53 background-repeat: no-repeat; 53 font-size: 28px;
54 background-attachment: 5%; 54 color: #4b4b4b;
55 background-size: 20% auto; 55 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
56 } 56 background-image: url(&quot;logo.svg&quot;);
57 57 background-position: right 3% bottom 2%;
58 section.title h1 { 58 background-repeat: no-repeat;
59 color: #808db5; 59 background-attachment: 5%;
60 text-align: center; 60 background-size: 20% auto;
61 } 61 }
62 62
63 section.title p { 63 section.title h1 {
64 bottom: 25%; 64 color: #808db5;
65 width: 100%; 65 text-align: center;
66 position: absolute; 66 }
67 font-size: 25px; 67
68 color: #4b4b4b; 68 section.title p {
69 background: linear-gradient(transparent 90%, #ffcc00 0%); 69 bottom: 25%;
70 } 70 width: 100%;
71 71 position: absolute;
72 section.slide h1 { 72 font-size: 25px;
73 width: 95%; 73 color: #4b4b4b;
74 color: white; 74 background: linear-gradient(transparent 90%, #ffcc00 0%);
75 background-color: #808db5; 75 }
76 position: absolute; 76
77 left: 50px; 77 section.slide h1 {
78 top: 35px; 78 width: 95%;
79 color: white;
80 background-color: #808db5;
81 position: absolute;
82 left: 50px;
83 top: 35px;
84 }
85
86 section.fig_cg p {
87 top: 300px;
88 text-align: center;
79 } 89 }
80 ;--heading-divider:1;" data-size="16:9"> 90 ;--heading-divider:1;" data-size="16:9">
81 <h1>Gears Agda による <br /> Left Learning Red Black Tree の検証</h1> 91 <h1>Gears Agda による <br /> Left Learning Red Black Tree の検証</h1>
82 92
83 <p>Uechi Yuto, Shinji Kono 琉球大学</p> 93 <p>Uechi Yuto, Shinji Kono 琉球大学</p>
114 background-color: #808db5; 124 background-color: #808db5;
115 position: absolute; 125 position: absolute;
116 left: 50px; 126 left: 50px;
117 top: 35px; 127 top: 35px;
118 } 128 }
119 " data-heading-divider="1" class="slide" data-marpit-pagination="2" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { 129
120 background-color: #FFFFFF; 130 section.fig_cg p {
121 font-size: 28px; 131 top: 300px;
122 color: #4b4b4b; 132 text-align: center;
123 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 133 }
124 background-image: url(&quot;logo.svg&quot;); 134 " data-heading-divider="1" class="slide" data-marpit-pagination="2" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section {
125 background-position: right 3% bottom 2%; 135 background-color: #FFFFFF;
126 background-repeat: no-repeat; 136 font-size: 28px;
127 background-attachment: 5%; 137 color: #4b4b4b;
128 background-size: 20% auto; 138 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
129 } 139 background-image: url(&quot;logo.svg&quot;);
130 140 background-position: right 3% bottom 2%;
131 section.title h1 { 141 background-repeat: no-repeat;
132 color: #808db5; 142 background-attachment: 5%;
133 text-align: center; 143 background-size: 20% auto;
134 } 144 }
135 145
136 section.title p { 146 section.title h1 {
137 bottom: 25%; 147 color: #808db5;
138 width: 100%; 148 text-align: center;
139 position: absolute; 149 }
140 font-size: 25px; 150
141 color: #4b4b4b; 151 section.title p {
142 background: linear-gradient(transparent 90%, #ffcc00 0%); 152 bottom: 25%;
143 } 153 width: 100%;
144 154 position: absolute;
145 section.slide h1 { 155 font-size: 25px;
146 width: 95%; 156 color: #4b4b4b;
147 color: white; 157 background: linear-gradient(transparent 90%, #ffcc00 0%);
148 background-color: #808db5; 158 }
149 position: absolute; 159
150 left: 50px; 160 section.slide h1 {
151 top: 35px; 161 width: 95%;
162 color: white;
163 background-color: #808db5;
164 position: absolute;
165 left: 50px;
166 top: 35px;
167 }
168
169 section.fig_cg p {
170 top: 300px;
171 text-align: center;
152 } 172 }
153 ;--heading-divider:1;" data-size="16:9"> 173 ;--heading-divider:1;" data-size="16:9">
154 <h1>証明を用いてプログラムの信頼性の向上を目指す</h1> 174 <h1>証明を用いてプログラムの信頼性の向上を目指す</h1>
155 175
156 <ul> 176 <ul>
200 background-color: #808db5; 220 background-color: #808db5;
201 position: absolute; 221 position: absolute;
202 left: 50px; 222 left: 50px;
203 top: 35px; 223 top: 35px;
204 } 224 }
205 " data-heading-divider="1" class="slide" data-marpit-pagination="3" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { 225
206 background-color: #FFFFFF; 226 section.fig_cg p {
207 font-size: 28px; 227 top: 300px;
208 color: #4b4b4b; 228 text-align: center;
209 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 229 }
210 background-image: url(&quot;logo.svg&quot;); 230 " data-heading-divider="1" class="slide" data-marpit-pagination="3" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section {
211 background-position: right 3% bottom 2%; 231 background-color: #FFFFFF;
212 background-repeat: no-repeat; 232 font-size: 28px;
213 background-attachment: 5%; 233 color: #4b4b4b;
214 background-size: 20% auto; 234 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
215 } 235 background-image: url(&quot;logo.svg&quot;);
216 236 background-position: right 3% bottom 2%;
217 section.title h1 { 237 background-repeat: no-repeat;
218 color: #808db5; 238 background-attachment: 5%;
219 text-align: center; 239 background-size: 20% auto;
220 } 240 }
221 241
222 section.title p { 242 section.title h1 {
223 bottom: 25%; 243 color: #808db5;
224 width: 100%; 244 text-align: center;
225 position: absolute; 245 }
226 font-size: 25px; 246
227 color: #4b4b4b; 247 section.title p {
228 background: linear-gradient(transparent 90%, #ffcc00 0%); 248 bottom: 25%;
229 } 249 width: 100%;
230 250 position: absolute;
231 section.slide h1 { 251 font-size: 25px;
232 width: 95%; 252 color: #4b4b4b;
233 color: white; 253 background: linear-gradient(transparent 90%, #ffcc00 0%);
234 background-color: #808db5; 254 }
235 position: absolute; 255
236 left: 50px; 256 section.slide h1 {
237 top: 35px; 257 width: 95%;
258 color: white;
259 background-color: #808db5;
260 position: absolute;
261 left: 50px;
262 top: 35px;
263 }
264
265 section.fig_cg p {
266 top: 300px;
267 text-align: center;
238 } 268 }
239 ;--heading-divider:1;" data-size="16:9"> 269 ;--heading-divider:1;" data-size="16:9">
240 <h1>CbC について</h1> 270 <h1>CbC について</h1>
241 <ul> 271 <ul>
242 <li>CbCとは当研究室で開発しているC言語の下位言語 272 <li>CbCとは当研究室で開発しているC言語の下位言語
281 background-color: #808db5; 311 background-color: #808db5;
282 position: absolute; 312 position: absolute;
283 left: 50px; 313 left: 50px;
284 top: 35px; 314 top: 35px;
285 } 315 }
286 " data-heading-divider="1" class="slide" data-marpit-pagination="4" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { 316
287 background-color: #FFFFFF; 317 section.fig_cg p {
288 font-size: 28px; 318 top: 300px;
289 color: #4b4b4b; 319 text-align: center;
290 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 320 }
291 background-image: url(&quot;logo.svg&quot;); 321 " data-heading-divider="1" class="slide" data-marpit-pagination="4" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section {
292 background-position: right 3% bottom 2%; 322 background-color: #FFFFFF;
293 background-repeat: no-repeat; 323 font-size: 28px;
294 background-attachment: 5%; 324 color: #4b4b4b;
295 background-size: 20% auto; 325 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
296 } 326 background-image: url(&quot;logo.svg&quot;);
297 327 background-position: right 3% bottom 2%;
298 section.title h1 { 328 background-repeat: no-repeat;
299 color: #808db5; 329 background-attachment: 5%;
300 text-align: center; 330 background-size: 20% auto;
301 } 331 }
302 332
303 section.title p { 333 section.title h1 {
304 bottom: 25%; 334 color: #808db5;
305 width: 100%; 335 text-align: center;
306 position: absolute; 336 }
307 font-size: 25px; 337
308 color: #4b4b4b; 338 section.title p {
309 background: linear-gradient(transparent 90%, #ffcc00 0%); 339 bottom: 25%;
310 } 340 width: 100%;
311 341 position: absolute;
312 section.slide h1 { 342 font-size: 25px;
313 width: 95%; 343 color: #4b4b4b;
314 color: white; 344 background: linear-gradient(transparent 90%, #ffcc00 0%);
315 background-color: #808db5; 345 }
316 position: absolute; 346
317 left: 50px; 347 section.slide h1 {
318 top: 35px; 348 width: 95%;
349 color: white;
350 background-color: #808db5;
351 position: absolute;
352 left: 50px;
353 top: 35px;
354 }
355
356 section.fig_cg p {
357 top: 300px;
358 text-align: center;
319 } 359 }
320 ;--heading-divider:1;" data-size="16:9"> 360 ;--heading-divider:1;" data-size="16:9">
321 <h1>Agda の基本</h1> 361 <h1>Agda の基本</h1>
322 <ul> 362 <ul>
323 <li>Agdaとは定理証明支援器であり、関数型言語である</li> 363 <li>Agdaとは定理証明支援器であり、関数型言語である</li>
376 background-color: #808db5; 416 background-color: #808db5;
377 position: absolute; 417 position: absolute;
378 left: 50px; 418 left: 50px;
379 top: 35px; 419 top: 35px;
380 } 420 }
381 " data-heading-divider="1" class="slide" data-marpit-pagination="5" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { 421
382 background-color: #FFFFFF; 422 section.fig_cg p {
383 font-size: 28px; 423 top: 300px;
384 color: #4b4b4b; 424 text-align: center;
385 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 425 }
386 background-image: url(&quot;logo.svg&quot;); 426 " data-heading-divider="1" class="slide" data-marpit-pagination="5" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section {
387 background-position: right 3% bottom 2%; 427 background-color: #FFFFFF;
388 background-repeat: no-repeat; 428 font-size: 28px;
389 background-attachment: 5%; 429 color: #4b4b4b;
390 background-size: 20% auto; 430 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
391 } 431 background-image: url(&quot;logo.svg&quot;);
392 432 background-position: right 3% bottom 2%;
393 section.title h1 { 433 background-repeat: no-repeat;
394 color: #808db5; 434 background-attachment: 5%;
395 text-align: center; 435 background-size: 20% auto;
396 } 436 }
397 437
398 section.title p { 438 section.title h1 {
399 bottom: 25%; 439 color: #808db5;
400 width: 100%; 440 text-align: center;
401 position: absolute; 441 }
402 font-size: 25px; 442
403 color: #4b4b4b; 443 section.title p {
404 background: linear-gradient(transparent 90%, #ffcc00 0%); 444 bottom: 25%;
405 } 445 width: 100%;
406 446 position: absolute;
407 section.slide h1 { 447 font-size: 25px;
408 width: 95%; 448 color: #4b4b4b;
409 color: white; 449 background: linear-gradient(transparent 90%, #ffcc00 0%);
410 background-color: #808db5; 450 }
411 position: absolute; 451
412 left: 50px; 452 section.slide h1 {
413 top: 35px; 453 width: 95%;
454 color: white;
455 background-color: #808db5;
456 position: absolute;
457 left: 50px;
458 top: 35px;
459 }
460
461 section.fig_cg p {
462 top: 300px;
463 text-align: center;
414 } 464 }
415 ;--heading-divider:1;" data-size="16:9"> 465 ;--heading-divider:1;" data-size="16:9">
416 <h1>Agda の基本 record</h1> 466 <h1>Agda の基本 record</h1>
417 <ul> 467 <ul>
418 <li>2つのものが同時に存在すること</li> 468 <li>2つのものが同時に存在すること</li>
419 <li>Record 型とはオブジェクトあるいは構造体のようなもの</li> 469 <li>Record 型とはオブジェクトあるいは構造体</li>
420 </ul> 470 </ul>
421 <pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>record Env : Set where 471 <pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>record Env : Set where
422 field 472 field
423 varn : N 473 varn : N
424 vari : N 474 vari : N
425 open Env 475 open Env
426 </span></span></foreignObject></svg></code></pre> 476 </span></span></foreignObject></svg></code></pre>
427 <p>記述する際の基本的な例を以下に挙げる</p> 477 <p>型に対応する値の導入(intro)</p>
428 <pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>record {varx = zero ; vary = suc zero} 478 <pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>record {varx = zero ; vary = suc zero}
429 </span></span></foreignObject></svg></code></pre> 479 </span></span></foreignObject></svg></code></pre>
480 <p>record の値のアクセス(elim)</p>
481 <pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>(env : Env) → varx env
482 </span></span></foreignObject></svg></code></pre>
430 </section> 483 </section>
431 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="6" data-paginate="true" data-class="slide" data-theme="default" data-style="section { 484 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="6" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
432 background-color: #FFFFFF; 485 background-color: #FFFFFF;
433 font-size: 28px; 486 font-size: 28px;
434 color: #4b4b4b; 487 color: #4b4b4b;
460 background-color: #808db5; 513 background-color: #808db5;
461 position: absolute; 514 position: absolute;
462 left: 50px; 515 left: 50px;
463 top: 35px; 516 top: 35px;
464 } 517 }
465 " data-heading-divider="1" class="slide" data-marpit-pagination="6" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { 518
466 background-color: #FFFFFF; 519 section.fig_cg p {
467 font-size: 28px; 520 top: 300px;
468 color: #4b4b4b; 521 text-align: center;
469 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 522 }
470 background-image: url(&quot;logo.svg&quot;); 523 " data-heading-divider="1" class="slide" data-marpit-pagination="6" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section {
471 background-position: right 3% bottom 2%; 524 background-color: #FFFFFF;
472 background-repeat: no-repeat; 525 font-size: 28px;
473 background-attachment: 5%; 526 color: #4b4b4b;
474 background-size: 20% auto; 527 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
475 } 528 background-image: url(&quot;logo.svg&quot;);
476 529 background-position: right 3% bottom 2%;
477 section.title h1 { 530 background-repeat: no-repeat;
478 color: #808db5; 531 background-attachment: 5%;
479 text-align: center; 532 background-size: 20% auto;
480 } 533 }
481 534
482 section.title p { 535 section.title h1 {
483 bottom: 25%; 536 color: #808db5;
484 width: 100%; 537 text-align: center;
485 position: absolute; 538 }
486 font-size: 25px; 539
487 color: #4b4b4b; 540 section.title p {
488 background: linear-gradient(transparent 90%, #ffcc00 0%); 541 bottom: 25%;
489 } 542 width: 100%;
490 543 position: absolute;
491 section.slide h1 { 544 font-size: 25px;
492 width: 95%; 545 color: #4b4b4b;
493 color: white; 546 background: linear-gradient(transparent 90%, #ffcc00 0%);
494 background-color: #808db5; 547 }
495 position: absolute; 548
496 left: 50px; 549 section.slide h1 {
497 top: 35px; 550 width: 95%;
551 color: white;
552 background-color: #808db5;
553 position: absolute;
554 left: 50px;
555 top: 35px;
556 }
557
558 section.fig_cg p {
559 top: 300px;
560 text-align: center;
498 } 561 }
499 ;--heading-divider:1;" data-size="16:9"> 562 ;--heading-divider:1;" data-size="16:9">
500 <h1>Agda の基本 data</h1> 563 <h1>Agda の基本 data</h1>
501 <ul> 564 <ul>
502 <li>一つでも存在すること</li> 565 <li>一つでも存在すること</li>
544 background-color: #808db5; 607 background-color: #808db5;
545 position: absolute; 608 position: absolute;
546 left: 50px; 609 left: 50px;
547 top: 35px; 610 top: 35px;
548 } 611 }
549 " data-heading-divider="1" class="slide" data-marpit-pagination="7" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { 612
550 background-color: #FFFFFF; 613 section.fig_cg p {
551 font-size: 28px; 614 top: 300px;
552 color: #4b4b4b; 615 text-align: center;
553 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 616 }
554 background-image: url(&quot;logo.svg&quot;); 617 " data-heading-divider="1" class="slide" data-marpit-pagination="7" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section {
555 background-position: right 3% bottom 2%; 618 background-color: #FFFFFF;
556 background-repeat: no-repeat; 619 font-size: 28px;
557 background-attachment: 5%; 620 color: #4b4b4b;
558 background-size: 20% auto; 621 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
559 } 622 background-image: url(&quot;logo.svg&quot;);
560 623 background-position: right 3% bottom 2%;
561 section.title h1 { 624 background-repeat: no-repeat;
562 color: #808db5; 625 background-attachment: 5%;
563 text-align: center; 626 background-size: 20% auto;
564 } 627 }
565 628
566 section.title p { 629 section.title h1 {
567 bottom: 25%; 630 color: #808db5;
568 width: 100%; 631 text-align: center;
569 position: absolute; 632 }
570 font-size: 25px; 633
571 color: #4b4b4b; 634 section.title p {
572 background: linear-gradient(transparent 90%, #ffcc00 0%); 635 bottom: 25%;
573 } 636 width: 100%;
574 637 position: absolute;
575 section.slide h1 { 638 font-size: 25px;
576 width: 95%; 639 color: #4b4b4b;
577 color: white; 640 background: linear-gradient(transparent 90%, #ffcc00 0%);
578 background-color: #808db5; 641 }
579 position: absolute; 642
580 left: 50px; 643 section.slide h1 {
581 top: 35px; 644 width: 95%;
645 color: white;
646 background-color: #808db5;
647 position: absolute;
648 left: 50px;
649 top: 35px;
650 }
651
652 section.fig_cg p {
653 top: 300px;
654 text-align: center;
582 } 655 }
583 ;--heading-divider:1;" data-size="16:9"> 656 ;--heading-divider:1;" data-size="16:9">
584 <h1>Agda の基本 短縮記法</h1> 657 <h1>Agda の基本 短縮記法</h1>
585 <ul> 658 <ul>
586 <li>with を使用することでその変数のパターンマッチすることもできる</li> 659 <li>with を使用することでその変数のパターンマッチすることもできる</li>
635 background-color: #808db5; 708 background-color: #808db5;
636 position: absolute; 709 position: absolute;
637 left: 50px; 710 left: 50px;
638 top: 35px; 711 top: 35px;
639 } 712 }
640 " data-heading-divider="1" class="slide" data-marpit-pagination="8" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { 713
641 background-color: #FFFFFF; 714 section.fig_cg p {
642 font-size: 28px; 715 top: 300px;
643 color: #4b4b4b; 716 text-align: center;
644 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 717 }
645 background-image: url(&quot;logo.svg&quot;); 718 " data-heading-divider="1" class="slide" data-marpit-pagination="8" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section {
646 background-position: right 3% bottom 2%; 719 background-color: #FFFFFF;
647 background-repeat: no-repeat; 720 font-size: 28px;
648 background-attachment: 5%; 721 color: #4b4b4b;
649 background-size: 20% auto; 722 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
650 } 723 background-image: url(&quot;logo.svg&quot;);
651 724 background-position: right 3% bottom 2%;
652 section.title h1 { 725 background-repeat: no-repeat;
653 color: #808db5; 726 background-attachment: 5%;
654 text-align: center; 727 background-size: 20% auto;
655 } 728 }
656 729
657 section.title p { 730 section.title h1 {
658 bottom: 25%; 731 color: #808db5;
659 width: 100%; 732 text-align: center;
660 position: absolute; 733 }
661 font-size: 25px; 734
662 color: #4b4b4b; 735 section.title p {
663 background: linear-gradient(transparent 90%, #ffcc00 0%); 736 bottom: 25%;
664 } 737 width: 100%;
665 738 position: absolute;
666 section.slide h1 { 739 font-size: 25px;
667 width: 95%; 740 color: #4b4b4b;
668 color: white; 741 background: linear-gradient(transparent 90%, #ffcc00 0%);
669 background-color: #808db5; 742 }
670 position: absolute; 743
671 left: 50px; 744 section.slide h1 {
672 top: 35px; 745 width: 95%;
746 color: white;
747 background-color: #808db5;
748 position: absolute;
749 left: 50px;
750 top: 35px;
751 }
752
753 section.fig_cg p {
754 top: 300px;
755 text-align: center;
673 } 756 }
674 ;--heading-divider:1;" data-size="16:9"> 757 ;--heading-divider:1;" data-size="16:9">
675 <h1>Gears Agda の記法</h1> 758 <h1>Gears Agda の記法</h1>
676 <ul> 759 <ul>
677 <li>Agda では関数の再帰呼び出しが可能であるが、CbC で再起処理を実装しても値は帰って来ない 760 <li>Agda では関数の再帰呼び出しが可能であるが、CbC で再起処理を実装しても値は帰って来ない
721 background-color: #808db5; 804 background-color: #808db5;
722 position: absolute; 805 position: absolute;
723 left: 50px; 806 left: 50px;
724 top: 35px; 807 top: 35px;
725 } 808 }
726 " data-heading-divider="1" class="slide" data-marpit-pagination="9" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { 809
727 background-color: #FFFFFF; 810 section.fig_cg p {
728 font-size: 28px; 811 top: 300px;
729 color: #4b4b4b; 812 text-align: center;
730 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 813 }
731 background-image: url(&quot;logo.svg&quot;); 814 " data-heading-divider="1" class="slide" data-marpit-pagination="9" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section {
732 background-position: right 3% bottom 2%; 815 background-color: #FFFFFF;
733 background-repeat: no-repeat; 816 font-size: 28px;
734 background-attachment: 5%; 817 color: #4b4b4b;
735 background-size: 20% auto; 818 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
736 } 819 background-image: url(&quot;logo.svg&quot;);
737 820 background-position: right 3% bottom 2%;
738 section.title h1 { 821 background-repeat: no-repeat;
739 color: #808db5; 822 background-attachment: 5%;
740 text-align: center; 823 background-size: 20% auto;
741 } 824 }
742 825
743 section.title p { 826 section.title h1 {
744 bottom: 25%; 827 color: #808db5;
745 width: 100%; 828 text-align: center;
746 position: absolute; 829 }
747 font-size: 25px; 830
748 color: #4b4b4b; 831 section.title p {
749 background: linear-gradient(transparent 90%, #ffcc00 0%); 832 bottom: 25%;
750 } 833 width: 100%;
751 834 position: absolute;
752 section.slide h1 { 835 font-size: 25px;
753 width: 95%; 836 color: #4b4b4b;
754 color: white; 837 background: linear-gradient(transparent 90%, #ffcc00 0%);
755 background-color: #808db5; 838 }
756 position: absolute; 839
757 left: 50px; 840 section.slide h1 {
758 top: 35px; 841 width: 95%;
842 color: white;
843 background-color: #808db5;
844 position: absolute;
845 left: 50px;
846 top: 35px;
847 }
848
849 section.fig_cg p {
850 top: 300px;
851 text-align: center;
759 } 852 }
760 ;--heading-divider:1;" data-size="16:9"> 853 ;--heading-divider:1;" data-size="16:9">
761 <h1>Gears Agda と Gears CbC の対応 x</h1> 854 <h1>Gears Agda と Gears CbC の対応 x</h1>
762 <ul> 855 <ul>
763 <li> 856 <li>
769 <li> 862 <li>
770 <p>Gears Agda での検証がCbCによる高速な実行の信頼性となる</p> 863 <p>Gears Agda での検証がCbCによる高速な実行の信頼性となる</p>
771 </li> 864 </li>
772 </ul> 865 </ul>
773 </section> 866 </section>
774 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="10" data-paginate="true" data-class="slide" data-theme="default" data-style="section { 867 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="10" data-paginate="true" data-class="fig_cg" data-theme="default" data-style="section {
775 background-color: #FFFFFF; 868 background-color: #FFFFFF;
776 font-size: 28px; 869 font-size: 28px;
777 color: #4b4b4b; 870 color: #4b4b4b;
778 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 871 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
779 background-image: url(&quot;logo.svg&quot;); 872 background-image: url(&quot;logo.svg&quot;);
780 background-position: right 3% bottom 2%; 873 background-position: right 3% bottom 2%;
781 background-repeat: no-repeat; 874 background-repeat: no-repeat;
782 background-attachment: 5%; 875 background-attachment: 5%;
783 background-size: 20% auto; 876 background-size: 20% auto;
784 } 877 }
785 878
786 section.title h1 { 879 section.title h1 {
787 color: #808db5; 880 color: #808db5;
788 text-align: center; 881 text-align: center;
789 } 882 }
790 883
791 section.title p { 884 section.title p {
792 bottom: 25%; 885 bottom: 25%;
793 width: 100%; 886 width: 100%;
794 position: absolute; 887 position: absolute;
795 font-size: 25px; 888 font-size: 25px;
796 color: #4b4b4b; 889 color: #4b4b4b;
797 background: linear-gradient(transparent 90%, #ffcc00 0%); 890 background: linear-gradient(transparent 90%, #ffcc00 0%);
798 } 891 }
799 892
800 section.slide h1 { 893 section.slide h1 {
801 width: 95%; 894 width: 95%;
802 color: white; 895 color: white;
803 background-color: #808db5; 896 background-color: #808db5;
804 position: absolute; 897 position: absolute;
805 left: 50px; 898 left: 50px;
806 top: 35px; 899 top: 35px;
807 } 900 }
808 " data-heading-divider="1" class="slide" data-marpit-pagination="10" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { 901
809 background-color: #FFFFFF; 902 section.fig_cg p {
810 font-size: 28px; 903 top: 300px;
811 color: #4b4b4b; 904 text-align: center;
812 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 905 }
813 background-image: url(&quot;logo.svg&quot;); 906 " data-heading-divider="1" class="fig_cg" data-marpit-pagination="10" data-marpit-pagination-total="24" style="--paginate:true;--class:fig_cg;--theme:default;--style:section {
814 background-position: right 3% bottom 2%; 907 background-color: #FFFFFF;
815 background-repeat: no-repeat; 908 font-size: 28px;
816 background-attachment: 5%; 909 color: #4b4b4b;
817 background-size: 20% auto; 910 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
818 } 911 background-image: url(&quot;logo.svg&quot;);
819 912 background-position: right 3% bottom 2%;
820 section.title h1 { 913 background-repeat: no-repeat;
821 color: #808db5; 914 background-attachment: 5%;
822 text-align: center; 915 background-size: 20% auto;
823 } 916 }
824 917
825 section.title p { 918 section.title h1 {
826 bottom: 25%; 919 color: #808db5;
827 width: 100%; 920 text-align: center;
828 position: absolute; 921 }
829 font-size: 25px; 922
830 color: #4b4b4b; 923 section.title p {
831 background: linear-gradient(transparent 90%, #ffcc00 0%); 924 bottom: 25%;
832 } 925 width: 100%;
833 926 position: absolute;
834 section.slide h1 { 927 font-size: 25px;
835 width: 95%; 928 color: #4b4b4b;
836 color: white; 929 background: linear-gradient(transparent 90%, #ffcc00 0%);
837 background-color: #808db5; 930 }
838 position: absolute; 931
839 left: 50px; 932 section.slide h1 {
840 top: 35px; 933 width: 95%;
934 color: white;
935 background-color: #808db5;
936 position: absolute;
937 left: 50px;
938 top: 35px;
939 }
940
941 section.fig_cg p {
942 top: 300px;
943 text-align: center;
841 } 944 }
842 ;--heading-divider:1;" data-size="16:9"> 945 ;--heading-divider:1;" data-size="16:9">
843 <h1>Normal level と Meta Level を用いた信頼性の向上</h1> 946 <h1>Normal level と Meta Level を用いた信頼性の向上</h1>
844 <p>CbCのプログラムの実行部分は以下の2つから構成される</p> 947 <ul>
845 <ul> 948 <li>CbCのプログラムの実行部分は以下の2つから構成される</li>
846 <li>Normal Level は軽量継続で関数型プログラミングとなる 949 <li>Normal Level は軽量継続で関数型プログラミングとなる
847 <ul> 950 <ul>
848 <li>atomicってなんだろう</li>
849 <li>ポインタの操作はここでは行わず Meta Level にて行う</li> 951 <li>ポインタの操作はここでは行わず Meta Level にて行う</li>
850 </ul> 952 </ul>
851 </li> 953 </li>
852 <li>Meta Level では信頼性を保証するために必要な計算を行う 954 <li>Meta Level では信頼性を保証するために必要な計算を行う
853 <ul> 955 <ul>
857 <li>並列実行（他のプロセスとの干渉）</li> 959 <li>並列実行（他のプロセスとの干渉）</li>
858 <li>monad</li> 960 <li>monad</li>
859 </ul> 961 </ul>
860 </li> 962 </li>
861 </ul> 963 </ul>
964
965 <p><img src="meta_cg_dg.svg" alt="" style="height:500px;" /></p>
862 </section> 966 </section>
863 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="11" data-paginate="true" data-class="slide" data-theme="default" data-style="section { 967 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="11" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
864 background-color: #FFFFFF; 968 background-color: #FFFFFF;
865 font-size: 28px; 969 font-size: 28px;
866 color: #4b4b4b; 970 color: #4b4b4b;
892 background-color: #808db5; 996 background-color: #808db5;
893 position: absolute; 997 position: absolute;
894 left: 50px; 998 left: 50px;
895 top: 35px; 999 top: 35px;
896 } 1000 }
897 " data-heading-divider="1" class="slide" data-marpit-pagination="11" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { 1001
898 background-color: #FFFFFF; 1002 section.fig_cg p {
899 font-size: 28px; 1003 top: 300px;
900 color: #4b4b4b; 1004 text-align: center;
901 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 1005 }
902 background-image: url(&quot;logo.svg&quot;); 1006 " data-heading-divider="1" class="slide" data-marpit-pagination="11" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section {
903 background-position: right 3% bottom 2%; 1007 background-color: #FFFFFF;
904 background-repeat: no-repeat; 1008 font-size: 28px;
905 background-attachment: 5%; 1009 color: #4b4b4b;
906 background-size: 20% auto; 1010 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
907 } 1011 background-image: url(&quot;logo.svg&quot;);
908 1012 background-position: right 3% bottom 2%;
909 section.title h1 { 1013 background-repeat: no-repeat;
910 color: #808db5; 1014 background-attachment: 5%;
911 text-align: center; 1015 background-size: 20% auto;
912 } 1016 }
913 1017
914 section.title p { 1018 section.title h1 {
915 bottom: 25%; 1019 color: #808db5;
916 width: 100%; 1020 text-align: center;
917 position: absolute; 1021 }
918 font-size: 25px; 1022
919 color: #4b4b4b; 1023 section.title p {
920 background: linear-gradient(transparent 90%, #ffcc00 0%); 1024 bottom: 25%;
921 } 1025 width: 100%;
922 1026 position: absolute;
923 section.slide h1 { 1027 font-size: 25px;
924 width: 95%; 1028 color: #4b4b4b;
925 color: white; 1029 background: linear-gradient(transparent 90%, #ffcc00 0%);
926 background-color: #808db5; 1030 }
927 position: absolute; 1031
928 left: 50px; 1032 section.slide h1 {
929 top: 35px; 1033 width: 95%;
930 } 1034 color: white;
931 ;--heading-divider:1;" data-size="16:9"> 1035 background-color: #808db5;
932 <h1>s</h1> 1036 position: absolute;
933 &lt;div src="meta-cg-dg.pdf"&gt; &lt;/div&gt; 1037 left: 50px;
934 </section> 1038 top: 35px;
935 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="12" data-paginate="true" data-class="slide" data-theme="default" data-style="section { 1039 }
936 background-color: #FFFFFF; 1040
937 font-size: 28px; 1041 section.fig_cg p {
938 color: #4b4b4b; 1042 top: 300px;
939 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 1043 text-align: center;
940 background-image: url(&quot;logo.svg&quot;); 1044 }
941 background-position: right 3% bottom 2%; 1045 ;--heading-divider:1;" data-size="16:9">
942 background-repeat: no-repeat; 1046 <h1>Gears Agda と Hoare Logic</h1>
943 background-attachment: 5%; 1047
944 background-size: 20% auto; 1048 <p>C.A.R Hoare, R.W Floyd が考案</p>
945 } 1049 <ul>
946 1050 <li>Pre Condition → Command → Post Condition</li>
947 section.title h1 { 1051 </ul>
948 color: #808db5; 1052 <p>Gears Agda による Command の例</p>
949 text-align: center;
950 }
951
952 section.title p {
953 bottom: 25%;
954 width: 100%;
955 position: absolute;
956 font-size: 25px;
957 color: #4b4b4b;
958 background: linear-gradient(transparent 90%, #ffcc00 0%);
959 }
960
961 section.slide h1 {
962 width: 95%;
963 color: white;
964 background-color: #808db5;
965 position: absolute;
966 left: 50px;
967 top: 35px;
968 }
969 " data-heading-divider="1" class="slide" data-marpit-pagination="12" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section {
970 background-color: #FFFFFF;
971 font-size: 28px;
972 color: #4b4b4b;
973 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
974 background-image: url(&quot;logo.svg&quot;);
975 background-position: right 3% bottom 2%;
976 background-repeat: no-repeat;
977 background-attachment: 5%;
978 background-size: 20% auto;
979 }
980
981 section.title h1 {
982 color: #808db5;
983 text-align: center;
984 }
985
986 section.title p {
987 bottom: 25%;
988 width: 100%;
989 position: absolute;
990 font-size: 25px;
991 color: #4b4b4b;
992 background: linear-gradient(transparent 90%, #ffcc00 0%);
993 }
994
995 section.slide h1 {
996 width: 95%;
997 color: white;
998 background-color: #808db5;
999 position: absolute;
1000 left: 50px;
1001 top: 35px;
1002 }
1003 ;--heading-divider:1;" data-size="16:9">
1004 <h1>Hoare Logic について</h1>
1005 <ul>
1006 <li>Hoare Logic とは C.A.R Hoare, R.W Floyd が考案したプログラムの検証の手法</li>
1007 <li>「プログラムの事前条件 (P) が成立しているときコマンド (C) 実行して停止すると事後条件 (Q) が成り立つ」というもの
1008 <ul>
1009 <li>CbC の実行を継続するという性質に非常に相性が良い</li>
1010 </ul>
1011 </li>
1012 </ul>
1013 <p>pre/post condition を Gears Agda では Meta Input Data Gear として<br />
1014 プログラム中に遷移させていくことで、プログラムが終始仕様に沿った動きをしている<br />
1015 ことを検証する</p>
1016 </section>
1017 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="13" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
1018 background-color: #FFFFFF;
1019 font-size: 28px;
1020 color: #4b4b4b;
1021 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
1022 background-image: url(&quot;logo.svg&quot;);
1023 background-position: right 3% bottom 2%;
1024 background-repeat: no-repeat;
1025 background-attachment: 5%;
1026 background-size: 20% auto;
1027 }
1028
1029 section.title h1 {
1030 color: #808db5;
1031 text-align: center;
1032 }
1033
1034 section.title p {
1035 bottom: 25%;
1036 width: 100%;
1037 position: absolute;
1038 font-size: 25px;
1039 color: #4b4b4b;
1040 background: linear-gradient(transparent 90%, #ffcc00 0%);
1041 }
1042
1043 section.slide h1 {
1044 width: 95%;
1045 color: white;
1046 background-color: #808db5;
1047 position: absolute;
1048 left: 50px;
1049 top: 35px;
1050 }
1051 " data-heading-divider="1" class="slide" data-marpit-pagination="13" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section {
1052 background-color: #FFFFFF;
1053 font-size: 28px;
1054 color: #4b4b4b;
1055 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
1056 background-image: url(&quot;logo.svg&quot;);
1057 background-position: right 3% bottom 2%;
1058 background-repeat: no-repeat;
1059 background-attachment: 5%;
1060 background-size: 20% auto;
1061 }
1062
1063 section.title h1 {
1064 color: #808db5;
1065 text-align: center;
1066 }
1067
1068 section.title p {
1069 bottom: 25%;
1070 width: 100%;
1071 position: absolute;
1072 font-size: 25px;
1073 color: #4b4b4b;
1074 background: linear-gradient(transparent 90%, #ffcc00 0%);
1075 }
1076
1077 section.slide h1 {
1078 width: 95%;
1079 color: white;
1080 background-color: #808db5;
1081 position: absolute;
1082 left: 50px;
1083 top: 35px;
1084 }
1085 ;--heading-divider:1;" data-size="16:9">
1086 <h1>Gears Agda による検証の例（実装）</h1>
1087 <ul>
1088 <li>while program の検証を例に挙げる
1089 <ul>
1090 <li>以下は実装部分のコードとなる</li>
1091 </ul>
1092 </li>
1093 </ul>
1094 <pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>{-# TERMINATING #-} 1053 <pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>{-# TERMINATING #-}
1095 whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t 1054 whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t
1096 whileLoop env next with lt 0 (varn env) 1055 whileLoop env next with lt 0 (varn env)
1097 whileLoop env next | false = next env 1056 whileLoop env next | false = next env
1098 whileLoop env next | true = whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next 1057 whileLoop env next | true = whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
1099 </span></span></foreignObject></svg></code></pre> 1058 </span></span></foreignObject></svg></code></pre>
1100 </section> 1059 <ul>
1101 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="14" data-paginate="true" data-class="slide" data-theme="default" data-style="section { 1060 <li><code>{-# TERMINATING #-}</code></li>
1102 background-color: #FFFFFF; 1061 <li>with 文</li>
1103 font-size: 28px; 1062 <li>型と値</li>
1104 color: #4b4b4b; 1063 </ul>
1105 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 1064 </section>
1106 background-image: url(&quot;logo.svg&quot;); 1065 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="12" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
1107 background-position: right 3% bottom 2%; 1066 background-color: #FFFFFF;
1108 background-repeat: no-repeat; 1067 font-size: 28px;
1109 background-attachment: 5%; 1068 color: #4b4b4b;
1110 background-size: 20% auto; 1069 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
1111 } 1070 background-image: url(&quot;logo.svg&quot;);
1112 1071 background-position: right 3% bottom 2%;
1113 section.title h1 { 1072 background-repeat: no-repeat;
1114 color: #808db5; 1073 background-attachment: 5%;
1115 text-align: center; 1074 background-size: 20% auto;
1116 } 1075 }
1117 1076
1118 section.title p { 1077 section.title h1 {
1119 bottom: 25%; 1078 color: #808db5;
1120 width: 100%; 1079 text-align: center;
1121 position: absolute; 1080 }
1122 font-size: 25px; 1081
1123 color: #4b4b4b; 1082 section.title p {
1124 background: linear-gradient(transparent 90%, #ffcc00 0%); 1083 bottom: 25%;
1125 } 1084 width: 100%;
1126 1085 position: absolute;
1127 section.slide h1 { 1086 font-size: 25px;
1128 width: 95%; 1087 color: #4b4b4b;
1129 color: white; 1088 background: linear-gradient(transparent 90%, #ffcc00 0%);
1130 background-color: #808db5; 1089 }
1131 position: absolute; 1090
1132 left: 50px; 1091 section.slide h1 {
1133 top: 35px; 1092 width: 95%;
1134 } 1093 color: white;
1135 " data-heading-divider="1" class="slide" data-marpit-pagination="14" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { 1094 background-color: #808db5;
1136 background-color: #FFFFFF; 1095 position: absolute;
1137 font-size: 28px; 1096 left: 50px;
1138 color: #4b4b4b; 1097 top: 35px;
1139 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 1098 }
1140 background-image: url(&quot;logo.svg&quot;); 1099
1141 background-position: right 3% bottom 2%; 1100 section.fig_cg p {
1142 background-repeat: no-repeat; 1101 top: 300px;
1143 background-attachment: 5%; 1102 text-align: center;
1144 background-size: 20% auto; 1103 }
1145 } 1104 " data-heading-divider="1" class="slide" data-marpit-pagination="12" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section {
1146 1105 background-color: #FFFFFF;
1147 section.title h1 { 1106 font-size: 28px;
1148 color: #808db5; 1107 color: #4b4b4b;
1149 text-align: center; 1108 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
1150 } 1109 background-image: url(&quot;logo.svg&quot;);
1151 1110 background-position: right 3% bottom 2%;
1152 section.title p { 1111 background-repeat: no-repeat;
1153 bottom: 25%; 1112 background-attachment: 5%;
1154 width: 100%; 1113 background-size: 20% auto;
1155 position: absolute; 1114 }
1156 font-size: 25px; 1115
1157 color: #4b4b4b; 1116 section.title h1 {
1158 background: linear-gradient(transparent 90%, #ffcc00 0%); 1117 color: #808db5;
1159 } 1118 text-align: center;
1160 1119 }
1161 section.slide h1 { 1120
1162 width: 95%; 1121 section.title p {
1163 color: white; 1122 bottom: 25%;
1164 background-color: #808db5; 1123 width: 100%;
1165 position: absolute; 1124 position: absolute;
1166 left: 50px; 1125 font-size: 25px;
1167 top: 35px; 1126 color: #4b4b4b;
1127 background: linear-gradient(transparent 90%, #ffcc00 0%);
1128 }
1129
1130 section.slide h1 {
1131 width: 95%;
1132 color: white;
1133 background-color: #808db5;
1134 position: absolute;
1135 left: 50px;
1136 top: 35px;
1137 }
1138
1139 section.fig_cg p {
1140 top: 300px;
1141 text-align: center;
1168 } 1142 }
1169 ;--heading-divider:1;" data-size="16:9"> 1143 ;--heading-divider:1;" data-size="16:9">
1170 <h1>Gears Agda による検証の例（検証付き実装）</h1> 1144 <h1>Gears Agda による検証の例（検証付き実装）</h1>
1171 <ul> 1145 <ul>
1172 <li>先ほど実装した while program に対して証明を付ける</li> 1146 <li>先ほど実装した while program に対して証明を付ける</li>
1186 <li>Meta Gear にて証明を値としてあたえているため</li> 1160 <li>Meta Gear にて証明を値としてあたえているため</li>
1187 </ul> 1161 </ul>
1188 </li> 1162 </li>
1189 </ul> 1163 </ul>
1190 </section> 1164 </section>
1191 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="15" data-paginate="true" data-class="slide" data-theme="default" data-style="section { 1165 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="13" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
1192 background-color: #FFFFFF; 1166 background-color: #FFFFFF;
1193 font-size: 28px; 1167 font-size: 28px;
1194 color: #4b4b4b; 1168 color: #4b4b4b;
1195 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 1169 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
1196 background-image: url(&quot;logo.svg&quot;); 1170 background-image: url(&quot;logo.svg&quot;);
1197 background-position: right 3% bottom 2%; 1171 background-position: right 3% bottom 2%;
1198 background-repeat: no-repeat; 1172 background-repeat: no-repeat;
1199 background-attachment: 5%; 1173 background-attachment: 5%;
1200 background-size: 20% auto; 1174 background-size: 20% auto;
1201 } 1175 }
1202 1176
1203 section.title h1 { 1177 section.title h1 {
1204 color: #808db5; 1178 color: #808db5;
1205 text-align: center; 1179 text-align: center;
1206 } 1180 }
1207 1181
1208 section.title p { 1182 section.title p {
1209 bottom: 25%; 1183 bottom: 25%;
1210 width: 100%; 1184 width: 100%;
1211 position: absolute; 1185 position: absolute;
1212 font-size: 25px; 1186 font-size: 25px;
1213 color: #4b4b4b; 1187 color: #4b4b4b;
1214 background: linear-gradient(transparent 90%, #ffcc00 0%); 1188 background: linear-gradient(transparent 90%, #ffcc00 0%);
1215 } 1189 }
1216 1190
1217 section.slide h1 { 1191 section.slide h1 {
1218 width: 95%; 1192 width: 95%;
1219 color: white; 1193 color: white;
1220 background-color: #808db5; 1194 background-color: #808db5;
1221 position: absolute; 1195 position: absolute;
1222 left: 50px; 1196 left: 50px;
1223 top: 35px; 1197 top: 35px;
1224 } 1198 }
1225 " data-heading-divider="1" class="slide" data-marpit-pagination="15" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { 1199
1226 background-color: #FFFFFF; 1200 section.fig_cg p {
1227 font-size: 28px; 1201 top: 300px;
1228 color: #4b4b4b; 1202 text-align: center;
1229 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 1203 }
1230 background-image: url(&quot;logo.svg&quot;); 1204 " data-heading-divider="1" class="slide" data-marpit-pagination="13" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section {
1231 background-position: right 3% bottom 2%; 1205 background-color: #FFFFFF;
1232 background-repeat: no-repeat; 1206 font-size: 28px;
1233 background-attachment: 5%; 1207 color: #4b4b4b;
1234 background-size: 20% auto; 1208 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
1235 } 1209 background-image: url(&quot;logo.svg&quot;);
1236 1210 background-position: right 3% bottom 2%;
1237 section.title h1 { 1211 background-repeat: no-repeat;
1238 color: #808db5; 1212 background-attachment: 5%;
1239 text-align: center; 1213 background-size: 20% auto;
1240 } 1214 }
1241 1215
1242 section.title p { 1216 section.title h1 {
1243 bottom: 25%; 1217 color: #808db5;
1244 width: 100%; 1218 text-align: center;
1245 position: absolute; 1219 }
1246 font-size: 25px; 1220
1247 color: #4b4b4b; 1221 section.title p {
1248 background: linear-gradient(transparent 90%, #ffcc00 0%); 1222 bottom: 25%;
1249 } 1223 width: 100%;
1250 1224 position: absolute;
1251 section.slide h1 { 1225 font-size: 25px;
1252 width: 95%; 1226 color: #4b4b4b;
1253 color: white; 1227 background: linear-gradient(transparent 90%, #ffcc00 0%);
1254 background-color: #808db5; 1228 }
1255 position: absolute; 1229
1256 left: 50px; 1230 section.slide h1 {
1257 top: 35px; 1231 width: 95%;
1232 color: white;
1233 background-color: #808db5;
1234 position: absolute;
1235 left: 50px;
1236 top: 35px;
1237 }
1238
1239 section.fig_cg p {
1240 top: 300px;
1241 text-align: center;
1258 } 1242 }
1259 ;--heading-divider:1;" data-size="16:9"> 1243 ;--heading-divider:1;" data-size="16:9">
1260 <h1>test との違い</h1> 1244 <h1>test との違い</h1>
1261 <ul> 1245 <ul>
1262 <li>test では実数を与えた際の出力が仕様に沿ったものであるかを検証する 1246 <li>test では実数を与えた際の出力が仕様に沿ったものであるかを検証する
1269 <li>そのため、入力の型の範囲全てに対して仕様を満たしているか検証できる</li> 1253 <li>そのため、入力の型の範囲全てに対して仕様を満たしているか検証できる</li>
1270 </ul> 1254 </ul>
1271 </li> 1255 </li>
1272 </ul> 1256 </ul>
1273 </section> 1257 </section>
1274 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="16" data-paginate="true" data-class="slide" data-theme="default" data-style="section { 1258 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="14" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
1275 background-color: #FFFFFF; 1259 background-color: #FFFFFF;
1276 font-size: 28px; 1260 font-size: 28px;
1277 color: #4b4b4b; 1261 color: #4b4b4b;
1278 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 1262 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
1279 background-image: url(&quot;logo.svg&quot;); 1263 background-image: url(&quot;logo.svg&quot;);
1280 background-position: right 3% bottom 2%; 1264 background-position: right 3% bottom 2%;
1281 background-repeat: no-repeat; 1265 background-repeat: no-repeat;
1282 background-attachment: 5%; 1266 background-attachment: 5%;
1283 background-size: 20% auto; 1267 background-size: 20% auto;
1284 } 1268 }
1285 1269
1286 section.title h1 { 1270 section.title h1 {
1287 color: #808db5; 1271 color: #808db5;
1288 text-align: center; 1272 text-align: center;
1289 } 1273 }
1290 1274
1291 section.title p { 1275 section.title p {
1292 bottom: 25%; 1276 bottom: 25%;
1293 width: 100%; 1277 width: 100%;
1294 position: absolute; 1278 position: absolute;
1295 font-size: 25px; 1279 font-size: 25px;
1296 color: #4b4b4b; 1280 color: #4b4b4b;
1297 background: linear-gradient(transparent 90%, #ffcc00 0%); 1281 background: linear-gradient(transparent 90%, #ffcc00 0%);
1298 } 1282 }
1299 1283
1300 section.slide h1 { 1284 section.slide h1 {
1301 width: 95%; 1285 width: 95%;
1302 color: white; 1286 color: white;
1303 background-color: #808db5; 1287 background-color: #808db5;
1304 position: absolute; 1288 position: absolute;
1305 left: 50px; 1289 left: 50px;
1306 top: 35px; 1290 top: 35px;
1307 } 1291 }
1308 " data-heading-divider="1" class="slide" data-marpit-pagination="16" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { 1292
1309 background-color: #FFFFFF; 1293 section.fig_cg p {
1310 font-size: 28px; 1294 top: 300px;
1311 color: #4b4b4b; 1295 text-align: center;
1312 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 1296 }
1313 background-image: url(&quot;logo.svg&quot;); 1297 " data-heading-divider="1" class="slide" data-marpit-pagination="14" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section {
1314 background-position: right 3% bottom 2%; 1298 background-color: #FFFFFF;
1315 background-repeat: no-repeat; 1299 font-size: 28px;
1316 background-attachment: 5%; 1300 color: #4b4b4b;
1317 background-size: 20% auto; 1301 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
1318 } 1302 background-image: url(&quot;logo.svg&quot;);
1319 1303 background-position: right 3% bottom 2%;
1320 section.title h1 { 1304 background-repeat: no-repeat;
1321 color: #808db5; 1305 background-attachment: 5%;
1322 text-align: center; 1306 background-size: 20% auto;
1323 } 1307 }
1324 1308
1325 section.title p { 1309 section.title h1 {
1326 bottom: 25%; 1310 color: #808db5;
1327 width: 100%; 1311 text-align: center;
1328 position: absolute; 1312 }
1329 font-size: 25px; 1313
1330 color: #4b4b4b; 1314 section.title p {
1331 background: linear-gradient(transparent 90%, #ffcc00 0%); 1315 bottom: 25%;
1332 } 1316 width: 100%;
1333 1317 position: absolute;
1334 section.slide h1 { 1318 font-size: 25px;
1335 width: 95%; 1319 color: #4b4b4b;
1336 color: white; 1320 background: linear-gradient(transparent 90%, #ffcc00 0%);
1337 background-color: #808db5; 1321 }
1338 position: absolute; 1322
1339 left: 50px; 1323 section.slide h1 {
1340 top: 35px; 1324 width: 95%;
1325 color: white;
1326 background-color: #808db5;
1327 position: absolute;
1328 left: 50px;
1329 top: 35px;
1330 }
1331
1332 section.fig_cg p {
1333 top: 300px;
1334 text-align: center;
1341 } 1335 }
1342 ;--heading-divider:1;" data-size="16:9"> 1336 ;--heading-divider:1;" data-size="16:9">
1343 <h1>Gears Agda による BinaryTree の実装</h1> 1337 <h1>Gears Agda による BinaryTree の実装</h1>
1344 <ul> 1338 <ul>
1345 <li>Agdaが変数への再代入を許していないためそのままでは木構造を実装できない 1339 <li>Agdaが変数への再代入を許していないためそのままでは木構造を実装できない
1350 </ul> 1344 </ul>
1351 </li> 1345 </li>
1352 <li>ここの説明いらないかも？</li> 1346 <li>ここの説明いらないかも？</li>
1353 </ul> 1347 </ul>
1354 </section> 1348 </section>
1355 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="17" data-paginate="true" data-class="slide" data-theme="default" data-style="section { 1349 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="15" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
1356 background-color: #FFFFFF; 1350 background-color: #FFFFFF;
1357 font-size: 28px; 1351 font-size: 28px;
1358 color: #4b4b4b; 1352 color: #4b4b4b;
1359 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 1353 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
1360 background-image: url(&quot;logo.svg&quot;); 1354 background-image: url(&quot;logo.svg&quot;);
1361 background-position: right 3% bottom 2%; 1355 background-position: right 3% bottom 2%;
1362 background-repeat: no-repeat; 1356 background-repeat: no-repeat;
1363 background-attachment: 5%; 1357 background-attachment: 5%;
1364 background-size: 20% auto; 1358 background-size: 20% auto;
1365 } 1359 }
1366 1360
1367 section.title h1 { 1361 section.title h1 {
1368 color: #808db5; 1362 color: #808db5;
1369 text-align: center; 1363 text-align: center;
1370 } 1364 }
1371 1365
1372 section.title p { 1366 section.title p {
1373 bottom: 25%; 1367 bottom: 25%;
1374 width: 100%; 1368 width: 100%;
1375 position: absolute; 1369 position: absolute;
1376 font-size: 25px; 1370 font-size: 25px;
1377 color: #4b4b4b; 1371 color: #4b4b4b;
1378 background: linear-gradient(transparent 90%, #ffcc00 0%); 1372 background: linear-gradient(transparent 90%, #ffcc00 0%);
1379 } 1373 }
1380 1374
1381 section.slide h1 { 1375 section.slide h1 {
1382 width: 95%; 1376 width: 95%;
1383 color: white; 1377 color: white;
1384 background-color: #808db5; 1378 background-color: #808db5;
1385 position: absolute; 1379 position: absolute;
1386 left: 50px; 1380 left: 50px;
1387 top: 35px; 1381 top: 35px;
1388 } 1382 }
1389 " data-heading-divider="1" class="slide" data-marpit-pagination="17" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { 1383
1390 background-color: #FFFFFF; 1384 section.fig_cg p {
1391 font-size: 28px; 1385 top: 300px;
1392 color: #4b4b4b; 1386 text-align: center;
1393 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 1387 }
1394 background-image: url(&quot;logo.svg&quot;); 1388 " data-heading-divider="1" class="slide" data-marpit-pagination="15" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section {
1395 background-position: right 3% bottom 2%; 1389 background-color: #FFFFFF;
1396 background-repeat: no-repeat; 1390 font-size: 28px;
1397 background-attachment: 5%; 1391 color: #4b4b4b;
1398 background-size: 20% auto; 1392 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
1399 } 1393 background-image: url(&quot;logo.svg&quot;);
1400 1394 background-position: right 3% bottom 2%;
1401 section.title h1 { 1395 background-repeat: no-repeat;
1402 color: #808db5; 1396 background-attachment: 5%;
1403 text-align: center; 1397 background-size: 20% auto;
1404 } 1398 }
1405 1399
1406 section.title p { 1400 section.title h1 {
1407 bottom: 25%; 1401 color: #808db5;
1408 width: 100%; 1402 text-align: center;
1409 position: absolute; 1403 }
1410 font-size: 25px; 1404
1411 color: #4b4b4b; 1405 section.title p {
1412 background: linear-gradient(transparent 90%, #ffcc00 0%); 1406 bottom: 25%;
1413 } 1407 width: 100%;
1414 1408 position: absolute;
1415 section.slide h1 { 1409 font-size: 25px;
1416 width: 95%; 1410 color: #4b4b4b;
1417 color: white; 1411 background: linear-gradient(transparent 90%, #ffcc00 0%);
1418 background-color: #808db5; 1412 }
1419 position: absolute; 1413
1420 left: 50px; 1414 section.slide h1 {
1421 top: 35px; 1415 width: 95%;
1416 color: white;
1417 background-color: #808db5;
1418 position: absolute;
1419 left: 50px;
1420 top: 35px;
1421 }
1422
1423 section.fig_cg p {
1424 top: 300px;
1425 text-align: center;
1422 } 1426 }
1423 ;--heading-divider:1;" data-size="16:9"> 1427 ;--heading-divider:1;" data-size="16:9">
1424 <h1>Gears Agda による BinaryTree の実装 find node</h1> 1428 <h1>Gears Agda による BinaryTree の実装 find node</h1>
1425 <pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>find : {n m : Level} {A : Set n} {t : Set m} → (env : Env A ) 1429 <pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>find : {n m : Level} {A : Set n} {t : Set m} → (env : Env A )
1426 → (next : (env : Env A ) → t ) → (exit : (env : Env A ) → t ) → t 1430 → (next : (env : Env A ) → t ) → (exit : (env : Env A ) → t ) → t
1429 find key n st _ exit | tri≈ ¬a b ¬c = exit n st 1433 find key n st _ exit | tri≈ ¬a b ¬c = exit n st
1430 find key n@(node key₁ v1 tree tree₁) st next _ | tri&lt; a ¬b ¬c = next tree (n ∷ st) 1434 find key n@(node key₁ v1 tree tree₁) st next _ | tri&lt; a ¬b ¬c = next tree (n ∷ st)
1431 find key n@(node key₁ v1 tree tree₁) st next _ | tri&gt; ¬a ¬b c = next tree₁ (n ∷ st) 1435 find key n@(node key₁ v1 tree tree₁) st next _ | tri&gt; ¬a ¬b c = next tree₁ (n ∷ st)
1432 </span></span></foreignObject></svg></code></pre> 1436 </span></span></foreignObject></svg></code></pre>
1433 </section> 1437 </section>
1434 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="18" data-paginate="true" data-class="slide" data-theme="default" data-style="section { 1438 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="16" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
1435 background-color: #FFFFFF; 1439 background-color: #FFFFFF;
1436 font-size: 28px; 1440 font-size: 28px;
1437 color: #4b4b4b; 1441 color: #4b4b4b;
1438 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 1442 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
1439 background-image: url(&quot;logo.svg&quot;); 1443 background-image: url(&quot;logo.svg&quot;);
1440 background-position: right 3% bottom 2%; 1444 background-position: right 3% bottom 2%;
1441 background-repeat: no-repeat; 1445 background-repeat: no-repeat;
1442 background-attachment: 5%; 1446 background-attachment: 5%;
1443 background-size: 20% auto; 1447 background-size: 20% auto;
1444 } 1448 }
1445 1449
1446 section.title h1 { 1450 section.title h1 {
1447 color: #808db5; 1451 color: #808db5;
1448 text-align: center; 1452 text-align: center;
1449 } 1453 }
1450 1454
1451 section.title p { 1455 section.title p {
1452 bottom: 25%; 1456 bottom: 25%;
1453 width: 100%; 1457 width: 100%;
1454 position: absolute; 1458 position: absolute;
1455 font-size: 25px; 1459 font-size: 25px;
1456 color: #4b4b4b; 1460 color: #4b4b4b;
1457 background: linear-gradient(transparent 90%, #ffcc00 0%); 1461 background: linear-gradient(transparent 90%, #ffcc00 0%);
1458 } 1462 }
1459 1463
1460 section.slide h1 { 1464 section.slide h1 {
1461 width: 95%; 1465 width: 95%;
1462 color: white; 1466 color: white;
1463 background-color: #808db5; 1467 background-color: #808db5;
1464 position: absolute; 1468 position: absolute;
1465 left: 50px; 1469 left: 50px;
1466 top: 35px; 1470 top: 35px;
1467 } 1471 }
1468 " data-heading-divider="1" class="slide" data-marpit-pagination="18" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { 1472
1469 background-color: #FFFFFF; 1473 section.fig_cg p {
1470 font-size: 28px; 1474 top: 300px;
1471 color: #4b4b4b; 1475 text-align: center;
1472 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 1476 }
1473 background-image: url(&quot;logo.svg&quot;); 1477 " data-heading-divider="1" class="slide" data-marpit-pagination="16" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section {
1474 background-position: right 3% bottom 2%; 1478 background-color: #FFFFFF;
1475 background-repeat: no-repeat; 1479 font-size: 28px;
1476 background-attachment: 5%; 1480 color: #4b4b4b;
1477 background-size: 20% auto; 1481 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
1478 } 1482 background-image: url(&quot;logo.svg&quot;);
1479 1483 background-position: right 3% bottom 2%;
1480 section.title h1 { 1484 background-repeat: no-repeat;
1481 color: #808db5; 1485 background-attachment: 5%;
1482 text-align: center; 1486 background-size: 20% auto;
1483 } 1487 }
1484 1488
1485 section.title p { 1489 section.title h1 {
1486 bottom: 25%; 1490 color: #808db5;
1487 width: 100%; 1491 text-align: center;
1488 position: absolute; 1492 }
1489 font-size: 25px; 1493
1490 color: #4b4b4b; 1494 section.title p {
1491 background: linear-gradient(transparent 90%, #ffcc00 0%); 1495 bottom: 25%;
1492 } 1496 width: 100%;
1493 1497 position: absolute;
1494 section.slide h1 { 1498 font-size: 25px;
1495 width: 95%; 1499 color: #4b4b4b;
1496 color: white; 1500 background: linear-gradient(transparent 90%, #ffcc00 0%);
1497 background-color: #808db5; 1501 }
1498 position: absolute; 1502
1499 left: 50px; 1503 section.slide h1 {
1500 top: 35px; 1504 width: 95%;
1505 color: white;
1506 background-color: #808db5;
1507 position: absolute;
1508 left: 50px;
1509 top: 35px;
1510 }
1511
1512 section.fig_cg p {
1513 top: 300px;
1514 text-align: center;
1501 } 1515 }
1502 ;--heading-divider:1;" data-size="16:9"> 1516 ;--heading-divider:1;" data-size="16:9">
1503 <h1>Gears Agda による BinaryTree の実装 replace node</h1> 1517 <h1>Gears Agda による BinaryTree の実装 replace node</h1>
1504 <pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>replace : {n m : Level} {A : Set n} {t : Set m} 1518 <pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>replace : {n m : Level} {A : Set n} {t : Set m}
1505 → (key : N) → (value : A) → bt A → List (bt A) 1519 → (key : N) → (value : A) → bt A → List (bt A)
1516 ... | tri&lt; a ¬b ¬c = next key value (node key₁ value₁ repl right ) st 1530 ... | tri&lt; a ¬b ¬c = next key value (node key₁ value₁ repl right ) st
1517 ... | tri≈ ¬a b ¬c = next key value (node key₁ value left right ) st 1531 ... | tri≈ ¬a b ¬c = next key value (node key₁ value left right ) st
1518 ... | tri&gt; ¬a ¬b c = next key value (node key₁ value₁ left repl ) st 1532 ... | tri&gt; ¬a ¬b c = next key value (node key₁ value₁ left repl ) st
1519 </span></span></foreignObject></svg></code></pre> 1533 </span></span></foreignObject></svg></code></pre>
1520 </section> 1534 </section>
1521 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="19" data-paginate="true" data-class="slide" data-theme="default" data-style="section { 1535 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="17" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
1522 background-color: #FFFFFF; 1536 background-color: #FFFFFF;
1523 font-size: 28px; 1537 font-size: 28px;
1524 color: #4b4b4b; 1538 color: #4b4b4b;
1525 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 1539 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
1526 background-image: url(&quot;logo.svg&quot;); 1540 background-image: url(&quot;logo.svg&quot;);
1527 background-position: right 3% bottom 2%; 1541 background-position: right 3% bottom 2%;
1528 background-repeat: no-repeat; 1542 background-repeat: no-repeat;
1529 background-attachment: 5%; 1543 background-attachment: 5%;
1530 background-size: 20% auto; 1544 background-size: 20% auto;
1531 } 1545 }
1532 1546
1533 section.title h1 { 1547 section.title h1 {
1534 color: #808db5; 1548 color: #808db5;
1535 text-align: center; 1549 text-align: center;
1536 } 1550 }
1537 1551
1538 section.title p { 1552 section.title p {
1539 bottom: 25%; 1553 bottom: 25%;
1540 width: 100%; 1554 width: 100%;
1541 position: absolute; 1555 position: absolute;
1542 font-size: 25px; 1556 font-size: 25px;
1543 color: #4b4b4b; 1557 color: #4b4b4b;
1544 background: linear-gradient(transparent 90%, #ffcc00 0%); 1558 background: linear-gradient(transparent 90%, #ffcc00 0%);
1545 } 1559 }
1546 1560
1547 section.slide h1 { 1561 section.slide h1 {
1548 width: 95%; 1562 width: 95%;
1549 color: white; 1563 color: white;
1550 background-color: #808db5; 1564 background-color: #808db5;
1551 position: absolute; 1565 position: absolute;
1552 left: 50px; 1566 left: 50px;
1553 top: 35px; 1567 top: 35px;
1554 } 1568 }
1555 " data-heading-divider="1" class="slide" data-marpit-pagination="19" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { 1569
1556 background-color: #FFFFFF; 1570 section.fig_cg p {
1557 font-size: 28px; 1571 top: 300px;
1558 color: #4b4b4b; 1572 text-align: center;
1559 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 1573 }
1560 background-image: url(&quot;logo.svg&quot;); 1574 " data-heading-divider="1" class="slide" data-marpit-pagination="17" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section {
1561 background-position: right 3% bottom 2%; 1575 background-color: #FFFFFF;
1562 background-repeat: no-repeat; 1576 font-size: 28px;
1563 background-attachment: 5%; 1577 color: #4b4b4b;
1564 background-size: 20% auto; 1578 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
1565 } 1579 background-image: url(&quot;logo.svg&quot;);
1566 1580 background-position: right 3% bottom 2%;
1567 section.title h1 { 1581 background-repeat: no-repeat;
1568 color: #808db5; 1582 background-attachment: 5%;
1569 text-align: center; 1583 background-size: 20% auto;
1570 } 1584 }
1571 1585
1572 section.title p { 1586 section.title h1 {
1573 bottom: 25%; 1587 color: #808db5;
1574 width: 100%; 1588 text-align: center;
1575 position: absolute; 1589 }
1576 font-size: 25px; 1590
1577 color: #4b4b4b; 1591 section.title p {
1578 background: linear-gradient(transparent 90%, #ffcc00 0%); 1592 bottom: 25%;
1579 } 1593 width: 100%;
1580 1594 position: absolute;
1581 section.slide h1 { 1595 font-size: 25px;
1582 width: 95%; 1596 color: #4b4b4b;
1583 color: white; 1597 background: linear-gradient(transparent 90%, #ffcc00 0%);
1584 background-color: #808db5; 1598 }
1585 position: absolute; 1599
1586 left: 50px; 1600 section.slide h1 {
1587 top: 35px; 1601 width: 95%;
1602 color: white;
1603 background-color: #808db5;
1604 position: absolute;
1605 left: 50px;
1606 top: 35px;
1607 }
1608
1609 section.fig_cg p {
1610 top: 300px;
1611 text-align: center;
1588 } 1612 }
1589 ;--heading-divider:1;" data-size="16:9"> 1613 ;--heading-divider:1;" data-size="16:9">
1590 <h1>Gears Agda による BinaryTree の実装 loop connecter</h1> 1614 <h1>Gears Agda による BinaryTree の実装 loop connecter</h1>
1591 <pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap> 1615 <pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>
1592 </span></span></foreignObject></svg></code></pre> 1616 </span></span></foreignObject></svg></code></pre>
1593 </section> 1617 </section>
1594 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="20" data-paginate="true" data-class="slide" data-theme="default" data-style="section { 1618 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="18" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
1595 background-color: #FFFFFF; 1619 background-color: #FFFFFF;
1596 font-size: 28px; 1620 font-size: 28px;
1597 color: #4b4b4b; 1621 color: #4b4b4b;
1598 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 1622 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
1599 background-image: url(&quot;logo.svg&quot;); 1623 background-image: url(&quot;logo.svg&quot;);
1600 background-position: right 3% bottom 2%; 1624 background-position: right 3% bottom 2%;
1601 background-repeat: no-repeat; 1625 background-repeat: no-repeat;
1602 background-attachment: 5%; 1626 background-attachment: 5%;
1603 background-size: 20% auto; 1627 background-size: 20% auto;
1604 } 1628 }
1605 1629
1606 section.title h1 { 1630 section.title h1 {
1607 color: #808db5; 1631 color: #808db5;
1608 text-align: center; 1632 text-align: center;
1609 } 1633 }
1610 1634
1611 section.title p { 1635 section.title p {
1612 bottom: 25%; 1636 bottom: 25%;
1613 width: 100%; 1637 width: 100%;
1614 position: absolute; 1638 position: absolute;
1615 font-size: 25px; 1639 font-size: 25px;
1616 color: #4b4b4b; 1640 color: #4b4b4b;
1617 background: linear-gradient(transparent 90%, #ffcc00 0%); 1641 background: linear-gradient(transparent 90%, #ffcc00 0%);
1618 } 1642 }
1619 1643
1620 section.slide h1 { 1644 section.slide h1 {
1621 width: 95%; 1645 width: 95%;
1622 color: white; 1646 color: white;
1623 background-color: #808db5; 1647 background-color: #808db5;
1624 position: absolute; 1648 position: absolute;
1625 left: 50px; 1649 left: 50px;
1626 top: 35px; 1650 top: 35px;
1627 } 1651 }
1628 " data-heading-divider="1" class="slide" data-marpit-pagination="20" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { 1652
1629 background-color: #FFFFFF; 1653 section.fig_cg p {
1630 font-size: 28px; 1654 top: 300px;
1631 color: #4b4b4b; 1655 text-align: center;
1632 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 1656 }
1633 background-image: url(&quot;logo.svg&quot;); 1657 " data-heading-divider="1" class="slide" data-marpit-pagination="18" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section {
1634 background-position: right 3% bottom 2%; 1658 background-color: #FFFFFF;
1635 background-repeat: no-repeat; 1659 font-size: 28px;
1636 background-attachment: 5%; 1660 color: #4b4b4b;
1637 background-size: 20% auto; 1661 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
1638 } 1662 background-image: url(&quot;logo.svg&quot;);
1639 1663 background-position: right 3% bottom 2%;
1640 section.title h1 { 1664 background-repeat: no-repeat;
1641 color: #808db5; 1665 background-attachment: 5%;
1642 text-align: center; 1666 background-size: 20% auto;
1643 } 1667 }
1644 1668
1645 section.title p { 1669 section.title h1 {
1646 bottom: 25%; 1670 color: #808db5;
1647 width: 100%; 1671 text-align: center;
1648 position: absolute; 1672 }
1649 font-size: 25px; 1673
1650 color: #4b4b4b; 1674 section.title p {
1651 background: linear-gradient(transparent 90%, #ffcc00 0%); 1675 bottom: 25%;
1652 } 1676 width: 100%;
1653 1677 position: absolute;
1654 section.slide h1 { 1678 font-size: 25px;
1655 width: 95%; 1679 color: #4b4b4b;
1656 color: white; 1680 background: linear-gradient(transparent 90%, #ffcc00 0%);
1657 background-color: #808db5; 1681 }
1658 position: absolute; 1682
1659 left: 50px; 1683 section.slide h1 {
1660 top: 35px; 1684 width: 95%;
1685 color: white;
1686 background-color: #808db5;
1687 position: absolute;
1688 left: 50px;
1689 top: 35px;
1690 }
1691
1692 section.fig_cg p {
1693 top: 300px;
1694 text-align: center;
1661 } 1695 }
1662 ;--heading-divider:1;" data-size="16:9"> 1696 ;--heading-divider:1;" data-size="16:9">
1663 <h1>Gears Agda による Binary Tree の検証 Invariant</h1> 1697 <h1>Gears Agda による Binary Tree の検証 Invariant</h1>
1664 <p>具体的な例を一つ挙げて、Invariantの説明を行う</p> 1698 <p>具体的な例を一つ挙げて、Invariantの説明を行う</p>
1665 <ul> 1699 <ul>
1667 右の子のkeyは親より大きいことを検証</li> 1701 右の子のkeyは親より大きいことを検証</li>
1668 <li>Stack に格納されているTreeはその次のStackの減少列になっているか</li> 1702 <li>Stack に格納されているTreeはその次のStackの減少列になっているか</li>
1669 <li>Tree を正しく入れ替えられているか</li> 1703 <li>Tree を正しく入れ替えられているか</li>
1670 </ul> 1704 </ul>
1671 </section> 1705 </section>
1672 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="21" data-paginate="true" data-class="slide" data-theme="default" data-style="section { 1706 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="19" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
1673 background-color: #FFFFFF; 1707 background-color: #FFFFFF;
1674 font-size: 28px; 1708 font-size: 28px;
1675 color: #4b4b4b; 1709 color: #4b4b4b;
1676 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 1710 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
1677 background-image: url(&quot;logo.svg&quot;); 1711 background-image: url(&quot;logo.svg&quot;);
1678 background-position: right 3% bottom 2%; 1712 background-position: right 3% bottom 2%;
1679 background-repeat: no-repeat; 1713 background-repeat: no-repeat;
1680 background-attachment: 5%; 1714 background-attachment: 5%;
1681 background-size: 20% auto; 1715 background-size: 20% auto;
1682 } 1716 }
1683 1717
1684 section.title h1 { 1718 section.title h1 {
1685 color: #808db5; 1719 color: #808db5;
1686 text-align: center; 1720 text-align: center;
1687 } 1721 }
1688 1722
1689 section.title p { 1723 section.title p {
1690 bottom: 25%; 1724 bottom: 25%;
1691 width: 100%; 1725 width: 100%;
1692 position: absolute; 1726 position: absolute;
1693 font-size: 25px; 1727 font-size: 25px;
1694 color: #4b4b4b; 1728 color: #4b4b4b;
1695 background: linear-gradient(transparent 90%, #ffcc00 0%); 1729 background: linear-gradient(transparent 90%, #ffcc00 0%);
1696 } 1730 }
1697 1731
1698 section.slide h1 { 1732 section.slide h1 {
1699 width: 95%; 1733 width: 95%;
1700 color: white; 1734 color: white;
1701 background-color: #808db5; 1735 background-color: #808db5;
1702 position: absolute; 1736 position: absolute;
1703 left: 50px; 1737 left: 50px;
1704 top: 35px; 1738 top: 35px;
1705 } 1739 }
1706 " data-heading-divider="1" class="slide" data-marpit-pagination="21" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { 1740
1707 background-color: #FFFFFF; 1741 section.fig_cg p {
1708 font-size: 28px; 1742 top: 300px;
1709 color: #4b4b4b; 1743 text-align: center;
1710 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 1744 }
1711 background-image: url(&quot;logo.svg&quot;); 1745 " data-heading-divider="1" class="slide" data-marpit-pagination="19" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section {
1712 background-position: right 3% bottom 2%; 1746 background-color: #FFFFFF;
1713 background-repeat: no-repeat; 1747 font-size: 28px;
1714 background-attachment: 5%; 1748 color: #4b4b4b;
1715 background-size: 20% auto; 1749 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
1716 } 1750 background-image: url(&quot;logo.svg&quot;);
1717 1751 background-position: right 3% bottom 2%;
1718 section.title h1 { 1752 background-repeat: no-repeat;
1719 color: #808db5; 1753 background-attachment: 5%;
1720 text-align: center; 1754 background-size: 20% auto;
1721 } 1755 }
1722 1756
1723 section.title p { 1757 section.title h1 {
1724 bottom: 25%; 1758 color: #808db5;
1725 width: 100%; 1759 text-align: center;
1726 position: absolute; 1760 }
1727 font-size: 25px; 1761
1728 color: #4b4b4b; 1762 section.title p {
1729 background: linear-gradient(transparent 90%, #ffcc00 0%); 1763 bottom: 25%;
1730 } 1764 width: 100%;
1731 1765 position: absolute;
1732 section.slide h1 { 1766 font-size: 25px;
1733 width: 95%; 1767 color: #4b4b4b;
1734 color: white; 1768 background: linear-gradient(transparent 90%, #ffcc00 0%);
1735 background-color: #808db5; 1769 }
1736 position: absolute; 1770
1737 left: 50px; 1771 section.slide h1 {
1738 top: 35px; 1772 width: 95%;
1773 color: white;
1774 background-color: #808db5;
1775 position: absolute;
1776 left: 50px;
1777 top: 35px;
1778 }
1779
1780 section.fig_cg p {
1781 top: 300px;
1782 text-align: center;
1739 } 1783 }
1740 ;--heading-divider:1;" data-size="16:9"> 1784 ;--heading-divider:1;" data-size="16:9">
1741 <h1>Gears Agda による Binary Tree の検証 Invariant</h1> 1785 <h1>Gears Agda による Binary Tree の検証 Invariant</h1>
1742 <ul> 1786 <ul>
1743 <li>Tree Invariant</li> 1787 <li>Tree Invariant</li>
1756 → treeInvariant (node key value t₁ t₂) 1800 → treeInvariant (node key value t₁ t₂)
1757 → treeInvariant (node key₂ value₂ t₃ t₄) 1801 → treeInvariant (node key₂ value₂ t₃ t₄)
1758 → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄)) 1802 → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄))
1759 </span></span></foreignObject></svg></code></pre> 1803 </span></span></foreignObject></svg></code></pre>
1760 </section> 1804 </section>
1761 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="22" data-paginate="true" data-class="slide" data-theme="default" data-style="section { 1805 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="20" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
1762 background-color: #FFFFFF; 1806 background-color: #FFFFFF;
1763 font-size: 28px; 1807 font-size: 28px;
1764 color: #4b4b4b; 1808 color: #4b4b4b;
1765 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 1809 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
1766 background-image: url(&quot;logo.svg&quot;); 1810 background-image: url(&quot;logo.svg&quot;);
1767 background-position: right 3% bottom 2%; 1811 background-position: right 3% bottom 2%;
1768 background-repeat: no-repeat; 1812 background-repeat: no-repeat;
1769 background-attachment: 5%; 1813 background-attachment: 5%;
1770 background-size: 20% auto; 1814 background-size: 20% auto;
1771 } 1815 }
1772 1816
1773 section.title h1 { 1817 section.title h1 {
1774 color: #808db5; 1818 color: #808db5;
1775 text-align: center; 1819 text-align: center;
1776 } 1820 }
1777 1821
1778 section.title p { 1822 section.title p {
1779 bottom: 25%; 1823 bottom: 25%;
1780 width: 100%; 1824 width: 100%;
1781 position: absolute; 1825 position: absolute;
1782 font-size: 25px; 1826 font-size: 25px;
1783 color: #4b4b4b; 1827 color: #4b4b4b;
1784 background: linear-gradient(transparent 90%, #ffcc00 0%); 1828 background: linear-gradient(transparent 90%, #ffcc00 0%);
1785 } 1829 }
1786 1830
1787 section.slide h1 { 1831 section.slide h1 {
1788 width: 95%; 1832 width: 95%;
1789 color: white; 1833 color: white;
1790 background-color: #808db5; 1834 background-color: #808db5;
1791 position: absolute; 1835 position: absolute;
1792 left: 50px; 1836 left: 50px;
1793 top: 35px; 1837 top: 35px;
1794 } 1838 }
1795 " data-heading-divider="1" class="slide" data-marpit-pagination="22" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { 1839
1796 background-color: #FFFFFF; 1840 section.fig_cg p {
1797 font-size: 28px; 1841 top: 300px;
1798 color: #4b4b4b; 1842 text-align: center;
1799 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 1843 }
1800 background-image: url(&quot;logo.svg&quot;); 1844 " data-heading-divider="1" class="slide" data-marpit-pagination="20" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section {
1801 background-position: right 3% bottom 2%; 1845 background-color: #FFFFFF;
1802 background-repeat: no-repeat; 1846 font-size: 28px;
1803 background-attachment: 5%; 1847 color: #4b4b4b;
1804 background-size: 20% auto; 1848 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
1805 } 1849 background-image: url(&quot;logo.svg&quot;);
1806 1850 background-position: right 3% bottom 2%;
1807 section.title h1 { 1851 background-repeat: no-repeat;
1808 color: #808db5; 1852 background-attachment: 5%;
1809 text-align: center; 1853 background-size: 20% auto;
1810 } 1854 }
1811 1855
1812 section.title p { 1856 section.title h1 {
1813 bottom: 25%; 1857 color: #808db5;
1814 width: 100%; 1858 text-align: center;
1815 position: absolute; 1859 }
1816 font-size: 25px; 1860
1817 color: #4b4b4b; 1861 section.title p {
1818 background: linear-gradient(transparent 90%, #ffcc00 0%); 1862 bottom: 25%;
1819 } 1863 width: 100%;
1820 1864 position: absolute;
1821 section.slide h1 { 1865 font-size: 25px;
1822 width: 95%; 1866 color: #4b4b4b;
1823 color: white; 1867 background: linear-gradient(transparent 90%, #ffcc00 0%);
1824 background-color: #808db5; 1868 }
1825 position: absolute; 1869
1826 left: 50px; 1870 section.slide h1 {
1827 top: 35px; 1871 width: 95%;
1872 color: white;
1873 background-color: #808db5;
1874 position: absolute;
1875 left: 50px;
1876 top: 35px;
1877 }
1878
1879 section.fig_cg p {
1880 top: 300px;
1881 text-align: center;
1828 } 1882 }
1829 ;--heading-divider:1;" data-size="16:9"> 1883 ;--heading-divider:1;" data-size="16:9">
1830 <h1>Gears Agda による Binary Tree の検証 Invariant</h1> 1884 <h1>Gears Agda による Binary Tree の検証 Invariant</h1>
1831 <ul> 1885 <ul>
1832 <li>Stack Invariant</li> 1886 <li>Stack Invariant</li>
1840 s-left : {tree₁ tree0 tree : bt A} → {key₁ : N } → {v1 : A } → {st : List (bt A)} 1894 s-left : {tree₁ tree0 tree : bt A} → {key₁ : N } → {v1 : A } → {st : List (bt A)}
1841 → key &lt; key₁ → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st 1895 → key &lt; key₁ → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st
1842 → stackInvariant key tree₁ tree0 (tree₁ ∷ st) 1896 → stackInvariant key tree₁ tree0 (tree₁ ∷ st)
1843 </span></span></foreignObject></svg></code></pre> 1897 </span></span></foreignObject></svg></code></pre>
1844 </section> 1898 </section>
1845 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="23" data-paginate="true" data-class="slide" data-theme="default" data-style="section { 1899 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="21" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
1846 background-color: #FFFFFF; 1900 background-color: #FFFFFF;
1847 font-size: 28px; 1901 font-size: 28px;
1848 color: #4b4b4b; 1902 color: #4b4b4b;
1849 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 1903 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
1850 background-image: url(&quot;logo.svg&quot;); 1904 background-image: url(&quot;logo.svg&quot;);
1851 background-position: right 3% bottom 2%; 1905 background-position: right 3% bottom 2%;
1852 background-repeat: no-repeat; 1906 background-repeat: no-repeat;
1853 background-attachment: 5%; 1907 background-attachment: 5%;
1854 background-size: 20% auto; 1908 background-size: 20% auto;
1855 } 1909 }
1856 1910
1857 section.title h1 { 1911 section.title h1 {
1858 color: #808db5; 1912 color: #808db5;
1859 text-align: center; 1913 text-align: center;
1860 } 1914 }
1861 1915
1862 section.title p { 1916 section.title p {
1863 bottom: 25%; 1917 bottom: 25%;
1864 width: 100%; 1918 width: 100%;
1865 position: absolute; 1919 position: absolute;
1866 font-size: 25px; 1920 font-size: 25px;
1867 color: #4b4b4b; 1921 color: #4b4b4b;
1868 background: linear-gradient(transparent 90%, #ffcc00 0%); 1922 background: linear-gradient(transparent 90%, #ffcc00 0%);
1869 } 1923 }
1870 1924
1871 section.slide h1 { 1925 section.slide h1 {
1872 width: 95%; 1926 width: 95%;
1873 color: white; 1927 color: white;
1874 background-color: #808db5; 1928 background-color: #808db5;
1875 position: absolute; 1929 position: absolute;
1876 left: 50px; 1930 left: 50px;
1877 top: 35px; 1931 top: 35px;
1878 } 1932 }
1879 " data-heading-divider="1" class="slide" data-marpit-pagination="23" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { 1933
1880 background-color: #FFFFFF; 1934 section.fig_cg p {
1881 font-size: 28px; 1935 top: 300px;
1882 color: #4b4b4b; 1936 text-align: center;
1883 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 1937 }
1884 background-image: url(&quot;logo.svg&quot;); 1938 " data-heading-divider="1" class="slide" data-marpit-pagination="21" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section {
1885 background-position: right 3% bottom 2%; 1939 background-color: #FFFFFF;
1886 background-repeat: no-repeat; 1940 font-size: 28px;
1887 background-attachment: 5%; 1941 color: #4b4b4b;
1888 background-size: 20% auto; 1942 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
1889 } 1943 background-image: url(&quot;logo.svg&quot;);
1890 1944 background-position: right 3% bottom 2%;
1891 section.title h1 { 1945 background-repeat: no-repeat;
1892 color: #808db5; 1946 background-attachment: 5%;
1893 text-align: center; 1947 background-size: 20% auto;
1894 } 1948 }
1895 1949
1896 section.title p { 1950 section.title h1 {
1897 bottom: 25%; 1951 color: #808db5;
1898 width: 100%; 1952 text-align: center;
1899 position: absolute; 1953 }
1900 font-size: 25px; 1954
1901 color: #4b4b4b; 1955 section.title p {
1902 background: linear-gradient(transparent 90%, #ffcc00 0%); 1956 bottom: 25%;
1903 } 1957 width: 100%;
1904 1958 position: absolute;
1905 section.slide h1 { 1959 font-size: 25px;
1906 width: 95%; 1960 color: #4b4b4b;
1907 color: white; 1961 background: linear-gradient(transparent 90%, #ffcc00 0%);
1908 background-color: #808db5; 1962 }
1909 position: absolute; 1963
1910 left: 50px; 1964 section.slide h1 {
1911 top: 35px; 1965 width: 95%;
1966 color: white;
1967 background-color: #808db5;
1968 position: absolute;
1969 left: 50px;
1970 top: 35px;
1971 }
1972
1973 section.fig_cg p {
1974 top: 300px;
1975 text-align: center;
1912 } 1976 }
1913 ;--heading-divider:1;" data-size="16:9"> 1977 ;--heading-divider:1;" data-size="16:9">
1914 <h1>Gears Agda による Binary Tree の検証 Invariant</h1> 1978 <h1>Gears Agda による Binary Tree の検証 Invariant</h1>
1915 <ul> 1979 <ul>
1916 <li>Replace Invariant</li> 1980 <li>Replace Invariant</li>
1925 r-left : {k : N } {v1 : A} → {t t1 t2 : bt A} 1989 r-left : {k : N } {v1 : A} → {t t1 t2 : bt A}
1926 → key &lt; k → replacedTree key value t1 t 1990 → key &lt; k → replacedTree key value t1 t
1927 → replacedTree key value (node k v1 t1 t2) (node k v1 t t2) 1991 → replacedTree key value (node k v1 t1 t2) (node k v1 t t2)
1928 </span></span></foreignObject></svg></code></pre> 1992 </span></span></foreignObject></svg></code></pre>
1929 </section> 1993 </section>
1930 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="24" data-paginate="true" data-class="slide" data-theme="default" data-style="section { 1994 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="22" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
1931 background-color: #FFFFFF; 1995 background-color: #FFFFFF;
1932 font-size: 28px; 1996 font-size: 28px;
1933 color: #4b4b4b; 1997 color: #4b4b4b;
1934 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 1998 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
1935 background-image: url(&quot;logo.svg&quot;); 1999 background-image: url(&quot;logo.svg&quot;);
1936 background-position: right 3% bottom 2%; 2000 background-position: right 3% bottom 2%;
1937 background-repeat: no-repeat; 2001 background-repeat: no-repeat;
1938 background-attachment: 5%; 2002 background-attachment: 5%;
1939 background-size: 20% auto; 2003 background-size: 20% auto;
1940 } 2004 }
1941 2005
1942 section.title h1 { 2006 section.title h1 {
1943 color: #808db5; 2007 color: #808db5;
1944 text-align: center; 2008 text-align: center;
1945 } 2009 }
1946 2010
1947 section.title p { 2011 section.title p {
1948 bottom: 25%; 2012 bottom: 25%;
1949 width: 100%; 2013 width: 100%;
1950 position: absolute; 2014 position: absolute;
1951 font-size: 25px; 2015 font-size: 25px;
1952 color: #4b4b4b; 2016 color: #4b4b4b;
1953 background: linear-gradient(transparent 90%, #ffcc00 0%); 2017 background: linear-gradient(transparent 90%, #ffcc00 0%);
1954 } 2018 }
1955 2019
1956 section.slide h1 { 2020 section.slide h1 {
1957 width: 95%; 2021 width: 95%;
1958 color: white; 2022 color: white;
1959 background-color: #808db5; 2023 background-color: #808db5;
1960 position: absolute; 2024 position: absolute;
1961 left: 50px; 2025 left: 50px;
1962 top: 35px; 2026 top: 35px;
1963 } 2027 }
1964 " data-heading-divider="1" class="slide" data-marpit-pagination="24" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { 2028
1965 background-color: #FFFFFF; 2029 section.fig_cg p {
1966 font-size: 28px; 2030 top: 300px;
1967 color: #4b4b4b; 2031 text-align: center;
1968 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 2032 }
1969 background-image: url(&quot;logo.svg&quot;); 2033 " data-heading-divider="1" class="slide" data-marpit-pagination="22" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section {
1970 background-position: right 3% bottom 2%; 2034 background-color: #FFFFFF;
1971 background-repeat: no-repeat; 2035 font-size: 28px;
1972 background-attachment: 5%; 2036 color: #4b4b4b;
1973 background-size: 20% auto; 2037 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
1974 } 2038 background-image: url(&quot;logo.svg&quot;);
1975 2039 background-position: right 3% bottom 2%;
1976 section.title h1 { 2040 background-repeat: no-repeat;
1977 color: #808db5; 2041 background-attachment: 5%;
1978 text-align: center; 2042 background-size: 20% auto;
1979 } 2043 }
1980 2044
1981 section.title p { 2045 section.title h1 {
1982 bottom: 25%; 2046 color: #808db5;
1983 width: 100%; 2047 text-align: center;
1984 position: absolute; 2048 }
1985 font-size: 25px; 2049
1986 color: #4b4b4b; 2050 section.title p {
1987 background: linear-gradient(transparent 90%, #ffcc00 0%); 2051 bottom: 25%;
1988 } 2052 width: 100%;
1989 2053 position: absolute;
1990 section.slide h1 { 2054 font-size: 25px;
1991 width: 95%; 2055 color: #4b4b4b;
1992 color: white; 2056 background: linear-gradient(transparent 90%, #ffcc00 0%);
1993 background-color: #808db5; 2057 }
1994 position: absolute; 2058
1995 left: 50px; 2059 section.slide h1 {
1996 top: 35px; 2060 width: 95%;
2061 color: white;
2062 background-color: #808db5;
2063 position: absolute;
2064 left: 50px;
2065 top: 35px;
2066 }
2067
2068 section.fig_cg p {
2069 top: 300px;
2070 text-align: center;
1997 } 2071 }
1998 ;--heading-divider:1;" data-size="16:9"> 2072 ;--heading-divider:1;" data-size="16:9">
1999 <h1>Gears Agda による Binary Tree の検証</h1> 2073 <h1>Gears Agda による Binary Tree の検証</h1>
2000 <p>Binary Tree の実装に対して上述した3つのInvariantを<br /> 2074 <p>Binary Tree の実装に対して上述した3つのInvariantを<br />
2001 Meta Data Gear として渡しながら実行できるように記述する</p> 2075 Meta Data Gear として渡しながら実行できるように記述する</p>
2002 <pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>findP : {n m : Level} {A : Set n} {t : Set m} → (env : Env A) 2076 <pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>findP : {n m : Level} {A : Set n} {t : Set m} → (env : Env A)
2003 → treeInvariant env ∧ stackInvariant env 2077 → treeInvariant env ∧ stackInvariant env
2004 → (exit : (env : Env A) → treeInvariant env ∧ stackInvariant env → t ) → t 2078 → (exit : (env : Env A) → treeInvariant env ∧ stackInvariant env → t ) → t
2005 </span></span></foreignObject></svg></code></pre> 2079 </span></span></foreignObject></svg></code></pre>
2006 </section> 2080 </section>
2007 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="25" data-paginate="true" data-class="slide" data-theme="default" data-style="section { 2081 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="23" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
2008 background-color: #FFFFFF; 2082 background-color: #FFFFFF;
2009 font-size: 28px; 2083 font-size: 28px;
2010 color: #4b4b4b; 2084 color: #4b4b4b;
2011 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 2085 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
2012 background-image: url(&quot;logo.svg&quot;); 2086 background-image: url(&quot;logo.svg&quot;);
2013 background-position: right 3% bottom 2%; 2087 background-position: right 3% bottom 2%;
2014 background-repeat: no-repeat; 2088 background-repeat: no-repeat;
2015 background-attachment: 5%; 2089 background-attachment: 5%;
2016 background-size: 20% auto; 2090 background-size: 20% auto;
2017 } 2091 }
2018 2092
2019 section.title h1 { 2093 section.title h1 {
2020 color: #808db5; 2094 color: #808db5;
2021 text-align: center; 2095 text-align: center;
2022 } 2096 }
2023 2097
2024 section.title p { 2098 section.title p {
2025 bottom: 25%; 2099 bottom: 25%;
2026 width: 100%; 2100 width: 100%;
2027 position: absolute; 2101 position: absolute;
2028 font-size: 25px; 2102 font-size: 25px;
2029 color: #4b4b4b; 2103 color: #4b4b4b;
2030 background: linear-gradient(transparent 90%, #ffcc00 0%); 2104 background: linear-gradient(transparent 90%, #ffcc00 0%);
2031 } 2105 }
2032 2106
2033 section.slide h1 { 2107 section.slide h1 {
2034 width: 95%; 2108 width: 95%;
2035 color: white; 2109 color: white;
2036 background-color: #808db5; 2110 background-color: #808db5;
2037 position: absolute; 2111 position: absolute;
2038 left: 50px; 2112 left: 50px;
2039 top: 35px; 2113 top: 35px;
2040 } 2114 }
2041 " data-heading-divider="1" class="slide" data-marpit-pagination="25" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { 2115
2042 background-color: #FFFFFF; 2116 section.fig_cg p {
2043 font-size: 28px; 2117 top: 300px;
2044 color: #4b4b4b; 2118 text-align: center;
2045 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 2119 }
2046 background-image: url(&quot;logo.svg&quot;); 2120 " data-heading-divider="1" class="slide" data-marpit-pagination="23" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section {
2047 background-position: right 3% bottom 2%; 2121 background-color: #FFFFFF;
2048 background-repeat: no-repeat; 2122 font-size: 28px;
2049 background-attachment: 5%; 2123 color: #4b4b4b;
2050 background-size: 20% auto; 2124 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
2051 } 2125 background-image: url(&quot;logo.svg&quot;);
2052 2126 background-position: right 3% bottom 2%;
2053 section.title h1 { 2127 background-repeat: no-repeat;
2054 color: #808db5; 2128 background-attachment: 5%;
2055 text-align: center; 2129 background-size: 20% auto;
2056 } 2130 }
2057 2131
2058 section.title p { 2132 section.title h1 {
2059 bottom: 25%; 2133 color: #808db5;
2060 width: 100%; 2134 text-align: center;
2061 position: absolute; 2135 }
2062 font-size: 25px; 2136
2063 color: #4b4b4b; 2137 section.title p {
2064 background: linear-gradient(transparent 90%, #ffcc00 0%); 2138 bottom: 25%;
2065 } 2139 width: 100%;
2066 2140 position: absolute;
2067 section.slide h1 { 2141 font-size: 25px;
2068 width: 95%; 2142 color: #4b4b4b;
2069 color: white; 2143 background: linear-gradient(transparent 90%, #ffcc00 0%);
2070 background-color: #808db5; 2144 }
2071 position: absolute; 2145
2072 left: 50px; 2146 section.slide h1 {
2073 top: 35px; 2147 width: 95%;
2148 color: white;
2149 background-color: #808db5;
2150 position: absolute;
2151 left: 50px;
2152 top: 35px;
2153 }
2154
2155 section.fig_cg p {
2156 top: 300px;
2157 text-align: center;
2074 } 2158 }
2075 ;--heading-divider:1;" data-size="16:9"> 2159 ;--heading-divider:1;" data-size="16:9">
2076 <h1>今後の研究方針</h1> 2160 <h1>今後の研究方針</h1>
2077 <ul> 2161 <ul>
2078 <li>現在は Binary Tree の検証までしか行えていないが、<br /> 2162 <li>現在は Binary Tree の検証までしか行えていないが、<br />
2079 今回定義した条件はそのまま Red Black Tree の検証に使用できるはず</li> 2163 今回定義した条件はそのまま Red Black Tree の検証に使用できるはず</li>
2080 <li>今後は Gears Agda による実装と条件の追加をおこなう</li> 2164 <li>今後は Gears Agda による実装と条件の追加をおこなう</li>
2081 <li>モデル検査</li> 2165 <li>モデル検査</li>
2082 </ul> 2166 </ul>
2083 </section> 2167 </section>
2084 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="26" data-paginate="true" data-class="slide" data-theme="default" data-style="section { 2168 </foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="24" data-paginate="true" data-class="slide" data-theme="default" data-style="section {
2085 background-color: #FFFFFF; 2169 background-color: #FFFFFF;
2086 font-size: 28px; 2170 font-size: 28px;
2087 color: #4b4b4b; 2171 color: #4b4b4b;
2088 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 2172 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
2089 background-image: url(&quot;logo.svg&quot;); 2173 background-image: url(&quot;logo.svg&quot;);
2090 background-position: right 3% bottom 2%; 2174 background-position: right 3% bottom 2%;
2091 background-repeat: no-repeat; 2175 background-repeat: no-repeat;
2092 background-attachment: 5%; 2176 background-attachment: 5%;
2093 background-size: 20% auto; 2177 background-size: 20% auto;
2094 } 2178 }
2095 2179
2096 section.title h1 { 2180 section.title h1 {
2097 color: #808db5; 2181 color: #808db5;
2098 text-align: center; 2182 text-align: center;
2099 } 2183 }
2100 2184
2101 section.title p { 2185 section.title p {
2102 bottom: 25%; 2186 bottom: 25%;
2103 width: 100%; 2187 width: 100%;
2104 position: absolute; 2188 position: absolute;
2105 font-size: 25px; 2189 font-size: 25px;
2106 color: #4b4b4b; 2190 color: #4b4b4b;
2107 background: linear-gradient(transparent 90%, #ffcc00 0%); 2191 background: linear-gradient(transparent 90%, #ffcc00 0%);
2108 } 2192 }
2109 2193
2110 section.slide h1 { 2194 section.slide h1 {
2111 width: 95%; 2195 width: 95%;
2112 color: white; 2196 color: white;
2113 background-color: #808db5; 2197 background-color: #808db5;
2114 position: absolute; 2198 position: absolute;
2115 left: 50px; 2199 left: 50px;
2116 top: 35px; 2200 top: 35px;
2117 } 2201 }
2118 " data-heading-divider="1" class="slide" data-marpit-pagination="26" data-marpit-pagination-total="26" style="--paginate:true;--class:slide;--theme:default;--style:section { 2202
2119 background-color: #FFFFFF; 2203 section.fig_cg p {
2120 font-size: 28px; 2204 top: 300px;
2121 color: #4b4b4b; 2205 text-align: center;
2122 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;; 2206 }
2123 background-image: url(&quot;logo.svg&quot;); 2207 " data-heading-divider="1" class="slide" data-marpit-pagination="24" data-marpit-pagination-total="24" style="--paginate:true;--class:slide;--theme:default;--style:section {
2124 background-position: right 3% bottom 2%; 2208 background-color: #FFFFFF;
2125 background-repeat: no-repeat; 2209 font-size: 28px;
2126 background-attachment: 5%; 2210 color: #4b4b4b;
2127 background-size: 20% auto; 2211 font-family: &quot;Droid Sans Mono&quot;, &quot;Hiragino Maru Gothic ProN&quot;;
2128 } 2212 background-image: url(&quot;logo.svg&quot;);
2129 2213 background-position: right 3% bottom 2%;
2130 section.title h1 { 2214 background-repeat: no-repeat;
2131 color: #808db5; 2215 background-attachment: 5%;
2132 text-align: center; 2216 background-size: 20% auto;
2133 } 2217 }
2134 2218
2135 section.title p { 2219 section.title h1 {
2136 bottom: 25%; 2220 color: #808db5;
2137 width: 100%; 2221 text-align: center;
2138 position: absolute; 2222 }
2139 font-size: 25px; 2223
2140 color: #4b4b4b; 2224 section.title p {
2141 background: linear-gradient(transparent 90%, #ffcc00 0%); 2225 bottom: 25%;
2142 } 2226 width: 100%;
2143 2227 position: absolute;
2144 section.slide h1 { 2228 font-size: 25px;
2145 width: 95%; 2229 color: #4b4b4b;
2146 color: white; 2230 background: linear-gradient(transparent 90%, #ffcc00 0%);
2147 background-color: #808db5; 2231 }
2148 position: absolute; 2232
2149 left: 50px; 2233 section.slide h1 {
2150 top: 35px; 2234 width: 95%;
2235 color: white;
2236 background-color: #808db5;
2237 position: absolute;
2238 left: 50px;
2239 top: 35px;
2240 }
2241
2242 section.fig_cg p {
2243 top: 300px;
2244 text-align: center;
2151 } 2245 }
2152 ;--heading-divider:1;" data-size="16:9"> 2246 ;--heading-divider:1;" data-size="16:9">
2153 <h1>まとめ</h1> 2247 <h1>まとめ</h1>
2154 <ul> 2248 <ul>
2155 <li>Gears Agda にて Binary Tree を検証することができた 2249 <li>Gears Agda にて Binary Tree を検証することができた
2163 </ul> 2257 </ul>
2164 <p>英語版も欲しい</p> 2258 <p>英語版も欲しい</p>
2165 <p>condition を テンプレみたいに作ってかきやすくする話</p> 2259 <p>condition を テンプレみたいに作ってかきやすくする話</p>
2166 </section> 2260 </section>
2167 <script>!function(){"use strict";const t="marpitSVGPolyfill:setZoomFactor,",e=Symbol();let r,o;function n(n){const i="object"==typeof n&&n.target||document,a="object"==typeof n?n.zoom:n;window[e]||(Object.defineProperty(window,e,{configurable:!0,value:!0}),window.addEventListener("message",(({data:e,origin:r})=>{if(r===window.origin)try{if(e&&"string"==typeof e&&e.startsWith(t)){const[,t]=e.split(","),r=Number.parseFloat(t);Number.isNaN(r)||(o=r)}}catch(t){console.error(t)}})));let l=!1;Array.from(i.querySelectorAll("svg[data-marpit-svg]"),(t=>{var e,n,i,s;t.style.transform||(t.style.transform="translateZ(0)");const c=a||o||t.currentScale||1;r!==c&&(r=c,l=c);const d=t.getBoundingClientRect(),{length:u}=t.children;for(let r=0;r<u;r+=1){const o=t.children[r],a=o.getScreenCTM();if(a){const t=null!==(n=null===(e=o.x)||void 0===e?void 0:e.baseVal.value)&&void 0!==n?n:0,r=null!==(s=null===(i=o.y)||void 0===i?void 0:i.baseVal.value)&&void 0!==s?s:0,l=o.firstElementChild,{style:u}=l;u.transformOrigin||(u.transformOrigin=`${-t}px ${-r}px`),u.transform=`scale(${c}) matrix(${a.a}, ${a.b}, ${a.c}, ${a.d}, ${a.e-d.left}, ${a.f-d.top}) translateZ(0.0001px)`}}})),!1!==l&&Array.from(i.querySelectorAll("iframe"),(({contentWindow:e})=>{null==e||e.postMessage(`${t}${l}`,"null"===window.origin?"*":window.origin)}))}r=1,o=void 0;const i=(t,e,r)=>{if(t.getAttribute(e)!==r)return t.setAttribute(e,r),!0};function a({once:t=!1,target:e=document}={}){const r="Apple Computer, Inc."===navigator.vendor?[n]:[];let o=!t;const a=()=>{for(const t of r)t({target:e});!function(t=document){Array.from(t.querySelectorAll('svg[data-marp-fitting="svg"]'),(t=>{var e;const r=t.firstChild,o=r.firstChild,{scrollWidth:n,scrollHeight:a}=o;let l,s=1;if(t.hasAttribute("data-marp-fitting-code")&&(l=null===(e=t.parentElement)||void 0===e?void 0:e.parentElement),t.hasAttribute("data-marp-fitting-math")&&(l=t.parentElement),l){const t=getComputedStyle(l),e=Math.ceil(l.clientWidth-parseFloat(t.paddingLeft||"0")-parseFloat(t.paddingRight||"0"));e&&(s=e)}const c=Math.max(n,s),d=Math.max(a,1),u=`0 0 ${c} ${d}`;i(r,"width",`${c}`),i(r,"height",`${d}`),i(t,"preserveAspectRatio",getComputedStyle(t).getPropertyValue("--preserve-aspect-ratio")||"xMinYMin meet"),i(t,"viewBox",u)&&t.classList.toggle("__reflow__")}))}(e),o&&window.requestAnimationFrame(a)};return a(),()=>{o=!1}}const l=Symbol(),s=document.currentScript;((t=document)=>{if("undefined"==typeof window)throw new Error("Marp Core's browser script is valid only in browser context.");if(t[l])return t[l];const e=a({target:t}),r=()=>{e(),delete t[l]};Object.defineProperty(t,l,{configurable:!0,value:r})})(s?s.getRootNode():document)}(); 2261 <script>!function(){"use strict";const t="marpitSVGPolyfill:setZoomFactor,",e=Symbol();let r,o;function n(n){const i="object"==typeof n&&n.target||document,a="object"==typeof n?n.zoom:n;window[e]||(Object.defineProperty(window,e,{configurable:!0,value:!0}),window.addEventListener("message",(({data:e,origin:r})=>{if(r===window.origin)try{if(e&&"string"==typeof e&&e.startsWith(t)){const[,t]=e.split(","),r=Number.parseFloat(t);Number.isNaN(r)||(o=r)}}catch(t){console.error(t)}})));let l=!1;Array.from(i.querySelectorAll("svg[data-marpit-svg]"),(t=>{var e,n,i,s;t.style.transform||(t.style.transform="translateZ(0)");const c=a||o||t.currentScale||1;r!==c&&(r=c,l=c);const d=t.getBoundingClientRect(),{length:u}=t.children;for(let r=0;r<u;r+=1){const o=t.children[r],a=o.getScreenCTM();if(a){const t=null!==(n=null===(e=o.x)||void 0===e?void 0:e.baseVal.value)&&void 0!==n?n:0,r=null!==(s=null===(i=o.y)||void 0===i?void 0:i.baseVal.value)&&void 0!==s?s:0,l=o.firstElementChild,{style:u}=l;u.transformOrigin||(u.transformOrigin=`${-t}px ${-r}px`),u.transform=`scale(${c}) matrix(${a.a}, ${a.b}, ${a.c}, ${a.d}, ${a.e-d.left}, ${a.f-d.top}) translateZ(0.0001px)`}}})),!1!==l&&Array.from(i.querySelectorAll("iframe"),(({contentWindow:e})=>{null==e||e.postMessage(`${t}${l}`,"null"===window.origin?"*":window.origin)}))}r=1,o=void 0;const i=(t,e,r)=>{if(t.getAttribute(e)!==r)return t.setAttribute(e,r),!0};function a({once:t=!1,target:e=document}={}){const r="Apple Computer, Inc."===navigator.vendor?[n]:[];let o=!t;const a=()=>{for(const t of r)t({target:e});!function(t=document){Array.from(t.querySelectorAll('svg[data-marp-fitting="svg"]'),(t=>{var e;const r=t.firstChild,o=r.firstChild,{scrollWidth:n,scrollHeight:a}=o;let l,s=1;if(t.hasAttribute("data-marp-fitting-code")&&(l=null===(e=t.parentElement)||void 0===e?void 0:e.parentElement),t.hasAttribute("data-marp-fitting-math")&&(l=t.parentElement),l){const t=getComputedStyle(l),e=Math.ceil(l.clientWidth-parseFloat(t.paddingLeft||"0")-parseFloat(t.paddingRight||"0"));e&&(s=e)}const c=Math.max(n,s),d=Math.max(a,1),u=`0 0 ${c} ${d}`;i(r,"width",`${c}`),i(r,"height",`${d}`),i(t,"preserveAspectRatio",getComputedStyle(t).getPropertyValue("--preserve-aspect-ratio")||"xMinYMin meet"),i(t,"viewBox",u)&&t.classList.toggle("__reflow__")}))}(e),o&&window.requestAnimationFrame(a)};return a(),()=>{o=!1}}const l=Symbol(),s=document.currentScript;((t=document)=>{if("undefined"==typeof window)throw new Error("Marp Core's browser script is valid only in browser context.");if(t[l])return t[l];const e=a({target:t}),r=()=>{e(),delete t[l]};Object.defineProperty(t,l,{configurable:!0,value:r})})(s?s.getRootNode():document)}();
2168 </script></foreignObject></svg></div><div class="bespoke-marp-note" data-index="1" tabindex="0"><p>研究目的</p></div><div class="bespoke-marp-note" data-index="13" tabindex="0"><p>コードの解説 2262 </script></foreignObject></svg></div><div class="bespoke-marp-note" data-index="1" tabindex="0"><p>研究目的</p></div><div class="bespoke-marp-note" data-index="11" tabindex="0"><p>コードの解説
2169 あとで…</p></div><div class="bespoke-marp-note" data-index="16" tabindex="0"><p>findは全部書いても大丈夫そう</p></div><div class="bespoke-marp-note" data-index="17" tabindex="0"><p>これは途中省略してよさそう</p></div><div class="bespoke-marp-note" data-index="20" tabindex="0"><p>コードの解説 2263 あとで…</p></div><div class="bespoke-marp-note" data-index="14" tabindex="0"><p>findは全部書いても大丈夫そう</p></div><div class="bespoke-marp-note" data-index="15" tabindex="0"><p>これは途中省略してよさそう</p></div><div class="bespoke-marp-note" data-index="18" tabindex="0"><p>コードの解説
2170 省略した方がたぶん絶対良い 2264 省略した方がたぶん絶対良い
2171 right と left なんかはほとんど対照的なので省略とかでよさそう 2265 right と left なんかはほとんど対照的なので省略とかでよさそう
2172 あとは、木構造の仕様を満たすためにData型になっている説明があるとよさそう</p></div><script>/*!! License: https://unpkg.com/@marp-team/marp-cli@1.5.0/lib/bespoke.js.LICENSE.txt */ 2266 あとは、木構造の仕様を満たすためにData型になっている説明があるとよさそう</p></div><script>/*!! License: https://unpkg.com/@marp-team/marp-cli@1.5.0/lib/bespoke.js.LICENSE.txt */
2173 !function(){"use strict";const e=document.body,t=(...e)=>history.replaceState(...e),n="presenter",r="next",o=["",n,r],a="data-bespoke-marp-",i=(e,{protocol:t,host:n,pathname:r,hash:o}=location)=>{const a=e.toString();return`${t}//${n}${r}${a?"?":""}${a}${o}`},s=()=>e.dataset.bespokeView,l=e=>new URLSearchParams(location.search).get(e),c=(e,n={})=>{var r;const o={location,setter:t,...n},a=new URLSearchParams(o.location.search);for(const t of Object.keys(e)){const n=e[t];"string"==typeof n?a.set(t,n):a.delete(t)}try{o.setter({...null!==(r=window.history.state)&&void 0!==r?r:{}},"",i(a,o.location))}catch(e){console.error(e)}},d=(()=>{const e="bespoke-marp";try{return localStorage.setItem(e,e),localStorage.removeItem(e),!0}catch(e){return!1}})(),f=e=>{try{return localStorage.getItem(e)}catch(e){return null}},u=(e,t)=>{try{return localStorage.setItem(e,t),!0}catch(e){return!1}},m=e=>{try{return localStorage.removeItem(e),!0}catch(e){return!1}},g=(e,t)=>{const n="aria-hidden";t?e.setAttribute(n,"true"):e.removeAttribute(n)},p=e=>{e.parent.classList.add("bespoke-marp-parent"),e.slides.forEach((e=>e.classList.add("bespoke-marp-slide"))),e.on("activate",(t=>{const n="bespoke-marp-active",r=t.slide,o=r.classList,a=!o.contains(n);if(e.slides.forEach((e=>{e.classList.remove(n),g(e,!0)})),o.add(n),g(r,!1),a){const e=`${n}-ready`;o.add(e),document.body.clientHeight,o.remove(e)}}))},v=e=>{let t=0,n=0;Object.defineProperty(e,"fragments",{enumerable:!0,value:e.slides.map((e=>[null,...e.querySelectorAll("[data-marpit-fragment]")]))});const r=r=>void 0!==e.fragments[t][n+r],o=(r,o)=>{t=r,n=o,e.fragments.forEach(((e,t)=>{e.forEach(((e,n)=>{if(null==e)return;const i=t<r||t===r&&n<=o;e.setAttribute(`${a}fragment`,(i?"":"in")+"active");const s=`${a}current-fragment`;t===r&&n===o?e.setAttribute(s,"current"):e.removeAttribute(s)}))})),e.fragmentIndex=o;const i={slide:e.slides[r],index:r,fragments:e.fragments[r],fragmentIndex:o};e.fire("fragment",i)};e.on("next",(({fragment:a=!0})=>{if(a){if(r(1))return o(t,n+1),!1;const a=t+1;e.fragments[a]&&o(a,0)}else{const r=e.fragments[t].length;if(n+1<r)return o(t,r-1),!1;const a=e.fragments[t+1];a&&o(t+1,a.length-1)}})),e.on("prev",(({fragment:a=!0})=>{if(r(-1)&&a)return o(t,n-1),!1;const i=t-1;e.fragments[i]&&o(i,e.fragments[i].length-1)})),e.on("slide",(({index:t,fragment:n})=>{let r=0;if(void 0!==n){const o=e.fragments[t];if(o){const{length:e}=o;r=-1===n?e-1:Math.min(Math.max(n,0),e-1)}}o(t,r)})),o(0,0)},h=document,y=()=>!(!h.fullscreenEnabled&&!h.webkitFullscreenEnabled),x=()=>!(!h.fullscreenElement&&!h.webkitFullscreenElement),w=e=>{e.fullscreen=()=>{y()&&(async()=>{return x()?null===(e=h.exitFullscreen||h.webkitExitFullscreen)||void 0===e?void 0:e.call(h):((e=h.body)=>{var t;return null===(t=e.requestFullscreen||e.webkitRequestFullscreen)||void 0===t?void 0:t.call(e)})();var e})()},document.addEventListener("keydown",(t=>{"f"!==t.key&&"F11"!==t.key||t.altKey||t.ctrlKey||t.metaKey||!y()||(e.fullscreen(),t.preventDefault())}))},b="bespoke-marp-inactive",k=(e=2e3)=>({parent:t,fire:n})=>{const r=t.classList,o=e=>n(`marp-${e?"":"in"}active`);let a;const i=()=>{a&&clearTimeout(a),a=setTimeout((()=>{r.add(b),o()}),e),r.contains(b)&&(r.remove(b),o(!0))};for(const e of["mousedown","mousemove","touchend"])document.addEventListener(e,i);setTimeout(i,0)},E=["AUDIO","BUTTON","INPUT","SELECT","TEXTAREA","VIDEO"],L=e=>{e.parent.addEventListener("keydown",(e=>{if(!e.target)return;const t=e.target;(E.includes(t.nodeName)||"true"===t.contentEditable)&&e.stopPropagation()}))},$=e=>{window.addEventListener("load",(()=>{for(const t of e.slides){const e=t.querySelector("[data-marp-fitting]")?"":"hideable";t.setAttribute(`${a}load`,e)}}))},P=({interval:e=250}={})=>t=>{document.addEventListener("keydown",(e=>{if(" "===e.key&&e.shiftKey)t.prev();else if("ArrowLeft"===e.key||"ArrowUp"===e.key||"PageUp"===e.key)t.prev({fragment:!e.shiftKey});else if(" "!==e.key||e.shiftKey)if("ArrowRight"===e.key||"ArrowDown"===e.key||"PageDown"===e.key)t.next({fragment:!e.shiftKey});else if("End"===e.key)t.slide(t.slides.length-1,{fragment:-1});else{if("Home"!==e.key)return;t.slide(0)}else t.next();e.preventDefault()}));let n,r,o=0;t.parent.addEventListener("wheel",(a=>{let i=!1;const s=(e,t)=>{e&&(i=i||((e,t)=>((e,t)=>{const n="X"===t?"Width":"Height";return e[`client${n}`]<e[`scroll${n}`]})(e,t)&&((e,t)=>{const{overflow:n}=e,r=e[`overflow${t}`];return"auto"===n||"scroll"===n||"auto"===r||"scroll"===r})(getComputedStyle(e),t))(e,t)),(null==e?void 0:e.parentElement)&&s(e.parentElement,t)};if(0!==a.deltaX&&s(a.target,"X"),0!==a.deltaY&&s(a.target,"Y"),i)return;a.preventDefault();const l=Math.sqrt(a.deltaX**2+a.deltaY**2);if(void 0!==a.wheelDelta){if(void 0===a.webkitForce&&Math.abs(a.wheelDelta)<40)return;if(a.deltaMode===a.DOM_DELTA_PIXEL&&l<4)return}else if(a.deltaMode===a.DOM_DELTA_PIXEL&&l<12)return;r&&clearTimeout(r),r=setTimeout((()=>{n=0}),e);const c=Date.now()-o<e,d=l<=n;if(n=l,c||d)return;let f;(a.deltaX>0||a.deltaY>0)&&(f="next"),(a.deltaX<0||a.deltaY<0)&&(f="prev"),f&&(t[f](),o=Date.now())}))},S=(e=".bespoke-marp-osc")=>{const t=document.querySelector(e);if(!t)return()=>{};const n=(e,n)=>{t.querySelectorAll(`[${a}osc=${JSON.stringify(e)}]`).forEach(n)};return y()||n("fullscreen",(e=>e.style.display="none")),d||n("presenter",(e=>{e.disabled=!0,e.title="Presenter view is disabled due to restricted localStorage."})),e=>{t.addEventListener("click",(t=>{if(t.target instanceof HTMLElement){const{bespokeMarpOsc:n}=t.target.dataset;n&&t.target.blur();const r={fragment:!t.shiftKey};"next"===n?e.next(r):"prev"===n?e.prev(r):"fullscreen"===n?null==e||e.fullscreen():"presenter"===n&&e.openPresenterView()}})),e.parent.appendChild(t),e.on("activate",(({index:t})=>{n("page",(n=>n.textContent=`Page ${t+1} of ${e.slides.length}`))})),e.on("fragment",(({index:t,fragments:r,fragmentIndex:o})=>{n("prev",(e=>e.disabled=0===t&&0===o)),n("next",(n=>n.disabled=t===e.slides.length-1&&o===r.length-1))})),e.on("marp-active",(()=>g(t,!1))),e.on("marp-inactive",(()=>g(t,!0))),y()&&(e=>{for(const t of["","webkit"])h.addEventListener(t+"fullscreenchange",e)})((()=>n("fullscreen",(e=>e.classList.toggle("exit",y()&&x())))))}},I=e=>{window.addEventListener("message",(t=>{if(t.origin!==window.origin)return;const[n,r]=t.data.split(":");if("navigate"===n){const[t,n]=r.split(",");let o=Number.parseInt(t,10),a=Number.parseInt(n,10)+1;a>=e.fragments[o].length&&(o+=1,a=0),e.slide(o,{fragment:a})}}))};var T=["area","base","br","col","command","embed","hr","img","input","keygen","link","meta","param","source","track","wbr"];let A=e=>String(e).replace(/[&<>"']/g,(e=>`&${C[e]};`)),C={"&":"amp","<":"lt",">":"gt",'"':"quot","'":"apos"},N="dangerouslySetInnerHTML",K={className:"class",htmlFor:"for"},O={};function D(e,t){let n=[],r="";t=t||{};for(let e=arguments.length;e-- >2;)n.push(arguments[e]);if("function"==typeof e)return t.children=n.reverse(),e(t);if(e){if(r+="<"+e,t)for(let e in t)!1!==t[e]&&null!=t[e]&&e!==N&&(r+=` ${K[e]?K[e]:A(e)}="${A(t[e])}"`);r+=">"}if(-1===T.indexOf(e)){if(t[N])r+=t[N].__html;else for(;n.length;){let e=n.pop();if(e)if(e.pop)for(let t=e.length;t--;)n.push(e[t]);else r+=!0===O[e]?e:A(e)}r+=e?`</${e}>`:""}return O[r]=!0,r}const M=({children:e})=>D(null,null,...e),q="bespoke-marp-presenter-",_={container:`${q}container`,next:`${q}next`,nextContainer:`${q}next-container`,noteContainer:`${q}note-container`,infoContainer:`${q}info-container`,infoPage:`${q}info-page`,infoPageText:`${q}info-page-text`,infoPagePrev:`${q}info-page-prev`,infoPageNext:`${q}info-page-next`,infoTime:`${q}info-time`,infoTimer:`${q}info-timer`},U=e=>{const{title:t}=document;document.title="[Presenter view]"+(t?` - ${t}`:"");const n={},r=e=>(n[e]=n[e]||document.querySelector(`.${e}`),n[e]);document.body.appendChild((e=>{const t=document.createElement("div");return t.className=_.container,t.appendChild(e),t.insertAdjacentHTML("beforeend",D(M,null,D("div",{class:_.nextContainer},D("iframe",{class:_.next,src:"?view=next"})),D("div",{class:_.noteContainer}),D("div",{class:_.infoContainer},D("div",{class:_.infoPage},D("button",{class:_.infoPagePrev,tabindex:"-1",title:"Previous"},"Previous"),D("span",{class:_.infoPageText}),D("button",{class:_.infoPageNext,tabindex:"-1",title:"Next"},"Next")),D("time",{class:_.infoTime,title:"Current time"}),D("div",{class:_.infoTimer})))),t})(e.parent)),(e=>{r(_.nextContainer).addEventListener("click",(()=>e.next()));const t=r(_.next),n=(o=t,(e,t)=>{var n;return null===(n=o.contentWindow)||void 0===n?void 0:n.postMessage(`navigate:${e},${t}`,"null"===window.origin?"*":window.origin)});var o;t.addEventListener("load",(()=>{r(_.nextContainer).classList.add("active"),n(e.slide(),e.fragmentIndex),e.on("fragment",(({index:e,fragmentIndex:t})=>n(e,t)))}));const a=document.querySelectorAll(".bespoke-marp-note");a.forEach((e=>{e.addEventListener("keydown",(e=>e.stopPropagation())),r(_.noteContainer).appendChild(e)})),e.on("activate",(()=>a.forEach((t=>t.classList.toggle("active",t.dataset.index==e.slide()))))),e.on("activate",(({index:t})=>{r(_.infoPageText).textContent=`${t+1} / ${e.slides.length}`}));const i=r(_.infoPagePrev),s=r(_.infoPageNext);i.addEventListener("click",(t=>{i.blur(),e.prev({fragment:!t.shiftKey})})),s.addEventListener("click",(t=>{s.blur(),e.next({fragment:!t.shiftKey})})),e.on("fragment",(({index:t,fragments:n,fragmentIndex:r})=>{i.disabled=0===t&&0===r,s.disabled=t===e.slides.length-1&&r===n.length-1}));const l=()=>r(_.infoTime).textContent=(new Date).toLocaleTimeString();l(),setInterval(l,250)})(e)},V=e=>{if(!(e=>e.syncKey&&"string"==typeof e.syncKey)(e))throw new Error("The current instance of Bespoke.js is invalid for Marp bespoke presenter plugin.");Object.defineProperties(e,{openPresenterView:{enumerable:!0,value:X},presenterUrl:{enumerable:!0,get:F}}),d&&document.addEventListener("keydown",(t=>{"p"!==t.key||t.altKey||t.ctrlKey||t.metaKey||(t.preventDefault(),e.openPresenterView())}))};function X(){const{max:e,floor:t}=Math,n=e(t(.85*window.innerWidth),640),r=e(t(.85*window.innerHeight),360);return window.open(this.presenterUrl,q+this.syncKey,`width=${n},height=${r},menubar=no,toolbar=no`)}function F(){const e=new URLSearchParams(location.search);return e.set("view","presenter"),e.set("sync",this.syncKey),i(e)}const B=e=>{const t=s();return t===r&&e.appendChild(document.createElement("span")),{"":V,[n]:U,[r]:I}[t]},R=e=>{e.on("activate",(t=>{document.querySelectorAll(".bespoke-progress-parent > .bespoke-progress-bar").forEach((n=>{n.style.flexBasis=100*t.index/(e.slides.length-1)+"%"}))}))},j=e=>{const t=Number.parseInt(e,10);return Number.isNaN(t)?null:t},H=(e={})=>{const t={history:!0,...e};return e=>{let n=!0;const r=e=>{const t=n;try{return n=!0,e()}finally{n=t}},o=(t={fragment:!0})=>{((t,n)=>{const{min:r,max:o}=Math,{fragments:a,slides:i}=e,s=o(0,r(t,i.length-1)),l=o(0,r(n||0,a[s].length-1));s===e.slide()&&l===e.fragmentIndex||e.slide(s,{fragment:l})})((j(location.hash.slice(1))||1)-1,t.fragment?j(l("f")||""):null)};e.on("fragment",(({index:e,fragmentIndex:r})=>{n||c({f:0===r||r.toString()},{location:{...location,hash:`#${e+1}`},setter:(...e)=>t.history?history.pushState(...e):history.replaceState(...e)})})),setTimeout((()=>{o(),window.addEventListener("hashchange",(()=>r((()=>{o({fragment:!1}),c({f:void 0})})))),window.addEventListener("popstate",(()=>{n||r((()=>o()))})),n=!1}),0)}},Y=(e={})=>{var n;const r=e.key||(null===(n=window.history.state)||void 0===n?void 0:n.marpBespokeSyncKey)||Math.random().toString(36).slice(2),o=`bespoke-marp-sync-${r}`;var a;a={marpBespokeSyncKey:r},c({},{setter:(e,...n)=>t({...e,...a},...n)});const i=()=>{const e=f(o);return e?JSON.parse(e):Object.create(null)},s=e=>{const t=i(),n={...t,...e(t)};return u(o,JSON.stringify(n)),n},l=()=>{window.removeEventListener("pageshow",l),s((e=>({reference:(e.reference||0)+1})))};return e=>{l(),Object.defineProperty(e,"syncKey",{value:r,enumerable:!0});let t=!0;setTimeout((()=>{e.on("fragment",(e=>{t&&s((()=>({index:e.index,fragmentIndex:e.fragmentIndex})))}))}),0),window.addEventListener("storage",(n=>{if(n.key===o&&n.oldValue&&n.newValue){const r=JSON.parse(n.oldValue),o=JSON.parse(n.newValue);if(r.index!==o.index||r.fragmentIndex!==o.fragmentIndex)try{t=!1,e.slide(o.index,{fragment:o.fragmentIndex})}finally{t=!0}}}));const n=()=>{const{reference:e}=i();void 0===e||e<=1?m(o):s((()=>({reference:e-1})))};window.addEventListener("pagehide",(e=>{e.persisted&&window.addEventListener("pageshow",l),n()})),e.on("destroy",n)}},{PI:J,abs:W,sqrt:z,atan2:G}=Math,Q={passive:!0},Z=({slope:e=-.7,swipeThreshold:t=30}={})=>n=>{let r;const o=n.parent,a=e=>{const t=o.getBoundingClientRect();return{x:e.pageX-(t.left+t.right)/2,y:e.pageY-(t.top+t.bottom)/2}};o.addEventListener("touchstart",(({touches:e})=>{r=1===e.length?a(e[0]):void 0}),Q),o.addEventListener("touchmove",(e=>{if(r)if(1===e.touches.length){e.preventDefault();const t=a(e.touches[0]),n=t.x-r.x,o=t.y-r.y;r.delta=z(W(n)**2+W(o)**2),r.radian=G(n,o)}else r=void 0})),o.addEventListener("touchend",(o=>{if(r){if(r.delta&&r.delta>=t&&r.radian){const t=(r.radian-e+J)%(2*J)-J;n[t<0?"next":"prev"](),o.stopPropagation()}r=void 0}}),Q)},ee="_tA",te=e=>{const t=document.documentTransition;if(!t)return;let n;e._tP=!1;const r=(n,{back:r,cond:o})=>a=>{const i=e.slides[e.slide()].querySelector("section[data-transition]");if(!i)return!0;const s=document.querySelector(".bespoke-marp-osc"),l=s?[s]:void 0;if(e._tP){if(a._tA){e._tP=!1;try{t.start({sharedElements:l}).catch((()=>{}))}catch(e){}return!0}}else{if(!o(a))return!0;e._tP=t.prepare({rootTransition:a.back||r?i.dataset.transitionBack:i.dataset.transition,sharedElements:l}).then((()=>n(a))).catch((()=>n(a)))}return!1};e.on("prev",r((t=>e.prev({...t,[ee]:!0})),{back:!0,cond:e=>{var t;return e.index>0&&!((null===(t=e.fragment)||void 0===t||t)&&n.fragmentIndex>0)}})),e.on("next",r((t=>e.next({...t,[ee]:!0})),{cond:t=>t.index+1<e.slides.length&&!(n.fragmentIndex+1<n.fragments.length)})),setTimeout((()=>{e.on("slide",r((t=>e.slide(t.index,{...t,[ee]:!0})),{cond:t=>{const n=e.slide();return t.index!==n&&(t.back=t.index<n,!0)}}))}),0),e.on("fragment",(e=>{n=e}))};let ne;const re=()=>(void 0===ne&&(ne="wakeLock"in navigator&&navigator.wakeLock),ne),oe=async()=>{const e=re();if(e)try{return await e.request("screen")}catch(e){console.warn(e)}return null},ae=async()=>{if(!re())return;let e;const t=()=>{e&&"visible"===document.visibilityState&&oe()};for(const e of["visibilitychange","fullscreenchange"])document.addEventListener(e,t);return e=await oe(),e};((t=document.getElementById("p"))=>{(()=>{const t=l("view");e.dataset.bespokeView=t===r||t===n?t:""})();const a=(e=>{const t=l(e);return c({[e]:void 0}),t})("sync")||void 0;var i,d,f,u,m,g,h,y,x,b,E,I;i=t,d=((...e)=>{const t=o.findIndex((e=>s()===e));return e.map((([e,n])=>e[t]&&n)).filter((e=>e))})([[1,1,0],Y({key:a})],[[1,1,1],B(t)],[[1,1,0],L],[[1,1,1],p],[[1,0,0],k()],[[1,1,1],$],[[1,1,1],H({history:!1})],[[1,1,0],P()],[[1,1,0],w],[[1,0,0],R],[[1,1,0],Z()],[[1,0,0],S()],[[1,0,0],te],[[1,1,1],v],[[1,1,0],ae]),u=1===(i.parent||i).nodeType?i.parent||i:document.querySelector(i.parent||i),m=[].filter.call("string"==typeof i.slides?u.querySelectorAll(i.slides):i.slides||u.children,(function(e){return"SCRIPT"!==e.nodeName})),g={},h=function(e,t){return(t=t||{}).index=m.indexOf(e),t.slide=e,t},b=function(e,t){m[e]&&(f&&x("deactivate",h(f,t)),f=m[e],x("activate",h(f,t)))},E=function(e,t){var n=m.indexOf(f)+e;x(e>0?"next":"prev",h(f,t))&&b(n,t)},I={off:y=function(e,t){g[e]=(g[e]||[]).filter((function(e){return e!==t}))},on:function(e,t){return(g[e]||(g[e]=[])).push(t),y.bind(null,e,t)},fire:x=function(e,t){return(g[e]||[]).reduce((function(e,n){return e&&!1!==n(t)}),!0)},slide:function(e,t){if(!arguments.length)return m.indexOf(f);x("slide",h(m[e],t))&&b(e,t)},next:E.bind(null,1),prev:E.bind(null,-1),parent:u,slides:m,destroy:function(e){x("destroy",h(f,e)),g={}}},(d||[]).forEach((function(e){e(I)})),f||b(0)})()}();</script></body></html> 2267 !function(){"use strict";const e=document.body,t=(...e)=>history.replaceState(...e),n="presenter",r="next",o=["",n,r],a="data-bespoke-marp-",i=(e,{protocol:t,host:n,pathname:r,hash:o}=location)=>{const a=e.toString();return`${t}//${n}${r}${a?"?":""}${a}${o}`},s=()=>e.dataset.bespokeView,l=e=>new URLSearchParams(location.search).get(e),c=(e,n={})=>{var r;const o={location,setter:t,...n},a=new URLSearchParams(o.location.search);for(const t of Object.keys(e)){const n=e[t];"string"==typeof n?a.set(t,n):a.delete(t)}try{o.setter({...null!==(r=window.history.state)&&void 0!==r?r:{}},"",i(a,o.location))}catch(e){console.error(e)}},d=(()=>{const e="bespoke-marp";try{return localStorage.setItem(e,e),localStorage.removeItem(e),!0}catch(e){return!1}})(),f=e=>{try{return localStorage.getItem(e)}catch(e){return null}},u=(e,t)=>{try{return localStorage.setItem(e,t),!0}catch(e){return!1}},m=e=>{try{return localStorage.removeItem(e),!0}catch(e){return!1}},g=(e,t)=>{const n="aria-hidden";t?e.setAttribute(n,"true"):e.removeAttribute(n)},p=e=>{e.parent.classList.add("bespoke-marp-parent"),e.slides.forEach((e=>e.classList.add("bespoke-marp-slide"))),e.on("activate",(t=>{const n="bespoke-marp-active",r=t.slide,o=r.classList,a=!o.contains(n);if(e.slides.forEach((e=>{e.classList.remove(n),g(e,!0)})),o.add(n),g(r,!1),a){const e=`${n}-ready`;o.add(e),document.body.clientHeight,o.remove(e)}}))},v=e=>{let t=0,n=0;Object.defineProperty(e,"fragments",{enumerable:!0,value:e.slides.map((e=>[null,...e.querySelectorAll("[data-marpit-fragment]")]))});const r=r=>void 0!==e.fragments[t][n+r],o=(r,o)=>{t=r,n=o,e.fragments.forEach(((e,t)=>{e.forEach(((e,n)=>{if(null==e)return;const i=t<r||t===r&&n<=o;e.setAttribute(`${a}fragment`,(i?"":"in")+"active");const s=`${a}current-fragment`;t===r&&n===o?e.setAttribute(s,"current"):e.removeAttribute(s)}))})),e.fragmentIndex=o;const i={slide:e.slides[r],index:r,fragments:e.fragments[r],fragmentIndex:o};e.fire("fragment",i)};e.on("next",(({fragment:a=!0})=>{if(a){if(r(1))return o(t,n+1),!1;const a=t+1;e.fragments[a]&&o(a,0)}else{const r=e.fragments[t].length;if(n+1<r)return o(t,r-1),!1;const a=e.fragments[t+1];a&&o(t+1,a.length-1)}})),e.on("prev",(({fragment:a=!0})=>{if(r(-1)&&a)return o(t,n-1),!1;const i=t-1;e.fragments[i]&&o(i,e.fragments[i].length-1)})),e.on("slide",(({index:t,fragment:n})=>{let r=0;if(void 0!==n){const o=e.fragments[t];if(o){const{length:e}=o;r=-1===n?e-1:Math.min(Math.max(n,0),e-1)}}o(t,r)})),o(0,0)},h=document,y=()=>!(!h.fullscreenEnabled&&!h.webkitFullscreenEnabled),x=()=>!(!h.fullscreenElement&&!h.webkitFullscreenElement),w=e=>{e.fullscreen=()=>{y()&&(async()=>{return x()?null===(e=h.exitFullscreen||h.webkitExitFullscreen)||void 0===e?void 0:e.call(h):((e=h.body)=>{var t;return null===(t=e.requestFullscreen||e.webkitRequestFullscreen)||void 0===t?void 0:t.call(e)})();var e})()},document.addEventListener("keydown",(t=>{"f"!==t.key&&"F11"!==t.key||t.altKey||t.ctrlKey||t.metaKey||!y()||(e.fullscreen(),t.preventDefault())}))},b="bespoke-marp-inactive",k=(e=2e3)=>({parent:t,fire:n})=>{const r=t.classList,o=e=>n(`marp-${e?"":"in"}active`);let a;const i=()=>{a&&clearTimeout(a),a=setTimeout((()=>{r.add(b),o()}),e),r.contains(b)&&(r.remove(b),o(!0))};for(const e of["mousedown","mousemove","touchend"])document.addEventListener(e,i);setTimeout(i,0)},E=["AUDIO","BUTTON","INPUT","SELECT","TEXTAREA","VIDEO"],L=e=>{e.parent.addEventListener("keydown",(e=>{if(!e.target)return;const t=e.target;(E.includes(t.nodeName)||"true"===t.contentEditable)&&e.stopPropagation()}))},$=e=>{window.addEventListener("load",(()=>{for(const t of e.slides){const e=t.querySelector("[data-marp-fitting]")?"":"hideable";t.setAttribute(`${a}load`,e)}}))},P=({interval:e=250}={})=>t=>{document.addEventListener("keydown",(e=>{if(" "===e.key&&e.shiftKey)t.prev();else if("ArrowLeft"===e.key||"ArrowUp"===e.key||"PageUp"===e.key)t.prev({fragment:!e.shiftKey});else if(" "!==e.key||e.shiftKey)if("ArrowRight"===e.key||"ArrowDown"===e.key||"PageDown"===e.key)t.next({fragment:!e.shiftKey});else if("End"===e.key)t.slide(t.slides.length-1,{fragment:-1});else{if("Home"!==e.key)return;t.slide(0)}else t.next();e.preventDefault()}));let n,r,o=0;t.parent.addEventListener("wheel",(a=>{let i=!1;const s=(e,t)=>{e&&(i=i||((e,t)=>((e,t)=>{const n="X"===t?"Width":"Height";return e[`client${n}`]<e[`scroll${n}`]})(e,t)&&((e,t)=>{const{overflow:n}=e,r=e[`overflow${t}`];return"auto"===n||"scroll"===n||"auto"===r||"scroll"===r})(getComputedStyle(e),t))(e,t)),(null==e?void 0:e.parentElement)&&s(e.parentElement,t)};if(0!==a.deltaX&&s(a.target,"X"),0!==a.deltaY&&s(a.target,"Y"),i)return;a.preventDefault();const l=Math.sqrt(a.deltaX**2+a.deltaY**2);if(void 0!==a.wheelDelta){if(void 0===a.webkitForce&&Math.abs(a.wheelDelta)<40)return;if(a.deltaMode===a.DOM_DELTA_PIXEL&&l<4)return}else if(a.deltaMode===a.DOM_DELTA_PIXEL&&l<12)return;r&&clearTimeout(r),r=setTimeout((()=>{n=0}),e);const c=Date.now()-o<e,d=l<=n;if(n=l,c||d)return;let f;(a.deltaX>0||a.deltaY>0)&&(f="next"),(a.deltaX<0||a.deltaY<0)&&(f="prev"),f&&(t[f](),o=Date.now())}))},S=(e=".bespoke-marp-osc")=>{const t=document.querySelector(e);if(!t)return()=>{};const n=(e,n)=>{t.querySelectorAll(`[${a}osc=${JSON.stringify(e)}]`).forEach(n)};return y()||n("fullscreen",(e=>e.style.display="none")),d||n("presenter",(e=>{e.disabled=!0,e.title="Presenter view is disabled due to restricted localStorage."})),e=>{t.addEventListener("click",(t=>{if(t.target instanceof HTMLElement){const{bespokeMarpOsc:n}=t.target.dataset;n&&t.target.blur();const r={fragment:!t.shiftKey};"next"===n?e.next(r):"prev"===n?e.prev(r):"fullscreen"===n?null==e||e.fullscreen():"presenter"===n&&e.openPresenterView()}})),e.parent.appendChild(t),e.on("activate",(({index:t})=>{n("page",(n=>n.textContent=`Page ${t+1} of ${e.slides.length}`))})),e.on("fragment",(({index:t,fragments:r,fragmentIndex:o})=>{n("prev",(e=>e.disabled=0===t&&0===o)),n("next",(n=>n.disabled=t===e.slides.length-1&&o===r.length-1))})),e.on("marp-active",(()=>g(t,!1))),e.on("marp-inactive",(()=>g(t,!0))),y()&&(e=>{for(const t of["","webkit"])h.addEventListener(t+"fullscreenchange",e)})((()=>n("fullscreen",(e=>e.classList.toggle("exit",y()&&x())))))}},I=e=>{window.addEventListener("message",(t=>{if(t.origin!==window.origin)return;const[n,r]=t.data.split(":");if("navigate"===n){const[t,n]=r.split(",");let o=Number.parseInt(t,10),a=Number.parseInt(n,10)+1;a>=e.fragments[o].length&&(o+=1,a=0),e.slide(o,{fragment:a})}}))};var T=["area","base","br","col","command","embed","hr","img","input","keygen","link","meta","param","source","track","wbr"];let A=e=>String(e).replace(/[&<>"']/g,(e=>`&${C[e]};`)),C={"&":"amp","<":"lt",">":"gt",'"':"quot","'":"apos"},N="dangerouslySetInnerHTML",K={className:"class",htmlFor:"for"},O={};function D(e,t){let n=[],r="";t=t||{};for(let e=arguments.length;e-- >2;)n.push(arguments[e]);if("function"==typeof e)return t.children=n.reverse(),e(t);if(e){if(r+="<"+e,t)for(let e in t)!1!==t[e]&&null!=t[e]&&e!==N&&(r+=` ${K[e]?K[e]:A(e)}="${A(t[e])}"`);r+=">"}if(-1===T.indexOf(e)){if(t[N])r+=t[N].__html;else for(;n.length;){let e=n.pop();if(e)if(e.pop)for(let t=e.length;t--;)n.push(e[t]);else r+=!0===O[e]?e:A(e)}r+=e?`</${e}>`:""}return O[r]=!0,r}const M=({children:e})=>D(null,null,...e),q="bespoke-marp-presenter-",_={container:`${q}container`,next:`${q}next`,nextContainer:`${q}next-container`,noteContainer:`${q}note-container`,infoContainer:`${q}info-container`,infoPage:`${q}info-page`,infoPageText:`${q}info-page-text`,infoPagePrev:`${q}info-page-prev`,infoPageNext:`${q}info-page-next`,infoTime:`${q}info-time`,infoTimer:`${q}info-timer`},U=e=>{const{title:t}=document;document.title="[Presenter view]"+(t?` - ${t}`:"");const n={},r=e=>(n[e]=n[e]||document.querySelector(`.${e}`),n[e]);document.body.appendChild((e=>{const t=document.createElement("div");return t.className=_.container,t.appendChild(e),t.insertAdjacentHTML("beforeend",D(M,null,D("div",{class:_.nextContainer},D("iframe",{class:_.next,src:"?view=next"})),D("div",{class:_.noteContainer}),D("div",{class:_.infoContainer},D("div",{class:_.infoPage},D("button",{class:_.infoPagePrev,tabindex:"-1",title:"Previous"},"Previous"),D("span",{class:_.infoPageText}),D("button",{class:_.infoPageNext,tabindex:"-1",title:"Next"},"Next")),D("time",{class:_.infoTime,title:"Current time"}),D("div",{class:_.infoTimer})))),t})(e.parent)),(e=>{r(_.nextContainer).addEventListener("click",(()=>e.next()));const t=r(_.next),n=(o=t,(e,t)=>{var n;return null===(n=o.contentWindow)||void 0===n?void 0:n.postMessage(`navigate:${e},${t}`,"null"===window.origin?"*":window.origin)});var o;t.addEventListener("load",(()=>{r(_.nextContainer).classList.add("active"),n(e.slide(),e.fragmentIndex),e.on("fragment",(({index:e,fragmentIndex:t})=>n(e,t)))}));const a=document.querySelectorAll(".bespoke-marp-note");a.forEach((e=>{e.addEventListener("keydown",(e=>e.stopPropagation())),r(_.noteContainer).appendChild(e)})),e.on("activate",(()=>a.forEach((t=>t.classList.toggle("active",t.dataset.index==e.slide()))))),e.on("activate",(({index:t})=>{r(_.infoPageText).textContent=`${t+1} / ${e.slides.length}`}));const i=r(_.infoPagePrev),s=r(_.infoPageNext);i.addEventListener("click",(t=>{i.blur(),e.prev({fragment:!t.shiftKey})})),s.addEventListener("click",(t=>{s.blur(),e.next({fragment:!t.shiftKey})})),e.on("fragment",(({index:t,fragments:n,fragmentIndex:r})=>{i.disabled=0===t&&0===r,s.disabled=t===e.slides.length-1&&r===n.length-1}));const l=()=>r(_.infoTime).textContent=(new Date).toLocaleTimeString();l(),setInterval(l,250)})(e)},V=e=>{if(!(e=>e.syncKey&&"string"==typeof e.syncKey)(e))throw new Error("The current instance of Bespoke.js is invalid for Marp bespoke presenter plugin.");Object.defineProperties(e,{openPresenterView:{enumerable:!0,value:X},presenterUrl:{enumerable:!0,get:F}}),d&&document.addEventListener("keydown",(t=>{"p"!==t.key||t.altKey||t.ctrlKey||t.metaKey||(t.preventDefault(),e.openPresenterView())}))};function X(){const{max:e,floor:t}=Math,n=e(t(.85*window.innerWidth),640),r=e(t(.85*window.innerHeight),360);return window.open(this.presenterUrl,q+this.syncKey,`width=${n},height=${r},menubar=no,toolbar=no`)}function F(){const e=new URLSearchParams(location.search);return e.set("view","presenter"),e.set("sync",this.syncKey),i(e)}const B=e=>{const t=s();return t===r&&e.appendChild(document.createElement("span")),{"":V,[n]:U,[r]:I}[t]},R=e=>{e.on("activate",(t=>{document.querySelectorAll(".bespoke-progress-parent > .bespoke-progress-bar").forEach((n=>{n.style.flexBasis=100*t.index/(e.slides.length-1)+"%"}))}))},j=e=>{const t=Number.parseInt(e,10);return Number.isNaN(t)?null:t},H=(e={})=>{const t={history:!0,...e};return e=>{let n=!0;const r=e=>{const t=n;try{return n=!0,e()}finally{n=t}},o=(t={fragment:!0})=>{((t,n)=>{const{min:r,max:o}=Math,{fragments:a,slides:i}=e,s=o(0,r(t,i.length-1)),l=o(0,r(n||0,a[s].length-1));s===e.slide()&&l===e.fragmentIndex||e.slide(s,{fragment:l})})((j(location.hash.slice(1))||1)-1,t.fragment?j(l("f")||""):null)};e.on("fragment",(({index:e,fragmentIndex:r})=>{n||c({f:0===r||r.toString()},{location:{...location,hash:`#${e+1}`},setter:(...e)=>t.history?history.pushState(...e):history.replaceState(...e)})})),setTimeout((()=>{o(),window.addEventListener("hashchange",(()=>r((()=>{o({fragment:!1}),c({f:void 0})})))),window.addEventListener("popstate",(()=>{n||r((()=>o()))})),n=!1}),0)}},Y=(e={})=>{var n;const r=e.key||(null===(n=window.history.state)||void 0===n?void 0:n.marpBespokeSyncKey)||Math.random().toString(36).slice(2),o=`bespoke-marp-sync-${r}`;var a;a={marpBespokeSyncKey:r},c({},{setter:(e,...n)=>t({...e,...a},...n)});const i=()=>{const e=f(o);return e?JSON.parse(e):Object.create(null)},s=e=>{const t=i(),n={...t,...e(t)};return u(o,JSON.stringify(n)),n},l=()=>{window.removeEventListener("pageshow",l),s((e=>({reference:(e.reference||0)+1})))};return e=>{l(),Object.defineProperty(e,"syncKey",{value:r,enumerable:!0});let t=!0;setTimeout((()=>{e.on("fragment",(e=>{t&&s((()=>({index:e.index,fragmentIndex:e.fragmentIndex})))}))}),0),window.addEventListener("storage",(n=>{if(n.key===o&&n.oldValue&&n.newValue){const r=JSON.parse(n.oldValue),o=JSON.parse(n.newValue);if(r.index!==o.index||r.fragmentIndex!==o.fragmentIndex)try{t=!1,e.slide(o.index,{fragment:o.fragmentIndex})}finally{t=!0}}}));const n=()=>{const{reference:e}=i();void 0===e||e<=1?m(o):s((()=>({reference:e-1})))};window.addEventListener("pagehide",(e=>{e.persisted&&window.addEventListener("pageshow",l),n()})),e.on("destroy",n)}},{PI:J,abs:W,sqrt:z,atan2:G}=Math,Q={passive:!0},Z=({slope:e=-.7,swipeThreshold:t=30}={})=>n=>{let r;const o=n.parent,a=e=>{const t=o.getBoundingClientRect();return{x:e.pageX-(t.left+t.right)/2,y:e.pageY-(t.top+t.bottom)/2}};o.addEventListener("touchstart",(({touches:e})=>{r=1===e.length?a(e[0]):void 0}),Q),o.addEventListener("touchmove",(e=>{if(r)if(1===e.touches.length){e.preventDefault();const t=a(e.touches[0]),n=t.x-r.x,o=t.y-r.y;r.delta=z(W(n)**2+W(o)**2),r.radian=G(n,o)}else r=void 0})),o.addEventListener("touchend",(o=>{if(r){if(r.delta&&r.delta>=t&&r.radian){const t=(r.radian-e+J)%(2*J)-J;n[t<0?"next":"prev"](),o.stopPropagation()}r=void 0}}),Q)},ee="_tA",te=e=>{const t=document.documentTransition;if(!t)return;let n;e._tP=!1;const r=(n,{back:r,cond:o})=>a=>{const i=e.slides[e.slide()].querySelector("section[data-transition]");if(!i)return!0;const s=document.querySelector(".bespoke-marp-osc"),l=s?[s]:void 0;if(e._tP){if(a._tA){e._tP=!1;try{t.start({sharedElements:l}).catch((()=>{}))}catch(e){}return!0}}else{if(!o(a))return!0;e._tP=t.prepare({rootTransition:a.back||r?i.dataset.transitionBack:i.dataset.transition,sharedElements:l}).then((()=>n(a))).catch((()=>n(a)))}return!1};e.on("prev",r((t=>e.prev({...t,[ee]:!0})),{back:!0,cond:e=>{var t;return e.index>0&&!((null===(t=e.fragment)||void 0===t||t)&&n.fragmentIndex>0)}})),e.on("next",r((t=>e.next({...t,[ee]:!0})),{cond:t=>t.index+1<e.slides.length&&!(n.fragmentIndex+1<n.fragments.length)})),setTimeout((()=>{e.on("slide",r((t=>e.slide(t.index,{...t,[ee]:!0})),{cond:t=>{const n=e.slide();return t.index!==n&&(t.back=t.index<n,!0)}}))}),0),e.on("fragment",(e=>{n=e}))};let ne;const re=()=>(void 0===ne&&(ne="wakeLock"in navigator&&navigator.wakeLock),ne),oe=async()=>{const e=re();if(e)try{return await e.request("screen")}catch(e){console.warn(e)}return null},ae=async()=>{if(!re())return;let e;const t=()=>{e&&"visible"===document.visibilityState&&oe()};for(const e of["visibilitychange","fullscreenchange"])document.addEventListener(e,t);return e=await oe(),e};((t=document.getElementById("p"))=>{(()=>{const t=l("view");e.dataset.bespokeView=t===r||t===n?t:""})();const a=(e=>{const t=l(e);return c({[e]:void 0}),t})("sync")||void 0;var i,d,f,u,m,g,h,y,x,b,E,I;i=t,d=((...e)=>{const t=o.findIndex((e=>s()===e));return e.map((([e,n])=>e[t]&&n)).filter((e=>e))})([[1,1,0],Y({key:a})],[[1,1,1],B(t)],[[1,1,0],L],[[1,1,1],p],[[1,0,0],k()],[[1,1,1],$],[[1,1,1],H({history:!1})],[[1,1,0],P()],[[1,1,0],w],[[1,0,0],R],[[1,1,0],Z()],[[1,0,0],S()],[[1,0,0],te],[[1,1,1],v],[[1,1,0],ae]),u=1===(i.parent||i).nodeType?i.parent||i:document.querySelector(i.parent||i),m=[].filter.call("string"==typeof i.slides?u.querySelectorAll(i.slides):i.slides||u.children,(function(e){return"SCRIPT"!==e.nodeName})),g={},h=function(e,t){return(t=t||{}).index=m.indexOf(e),t.slide=e,t},b=function(e,t){m[e]&&(f&&x("deactivate",h(f,t)),f=m[e],x("activate",h(f,t)))},E=function(e,t){var n=m.indexOf(f)+e;x(e>0?"next":"prev",h(f,t))&&b(n,t)},I={off:y=function(e,t){g[e]=(g[e]||[]).filter((function(e){return e!==t}))},on:function(e,t){return(g[e]||(g[e]=[])).push(t),y.bind(null,e,t)},fire:x=function(e,t){return(g[e]||[]).reduce((function(e,n){return e&&!1!==n(t)}),!0)},slide:function(e,t){if(!arguments.length)return m.indexOf(f);x("slide",h(m[e],t))&&b(e,t)},next:E.bind(null,1),prev:E.bind(null,-1),parent:u,slides:m,destroy:function(e){x("destroy",h(f,e)),g={}}},(d||[]).forEach((function(e){e(I)})),f||b(0)})()}();</script></body></html>