function deduce (...ts) {
ts = ts.map(t => (t._proof || t.nodeName) ? t : html`<div>${t}</div>`);
const proof = html`<div class="proof"
style="display: inline-flex;
flex-direction: column;">
<div class="premises"
style="display: inline-flex;
flex-wrap: nowrap;
align-items: flex-end;
justify-content: center;
border-bottom: 2px solid #000;">
</div>
<div class="conclusion"
style="display: inline-flex;
margin-bottom: -2px;">
<div class="le" style="flex-grow: 1;"></div>
<div class="ct" style="margin-bottom: 2px;"></div>
<div class="ri" style="flex-grow: 1;"></div>
</div>
</div>`;
const conclusion = ts.pop();
proof.children[1].children[1].appendChild(conclusion);
const prem = proof.children[0];
ts.forEach((t, i) => {
prem.appendChild(t);
if (t._proof) {
if (i == 0) {
t.children[1].children[0].style['border-bottom'] = '2px solid #fff';
} else if (i+1 == ts.length) {
t.children[1].children[2].style['border-bottom'] = '2px solid #fff';
}
}
if (i + 1 < ts.length) {
prem.appendChild(html`<div class="premiss space" style="width: 2em;"></div>`);
}
});
proof._proof = true;
return proof;
}