:root{--ground:#fdfbf7;--ground-sunk:#f6f2e9;--ink:#1a1a18;--ink-muted:#6b665c;--accent:#8b1a1a;--accent-sunk:#f3e7e2;--rule:#d9d2c4;--rule-strong:#a8a196;--serif:"Iowan Old Style", "Palatino Linotype", palatino, georgia, serif;--sans:system-ui, -apple-system, "Segoe UI", sans-serif;--mono:ui-monospace, "SF Mono", "Cascadia Mono", menlo, consolas, monospace;--text-xs:.72rem;--text-sm:.9rem;--text-base:1.125rem;--text-md:1.406rem;--text-lg:1.758rem;--text-xl:2.197rem;--text-2xl:2.747rem;--space-1:.25rem;--space-2:.5rem;--space-3:.75rem;--space-4:1rem;--space-6:1.5rem;--space-8:2rem;--space-12:3rem;--space-16:4rem;--measure:65ch;--wide:100rem;--gutter:var(--space-6)}@media (width<=30rem){:root{--gutter:var(--space-4)}}*,:before,:after{box-sizing:border-box}body{background:var(--ground);color:var(--ink);font-family:var(--serif);font-size:var(--text-base);text-rendering:optimizelegibility;margin:0;line-height:1.6}.frame{grid-template-columns:minmax(var(--gutter), 1fr) min(100% - 2 * var(--gutter), var(--measure)) minmax(var(--gutter), 1fr);display:grid}.frame>*{grid-column:2}.frame>.wide{width:min(100% - 2 * var(--gutter), var(--wide));grid-column:1/-1;margin-inline:auto}h1,h2,h3{margin-block:0 var(--space-4);text-wrap:balance;font-weight:600;line-height:1.15}h1{font-size:var(--text-2xl);letter-spacing:-.015em}h2{font-size:var(--text-lg);margin-block-start:var(--space-12)}h3{font-size:var(--text-md);margin-block-start:var(--space-8)}p,ul,ol,dl,blockquote{margin-block:0 var(--space-4)}p{text-wrap:pretty}.lede{font-size:var(--text-md);color:var(--ink-muted);line-height:1.45}.kicker{font-family:var(--sans);font-size:var(--text-sm);letter-spacing:.08em;text-transform:uppercase;color:var(--accent);margin-block-end:var(--space-2);font-weight:600}small,.small{font-size:var(--text-sm)}.muted{color:var(--ink-muted)}address{margin-block:0 var(--space-4);border-inline-start:3px solid var(--accent);padding-inline-start:var(--space-4);font-style:normal}address :where(p:last-child){margin-block-end:0}.tabular{font-family:var(--mono);font-variant-numeric:tabular-nums;font-size:.9em}.visually-hidden{clip-path:inset(50%);white-space:nowrap;width:1px;height:1px;position:absolute;overflow:hidden}a{color:var(--accent);text-underline-offset:.15em;text-decoration-thickness:.06em}a:hover{text-decoration-thickness:.12em}:focus-visible{outline:2px solid var(--accent);outline-offset:2px}.skip-link{left:var(--space-2);top:var(--space-2);z-index:1;padding:var(--space-2) var(--space-3);background:var(--ground);border:2px solid var(--accent);font-family:var(--sans);font-size:var(--text-sm);position:absolute;transform:translateY(-200%)}.skip-link:focus{transform:none}.site-header{border-block-end:1px solid var(--rule);padding-block:var(--space-4)}.site-header .wide{gap:var(--space-2) var(--space-6);flex-wrap:wrap;justify-content:space-between;align-items:baseline;display:flex}.wordmark{font-size:var(--text-base);color:var(--ink);font-weight:600;text-decoration:none}.wordmark:hover{text-decoration:underline}.wordmark .muted{font-weight:400}.site-nav ul{gap:var(--space-2) var(--space-4);font-family:var(--sans);font-size:var(--text-sm);flex-wrap:wrap;margin:0;padding:0;list-style:none;display:flex}.site-nav a[aria-current=page]{color:var(--ink);text-decoration-thickness:.12em;text-decoration-color:var(--accent)}main{padding-block:var(--space-12) var(--space-16)}.site-footer{border-block-start:1px solid var(--rule);padding-block:var(--space-8);font-size:var(--text-sm);color:var(--ink-muted)}.site-footer p{margin-block-end:var(--space-2)}.site-footer p:last-child{margin-block-end:0}.matrix{border-collapse:collapse;width:100%;font-size:var(--text-sm);line-height:1.3}.matrix caption{color:var(--ink-muted);font-size:var(--text-sm);text-align:start;text-wrap:pretty;margin-block-end:var(--space-4)}.matrix .theorem{text-align:start;font-weight:400}.theorem-number{color:var(--ink-muted)}.theorem-title{margin-inline-start:var(--space-2)}.flag{border:1px solid var(--accent);color:var(--accent);font-family:var(--sans);font-size:var(--text-xs);letter-spacing:.04em;text-transform:uppercase;white-space:nowrap;margin-inline-start:var(--space-2);padding-inline:.35em}.cell{text-align:center}.cell-mark{min-width:2.75rem;min-height:2.75rem;color:var(--ink);justify-content:center;align-items:center;text-decoration:none;display:flex}.is-constructive .cell-mark{color:var(--accent)}.is-empty .cell-mark{color:var(--ink-muted);font-size:1.4em}a.cell-mark:hover,a.cell-mark:focus-visible{background:var(--accent-sunk)}.coverage{color:var(--ink-muted);text-align:end;white-space:nowrap}@media (width>=64rem){.matrix{border-collapse:separate;border-spacing:0;width:min(100%,72rem);margin-inline:auto}.matrix caption{max-width:var(--measure)}.matrix thead th{z-index:2;background:var(--ground);border-block-end:1px solid var(--rule-strong);vertical-align:bottom;padding-block-end:var(--space-2);position:sticky;top:0}.col-theorem{text-align:start}.col-system{height:9rem;font-weight:600}.col-system .system-name{writing-mode:vertical-rl;white-space:nowrap;margin-inline:auto;display:block;rotate:180deg}.col-system .system-count{color:var(--ink-muted);margin-block-start:var(--space-2);font-weight:400;display:block}.col-coverage{text-align:end;padding-inline-start:var(--space-2)}.matrix tbody tr{background:var(--ground);scroll-margin-block-start:11rem}.matrix tbody tr:nth-child(2n){background:var(--ground-sunk)}.matrix tbody tr:hover{background:var(--accent-sunk)}.matrix tbody tr:target{background:var(--accent-sunk);outline:2px solid var(--accent)}.matrix .theorem{z-index:1;background:inherit;padding-block:var(--space-1);padding-inline-end:var(--space-4);position:sticky;left:0}.cell-label,.coverage-of{display:none}}@media (width<64rem){.matrix{max-width:32rem;margin-inline:auto}.matrix thead{display:none}.matrix tbody tr{border-block-start:1px solid var(--rule);padding-block:var(--space-3);grid-template-columns:repeat(7,minmax(0,1fr));scroll-margin-block-start:var(--space-4);display:grid}.matrix tbody tr:target{background:var(--accent-sunk)}.matrix .theorem{grid-column:1/7;padding-block-end:var(--space-2)}.matrix .coverage{grid-area:1/7}.cell-label{color:var(--ink-muted);font-family:var(--sans);font-size:var(--text-xs);display:block}.cell-mark{min-width:100%}}.legend{gap:var(--space-2) var(--space-4);font-size:var(--text-sm);grid-template-columns:max-content 1fr;align-items:baseline;margin-block-end:var(--space-8);display:grid}.legend>div{grid-column:1/-1;grid-template-columns:subgrid;display:grid}.legend dt{text-align:center}.legend dd{color:var(--ink-muted);margin:0}.listing{border-collapse:collapse;width:min(100%,64rem);font-size:var(--text-sm);text-align:start;margin-inline:auto}.listing caption{max-width:var(--measure);color:var(--ink-muted);font-size:var(--text-sm);text-align:start;text-wrap:pretty;margin-block-end:var(--space-4)}.listing th,.listing td{padding-block:var(--space-2);vertical-align:baseline;padding-inline-end:var(--space-4)}.listing thead th{border-block-end:1px solid var(--rule-strong);text-align:start;vertical-align:bottom;padding-block-end:var(--space-2)}.listing tbody tr{border-block-start:1px solid var(--rule)}.listing tbody tr:hover{background:var(--accent-sunk)}.listing tbody th{text-align:start;font-weight:400}.listing-name{text-wrap:pretty;width:60%}.state{white-space:nowrap}.state-mark{margin-inline-end:var(--space-2)}.state .state-mark{color:var(--ink)}.state.is-empty .state-mark,.state.is-empty .state-word{color:var(--ink-muted)}.credits{width:min(100%,76rem)}.credits .listing-name{width:22%}.listing .numeric{text-align:end;white-space:nowrap}.listing .systems{font-family:var(--sans);font-size:var(--text-xs);color:var(--ink-muted);letter-spacing:.04em}.listing .theorems{width:40%;line-height:1.8}.listing .theorems a{border-block-end:1px solid var(--rule-strong);text-decoration:none}.listing .theorems a:hover,.listing .theorems a:focus-visible{background:var(--accent-sunk);border-block-end-color:var(--accent)}.system{border-block-start:1px solid var(--rule);margin-block-start:var(--space-12);padding-block-start:var(--space-4)}.system h2{font-size:var(--text-md);margin-block-start:0}.system-stat{align-items:center;gap:var(--space-3);color:var(--ink-muted);font-size:var(--text-sm);margin-block-end:var(--space-3);display:flex}.bar{background:var(--ground-sunk);border:1px solid var(--rule);flex:1;max-width:24rem;height:.5rem}.bar-fill{background:var(--accent);height:100%;display:block}.system-facts{color:var(--ink-muted);margin-block-end:var(--space-3);padding-inline-start:var(--space-4)}.system-links{margin-block-end:0}.system+:where(p){margin-block-start:var(--space-8)}