:root {
  --lc-def: #dfeeff;
  --lc-lem: #e6f7ea;
  --lc-thm: #ffe5e5;
  --lc-ex: #eef6ff;
  --lc-rem: #fff3c4;
  --lc-exr: #f5f5f5;
  --lc-sol: #ffffff;
  --lc-border: #2b2b2b;
  --lc-accent: #0f4c81;
  --lc-accent-soft: #ecf4fb;
  --lc-panel-bg: #f8fafc;
  --lc-panel-border: #bfd7ea;
  --lc-node: #ffffff;
  --lc-node-border: #8aa4ba;
}

/* Dark-mode palette for custom highlight boxes.
   Use pydata-sphinx-theme/sphinx-design variables so colors remain consistent. */
html[data-theme="dark"] {
  --lc-def: var(--sd-color-info-bg);
  --lc-lem: var(--sd-color-success-bg);
  --lc-thm: var(--sd-color-danger-bg);
  --lc-ex: var(--sd-color-info-bg);
  --lc-rem: var(--sd-color-warning-bg);
  --lc-exr: var(--sd-color-muted-bg);
  --lc-sol: var(--pst-color-surface);
  --lc-border: var(--pst-color-border);
  --lc-accent: var(--pst-color-primary);
  --lc-accent-soft: var(--sd-color-primary-bg);
  --lc-panel-bg: var(--pst-color-surface);
  --lc-panel-border: var(--pst-color-border);
  --lc-node: var(--pst-color-surface);
  --lc-node-border: var(--pst-color-border);
}

/* Base style for custom admonitions */
.admonition.definition,
.admonition.lemma,
.admonition.theorem,
.admonition.example,
.admonition.remark,
.admonition.exercise,
.admonition.solution {
  border-left: 6px solid var(--lc-border);
  box-shadow: 0 1px 4px rgba(0,0,0,0.08);
}

.admonition.definition { background: var(--lc-def); border-color: #2b6cb0; }
.admonition.lemma { background: var(--lc-lem); border-color: #2f855a; }
.admonition.theorem { background: var(--lc-thm); border-color: #c53030; }
.admonition.example { background: var(--lc-ex); border-color: #2b6cb0; }
.admonition.remark { background: var(--lc-rem); border-color: #b7791f; }
.admonition.exercise { background: var(--lc-exr); border-color: #2d3748; }
.admonition.solution { background: var(--lc-sol); border-color: #4a5568; }

/* Dark-mode border colors (avoid low-contrast light-mode hues). */
html[data-theme="dark"] .admonition.definition { border-color: var(--sd-color-info); }
html[data-theme="dark"] .admonition.lemma { border-color: var(--sd-color-success); }
html[data-theme="dark"] .admonition.theorem { border-color: var(--sd-color-danger); }
html[data-theme="dark"] .admonition.example { border-color: var(--sd-color-info); }
html[data-theme="dark"] .admonition.remark { border-color: var(--sd-color-warning); }
html[data-theme="dark"] .admonition.exercise { border-color: var(--sd-color-muted); }
html[data-theme="dark"] .admonition.solution { border-color: var(--pst-color-border); }

/* Improve math blocks and code visibility */
.math { font-size: 1.02em; }
pre, code { font-size: 0.95em; }

/* Notebook cell headings */
div.cell .output_area { padding-left: 4px; }

/* ------------------------------ */
/* Bussproofs-style proof trees   */
/* ------------------------------ */
.lc-proof-tree {
  display: inline-flex;
  flex-direction: column;
  align-items: center;
  gap: 0.2rem;
  margin: 0.6rem 0.25rem;
  padding: 0.2rem 0.35rem;
  max-width: 100%;
}

.lc-pt-premises {
  display: flex;
  flex-wrap: wrap;
  justify-content: center;
  gap: 0.6rem;
  width: 100%;
}

.lc-pt-formula {
  font-family: "Times New Roman", "STIX Two Text", serif;
  font-size: 1.03rem;
  padding: 0.15rem 0.55rem;
  border: 1px solid var(--lc-node-border);
  border-radius: 0.35rem;
  background: var(--lc-node);
  white-space: nowrap;
}

.lc-pt-conclusion {
  border-top: 2px solid #2f3e4d;
  padding-top: 0.25rem;
  width: 100%;
  display: flex;
  justify-content: center;
}

.lc-pt-rule {
  font-size: 0.8rem;
  color: #334e68;
  margin-top: -0.1rem;
}

html[data-theme="dark"] .lc-pt-rule {
  color: var(--pst-color-text-muted);
}

/* ------------------------------ */
/* Glossary sidebar               */
/* ------------------------------ */
.lc-glossary-toggle {
  position: fixed;
  right: 0.7rem;
  bottom: 0.9rem;
  z-index: 1200;
  border: 1px solid var(--lc-panel-border);
  background: #ffffff;
  color: #1e2a35;
  font-weight: 600;
  border-radius: 999px;
  padding: 0.42rem 0.78rem;
  cursor: pointer;
  box-shadow: 0 3px 10px rgba(20, 48, 75, 0.15);
}

html[data-theme="dark"] .lc-glossary-toggle {
  background: var(--pst-color-surface);
  color: var(--pst-color-text-base);
  border-color: var(--pst-color-border);
  box-shadow: 0 3px 12px rgba(0, 0, 0, 0.4);
}

.lc-glossary-sidebar {
  position: fixed;
  right: 0.7rem;
  top: 4.5rem;
  width: 300px;
  max-height: calc(100vh - 6rem);
  overflow-y: auto;
  z-index: 1150;
  background: var(--lc-panel-bg);
  border: 1px solid var(--lc-panel-border);
  border-radius: 0.6rem;
  padding: 0.8rem 0.85rem;
  box-shadow: 0 8px 18px rgba(20, 48, 75, 0.18);
  transform: translateX(110%);
  transition: transform 220ms ease-in-out;
}

.lc-glossary-sidebar.open {
  transform: translateX(0);
}

.lc-glossary-sidebar h3 {
  margin: 0 0 0.45rem 0;
  font-size: 0.95rem;
  color: #0f4c81;
}

html[data-theme="dark"] .lc-glossary-sidebar h3 {
  color: var(--pst-color-primary);
}

.lc-glossary-sidebar dl {
  margin: 0;
}

.lc-glossary-sidebar dt {
  font-weight: 700;
  margin-top: 0.45rem;
  color: #1f2d3a;
}

html[data-theme="dark"] .lc-glossary-sidebar dt {
  color: var(--pst-color-text-base);
}

.lc-glossary-sidebar dd {
  margin: 0.1rem 0 0.2rem 0;
  color: #314559;
  font-size: 0.9rem;
  line-height: 1.35;
}

html[data-theme="dark"] .lc-glossary-sidebar dd {
  color: var(--pst-color-text-muted);
}

.lc-glossary-footer {
  margin-top: 0.5rem;
  font-size: 0.84rem;
}

/* ------------------------------ */
/* Reduction player               */
/* ------------------------------ */
.lc-reduction-player {
  border: 1px solid var(--lc-panel-border);
  border-radius: 0.6rem;
  background: #fff;
  margin: 0.9rem 0;
  overflow: hidden;
}

html[data-theme="dark"] .lc-reduction-player {
  background: var(--pst-color-surface);
  border-color: var(--pst-color-border);
}

.lc-rp-head {
  background: var(--lc-accent-soft);
  border-bottom: 1px solid var(--lc-panel-border);
  padding: 0.5rem 0.7rem;
  font-weight: 650;
  color: #1f3e5a;
  font-size: 0.95rem;
}

html[data-theme="dark"] .lc-rp-head {
  color: var(--pst-color-text-base);
  border-bottom-color: var(--pst-color-border);
}

.lc-rp-body {
  padding: 0.75rem 0.8rem 0.35rem 0.8rem;
}

.lc-rp-step {
  display: none;
  font-family: "Times New Roman", "STIX Two Text", serif;
  font-size: 1.03rem;
  padding: 0.5rem 0.55rem;
  border-left: 4px solid #7ea7cc;
  background: #f7fbff;
  margin: 0.15rem 0 0.45rem 0;
}

html[data-theme="dark"] .lc-rp-step {
  background: rgba(121, 163, 242, 0.1);
  border-left-color: var(--sd-color-info);
}

.lc-rp-step.active {
  display: block;
  animation: lcFadeIn 240ms ease-in;
}

.lc-rp-controls {
  display: flex;
  align-items: center;
  gap: 0.35rem;
  padding: 0 0.8rem 0.75rem 0.8rem;
}

.lc-rp-controls button {
  border: 1px solid #95b6d4;
  background: #fff;
  color: #173a55;
  padding: 0.2rem 0.5rem;
  border-radius: 0.35rem;
  cursor: pointer;
}

html[data-theme="dark"] .lc-rp-controls button {
  border-color: var(--pst-color-border);
  background: var(--pst-color-surface);
  color: var(--pst-color-text-base);
}

.lc-rp-status {
  margin-left: 0.35rem;
  color: #3c5870;
  font-size: 0.88rem;
}

html[data-theme="dark"] .lc-rp-status {
  color: var(--pst-color-text-muted);
}

/* ------------------------------ */
/* Substitution diagrams          */
/* ------------------------------ */
.lc-subst-diagram {
  border: 1px solid var(--lc-panel-border);
  border-radius: 0.6rem;
  background: #fff;
  margin: 1rem 0;
  padding: 0.65rem 0.7rem 0.3rem 0.7rem;
}

html[data-theme="dark"] .lc-subst-diagram {
  background: var(--pst-color-surface);
  border-color: var(--pst-color-border);
}

.lc-subst-title {
  font-weight: 700;
  color: #1f3f5a;
  margin-bottom: 0.5rem;
}

html[data-theme="dark"] .lc-subst-title {
  color: var(--pst-color-text-base);
}

.lc-subst-row {
  display: flex;
  align-items: center;
  gap: 0.55rem;
  margin-bottom: 0.55rem;
  opacity: 0;
  transform: translateY(8px);
  transition: opacity 350ms ease, transform 350ms ease;
}

.lc-subst-row.in-view {
  opacity: 1;
  transform: translateY(0);
}

.lc-subst-box {
  border: 1px solid var(--lc-node-border);
  background: #f9fcff;
  border-radius: 0.45rem;
  padding: 0.35rem 0.45rem;
  font-family: "Times New Roman", "STIX Two Text", serif;
  font-size: 1rem;
  white-space: nowrap;
}

html[data-theme="dark"] .lc-subst-box {
  background: rgba(121, 163, 242, 0.08);
  border-color: var(--pst-color-border);
}

.lc-subst-arrow {
  color: #1f4d75;
  font-weight: 700;
  white-space: nowrap;
}

html[data-theme="dark"] .lc-subst-arrow {
  color: var(--pst-color-text-base);
}

/* ------------------------------ */
/* Reduction diffs (Python side)  */
/* ------------------------------ */
.lc-trace-table {
  width: 100%;
  border-collapse: collapse;
  margin: 0.8rem 0;
  font-size: 0.95rem;
}

.lc-trace-table th,
.lc-trace-table td {
  border: 1px solid #d4e3ef;
  padding: 0.35rem 0.45rem;
  vertical-align: top;
}

html[data-theme="dark"] .lc-trace-table th,
html[data-theme="dark"] .lc-trace-table td {
  border-color: var(--pst-color-border);
}

.lc-trace-table th {
  background: #eef5fb;
  color: #1f3a54;
  text-align: left;
}

html[data-theme="dark"] .lc-trace-table th {
  background: rgba(63, 177, 197, 0.12);
  color: var(--pst-color-text-base);
}

.lc-diff-panel {
  border: 1px solid #d4e3ef;
  background: #fbfdff;
  border-radius: 0.45rem;
  padding: 0.45rem 0.55rem;
  margin: 0.5rem 0;
}

html[data-theme="dark"] .lc-diff-panel {
  border-color: var(--pst-color-border);
  background: var(--pst-color-surface);
}

.lc-diff-del {
  background: #ffe3e3;
  border-bottom: 2px solid #d64545;
}

.lc-diff-ins {
  background: #e8f8e8;
  border-bottom: 2px solid #2f9a4f;
}

html[data-theme="dark"] .lc-diff-del {
  background: rgba(231, 136, 148, 0.2);
  border-bottom-color: var(--sd-color-danger);
}

html[data-theme="dark"] .lc-diff-ins {
  background: rgba(95, 180, 136, 0.2);
  border-bottom-color: var(--sd-color-success);
}

@keyframes lcFadeIn {
  from { opacity: 0; transform: translateY(6px); }
  to { opacity: 1; transform: translateY(0); }
}

@media (max-width: 1080px) {
  .lc-glossary-sidebar,
  .lc-glossary-toggle {
    display: none;
  }
}